OAI/Analysis/KadisonKastler/FrequencyActionAlignment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Common modular actions from the actual frequency defects

The tolerance is fixed before the Hilbert space, the factors and their actions. The pointwise normalizers are selected with no regularity claim; the discrete real invariant mean then produces one small change of position.

  1. def OAI.KadisonKastler.modularComparisonField line 24
  2. def OAI.KadisonKastler.FrequencyDefectBound line 28
  3. theorem OAI.KadisonKastler.uniform_common_action_of_frequency_defects line 41