Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Positive square commutation on arbitrary real L²

Fan Chen,Sinho Chewi,Jianfeng Lu and Matthew S. Zhang supply Appendix D.1 spectral-calculus background. This ASTIS auxiliary real-L2 corollary uses pinned Mathlib CFC and local complexification;it is not a separately printed theorem.

arXiv:2609.06905v1;Lean4.33.0/fixedMathlib · PBPS2609.06905v1 Appendix D.1 spectral calculus background;ASTIS positive real-L2 square commutation corollary for B23/B21. · faithful paraphrase

Complete source statement (Samplinglib restatement)

For every measurable space Ω and every measure μ,let G,D be bounded real linear operators on real L²(μ). Assume G,D positive:selfadjoint with nonnegative quadratic form. If G²D=DG²,then GD=DG. No probability,finite measure,finite-dimensional L²,nontriviality or caller CFC instance is required. This ASTIS auxiliary consequence of unique positive-root functional calculus is not a separately printed PBPS theorem. Its actual paper consumer internally proves D=I+T positive and G² commuting with D;these are not extra paper premises.

  • Arbitrary measurable space and measure;bounded positive real operators G,D on real L²;Commute(G²,D). No CFC/finiteness/nontriviality premise.

Positive square commutation on arbitrary real L²

\[G,D\ge0,\quad[G^2,D]=0\Longrightarrow[G,D]=0.\]

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 commutation on arbitrary real L²

AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareCommute.positive_square_commutation · theorem · Teaching coverage

Read this first

Mathematical statement

For every measurable space Ω and every measure μ,let G,D be bounded real linear operators on real L²(μ). Assume G,D positive:selfadjoint with nonnegative quadratic form. If G²D=DG²,then GD=DG. No probability,finite measure,finite-dimensional L²,nontriviality or caller CFC instance is required. This ASTIS auxiliary consequence of unique positive-root functional calculus is not a separately printed PBPS theorem. Its actual paper consumer internally proves D=I+T positive and G² commuting with D;these are not extra paper premises.

\[G,D\ge0,\quad[G^2,D]=0\Longrightarrow[G,D]=0.\]
Lean statement · positive_square_commutation

For every measurable space Ω and every measure μ,let G,D be bounded real linear operators on real L²(μ). Assume G,D positive:selfadjoint with nonnegative quadratic form. If G²D=DG²,then GD=DG. No probability,finite measure,finite-dimensional L²,nontriviality or caller CFC instance is required. This ASTIS auxiliary consequence of unique positive-root functional calculus is not a separately printed PBPS theorem. Its actual paper consumer internally proves D=I+T positive and G² commuting with D;these are not extra paper premises.

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_commutation
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (G D : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ)
    (hG : G.IsPositive) (hD : D.IsPositive)
    (hCommute : Commute (G*G) D) : Commute G D

Exact module and namespace context

Proof roadmap

  1. 1Complexify the positive operators

    Use the existing canonical complex lift,its action on every complex vector and the norm-preserving real embedding.

  2. 2Lift square commutation

    Apply the real identity separately to real and imaginary parts and use complex linearity;this proves equality of full complex operators.

  3. 3Commute with the same positive square root

    The unique positive root of Gc² is Gc. Commutation with the argument passes to its continuous functional calculus.

  4. 4Descend by injectivity

    Evaluate on the embedded real vector;exact intertwining and norm-injectivity recover real commutation.

Full assumptions and notation

All objects and hypotheses

  • Arbitrary measurable space and measure;bounded positive real operators G,D on real L²;Commute(G²,D). No CFC/finiteness/nontriviality premise.

Mathematical proof

1. Complexify the positive operators

Use the existing canonical complex lift,its action on every complex vector and the norm-preserving real embedding.

\[G_{\mathbb C}\iota u=\iota Gu,\quad D_{\mathbb C}\iota u=\iota Du,\quad\|\iota u\|=\|u\|.\]
Corresponding Lean step
  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,_,Gc,hGc,hGf,hGi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ G hG
  obtain ⟨_,_,Dc,hDc,hDf,hDi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ D hD

Literal compiled BODY span;exact preceding locals remain in scope.

2. Lift square commutation

Apply the real identity separately to real and imaginary parts and use complex linearity;this proves equality of full complex operators.

\[G^2D=DG^2\Rightarrow G_{\mathbb C}^2D_{\mathbb C}=D_{\mathbb C}G_{\mathbb C}^2.\]
Corresponding Lean step
  have hReal (u : Lp ℝ 2 μ) : G (G (D u)) = D (G (G u)) :=
    congrArg (fun A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ => A u) hCommute.eq
  have hComplex : Commute (Gc*Gc) Dc := by
    apply ContinuousLinearMap.ext
    intro g
    change Gc (Gc (Dc g)) = Dc (Gc (Gc g))
    calc
      Gc (Gc (Dc g)) = ι (G (G (D (R g)))) + Complex.I • ι (G (G (D (Q g)))) := by
        rw [hDf g, map_add, map_smul, hGi, hGi, map_add, map_smul, hGi, hGi]
      _ = ι (D (G (G (R g)))) + Complex.I • ι (D (G (G (Q g)))) := by
        rw [hReal (R g),hReal (Q g)]
      _ = Dc (Gc (Gc g)) := by
        rw [hGf g,map_add,map_smul,hGi,hGi,map_add,map_smul,hDi,hDi]

Literal compiled BODY span;exact preceding locals remain in scope.

3. Commute with the same positive square root

The unique positive root of Gc² is Gc. Commutation with the argument passes to its continuous functional calculus.

\[\sqrt{G_{\mathbb C}^2}=G_{\mathbb C},\quad[G_{\mathbb C}^2,D_{\mathbb C}]=0\Rightarrow[G_{\mathbb C},D_{\mathbb C}]=0.\]
Corresponding Lean step
  have hGcNonneg : 0 ≤ Gc := (ContinuousLinearMap.nonneg_iff_isPositive Gc).mpr hGc
  have hRoot : CFC.sqrt (Gc*Gc)=Gc := CFC.sqrt_unique rfl hGcNonneg
  have hLift : Commute Gc Dc := by
    have h := hComplex.cfcₙ_nnreal NNReal.sqrt
    change Commute (CFC.sqrt (Gc*Gc)) Dc at h
    rwa [hRoot] at h

Literal compiled BODY span;exact preceding locals remain in scope.

4. Descend by injectivity

Evaluate on the embedded real vector;exact intertwining and norm-injectivity recover real commutation.

\[\iota GD u=G_{\mathbb C}D_{\mathbb C}\iota u=D_{\mathbb C}G_{\mathbb C}\iota u=\iota DG u\Rightarrow GD=DG.\]
Corresponding Lean step
  let e : Lp ℝ 2 μ →ₗᵢ[ℝ] Lp ℂ 2 μ :=
    { toLinearMap := ι.toLinearMap, norm_map' := hNorm }
  apply ContinuousLinearMap.ext
  intro u
  apply e.injective
  change ι (G (D u))=ι (D (G u))
  rw [← hGi (D u), ← hDi u, ← hDi (G u), ← hGi u]
  exact congrArg (fun A : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ => A (ι u)) hLift.eq

Literal compiled BODY span;exact preceding locals 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_commutation

Complexify the positive operators; Lift square commutation; Commute with the same positive square root; Descend by injectivity

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_commutation
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (G D : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ)
    (hG : G.IsPositive) (hD : D.IsPositive)
    (hCommute : Commute (G*G) D) : Commute G D
 := 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 μ)
  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,_,Gc,hGc,hGf,hGi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ G hG
  obtain ⟨_,_,Dc,hDc,hDf,hDi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ D hD
  have hReal (u : Lp ℝ 2 μ) : G (G (D u)) = D (G (G u)) :=
    congrArg (fun A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ => A u) hCommute.eq
  have hComplex : Commute (Gc*Gc) Dc := by
    apply ContinuousLinearMap.ext
    intro g
    change Gc (Gc (Dc g)) = Dc (Gc (Gc g))
    calc
      Gc (Gc (Dc g)) = ι (G (G (D (R g)))) + Complex.I • ι (G (G (D (Q g)))) := by
        rw [hDf g, map_add, map_smul, hGi, hGi, map_add, map_smul, hGi, hGi]
      _ = ι (D (G (G (R g)))) + Complex.I • ι (D (G (G (Q g)))) := by
        rw [hReal (R g),hReal (Q g)]
      _ = Dc (Gc (Gc g)) := by
        rw [hGf g,map_add,map_smul,hGi,hGi,map_add,map_smul,hDi,hDi]
  have hGcNonneg : 0 ≤ Gc := (ContinuousLinearMap.nonneg_iff_isPositive Gc).mpr hGc
  have hRoot : CFC.sqrt (Gc*Gc)=Gc := CFC.sqrt_unique rfl hGcNonneg
  have hLift : Commute Gc Dc := by
    have h := hComplex.cfcₙ_nnreal NNReal.sqrt
    change Commute (CFC.sqrt (Gc*Gc)) Dc at h
    rwa [hRoot] at h
  let e : Lp ℝ 2 μ →ₗᵢ[ℝ] Lp ℂ 2 μ :=
    { toLinearMap := ι.toLinearMap, norm_map' := hNorm }
  apply ContinuousLinearMap.ext
  intro u
  apply e.injective
  change ι (G (D u))=ι (D (G u))
  rw [← hGi (D u), ← hDi u, ← hDi (G u), ← hGi u]
  exact congrArg (fun A : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ => A (ι u)) hLift.eq

end
end AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareCommute

#print axioms AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareCommute.positive_square_commutation

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Arbitrary measurable space and measure;bounded positive real operators G,D on real L²;Commute(G²,D). No CFC/finiteness/nontriviality premise.Arbitrary measurable space and measure;bounded positive real operators G,D on real L²;Commute(G²,D). No CFC/finiteness/nontriviality premise.sameExact independently reviewed header;all actual operator facts are conclusions.
Remaining sharp B23/B21/full dynamics and expected costs/composition.ASTIS auxiliary on arbitrary real L2;positivity of D is not a PBPS caller premise. Actual D=I+T positivity is internally produced.unresolvedBounded commutation/coefficient ingredient only.

ASTIS auxiliary on arbitrary real L2;positivity of D is not a PBPS caller premise. Actual D=I+T positivity is internally produced.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • scopes: ASTIS auxiliary expands D1 spectral background to arbitrary real L2;not printed standalone PBPS. — D1 spectral calculus/unique positive root accurately attributed; exact source URL corrected separately; no source mathematical repair.

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
  • ASTIS auxiliary on arbitrary real L2;positivity of D is not a PBPS caller premise. Actual D=I+T positivity is internally produced.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Commute.cfcₙ_nnreal
  • CFC.sqrt_unique
  • ContinuousLinearMap.ext

Mathematical sources

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

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Positive square commutation on arbitrary real L²
  • TODO — not closed by these contributions Remaining sharp energy,rotation,dynamics,mixing,errors and expected costs/composition