MinimalRowDynamics.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Every orbit in a minimal row family is dense in that family.

theorem OAI.KadisonKastler.boundedWeakAlgebraMap_ext line 20
theorem OAI.KadisonKastler.boundedWeakRowOrbit_subset_of_invariant line 27
theorem OAI.KadisonKastler.minimal_row_family_orbit_dense line 36

theorem OAI.KadisonKastler.minimal_row_family_quantity_constant line 49

Source documentation

Every lower-semicontinuous quantity decreased by all row averages is constant on a minimal invariant family. This is the norm-minimization step; no right-module conclusion is built into it.

theorem minimal_row_family_quantity_constant {M : VonNeumannAlgebra H} {c : ℝ}
    (hc : 0 ≤ c) (K : Set (BoundedWeakAlgebraMap M c)) (hclosed : IsClosed K)
    (hinv : RowInvariant hc K)
    (hmin : ∀ L : Set (BoundedWeakAlgebraMap M c), L ⊆ K → L.Nonempty → IsClosed L →
      RowInvariant hc L → L = K)
    (q : BoundedWeakAlgebraMap M c → ℝ) (hsub : ∀ a, IsClosed {F | q F ≤ a})
    (hdec : ∀ (n : ℕ) (r : Fin n → Algebra M) (hr : ∑ i, r i * star (r i) = 1)
      (F : BoundedWeakAlgebraMap M c), q (boundedWeakRowAverage hc r hr F) ≤ q F)
    {F G : BoundedWeakAlgebraMap M c} (hF : F ∈ K) (hG : G ∈ K) : q F = q G := by
…

Mentions: OAI.KadisonKastler.BoundedWeakAlgebraMap, OAI.KadisonKastler.RowInvariant, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.boundedWeakRowAverage