OAI/Geometry/CylinderCovering/Caps/FractionalEstimates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.P_half line 10
2. lemma OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.g_half line 14
3. lemma OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.defect line 18
4. lemma OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.square_difference line 23
5. lemma OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.polynomial_errors line 38
6. lemma OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.profile_comparison line 56
7. lemma OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.first_identity line 68
8. lemma OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.fractional_le_square line 74
9. theorem OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.first_failure_estimate line 82
10. theorem OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.paired_failure_estimates line 112
11. lemma OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.fractional_dominates_cube line 138
12. theorem OAI.CylinderCovering.HalfHeightCaps.FractionalEstimates.fractional_failures_incompatible line 153