Source indexedlemma · leanprover/lean4:v4.32.0

wiener_ikehara_smooth_real

PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2032 to 2046

Mathematical statement

Exact Lean statement

lemma wiener_ikehara_smooth_real {f : ℕ → ℝ} {Ψ : ℝ → ℝ}
    (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))
    (hcheby : cheby f) (hG : ContinuousOn G {s | 1 ≤ s.re})
    (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})
    (hsmooth : ContDiff ℝ ∞ Ψ) (hsupp : HasCompactSupport Ψ)
    (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) :
    Tendsto (fun x : ℝ ↦ (∑' n, f n * Ψ (n / x)) / x) atTop (nhds (A * ∫ y in Set.Ioi 0, Ψ y))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma wiener_ikehara_smooth_real {f : ℕ → ℝ} {Ψ : ℝ → ℝ}    (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))    (hcheby : cheby f) (hG : ContinuousOn G {s | 1 ≤ s.re})    (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})    (hsmooth : ContDiff ℝ ∞ Ψ) (hsupp : HasCompactSupport Ψ)    (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) :    Tendsto (fun x : ℝ ↦ (∑' n, f n * Ψ (n / x)) / x) atTop (nhds (A * ∫ y in Set.Ioi 0, Ψ y)) := by   let Ψ' := ofReal ∘ Ψ  have l1 : ContDiff ℝ ∞ Ψ' := contDiff_ofReal.comp hsmooth  have l2 : HasCompactSupport Ψ' := hsupp.comp_left rfl  have l3 : closure (Function.support Ψ') ⊆ Ioi 0 := by rwa [Function.support_comp_eq] ; simp  have key := (continuous_re.tendsto _).comp    (@wiener_ikehara_smooth' A Ψ G f hf hcheby hG hG' l1 l2 l3)  simp at key ; norm_cast at key