OAI/NumberTheory/CubicMoment/Transform/MetaplecticPartialSums.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact collection of the literal primary Gauss series by its integer norm, and the elementary specialization of HB2000 Lemma 1.

  1. lemma OAI.CubicFirstMoment.tsum_vanish line 14
  2. def OAI.CubicFirstMoment.metaplecticNormCoefficient line 19
  3. lemma OAI.CubicFirstMoment.metaplecticNormCoefficient_zero line 22
  4. lemma OAI.CubicFirstMoment.metaplectic_norm_LSeries line 30
  5. def OAI.CubicFirstMoment.metaplecticPartialSum line 64
  6. lemma OAI.CubicFirstMoment.abelCumulative_metaplecticNormCoefficient line 67
  7. lemma OAI.CubicFirstMoment.MetaplecticContinuation.differentiable_right line 113
  8. lemma OAI.CubicFirstMoment.metaplectic_right_abel line 134

    Source documentation

    A cumulative coefficient estimate constructs the right-half-plane continuation; neither the integral identity nor its growth bound is assumed.

    lemma metaplectic_right_abel {F : Eisenstein → ℂ → ℂ}
    (hF : MetaplecticContinuation F) {r : Eisenstein} (hr : primary r) (hs : Squarefree r)
    {B : ℝ} (hB : ∀ x : ℝ, 1 ≤ x →
      ‖metaplecticPartialSum r x‖ ≤ B*x^(5/6:ℝ)) :
    ∀ s : ℂ, (5/6:ℝ) < s.re →
      F r s = abelContinuation (metaplecticNormCoefficient r) s := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticContinuation, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticPartialSum, OAI.CubicFirstMoment.abelContinuation, OAI.CubicFirstMoment.metaplecticNormCoefficient