OAI/Geometry/CAT0Fillings/Radial/SpatialBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.spatialRadialForm_rankOne_decomposition line 28
2. lemma OAI.CAT0Fillings.dotProduct_vecMulVec_self line 39
3. theorem OAI.CAT0Fillings.spatialRadialForm_posSemidef line 44
4. lemma OAI.CAT0Fillings.spatialRadialForm_quadratic line 60
5. theorem OAI.CAT0Fillings.abs_det_le_spatialRadialJacobian line 71