OAI/NumberTheory/CubicMoment/Theta/CubicThetaExponential.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform exponential decay of the nonconstant cubic cusp expansion.

  1. lemma OAI.CubicFirstMoment.cubicThetaFrequency_lower line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaWhittaker_frequency_exp_bound line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_exp_bound line 44
  4. def OAI.CubicFirstMoment.cubicThetaExpConstant line 72
  5. theorem OAI.CubicFirstMoment.cubicThetaNonconstant_exponential_bound line 76

    Source documentation

    An explicit exponential bound uniform in horizontal position.

    theorem cubicThetaNonconstant_exponential_bound {a : Eisenstein → ℂ} {C v : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, n ≠ 0 → ‖a n‖ ≤ C*norm n)
    (hv : 1 ≤ v) (z : ℂ) :
    ‖cubicThetaNonconstant a (z,v)‖ ≤ cubicThetaExpConstant C*Real.exp (-(Real.pi/9)*v) := by
…

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