OAI/NumberTheory/CubicMoment/Transform/MetaplecticCoefficientSeries.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Summing the separated arithmetic majorant from the actual Voronoi support. The two free norm series and the ramified geometric series converge, while the squarefree supported factor is a divisor of the level.

  1. theorem OAI.CubicFirstMoment.metaplectic_divisor_weight_small_power line 13
  2. abbrev OAI.CubicFirstMoment.MetaplecticCoefficientCode line 30
  3. def OAI.CubicFirstMoment.metaplecticCodeWeight line 33
  4. lemma OAI.CubicFirstMoment.metaplecticCodeWeight_nonneg line 38
  5. lemma OAI.CubicFirstMoment.metaplectic_product_hasSum line 45
  6. lemma OAI.CubicFirstMoment.metaplecticCodeWeight_hasSum line 51
  7. lemma OAI.CubicFirstMoment.metaplecticCodeWeight_summable line 95
  8. lemma OAI.CubicFirstMoment.metaplecticCodeWeight_tsum line 98
  9. theorem OAI.CubicFirstMoment.metaplecticCodeWeight_small_power line 107

    Source documentation

    The full separated majorant has an arbitrarily small level loss.

    theorem metaplecticCodeWeight_small_power {ε σ : ℝ} (hε : 0 < ε) (hσ : 0 < σ) :
    ∃ C : ℝ, 0 < C ∧ ∀ r : Eisenstein, primary r →
      (∑' z : MetaplecticCoefficientCode r, metaplecticCodeWeight r σ z) ≤ C*norm r^ε := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.MetaplecticCoefficientCode, OAI.CubicFirstMoment.metaplecticCodeWeight, OAI.CubicFirstMoment.norm