OAI/Analysis/KadisonKastler/TracialFiniteAveraging.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.traceStateVectorLinear line 18
2. def OAI.KadisonKastler.tracialFiniteAverage line 23
3. theorem OAI.KadisonKastler.tracialFiniteAverage_commutes line 27
4. theorem OAI.KadisonKastler.trace_tracialFiniteAverage line 43
5. theorem OAI.KadisonKastler.traceTwoNorm_sub_tracialFiniteAverage_le line 51
6. theorem OAI.KadisonKastler.exists_unitary_trace_variance_of_finite_group line 78

   Source documentation

   A finite matrix conjugation group with scalar commutant detects the tracial distance to scalars by one of its unitaries.

   theorem exists_unitary_trace_variance_of_finite_group (τ : FaithfulTracialState A)
       (ρ : G →* unitary A)
       (hscalar : ∀ a : A, (∀ g, Commute (ρ g : A) a) → ∃ c : ℂ, a = c • 1)
       (x : A) : ∃ u : unitary A,
         traceTwoNorm τ (x - τ.toLinearMap x • 1) ≤
           2 * traceTwoNorm τ ((u : A) * x - x * u) := by
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm