OAI/Geometry/CylinderCovering/Radial/CollarRate.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.RadialRiemann.weighted_square_collar_bounds line 10
2. lemma OAI.CylinderCovering.RadialRiemann.step_le_length line 27
3. theorem OAI.CylinderCovering.RadialRiemann.collarSum_sub_zero_bounds line 34
4. theorem OAI.CylinderCovering.RadialRiemann.collarSum_sub_zero_le_div line 66
5. lemma OAI.CylinderCovering.RadialSweep.projectionWeight_bounds line 92
6. lemma OAI.CylinderCovering.RadialSweep.sum_frozenArea_eq_collarSum line 102
7. theorem OAI.CylinderCovering.RadialSweep.frozenCylinder_collar_bounds line 113
8. theorem OAI.CylinderCovering.RadialSweep.frozenCylinder_collar_le_div line 139
9. theorem OAI.CylinderCovering.RadialSweep.frozenCylinder_collar_uniform line 161