OAI/Analysis/KadisonSimilarity/Tracial/TracialMomentContinuity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KadisonSimilarity.gnsTendsto_smul line 17
2. lemma OAI.KadisonSimilarity.gnsTendsto_centered line 24
3. lemma OAI.KadisonSimilarity.wordCoeff_norm_le_bound line 35
4. lemma OAI.KadisonSimilarity.gnsTendsto_wordCoeff line 41
5. lemma OAI.KadisonSimilarity.gnsTendsto_integerEval line 49
6. theorem OAI.KadisonSimilarity.integer_moment_zero_of_bounded_limits line 73

   Source documentation

   Vanishing moments persist when each coefficient is approximated in trace norm with a common operator-norm bound.

   theorem integer_moment_zero_of_bounded_limits
       {F : ℕ → I → B} {G : I → B}
       (h : ∀ i, GNSTendsto τ (fun j => F j i) atTop (G i))
       {C : ℝ} (hC : 1 ≤ C) (hF : ∀ j i, ‖F j i‖ ≤ C)
       (u : unitary B) (a : Option I) (w : List (IntAtom I))
       (hz : ∀ j, τ (integerEval (F j) u a w) = 0) :
       τ (integerEval G u a w) = 0 := by
   …