OAI/Geometry/CylinderCovering/Convexity/ResidualDisk.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.ResidualDisk.distance_le_sqrt_two line 11
2. lemma OAI.CylinderCovering.ResidualDisk.physicalWeight_le_one line 23
3. lemma OAI.CylinderCovering.ResidualDisk.disk_area line 30
4. theorem OAI.CylinderCovering.ResidualDisk.disk_cylinder_area line 37
5. theorem OAI.CylinderCovering.ResidualDisk.disk_cover_of_increment_bound line 50
6. theorem OAI.CylinderCovering.ResidualDisk.disk_cover_of_derivative_bound line 84
7. theorem OAI.CylinderCovering.ResidualDisk.uniform_residual_disks line 99
8. theorem OAI.CylinderCovering.ResidualDisk.summable_residual_cost line 126
9. theorem OAI.CylinderCovering.ResidualDisk.logarithmic_summable_cost line 153