OAI/Geometry/IntegralFillings/Differentiation/Centered.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpIntegralFillings.MetricDifferentiation.metricQuotient line 21
2. lemma OAI.SharpIntegralFillings.MetricDifferentiation.metricQuotient_lipschitz line 24
3. def OAI.SharpIntegralFillings.MetricDifferentiation.HasCenteredMetricDifferential line 43
4. lemma OAI.SharpIntegralFillings.MetricDifferentiation.hasCenteredMetricDifferential_of_dense_directions line 46
5. theorem OAI.SharpIntegralFillings.MetricDifferentiation.ae_hasCenteredMetricDifferential line 90