OAI/Geometry/CylinderCovering/Rational/Integrals.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.RationalIntegrals.ceiling_integral line 11
  2. theorem OAI.CylinderCovering.RationalIntegrals.limiting_ceiling_integral line 25
  3. theorem OAI.CylinderCovering.RationalIntegrals.limiting_energy_angular_integral line 32
  4. theorem OAI.CylinderCovering.RationalIntegrals.limiting_energy_integral line 50
  5. theorem OAI.CylinderCovering.RationalIntegrals.limiting_coefficient_gap line 58
  6. theorem OAI.CylinderCovering.RationalIntegrals.rational_ceiling_coefficient_formula line 63
  7. theorem OAI.CylinderCovering.RationalIntegrals.rational_ceiling_integral_tendsto line 76
  8. theorem OAI.CylinderCovering.RationalIntegrals.rational_ceiling_integral_tendsto_right line 90
  9. theorem OAI.CylinderCovering.RationalIntegrals.uncentered_ceiling_integral line 99
  10. theorem OAI.CylinderCovering.RationalIntegrals.uncentered_energy_integral line 113
  11. theorem OAI.CylinderCovering.RationalIntegrals.uncentered_limiting_gap line 130