OAI/Geometry/KahlerSplitting/AreaBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniversalCoverSplitting.chart_trapping_on_interval line 20
  2. theorem OAI.UniversalCoverSplitting.chart_trapping_on_disk line 77
  3. theorem OAI.UniversalCoverSplitting.norm_circleAverage_sq_le line 116
  4. theorem OAI.UniversalCoverSplitting.norm_sq_le_circleAverage line 132
  5. def OAI.UniversalCoverSplitting.polarEnergy line 142
  6. theorem OAI.UniversalCoverSplitting.norm_sq_mul_diskArea_le_polarEnergy line 145
  7. lemma OAI.UniversalCoverSplitting.polar_symm_circle line 178
  8. theorem OAI.UniversalCoverSplitting.disk_integral_eq_polar line 183
  9. theorem OAI.UniversalCoverSplitting.norm_sq_mul_diskArea_le_integral line 256
  10. theorem OAI.UniversalCoverSplitting.ofReal_norm_sq_mul_diskArea_le_lintegral line 262
  11. theorem OAI.UniversalCoverSplitting.curveArea_mono line 279
  12. theorem OAI.UniversalCoverSplitting.curveArea_eq_ofReal_integral line 283
  13. theorem OAI.UniversalCoverSplitting.exists_normalized_curveArea_lowerBound line 288
  14. theorem OAI.UniversalCoverSplitting.exists_uniform_normalized_curveArea_lowerBound line 391
  15. theorem OAI.UniversalCoverSplitting.lintegral_comp_positive_affine line 422
  16. theorem OAI.UniversalCoverSplitting.curveArea_positive_affine line 453