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

L2RealSquareRootUnique: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Positive real L² operators: equality from equal squares
Samplinglib mathematical lesson

Positive real L² operators: equality from equal squares

AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRootUnique.positive_square_roots_unique · theorem · Teaching coverage

Read this first

Mathematical statement

Let Ω be any measurable space, μ any measure, and A,B bounded positive real-linear operators on L²(μ;ℝ). Assume A²=B², where multiplication is composition. Then A=B. Positivity is symmetry plus nonnegative quadratic form on the complete real L² space. No finite/probability measure, finite-dimensional L², nontriviality, energy identity or real/complex CFC/extension certificate is assumed.

\[A\ge0,\quad B\ge0,\quad A^2=B^2\quad\Longrightarrow\quad A=B.\]
Lean statement · positive_square_roots_unique

Let Ω be any measurable space, μ any measure, and A,B bounded positive real-linear operators on L²(μ;ℝ). Assume A²=B², where multiplication is composition. Then A=B. Positivity is symmetry plus nonnegative quadratic form on the complete real L² space. No finite/probability measure, finite-dimensional L², nontriviality, energy identity or real/complex CFC/extension certificate is assumed.

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

Exact module and namespace context

Proof roadmap

  1. 1Lift both positive real operators canonically

    Use the compiled shared positive complex lift twice over the SAME arbitrary measure. The actual quotient maps ι,R,Q are identical in both results. The internally produced positive complex Ac,Bc satisfy Acι=ιA, Bcι=ιB and the literal coordinate formula for every complex L² class. The same theorem proves ‖ιu‖=‖u‖.

  2. 2Transport equality of squares

    Complex linearity and intertwining give Ac²g=ι(A²Rg)+iι(A²Qg), and the corresponding formula for Bc. The original equality A²=B² applies separately to Rg and Qg, giving Ac²=Bc² on every complex class. No multiplicativity or decomposition certificate is a public premise.

  3. 3Apply complex positive-root uniqueness internally

    The fixed Mathlib complex operator algebra provides complex functional calculus and its restricted real selfadjoint instance internally. Both positive Ac and Bc equal the positive square root of their common square by CFC.sqrt_unique. Hence Ac=Bc. This requires no real functional-calculus instance on the original operator algebra.

  4. 4Recover equality of the real operators

    Norm preservation constructs a real-linear isometry e=ι, so ι is injective. Evaluate Ac=Bc on ιu; intertwining gives ιAu=ιBu, then injectivity gives Au=Bu for every real L² class. Extensionality proves A=B, including zero/subsingleton spaces.

Full assumptions and notation

All objects and hypotheses

  • Let Ω be any measurable space, μ any measure, and A,B bounded positive real-linear operators on L²(μ;ℝ). Assume A²=B², where multiplication is composition. Then A=B. Positivity is symmetry plus nonnegative quadratic form on the complete real L² space. No finite/probability measure, finite-dimensional L², nontriviality, energy identity or real/complex CFC/extension certificate is assumed.
  • Arbitrary measure, including zero/subsingleton/infinite-dimensional L²; no energy, CFC, complex extension or norm-preserving embedding certificate supplied.

Mathematical proof

1. Lift both positive real operators canonically

Use the compiled shared positive complex lift twice over the SAME arbitrary measure. The actual quotient maps ι,R,Q are identical in both results. The internally produced positive complex Ac,Bc satisfy Acι=ιA, Bcι=ιB and the literal coordinate formula for every complex L² class. The same theorem proves ‖ιu‖=‖u‖.

\[A_{\mathbb C},B_{\mathbb C}\ge0,\quad A_{\mathbb C}\iota=\iota A,\quad B_{\mathbb C}\iota=\iota B,\quad\|\iota u\|=\|u\|.\]
Corresponding Lean step

L2RealComplexOperator.exists_positive_complex_lift; hNorm; hAf; hBf; hAi; hBi

2. Transport equality of squares

Complex linearity and intertwining give Ac²g=ι(A²Rg)+iι(A²Qg), and the corresponding formula for Bc. The original equality A²=B² applies separately to Rg and Qg, giving Ac²=Bc² on every complex class. No multiplicativity or decomposition certificate is a public premise.

\[A_{\mathbb C}^2g=\iota A^2Rg+i\iota A^2Qg=\iota B^2Rg+i\iota B^2Qg=B_{\mathbb C}^2g.\]
Corresponding Lean step

hReal; hComplexSquare; map_add; map_smul; ContinuousLinearMap.ext

3. Apply complex positive-root uniqueness internally

The fixed Mathlib complex operator algebra provides complex functional calculus and its restricted real selfadjoint instance internally. Both positive Ac and Bc equal the positive square root of their common square by CFC.sqrt_unique. Hence Ac=Bc. This requires no real functional-calculus instance on the original operator algebra.

\[A_{\mathbb C}=\sqrt{B_{\mathbb C}^2}=B_{\mathbb C}.\]
Corresponding Lean step

hAcNonneg; hBcNonneg; CFC.sqrt_unique; hSame

4. Recover equality of the real operators

Norm preservation constructs a real-linear isometry e=ι, so ι is injective. Evaluate Ac=Bc on ιu; intertwining gives ιAu=ιBu, then injectivity gives Au=Bu for every real L² class. Extensionality proves A=B, including zero/subsingleton spaces.

\[\iota Au=A_{\mathbb C}\iota u=B_{\mathbb C}\iota u=\iota Bu\quad\Longrightarrow\quad A=B.\]
Corresponding Lean step

e; LinearIsometry.injective; hAi; hBi; ContinuousLinearMap.ext

Lean verification

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

Lean proof · positive_square_roots_unique

Lift both positive real operators canonically; Transport equality of squares; Apply complex positive-root uniqueness internally; Recover equality of the real operators

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_roots_unique
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (A B : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ)
    (hA : A.IsPositive) (hB : B.IsPositive) (hSq : A*A=B*B) :
    A=B := 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,_,Ac,hAc,hAf,hAi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ A hA
  obtain ⟨_,_,Bc,hBc,hBf,hBi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ B hB
  have hReal (u : Lp ℝ 2 μ) : A (A u) = B (B u) :=
    congrArg (fun D : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ => D u) hSq
  have hComplexSquare : Ac*Ac = Bc*Bc := by
    apply ContinuousLinearMap.ext
    intro g
    change Ac (Ac g) = Bc (Bc g)
    calc
      Ac (Ac g) = ι (A (A (R g))) + Complex.I • ι (A (A (Q g))) := by
        rw [hAf g, map_add, map_smul, hAi, hAi]
      _ = ι (B (B (R g))) + Complex.I • ι (B (B (Q g))) := by
        rw [hReal (R g),hReal (Q g)]
      _ = Bc (Bc g) := by rw [hBf g, map_add, map_smul, hBi, hBi]
  have hAcNonneg : 0 ≤ Ac := (ContinuousLinearMap.nonneg_iff_isPositive Ac).mpr hAc
  have hBcNonneg : 0 ≤ Bc := (ContinuousLinearMap.nonneg_iff_isPositive Bc).mpr hBc
  have hSame : Ac = Bc :=
    (CFC.sqrt_unique hComplexSquare hAcNonneg).symm.trans (CFC.sqrt_unique rfl hBcNonneg)
  let e : Lp ℝ 2 μ →ₗᵢ[ℝ] Lp ℂ 2 μ :=
    { toLinearMap := ι.toLinearMap
      norm_map' := hNorm }
  apply ContinuousLinearMap.ext
  intro u
  apply e.injective
  change ι (A u) = ι (B u)
  rw [← hAi u, ← hBi u, hSame]

end
end AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRootUnique

#print axioms AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRootUnique.positive_square_roots_unique

Exact module and namespace context

Scope and omitted-condition boundaries
  • Exported real scalar uniqueness and genuine original-input same defect/root only. Printed joint GammaP/ontoM/typed B*B, centered order/inverse/polar/H1/dynamics/main/cost/composition remain separate.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • ContinuousLinearMap.ext
  • map_add
  • map_smul
  • ContinuousLinearMap.nonneg_iff_isPositive
  • CFC.sqrt_unique
  • LinearIsometry.injective

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.