OAI/Geometry/CylinderCovering/Beams/Neighborhood.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.BeamNeighborhood.radial_cancellation line 10
2. lemma OAI.CylinderCovering.BeamNeighborhood.intercept_decomposition line 18
3. lemma OAI.CylinderCovering.BeamNeighborhood.transverse_norm_le line 24
4. lemma OAI.CylinderCovering.BeamNeighborhood.shortening_bounds line 30
5. lemma OAI.CylinderCovering.BeamNeighborhood.midpoint_radial_error line 36
6. lemma OAI.CylinderCovering.BeamNeighborhood.midpoint_transverse_error line 47
7. theorem OAI.CylinderCovering.BeamNeighborhood.intercept_mem_paddedSector line 62
8. theorem OAI.CylinderCovering.BeamNeighborhood.sector_isCompact line 78
9. theorem OAI.CylinderCovering.BeamNeighborhood.paddedSector_isCompact line 92
10. theorem OAI.CylinderCovering.BeamNeighborhood.paddedSector_measurable line 95
11. theorem OAI.CylinderCovering.BeamNeighborhood.paddedSector_finiteMeasure line 98