HeckeSmoothApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual smooth Hecke sums are approximated by their retained dual integrals, with an error smaller than any prescribed power.

def OAI.CubicFirstMoment.retainedHeckeIntegral line 14

theorem OAI.CubicFirstMoment.hecke_smooth_approximation line 23

Source documentation

Uniform arbitrary-power approximation beyond the natural dual length. The original sum and retained integral are explicitly defined.

theorem hecke_smooth_approximation
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {δ : ℝ} (hδ : 0 < δ) (B R : ℝ) :
    ∃ (m : ℕ) (C : ℝ), 2 ≤ m ∧ 0 ≤ C ∧
      ∀ (χ χdual : EisensteinIdealExponent → ℂ),
      (∀ ν, ‖χ ν‖ ≤ 1) → (∀ ν, ‖χdual ν‖ ≤ 1) →
      ∀ (ε : ℂ), ‖ε‖ ≤ 1 → ∀ (Y A Z J t : ℝ),
      1 ≤ Y → 0 < A → 1 ≤ Z → 0 < J → Z ≤ Y^B → J ≤ Y^B →
      (A^2*(1+|t|)^2)/(Z*J) ≤ Y^(-δ) →
      ∀ (L Ldual : ℂ → ℂ), PrimitiveHeckeAnalyticData χ χdual A ε L Ldual →
      GammaQuotientStripBound (1/2-(m:ℝ)) →
      ‖(∑' ν, χ ν*mellinPhase t (idealExponentNorm ν)*W (idealExponentNorm ν/Z)) -
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.PrimitiveHeckeAnalyticData, OAI.CubicFirstMoment.GammaQuotientStripBound, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.idealExponentNorm

theorem OAI.CubicFirstMoment.hecke_smooth_approximation_of_completed line 55

Source documentation

Smooth dual approximation from the completed functional equation and reciprocal-Gamma bounds.

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

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