OAI/Analysis/KadisonKastler/MinimalRowFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Minimal compact invariant families for normalized row averaging.

  1. def OAI.KadisonKastler.RowInvariant line 21
  2. theorem OAI.KadisonKastler.rowInvariant_sInter line 26
  3. theorem OAI.KadisonKastler.rowInvariant_closure_orbit line 34
  4. theorem OAI.KadisonKastler.exists_minimal_row_family line 41

    Source documentation

    Compactness and Zorn's lemma give a genuine minimal invariant family. This theorem does not assert that the family is a singleton.

    theorem exists_minimal_row_family {M : VonNeumannAlgebra H} {c : ℝ} (hc : 0 ≤ c)
    (F : BoundedWeakAlgebraMap M c) :
    ∃ K : Set (BoundedWeakAlgebraMap M c), K ⊆ closure (boundedWeakRowOrbit F) ∧
      K.Nonempty ∧ IsClosed K ∧ RowInvariant hc K ∧
      ∀ L : Set (BoundedWeakAlgebraMap M c), L ⊆ K → L.Nonempty → IsClosed L →
        RowInvariant hc L → L = K := by
…

    Mentions: OAI.KadisonKastler.BoundedWeakAlgebraMap, OAI.KadisonKastler.boundedWeakRowOrbit, OAI.KadisonKastler.RowInvariant