OAI/Analysis/KadisonKastler/ModularStrongContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Strong continuity of the limiting modular group

The cutoff error is bounded by |t| ε ‖x‖. At time zero this proves continuity on the dense cutoff range using just one bounded approximation. Contraction bounds and the group law give continuity on the whole space.

  1. theorem OAI.KadisonKastler.modularApproximation_limit_cutoff_bound line 22
  2. theorem OAI.KadisonKastler.modularStrongLimit_cutoff_tendsto_zero line 44
  3. theorem OAI.KadisonKastler.modularStrongLimit_tendsto_zero line 74
  4. theorem OAI.KadisonKastler.modularStrongLimit_continuous line 97
  5. theorem OAI.KadisonKastler.modularStrongGroup_continuous line 116