OAI/Geometry/IntegralFillings/Differentiation/Seminorm.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpIntegralFillings.MetricDifferentiation.coordinateSeminorm line 18
2. lemma OAI.SharpIntegralFillings.MetricDifferentiation.coordinateSeminorm_apply line 21
3. lemma OAI.SharpIntegralFillings.MetricDifferentiation.coordinateSeminorm_le line 24
4. def OAI.SharpIntegralFillings.MetricDifferentiation.metricSeminorm line 31
5. lemma OAI.SharpIntegralFillings.MetricDifferentiation.bddAbove_coordinateSeminorm line 34
6. lemma OAI.SharpIntegralFillings.MetricDifferentiation.metricSeminorm_apply line 38
7. lemma OAI.SharpIntegralFillings.MetricDifferentiation.metricSeminorm_le line 43
8. lemma OAI.SharpIntegralFillings.MetricDifferentiation.metricSeminorm_lipschitz line 48
9. lemma OAI.SharpIntegralFillings.MetricDifferentiation.lineSpeed_eq_metricSeminorm line 55
10. theorem OAI.SharpIntegralFillings.MetricDifferentiation.ae_dense_directionalSeminorm line 63
11. lemma OAI.SharpIntegralFillings.uniformly_tendsto_of_lipschitz line 87