OAI/Geometry/Immersion/ClosedSurface/LengthMargins.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.PhaseGeometry.universal_normalized_length_margin line 14
2. theorem OAI.ClosedSurfaceR4.PhaseGeometry.universal_relative_length_margin line 54
3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.norm_secondQuadratic_rotated_smul line 79
4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.norm_secondQuadratic_rotated_neg line 86
5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.power_weight_length_pairs line 91
6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.good_of_direction_length_pos line 118
7. theorem OAI.ClosedSurfaceR4.PhaseGeometry.quantitative_labeled_phase_lengths_with_catalog line 128
8. theorem OAI.ClosedSurfaceR4.PhaseGeometry.quantitative_labeled_phase_lengths line 176