OAI/Geometry/CylinderCovering/Rational/Field.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SlopeRational.vec2_zero line 11
2. theorem OAI.SlopeRational.vec2_one line 12
3. theorem OAI.SlopeRational.a_even line 14
4. theorem OAI.SlopeRational.b_odd line 17
5. theorem OAI.SlopeRational.a_simplified line 21
6. theorem OAI.SlopeRational.ceilingCoefficient_eq line 27
7. theorem OAI.SlopeRational.b_at_divider line 31
8. theorem OAI.SlopeRational.ceiling_square_surplus line 35
9. theorem OAI.SlopeRational.ceiling_square_surplus_nonneg line 42
10. theorem OAI.SlopeRational.right_wall_tangent line 49
11. theorem OAI.SlopeRational.left_wall_tangent line 55
12. theorem OAI.SlopeRational.potential_right_wall line 61
13. theorem OAI.SlopeRational.potential_left_wall line 66
14. def OAI.SlopeRational.matrixCLM line 71
15. theorem OAI.SlopeRational.matrixCLM_apply line 77
16. theorem OAI.SlopeRational.hasFDerivAt_vec2 line 82
17. theorem OAI.SlopeRational.field_fderiv line 94
18. theorem OAI.SlopeRational.matrixCLM_trace line 128
19. theorem OAI.SlopeRational.matrixCLM_det line 135
20. theorem OAI.SlopeRational.field_trace_det line 142
21. theorem OAI.SlopeRational.field_det_neg line 152
22. theorem OAI.SlopeRational.field_contDiffAt line 160
23. theorem OAI.SlopeRational.field_contDiffOn line 177
24. theorem OAI.SlopeRational.radius_nonneg_of_mem_wedge line 181
25. theorem OAI.SlopeRational.denominator_pos_of_mem_wedge line 184
26. theorem OAI.SlopeRational.field_smoothNear_labelDomain line 187
27. theorem OAI.SlopeRational.plane_charpoly line 194
28. theorem OAI.SlopeRational.field_eigenvalues line 200
29. theorem OAI.SlopeRational.labelDomain_coordinate_bounds line 213
30. theorem OAI.SlopeRational.plane_norm_sq line 221
31. theorem OAI.SlopeRational.plane_norm_le_sum line 225
32. theorem OAI.SlopeRational.eigenvalue_smul line 231
33. theorem OAI.SlopeRational.scaled_field_eigenvalues line 242
34. theorem OAI.SlopeRational.eigenvalue_bound_on_wedge line 253
35. theorem OAI.SlopeRational.scaled_field_spectral_window line 264
36. theorem OAI.SlopeRational.a_combined line 279
37. theorem OAI.SlopeRational.field_coordinate_bounds line 288
38. theorem OAI.SlopeRational.field_norm_bound line 314
39. theorem OAI.SlopeRational.potential_hasDerivAt_Y line 322
40. theorem OAI.SlopeRational.potential_hasDerivAt_T line 329
41. theorem OAI.SlopeRational.wall_plus_factor line 339
42. theorem OAI.SlopeRational.wall_minus_factor line 347
43. theorem OAI.SlopeRational.tilted_wall_plus line 355
44. theorem OAI.SlopeRational.tilted_wall_minus line 365
45. theorem OAI.SlopeRational.mem_wedge_iff_walls_nonneg line 375
46. theorem OAI.SlopeRational.tilted_mem_wedge_iff line 385