OAI/Geometry/Cannon/Uniformization/EventualRelativeShrink.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonRealization.EventualRelativeShrink line 18
  2. def OAI.CannonRealization.RelativeShrink line 24
  3. lemma OAI.CannonRealization.EventualRelativeShrink.equicontinuous line 30
  4. lemma OAI.CannonRealization.compact_map_subsequence line 68
  5. lemma OAI.CannonRealization.EventualRelativeShrink.limit line 96
  6. theorem OAI.CannonRealization.RelativeShrink.injective line 115
  7. lemma OAI.CannonRealization.surjective_limit line 145
  8. theorem OAI.CannonRealization.realization_homeomorph_limit line 157
  9. def OAI.CannonRealization.WeakQS line 193
  10. lemma OAI.CannonRealization.radial_point line 196
  11. theorem OAI.CannonRealization.inverse_weakQS_ratio_bound line 203
  12. theorem OAI.CannonRealization.RelativeShrink.inverse_weakQS line 299
  13. theorem OAI.CannonRealization.RelativeShrink.forward_ratio_bounds line 319
  14. theorem OAI.CannonRealization.RelativeShrink.forward_weakQS line 329
  15. lemma OAI.CannonRealization.small_scale_geometric line 347
  16. lemma OAI.CannonRealization.large_scale_geometric line 363
  17. theorem OAI.CannonRealization.relative_small_power line 379
  18. theorem OAI.CannonRealization.relative_large_power line 410
  19. def OAI.CannonDistortion.maxIso line 448
  20. lemma OAI.CannonDistortion.maxIso_apply line 464
  21. def OAI.CannonDistortion.powerGauge line 467
  22. def OAI.CannonDistortion.powerIso line 469
  23. lemma OAI.CannonDistortion.powerIso_coe line 472
  24. lemma OAI.CannonDistortion.powerGauge_nonneg line 476
  25. lemma OAI.CannonDistortion.powerGauge_monotone line 479
  26. theorem OAI.CannonDistortion.mixed_power_bound line 483
  27. theorem OAI.CannonRealization.RelativeShrink.power_control line 524