OAI/Geometry/CylinderCovering/Radial/SqrtCap.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.RadialSqrtCap.profile_nonneg line 11
2. lemma OAI.CylinderCovering.RadialSqrtCap.profile_le_one line 13
3. lemma OAI.CylinderCovering.RadialSqrtCap.speedSq_nonneg line 19
4. lemma OAI.CylinderCovering.RadialSqrtCap.speedSq_le_three line 21
5. lemma OAI.CylinderCovering.RadialSqrtCap.cap_sq line 27
6. lemma OAI.CylinderCovering.RadialSqrtCap.cap_nonneg line 32
7. lemma OAI.CylinderCovering.RadialSqrtCap.cap_ge_one line 34
8. lemma OAI.CylinderCovering.RadialSqrtCap.cap_continuous line 40
9. lemma OAI.CylinderCovering.RadialSqrtCap.cap_rationalization line 44
10. lemma OAI.CylinderCovering.RadialSqrtCap.cap_padding line 52
11. lemma OAI.CylinderCovering.RadialSqrtCap.integrand_remainder line 67
12. lemma OAI.CylinderCovering.RadialSqrtCap.coefficient_eq line 120
13. lemma OAI.CylinderCovering.RadialSqrtCap.coefficient_integral line 125
14. lemma OAI.CylinderCovering.RadialSqrtCap.integrand_continuous line 144
15. theorem OAI.CylinderCovering.RadialSqrtCap.cost_expansion line 153
16. theorem OAI.CylinderCovering.RadialSqrtCap.exists_padding_threshold line 185
17. theorem OAI.CylinderCovering.RadialSqrtCap.exists_saving_threshold line 206