MellinDualTail.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Actual far-left dual-series tails. The integer-line Gamma estimate and smooth Mellin decay provide the analytic bounds.

lemma OAI.CubicFirstMoment.shifted_power_le line 15
lemma OAI.CubicFirstMoment.mellin_polynomial_majorant line 23
lemma OAI.CubicFirstMoment.ideal_norm_tail_le line 44
def OAI.CubicFirstMoment.idealDirichletTail line 71
Source documentation
The tail is the tail of the full ideal series, with all Euler factors.
```
def idealDirichletTail (χ : EisensteinIdealExponent → ℂ) (J : ℝ) (s : ℂ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.norm_idealDirichletTail_le line 75
def OAI.CubicFirstMoment.heckeDualTailIntegrand line 101
Source documentation
The integrand of the omitted part of the functional-equation series on the line Re s = 1/2-m.
```
def heckeDualTailIntegrand (W : ℝ → ℂ) (χ : EisensteinIdealExponent → ℂ)
    (ε : ℂ) (A Z J : ℝ) (m : ℕ) (t τ : ℝ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.norm_heckeDualTailIntegrand_le line 108
lemma OAI.CubicFirstMoment.dual_tail_scale_identity line 158

theorem OAI.CubicFirstMoment.hecke_dual_tail_integral_bound line 168

Source documentation

An arbitrary-order tail bound with the natural dual length displayed. The constant depends only on the fixed weight and the chosen order m.

theorem hecke_dual_tail_integral_bound (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hpos : tsupport W ⊆ Ioi 0) (hsm : ContDiff ℝ ∞ W)
    {m : ℕ} (hm : 2 ≤ m) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (χ : EisensteinIdealExponent → ℂ),
      (∀ ν, ‖χ ν‖ ≤ 1) → ∀ (ε : ℂ), ‖ε‖ ≤ 1 →
      ∀ (A Z J : ℝ), 0 < A → 0 < Z → 0 < J → ∀ t : ℝ,
      ‖∫ τ : ℝ, heckeDualTailIntegrand W χ ε A Z J m t τ‖ ≤
        C*Z^(1/2:ℝ)*J^(3/2:ℝ)*((A^2*(1+|t|)^2)/(Z*J))^m := by
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.heckeDualTailIntegrand