Uniform limits from summable successive increments, with reusable tail estimates.

noncomputable def KamProject.Arnold1963.Convergence.sequenceLimit {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (f : ℕ → α → E) (x : α) : E

The initial value plus the infinite sum of successive increments of a sequence.

Equations

• KamProject.Arnold1963.Convergence.sequenceLimit f x = f 0 x + ∑' (s : ℕ), (f (s + 1) x - f s x)

theorem KamProject.Arnold1963.Convergence.sequenceLimit_tendstoUniformlyOn {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] {f : ℕ → α → E} {U : Set α} {u : ℕ → ℝ} (hu : Summable u) (hf : ∀ (s : ℕ), ∀ x ∈ U, ‖f (s + 1) x - f s x‖ ≤ u s) : TendstoUniformlyOn f (sequenceLimit f) Filter.atTop U

theorem KamProject.Arnold1963.Convergence.sequenceLimit_sub_eq_tsum {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] {f : ℕ → α → E} {x : α} {u : ℕ → ℝ} (hu : Summable u) (hf : ∀ (s : ℕ), ‖f (s + 1) x - f s x‖ ≤ u s) (s : ℕ) : sequenceLimit f x - f s x = ∑' (j : ℕ), (f (j + s + 1) x - f (j + s) x)

theorem KamProject.Arnold1963.Convergence.sequenceLimit_tail_le {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] {f : ℕ → α → E} {x : α} {u : ℕ → ℝ} (hu : Summable u) (hf : ∀ (s : ℕ), ‖f (s + 1) x - f s x‖ ≤ u s) (s : ℕ) : ‖sequenceLimit f x - f s x‖ ≤ ∑' (j : ℕ), u (j + s)