OAI/Analysis/KadisonKastler/GraphLowCutBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The complementary low-cut estimate

Clipping the decreasing resolvent complement at the cut changes it by a multiple of the cut generator. This difference vanishes on the low cut.

  1. theorem OAI.KadisonKastler.graphComplementScalar_continuousOn line 19
  2. theorem OAI.KadisonKastler.resolventCutGenerator_mul_complement line 28
  3. theorem OAI.KadisonKastler.graphLowCut_clipped line 35
  4. theorem OAI.KadisonKastler.graphLowCut_bound line 71
  5. theorem OAI.KadisonKastler.graphLowCut_support line 99