OAI/NumberTheory/CubicMoment/Estimates/CubicWhittakerExponential.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exponential decay retaining an arbitrarily summable polynomial factor.

  1. def OAI.CubicFirstMoment.cubicWhittakerExpConstant line 9
  2. lemma OAI.CubicFirstMoment.cubicWhittakerExpConstant_pos line 12
  3. lemma OAI.CubicFirstMoment.cubicBesselKernel_exp_power_bound line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaWhittaker_exponential_bound line 25
  5. def OAI.CubicFirstMoment.cubicWhittakerMixedConstant line 50
  6. lemma OAI.CubicFirstMoment.cubicWhittakerMixedConstant_pos line 52
  7. theorem OAI.CubicFirstMoment.cubicThetaWhittaker_mixed_bound line 58

    Source documentation

    Half the exponential is retained, while the other half supplies six powers of decay for the two-dimensional frequency sum.

    theorem cubicThetaWhittaker_mixed_bound {v : ℝ} (hv : 0 < v) :
    ‖cubicThetaWhittaker v‖ ≤
      cubicWhittakerMixedConstant*v^(-16/3:ℝ)*Real.exp (-Real.pi*v) := by
…

    Mentions: OAI.CubicFirstMoment.cubicThetaWhittaker, OAI.CubicFirstMoment.cubicWhittakerMixedConstant