OAI/Geometry/KahlerSplitting/DiskArea.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalCoverSplitting.finTwo_box_integral_eq_prod line 34
  2. theorem OAI.UniversalCoverSplitting.normalized_polar_integral_eq_disk line 55
  3. def OAI.UniversalCoverSplitting.sliceDensity line 107
  4. theorem OAI.UniversalCoverSplitting.sliceDensity_nonneg line 110
  5. theorem OAI.UniversalCoverSplitting.curveSpeed_slice_sq line 113
  6. theorem OAI.UniversalCoverSplitting.sliceDensity_continuousOn line 127
  7. theorem OAI.UniversalCoverSplitting.curveArea_slice_eq_ofReal_integral line 136
  8. theorem OAI.UniversalCoverSplitting.movingKahlerForm_zero_density line 155
  9. theorem OAI.UniversalCoverSplitting.moving_disk_face_eq_areaIntegral line 172
  10. theorem OAI.UniversalCoverSplitting.moving_disk_area_le line 196
  11. theorem OAI.UniversalCoverSplitting.curveArea_slice_ne_top line 243
  12. def OAI.UniversalCoverSplitting.shrinkingRadius line 258
  13. theorem OAI.UniversalCoverSplitting.shrinkingRadius_contDiffOn line 260
  14. theorem OAI.UniversalCoverSplitting.shrinkingRadius_hasDerivAt line 267
  15. theorem OAI.UniversalCoverSplitting.shrinkingRadius_nonneg line 272
  16. theorem OAI.UniversalCoverSplitting.exists_shrinkingRadius_deriv_le line 275
  17. theorem OAI.UniversalCoverSplitting.moving_disk_area_le_of_slices line 304
  18. theorem OAI.UniversalCoverSplitting.shrinking_disk_area_bound line 336