OAI/Geometry/NodalSets/Charts/CorrugationFrozenFrame.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Geometry.metric_perpendicular_unit_compact line 11
2. lemma OAI.Yau.Geometry.exists_maximizing_perpendicular_axis line 27
3. def OAI.Yau.Geometry.frozenFrameCovector line 37
4. lemma OAI.Yau.Geometry.frozenFrameCovector_apply line 40
5. lemma OAI.Yau.Geometry.frozenFrameCovector_axis line 43
6. lemma OAI.Yau.Geometry.frozenFrameCovector_metric line 47
7. theorem OAI.Yau.Geometry.exists_corrugation_frozen_frame line 55