TracialDiagonalLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded diagonal limits in the tracial sequence quotient

theorem OAI.KadisonKastler.exists_tracial_diagonal_limit line 20

Source documentation

A uniformly bounded, rapidly two-Cauchy family has a coordinatewise diagonal representative with the same uniform bound.

theorem exists_tracial_diagonal_limit (hω : (ω : Filter ℕ) ≤ atTop)
    (x : ℕ → VaryingBoundedSequence B) (C : ℝ) (hC : 0 ≤ C)
    (hx : ∀ n j, ‖x n j‖ ≤ C) (a : ℕ → ℝ)
    (hfast : ∀ n m, n ≤ m → traceTwoNorm (tracialQuotientTrace τ ω)
      (tracialSequenceQuotientMap τ ω (x m) - tracialSequenceQuotientMap τ ω (x n)) < a n) :
    ∃ y : VaryingBoundedSequence B, ‖y‖ ≤ C ∧ ∀ n,
      traceTwoNorm (tracialQuotientTrace τ ω)
        (tracialSequenceQuotientMap τ ω y - tracialSequenceQuotientMap τ ω (x n)) ≤ a n := by
…

Mentions: OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.tracialQuotientTrace, OAI.KadisonKastler.tracialSequenceQuotientMap