OAI/Geometry/NegativeCurvature/Tube.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Epigraph tube coordinates, holomorphic descent, and curvature of coordinate metrics.

  1. abbrev OAI.OneSidedNegative.ComplexSpace line 14
  2. abbrev OAI.OneSidedNegative.RealSpace line 15
  3. def OAI.OneSidedNegative.DiffeomorphicToRealSpace line 17
  4. def OAI.OneSidedNegative.HolomorphicLiouville line 24
  5. structure OAI.OneSidedNegative.CoordinateMetric line 33
  6. def OAI.OneSidedNegative.CoordinateMetric.curvature line 49
  7. def OAI.OneSidedNegative.CoordinateMetric.sectionalCurvature line 55
  8. def OAI.OneSidedNegative.CoordinateMetric.pathLength line 59
  9. def OAI.OneSidedNegative.CoordinateMetric.lengthDistance line 63
  10. def OAI.OneSidedNegative.CoordinateMetric.IsComplete line 68
  11. def OAI.OneSidedNegative.CoordinateMetric.SectionalAtMost line 75
  12. def OAI.OneSidedNegative.CoordinateMetric.SectionalUnboundedBelow line 79
  13. def OAI.OneSidedNegative.IsKahler line 86
  14. theorem OAI.OneSidedNegative.CoordinateMetric.koszul_formula line 98
  15. theorem OAI.OneSidedNegative.CoordinateMetric.eq_of_tensor_eq line 109
  16. theorem OAI.OneSidedNegative.CoordinateMetric.connection_unique line 117
  17. theorem OAI.OneSidedNegative.CoordinateMetric.curvature_unique line 127
  18. theorem OAI.OneSidedNegative.CoordinateMetric.gram_determinant_pos line 139
  19. def OAI.OneSidedNegative.tube line 163
  20. def OAI.OneSidedNegative.tubeParam line 165
  21. def OAI.OneSidedNegative.tubeParamInv line 168
  22. theorem OAI.OneSidedNegative.tubeParam_mem line 171
  23. theorem OAI.OneSidedNegative.tubeParamInv_tubeParam line 175
  24. theorem OAI.OneSidedNegative.tubeParam_tubeParamInv line 179
  25. theorem OAI.OneSidedNegative.range_tubeParam line 185
  26. theorem OAI.OneSidedNegative.isOpen_tube line 195
  27. theorem OAI.OneSidedNegative.continuous_tubeParam line 198
  28. theorem OAI.OneSidedNegative.isConnected_tube line 205
  29. theorem OAI.OneSidedNegative.contDiff_tubeParam line 209
  30. theorem OAI.OneSidedNegative.contDiffOn_tubeParamInv line 215
  31. theorem OAI.OneSidedNegative.tube_smooth_coordinates line 224
  32. theorem OAI.OneSidedNegative.fiber_constant_of_vertical_deriv_zero line 241
  33. theorem OAI.OneSidedNegative.holomorphic_descent_on_tube line 254
  34. theorem OAI.OneSidedNegative.constant_of_bounded_holomorphic_vertical_deriv_zero line 283
  35. def OAI.OneSidedNegative.complexTubeEquiv line 295
  36. def OAI.OneSidedNegative.realTubeEquiv line 298
  37. def OAI.OneSidedNegative.tubeInCoordinates line 305
  38. theorem OAI.OneSidedNegative.tubeInCoordinates_topology line 308
  39. theorem OAI.OneSidedNegative.unbounded_below_of_negative_linear_term line 339
  40. theorem OAI.OneSidedNegative.CoordinateMetric.unboundedBelow_of_ray line 353