OAI/Analysis/BoxTransport/Motion.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoxTransport.Routing.centerKey line 13
2. def OAI.BoxTransport.Routing.coordinateRank line 15
3. theorem OAI.BoxTransport.Routing.centerKey_injective line 18
4. theorem OAI.BoxTransport.Routing.coordinateRank_strict line 23
5. theorem OAI.BoxTransport.Routing.coordinateRank_lt line 37
6. theorem OAI.BoxTransport.Routing.centerKey_coordinate_le line 47
7. def OAI.BoxTransport.Routing.spreadCenter line 51
8. theorem OAI.BoxTransport.Routing.spreadCenter_zero line 55
9. theorem OAI.BoxTransport.Routing.spreadCenter_gap line 60
10. theorem OAI.BoxTransport.Routing.spreadCenter_separated line 83
11. theorem OAI.BoxTransport.Routing.spreadCenter_disjoint line 100
12. def OAI.BoxTransport.Routing.stageSwitch line 111
13. theorem OAI.BoxTransport.Routing.contDiff_stageSwitch line 114
14. theorem OAI.BoxTransport.Routing.stageSwitch_mem line 118
15. theorem OAI.BoxTransport.Routing.stageSwitch_zero line 121
16. theorem OAI.BoxTransport.Routing.stageSwitch_one line 125
17. theorem OAI.BoxTransport.Routing.stageSwitch_before line 129
18. theorem OAI.BoxTransport.Routing.stageSwitch_after line 134
19. theorem OAI.BoxTransport.Routing.stageSwitch_cases line 139
20. def OAI.BoxTransport.Routing.routeCenterParameters line 164
21. def OAI.BoxTransport.Routing.routeCenters line 174
22. theorem OAI.BoxTransport.Routing.contDiff_routeCenters line 177
23. theorem OAI.BoxTransport.Routing.routeCenter_stage₀ line 184
24. theorem OAI.BoxTransport.Routing.routeCenter_stage₁ line 190
25. theorem OAI.BoxTransport.Routing.routeCenter_stage₂ line 195
26. theorem OAI.BoxTransport.Routing.routeCenter_stage₃ line 200
27. theorem OAI.BoxTransport.Routing.routeCenter_stage₄ line 205
28. theorem OAI.BoxTransport.Routing.routeCenters_before line 212
29. theorem OAI.BoxTransport.Routing.routeCenters_after line 218
30. theorem OAI.BoxTransport.Routing.private_layers_separated line 224
31. def OAI.BoxTransport.Routing.scaleRatio line 232
32. def OAI.BoxTransport.Routing.balancedScale line 235
33. theorem OAI.BoxTransport.Routing.balancedScale_zero line 239
34. theorem OAI.BoxTransport.Routing.balancedScale_one line 242
35. theorem OAI.BoxTransport.Routing.linearBlend_between line 251
36. theorem OAI.BoxTransport.Routing.linearBlend_pos line 264
37. theorem OAI.BoxTransport.Routing.linearBlend_product_lower line 268
38. theorem OAI.BoxTransport.Routing.balancedScale_pos line 292
39. theorem OAI.BoxTransport.Routing.balancedScale_det line 300
40. theorem OAI.BoxTransport.Routing.balancedScale_le line 307
41. def OAI.BoxTransport.Routing.routeScales line 326
42. theorem OAI.BoxTransport.Routing.scaleRatio_pos line 329
43. theorem OAI.BoxTransport.Routing.scaleRatio_mul_width line 335
44. theorem OAI.BoxTransport.Routing.contDiff_routeScales line 341
45. theorem OAI.BoxTransport.Routing.routeScales_pos line 359
46. theorem OAI.BoxTransport.Routing.routeScales_det line 364
47. theorem OAI.BoxTransport.Routing.scaleRatio_det line 370
48. theorem OAI.BoxTransport.Routing.routeScales_le line 376
49. theorem OAI.BoxTransport.Routing.routeScales_before line 384
50. theorem OAI.BoxTransport.Routing.routeScales_after line 388
51. theorem OAI.BoxTransport.Routing.routeScales_width_le line 393
52. def OAI.BoxTransport.Routing.boxDataBound line 404
53. theorem OAI.BoxTransport.Routing.boxDataBound_ge_one line 407
54. theorem OAI.BoxTransport.Routing.boxDataBound_bounds line 413
55. theorem OAI.BoxTransport.Routing.route_padded_disjoint line 436
56. def OAI.BoxTransport.Routing.stationaryMotionField line 490
57. theorem OAI.BoxTransport.Routing.finite_motion_bound line 496
58. theorem OAI.BoxTransport.Routing.stationaryMotionField_realizes line 516
59. def OAI.BoxTransport.Routing.routedField line 580
60. theorem OAI.BoxTransport.Routing.routedField_realizes line 584
61. theorem OAI.BoxTransport.Routing.exists_routedField_realization line 633