NormUltraproductSimplicity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A concrete uniform-fullness criterion for the norm ultraproduct

A coordinate compression estimate implies simplicity of the norm ultraproduct. For type III factors, this estimate follows from projection comparison.

theorem OAI.KadisonKastler.exists_eventually_norm_lower_bound line 22

theorem OAI.KadisonKastler.normUltraproduct_simple_of_uniform_fullness line 37

Source documentation

Uniform coordinate compression to 1 makes every nonzero ideal of the norm ultraproduct contain 1. This proves even algebraic simplicity.

theorem normUltraproduct_simple_of_uniform_fullness
    (hfull : ∀ ε R : ℝ, 0 < ε → 0 ≤ R → ∃ K : ℝ, 0 ≤ K ∧
      ∀ j (x : B j), ε ≤ ‖x‖ → ‖x‖ ≤ R → ∃ b c : B j,
        ‖b‖ ≤ K ∧ ‖c‖ ≤ K ∧ b * x * c = 1)
    (ω : Ultrafilter ℕ) : CStarSimple (NormUltraproduct B ω) := by
…

Mentions: OAI.KadisonKastler.CStarSimple, OAI.KadisonKastler.NormUltraproduct