OAI/Geometry/IsometricImmersion/Metrics/MetricPBundleBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.HighEquation.norm_iteratedFDeriv_pi_le line 17
  2. theorem OAI.SmoothLocal.HighEquation.norm_iteratedFDeriv_prod_le line 32
  3. theorem OAI.SmoothLocal.HighEquation.norm_iteratedFDeriv_comp_contraction line 42
  4. theorem OAI.SmoothLocal.HighEquation.norm_iteratedFDeriv_id_pos line 60
  5. theorem OAI.SmoothLocal.HighEquation.norm_iteratedFDeriv_coordPartial_le line 75
  6. def OAI.SmoothLocal.HighEquation.statePointCLM line 90
  7. theorem OAI.SmoothLocal.HighEquation.statePointCLM_eq line 94
  8. theorem OAI.SmoothLocal.HighEquation.statePointCLM_norm_le line 98
  9. theorem OAI.SmoothLocal.HighEquation.norm_iteratedFDeriv_comp_statePoint line 108
  10. theorem OAI.SmoothLocal.HighEquation.metricPBundle_contDiffOn line 126
  11. theorem OAI.SmoothLocal.HighEquation.metricPBundle_positive_jet_bound line 159