Source indexedlemma · leanprover/lean4:v4.32.0

tendsto_mul_ceil_div

PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2346 to 2359

Source documentation

A version of the Wiener-Ikehara Tauberian Theorem: If f is a nonnegative arithmetic function whose L-series has a simple pole at s = 1 with residue A and otherwise extends continuously to the closed half-plane re s ≥ 1, then ∑ n < N, f n is asymptotic to A*N.

Exact Lean statement

lemma tendsto_mul_ceil_div :
    Tendsto (fun (p : ℝ × ℕ) => ⌈p.1 * p.2⌉₊ / (p.2 : ℝ)) (𝓝[>] 0 ×ˢ atTop) (𝓝 0)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tendsto_mul_ceil_div :    Tendsto (fun (p : ℝ × ℕ) => ⌈p.1 * p.2⌉₊ / (p.2 : ℝ)) (𝓝[>] 0 ×ˢ atTop) (𝓝 0) := by  rw [Metric.tendsto_nhds] ; intro δ hδ  have l1 : ∀ᶠ ε : ℝ in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2) := inter_mem_nhdsWithin _ (Iio_mem_nhds (by positivity))  have l2 : ∀ᶠ N : ℕ in atTop, 1 ≤ δ / 2 * N := by    apply Tendsto.eventually_ge_atTop    exact tendsto_natCast_atTop_atTop.const_mul_atTop (by positivity)  filter_upwards [l1.prod_mk l2] with (ε, N) ⟨⟨hε, h1⟩, h2⟩ ; dsimp only at *  have l3 : 0 < (N : ℝ) := by    simp only [Nat.cast_pos, Nat.pos_iff_ne_zero] ; rintro rfl ; simp [zero_lt_one.not_ge] at h2  have l5 : 0 ≤ ε * ↑N := by positivity  have l6 : ε * N ≤ δ / 2 * N := mul_le_mul h1.le le_rfl (by positivity) (by positivity)  simp only [dist_zero_right, norm_div, RCLike.norm_natCast, div_lt_iff₀ l3, gt_iff_lt]  convert (Nat.ceil_lt_add_one l5).trans_le (add_le_add l6 h2) using 1 ; ring