OAI/Geometry/CylinderCovering/Caps/CompensationEstimates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.square_le_one line 7
2. lemma OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.alpha_bounds line 10
3. lemma OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.profile_bounds line 17
4. lemma OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.abs_product_le_one line 25
5. lemma OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.weight_bounds line 31
6. lemma OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.weighted_square_le_half line 40
7. lemma OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.identity line 47
8. theorem OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.radial_excess_bounds line 55
9. lemma OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.radial_coordinate_error line 75
10. theorem OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.angular_errors line 97
11. lemma OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.squared_error line 109
12. lemma OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.monotone_profile_comparison line 123
13. theorem OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.weighted_comparison line 128
14. theorem OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.cubic_padding_lower line 142
15. theorem OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.cubic_failure_lower line 151
16. theorem OAI.CylinderCovering.HalfHeightCaps.CompensationEstimates.cubic_failures_incompatible line 174