OAI/NumberTheory/CubicMoment/Estimates/CubicBesselSumIntegral.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The positive-quadrant Gamma integral needed for the square of the fixed order-one-third Schlaefli kernel.

  1. def OAI.CubicFirstMoment.cubicBesselSumWeight line 13
  2. def OAI.CubicFirstMoment.cubicBesselTriangle line 15
  3. lemma OAI.CubicFirstMoment.cubicBesselTriangle_nonneg line 18
  4. lemma OAI.CubicFirstMoment.cubicBesselTriangle_inner_integrable line 24
  5. lemma OAI.CubicFirstMoment.cubicBesselTriangle_inner line 32
  6. lemma OAI.CubicFirstMoment.cubicBesselTriangle_integrable line 50
  7. lemma OAI.CubicFirstMoment.cubicBesselTriangle_integral line 72
  8. def OAI.CubicFirstMoment.cubicBesselSumShear line 80
  9. lemma OAI.CubicFirstMoment.cubicBesselSumShear_preserving line 92
  10. lemma OAI.CubicFirstMoment.cubicBesselSumShear_weight line 96
  11. lemma OAI.CubicFirstMoment.cubicBesselSumWeight_integrable line 106
  12. theorem OAI.CubicFirstMoment.cubicBesselSumWeight_integral line 115