FreeJointLaw.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The common joint trace law of a projection and a free Haar unitary

The paired-algebra argument applies the same finite normal forms to both representations. Its scalar coefficients depend only on the trace of the projection, so the two traces agree throughout the generated algebra and its norm closure.

def OAI.KadisonKastler.pairedHaarUnitary line 23
theorem OAI.KadisonKastler.pairedHaarPower_nat line 26
theorem OAI.KadisonKastler.pairedHaarPower line 33
theorem OAI.KadisonKastler.projectionNormalTail_pair line 42
theorem OAI.KadisonKastler.projectionNormalEval_pair line 52
def OAI.KadisonKastler.jointTraceDifference line 63
theorem OAI.KadisonKastler.trace_centered_normalWord line 67

theorem OAI.KadisonKastler.freeHaar_joint_trace_eq line 86

Source documentation

Equal projection traces determine the full algebraic joint trace law.

theorem freeHaar_joint_trace_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 ∈ Algebra.adjoin ℂ
      (insert (p, r) (Set.range (haarPower (pairedHaarUnitary u v))))) :
    τ.toLinearMap x.1 = σ.toLinearMap x.2 := by
…

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

def OAI.KadisonKastler.boundedTrace line 114

theorem OAI.KadisonKastler.freeHaar_joint_trace_eq_of_mem_closure line 119

Source documentation

The same joint law holds for norm limits, which includes the continuous functional-calculus operations used in the recovery contraction.

theorem freeHaar_joint_trace_eq_of_mem_closure
    (τ : 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 ∈ closure (Algebra.adjoin ℂ
      (insert (p, r) (Set.range (haarPower (pairedHaarUnitary u v)))) : Set (B × C))) :
    τ.toLinearMap x.1 = σ.toLinearMap x.2 := by
…

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