MetaplecticCoefficientDecay.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual dual coefficient bound becomes a product of a geometric ramified factor and convergent norm powers.

def OAI.CubicFirstMoment.metaplecticRamifiedRatio line 11
lemma OAI.CubicFirstMoment.metaplectic_monomial_decay line 13
lemma OAI.CubicFirstMoment.metaplecticRamifiedRatio_bounds line 51

theorem OAI.CubicFirstMoment.metaplectic_coefficient_decay line 59

Source documentation

Decay of an actual nonzero Voronoi coefficient with its published support representation. The free and cubed factors now have convergent norm exponents.

theorem metaplectic_coefficient_decay
    {a : Eisenstein → MetaplecticDualArgument → ℂ} {C : ℝ} (hC : 0 ≤ C)
    {r : Eisenstein} (hr : primary r) (n : MetaplecticDualArgument)
    {j : ℤ} (hj : -1 ≤ j) (ζ : Eisensteinˣ) {h h' w : Eisenstein}
    (hh : primary h) (hh' : primary h') (hw : primary w) (hwr : IsCoprime w r)
    (he : metaplecticFrequency n = traceLambda^j*(ζ.val:ℂ)*(h:ℂ)*(w:ℂ)*(h':ℂ)^3)
    (ha : ‖a r n‖ ≤ C*3^((max j 0:ℤ)/3:ℝ)*Real.sqrt (norm h')) (σ : ℝ) :
    ‖a r n*metaplecticLocalCoefficient r n‖/
        (Complex.normSq (metaplecticFrequency n))^(1+σ) ≤
      C*(3:ℝ)^(1+σ)*metaplecticRamifiedRatio σ^((j+1).toNat)*
        norm h^(-σ)*norm w^(-1-σ)*norm h'^(-3/2-3*σ) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticFrequency, OAI.CubicFirstMoment.traceLambda, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticLocalCoefficient, OAI.CubicFirstMoment.metaplecticRamifiedRatio