Samplinglib mathematical lesson

Positive real L² operator: genuine square root and energy

AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRoot.exists_positive_real_square_root · theorem · Teaching coverage

Read this first

Mathematical statement

Let Ω be an arbitrary measurable space and μ any measure. Let D be a bounded positive real-linear operator on L²(μ;ℝ); positivity includes selfadjointness. There exists a bounded positive REAL operator Γ with Γ²=D, and for EVERY real L² class u, ‖Γu‖²=⟨Du,u⟩ℝ. No CFC instance, complex extension, root, finite/probability measure or finite-dimensional L² is a hypothesis.

\[\Gamma\ge0,\quad\Gamma^2=D,\quad\forall u\in L^2(\mu;\mathbb R),\ \|\Gamma u\|^2=\langle Du,u\rangle_{\mathbb R}.\]

Lean statement · exists_positive_real_square_root

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem exists_positive_real_square_root
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (D : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hD : D.IsPositive) :
    ∃ Γ : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ,
      Γ.IsPositive ∧ Γ*Γ = D ∧
      ∀ u : Lp ℝ 2 μ, ‖Γ u‖^2 = inner ℝ (D u) u

Exact module and namespace context

Proof roadmap

1Reuse the genuine positive complex lift
The compiled canonical complexification theorem constructs ι, the real-part map R, pointwise conjugation C and positive complex-linear Dc from D. It proves Fix(C)=ran(ι) and Dcι=ιD internally. All maps act on actual AE classes for the same arbitrary measure.
2Establish the antiunitary quotient identities
Pointwise scalar conjugation lifted by compLpL satisfies C²=I, C(cg)=conj(c)Cg and ⟨Cg,Ch⟩ℂ=conj(⟨g,h⟩ℂ). The AE formulas and conjugation of the Bochner integral establish these identities without choosing additional representatives. Also Rι=I and the embedding preserves the integral inner product.
3Construct the complex positive square root internally
On the complex L² operator algebra the pinned Mathlib supplies complex CFC, and its restricted-real selfadjoint CFC is explicitly target-typed inside the proof. Thus Rc=sqrt(Dc) is positive and Rc²=Dc. This derives the needed instance rather than adding a real functional-calculus premise to the theorem.
4Prove root preservation by positive-root uniqueness
K=CRcC is bounded and complex-linear because conjugation reverses complex scalars twice. Its quadratic form is the conjugate of the nonnegative real quadratic form of Rc at Cg, so K is positive. C²=I and CDc=DcC give K²=Dc. Uniqueness of the complex positive square root gives K=Rc, hence CRc=RcC. This is pointwise conjugation, never operator adjoint.
5Descend to the full real L² space
Define the bounded real map Γ=R Rc ι. Since Rc preserves Fix(C), its value Rcιu lies in the full image of ι. The identity Rι=I then gives ιΓu=Rcιu. Applying this twice and using Dcι=ιD proves Γ²=D, with embedding injectivity. Real uniqueness and the centered restriction are separate statements.
6Transport positivity and derive the energy identity
The embedding preserves inner products. Therefore complex selfadjointness and positivity of Rc imply real selfadjointness and positivity of Γ. Its symmetry and exact square now yield ‖Γu‖²=⟨Γu,Γu⟩ℝ=⟨Γ²u,u⟩ℝ=⟨Du,u⟩ℝ for every u. No invertibility or strict positive lower bound follows on the full space.

Full assumptions and notation

All objects and hypotheses

Let Ω be an arbitrary measurable space and μ any measure. Let D be a bounded positive real-linear operator on L²(μ;ℝ); positivity includes selfadjointness. There exists a bounded positive REAL operator Γ with Γ²=D, and for EVERY real L² class u, ‖Γu‖²=⟨Du,u⟩ℝ. No CFC instance, complex extension, root, finite/probability measure or finite-dimensional L² is a hypothesis.
No finite/probability measure, finite-dimensional L², nontriviality, CFC/root or conjugation-preservation input.
Pointwise conjugation is antiunitary on complex L² and differs from operator adjoint; its root-preservation and the descent are proved internally.

Mathematical proof

1. Reuse the genuine positive complex lift

The compiled canonical complexification theorem constructs ι, the real-part map R, pointwise conjugation C and positive complex-linear Dc from D. It proves Fix(C)=ran(ι) and Dcι=ιD internally. All maps act on actual AE classes for the same arbitrary measure.

\[D_{\mathbb C}\ge0,\quad D_{\mathbb C}\iota=\iota D,\quad\operatorname{Fix}(C)=\operatorname{ran}(\iota).\]

Corresponding Lean step

L2RealComplexOperator.exists_positive_complex_lift; hfixed; hintertwine

2. Establish the antiunitary quotient identities

Pointwise scalar conjugation lifted by compLpL satisfies C²=I, C(cg)=conj(c)Cg and ⟨Cg,Ch⟩ℂ=conj(⟨g,h⟩ℂ). The AE formulas and conjugation of the Bochner integral establish these identities without choosing additional representatives. Also Rι=I and the embedding preserves the integral inner product.

\[C^2=I,\quad C(cg)=\overline c\,Cg,\quad\langle Cg,Ch\rangle_{\mathbb C}=\overline{\langle g,h\rangle_{\mathbb C}},\quad R\iota=I.\]

Corresponding Lean step

conjugate_involutive; conjugate_smul; inner_conjugate; real_embed; inner_embed

3. Construct the complex positive square root internally

On the complex L² operator algebra the pinned Mathlib supplies complex CFC, and its restricted-real selfadjoint CFC is explicitly target-typed inside the proof. Thus Rc=sqrt(Dc) is positive and Rc²=Dc. This derives the needed instance rather than adding a real functional-calculus premise to the theorem.

\[R_{\mathbb C}=\sqrt{D_{\mathbb C}}\ge0,\quad R_{\mathbb C}^2=D_{\mathbb C}.\]

Corresponding Lean step

hRcNonneg; hRc; hRcSq; CFC.sqrt_nonneg; CFC.sqrt_mul_sqrt_self

4. Prove root preservation by positive-root uniqueness

K=CRcC is bounded and complex-linear because conjugation reverses complex scalars twice. Its quadratic form is the conjugate of the nonnegative real quadratic form of Rc at Cg, so K is positive. C²=I and CDc=DcC give K²=Dc. Uniqueness of the complex positive square root gives K=Rc, hence CRc=RcC. This is pointwise conjugation, never operator adjoint.

\[K=CR_{\mathbb C}C\ge0,\quad K^2=D_{\mathbb C},\quad K=R_{\mathbb C},\quad CR_{\mathbb C}=R_{\mathbb C}C.\]

Corresponding Lean step

conjugateOperator; conjugateOperator_positive; hKSq; hK; CFC.sqrt_unique; hrootConj

5. Descend to the full real L² space

Define the bounded real map Γ=R Rc ι. Since Rc preserves Fix(C), its value Rcιu lies in the full image of ι. The identity Rι=I then gives ιΓu=Rcιu. Applying this twice and using Dcι=ιD proves Γ²=D, with embedding injectivity. Real uniqueness and the centered restriction are separate statements.

\[\Gamma=RR_{\mathbb C}\iota,\quad\iota\Gamma=R_{\mathbb C}\iota,\quad\Gamma^2=D.\]

Corresponding Lean step

Γ; hbridge; hinj; hΓSq

6. Transport positivity and derive the energy identity

The embedding preserves inner products. Therefore complex selfadjointness and positivity of Rc imply real selfadjointness and positivity of Γ. Its symmetry and exact square now yield ‖Γu‖²=⟨Γu,Γu⟩ℝ=⟨Γ²u,u⟩ℝ=⟨Du,u⟩ℝ for every u. No invertibility or strict positive lower bound follows on the full space.

\[\Gamma\ge0,\quad\|\Gamma u\|^2=\langle\Gamma^2u,u\rangle_{\mathbb R}=\langle Du,u\rangle_{\mathbb R}.\]

Corresponding Lean step

inner_embed; hΓ; hΓSq; real_inner_self_eq_norm_sq

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · exists_positive_real_square_root

Reuse the genuine positive complex lift; Establish the antiunitary quotient identities; Construct the complex positive square root internally; Prove root preservation by positive-root uniqueness; Descend to the full real L² space; Transport positivity and derive the energy identity

Download module (.lean)

theorem exists_positive_real_square_root
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (D : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hD : D.IsPositive) :
    ∃ Γ : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ,
      Γ.IsPositive ∧ Γ*Γ = D ∧
      ∀ u : Lp ℝ 2 μ, ‖Γ u‖^2 = inner ℝ (D u) u := by
  letI := IsStarNormal.instNonUnitalContinuousFunctionalCalculus
    (A := Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ)
  letI : NonUnitalContinuousFunctionalCalculus ℂ
      (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) IsStarNormal :=
    NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus
  letI : NonUnitalContinuousFunctionalCalculus ℝ
      (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) IsSelfAdjoint :=
    IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus
    (A := Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ)
  obtain ⟨hnorm,hfixed,Dc,hDc,hformula,hintertwine,hconj⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ D hD
  let Rc : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ := CFC.sqrt Dc
  have hDcNonneg : 0 ≤ Dc := (ContinuousLinearMap.nonneg_iff_isPositive Dc).mpr hDc
  have hRcNonneg : 0 ≤ Rc := CFC.sqrt_nonneg Dc
  have hRc : Rc.IsPositive := (ContinuousLinearMap.nonneg_iff_isPositive Rc).mp hRcNonneg
  have hRcSq : Rc*Rc = Dc := CFC.sqrt_mul_sqrt_self Dc hDcNonneg
  have hKSq : conjugateOperator μ Rc * conjugateOperator μ Rc = Dc := by
    apply ContinuousLinearMap.ext
    intro g
    change conjugate μ (Rc (conjugate μ (conjugate μ (Rc (conjugate μ g))))) = Dc g
    rw [conjugate_involutive]
    have hpoint : Rc (Rc (conjugate μ g)) = Dc (conjugate μ g) :=
      congrArg (fun A : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ => A (conjugate μ g)) hRcSq
    rw [hpoint, hconj, conjugate_involutive]
  have hKNonneg : 0 ≤ conjugateOperator μ Rc :=
    (ContinuousLinearMap.nonneg_iff_isPositive _).mpr (conjugateOperator_positive μ Rc hRc)
  have hK : conjugateOperator μ Rc = Rc := (CFC.sqrt_unique hKSq hKNonneg).symm
  have hrootConj (g : Lp ℂ 2 μ) : conjugate μ (Rc g) = Rc (conjugate μ g) := by
    have hh := congrArg (fun A : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ => A (conjugate μ g)) hK
    change conjugate μ (Rc (conjugate μ (conjugate μ g))) = Rc (conjugate μ g) at hh
    simpa only [conjugate_involutive] using hh
  let Γ : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ :=
    realPart μ ∘L Rc.restrictScalars ℝ ∘L embed μ
  have hbridge (u : Lp ℝ 2 μ) : embed μ (Γ u) = Rc (embed μ u) := by
    have hf : conjugate μ (embed μ u) = embed μ u := (hfixed _).mpr ⟨u,rfl⟩
    have hr : conjugate μ (Rc (embed μ u)) = Rc (embed μ u) := by rw [hrootConj, hf]
    obtain ⟨v,hv⟩ := (hfixed _).mp hr
    change embed μ (realPart μ (Rc (embed μ u))) = Rc (embed μ u)
    rw [← hv, real_embed]
  have hinj : Function.Injective (embed μ) := by
    intro u v h
    have hh := congrArg (realPart μ) h
    simpa only [real_embed] using hh
  have hΓSq : Γ*Γ = D := by
    apply ContinuousLinearMap.ext
    intro u
    apply hinj
    change embed μ (Γ (Γ u)) = embed μ (D u)
    rw [hbridge (Γ u),hbridge u]
    have hp : Rc (Rc (embed μ u)) = Dc (embed μ u) :=
      congrArg (fun A : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ => A (embed μ u)) hRcSq
    exact hp.trans (hintertwine u)
  have hΓ : Γ.IsPositive := by
    constructor
    · intro u v
      have hh := hRc.inner_left_eq_inner_right (embed μ u) (embed μ v)
      rw [← hbridge u, ← hbridge v, inner_embed, inner_embed] at hh
      exact Complex.ofReal_injective hh
    · intro u
      have hh := hRc.re_inner_nonneg_left (embed μ u)
      rw [← hbridge u, inner_embed] at hh
      simpa [ContinuousLinearMap.reApplyInnerSelf] using hh
  refine ⟨Γ,hΓ,hΓSq,?_⟩
  intro u
  calc
    ‖Γ u‖^2 = inner ℝ (Γ u) (Γ u) := (real_inner_self_eq_norm_sq _).symm
    _ = inner ℝ (Γ (Γ u)) u := (hΓ.inner_left_eq_inner_right (Γ u) u).symm
    _ = inner ℝ (D u) u := by
      change inner ℝ ((Γ*Γ) u) u = inner ℝ (D u) u
      rw [hΓSq]


end
end AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRoot

#print axioms AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRoot.exists_positive_real_square_root

Exact module and namespace context

Scope and omitted-condition boundaries

REAL scalar positive root and scalar energy only. Generic real uniqueness, canonical joint GammaP / P U blocks / onto transport / typed B*B, centered root order/inverse/polar, weakH1,dynamics,hypocoercivity,main,error,cost,composition remain separate; paper/Goal open.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Measure.L2RealComplexOperator.exists_positive_complex_lift

Mathlib API called (external library)

ContinuousLinearMap.compLpL
ContinuousLinearMap.coeFn_compLpL
Lp.ext
L2.inner_def
Complex.conjCLE.integral_comp_comm
ContinuousLinearMap.isPositive_iff_complex
ContinuousLinearMap.nonneg_iff_isPositive
CFC.sqrt_nonneg
CFC.sqrt_mul_sqrt_self
CFC.sqrt_unique
RCLike.re_to_complex
real_inner_self_eq_norm_sq

Mathematical sources

Appendix D.1 positive real square-root background; B.10-B.11 scalar defect energy precursor. ASTIS background completion, not printed joint GammaP. — REAL scalar positive root and scalar energy only. Generic real uniqueness, canonical joint GammaP / P U blocks / onto transport / typed B*B, centered root order/inverse/polar, weakH1,dynamics,hypocoercivity,main,error,cost,composition remain separate; paper/Goal open.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.