`BookProof.WallEsaBddBelow.wallHam_stone_flow_of_bddBelow` (V : ℝ → ℝ) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V) {c : ℝ} (hVc : ∀ x, -c ≤ V x) : ∃ (T :...

Proved

BookProof.WallEsaBddBelow.wallHam_stone_flow_of_bddBelow

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterWallEsaBddBelow.

BookProof.WallEsaBddBelow.wallHam_stone_flow_of_bddBelow (V : ℝ → ℝ) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V) {c : ℝ} (hVc : ∀ x, -c ≤ V x) : ∃ (T : UnboundedSelfAdjoint (Lp ℂ 2 (volume : Measure ℝ))) (U : ℝ → (Lp ℂ 2 (volume : Measure ℝ) →L[ℂ] Lp ℂ 2 (volume : Measure ℝ))), IsSelfAdjointExtension (wallHam V hV) T.op ∧ IsStoneFlow T U

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

Preamble

-- Generated from ChapterWallEsaBddBelow.lean — theorem BookProof.WallEsaBddBelow.wallHam_stone_flow_of_bddBelow
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterKatoRellichDeficiency
import Definitions.Def_ChapterKatoRellichDeficiencyCore
import Definitions.Def_ChapterSirkTrotterKato
import Mathlib
import Definitions.Def_ChapterWallEsaBddBelow
import Definitions.Def_ChapterEsaClosureCore
import Definitions.Def_ChapterScalaronCoreEsa
import Definitions.Def_ChapterScalaronWallEsa
import Definitions.Def_ChapterStoneBridge
import Definitions.Def_ChapterStoneResolvent
open BookProof.EsaClosure
open BookProof.ScalaronEsa
open BookProof.ScalaronWallEsa
open BookProof.StoneBridge
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.wallHam_stone_flow_of_bddBelow (V : ℝ → ℝ)
    (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V) {c : ℝ} (hVc : ∀ x, -c ≤ V x) :
    ∃ (T : UnboundedSelfAdjoint (Lp ℂ 2 (volume : Measure ℝ)))
      (U : ℝ → (Lp ℂ 2 (volume : Measure ℝ) →L[ℂ] Lp ℂ 2 (volume : Measure ℝ))),
      IsSelfAdjointExtension (wallHam V hV) T.op ∧ IsStoneFlow T U := by sorry

View graph