`BookProof.WallEsaBddBelow.constOp_symmetric` (c : ℝ) (x y : Lp ℂ 2 (volume : Measure ℝ)) : (inner ℂ (constOp c x) y : ℂ) = inner ℂ x (constOp c y)

Proved

BookProof.WallEsaBddBelow.constOp_symmetric

by leonardopedro · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterWallEsaBddBelow.

BookProof.WallEsaBddBelow.constOp_symmetric (c : ℝ) (x y : Lp ℂ 2 (volume : Measure ℝ)) : (inner ℂ (constOp c x) y : ℂ) = inner ℂ x (constOp c y)

Formalization note: Lean 4 identifier BookProof.WallEsaBddBelow.constOp_symmetric.

Preamble

-- Generated from ChapterWallEsaBddBelow.lean — theorem BookProof.WallEsaBddBelow.constOp_symmetric
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterScalaronCoreEsa
import Definitions.Def_ChapterScalaronWallEsa
import Definitions.Def_ChapterKatoRellichDeficiency
import Definitions.Def_ChapterKatoRellichDeficiencyCore
import Definitions.Def_ChapterStoneBridge
import Definitions.Def_ChapterEsaClosureCore
import Definitions.Def_ChapterSirkTrotterKato
import Mathlib
import Definitions.Def_ChapterWallEsaBddBelow
open BookProof.WallEsaBddBelow



open MeasureTheory SchwartzMap Set
open BookProof.FarisLavine BookProof.ScalaronEsa BookProof.ScalaronWallEsa
open BookProof.KatoRellich BookProof.StoneBridge BookProof.EsaClosure
open BookProof.ChapterStoneResolvent

noncomputable section

Formal statement

theorem BookProof.WallEsaBddBelow.constOp_symmetric (c : ℝ) (x y : Lp ℂ 2 (volume : Measure ℝ)) :
    (inner ℂ (constOp c x) y : ℂ) = inner ℂ x (constOp c y) := by sorry

View graph