MetaplecticDualTailWeights.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact exponent bookkeeping for truncating the metaplectic dual series. The cutoff is in the actual norm N(d³ν).

def OAI.CubicFirstMoment.metaplecticDualNorm line 11
lemma OAI.CubicFirstMoment.metaplecticDualNorm_pos line 14
lemma OAI.CubicFirstMoment.metaplectic_dual_weight_split line 19
lemma OAI.CubicFirstMoment.metaplectic_dual_weight_tail line 50
def OAI.CubicFirstMoment.metaplecticFarTailTerm line 63

theorem OAI.CubicFirstMoment.metaplecticFarTail_norm_bound line 70

Source documentation

The tail costs the cutoff power while retaining only the already summable small-line coefficient mass.

theorem metaplecticFarTail_norm_bound
    (a : Eisenstein → MetaplecticDualArgument → ℂ) {r : Eisenstein} (hr : primary r)
    (ℓ : ℤ) (W : ℝ → ℂ) {σ A X J C M : ℝ}
    (hσ : 0 < σ) (hA : σ ≤ A) (hX : 0 < X) (hJ : 0 < J) (hC : 0 ≤ C)
    (hW : ∀ v : ℝ, 0 < v → ‖metaplecticTransform ℓ W A v‖ ≤ C*v^(-A))
    (hm : Summable (metaplecticCoefficientMassTerm a r σ))
    (hM : (∑' n, metaplecticCoefficientMassTerm a r σ n) ≤ M) :
    ‖∑' nd, metaplecticFarTailTerm a r ℓ W A X J nd‖ ≤
      (C*((2*Real.pi)^(-4*A)*X^(-A)*norm r^(2*A)))*J^(-(A-σ))*M*
        (∑' d : PrimaryArgument, norm d^(-5/2-3*σ)) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticTransform, OAI.CubicFirstMoment.metaplecticCoefficientMassTerm, OAI.CubicFirstMoment.metaplecticFarTailTerm, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.PrimaryArgument