OAI/Analysis/PureInfiniteness/CutSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Fixed-cut action on a supported element, used for the return column in KR02 Lemma 7.6. A continuous divided difference avoids spectral projections and works in a nonunital algebra.

  1. def OAI.WeakPureInfiniteness.cutDifferenceRatio line 13
  2. lemma OAI.WeakPureInfiniteness.continuous_cutDifferenceRatio line 16
  3. lemma OAI.WeakPureInfiniteness.cutDifferenceRatio_zero line 24
  4. lemma OAI.WeakPureInfiniteness.cutDifferenceRatio_identity line 28
  5. theorem OAI.WeakPureInfiniteness.cut_mul_of_mul_eq line 47