OAI/NumberTheory/CubicMoment/Estimates/CubicWhittakerEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Absolute squared Mellin masses for the fixed cubic Whittaker kernel.

  1. lemma OAI.CubicFirstMoment.cubicThetaWhittaker_sq_bound line 11
  2. def OAI.CubicFirstMoment.cubicWhittakerEnergyMass line 26
  3. lemma OAI.CubicFirstMoment.cubicWhittakerEnergy_integrable line 29
  4. lemma OAI.CubicFirstMoment.cubicWhittakerEnergyMass_nonneg line 52
  5. lemma OAI.CubicFirstMoment.cubicWhittakerEnergy_mass_scale line 57
  6. lemma OAI.CubicFirstMoment.cubicWhittakerEnergy_scaled_integrable line 82