RecoveryJointLaw.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Equality of the actual recovery expression for free pairs

Continuous clipping stays in the closed algebra generated by the projection and the Haar unitary. The finite normal-word trace law therefore applies to the concrete recovery contraction, without a spectral premise.

def OAI.KadisonKastler.projectionHaarClosedAlgebra line 27
theorem OAI.KadisonKastler.projectionHaarClosedAlgebra_coe line 30
theorem OAI.KadisonKastler.projection_mem_projectionHaarClosedAlgebra line 51
theorem OAI.KadisonKastler.haarPower_mem_projectionHaarClosedAlgebra line 55
theorem OAI.KadisonKastler.unitaryHaarPolynomial_mem_projectionHaarClosedAlgebra line 60
theorem OAI.KadisonKastler.spectralClip_mem_closedStarSubalgebra line 70
theorem OAI.KadisonKastler.recoveryContraction_mem_closedStarSubalgebra line 80
theorem OAI.KadisonKastler.recoveryExpression_mem_projectionHaarClosedAlgebra line 89
theorem OAI.KadisonKastler.map_recoveryContraction line 107
theorem OAI.KadisonKastler.map_unitaryHaarPolynomial line 112

theorem OAI.KadisonKastler.freeHaar_joint_pairings_eq line 121

Source documentation

Both scalar pairings needed to identify the two affine expectation coefficients agree on the closed paired algebra.

theorem freeHaar_joint_pairings_eq
    (τ : FaithfulTracialState B) (σ : FaithfulTracialState C)
    {A : StarSubalgebra ℂ B} {D : StarSubalgebra ℂ C}
    {u : unitary B} {v : unitary C}
    (hu : FreeHaarMoments τ A u) (hv : FreeHaarMoments σ D v)
    {p : B} {r : C} (hp : IsStarProjection p) (hr : IsStarProjection r)
    (hpA : p ∈ A) (hrD : r ∈ D) {t : ℂ}
    (hpτ : τ.toLinearMap p = t) (hrσ : σ.toLinearMap r = t)
    {x : B × C}
    (hx : x ∈ projectionHaarClosedAlgebra (p, r) (pairedHaarUnitary u v)) :
    τ.toLinearMap x.1 = σ.toLinearMap x.2 ∧
      τ.toLinearMap (p * x.1) = σ.toLinearMap (r * x.2) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.projectionHaarClosedAlgebra, OAI.KadisonKastler.pairedHaarUnitary

theorem OAI.KadisonKastler.freeHaar_recovery_pairings_eq line 148

Source documentation

The actual clipped recovery expressions have identical traces for any two free projection--Haar pairs with equal projection traces.

theorem freeHaar_recovery_pairings_eq
    (τ : FaithfulTracialState B) (σ : FaithfulTracialState C)
    {A : StarSubalgebra ℂ B} {D : StarSubalgebra ℂ C}
    {u : unitary B} {v : unitary C}
    (hu : FreeHaarMoments τ A u) (hv : FreeHaarMoments σ D v)
    {p : B} {r : C} (hp : IsStarProjection p) (hr : IsStarProjection r)
    (hpA : p ∈ A) (hrD : r ∈ D) {t : ℂ}
    (hpτ : τ.toLinearMap p = t) (hrσ : σ.toLinearMap r = t)
    {n : ℕ} (hn : 0 < n) (N : ℕ) :
    τ.toLinearMap (unitaryHaarPolynomial N u *
      recoveryContraction n p (unitaryHaarPolynomial N u) * unitaryHaarPolynomial N u) =
    σ.toLinearMap (unitaryHaarPolynomial N v *
…

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

theorem OAI.KadisonKastler.freeHaar_recovery_trace_eq line 182