OAI/Geometry/IntegralFillings/Differentiation/Directional.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpIntegralFillings.MetricDifferentiation.signedDistance line 16
  2. lemma OAI.SharpIntegralFillings.MetricDifferentiation.signedDistance_zero line 19
  3. lemma OAI.SharpIntegralFillings.MetricDifferentiation.signedDistance_div line 22
  4. lemma OAI.SharpIntegralFillings.MetricDifferentiation.hasDerivAt_signedDistance_iff line 30
  5. lemma OAI.SharpIntegralFillings.MetricDifferentiation.continuous_signedDistance line 37
  6. lemma OAI.SharpIntegralFillings.MetricDifferentiation.measurableSet_metricDirectionalDeriv line 45
  7. def OAI.SharpIntegralFillings.MetricDifferentiation.scalarCoordinate line 73
  8. lemma OAI.SharpIntegralFillings.MetricDifferentiation.scalarCoordinate_lipschitz line 77
  9. def OAI.SharpIntegralFillings.MetricDifferentiation.lineSpeed line 83
  10. lemma OAI.SharpIntegralFillings.MetricDifferentiation.measurable_lineSpeed line 86
  11. lemma OAI.SharpIntegralFillings.MetricDifferentiation.deriv_coordinate_line line 92
  12. lemma OAI.SharpIntegralFillings.MetricDifferentiation.lineSpeed_eq_curveSpeed line 105
  13. lemma OAI.SharpIntegralFillings.MetricDifferentiation.measurableSet_hasMetricDirectionalDeriv line 109
  14. lemma OAI.SharpIntegralFillings.MetricDifferentiation.tendsto_add_zero_punctured line 131
  15. theorem OAI.SharpIntegralFillings.MetricDifferentiation.ae_hasMetricDirectionalDeriv line 139