OAI/Geometry/KahlerSplitting/SmallArea.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniversalCoverSplitting.exists_brody_maximum line 18
  2. theorem OAI.UniversalCoverSplitting.exists_brody_rescaling line 59
  3. theorem OAI.UniversalCoverSplitting.small_area_weighted_speed line 86
  4. theorem OAI.UniversalCoverSplitting.exists_small_area_speed_bound line 144
  5. theorem OAI.UniversalCoverSplitting.small_area_derivatives_tendstoUniformlyOn line 160
  6. theorem OAI.UniversalCoverSplitting.bounded_curveSpeed_local_trapping line 182
  7. abbrev OAI.UniversalCoverSplitting.compactManifoldMetric line 253
  8. theorem OAI.UniversalCoverSplitting.bounded_curveSpeed_uniform_trapping line 261
  9. theorem OAI.UniversalCoverSplitting.bounded_curveSpeed_equicontinuousOn line 292
  10. theorem OAI.UniversalCoverSplitting.equicontinuous_compact_target_subsequence line 336