OAI/Geometry/CAT0Fillings/Radial/TotalBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CAT0Fillings.abs_det_le_sqrt_det_of_posSemidef_finite line 28
2. lemma OAI.CAT0Fillings.metricTotalRadialForm_posSemidef line 55
3. lemma OAI.CAT0Fillings.metricTotalRadialForm_quadratic line 70
4. def OAI.CAT0Fillings.finiteDifferentialRow line 88
5. lemma OAI.CAT0Fillings.finiteDifferentialRow_dot line 92
6. def OAI.CAT0Fillings.spatialFunctional line 106
7. lemma OAI.CAT0Fillings.spatialFunctional_toLp line 110
8. theorem OAI.CAT0Fillings.total_radial_test_normalized_det_le line 115