OAI/Geometry/IntegralFillings/Differentiation/CurveSpeed.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpIntegralFillings.MetricDifferentiationDense.distanceCoordinate line 15
  2. def OAI.SharpIntegralFillings.MetricDifferentiationDense.metricSpeed line 18
  3. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.coordinate_lipschitz line 21
  4. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.coordinate_deriv_bound line 26
  5. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.coordinate_deriv_le_speed line 30
  6. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.metricSpeed_nonneg line 34
  7. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.metricSpeed_le line 37
  8. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.measurable_metricSpeed line 40
  9. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.locallyIntegrable_metricSpeed line 43
  10. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.intervalIntegrable_metricSpeed line 50
  11. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.coordinate_difference_bound line 55
  12. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.distance_le_integral_speed line 65
  13. def OAI.SharpIntegralFillings.MetricDifferentiationDense.integratedSpeed line 75
  14. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.distance_le_integratedSpeed line 78
  15. def OAI.SharpIntegralFillings.MetricDifferentiationDense.HasMetricDerivAt line 92
  16. lemma OAI.SharpIntegralFillings.MetricDifferentiationDense.abs_slope_tendsto line 95
  17. theorem OAI.SharpIntegralFillings.MetricDifferentiationDense.ae_hasMetricDerivAt line 100