OAI/Geometry/KahlerSplitting/Superellipsoids.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalCoverSplitting.superPotential line 34
  2. def OAI.UniversalCoverSplitting.superDomain line 37
  3. lemma OAI.UniversalCoverSplitting.normSq_contDiff line 39
  4. lemma OAI.UniversalCoverSplitting.superPotential_contDiff line 44
  5. lemma OAI.UniversalCoverSplitting.superPotential_nonneg line 47
  6. lemma OAI.UniversalCoverSplitting.superDomain_open line 50
  7. lemma OAI.UniversalCoverSplitting.superPotential_convex line 53
  8. lemma OAI.UniversalCoverSplitting.superDomain_convex line 63
  9. lemma OAI.UniversalCoverSplitting.superPotential_zero line 68
  10. lemma OAI.UniversalCoverSplitting.superDomain_zero line 71
  11. lemma OAI.UniversalCoverSplitting.superPotential_smul line 74
  12. lemma OAI.UniversalCoverSplitting.superDomain_mono line 80
  13. lemma OAI.UniversalCoverSplitting.superDomain_subset_bidisk line 83
  14. lemma OAI.UniversalCoverSplitting.normSq_hasFDerivAt line 99
  15. lemma OAI.UniversalCoverSplitting.normSq_fderiv_apply line 105
  16. lemma OAI.UniversalCoverSplitting.normSqPow_fderiv_mul line 117
  17. def OAI.UniversalCoverSplitting.superSource line 128
  18. lemma OAI.UniversalCoverSplitting.superSource_zero line 132
  19. lemma OAI.UniversalCoverSplitting.superSource_contDiff line 134
  20. lemma OAI.UniversalCoverSplitting.superSource_hasFDerivAt line 140
  21. lemma OAI.UniversalCoverSplitting.superSource_fderiv line 147
  22. lemma OAI.UniversalCoverSplitting.superPotential_fderiv_mul line 153
  23. lemma OAI.UniversalCoverSplitting.superPotential_superSource_fderiv line 167
  24. theorem OAI.UniversalCoverSplitting.superDomain_mixed_boundary line 187
  25. def OAI.UniversalCoverSplitting.IsHorizontalCurve line 239
  26. def OAI.UniversalCoverSplitting.IsVerticalCurve line 243
  27. lemma OAI.UniversalCoverSplitting.IsHorizontalCurve.mono line 247
  28. lemma OAI.UniversalCoverSplitting.IsVerticalCurve.mono line 251
  29. lemma OAI.UniversalCoverSplitting.SplittingChart.horizontal_coordinate_constant line 255
  30. lemma OAI.UniversalCoverSplitting.SplittingChart.vertical_coordinate_constant line 275
  31. lemma OAI.UniversalCoverSplitting.SplittingChart.mix_curves line 295
  32. lemma OAI.UniversalCoverSplitting.separated_eq_axes line 330
  33. lemma OAI.UniversalCoverSplitting.SplittingChart.mix_curves_axes line 354
  34. lemma OAI.UniversalCoverSplitting.exists_axis_box_germ line 369
  35. lemma OAI.UniversalCoverSplitting.IsBox.horizontal_slice line 392
  36. lemma OAI.UniversalCoverSplitting.IsBox.vertical_slice line 409