OAI/Geometry/CylinderCovering/Ruled/Retention.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RuledApproximation.OrthogonalRetention.affineVelocity line 9
2. def OAI.RuledApproximation.OrthogonalRetention.center line 12
3. def OAI.RuledApproximation.OrthogonalRetention.square line 15
4. lemma OAI.RuledApproximation.OrthogonalRetention.square_isSquareTile line 19
5. lemma OAI.RuledApproximation.OrthogonalRetention.inverse_bound line 24
6. lemma OAI.RuledApproximation.OrthogonalRetention.retention_bound line 40
7. lemma OAI.RuledApproximation.OrthogonalRetention.plane_cover line 60
8. lemma OAI.RuledApproximation.OrthogonalRetention.square_error_bound line 111
9. def OAI.RuledApproximation.OrthogonalRetention.indexBox line 119
10. lemma OAI.RuledApproximation.OrthogonalRetention.indexBox_card line 122
11. lemma OAI.RuledApproximation.OrthogonalRetention.mem_indexBox_of_norm_bound line 128
12. def OAI.RuledApproximation.OrthogonalRetention.retained line 158
13. lemma OAI.RuledApproximation.OrthogonalRetention.mem_retained_iff line 164
14. lemma OAI.RuledApproximation.OrthogonalRetention.retained_card_le line 177
15. lemma OAI.RuledApproximation.OrthogonalRetention.retained_empty line 184
16. theorem OAI.RuledApproximation.OrthogonalRetention.retained_cover_in_frame line 189
17. theorem OAI.RuledApproximation.OrthogonalRetention.finite_retained_cover line 220
18. def OAI.RuledApproximation.OrthogonalRetention.physicalFamily line 236
19. lemma OAI.RuledApproximation.OrthogonalRetention.physicalFamily_parallelogram line 242
20. lemma OAI.RuledApproximation.OrthogonalRetention.physicalFamily_area line 248
21. theorem OAI.RuledApproximation.OrthogonalRetention.physical_finite_retained_cover line 256