OAI/Geometry/Cannon/Conformal/ImageArea.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonMetricQC.image_ball_contains line 21
  2. def OAI.CannonMetricQC.imageArea line 35
  3. lemma OAI.CannonMetricQC.imageArea_apply line 37
  4. instance OAI.CannonMetricQC.imageArea_locallyFinite line 43
  5. lemma OAI.CannonMetricQC.area_controls_dist line 49
  6. theorem OAI.CannonMetricQC.weakQS_ae_pointwiseLip line 62
  7. theorem OAI.CannonMetricQC.weakQS_ae_differentiable line 107
  8. lemma OAI.CannonMetricQC.measurable_ballArea line 117
  9. theorem OAI.CannonMetricQC.integrated_ballArea line 133
  10. lemma OAI.CannonMetricQC.square_dist_le_area line 188
  11. theorem OAI.CannonMetricQC.weakQS_increment_energy line 206
  12. lemma OAI.CannonMetricQC.eLpNorm_two_sq line 237
  13. lemma OAI.CannonMetricQC.continuous_memLp_compact line 243
  14. theorem OAI.CannonMetricQC.weakQS_increment_lp line 251
  15. theorem OAI.CannonMetricQC.cutoff_increment_bound line 288
  16. lemma OAI.CannonMetricQC.cutoff_hasCompactSupport line 364
  17. theorem OAI.CannonMetricQC.weakQS_cutoff_increment_bound line 373