OAI/Analysis/KadisonSimilarity/Tracial/TraceDenseContractions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A countable family of contractions dense for the trace norm.

  1. theorem OAI.KadisonSimilarity.exists_trace_dense_contractions line 17

    Source documentation

    Separability of the GNS space suffices; the algebra need not be norm separable.

    theorem exists_trace_dense_contractions [TopologicalSpace.SeparableSpace τ.GNS] :
    ∃ d : ℕ → B, (∀ n, ‖d n‖ ≤ 1) ∧
      ∀ b : B, ‖b‖ ≤ 1 → ∃ j : ℕ → ℕ,
        GNSTendsto τ (fun k => d (j k)) atTop b := by
…