OAI/Geometry/CylinderCovering/Radial/AreaConvergence.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.RadialSweep.abs_scalar_le_bound line 11
2. lemma OAI.CylinderCovering.RadialSweep.scalarBound_nonneg line 15
3. lemma OAI.CylinderCovering.RadialSweep.radialError_nonneg line 19
4. lemma OAI.CylinderCovering.RadialSweep.collar_pos line 22
5. lemma OAI.CylinderCovering.RadialSweep.leftTip_lt_rightEdge line 26
6. lemma OAI.CylinderCovering.RadialSweep.kappa_nonneg line 37
7. lemma OAI.CylinderCovering.RadialSweep.frozenArea_nonneg line 39
8. theorem OAI.CylinderCovering.RadialSweep.frozenArea_tendsto line 47
9. lemma OAI.CylinderCovering.RadialSweep.weightedArea_nonneg line 54
10. lemma OAI.CylinderCovering.RadialSweep.frozenArea_eventually_lt line 61