OAI/Geometry/Cannon/Conformal/OpenMapMaxSphere.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonPlane.openMap_exists_max_on_sphere line 31
  2. lemma OAI.CannonPlane.openMap_exists_min_on_sphere line 52
  3. lemma OAI.CannonPlane.homeomorph_disk_oscillation line 59
  4. lemma OAI.CannonPlane.integral_sq_cauchy line 94
  5. lemma OAI.CannonPlane.circle_derivative_bound line 125
  6. lemma OAI.CannonPlane.circle_oscillation_bound line 135
  7. lemma OAI.CannonPlane.homeomorph_circle_energy line 166
  8. lemma OAI.CannonPlane.polar_circle line 183
  9. lemma OAI.CannonPlane.continuous_polar_circle line 186
  10. lemma OAI.CannonPlane.disk_polar_integral_zero line 190
  11. lemma OAI.CannonPlane.translated_disk_integral line 235
  12. lemma OAI.CannonPlane.disk_polar_integral line 249
  13. lemma OAI.CannonPlane.continuous_circle_integral line 256
  14. lemma OAI.CannonPlane.approximate_circle_energy line 261
  15. lemma OAI.CannonPlane.approximate_log_energy line 291
  16. theorem OAI.CannonMetricQC.weak_homeomorph_log_energy line 336
  17. lemma OAI.CannonMetricQC.WeakQS.two line 384
  18. lemma OAI.CannonMetricQC.WeakQS.four line 398
  19. theorem OAI.CannonMetricQC.imageArea_upper_four line 407
  20. theorem OAI.CannonMetricQC.measure_le_of_closedBall_le line 432
  21. lemma OAI.CannonMetricQC.locallyIntegrable_density_locallyFinite line 445
  22. theorem OAI.CannonMetricQC.weakQS_imageArea_le_energy line 460
  23. theorem OAI.CannonMetricQC.weakQS_weakW12_imageArea_ac line 507
  24. lemma OAI.CannonMetricQC.weakQS_full_weakW12 line 527
  25. theorem OAI.CannonMetricQC.weakQS_imageArea_ac line 552
  26. theorem OAI.CannonMetricQC.weakQS_image_null line 560
  27. theorem OAI.CannonMetricQC.weakQS_quasiMeasurePreserving line 572
  28. theorem OAI.CannonMetricQC.weakQS_ae_bijective_fderiv line 578
  29. theorem OAI.CannonMetricQC.weakQS_ae_fderiv_comp line 594