OAI/Geometry/CylinderCovering/Rational/Coefficients.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RationalCoefficients.ceiling_integral line 12
  2. theorem OAI.RationalCoefficients.limiting_ceiling_integral line 27
  3. theorem OAI.RationalCoefficients.limiting_angular_energy_integral line 36
  4. theorem OAI.RationalCoefficients.limiting_energy_integral line 52
  5. theorem OAI.RationalCoefficients.limiting_gap line 60
  6. theorem OAI.RationalCoefficients.angular_polynomial_integral line 62
  7. theorem OAI.RationalCoefficients.angular_energy_integral line 79
  8. theorem OAI.RationalCoefficients.angularA0_bounds line 86
  9. theorem OAI.RationalCoefficients.angularA2_bounds line 97
  10. theorem OAI.RationalCoefficients.angularB1_bounds line 108
  11. theorem OAI.RationalCoefficients.radialDensity_bounds line 118
  12. theorem OAI.RationalCoefficients.radialDensity_zero line 142
  13. theorem OAI.RationalCoefficients.radialDensity_limit line 145
  14. theorem OAI.RationalCoefficients.radialDensity_measurable line 162
  15. theorem OAI.RationalCoefficients.polarCost_eq line 166
  16. theorem OAI.RationalCoefficients.polarCost_limit line 171
  17. theorem OAI.RationalCoefficients.wedgeCost_eq_polarCost line 195
  18. theorem OAI.RationalCoefficients.wedgeCost_limit line 217