OAI/Geometry/CAT0Fillings/Gradient/Chart.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.inverse_quadratic_le line 13
2. def OAI.CAT0Fillings.ChartGeometry.covector line 38
3. def OAI.CAT0Fillings.ChartGeometry.normSq line 41
4. def OAI.CAT0Fillings.ChartGeometry.duNorm line 44
5. lemma OAI.CAT0Fillings.ChartGeometry.measurable_gram line 47
6. lemma OAI.CAT0Fillings.ChartGeometry.aestronglyMeasurable_covector line 58
7. lemma OAI.CAT0Fillings.ChartGeometry.aestronglyMeasurable_normSq line 72
8. lemma OAI.CAT0Fillings.ChartGeometry.aestronglyMeasurable_duNorm line 80
9. lemma OAI.CAT0Fillings.ChartGeometry.ae_normSq_bounds line 85
10. lemma OAI.CAT0Fillings.ChartGeometry.ae_duNorm_bounds line 107
11. lemma OAI.CAT0Fillings.ChartGeometry.integrable_gradient line 114
12. lemma OAI.CAT0Fillings.ChartGeometry.integrable_energy line 126
13. lemma OAI.CAT0Fillings.abs_det_le_prod_dual_norm line 149
14. lemma OAI.CAT0Fillings.abs_det_le_first_dual_norm line 182
15. theorem OAI.CAT0Fillings.ChartGeometry.ae_jacobian_le_duNorm line 197