OAI/Geometry/Immersion/ClosedSurface/DirectionStability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.secondQuadratic_sub_form line 13
2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.norm_secondQuadratic_le line 18
3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.norm_rotated_covector line 43
4. theorem OAI.ClosedSurfaceR4.PhaseGeometry.second_form_direction_persists line 50
5. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.convex_variation line 71
6. lemma OAI.ClosedSurfaceR4.RealModes.weighted_coordinate_second_jet line 88
7. lemma OAI.ClosedSurfaceR4.RealModes.coordinate_jets_variation line 100
8. theorem OAI.ClosedSurfaceR4.RealModes.second_form_cell_variation line 143