DualTailTruncation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative truncation at a small power beyond the natural Hecke length. The cutoff is a numerical inequality, not a duality assumption.

lemma OAI.CubicFirstMoment.exists_dual_tail_order line 13
lemma OAI.CubicFirstMoment.dual_tail_scale_bound line 23

theorem OAI.CubicFirstMoment.hecke_dual_tail_arbitrary_power line 50

Source documentation

The omitted far-left tail is smaller than every fixed negative power once the cutoff exceeds the natural length by Y^δ. Only polynomial upper bounds for the two lengths are used.

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

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