OAI/Geometry/CylinderCovering/Angular/CubicCost.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.Cubic.cubicCost_eq_areaSum line 13
2. lemma OAI.CylinderCovering.Cubic.cubicCost_div_H line 17
3. theorem OAI.CylinderCovering.Cubic.cubicCost_expansion line 22
4. theorem OAI.CylinderCovering.Cubic.cubicCost_strict line 27
5. theorem OAI.CylinderCovering.Cubic.cubicCost_bigO line 38
6. theorem OAI.CylinderCovering.Cubic.scaled_cubicCost_expansion line 54
7. lemma OAI.CylinderCovering.Cubic.scaled_ceil_count line 68
8. lemma OAI.CylinderCovering.Cubic.scaled_cap line 75