OAI/Geometry/IntegralFillings/Differentiation/HilbertCharts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.ae_restrict_of_arbitrarily_large_pieces line 18
2. theorem OAI.SharpIntegralFillings.MetricDifferentiation.ae_metricSeminorm_parallelogram_on line 50
3. theorem OAI.SharpIntegralFillings.MetricDifferentiation.ae_metricSeminorm_distance_bound_on line 76
4. def OAI.SharpIntegralFillings.MetricDifferentiation.HasCenteredMetricDifferentialWithin line 97
5. theorem OAI.SharpIntegralFillings.MetricDifferentiation.exists_hilbertian_chart_differential line 102