OAI/Geometry/Cannon/Flows/WeightedOscillation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonMagnification.exists_tail_maximum line 26
  2. theorem OAI.CannonMagnification.exists_tail_records line 40
  3. theorem OAI.CannonMagnification.weighted_tail_records line 53
  4. lemma OAI.CannonMagnification.oscillation_le_of_pairwise line 77
  5. theorem OAI.CannonMagnification.connected_oscillation_cover line 85
  6. def OAI.CannonMagnification.weightedOscillation line 110
  7. lemma OAI.CannonMagnification.weightedOscillation_bounds line 114
  8. theorem OAI.CannonMagnification.weightedOscillation_lower line 136
  9. lemma OAI.CannonMagnification.infDist_compl_weight line 195
  10. lemma OAI.CannonMagnification.infDist_compl_compact_lower line 206
  11. theorem OAI.CannonMagnification.weighted_centers_escape line 213
  12. theorem OAI.CannonMagnification.select_weighted_magnifications line 240
  13. lemma OAI.CannonMagnification.inverse_geometric_near line 314
  14. lemma OAI.CannonMagnification.reciprocal_pow_log line 334
  15. lemma OAI.CannonMagnification.abs_sub_le_oscillation line 344
  16. lemma OAI.CannonMagnification.infDist_comparable line 354
  17. theorem OAI.CannonMagnification.normalized_local_oscillation line 362
  18. theorem OAI.CannonMagnification.bounded_connected_variation line 379
  19. theorem OAI.CannonMagnification.holder_of_geometric_bounds line 406
  20. def OAI.CannonMagnification.normalized line 428
  21. lemma OAI.CannonMagnification.continuous_normalized line 431
  22. lemma OAI.CannonMagnification.normalized_dist line 435
  23. lemma OAI.CannonMagnification.compact_puncture_separation line 443
  24. theorem OAI.CannonMagnification.normalized_bounds_at_scale line 459
  25. theorem OAI.CannonMagnification.global_holder_of_discrete line 514
  26. theorem OAI.CannonMagnification.expansion_record_tails line 554