OAI/Probability/CriticalPercolation/GraphGeometry/EuclideanEllipse.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.EuclideanEllipse.diagonal line 12
2. lemma OAI.CriticalPercolation.EuclideanEllipse.diagonal_add line 14
3. lemma OAI.CriticalPercolation.EuclideanEllipse.diagonal_sub line 17
4. lemma OAI.CriticalPercolation.EuclideanEllipse.diagonal_comp line 20
5. lemma OAI.CriticalPercolation.EuclideanEllipse.diagonal_one line 23
6. lemma OAI.CriticalPercolation.EuclideanEllipse.diagonal_neg line 24
7. lemma OAI.CriticalPercolation.EuclideanEllipse.diagonal_norm_le line 27
8. def OAI.CriticalPercolation.EuclideanEllipse.normalize line 38
9. def OAI.CriticalPercolation.EuclideanEllipse.expand line 41
10. lemma OAI.CriticalPercolation.EuclideanEllipse.normalize_sub line 44
11. lemma OAI.CriticalPercolation.EuclideanEllipse.expand_normalize line 48
12. lemma OAI.CriticalPercolation.EuclideanEllipse.normalize_expand line 54
13. lemma OAI.CriticalPercolation.EuclideanEllipse.normalize_norm_le line 60
14. lemma OAI.CriticalPercolation.EuclideanEllipse.expand_norm_le line 69
15. lemma OAI.CriticalPercolation.EuclideanEllipse.normalize_center line 76
16. lemma OAI.CriticalPercolation.EuclideanEllipse.normalize_neg line 81
17. lemma OAI.CriticalPercolation.EuclideanEllipse.normalize_components line 85
18. lemma OAI.CriticalPercolation.EuclideanEllipse.normalize_origin line 90
19. lemma OAI.CriticalPercolation.EuclideanEllipse.normalize_real_linear line 93