OAI/Analysis/ModularTheory/HalfGraphCutoff.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The cutoff half-exponential identity on the actual closed Tomita graph. This is the bounded spectral calculation used before taking modular-weight limits; it does not assert the existence or traciality of a core weight.

  1. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_multiplier line 16
  2. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_cutoff line 36
  3. lemma OAI.BoundedRecovery.StandardModularData.cutoff_tomita_vector line 62