OAI/Analysis/KadisonKastler/ResolventCyclicCuts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The cyclic model identifies the concrete cut projections

  1. def OAI.KadisonKastler.resolventCutIndicator line 18
  2. theorem OAI.KadisonKastler.resolventCutIndicator_measurable line 22
  3. theorem OAI.KadisonKastler.resolventCutIndicator_bound line 27
  4. theorem OAI.KadisonKastler.resolventCyclicIsometry_cut line 31