`BookProof.QgOuterFockFL.dsFibOp_essentiallySelfAdjointOn` [∀ i, CompleteSpace (G i)] {K c : ℝ} (hc : 0 ≤ c) (hrel : ∀ (i : ι) (u : (C i).dom), ‖H i u‖ ≤ K * ‖(C i).op u + (u : G i

Proved

BookProof.QgOuterFockFL.dsFibOp_essentiallySelfAdjointOn

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterQgOuterFockFarisLavine.

BookProof.QgOuterFockFL.dsFibOp_essentiallySelfAdjointOn [∀ i, CompleteSpace (G i)] {K c : ℝ} (hc : 0 ≤ c) (hrel : ∀ (i : ι) (u : (C i).dom), ‖H i u‖ ≤ K * ‖(C i).op u + (u : G i)‖) (hsym : ∀ i, SymmetricOn (C i).dom (H i)) (hcomm : ∀ (i : ι) (u : (C i).dom), |commForm (H i) (C i).op u| ≤ c * quadForm (C i).op u) : EssentiallySelfAdjointOn (dsDom C) (dsFibOp C H K hrel)

Formalization note: Lean 4 identifier BookProof.QgOuterFockFL.dsFibOp_essentiallySelfAdjointOn.

Preamble

-- Generated from ChapterQgOuterFockFarisLavine.lean — theorem BookProof.QgOuterFockFL.dsFibOp_essentiallySelfAdjointOn
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterDirectSumEsa
import Definitions.Def_ChapterQgOuterFockEsa
import Definitions.Def_ChapterYangMillsFriedrichs
import Definitions.Def_ChapterFriedrichsExtension
import Definitions.Def_ChapterComplexShiftCore
import Definitions.Def_ChapterQgHermiteOscillatorEsa
import Definitions.Def_ChapterHermiteProductCore
import Mathlib
import Definitions.Def_ChapterQgOuterFockFarisLavine
import Definitions.Def_ChapterFarisLavineCore
open BookProof.QgOuterFockFL


open scoped ENNReal


open BookProof.FarisLavine
open BookProof.DirectSumEsa
open BookProof.QgOuterFock
open BookProof.YangMillsFriedrichs
open BookProof.FriedrichsExtension
open BookProof.FriedrichsExtension.FormDom
open BookProof.HashimotoShiftInvert
open BookProof.QgHermiteOscillator
open BookProof.HermiteProductCore

noncomputable section

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable {ι : Type*} {G : ι → Type*} [∀ i, NormedAddCommGroup (G i)]
  [∀ i, InnerProductSpace ℂ (G i)]
variable (C : ∀ i, Comparison (G i))
variable (H : ∀ i, (C i).dom →ₗ[ℂ] G i)
variable {C H}

Formal statement

theorem BookProof.QgOuterFockFL.dsFibOp_essentiallySelfAdjointOn [∀ i, CompleteSpace (G i)] {K c : ℝ} (hc : 0 ≤ c)
    (hrel : ∀ (i : ι) (u : (C i).dom), ‖H i u‖ ≤ K * ‖(C i).op u + (u : G i)‖)
    (hsym : ∀ i, SymmetricOn (C i).dom (H i))
    (hcomm : ∀ (i : ι) (u : (C i).dom), |commForm (H i) (C i).op u| ≤ c * quadForm (C i).op u) :
    EssentiallySelfAdjointOn (dsDom C) (dsFibOp C H K hrel) := by sorry

View graph