OAI/Analysis/KadisonKastler/ResolventCutOrder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Monotonicity of resolvent cuts

A smaller positive-part generator factors through every strictly larger one. Its closed range is therefore contained in the larger closed range.

  1. def OAI.KadisonKastler.cutFactor line 17
  2. theorem OAI.KadisonKastler.cutFactor_continuous line 19
  3. theorem OAI.KadisonKastler.cutFactor_identity line 25
  4. theorem OAI.KadisonKastler.resolventCutGenerator_factor line 34
  5. theorem OAI.KadisonKastler.resolventCutGenerator_range_mono line 43
  6. theorem OAI.KadisonKastler.resolventLowerCut_mul_of_le line 53
  7. theorem OAI.KadisonKastler.resolventLowerCut_norm_mono line 57