OAI/NumberTheory/CubicMoment/Theta/CubicThetaHeightDecay.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary power decay at the infinite cusp, derived from the actual Whittaker integral and a single absolutely convergent lattice majorant.

  1. lemma OAI.CubicFirstMoment.cubicThetaFrequency_rpow line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_height_bound line 27
  3. theorem OAI.CubicFirstMoment.cubicThetaNonconstant_height_bound line 69

    Source documentation

    The full nonconstant cusp expansion decreases faster than any prescribed power, uniformly in horizontal position.

    theorem cubicThetaNonconstant_height_bound (k : ℕ) (hk : 3 ≤ k)
    {a : Eisenstein → ℂ} {C v : ℝ} (hC : 0 ≤ C)
    (ha : ∀ n : Eisenstein, n ≠ 0 → ‖a n‖ ≤ C*norm n)
    (hv : 0 < v) (z : ℂ) :
    ‖cubicThetaNonconstant a (z,v)‖ ≤
      (C*cubicWhittakerPowerConstant k*81^((k:ℝ)-2/3)*
        (∑' n : Eisenstein, norm n^(-4/3:ℝ)))*v^(4/3-2*(k:ℝ)) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicWhittakerPowerConstant