Positive square order on arbitrary real L²

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang provide Appendix D.1 spectral-calculus and unique nonnegative-root background. The displayed arbitrary-real-L2 square-order statement is an ASTIS auxiliary corollary using Mathlib CFC monotonicity and canonical complexification, not a separately printed D.1 theorem.

Complete source statement (Samplinglib restatement)

For any measurable space Ω and any measure μ, let A and B be bounded real linear operators on real L²(μ). If A and B are positive (selfadjoint with nonnegative quadratic form) and B²−A² is positive, then B−A is positive. No finiteness or probability of μ, nontriviality, finite-dimensional L², commutation, or caller CFC instance is assumed. This is an ASTIS auxiliary consequence of positive square-root monotonicity, realized by the canonical complexification of real L²; it is consumed by the actual centered-root result.

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Positive square order on arbitrary real L²

AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareOrder.positive_square_order · theorem · Teaching coverage

Read this first

Mathematical statement

\[A\ge0,\ B\ge0,\ B^2-A^2\ge0\Rightarrow B-A\ge0.\]

Lean statement · positive_square_order

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 positive_square_order
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (A B : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ)
    (hA : A.IsPositive) (hB : B.IsPositive)
    (hSquareOrder : (B*B-A*A).IsPositive) :
    (B-A).IsPositive

Exact module and namespace context

Proof roadmap

1Complexify the three real positive operators
Use canonical real and imaginary decompositions for A, B and D=B²−A². Positivity is preserved. Applying the decompositions twice identifies the third lift with B_C²−A_C²; the two square lifts therefore inherit the correct order.
2Apply monotonicity to positive square roots
The complex operator algebra supplies its internal CFC instances, also in the trivial-space case. Monotonicity gives √(A_C²)≤√(B_C²); uniqueness of the positive roots identifies them with A_C and B_C. No commutation between A and B is used.
3Descend through the canonical real embedding
The real embedding preserves the real part of the complex inner product and intertwines both operators. Positivity of B_C−A_C restricted to embedded real vectors gives the required nonnegative quadratic form; symmetry descends from the original positives.

Full assumptions and notation

All objects and hypotheses

Arbitrary measurable space and measure; bounded real operators A,B on real L²; A,B and B²−A² positive. No commutation, finiteness, probability, finite-dimensional L² or nontriviality premise.

Mathematical proof

1. Complexify the three real positive operators

Use canonical real and imaginary decompositions for A, B and D=B²−A². Positivity is preserved. Applying the decompositions twice identifies the third lift with B_C²−A_C²; the two square lifts therefore inherit the correct order.

\[D=B^2-A^2\ge0,\quad D_C=B_C^2-A_C^2\ge0.\]

Corresponding Lean step

  letI : NormedSpace ℝ (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) :=
    NormedSpace.restrictScalars ℝ ℂ (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ)
  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 μ)
  let ι : Lp ℝ 2 μ →L[ℝ] Lp ℂ 2 μ := Complex.ofRealCLM.compLpL 2 μ
  let R : Lp ℂ 2 μ →L[ℝ] Lp ℝ 2 μ := Complex.reCLM.compLpL 2 μ
  let Q : Lp ℂ 2 μ →L[ℝ] Lp ℝ 2 μ := Complex.imCLM.compLpL 2 μ
  obtain ⟨hNorm,_,Ac,hAc,hAf,hAi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ A hA
  obtain ⟨_,_,Bc,hBc,hBf,hBi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ B hB
  obtain ⟨_,_,Dc,hDc,hDf,hDi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ (B*B-A*A) hSquareOrder
  have hAi' (u : Lp ℝ 2 μ) : Ac (ι u)=ι (A u) := hAi u
  have hBi' (u : Lp ℝ 2 μ) : Bc (ι u)=ι (B u) := hBi u
  have hComplexDiff : Bc*Bc-Ac*Ac=Dc := by
    apply ContinuousLinearMap.ext
    intro g
    change Bc (Bc g) - Ac (Ac g)=Dc g
    rw [hBf g,hAf g,map_add,map_smul,map_add,map_smul,hBi,hBi,hAi,hAi,hDf g]
    simp only [ContinuousLinearMap.sub_apply,ContinuousLinearMap.mul_apply,map_sub,smul_sub]
    abel

Literal excerpt of the compiled declaration; preceding local definitions and proved facts remain in scope.

2. Apply monotonicity to positive square roots

The complex operator algebra supplies its internal CFC instances, also in the trivial-space case. Monotonicity gives √(A_C²)≤√(B_C²); uniqueness of the positive roots identifies them with A_C and B_C. No commutation between A and B is used.

\[A_C^2\le B_C^2\Rightarrow A_C=\sqrt{A_C^2}\le\sqrt{B_C^2}=B_C.\]

Corresponding Lean step

  have hAcNonneg : 0 ≤ Ac := (ContinuousLinearMap.nonneg_iff_isPositive Ac).mpr hAc
  have hBcNonneg : 0 ≤ Bc := (ContinuousLinearMap.nonneg_iff_isPositive Bc).mpr hBc
  have hSqLe : Ac*Ac ≤ Bc*Bc := by
    apply (ContinuousLinearMap.le_def _ _).mpr
    rw [hComplexDiff]
    exact hDc
  have hLe : Ac ≤ Bc := by
    have h := CFC.sqrt_le_sqrt (Ac*Ac) (Bc*Bc) hSqLe
    have ha : CFC.sqrt (Ac*Ac)=Ac := CFC.sqrt_unique rfl hAcNonneg
    have hb : CFC.sqrt (Bc*Bc)=Bc := CFC.sqrt_unique rfl hBcNonneg
    exact ha.symm.le.trans (h.trans hb.le)
  have hDiff : (Bc-Ac).IsPositive := (ContinuousLinearMap.le_def _ _).mp hLe

Literal excerpt of the compiled declaration; preceding local definitions and proved facts remain in scope.

3. Descend through the canonical real embedding

The real embedding preserves the real part of the complex inner product and intertwines both operators. Positivity of B_C−A_C restricted to embedded real vectors gives the required nonnegative quadratic form; symmetry descends from the original positives.

\[\langle(B-A)u,u\rangle_{\mathbb R}=\Re\langle(B_C-A_C)\iota u,\iota u\rangle_{\mathbb C}\ge0.\]

Corresponding Lean step

  letI : InnerProductSpace ℝ (Lp ℂ 2 μ) := InnerProductSpace.rclikeToReal ℂ (Lp ℂ 2 μ)
  let e : Lp ℝ 2 μ →ₗᵢ[ℝ] Lp ℂ 2 μ :=
    { toLinearMap := ι.toLinearMap, norm_map' := hNorm }
  have hInner (v w : Lp ℝ 2 μ) : RCLike.re (inner ℂ (ι v) (ι w))=inner ℝ v w := by
    rw [← real_inner_eq_re_inner]
    exact e.inner_map_map v w
  refine ⟨hB.isSymmetric.sub hA.isSymmetric,?_⟩
  intro u
  have h := hDiff.re_inner_nonneg_left (ι u)
  have hAction : (Bc-Ac) (ι u)=ι ((B-A) u) := by
    simp only [ContinuousLinearMap.sub_apply,hBi',hAi',map_sub]
  rw [hAction,hInner] at h
  exact h

Literal excerpt of the compiled declaration; preceding local definitions and proved facts remain in scope.

Lean verification

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

Lean proof · positive_square_order

Complexify the three real positive operators; Apply monotonicity to positive square roots; Descend through the canonical real embedding

Download module (.lean)

theorem positive_square_order
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (A B : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ)
    (hA : A.IsPositive) (hB : B.IsPositive)
    (hSquareOrder : (B*B-A*A).IsPositive) :
    (B-A).IsPositive := by
  letI : NormedSpace ℝ (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) :=
    NormedSpace.restrictScalars ℝ ℂ (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ)
  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 μ)
  let ι : Lp ℝ 2 μ →L[ℝ] Lp ℂ 2 μ := Complex.ofRealCLM.compLpL 2 μ
  let R : Lp ℂ 2 μ →L[ℝ] Lp ℝ 2 μ := Complex.reCLM.compLpL 2 μ
  let Q : Lp ℂ 2 μ →L[ℝ] Lp ℝ 2 μ := Complex.imCLM.compLpL 2 μ
  obtain ⟨hNorm,_,Ac,hAc,hAf,hAi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ A hA
  obtain ⟨_,_,Bc,hBc,hBf,hBi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ B hB
  obtain ⟨_,_,Dc,hDc,hDf,hDi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ (B*B-A*A) hSquareOrder
  have hAi' (u : Lp ℝ 2 μ) : Ac (ι u)=ι (A u) := hAi u
  have hBi' (u : Lp ℝ 2 μ) : Bc (ι u)=ι (B u) := hBi u
  have hComplexDiff : Bc*Bc-Ac*Ac=Dc := by
    apply ContinuousLinearMap.ext
    intro g
    change Bc (Bc g) - Ac (Ac g)=Dc g
    rw [hBf g,hAf g,map_add,map_smul,map_add,map_smul,hBi,hBi,hAi,hAi,hDf g]
    simp only [ContinuousLinearMap.sub_apply,ContinuousLinearMap.mul_apply,map_sub,smul_sub]
    abel
  have hAcNonneg : 0 ≤ Ac := (ContinuousLinearMap.nonneg_iff_isPositive Ac).mpr hAc
  have hBcNonneg : 0 ≤ Bc := (ContinuousLinearMap.nonneg_iff_isPositive Bc).mpr hBc
  have hSqLe : Ac*Ac ≤ Bc*Bc := by
    apply (ContinuousLinearMap.le_def _ _).mpr
    rw [hComplexDiff]
    exact hDc
  have hLe : Ac ≤ Bc := by
    have h := CFC.sqrt_le_sqrt (Ac*Ac) (Bc*Bc) hSqLe
    have ha : CFC.sqrt (Ac*Ac)=Ac := CFC.sqrt_unique rfl hAcNonneg
    have hb : CFC.sqrt (Bc*Bc)=Bc := CFC.sqrt_unique rfl hBcNonneg
    exact ha.symm.le.trans (h.trans hb.le)
  have hDiff : (Bc-Ac).IsPositive := (ContinuousLinearMap.le_def _ _).mp hLe
  letI : InnerProductSpace ℝ (Lp ℂ 2 μ) := InnerProductSpace.rclikeToReal ℂ (Lp ℂ 2 μ)
  let e : Lp ℝ 2 μ →ₗᵢ[ℝ] Lp ℂ 2 μ :=
    { toLinearMap := ι.toLinearMap, norm_map' := hNorm }
  have hInner (v w : Lp ℝ 2 μ) : RCLike.re (inner ℂ (ι v) (ι w))=inner ℝ v w := by
    rw [← real_inner_eq_re_inner]
    exact e.inner_map_map v w
  refine ⟨hB.isSymmetric.sub hA.isSymmetric,?_⟩
  intro u
  have h := hDiff.re_inner_nonneg_left (ι u)
  have hAction : (Bc-Ac) (ι u)=ι ((B-A) u) := by
    simp only [ContinuousLinearMap.sub_apply,hBi',hAi',map_sub]
  rw [hAction,hInner] at h
  exact h

end
end AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareOrder

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Arbitrary measurable space and measure; bounded real operators A,B on real L²; A,B and B²−A² positive. No commutation, finiteness, probability, finite-dimensional L² or nontriviality premise.	Arbitrary measurable space and measure; bounded real operators A,B on real L²; A,B and B²−A² positive. No commutation, finiteness, probability, finite-dimensional L² or nontriviality premise.	same	Exact independently reviewed preproof statement; all implementation adapters remain internal.
Remaining paper results and actual-input expected costs.	Reusable real-L2 positive-square-order consequence only; no general Hilbert CFC public premise or independent algorithm result.	unresolved	This bounded edge is not the full paper or cost/composition theorem.

Reusable real-L2 positive-square-order consequence only; no general Hilbert CFC public premise or independent algorithm result.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Reusable real-L2 positive-square-order consequence only; no general Hilbert CFC public premise or independent algorithm result.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Measure.L2RealComplexOperator.exists_positive_complex_lift

Mathlib API called (external library)

CFC.sqrt_le_sqrt
CFC.sqrt_unique

Mathematical sources

Appendix D.1 bounded selfadjoint spectral calculus and unique nonnegative square root; ASTIS auxiliary real-L2 square-order corollary via Mathlib CFC monotonicity, consumed by B.15 — Reusable real-L2 positive-square-order consequence only; no general Hilbert CFC public premise or independent algorithm result.

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

Positive square order on arbitrary real L²

Complete source statement (Samplinglib restatement)

Positive square order on arbitrary real L²

Read the formalized proofs

Positive square order on arbitrary real L²

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Complexify the three real positive operators

2. Apply monotonicity to positive square roots

3. Descend through the canonical real embedding

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?