OAI/Geometry/KahlerSplitting/SmallAnnuli.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalCoverSplitting.IsBox.toMixed line 34
  2. lemma OAI.UniversalCoverSplitting.IsMixedBox.comp_translation line 45
  3. lemma OAI.UniversalCoverSplitting.IsMixedBox.slice_holomorphic_on line 65
  4. lemma OAI.UniversalCoverSplitting.mixed_shift_in_annulus line 80
  5. theorem OAI.UniversalCoverSplitting.chart_annulus_mixed_extension line 98
  6. def OAI.UniversalCoverSplitting.annulusPath line 144
  7. theorem OAI.UniversalCoverSplitting.annulusPath_zero line 147
  8. theorem OAI.UniversalCoverSplitting.annulusPath_one line 150
  9. theorem OAI.UniversalCoverSplitting.annulusPath_norm line 153
  10. theorem OAI.UniversalCoverSplitting.annulusPath_mem line 160
  11. theorem OAI.UniversalCoverSplitting.annulusPath_hasDerivAt line 166
  12. theorem OAI.UniversalCoverSplitting.annulusPath_deriv_bound line 176
  13. theorem OAI.UniversalCoverSplitting.chart_trapping_on_annulus line 202
  14. def OAI.UniversalCoverSplitting.compactAnnulus line 242
  15. def OAI.UniversalCoverSplitting.openAnnulus line 243
  16. theorem OAI.UniversalCoverSplitting.isCompact_compactAnnulus line 245
  17. theorem OAI.UniversalCoverSplitting.isOpen_openAnnulus line 251
  18. theorem OAI.UniversalCoverSplitting.compactAnnulus_subset_openAnnulus line 254
  19. theorem OAI.UniversalCoverSplitting.exists_annulus_speed_trapping line 258
  20. theorem OAI.UniversalCoverSplitting.exists_small_area_annulus_image_in_cover line 308
  21. def OAI.UniversalCoverSplitting.scaledAnnulus line 340
  22. lemma OAI.UniversalCoverSplitting.measurableSet_scaledAnnulus line 342
  23. lemma OAI.UniversalCoverSplitting.scaledAnnulus_disjoint line 346
  24. lemma OAI.UniversalCoverSplitting.geometric_annuli_pairwiseDisjoint line 354
  25. theorem OAI.UniversalCoverSplitting.exists_small_energy_annulus line 370
  26. theorem OAI.UniversalCoverSplitting.exists_number_of_annuli line 397
  27. lemma OAI.UniversalCoverSplitting.positive_smul_openAnnulus line 414
  28. lemma OAI.UniversalCoverSplitting.inv_smul_mem_compactAnnulus line 433
  29. lemma OAI.UniversalCoverSplitting.curveArea_rescale_annulus line 442
  30. lemma OAI.UniversalCoverSplitting.scaled_slice_holomorphic line 453