cauchy_series_of_le_geometric'' — Mathlib

English

If tail bounds hold after some index N, i.e., ∀ n ≥ N, ∥u(n)∥ ≤ C r^n with hr0 > 0 and hr1 < 1, then the tail partial sums form a Cauchy sequence when the head is truncated: define v(n) = 0 for n < N and v(n) = u(n) for n ≥ N; then the partial sums of v are Cauchy.

Русский

Если после некоторого индекса N выполняются хвостовые ограничения ∥u(n)∥ ≤ C r^n с hr0 > 0 и hr1 < 1, то частичные суммы хвоста образуют последовательность Коши, если прерывать голову: v(n)=0 для n<N, v(n)=u(n) для n≥N; частичные суммы v — Коши.

LaTeX

$$$\forall {\alpha} [\text{SeminormedAddCommGroup } \alpha] (C \in \mathbb{R}) (N \in \mathbb{N}) (u : \mathbb{N} \to \alpha) (r \in \mathbb{R}) (hr0 : 0 < r) (hr1 : r < 1) (h : \forall n \ge N, \|u(n)\| ≤ C r^n) \\ → \\ CauchySeq (\lambda n, \sum_{k=0}^{n} v(k)) \,\text{ where } v(n)=\begin{cases}0,& n

Lean4

theorem cauchy_series_of_le_geometric'' {C : ℝ} {u : ℕ → α} {N : ℕ} {r : ℝ} (hr₀ : 0 < r) (hr₁ : r < 1)
    (h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n) : CauchySeq fun n ↦ ∑ k ∈ range (n + 1), u k :=
  by
  set v : ℕ → α := fun n ↦ if n < N then 0 else u n
  have hC : 0 ≤ C := (mul_nonneg_iff_of_pos_right <| pow_pos hr₀ N).mp ((norm_nonneg _).trans <| h N <| le_refl N)
  have : ∀ n ≥ N, u n = v n := by
    intro n hn
    simp [v, if_neg (not_lt.mpr hn)]
  apply cauchySeq_sum_of_eventually_eq this (NormedAddCommGroup.cauchy_series_of_le_geometric' hr₁ _)
  · exact C
  intro n
  simp only [v]
  split_ifs with H
  · rw [norm_zero]
    exact mul_nonneg hC (pow_nonneg hr₀.le _)
  · push_neg at H
    exact h _ H

Похожие утверждения