ConcreteHaarRecovery.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Scalar recovery from a free Haar unitary

The spectral arc, its trace, the two centered projection moments and the tail identity are constructed from the actual unitary. The conclusion uses the explicit continuous corner contraction, with no spectral projection or freeness consequence left as an auxiliary premise.

theorem OAI.KadisonKastler.concrete_haar_recovery_at_least_half line 24

Source documentation

The explicit Haar-polynomial contraction recovers at least one half of the scalar, using only the free Haar moments and the finite-vector trace.

theorem concrete_haar_recovery_at_least_half
    (τ : FaithfulTracialState (Algebra M)) (hτ : FiniteVectorTrace τ)
    (u : unitary (Algebra M)) {Base : StarSubalgebra ℂ (Algebra M)}
    (hfree : FreeHaarMoments τ Base u)
    {n N : ℕ} (hn : 0 < n)
    (hsize : 100 * (n : ℝ) * (100 * Real.pi) ^ 3 ≤ N)
    (p : Algebra M) (hp : IsStarProjection p) (hpBase : p ∈ Base)
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ)) :
    1 / 2 ≤ (τ.toLinearMap ((n : ℂ) •
      (unitaryHaarPolynomial N u * recoveryContraction n p (unitaryHaarPolynomial N u) *
        unitaryHaarPolynomial N u))).re := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.unitaryHaarPolynomial, OAI.KadisonKastler.recoveryContraction

theorem OAI.KadisonKastler.concrete_haar_recovery line 69

Source documentation

Complete scalar-recovery data for the actual corner contraction.

theorem concrete_haar_recovery
    (τ : FaithfulTracialState (Algebra M)) (hτ : FiniteVectorTrace τ)
    (u : unitary (Algebra M)) {Base : StarSubalgebra ℂ (Algebra M)}
    (hfree : FreeHaarMoments τ Base u)
    {n N : ℕ} (hn : 0 < n)
    (hsize : 100 * (n : ℝ) * (100 * Real.pi) ^ 3 ≤ N)
    (p : Algebra M) (hp : IsStarProjection p) (hpBase : p ∈ Base)
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ)) :
    ‖recoveryContraction n p (unitaryHaarPolynomial N u)‖ ≤ 1 ∧
      p * recoveryContraction n p (unitaryHaarPolynomial N u) =
        recoveryContraction n p (unitaryHaarPolynomial N u) ∧
      recoveryContraction n p (unitaryHaarPolynomial N u) * p =
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.recoveryContraction, OAI.KadisonKastler.unitaryHaarPolynomial