OAI/Probability/CriticalPercolation/GraphGeometry/EllipseBoundary.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.EuclideanEllipse.rotated_re line 16
2. lemma OAI.CriticalPercolation.EuclideanEllipse.rotated_im line 20
3. lemma OAI.CriticalPercolation.EuclideanEllipse.norm_rotated line 24
4. lemma OAI.CriticalPercolation.EuclideanEllipse.original_components line 27
5. lemma OAI.CriticalPercolation.EuclideanEllipse.normalize_transverse_le line 34
6. lemma OAI.CriticalPercolation.EuclideanEllipse.normalized_far_major line 41
7. lemma OAI.CriticalPercolation.EuclideanEllipse.doubled_angle_le_sine line 59
8. lemma OAI.CriticalPercolation.BondGraph.ellipseExit_subset_longStrip line 84
9. theorem OAI.CriticalPercolation.BondGraph.favored_boundary_major_small line 104