Mathlib.Topology.Algebra.InfiniteSum.Real

cauchySeq_of_dist_le_of_summable theorem

(d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : Summable d) : CauchySeq f

Full source

/-- If the distance between consecutive points of a sequence is estimated by a summable series,
then the original sequence is a Cauchy sequence. -/
theorem cauchySeq_of_dist_le_of_summable (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n)
    (hd : Summable d) : CauchySeq f := by
  lift d to ℕ → ℝ≥0 using fun n ↦ dist_nonneg.trans (hf n)
  apply cauchySeq_of_edist_le_of_summable d (α := α) (f := f)
  · exact_mod_cast hf
  · exact_mod_cast hd

Cauchy Criterion via Summable Distance Bounds in Pseudometric Spaces

Informal description

Let $\{f(n)\}_{n \in \mathbb{N}}$ be a sequence in a pseudometric space $\alpha$, and let $\{d(n)\}_{n \in \mathbb{N}}$ be a sequence of real numbers. If for every $n \in \mathbb{N}$, the distance between consecutive terms satisfies $\text{dist}(f(n), f(n+1)) \leq d(n)$, and if the series $\sum_{n=0}^\infty d(n)$ is summable, then the sequence $\{f(n)\}$ is a Cauchy sequence.

cauchySeq_of_summable_dist theorem

(h : Summable fun n ↦ dist (f n) (f n.succ)) : CauchySeq f

Full source

theorem cauchySeq_of_summable_dist (h : Summable fun n ↦ dist (f n) (f n.succ)) : CauchySeq f :=
  cauchySeq_of_dist_le_of_summable _ (fun _ ↦ le_rfl) h

Cauchy Criterion via Summable Distances

Informal description

Let $\{f(n)\}_{n \in \mathbb{N}}$ be a sequence in a pseudometric space. If the series $\sum_{n=0}^\infty \text{dist}(f(n), f(n+1))$ is summable, then $\{f(n)\}$ is a Cauchy sequence.

dist_le_tsum_of_dist_le_of_tendsto theorem

 (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : Summable d) {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
  dist (f n) a ≤ ∑' m, d (n + m)

Full source

theorem dist_le_tsum_of_dist_le_of_tendsto (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n)
    (hd : Summable d) {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    dist (f n) a ≤ ∑' m, d (n + m) := by
  refine le_of_tendsto (tendsto_const_nhds.dist ha) (eventually_atTop.2 ⟨n, fun m hnm ↦ ?_⟩)
  refine le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ ↦ hf _) ?_
  rw [sum_Ico_eq_sum_range]
  refine Summable.sum_le_tsum (range _) (fun _ _ ↦ le_trans dist_nonneg (hf _)) ?_
  exact hd.comp_injective (add_right_injective n)

Distance Bound via Tail Sum for Convergent Sequences in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $f \colon \mathbb{N} \to \alpha$ be a sequence in $\alpha$. Suppose there exists a sequence of nonnegative real numbers $d \colon \mathbb{N} \to \mathbb{R}$ such that: 1. For every $n \in \mathbb{N}$, the distance between consecutive terms satisfies $\text{dist}(f(n), f(n+1)) \leq d(n)$. 2. The series $\sum_{n=0}^\infty d(n)$ is summable. 3. The sequence $f$ converges to a point $a \in \alpha$. Then, for any $n \in \mathbb{N}$, the distance from $f(n)$ to the limit point $a$ is bounded by the tail sum of the series $d$, i.e., \[ \text{dist}(f(n), a) \leq \sum_{m=n}^\infty d(m). \]

dist_le_tsum_of_dist_le_of_tendsto₀ theorem

 (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : Summable d) (ha : Tendsto f atTop (𝓝 a)) :
  dist (f 0) a ≤ tsum d

Full source

theorem dist_le_tsum_of_dist_le_of_tendsto₀ (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n)
    (hd : Summable d) (ha : Tendsto f atTop (𝓝 a)) : dist (f 0) a ≤ tsum d := by
  simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0

Distance Bound via Total Sum for Convergent Sequences in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $f \colon \mathbb{N} \to \alpha$ be a sequence in $\alpha$. Suppose there exists a sequence of nonnegative real numbers $d \colon \mathbb{N} \to \mathbb{R}$ such that: 1. For every $n \in \mathbb{N}$, the distance between consecutive terms satisfies $\text{dist}(f(n), f(n+1)) \leq d(n)$. 2. The series $\sum_{n=0}^\infty d(n)$ is summable. 3. The sequence $f$ converges to a point $a \in \alpha$. Then, the distance from the initial term $f(0)$ to the limit point $a$ is bounded by the sum of the series $d$, i.e., \[ \text{dist}(f(0), a) \leq \sum_{n=0}^\infty d(n). \]

dist_le_tsum_dist_of_tendsto theorem

 (h : Summable fun n ↦ dist (f n) (f n.succ)) (ha : Tendsto f atTop (𝓝 a)) (n) :
  dist (f n) a ≤ ∑' m, dist (f (n + m)) (f (n + m).succ)

Full source

theorem dist_le_tsum_dist_of_tendsto (h : Summable fun n ↦ dist (f n) (f n.succ))
    (ha : Tendsto f atTop (𝓝 a)) (n) : dist (f n) a ≤ ∑' m, dist (f (n + m)) (f (n + m).succ) :=
  show dist (f n) a ≤ ∑' m, (fun x ↦ dist (f x) (f x.succ)) (n + m) from
    dist_le_tsum_of_dist_le_of_tendsto (fun n ↦ dist (f n) (f n.succ)) (fun _ ↦ le_rfl) h ha n

Distance Bound via Tail Sum of Consecutive Distances for Convergent Sequences

Informal description

Let $\alpha$ be a pseudometric space and $f \colon \mathbb{N} \to \alpha$ be a sequence in $\alpha$. Suppose the series $\sum_{n=0}^\infty \text{dist}(f(n), f(n+1))$ is summable and the sequence $f$ converges to a point $a \in \alpha$. Then for any $n \in \mathbb{N}$, the distance from $f(n)$ to the limit point $a$ is bounded by the tail sum of the distances between consecutive terms, i.e., \[ \text{dist}(f(n), a) \leq \sum_{m=n}^\infty \text{dist}(f(m), f(m+1)). \]

dist_le_tsum_dist_of_tendsto₀ theorem

 (h : Summable fun n ↦ dist (f n) (f n.succ)) (ha : Tendsto f atTop (𝓝 a)) : dist (f 0) a ≤ ∑' n, dist (f n) (f n.succ)

Full source

theorem dist_le_tsum_dist_of_tendsto₀ (h : Summable fun n ↦ dist (f n) (f n.succ))
    (ha : Tendsto f atTop (𝓝 a)) : dist (f 0) a ≤ ∑' n, dist (f n) (f n.succ) := by
  simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0

Initial Distance Bound via Sum of Consecutive Distances for Convergent Sequences

Informal description

Let $\alpha$ be a pseudometric space and $f \colon \mathbb{N} \to \alpha$ be a sequence in $\alpha$. Suppose the series $\sum_{n=0}^\infty \text{dist}(f(n), f(n+1))$ is summable and the sequence $f$ converges to a point $a \in \alpha$. Then the distance from the initial term $f(0)$ to the limit point $a$ is bounded by the sum of the distances between consecutive terms, i.e., \[ \text{dist}(f(0), a) \leq \sum_{n=0}^\infty \text{dist}(f(n), f(n+1)). \]

not_summable_iff_tendsto_nat_atTop_of_nonneg theorem

 {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) : ¬Summable f ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop

Full source

theorem not_summable_iff_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) :
    ¬Summable f¬Summable f ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop := by
  lift f to ℕ → ℝ≥0 using hf
  simpa using mod_cast NNReal.not_summable_iff_tendsto_nat_atTop

Non-summability Criterion via Divergence of Partial Sums for Non-Negative Real Sequences

Informal description

For a sequence $(f_n)_{n \in \mathbb{N}}$ of non-negative real numbers, the sequence is not summable if and only if the sequence of partial sums $\sum_{i=0}^{n-1} f_i$ tends to infinity as $n \to \infty$.

summable_iff_not_tendsto_nat_atTop_of_nonneg theorem

 {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) : Summable f ↔ ¬Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop

Full source

theorem summable_iff_not_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) :
    SummableSummable f ↔ ¬Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop := by
  rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]

Summability Criterion via Bounded Partial Sums for Non-Negative Sequences

Informal description

For a sequence $(f_n)_{n \in \mathbb{N}}$ of non-negative real numbers, the sequence is summable if and only if the sequence of partial sums $\sum_{i=0}^{n-1} f_i$ does not tend to infinity as $n \to \infty$.

summable_sigma_of_nonneg theorem

 {α} {β : α → Type*} {f : (Σ x, β x) → ℝ} (hf : ∀ x, 0 ≤ f x) :
  Summable f ↔ (∀ x, Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' y, f ⟨x, y⟩

Full source

theorem summable_sigma_of_nonneg {α} {β : α → Type*} {f : (Σ x, β x) → ℝ} (hf : ∀ x, 0 ≤ f x) :
    SummableSummable f ↔ (∀ x, Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' y, f ⟨x, y⟩ := by
  lift f to (Σx, β x) → ℝ≥0 using hf
  simpa using mod_cast NNReal.summable_sigma

Summability Criterion for Non-Negative Functions on Dependent Sum Types

Informal description

For a non-negative function $f \colon \Sigma x, \beta x \to \mathbb{R}$, the function $f$ is summable if and only if for every $x$, the function $y \mapsto f(x, y)$ is summable, and the function $x \mapsto \sum_{y} f(x, y)$ is summable.

summable_partition theorem

 {α β : Type*} {f : β → ℝ} (hf : 0 ≤ f) {s : α → Set β} (hs : ∀ i, ∃! j, i ∈ s j) :
  Summable f ↔ (∀ j, Summable fun i : s j ↦ f i) ∧ Summable fun j ↦ ∑' i : s j, f i

Full source

lemma summable_partition {α β : Type*} {f : β → ℝ} (hf : 0 ≤ f) {s : α  → Set β}
    (hs : ∀ i, ∃! j, i ∈ s j) : SummableSummable f ↔
      (∀ j, Summable fun i : s j ↦ f i) ∧ Summable fun j ↦ ∑' i : s j, f i := by
  simpa only [← (Set.sigmaEquiv s hs).summable_iff] using summable_sigma_of_nonneg (fun _ ↦ hf _)

Summability Criterion for Non-Negative Functions on a Partitioned Domain

Informal description

Let $f \colon \beta \to \mathbb{R}$ be a non-negative function, and let $\{s_j\}_{j \in \alpha}$ be a partition of $\beta$ (i.e., for every $i \in \beta$, there exists a unique $j \in \alpha$ such that $i \in s_j$). Then $f$ is summable if and only if for every $j \in \alpha$, the restriction $f|_{s_j}$ is summable, and the function $j \mapsto \sum_{i \in s_j} f(i)$ is summable.

summable_prod_of_nonneg theorem

 {α β} {f : (α × β) → ℝ} (hf : 0 ≤ f) : Summable f ↔ (∀ x, Summable fun y ↦ f (x, y)) ∧ Summable fun x ↦ ∑' y, f (x, y)

Full source

theorem summable_prod_of_nonneg {α β} {f : (α × β) → ℝ} (hf : 0 ≤ f) :
    SummableSummable f ↔ (∀ x, Summable fun y ↦ f (x, y)) ∧ Summable fun x ↦ ∑' y, f (x, y) :=
  (Equiv.sigmaEquivProd _ _).summable_iff.symm.trans <| summable_sigma_of_nonneg fun _ ↦ hf _

Summability Criterion for Non-Negative Functions on Product Types

Informal description

For a non-negative function $f \colon \alpha \times \beta \to \mathbb{R}$, the function $f$ is summable if and only if for every $x \in \alpha$, the function $y \mapsto f(x, y)$ is summable, and the function $x \mapsto \sum_{y \in \beta} f(x, y)$ is summable.

summable_of_sum_le theorem

{ι : Type*} {f : ι → ℝ} {c : ℝ} (hf : 0 ≤ f) (h : ∀ u : Finset ι, ∑ x ∈ u, f x ≤ c) : Summable f

Full source

theorem summable_of_sum_le {ι : Type*} {f : ι → ℝ} {c : ℝ} (hf : 0 ≤ f)
    (h : ∀ u : Finset ι, ∑ x ∈ u, f x ≤ c) : Summable f :=
  ⟨⨆ u : Finset ι, ∑ x ∈ u, f x,
    tendsto_atTop_ciSup (Finset.sum_mono_set_of_nonneg hf) ⟨c, fun _ ⟨u, hu⟩ => hu ▸ h u⟩⟩

Summability Criterion for Non-Negative Functions with Bounded Partial Sums

Informal description

Let $f \colon \iota \to \mathbb{R}$ be a non-negative function and $c \in \mathbb{R}$ a constant. If for every finite subset $u \subseteq \iota$, the sum $\sum_{x \in u} f(x) \leq c$, then $f$ is summable.

summable_of_sum_range_le theorem

{f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n) (h : ∀ n, ∑ i ∈ Finset.range n, f i ≤ c) : Summable f

Full source

theorem summable_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n)
    (h : ∀ n, ∑ i ∈ Finset.range n, f i ≤ c) : Summable f := by
  refine (summable_iff_not_tendsto_nat_atTop_of_nonneg hf).2 fun H => ?_
  rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩
  exact lt_irrefl _ (hn.trans_le (h n))

Summability Criterion via Bounded Partial Sums for Non-Negative Sequences

Informal description

For a sequence $(f_n)_{n \in \mathbb{N}}$ of non-negative real numbers, if there exists a real number $c$ such that for all $n \in \mathbb{N}$, the partial sum $\sum_{i=0}^{n-1} f_i \leq c$, then the sequence $f$ is summable.

Real.tsum_le_of_sum_range_le theorem

 {f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n) (h : ∀ n, ∑ i ∈ Finset.range n, f i ≤ c) : ∑' n, f n ≤ c

Full source

theorem Real.tsum_le_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n)
    (h : ∀ n, ∑ i ∈ Finset.range n, f i ≤ c) : ∑' n, f n ≤ c :=
  (summable_of_sum_range_le hf h).tsum_le_of_sum_range_le h

Bounded Partial Sums Imply Bounded Infinite Sum for Non-Negative Sequences

Informal description

For a sequence $(f_n)_{n \in \mathbb{N}}$ of non-negative real numbers, if there exists a real number $c$ such that for all $n \in \mathbb{N}$, the partial sum $\sum_{i=0}^{n-1} f_i \leq c$, then the infinite sum $\sum_{n=0}^\infty f_n \leq c$.

Summable.tsum_lt_tsum_of_nonneg theorem

 {i : ℕ} {f g : ℕ → ℝ} (h0 : ∀ b : ℕ, 0 ≤ f b) (h : ∀ b : ℕ, f b ≤ g b) (hi : f i < g i) (hg : Summable g) :
  ∑' n, f n < ∑' n, g n

Full source

/-- If a sequence `f` with non-negative terms is dominated by a sequence `g` with summable
series and at least one term of `f` is strictly smaller than the corresponding term in `g`,
then the series of `f` is strictly smaller than the series of `g`. -/
protected theorem Summable.tsum_lt_tsum_of_nonneg {i : ℕ} {f g : ℕ → ℝ} (h0 : ∀ b : ℕ, 0 ≤ f b)
    (h : ∀ b : ℕ, f b ≤ g b) (hi : f i < g i) (hg : Summable g) : ∑' n, f n < ∑' n, g n :=
  Summable.tsum_lt_tsum h hi (.of_nonneg_of_le h0 h hg) hg

Strict Comparison Test for Non-Negative Series

Informal description

Let $(f_n)$ and $(g_n)$ be sequences of non-negative real numbers such that $f_n \leq g_n$ for all $n \in \mathbb{N}$. If there exists an index $i$ such that $f_i < g_i$ and the series $\sum_{n=0}^\infty g_n$ is summable, then $\sum_{n=0}^\infty f_n < \sum_{n=0}^\infty g_n$.