OAI/Geometry/Cannon/Flows/Domain.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonMagnification.all_bound_of_eventual line 28
  2. lemma OAI.CannonMagnification.equicontinuous_of_eventual_holder line 39
  3. theorem OAI.CannonMagnification.locally_bounded_holder_subsequence line 65
  4. theorem OAI.CannonMagnification.punctured_nonconstant_subsequence line 116
  5. lemma OAI.CannonMagnification.oscillation_attained line 191
  6. theorem OAI.CannonMagnification.expansion_record_limit line 200
  7. lemma OAI.CannonMagnification.continuous_oscillation_bound line 266
  8. lemma OAI.CannonMagnification.upper_geometric_of_eventual line 277
  9. theorem OAI.CannonMagnification.holder_weighted_records line 290
  10. theorem OAI.CannonMagnification.holder_magnification_global line 367
  11. theorem OAI.CannonMagnification.local_holder_extension line 424
  12. def OAI.CannonMagnification.onDomain line 457
  13. lemma OAI.CannonMagnification.onDomain_eq line 460
  14. theorem OAI.CannonMagnification.local_holder_magnification line 463
  15. theorem OAI.CannonRelease.boundary_holder_magnification line 535