OAI/Analysis/KadisonKastler/ModularCutBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative modular cuts in every graph identification

The graph comparison controls three bounded spectral cuts. These estimates are independent of the KMS condition and the Fourier gauge identity.

  1. theorem OAI.KadisonKastler.modularUpperCut_high_inverse line 18
  2. theorem OAI.KadisonKastler.modularUpperCut_low_bound line 33
  3. theorem OAI.KadisonKastler.modularUpperCut_low_support line 42