OAI/Analysis/KadisonKastler/ClosedExpectation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.FreeHaarMoments.expectation_eq_affine_projection_of_mem_closure line 17

   Source documentation

   Continuity extends the algebraic normal-form conclusion to the closed algebra generated by the projection and the Haar unitary.

   theorem FreeHaarMoments.expectation_eq_affine_projection_of_mem_closure
       {τ : FaithfulTracialState B} {A : StarSubalgebra ℂ B} {v : unitary B}
       (h : FreeHaarMoments τ A v)
       (E : B →L[ℂ] B) (hE : ∀ x, E x ∈ A)
       (hpair : ∀ b ∈ A, ∀ x, τ.toLinearMap (b * E x) = τ.toLinearMap (b * x))
       {p x : B} (hp : IsStarProjection p) (hpA : p ∈ A)
       (hx : x ∈ closure (Algebra.adjoin ℂ (insert p (Set.range (haarPower v))) : Set B)) :
       ∃ α β : ℂ, E x = α • p + β • (1 : B) := by
   …

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

2. theorem OAI.KadisonKastler.affine_projection_coefficients_unique_between_traces line 40

   Source documentation

   The two trace pairings determine the affine coefficients whenever the projection has trace strictly between zero and one.

   theorem affine_projection_coefficients_unique_between_traces
       {C : Type*} [CStarAlgebra C]
       (τ : FaithfulTracialState B) (σ : FaithfulTracialState C)
       {p : B} {q : C} (hp : IsStarProjection p) (hq : IsStarProjection q)
       {t α β γ δ : ℂ} (ht0 : t ≠ 0) (ht1 : t ≠ 1)
       (hpτ : τ.toLinearMap p = t) (hqσ : σ.toLinearMap q = t)
       (htrace : τ.toLinearMap (α • p + β • (1 : B)) =
         σ.toLinearMap (γ • q + δ • (1 : C)))
       (hptrace : τ.toLinearMap (p * (α • p + β • (1 : B))) =
         σ.toLinearMap (q * (γ • q + δ • (1 : C)))) :
       α = γ ∧ β = δ := by
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState