OAI/Analysis/SegmentLenses/Separated.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Separated families and uniform positive gaps

  1. theorem OAI.SegmentLenses.finite_head_close_pair line 24
  2. theorem OAI.SegmentLenses.separated_predual_family line 60
  3. abbrev OAI.SegmentLenses.CofiniteLargeSphere line 139
  4. def OAI.SegmentLenses.averagedLargeOn line 141
  5. def OAI.SegmentLenses.averagedLargeAt line 144
  6. def OAI.SegmentLenses.averagedLargeModulus line 147
  7. theorem OAI.SegmentLenses.average_nonneg_all line 151
  8. theorem OAI.SegmentLenses.averagedLargeOn_bounds line 159
  9. theorem OAI.SegmentLenses.averagedLargeModulus_lower line 173
  10. theorem OAI.SegmentLenses.predual_strong_large_average line 201
  11. theorem OAI.SegmentLenses.clipping_scalar line 210
  12. theorem OAI.SegmentLenses.infinite_paired_clipping line 216
  13. theorem OAI.SegmentLenses.forest_paired_clipping line 222
  14. def OAI.SegmentLenses.radialConstant line 227
  15. theorem OAI.SegmentLenses.radialConstant_ge line 229
  16. def OAI.SegmentLenses.originalOmega line 235
  17. theorem OAI.SegmentLenses.originalOmega_positive line 237
  18. theorem OAI.SegmentLenses.originalOmega_comparison line 246
  19. theorem OAI.SegmentLenses.infinite_original_modulus line 270