OAI/NumberTheory/CubicMoment/Theta/CubicThetaSeries.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence of the cubic theta Fourier expansion on its actual common cusp frequency lattice lambda^{-4} Z[omega]. The coefficient here includes the factor 1/|mu| when the Whittaker function is evaluated at |mu|v.

  1. def OAI.CubicFirstMoment.cubicThetaFrequency line 14
  2. def OAI.CubicFirstMoment.cubicThetaSeriesTerm line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaFrequency_pos line 20
  4. lemma OAI.CubicFirstMoment.cubicThetaFrequency_sq line 25
  5. lemma OAI.CubicFirstMoment.cubicThetaFrequency_power line 33
  6. lemma OAI.CubicFirstMoment.cubicThetaWhittaker_frequency_bound line 53
  7. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_bound line 64
  8. theorem OAI.CubicFirstMoment.cubicThetaSeries_summable line 93

    Source documentation

    Absolute convergence needs only this coarse coefficient bound; the arithmetic theta coefficient formulas are constructed separately.

    theorem cubicThetaSeries_summable {a : Eisenstein → ℂ} {C v : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, n ≠ 0 → ‖a n‖ ≤ C*norm n)
    (hv : 0 < v) (z : ℂ) : Summable (cubicThetaSeriesTerm a z v) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicThetaSeriesTerm