test module
Tests.ProximalBPSDefectComplexLift
0 named declarations scanned from Tests/ProximalBPSDefectComplexLift.lean.
Declarations
This aggregator contains no named declarations.
Complete Lean source
Tests/ProximalBPSDefectComplexLift.lean — full module with imports and context
import AutoSamplingTheory.ExampleCases.ProximalBPS.DefectComplexLift
import Mathlib.Analysis.InnerProductSpace.StarOrder
import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
open MeasureTheory
open scoped ENNReal ContinuousFunctionalCalculus NonUnitalContinuousFunctionalCalculus
set_option maxHeartbeats 1000000
/- The complex CFC API is genuinely available after the positive L2 lift.
This checks a complex square root only. Preservation of the real fixed
subspace and descent to the paper's real Gamma remain separate obligations. -/
example {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
(D : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hD : D.IsPositive) :
let ι : Lp ℝ 2 μ →L[ℝ] Lp ℂ 2 μ := Complex.ofRealCLM.compLpL 2 μ
∃ Dc : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ,
Dc.IsPositive ∧ (∀ u : Lp ℝ 2 μ, Dc (ι u) = ι (D u)) ∧
∃ Rc : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ, 0 ≤ Rc ∧ Rc*Rc = Dc := 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 μ)
dsimp only
obtain ⟨hι,hfixed,Dc,hpos,hformula,hintertwine,hconj⟩ :=
AutoSamplingTheory.TechnicalLemmas.Measure.L2RealComplexOperator.exists_positive_complex_lift μ D hD
have hnonneg : 0 ≤ Dc := (ContinuousLinearMap.nonneg_iff_isPositive Dc).mpr hpos
exact ⟨Dc,hpos,hintertwine,CFC.sqrt Dc,CFC.sqrt_nonneg Dc,CFC.sqrt_mul_sqrt_self Dc hnonneg⟩
#check AutoSamplingTheory.ExampleCases.ProximalBPS.DefectComplexLift.actual_positive_defect_complex_lift