`BookProof.QgOuterFockFL.Comparison.selfAdjoint` (C : Comparison F) (w u : F) (hw : ∀ v : C.dom, (inner ℂ (C.op v) w : ℂ) = inner ℂ (v : F) u) : ∃ h : w ∈ C.dom, C.op ⟨w, h⟩ = u

Proved

BookProof.QgOuterFockFL.Comparison.selfAdjoint

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterQgOuterFockFarisLavine.

BookProof.QgOuterFockFL.Comparison.selfAdjoint (C : Comparison F) (w u : F) (hw : ∀ v : C.dom, (inner ℂ (C.op v) w : ℂ) = inner ℂ (v : F) u) : ∃ h : w ∈ C.dom, C.op ⟨w, h⟩ = u

Formalization note: Lean 4 identifier BookProof.QgOuterFockFL.Comparison.selfAdjoint.

Preamble

-- Generated from ChapterQgOuterFockFarisLavine.lean — theorem BookProof.QgOuterFockFL.Comparison.selfAdjoint
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
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]

Formal statement

theorem BookProof.QgOuterFockFL.Comparison.selfAdjoint (C : Comparison F) (w u : F)
    (hw : ∀ v : C.dom, (inner ℂ (C.op v) w : ℂ) = inner ℂ (v : F) u) :
    ∃ h : w ∈ C.dom, C.op ⟨w, h⟩ = u := by sorry

View graph