exists_positive_real_square_root

Plain-English statement

Independently exact-science61 verified bcd245d90b21b899acb9937fc54dffcea20e86ee. Arbitrary measure and bounded positive real D; actual complex CFC root, conjugated-root positivity and uniqueness establish pointwise conjugation preservation; full fixed-space descent produces bounded positive REAL Gamma, Gamma squared equals D and full-domain quadratic energy. No finite/probability measure, finite L2, nontriviality or caller CFC/root certificate. Exported real uniqueness, joint GammaP/ontoM/typed B*B, centered root order/inverse/polar, weakH1/dynamics/main/error/cost/composition remain open.

Lean statement

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

Open AutoSamplingTheory/TechnicalLemmas/Measure/L2RealSquareRoot.lean:94published source at ed709a7f320d

Proof architecture

Actual PBPS consumer; no SALD admission

Lean proof walkthrough

• Read the quantified variables and typeclass brackets as part of the mathematical statement; inferred arguments are not missing assumptions.
• `intro` introduces quantified hypotheses into the local proof context.
• `have` creates a named intermediate mathematical fact.
• `calc` records an equality or inequality chain matching a paper calculation.
• `rw` rewrites by an established identity.
• `apply` reduces the goal to the hypotheses of a reusable theorem.
• `refine` instantiates a reusable theorem while leaving explicit subgoals.
• `exact` closes the current goal with an already typed term.

Why the statement has this shape

The declaration is kept at the reusable level recorded by its Registry tags and direct consumers. Explicit measures, spaces, wrappers, and regularity hypotheses expose interfaces that paper notation often infers. A theorem card explains those interfaces but never widens the compiled statement.

Hidden assumptions and non-claims

• Measurability is represented explicitly or must be supplied by a dependency.