OAI/Geometry/IsometricImmersion/Metrics/MetricQSpatialBundle.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.HorizontalMetricTwoJetBound line 12
  2. def OAI.SmoothLocal.HighEquation.qFixedTimeBaseDomain line 18
  3. def OAI.SmoothLocal.HighEquation.metricQSpatialBundle line 21
  4. theorem OAI.SmoothLocal.HighEquation.statePoint_qFixedTimeState line 24
  5. theorem OAI.SmoothLocal.HighEquation.qFixedTimeBaseDomain_isOpen line 30
  6. theorem OAI.SmoothLocal.HighEquation.metricQSpatialBundle_contDiffOn line 34
  7. theorem OAI.SmoothLocal.HighEquation.norm_iteratedFDeriv_fixedTime_coordinate line 42
  8. theorem OAI.SmoothLocal.HighEquation.qSpatialCLM_norm_le line 63
  9. theorem OAI.SmoothLocal.HighEquation.qFixedTimeState_positive_jet_bound line 77
  10. theorem OAI.SmoothLocal.HighEquation.metricQSpatialBundle_norm_bound line 91
  11. theorem OAI.SmoothLocal.HighEquation.metricQSpatialBundle_positive_jet_bound line 115