OAI/Analysis/KadisonSimilarity/Tracial/PredualGNSNormality.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A positive trace normal for a Banach predual has normal native GNS range. Bounded predual compactness and cyclic coefficients close the GNS trace-vector balls.

  1. theorem OAI.KadisonSimilarity.gnsCyclicSpace_eq_top line 21
  2. theorem OAI.KadisonSimilarity.gnsCyclic_coefficient_normal line 34
  3. theorem OAI.KadisonSimilarity.gnsVector_predual_tendsto line 48
  4. theorem OAI.KadisonSimilarity.predual_gns_trace_balls_closed line 58
  5. theorem OAI.KadisonSimilarity.hasNormalGNS_of_predual line 80

    Source documentation

    Banach-predual normality supplies exactly the GNS normality required by the finite-factor commutator argument.

    theorem hasNormalGNS_of_predual (hτ : TraceInPredual e τ)
    (htr : ∀ a b, τ (a * b) = τ (b * a)) : HasNormalGNS τ :=
…

    Mentions: OAI.KadisonSimilarity.HasNormalGNS