MetaplecticTailScale.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The natural metaplectic dual cutoff and its exact exponent algebra.

lemma OAI.CubicFirstMoment.metaplectic_tail_scale_identity line 10
lemma OAI.CubicFirstMoment.metaplectic_height_nat_power line 40

theorem OAI.CubicFirstMoment.metaplectic_twisted_tail_natural_cutoff line 48

Source documentation

The cutoff is independent of t throughout the full dyadic height range. Constants retain the harmless fixed factor 3^(4m).

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

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