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

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

1Complexify the positive operators
Use the existing canonical complex lift,its action on every complex vector and the norm-preserving real embedding.
2Lift square commutation
Apply the real identity separately to real and imaginary parts and use complex linearity;this proves equality of full complex operators.
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.
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

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

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

AutoSamplingTheory.TechnicalLemmas.Measure.L2RealComplexOperator.exists_positive_complex_lift

Mathlib API called (external library)

Commute.cfcₙ_nnreal
CFC.sqrt_unique
ContinuousLinearMap.ext

Mathematical sources

PBPS2609.06905v1 Appendix D.1 spectral calculus background;ASTIS positive real-L2 square commutation corollary for B23/B21. — ASTIS auxiliary on arbitrary real L2;positivity of D is not a PBPS caller premise. Actual D=I+T positivity is internally produced.

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