OAI/Geometry/CylinderCovering/Angular/CubicArea.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.Cubic.profile_le_one line 13
2. lemma OAI.CylinderCovering.Cubic.areaDensity_identity line 19
3. lemma OAI.CylinderCovering.Cubic.areaDensity_integral line 25
4. lemma OAI.CylinderCovering.Cubic.inverseSqrt_bounds line 45
5. theorem OAI.CylinderCovering.Cubic.scalar_cubic_remainder line 66
6. lemma OAI.CylinderCovering.Cubic.coefficient_bounds line 121
7. lemma OAI.CylinderCovering.Cubic.profile_lipschitz line 152
8. lemma OAI.CylinderCovering.Cubic.profileMax_error line 169
9. lemma OAI.CylinderCovering.Cubic.square_error line 185
10. lemma OAI.CylinderCovering.Cubic.density_error line 194
11. lemma OAI.CylinderCovering.Cubic.continuous_areaDensity line 233
12. lemma OAI.CylinderCovering.Cubic.interval_density_error line 237
13. lemma OAI.CylinderCovering.Cubic.count_mul_step line 254
14. def OAI.CylinderCovering.Cubic.areaCoefficientSum line 259
15. lemma OAI.CylinderCovering.Cubic.integral_mesh_sum line 263
16. lemma OAI.CylinderCovering.Cubic.areaCoefficientSum_error line 271
17. lemma OAI.CylinderCovering.Cubic.areaTerm_remainder line 303
18. lemma OAI.CylinderCovering.Cubic.areaSum_coefficient_remainder line 319
19. theorem OAI.CylinderCovering.Cubic.areaSum_expansion line 364