OAI/Analysis/KadisonSimilarity/Tracial/DenseMomentExtension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KadisonSimilarity.gnsTendsto_tracePreserving line 21
2. lemma OAI.KadisonSimilarity.norm_centered_contraction line 27
3. theorem OAI.KadisonSimilarity.integer_moments_of_trace_dense line 37

   Source documentation

   No norm separability is required. The approximating family is dense only in the trace norm on the unit ball.

   theorem integer_moments_of_trace_dense
       (d : ℕ → B) (hd : ∀ n, ‖d n‖ ≤ 1)
       (hdense : ∀ b : B, ‖b‖ ≤ 1 → ∃ j : ℕ → ℕ,
         GNSTendsto τ (fun k => d (j k)) atTop b)
       (u : unitary C)
       (hm : ∀ a : Option ℕ, ∀ l : List (IntAtom ℕ), admissibleIntTail l →
         (∀ b ∈ l, b.1 ≠ 0) →
         σ (integerEval (fun n => φ (d n) - σ (φ (d n)) • 1) u a l) = 0)
       (A : I → B) (hA : ∀ i, ‖A i‖ ≤ 1)
       (a : Option I) (l : List (IntAtom I)) (hl : admissibleIntTail l)
       (hk : ∀ b ∈ l, b.1 ≠ 0) :
       σ (integerEval (fun i => φ (A i) - σ (φ (A i)) • 1) u a l) = 0 := by
   …

4. theorem OAI.KadisonSimilarity.all_integer_moments_of_trace_dense line 83

   Source documentation

   Scaling each coefficient separately removes the contraction restriction.

   theorem all_integer_moments_of_trace_dense
       (d : ℕ → B) (hd : ∀ n, ‖d n‖ ≤ 1)
       (hdense : ∀ b : B, ‖b‖ ≤ 1 → ∃ j : ℕ → ℕ,
         GNSTendsto τ (fun k => d (j k)) atTop b)
       (u : unitary C)
       (hm : ∀ a : Option ℕ, ∀ l : List (IntAtom ℕ), admissibleIntTail l →
         (∀ b ∈ l, b.1 ≠ 0) →
         σ (integerEval (fun n => φ (d n) - σ (φ (d n)) • 1) u a l) = 0)
       (A : I → B) (a : Option I) (l : List (IntAtom I)) (hl : admissibleIntTail l)
       (hk : ∀ b ∈ l, b.1 ≠ 0) :
       σ (integerEval (fun i => φ (A i) - σ (φ (A i)) • 1) u a l) = 0 := by
   …