OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspCoefficients.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The two additional arithmetic families in DR v3 (5.13)--(5.14), normalized by |mu| on the common lambda^-4 frequency lattice.

  1. lemma OAI.CubicFirstMoment.cubicTheta_unit_norm line 11
  2. def OAI.CubicFirstMoment.CubicThetaCoordinates.cuspCoefficient line 17
  3. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.cuspCoefficient_norm_le line 26
  4. def OAI.CubicFirstMoment.cubicThetaCuspCoefficient line 43
  5. lemma OAI.CubicFirstMoment.cubicThetaCuspCoefficient_formula line 46
  6. lemma OAI.CubicFirstMoment.cubicThetaCuspCoefficient_zero line 52
  7. lemma OAI.CubicFirstMoment.cubicThetaCuspCoefficient_norm_le line 57
  8. lemma OAI.CubicFirstMoment.cubicThetaCuspCoefficient_bound line 64
  9. theorem OAI.CubicFirstMoment.cubicThetaCusp_summable line 71

    Source documentation

    All three literal arithmetic coefficient families define convergent Fourier expansions in the upper half-space.

    theorem cubicThetaCusp_summable (j : Fin 3) {v : ℝ} (hv : 0 < v) (z : ℂ) :
    Summable (cubicThetaSeriesTerm (cubicThetaCuspCoefficient j) z v) :=
…

    Mentions: OAI.CubicFirstMoment.cubicThetaSeriesTerm, OAI.CubicFirstMoment.cubicThetaCuspCoefficient