SmoothHeckeMoment.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A character average of actual full smooth sums is bounded by the normalized dual dyad averages plus the proved negligible tail.

lemma OAI.CubicFirstMoment.norm_sq_le_twice_approx line 13

theorem OAI.CubicFirstMoment.full_smooth_hecke_moment line 26

Source documentation

The full smooth-sum moment, from the precisely specified completed Hecke inputs and actual bounds for the normalized dual polynomials.

theorem full_smooth_hecke_moment
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {δ : ℝ} (hδ : 0 < δ) (H R : ℝ) :
    ∃ C D : ℝ, 0 ≤ C ∧ 0 ≤ D ∧
      ∀ {ι : Type*} [Fintype ι], ∀ (χ χdual : ι → EisensteinIdealExponent → ℂ) (ε : ι → ℂ) (A : ι → ℝ),
      (∀ i ν, ‖χ i ν‖ ≤ 1) → (∀ i ν, ‖χdual i ν‖ ≤ 1) →
      (∀ i, ‖ε i‖ = 1) → (∀ i, 0 < A i) → ∀ (Y Z J t : ℝ),
      1 ≤ Y → 1 ≤ Z → 0 < J → Z ≤ Y^H → J ≤ Y^H →
      (∀ i, ((A i)^2*(1+|t|)^2)/(Z*J) ≤ Y^(-δ)) →
      ∀ (L Ldual : ι → ℂ → ℂ),
      (∀ i, Differentiable ℂ (L i)) →
      (∀ i s, 1 < s.re → L i s = normDirichletSeries (χ i) idealExponentNorm s) →
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.normDirichletSeries, OAI.CubicFirstMoment.idealExponentNorm