Summing the errors of a sequence of increments

If the increments G (k + 1) - G k of a sequence G are each within D of a prescribed value g k for k < n, then G n - G 0 is within n • D of the sum ∑ k < n, g k. The increments telescope, and the errors add up by the triangle inequality.

Likewise, if a subadditive function q is small on each step F (r + 1) - F r of a sequence, relative to weights w r whose partial sums are at most 1, then it is small on the total displacement F (N + 1) - F 0. This is how per-stage perturbation estimates, with weights such as 2⁻⁽ʳ⁺¹⁾, are combined into an estimate for the limit of the stages.

Main results

• TauCeti.abs_sub_sub_sum_range_le_of_forall_lt: the bound on G n - G 0 - ∑ k < n, g k from the bounds on the increments.
• TauCeti.lt_of_forall_sub_lt_mul: the telescoping bound for a subadditive function and weights with partial sums at most 1.

theorem TauCeti.abs_sub_sub_sum_range_le_of_forall_lt {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {G g : ℕ → α} {D : α} {n : ℕ} (hstep : ∀ k < n, |G (k + 1) - G k - g k| ≤ D) : |G n - G 0 - ∑ k ∈ Finset.range n, g k| ≤ n • D

If the increments G (k + 1) - G k of a sequence are within D of g k for k < n, then G n - G 0 is within n • D of ∑ k ∈ range n, g k.

theorem TauCeti.lt_of_forall_sub_lt_mul {G : Type u_1} [AddCommGroup G] (q : G → ℝ) (hq0 : q 0 ≤ 0) (hadd : ∀ (a b : G), q (a + b) ≤ q a + q b) {t : ℝ} (ht : 0 < t) {w : ℕ → ℝ} (hw : ∀ (N : ℕ), ∑ r ∈ Finset.range N, w r ≤ 1) (F : ℕ → G) (N : ℕ) (h : ∀ r ≤ N, q (F (r + 1) - F r) < t * w r) : q (F (N + 1) - F 0) < t

A telescoping bound. If a subadditive function q is small on each step F (r + 1) - F r of a sequence, relative to weights w r summing to at most 1, then it is small on the total displacement F (N + 1) - F 0.