case intro
α : Type ?u.341642
β : Type ?u.341645
γ : Type ?u.341648
r : ℝ
f : ℕ → ℝ≥0
⊢ HasSum (fun i => ↑(f i)) r ↔ Tendsto (fun n => ∑ i in Finset.range n, (fun i => ↑(f i)) i) atTop (𝓝 r)
α : Type ?u.341642
β : Type ?u.341645
γ : Type ?u.341648
f : ℕ → ℝ
hf : ∀ (i : ℕ), 0 ≤ f i
r : ℝ
⊢ HasSum f r ↔ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
lift f to ℕ → ℝ≥0 using hf
case intro
α : Type ?u.341642
β : Type ?u.341645
γ : Type ?u.341648
r : ℝ
f : ℕ → ℝ≥0
⊢ (∃ hx, Tendsto (fun a => ∑ a in a, f a) atTop (𝓝 { val := r, property := hx })) ↔
    ∃ hx, Tendsto (fun a => ∑ a in Finset.range a, f a) atTop (𝓝 { val := r, property := hx })
case intro
α : Type ?u.341642
β : Type ?u.341645
γ : Type ?u.341648
r : ℝ
f : ℕ → ℝ≥0
⊢ HasSum (fun i => ↑(f i)) r ↔ Tendsto (fun n => ∑ i in Finset.range n, (fun i => ↑(f i)) i) atTop (𝓝 r)
simp only [HasSum, ← NNReal.coe_sum, NNReal.tendsto_coe']
no goals
case intro
α : Type ?u.341642
β : Type ?u.341645
γ : Type ?u.341648
r : ℝ
f : ℕ → ℝ≥0
⊢ (∃ hx, Tendsto (fun a => ∑ a in a, f a) atTop (𝓝 { val := r, property := hx })) ↔
    ∃ hx, Tendsto (fun a => ∑ a in Finset.range a, f a) atTop (𝓝 { val := r, property := hx })
exact exists_congr fun hr => NNReal.hasSum_iff_tendsto_nat