OAI/Geometry/IsometricImmersion/Estimates/UniversalQRaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.universalQCurvature line 13
  2. def OAI.SmoothLocal.HighEquation.universalQNumerator line 16
  3. def OAI.SmoothLocal.HighEquation.universalQRaw line 20
  4. theorem OAI.SmoothLocal.HighEquation.universalQCurvature_metricPBundle line 24
  5. theorem OAI.SmoothLocal.HighEquation.universalQNumerator_metricPBundle line 30
  6. theorem OAI.SmoothLocal.HighEquation.universalQCurvature_contDiffOn line 39
  7. theorem OAI.SmoothLocal.HighEquation.universalQNumerator_contDiffOn line 45
  8. theorem OAI.SmoothLocal.HighEquation.universalQRaw_contDiffOn line 56
  9. theorem OAI.SmoothLocal.HighEquation.universalQRaw_uniform_error line 66
  10. theorem OAI.SmoothLocal.HighEquation.universalQDenominator_uniform_bound line 81
  11. theorem OAI.SmoothLocal.HighEquation.universalQRaw_uniform_margins line 91