OAI/Geometry/CylinderCovering/Rational/CoordinateDictionary.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RationalDictionary.c0_pos line 10
2. theorem OAI.RationalDictionary.ell_pos line 11
3. theorem OAI.RationalDictionary.ell_ne_zero line 12
4. theorem OAI.RationalDictionary.c0_sq line 14
5. theorem OAI.RationalDictionary.ell_eq_half_c0 line 19
6. theorem OAI.RationalDictionary.two_ell_eq_c0 line 21
7. theorem OAI.RationalDictionary.ell_mul_c0 line 23
8. theorem OAI.RationalDictionary.ell_sq line 27
9. theorem OAI.RationalDictionary.hasDerivAt_g line 31
10. theorem OAI.RationalDictionary.a0_eq_sq_mul_v1 line 39
11. theorem OAI.RationalDictionary.centeredPadding_eq_margin_mul_tilt_sq line 46
12. theorem OAI.RationalDictionary.parameter_positivity line 53
13. theorem OAI.RationalDictionary.cutoff_iff line 60
14. theorem OAI.RationalDictionary.wedge_iff line 63
15. theorem OAI.RationalDictionary.v1_dictionary line 81
16. theorem OAI.RationalDictionary.v2_dictionary line 93
17. theorem OAI.RationalDictionary.ceiling_dictionary line 103
18. theorem OAI.RationalDictionary.ceiling_inequality_iff line 116
19. theorem OAI.RationalDictionary.labelDomain_iff line 131
20. theorem OAI.RationalDictionary.vec2_zero line 152
21. theorem OAI.RationalDictionary.vec2_one line 153
22. theorem OAI.RationalDictionary.vec3_zero line 154
23. theorem OAI.RationalDictionary.vec3_one line 155
24. theorem OAI.RationalDictionary.vec3_two line 156
25. theorem OAI.RationalDictionary.labelMap_inverseLabelMap line 158
26. theorem OAI.RationalDictionary.inverseLabelMap_labelMap line 164
27. theorem OAI.RationalDictionary.reflectLabel_involutive line 170
28. theorem OAI.RationalDictionary.reflectLabel_domain_iff line 174
29. theorem OAI.RationalDictionary.free_coordinate_iff line 180
30. theorem OAI.RationalDictionary.first_point_dictionary line 186
31. theorem OAI.RationalDictionary.centered_a_neg line 219
32. theorem OAI.RationalDictionary.centered_b_neg line 223
33. theorem OAI.RationalDictionary.second_point_dictionary line 228
34. theorem OAI.RationalDictionary.first_lineMap_dictionary line 256
35. theorem OAI.RationalDictionary.second_lineMap_dictionary line 264
36. theorem OAI.RationalDictionary.phi_image_firstSweep line 272
37. theorem OAI.RationalDictionary.phi_image_secondSweep line 297
38. theorem OAI.RationalDictionary.sweep_dictionary line 322
39. theorem OAI.RationalDictionary.v1_divider line 331
40. theorem OAI.RationalDictionary.threshold_sum line 337
41. theorem OAI.RationalDictionary.threshold_dichotomy line 344
42. theorem OAI.RationalDictionary.squared_slope_dictionary line 355
43. theorem OAI.RationalDictionary.coordinate_identity line 367