OAI/Geometry/CAT0Fillings/Gradient/HilbertAtlas.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.ChartGeometry.weightedMeasure line 19
2. lemma OAI.CAT0Fillings.ChartGeometry.weightedMeasure_le line 23
3. lemma OAI.CAT0Fillings.ChartGeometry.weightedMeasure_finite line 40
4. def OAI.CAT0Fillings.ChartGeometry.gradientMeasure line 45
5. def OAI.CAT0Fillings.ChartGeometry.energyMeasure line 47
6. lemma OAI.CAT0Fillings.ChartGeometry.gradientMeasure_le line 50
7. lemma OAI.CAT0Fillings.ChartGeometry.energyMeasure_le line 54
8. lemma OAI.CAT0Fillings.ChartGeometry.gradientMeasure_finite line 60
9. lemma OAI.CAT0Fillings.ChartGeometry.energyMeasure_finite line 64
10. lemma OAI.CAT0Fillings.ChartGeometry.integral_gradientMeasure line 68
11. lemma OAI.CAT0Fillings.ChartGeometry.gradient_summable line 83
12. lemma OAI.CAT0Fillings.matrix_posSemidef_closed line 110
13. lemma OAI.CAT0Fillings.measurable_matrix_sqrt line 126
14. def OAI.CAT0Fillings.ChartGeometry.normalizedCovector line 144
15. lemma OAI.CAT0Fillings.ChartGeometry.aestronglyMeasurable_normalizedCovector line 147
16. lemma OAI.CAT0Fillings.ChartGeometry.ae_normalizedCovector_norm_sq line 156
17. def OAI.CAT0Fillings.ChartGeometry.coordinateMeasure line 179
18. def OAI.CAT0Fillings.ChartGeometry.atlasMeasure line 181
19. instance OAI.CAT0Fillings.ChartGeometry.coordinateMeasure_finite line 184
20. lemma OAI.CAT0Fillings.ChartGeometry.coordinateMeasure_total line 187
21. instance OAI.CAT0Fillings.ChartGeometry.atlasMeasure_finite line 195
22. def OAI.CAT0Fillings.ChartGeometry.gradientFunction line 202
23. lemma OAI.CAT0Fillings.ChartGeometry.aestronglyMeasurable_gradientFunction line 205
24. lemma OAI.CAT0Fillings.ChartGeometry.ae_gradientFunction_bound line 213
25. lemma OAI.CAT0Fillings.ChartGeometry.memLp_gradientFunction line 223
26. def OAI.CAT0Fillings.ChartGeometry.gradient line 227
27. lemma OAI.CAT0Fillings.ChartGeometry.gradient_norm_sq line 230