Infinite sums in extended nonnegative reals

This file proves results on infinite sums in ℝ≥0∞.

In particular, we give lemmas relating sums of constants to the cardinality of the domain of these sums.

TODO

• Once we have a topology on ENat, provide an ENat-valued version
• Provide versions which sum over the whole type.

theorem ENNReal.hasSum_coe {α : Type u_1} {f : α → NNReal} {r : NNReal} : HasSum (fun (a : α) => ↑(f a)) ↑r ↔ HasSum f r

theorem ENNReal.tsum_coe_eq {α : Type u_1} {r : NNReal} {f : α → NNReal} (h : HasSum f r) : ∑' (a : α), ↑(f a) = ↑r

theorem ENNReal.coe_tsum {α : Type u_1} {f : α → NNReal} : Summable f → ↑(tsum f) = ∑' (a : α), ↑(f a)

theorem ENNReal.hasSum {α : Type u_1} {f : α → ENNReal} : HasSum f (⨆ (s : Finset α), ∑ a ∈ s, f a)

@[simp]

theorem ENNReal.summable {α : Type u_1} {f : α → ENNReal} : Summable f

theorem ENNReal.tsum_coe_ne_top_iff_summable {β : Type u_2} {f : β → NNReal} : ∑' (b : β), ↑(f b) ≠ ⊤ ↔ Summable f

theorem ENNReal.tsum_eq_iSup_sum {α : Type u_1} {f : α → ENNReal} : ∑' (a : α), f a = ⨆ (s : Finset α), ∑ a ∈ s, f a

theorem ENNReal.tsum_eq_iSup_sum' {α : Type u_1} {f : α → ENNReal} {ι : Type u_4} (s : ι → Finset α) (hs : ∀ (t : Finset α), ∃ (i : ι), t ⊆ s i) : ∑' (a : α), f a = ⨆ (i : ι), ∑ a ∈ s i, f a

theorem ENNReal.tsum_sigma {α : Type u_1} {β : α → Type u_4} (f : (a : α) → β a → ENNReal) : ∑' (p : (a : α) × β a), f p.fst p.snd = ∑' (a : α) (b : β a), f a b

theorem ENNReal.tsum_sigma' {α : Type u_1} {β : α → Type u_4} (f : (a : α) × β a → ENNReal) : ∑' (p : (a : α) × β a), f p = ∑' (a : α) (b : β a), f ⟨a, b⟩

theorem ENNReal.tsum_biUnion' {α : Type u_1} {ι : Type u_4} {S : Set ι} {f : α → ENNReal} {t : ι → Set α} (h : S.PairwiseDisjoint t) : ∑' (x : ↑(⋃ i ∈ S, t i)), f ↑x = ∑' (i : ↑S) (x : ↑(t ↑i)), f ↑x

theorem ENNReal.tsum_biUnion {α : Type u_1} {ι : Type u_4} {f : α → ENNReal} {t : ι → Set α} (h : Set.univ.PairwiseDisjoint t) : ∑' (x : ↑(⋃ (i : ι), t i)), f ↑x = ∑' (i : ι) (x : ↑(t i)), f ↑x

theorem ENNReal.tsum_prod {α : Type u_1} {β : Type u_2} {f : α → β → ENNReal} : ∑' (p : α × β), f p.1 p.2 = ∑' (a : α) (b : β), f a b

theorem ENNReal.tsum_prod' {α : Type u_1} {β : Type u_2} {f : α × β → ENNReal} : ∑' (p : α × β), f p = ∑' (a : α) (b : β), f (a, b)

theorem ENNReal.tsum_comm {α : Type u_1} {β : Type u_2} {f : α → β → ENNReal} : ∑' (a : α) (b : β), f a b = ∑' (b : β) (a : α), f a b

theorem ENNReal.tsum_add {α : Type u_1} {f g : α → ENNReal} : ∑' (a : α), (f a + g a) = ∑' (a : α), f a + ∑' (a : α), g a

theorem ENNReal.sum_add_tsum_compl {ι : Type u_4} (s : Finset ι) (f : ι → ENNReal) : ∑ i ∈ s, f i + ∑' (i : ↑(↑s)ᶜ), f ↑i = ∑' (i : ι), f i

theorem ENNReal.tsum_le_tsum {α : Type u_1} {f g : α → ENNReal} (h : ∀ (a : α), f a ≤ g a) : ∑' (a : α), f a ≤ ∑' (a : α), g a

theorem ENNReal.sum_le_tsum {α : Type u_1} {f : α → ENNReal} (s : Finset α) : ∑ x ∈ s, f x ≤ ∑' (x : α), f x

theorem ENNReal.tsum_eq_iSup_nat' {f : ℕ → ENNReal} {N : ℕ → ℕ} (hN : Filter.Tendsto N Filter.atTop Filter.atTop) : ∑' (i : ℕ), f i = ⨆ (i : ℕ), ∑ a ∈ Finset.range (N i), f a

theorem ENNReal.tsum_eq_iSup_nat {f : ℕ → ENNReal} : ∑' (i : ℕ), f i = ⨆ (i : ℕ), ∑ a ∈ Finset.range i, f a

theorem ENNReal.tsum_eq_liminf_sum_nat {f : ℕ → ENNReal} : ∑' (i : ℕ), f i = Filter.liminf (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop

theorem ENNReal.tsum_eq_limsup_sum_nat {f : ℕ → ENNReal} : ∑' (i : ℕ), f i = Filter.limsup (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop

theorem ENNReal.le_tsum {α : Type u_1} {f : α → ENNReal} (a : α) : f a ≤ ∑' (a : α), f a

@[simp]

theorem ENNReal.tsum_eq_zero {α : Type u_1} {f : α → ENNReal} : ∑' (i : α), f i = 0 ↔ ∀ (i : α), f i = 0

theorem ENNReal.tsum_eq_top_of_eq_top {α : Type u_1} {f : α → ENNReal} : (∃ (a : α), f a = ⊤) → ∑' (a : α), f a = ⊤

theorem ENNReal.lt_top_of_tsum_ne_top {α : Type u_1} {a : α → ENNReal} (tsum_ne_top : ∑' (i : α), a i ≠ ⊤) (j : α) : a j < ⊤

@[simp]

theorem ENNReal.tsum_top {α : Type u_1} [Nonempty α] : ∑' (x : α), ⊤ = ⊤

theorem ENNReal.tsum_const_eq_top_of_ne_zero {α : Type u_4} [Infinite α] {c : ENNReal} (hc : c ≠ 0) : ∑' (x : α), c = ⊤

theorem ENNReal.ne_top_of_tsum_ne_top {α : Type u_1} {f : α → ENNReal} (h : ∑' (a : α), f a ≠ ⊤) (a : α) : f a ≠ ⊤

theorem ENNReal.tsum_mul_left {α : Type u_1} {a : ENNReal} {f : α → ENNReal} : ∑' (i : α), a * f i = a * ∑' (i : α), f i

theorem ENNReal.tsum_mul_right {α : Type u_1} {a : ENNReal} {f : α → ENNReal} : ∑' (i : α), f i * a = (∑' (i : α), f i) * a

theorem ENNReal.tsum_const_smul {α : Type u_1} {f : α → ENNReal} {R : Type u_4} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (a : R) : ∑' (i : α), a • f i = a • ∑' (i : α), f i

@[simp]

theorem ENNReal.tsum_iSup_eq {α : Type u_4} (a : α) {f : α → ENNReal} : ∑' (b : α), ⨆ (_ : a = b), f b = f a

theorem ENNReal.hasSum_iff_tendsto_nat {f : ℕ → ENNReal} (r : ENNReal) : HasSum f r ↔ Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds r)

theorem ENNReal.tendsto_nat_tsum (f : ℕ → ENNReal) : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds (∑' (n : ℕ), f n))

theorem ENNReal.toNNReal_apply_of_tsum_ne_top {α : Type u_4} {f : α → ENNReal} (hf : ∑' (i : α), f i ≠ ⊤) (x : α) : ↑((ENNReal.toNNReal ∘ f) x) = f x

theorem ENNReal.summable_toNNReal_of_tsum_ne_top {α : Type u_4} {f : α → ENNReal} (hf : ∑' (i : α), f i ≠ ⊤) : Summable (ENNReal.toNNReal ∘ f)

theorem ENNReal.tendsto_cofinite_zero_of_tsum_ne_top {α : Type u_4} {f : α → ENNReal} (hf : ∑' (x : α), f x ≠ ⊤) : Filter.Tendsto f Filter.cofinite (nhds 0)

theorem ENNReal.tendsto_atTop_zero_of_tsum_ne_top {f : ℕ → ENNReal} (hf : ∑' (x : ℕ), f x ≠ ⊤) : Filter.Tendsto f Filter.atTop (nhds 0)

theorem ENNReal.tendsto_tsum_compl_atTop_zero {α : Type u_4} {f : α → ENNReal} (hf : ∑' (x : α), f x ≠ ⊤) : Filter.Tendsto (fun (s : Finset α) => ∑' (b : { x : α // x ∉ s }), f ↑b) Filter.atTop (nhds 0)

The sum over the complement of a finset tends to 0 when the finset grows to cover the whole space. This does not need a summability assumption, as otherwise all sums are zero.

theorem ENNReal.tsum_apply {ι : Type u_4} {α : Type u_5} {f : ι → α → ENNReal} {x : α} : (∑' (i : ι), f i) x = ∑' (i : ι), f i x

theorem ENNReal.tsum_sub {f g : ℕ → ENNReal} (h₁ : ∑' (i : ℕ), g i ≠ ⊤) (h₂ : g ≤ f) : ∑' (i : ℕ), (f i - g i) = ∑' (i : ℕ), f i - ∑' (i : ℕ), g i

theorem ENNReal.tsum_comp_le_tsum_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (g : β → ENNReal) : ∑' (x : α), g (f x) ≤ ∑' (y : β), g y

theorem ENNReal.tsum_le_tsum_comp_of_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) (g : β → ENNReal) : ∑' (y : β), g y ≤ ∑' (x : α), g (f x)

theorem ENNReal.tsum_mono_subtype {α : Type u_1} (f : α → ENNReal) {s t : Set α} (h : s ⊆ t) : ∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑t), f ↑x

theorem ENNReal.tsum_iUnion_le_tsum {α : Type u_1} {ι : Type u_4} (f : α → ENNReal) (t : ι → Set α) : ∑' (x : ↑(⋃ (i : ι), t i)), f ↑x ≤ ∑' (i : ι) (x : ↑(t i)), f ↑x

theorem ENNReal.tsum_biUnion_le_tsum {α : Type u_1} {ι : Type u_4} (f : α → ENNReal) (s : Set ι) (t : ι → Set α) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑' (i : ↑s) (x : ↑(t ↑i)), f ↑x

theorem ENNReal.tsum_biUnion_le {α : Type u_1} {ι : Type u_4} (f : α → ENNReal) (s : Finset ι) (t : ι → Set α) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x

theorem ENNReal.tsum_iUnion_le {α : Type u_1} {ι : Type u_4} [Fintype ι] (f : α → ENNReal) (t : ι → Set α) : ∑' (x : ↑(⋃ (i : ι), t i)), f ↑x ≤ ∑ i : ι, ∑' (x : ↑(t i)), f ↑x

theorem ENNReal.tsum_union_le {α : Type u_1} (f : α → ENNReal) (s t : Set α) : ∑' (x : ↑(s ∪ t)), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x

theorem ENNReal.tsum_eq_add_tsum_ite {β : Type u_2} {f : β → ENNReal} (b : β) : ∑' (x : β), f x = f b + ∑' (x : β), if x = b then 0 else f x

theorem ENNReal.tsum_add_one_eq_top {f : ℕ → ENNReal} (hf : ∑' (n : ℕ), f n = ⊤) (hf0 : f 0 ≠ ⊤) : ∑' (n : ℕ), f (n + 1) = ⊤

theorem ENNReal.finite_const_le_of_tsum_ne_top {ι : Type u_4} {a : ι → ENNReal} (tsum_ne_top : ∑' (i : ι), a i ≠ ⊤) {ε : ENNReal} (ε_ne_zero : ε ≠ 0) : {i : ι | ε ≤ a i}.Finite

A sum of extended nonnegative reals which is finite can have only finitely many terms above any positive threshold.

theorem ENNReal.finset_card_const_le_le_of_tsum_le {ι : Type u_4} {a : ι → ENNReal} {c : ENNReal} (c_ne_top : c ≠ ⊤) (tsum_le_c : ∑' (i : ι), a i ≤ c) {ε : ENNReal} (ε_ne_zero : ε ≠ 0) : ∃ (hf : {i : ι | ε ≤ a i}.Finite), ↑hf.toFinset.card ≤ c / ε

Markov's inequality for Finset.card and tsum in ℝ≥0∞.

theorem ENNReal.tsum_fiberwise {β : Type u_2} {γ : Type u_3} (f : β → ENNReal) (g : β → γ) : ∑' (x : γ) (b : ↑(g ⁻¹' {x})), f ↑b = ∑' (i : β), f i

theorem ENNReal.tsum_coe_ne_top_iff_summable_coe {α : Type u_1} {f : α → NNReal} : ∑' (a : α), ↑(f a) ≠ ⊤ ↔ Summable fun (a : α) => ↑(f a)

theorem ENNReal.tsum_coe_eq_top_iff_not_summable_coe {α : Type u_1} {f : α → NNReal} : ∑' (a : α), ↑(f a) = ⊤ ↔ ¬Summable fun (a : α) => ↑(f a)

theorem ENNReal.hasSum_toReal {α : Type u_1} {f : α → ENNReal} (hsum : ∑' (x : α), f x ≠ ⊤) : HasSum (fun (x : α) => (f x).toReal) (∑' (x : α), (f x).toReal)

theorem ENNReal.summable_toReal {α : Type u_1} {f : α → ENNReal} (hsum : ∑' (x : α), f x ≠ ⊤) : Summable fun (x : α) => (f x).toReal

theorem NNReal.tsum_eq_toNNReal_tsum {β : Type u_2} {f : β → NNReal} : ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

theorem NNReal.exists_le_hasSum_of_le {β : Type u_2} {f g : β → NNReal} {r : NNReal} (hgf : ∀ (b : β), g b ≤ f b) (hfr : HasSum f r) : ∃ p ≤ r, HasSum g p

Comparison test of convergence of ℝ≥0-valued series.

theorem NNReal.summable_of_le {β : Type u_2} {f g : β → NNReal} (hgf : ∀ (b : β), g b ≤ f b) : Summable f → Summable g

Comparison test of convergence of ℝ≥0-valued series.

theorem Summable.countable_support_nnreal {α : Type u_1} (f : α → NNReal) (h : Summable f) : (Function.support f).Countable

Summable non-negative functions have countable support

theorem NNReal.hasSum_iff_tendsto_nat {f : ℕ → NNReal} {r : NNReal} : HasSum f r ↔ Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds r)

A series of non-negative real numbers converges to r in the sense of HasSum if and only if the sequence of partial sum converges to r.

theorem NNReal.not_summable_iff_tendsto_nat_atTop {f : ℕ → NNReal} : ¬Summable f ↔ Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop Filter.atTop

theorem NNReal.summable_iff_not_tendsto_nat_atTop {f : ℕ → NNReal} : Summable f ↔ ¬Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop Filter.atTop

theorem NNReal.summable_of_sum_range_le {f : ℕ → NNReal} {c : NNReal} (h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) : Summable f

theorem NNReal.tsum_le_of_sum_range_le {f : ℕ → NNReal} {c : NNReal} (h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) : ∑' (n : ℕ), f n ≤ c

theorem NNReal.tsum_comp_le_tsum_of_inj {α : Type u_1} {β : Type u_4} {f : α → NNReal} (hf : Summable f) {i : β → α} (hi : Function.Injective i) : ∑' (x : β), f (i x) ≤ ∑' (x : α), f x

theorem NNReal.summable_sigma {α : Type u_1} {β : α → Type u_4} {f : (x : α) × β x → NNReal} : Summable f ↔ (∀ (x : α), Summable fun (y : β x) => f ⟨x, y⟩) ∧ Summable fun (x : α) => ∑' (y : β x), f ⟨x, y⟩

theorem NNReal.indicator_summable {α : Type u_1} {f : α → NNReal} (hf : Summable f) (s : Set α) : Summable (s.indicator f)

theorem NNReal.tsum_indicator_ne_zero {α : Type u_1} {f : α → NNReal} (hf : Summable f) {s : Set α} (h : ∃ a ∈ s, f a ≠ 0) : ∑' (x : α), s.indicator f x ≠ 0

theorem NNReal.tendsto_sum_nat_add (f : ℕ → NNReal) : Filter.Tendsto (fun (i : ℕ) => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)

For f : ℕ → ℝ≥0, then ∑' k, f (k + i) tends to zero. This does not require a summability assumption on f, as otherwise all sums are zero.

theorem NNReal.hasSum_lt {α : Type u_1} {f g : α → NNReal} {sf sg : NNReal} {i : α} (h : ∀ (a : α), f a ≤ g a) (hi : f i < g i) (hf : HasSum f sf) (hg : HasSum g sg) : sf < sg

theorem NNReal.hasSum_strict_mono {α : Type u_1} {f g : α → NNReal} {sf sg : NNReal} (hf : HasSum f sf) (hg : HasSum g sg) (h : f < g) : sf < sg

theorem NNReal.tsum_lt_tsum {α : Type u_1} {f g : α → NNReal} {i : α} (h : ∀ (a : α), f a ≤ g a) (hi : f i < g i) (hg : Summable g) : ∑' (n : α), f n < ∑' (n : α), g n

theorem NNReal.tsum_strict_mono {α : Type u_1} {f g : α → NNReal} (hg : Summable g) (h : f < g) : ∑' (n : α), f n < ∑' (n : α), g n

theorem NNReal.tsum_pos {α : Type u_1} {g : α → NNReal} (hg : Summable g) (i : α) (hi : 0 < g i) : 0 < ∑' (b : α), g b

theorem NNReal.tsum_eq_add_tsum_ite {α : Type u_1} {f : α → NNReal} (hf : Summable f) (i : α) : ∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x

theorem ENNReal.tsum_toNNReal_eq {α : Type u_1} {f : α → ENNReal} (hf : ∀ (a : α), f a ≠ ⊤) : (∑' (a : α), f a).toNNReal = ∑' (a : α), (f a).toNNReal

theorem ENNReal.tsum_toReal_eq {α : Type u_1} {f : α → ENNReal} (hf : ∀ (a : α), f a ≠ ⊤) : (∑' (a : α), f a).toReal = ∑' (a : α), (f a).toReal

theorem ENNReal.tendsto_sum_nat_add (f : ℕ → ENNReal) (hf : ∑' (i : ℕ), f i ≠ ⊤) : Filter.Tendsto (fun (i : ℕ) => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)

theorem ENNReal.tsum_le_of_sum_range_le {f : ℕ → ENNReal} {c : ENNReal} (h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) : ∑' (n : ℕ), f n ≤ c

theorem ENNReal.hasSum_lt {α : Type u_1} {f g : α → ENNReal} {sf sg : ENNReal} {i : α} (h : ∀ (a : α), f a ≤ g a) (hi : f i < g i) (hsf : sf ≠ ⊤) (hf : HasSum f sf) (hg : HasSum g sg) : sf < sg

theorem ENNReal.tsum_lt_tsum {α : Type u_1} {f g : α → ENNReal} {i : α} (hfi : tsum f ≠ ⊤) (h : ∀ (a : α), f a ≤ g a) (hi : f i < g i) : ∑' (x : α), f x < ∑' (x : α), g x

theorem tsum_comp_le_tsum_of_inj {α : Type u_1} {β : Type u_4} {f : α → ℝ} (hf : Summable f) (hn : ∀ (a : α), 0 ≤ f a) {i : β → α} (hi : Function.Injective i) : tsum (f ∘ i) ≤ tsum f

theorem Summable.of_nonneg_of_le {β : Type u_2} {f g : β → ℝ} (hg : ∀ (b : β), 0 ≤ g b) (hgf : ∀ (b : β), g b ≤ f b) (hf : Summable f) : Summable g

Comparison test of convergence of series of non-negative real numbers.

theorem Summable.toNNReal {α : Type u_1} {f : α → ℝ} (hf : Summable f) : Summable fun (n : α) => (f n).toNNReal

theorem Summable.tsum_ofReal_lt_top {α : Type u_1} {f : α → ℝ} (hf : Summable f) : ∑' (i : α), ENNReal.ofReal (f i) < ⊤

theorem Summable.tsum_ofReal_ne_top {α : Type u_1} {f : α → ℝ} (hf : Summable f) : ∑' (i : α), ENNReal.ofReal (f i) ≠ ⊤

theorem Summable.countable_support_ennreal {α : Type u_1} {f : α → ENNReal} (h : ∑' (i : α), f i ≠ ⊤) : (Function.support f).Countable

Finitely summable non-negative functions have countable support

theorem hasSum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} (hf : ∀ (i : ℕ), 0 ≤ f i) (r : ℝ) : HasSum f r ↔ Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds r)

A series of non-negative real numbers converges to r in the sense of HasSum if and only if the sequence of partial sum converges to r.

theorem ENNReal.ofReal_tsum_of_nonneg {α : Type u_1} {f : α → ℝ} (hf_nonneg : ∀ (n : α), 0 ≤ f n) (hf : Summable f) : ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)

theorem ENNReal.multipliable_of_le_one {α : Type u_1} {f : α → ENNReal} (h₀ : ∀ (i : α), f i ≤ 1) : Multipliable f

theorem ENNReal.hasProd_iInf_prod {α : Type u_1} {f : α → ENNReal} (h₀ : ∀ (i : α), f i ≤ 1) : HasProd f (⨅ (s : Finset α), ∏ i ∈ s, f i)

theorem ENNReal.tprod_eq_iInf_prod {α : Type u_1} {f : α → ENNReal} (h₀ : ∀ (i : α), f i ≤ 1) : ∏' (i : α), f i = ⨅ (s : Finset α), ∏ i ∈ s, f i

theorem cauchySeq_of_edist_le_of_summable {α : Type u_1} [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → NNReal) (hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)) (hd : Summable d) : CauchySeq f

If the extended distance between consecutive points of a sequence is estimated by a summable series of NNReals, then the original sequence is a Cauchy sequence.

theorem cauchySeq_of_edist_le_of_tsum_ne_top {α : Type u_1} [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal) (hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) (hd : tsum d ≠ ⊤) : CauchySeq f

theorem edist_le_tsum_of_edist_le_of_tendsto {α : Type u_1} [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal) (hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds a)) (n : ℕ) : edist (f n) a ≤ ∑' (m : ℕ), d (n + m)

If edist (f n) (f (n+1)) is bounded above by a function d : ℕ → ℝ≥0∞, then the distance from f n to the limit is bounded by ∑'_{k=n}^∞ d k.

theorem edist_le_tsum_of_edist_le_of_tendsto₀ {α : Type u_1} [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal) (hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds a)) : edist (f 0) a ≤ ∑' (m : ℕ), d m

If edist (f n) (f (n+1)) is bounded above by a function d : ℕ → ℝ≥0∞, then the distance from f 0 to the limit is bounded by ∑'_{k=0}^∞ d k.

theorem ENNReal.tsum_set_one {α : Type u_4} (s : Set α) : ∑' (x : ↑s), 1 = ↑s.encard

theorem ENNReal.tsum_set_const {α : Type u_4} (s : Set α) (c : ENNReal) : ∑' (x : ↑s), c = ↑s.encard * c

@[simp]

theorem ENNReal.tsum_one {α : Type u_4} : ∑' (x : α), 1 = ↑(ENat.card α)

@[simp]

theorem ENNReal.tsum_const {α : Type u_4} (c : ENNReal) : ∑' (x : α), c = ↑(ENat.card α) * c