OAI/Analysis/KadisonSimilarity/Tracial/ConjugateMomentCriterion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonSimilarity.conjugateMomentTail line 15
2. lemma OAI.KadisonSimilarity.conjugateMomentTail_admissible line 20
3. lemma OAI.KadisonSimilarity.conjugateMomentTail_nonzero line 27
4. def OAI.KadisonSimilarity.conjugateMomentBlock line 39
5. lemma OAI.KadisonSimilarity.conjugateMomentTail_eval line 43
6. lemma OAI.KadisonSimilarity.conjugate_blocks_zero line 54
7. lemma OAI.KadisonSimilarity.trace_conjugation line 72
8. lemma OAI.KadisonSimilarity.even_conjugate_blocks line 77
9. theorem OAI.KadisonSimilarity.scalarFree_conjugate_of_integer_moments line 112

   Source documentation

   The only moments needed for conjugate freeness are words with nonzero integer powers and centered coefficients in the original algebra.

   theorem scalarFree_conjugate_of_integer_moments
       (hm : ∀ a : Option B, ∀ l : List (IntAtom B), admissibleIntTail l →
         (∀ b ∈ l, b.1 ≠ 0) →
         σ (integerEval (fun b => φ b - σ (φ b) • 1) u a l) = 0) :
       ScalarFree σ φ.range
         (((Unitary.conjStarAlgAut ℂ C u).toStarAlgHom).comp φ).range := by
   …

   Mentions: OAI.KadisonSimilarity.ScalarFree