OAI/Probability/CriticalPercolation/GraphGeometry/EllipseAngles.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.EuclideanEllipse.lineAngle line 14
2. def OAI.CriticalPercolation.EuclideanEllipse.boundaryError line 16
3. lemma OAI.CriticalPercolation.EuclideanEllipse.circle_arg_re line 19
4. lemma OAI.CriticalPercolation.EuclideanEllipse.circle_arg_im line 22
5. lemma OAI.CriticalPercolation.EuclideanEllipse.circle_exp_re line 25
6. lemma OAI.CriticalPercolation.EuclideanEllipse.circle_exp_im line 30
7. lemma OAI.CriticalPercolation.EuclideanEllipse.rotated_major_cos line 35
8. lemma OAI.CriticalPercolation.EuclideanEllipse.boundary_error_lt line 40
9. lemma OAI.CriticalPercolation.EuclideanEllipse.boundary_lift line 55
10. lemma OAI.CriticalPercolation.EuclideanEllipse.boundary_error_seam line 60
11. lemma OAI.CriticalPercolation.EuclideanEllipse.circle_exp_pi line 67
12. lemma OAI.CriticalPercolation.EuclideanEllipse.diskNormalize_seam line 73
13. lemma OAI.CriticalPercolation.EuclideanEllipse.diskNormalize_center line 79