MetaplecticTailTruncation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed dyadic cutoff, larger than the natural dual length by a small power, makes the actual metaplectic tail arbitrarily small.

lemma OAI.CubicFirstMoment.exists_metaplectic_tail_order line 11
lemma OAI.CubicFirstMoment.metaplectic_tail_power_absorption line 27

theorem OAI.CubicFirstMoment.metaplectic_twisted_tail_arbitrary_power line 60

Source documentation

No tail estimate is assumed: the raw theta support, actual transform and polynomial scale bounds give every requested negative power.

theorem metaplectic_twisted_tail_arbitrary_power
    {a : Eisenstein → MetaplecticDualArgument → ℂ} (ha : MetaplecticCoefficientBounds a)
    (ℓ : ℤ) (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hpos : tsupport W ⊆ Set.Ioi 0) (hsm : ContDiff ℝ ∞ W)
    {σ δ : ℝ} (hσ : 0 < σ) (hδ : 0 < δ) (B H : ℝ) :
    ∃ (m : ℕ) (C : ℝ), 2 ≤ m ∧ σ ≤ (m:ℝ)-1/2 ∧ 0 ≤ C ∧
      ∀ r : Eisenstein, primary r → Squarefree r →
      ∀ Y X J T : ℝ, 1 ≤ Y → 0 < X → 0 < J → 1 ≤ T →
      norm r ≤ Y^B → T ≤ Y^B → norm r^2*T^4/X ≤ Y^B →
      (norm r^2*T^4/X)/J ≤ Y^(-δ) → ∀ t : ℝ, |t| ≤ 2*T →
      ‖∑' nd, metaplecticFarTailTerm a r ℓ (fun x => W x*mellinPhase t x)
          ((m:ℝ)-1/2) X J nd‖ ≤ C*Y^(-H) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.MetaplecticCoefficientBounds, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticFarTailTerm, OAI.CubicFirstMoment.mellinPhase