OAI/Geometry/CylinderCovering/Beams/Cost.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.BeamCost.inv_sqrt_quadratic line 10
  2. theorem OAI.CylinderCovering.BeamCost.perturbation_expansion line 43
  3. theorem OAI.CylinderCovering.BeamCost.ST_bounds line 76
  4. theorem OAI.CylinderCovering.BeamCost.beamDensity_expansion line 86
  5. theorem OAI.CylinderCovering.BeamCost.integral_S line 106
  6. theorem OAI.CylinderCovering.BeamCost.integral_T line 115
  7. theorem OAI.CylinderCovering.BeamCost.integral_S_sq line 127
  8. theorem OAI.CylinderCovering.BeamCost.integral_beam_taylor line 140
  9. theorem OAI.CylinderCovering.BeamCost.beamDensity_continuousOn line 158
  10. theorem OAI.CylinderCovering.BeamCost.beamCost_expansion_N line 173
  11. theorem OAI.CylinderCovering.BeamCost.beamCost_expansion line 197
  12. theorem OAI.CylinderCovering.BeamCost.inv_sqrt_loss line 223
  13. theorem OAI.CylinderCovering.BeamCost.positive_part_padding line 239
  14. theorem OAI.CylinderCovering.BeamCost.stripWidth_bounds line 249
  15. theorem OAI.CylinderCovering.BeamCost.stripDensity_width_error line 264
  16. theorem OAI.CylinderCovering.BeamCost.beamDensity_physical line 294
  17. theorem OAI.CylinderCovering.BeamCost.cutoff_bounds line 305
  18. theorem OAI.CylinderCovering.BeamCost.cutoff_eq_inv_sqrt line 313
  19. theorem OAI.CylinderCovering.BeamCost.strip_quadratic_bounds line 320
  20. theorem OAI.CylinderCovering.BeamCost.stripPolynomial_nonneg line 329
  21. theorem OAI.CylinderCovering.BeamCost.stripPolynomial_nonpos line 338
  22. theorem OAI.CylinderCovering.BeamCost.stripPolynomial_collar_bound line 354
  23. theorem OAI.CylinderCovering.BeamCost.stripDensity_core_error line 369
  24. theorem OAI.CylinderCovering.BeamCost.positive_part_integral_error line 388
  25. theorem OAI.CylinderCovering.BeamCost.continuous_stripDensity line 436
  26. theorem OAI.CylinderCovering.BeamCost.strip_half_integral_error line 444
  27. theorem OAI.CylinderCovering.BeamCost.stripDensity_even line 471
  28. theorem OAI.CylinderCovering.BeamCost.stripCost_half line 479
  29. theorem OAI.CylinderCovering.BeamCost.integral_stripPolynomial line 490
  30. theorem OAI.CylinderCovering.BeamCost.stripPolynomial_cost line 505
  31. theorem OAI.CylinderCovering.BeamCost.stripCost_expansion line 522
  32. theorem OAI.CylinderCovering.BeamCost.totalCost_expansion line 534
  33. theorem OAI.CylinderCovering.BeamCost.gain_coefficient_bound line 547
  34. theorem OAI.CylinderCovering.BeamCost.totalCost_saving line 552
  35. theorem OAI.CylinderCovering.BeamCost.totalCost_lt_four line 559
  36. theorem OAI.CylinderCovering.BeamCost.exists_strict_gain line 564
  37. theorem OAI.CylinderCovering.BeamCost.fullCost line 568