OAI/Analysis/KadisonKastler/GeometricCorrectionScale.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The summable error scale for multiplication correction

  1. def OAI.KadisonKastler.correctionScale line 14
  2. theorem OAI.KadisonKastler.correctionScale_zero line 16
  3. theorem OAI.KadisonKastler.correctionScale_succ line 19
  4. theorem OAI.KadisonKastler.correctionScale_nonneg line 24
  5. theorem OAI.KadisonKastler.correctionScale_le line 29
  6. theorem OAI.KadisonKastler.correctionScale_summable line 34
  7. theorem OAI.KadisonKastler.correctionScale_tsum line 38
  8. theorem OAI.KadisonKastler.correctionScale_tendsto line 44
  9. theorem OAI.KadisonKastler.correctionScale_partial_sum line 50