OAI/Geometry/KahlerSplitting/CompactCurves.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniversalCoverSplitting.finite_large_atoms line 24
  2. theorem OAI.UniversalCoverSplitting.eventually_small_ball_of_small_atom line 32
  3. theorem OAI.UniversalCoverSplitting.bounded_measure_finite_concentration line 44
  4. theorem OAI.UniversalCoverSplitting.bounded_density_finite_concentration line 83
  5. theorem OAI.UniversalCoverSplitting.manifold_holomorphic_locally_uniform_limit line 144
  6. theorem OAI.UniversalCoverSplitting.bounded_curveSpeed_holomorphic_subsequence line 207
  7. theorem OAI.UniversalCoverSplitting.eventual_curveSpeed_bound_to_bound line 231
  8. theorem OAI.UniversalCoverSplitting.bounded_curveArea_holomorphic_subsequence line 264
  9. theorem OAI.UniversalCoverSplitting.holomorphic_circleAverage_eq line 320
  10. theorem OAI.UniversalCoverSplitting.norm_circleAverage_le line 333
  11. theorem OAI.UniversalCoverSplitting.norm_sub_circleAverage_le line 345
  12. theorem OAI.UniversalCoverSplitting.holomorphic_circle_oscillation line 356
  13. theorem OAI.UniversalCoverSplitting.holomorphic_annulus_oscillation line 383