OAI/Analysis/KadisonSimilarity/Tracial/SourceQuotientMoments.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Vanishing ultrapower moments produced by a sequence of source unitaries.

  1. lemma OAI.KadisonSimilarity.source_map_asPartialUnitary line 18
  2. theorem OAI.KadisonSimilarity.exists_centered_source_moment_sequence line 41
  3. theorem OAI.KadisonSimilarity.exists_source_quotient_unitary_moments line 63

    Source documentation

    A sequence from the source annihilates all fixed finite quotient words in a countable family of centered ambient bounded sequences.

    theorem exists_source_quotient_unitary_moments
    (ω : Ultrafilter ℕ) (hω : (ω : Filter ℕ) ≤ atTop)
    (A : ℕ → (ℕ →ᵇ M.toStarSubalgebra)) (hA : ∀ i n, ‖A i n‖ ≤ 1) :
    ∃ u : ℕ → unitary R.toStarSubalgebra,
      FiniteQuotientMoments (B := M.toStarSubalgebra) (vectorPositiveFunctional M υ.vector) υ.trace_one ω υ.trace_mul_comm
…

    Mentions: OAI.KadisonSimilarity.FiniteQuotientMoments, OAI.KadisonSimilarity.vectorPositiveFunctional