OAI/Analysis/KadisonSimilarity/Tracial/UltrapowerTraceBalls.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.trace_sequence_norm_tendsto line 17
2. theorem OAI.KadisonSimilarity.exists_bounded_diagonal_trace_limit line 28

   Source documentation

   A rapidly converging sequence of uniformly bounded representatives has one bounded diagonal representative for its Hilbert-space limit.

   theorem exists_bounded_diagonal_trace_limit
       (hω : (ω : Filter ℕ) ≤ Filter.cofinite)
       (x : ℕ → (ℕ →ᵇ A)) (C : ℝ) (hC : 0 ≤ C) (hx : ∀ n, ‖x n‖ ≤ C)
       (ξ : (quotientTrace τ h1 ω htr).GNS)
       (hξ : ∀ n, dist (gnsTracialVector (quotientTrace τ h1 ω htr)
         (quotientHom τ h1 ω htr (x n))) ξ ≤ (1 / 2 : ℝ) ^ n) :
       ∃ y : ℕ →ᵇ A, ‖y‖ ≤ C ∧
         gnsTracialVector (quotientTrace τ h1 ω htr) (quotientHom τ h1 ω htr y) = ξ := by
   …

   Mentions: OAI.KadisonSimilarity.gnsTracialVector