α : Type ?u.258802
β : Type ?u.258805
γ : Type ?u.258808
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f r
α : Type ?u.258802
β : Type ?u.258805
γ : Type ?u.258808
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
⊢ HasSum f r ↔ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
refine' ⟨HasSum.tendsto_sum_nat, fun h => _⟩
α : Type ?u.258802
β : Type ?u.258805
γ : Type ?u.258808
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)

α : Type ?u.258802
β : Type ?u.258805
γ : Type ?u.258808
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n => ∑ i in Finset.range n, f i
α : Type ?u.258802
β : Type ?u.258805
γ : Type ?u.258808
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f r
rw [← iSup_eq_of_tendsto _ h, ← ENNReal.tsum_eq_iSup_nat]
no goals
α : Type ?u.258802
β : Type ?u.258805
γ : Type ?u.258808
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)
exact ENNReal.summable.hasSum
no goals
α : Type ?u.258802
β : Type ?u.258805
γ : Type ?u.258808
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n => ∑ i in Finset.range n, f i
exact fun s t hst => Finset.sum_le_sum_of_subset (Finset.range_subset.2 hst)