HaarRecovery.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Scalar recovery from the actual Haar polynomial

The scalar trace formula for the arc projection combines with the geometric-sum tail, tracial normalization, and compression estimates to recover scalar coefficients.

theorem OAI.KadisonKastler.haar_recovery_at_least_half line 23

Source documentation

The actual polynomial and the constructed corner contraction recover at least one half of the identity's scalar coefficient.

theorem haar_recovery_at_least_half
    (τ : FaithfulTracialState (Algebra M)) (u : unitary (Algebra M))
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower u k) = 0)
    {n N : ℕ} (hn : 0 < n)
    (hsize : 100 * (n : ℝ) * (100 * Real.pi) ^ 3 ≤ N)
    {A : StarSubalgebra ℂ (Algebra M)} (huA : (u : Algebra M) ∈ A)
    (p e : Algebra M) (hp : IsStarProjection p) (he : IsStarProjection e)
    (heA : e ∈ A)
    (hcomm : Commute (unitaryHaarPolynomial N u) e)
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ))
    (heτ : τ.toLinearMap e = ((100 / (N : ℝ) : ℝ) : ℂ))
    (hind : ProjectionTraceIndependent τ p A)
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.unitaryHaarPolynomial, OAI.KadisonKastler.ProjectionTraceIndependent