OAI/Geometry/CylinderCovering/Radial/CapCosts.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.RadialCaps.H_nonneg line 11
  2. theorem OAI.CylinderCovering.RadialCaps.D0_nonneg line 13
  3. theorem OAI.CylinderCovering.RadialCaps.H_le_one line 15
  4. theorem OAI.CylinderCovering.RadialCaps.D0_le_three line 21
  5. theorem OAI.CylinderCovering.RadialCaps.density_integral line 28
  6. theorem OAI.CylinderCovering.RadialCaps.scalar_remainder line 44
  7. theorem OAI.CylinderCovering.RadialCaps.continuous_Q_integrand line 82
  8. theorem OAI.CylinderCovering.RadialCaps.padded_cost_remainder line 93
  9. theorem OAI.CylinderCovering.RadialCaps.linear_cost_remainder line 133
  10. theorem OAI.CylinderCovering.RadialCaps.cubic_cost_remainder line 139
  11. theorem OAI.CylinderCovering.RadialCaps.rpow_five_halves line 154
  12. theorem OAI.CylinderCovering.RadialCaps.fractional_cost_remainder line 159
  13. theorem OAI.CylinderCovering.RadialCaps.eventually_small_scale line 176
  14. theorem OAI.CylinderCovering.RadialCaps.linear_cost_bigO line 188
  15. theorem OAI.CylinderCovering.RadialCaps.cubic_cost_bigO line 197
  16. theorem OAI.CylinderCovering.RadialCaps.fractional_cost_bigO line 206
  17. theorem OAI.CylinderCovering.RadialCaps.strict_of_remainder line 216
  18. theorem OAI.CylinderCovering.RadialCaps.linear_cost_strict line 226
  19. theorem OAI.CylinderCovering.RadialCaps.cubic_cost_strict line 240
  20. theorem OAI.CylinderCovering.RadialCaps.fractional_cost_strict line 254
  21. theorem OAI.CylinderCovering.RadialCaps.fixed_margin_coefficients line 270
  22. theorem OAI.CylinderCovering.RadialCaps.cubic_coefficients line 279
  23. theorem OAI.CylinderCovering.RadialCaps.fractional_coefficients line 283
  24. theorem OAI.CylinderCovering.RadialCaps.continuous_linearCap line 290
  25. theorem OAI.CylinderCovering.RadialCaps.continuous_cubicCap line 294
  26. theorem OAI.CylinderCovering.RadialCaps.continuous_fractionalCap line 298
  27. theorem OAI.CylinderCovering.RadialCaps.linearCap_pos line 302
  28. theorem OAI.CylinderCovering.RadialCaps.cubicCap_pos line 306
  29. theorem OAI.CylinderCovering.RadialCaps.fractionalCap_pos line 311