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

Proved

BookProof.WallEsaBddBelow.oscillatorPlus_esa

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterWallEsaBddBelow.

BookProof.WallEsaBddBelow.oscillatorPlus_esa (V : ℝ → ℝ) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V) {c : ℝ} (hVc : ∀ x, -c ≤ V x) : EssentiallySelfAdjointOn (ccDomain ℝ) (wallHam (fun x => x ^ 2 / 4 + V x) (((contDiff_id.pow 2).div_const 4).add hV))

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

Preamble

-- Generated from ChapterWallEsaBddBelow.lean — theorem BookProof.WallEsaBddBelow.oscillatorPlus_esa
import Definitions.Def_ChapterFarisLavine
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
import Definitions.Def_ChapterFarisLavineCore
import Definitions.Def_ChapterScalaronCoreEsa
import Definitions.Def_ChapterScalaronWallEsa
open BookProof.ScalaronEsa
open BookProof.ScalaronWallEsa
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.oscillatorPlus_esa (V : ℝ → ℝ) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
    {c : ℝ} (hVc : ∀ x, -c ≤ V x) :
    EssentiallySelfAdjointOn (ccDomain ℝ)
      (wallHam (fun x => x ^ 2 / 4 + V x)
        (((contDiff_id.pow 2).div_const 4).add hV)) := by sorry

View graph