OAI/Geometry/IsometricImmersion/Immersions/HeightPFirstBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.heightQuotientJetBound line 12
  2. def OAI.SmoothLocal.Geometry.heightAlongDJetBound line 14
  3. def OAI.SmoothLocal.Geometry.heightEnergyFirstQuotientBound line 17
  4. def OAI.SmoothLocal.Geometry.heightPFirstBound line 19
  5. theorem OAI.SmoothLocal.Geometry.heightQuotientJetBound_nonneg line 23
  6. theorem OAI.SmoothLocal.Geometry.heightAlongDJetBound_nonneg line 30
  7. theorem OAI.SmoothLocal.Geometry.heightEnergyFirstQuotientBound_nonneg line 37
  8. theorem OAI.SmoothLocal.Geometry.heightPFirstBound_nonneg line 45
  9. theorem OAI.SmoothLocal.Geometry.height_jetEnergy_first_coordinate_bound line 54
  10. theorem OAI.SmoothLocal.Geometry.height_christoffelAlongD_coordinate_bound line 96
  11. theorem OAI.SmoothLocal.Geometry.heightPFirst_coordinate_bound_one line 136