OAI/NumberTheory/CubicMoment/Theta/CubicThetaMellinWeights.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Absolute lattice and kernel masses for exchanging the theta sum with its Mellin integral on the initial right half-plane.

  1. def OAI.CubicFirstMoment.cubicWhittakerNormMass line 12
  2. lemma OAI.CubicFirstMoment.cubicWhittakerNormMass_nonneg line 15
  3. lemma OAI.CubicFirstMoment.cubicWhittaker_norm_integral_scale line 20
  4. lemma OAI.CubicFirstMoment.cubicTheta_mellin_weight_summable line 36

    Source documentation

    Bounded normalized coefficients give an absolutely convergent initial Dirichlet series for Re u > 2.

    lemma cubicTheta_mellin_weight_summable {a : Eisenstein → ℂ} {C σ : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, ‖a n‖ ≤ C) (hσ : 2 < σ) :
    Summable (fun n : Eisenstein => if n = 0 then (0:ℝ) else
      ‖a n‖*‖cubicThetaFrequency n‖^(-σ)) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicThetaFrequency