α : Type ?u.319791
β : Type ?u.319794
γ : Type ?u.319797
f : ℕ → ℝ≥0
⊢ Tendsto (fun a => ↑(∑' (k : ℕ), f (k + a))) atTop (𝓝 ↑0)
α : Type ?u.319791
β : Type ?u.319794
γ : Type ?u.319797
f : ℕ → ℝ≥0
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
rw [← tendsto_coe]
case h.e'_3.h
α : Type ?u.319791
β : Type ?u.319794
γ : Type ?u.319797
f : ℕ → ℝ≥0
x✝ : ℕ
⊢ ↑(∑' (k : ℕ), f (k + x✝)) = ∑' (k : ℕ), ↑(f (k + x✝))
α : Type ?u.319791
β : Type ?u.319794
γ : Type ?u.319797
f : ℕ → ℝ≥0
⊢ Tendsto (fun a => ↑(∑' (k : ℕ), f (k + a))) atTop (𝓝 ↑0)
convert _root_.tendsto_sum_nat_add fun i => (f i : ℝ)
no goals
case h.e'_3.h
α : Type ?u.319791
β : Type ?u.319794
γ : Type ?u.319797
f : ℕ → ℝ≥0
x✝ : ℕ
⊢ ↑(∑' (k : ℕ), f (k + x✝)) = ∑' (k : ℕ), ↑(f (k + x✝))
norm_cast