OAI/Analysis/KadisonKastler/TrivialCoreCenter.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The regular core of a trivial action has a nontrivial center

  1. theorem OAI.KadisonKastler.regularIndicatorProjection_mul_eq_zero_of_disjoint line 17
  2. theorem OAI.KadisonKastler.regularFrequencyWindow_mul_eq_zero_of_disjoint line 34
  3. theorem OAI.KadisonKastler.regularFrequencyWindow_not_scalar line 41
  4. theorem OAI.KadisonKastler.regularFrequencyWindow_commute_of_translations line 59
  5. theorem OAI.KadisonKastler.regularCore_not_factor_of_trivial line 83