OAI/Analysis/KadisonKastler/ModularSpectralCuts.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Concrete upper cuts for the logarithmic modular spectrum

An upper logarithmic cut is the support of the positive part of a scalar minus the graph resolvent. These are actual orthogonal projections on the original Hilbert space, with no assumed spectral measure.

  1. def OAI.KadisonKastler.resolventCutGenerator line 21
  2. def OAI.KadisonKastler.resolventLowerCut line 24
  3. theorem OAI.KadisonKastler.resolventLowerCut_projection line 27
  4. theorem OAI.KadisonKastler.resolventLowerCut_mul_generator line 31
  5. theorem OAI.KadisonKastler.mul_resolventLowerCut_eq_zero line 37
  6. theorem OAI.KadisonKastler.cut_range_invariant line 47
  7. theorem OAI.KadisonKastler.resolventLowerCut_commutes line 60
  8. theorem OAI.KadisonKastler.resolventLowerCut_commutes_cfc line 67
  9. def OAI.KadisonKastler.modularCutThreshold line 71
  10. theorem OAI.KadisonKastler.modularCutThreshold_pos line 73
  11. theorem OAI.KadisonKastler.modularCutThreshold_lt_one line 77
  12. def OAI.KadisonKastler.modularUpperCut line 81
  13. theorem OAI.KadisonKastler.modularUpperCut_projection line 85
  14. theorem OAI.KadisonKastler.modularUpperCut_contracts line 88
  15. theorem OAI.KadisonKastler.modularUpperCut_complement_contracts line 91
  16. theorem OAI.KadisonKastler.modularUpperCut_identification_independent line 94
  17. theorem OAI.KadisonKastler.modularUpperCut_commutes_resolvent line 99
  18. theorem OAI.KadisonKastler.modularUpperCut_commutes_group line 106