OAI/Geometry/CylinderCovering/Radial/Integral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.RadialIntegral.transverse_integral_bound line 11
2. theorem OAI.CylinderCovering.RadialIntegral.radial_integral_bound line 55
3. theorem OAI.CylinderCovering.RadialIntegral.integral_eq_sub_of_within_deriv line 63
4. theorem OAI.CylinderCovering.RadialIntegral.integral_footprint line 86
5. theorem OAI.CylinderCovering.RadialIntegral.aligned_increment line 130
6. theorem OAI.CylinderCovering.RadialIntegral.aligned_frozen_intercept line 156
7. theorem OAI.CylinderCovering.RadialIntegral.aligned_footprint line 170