case intro
α : Type ?u.333832
β : Type ?u.333835
γ : Type ?u.333838
f : ℕ → ℝ≥0
hf : (∑' (i : ℕ), (fun i => ↑(f i)) i) ≠ ⊤
⊢ Tendsto (fun i => ∑' (k : ℕ), (fun i => ↑(f i)) (k + i)) atTop (𝓝 0)
α : Type ?u.333832
β : Type ?u.333835
γ : Type ?u.333838
f : ℕ → ℝ≥0∞
hf : (∑' (i : ℕ), f i) ≠ ⊤
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
lift f to ℕ → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf
case intro
α : Type ?u.333832
β : Type ?u.333835
γ : Type ?u.333838
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i => ∑' (k : ℕ), (fun i => ↑(f i)) (k + i)) atTop (𝓝 0)
case intro
α : Type ?u.333832
β : Type ?u.333835
γ : Type ?u.333838
f : ℕ → ℝ≥0
hf : (∑' (i : ℕ), (fun i => ↑(f i)) i) ≠ ⊤
⊢ Tendsto (fun i => ∑' (k : ℕ), (fun i => ↑(f i)) (k + i)) atTop (𝓝 0)
replace hf : Summable f := tsum_coe_ne_top_iff_summable.1 hf
case intro
α : Type ?u.333832
β : Type ?u.333835
γ : Type ?u.333838
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i => ↑(∑' (a : ℕ), f (a + i))) atTop (𝓝 ↑0)
case intro
α : Type ?u.333832
β : Type ?u.333835
γ : Type ?u.333838
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i => ∑' (k : ℕ), (fun i => ↑(f i)) (k + i)) atTop (𝓝 0)
simp only [← ENNReal.coe_tsum, NNReal.summable_nat_add _ hf, ← ENNReal.coe_zero]
no goals
case intro
α : Type ?u.333832
β : Type ?u.333835
γ : Type ?u.333838
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i => ↑(∑' (a : ℕ), f (a + i))) atTop (𝓝 ↑0)
exact_mod_cast NNReal.tendsto_sum_nat_add f