Discrete Grönwall inequality

Various forms of the discrete Grönwall inequality, bounding solutions to recurrence inequalities u (n+1) ≤ c n * u n + b n and u (n+1) ≤ (1 + c n) * u n + b n.

Main results

• discrete_gronwall_prod_general: product form, over any ordered commutative semiring.
• discrete_gronwall: classical exponential bound for the (1 + c) form, over ℝ.
• discrete_gronwall_Ico: uniform bound over an interval, over ℝ.

References

• T. H. Grönwall, Note on the derivatives with respect to a parameter of the solutions of a system of differential equations

See also

• Mathlib.Analysis.ODE.Gronwall for the continuous Grönwall inequality for ODEs.

Generalized product form

theorem discrete_gronwall_prod_general {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {u b c : ℕ → R} {n₀ : ℕ} (hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n) (hc : ∀ n ≥ n₀, 0 ≤ c n) ⦃n : ℕ⦄ (hn : n₀ ≤ n) : u n ≤ u n₀ * ∏ i ∈ Finset.Ico n₀ n, c i + ∑ k ∈ Finset.Ico n₀ n, b k * ∏ i ∈ Finset.Ico (k + 1) n, c i

Discrete Grönwall inequality, product form: if u (n+1) ≤ c n * u n + b n and 0 ≤ c n then u n ≤ u n₀ * ∏ c i + ∑ b k * ∏ c i over the appropriate ranges.

Real-valued exponential form

theorem discrete_gronwall {u b c : ℕ → ℝ} {n₀ : ℕ} (hun₀ : 0 ≤ u n₀) (hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n) (hc : ∀ n ≥ n₀, 0 ≤ c n) (hb : ∀ n ≥ n₀, 0 ≤ b n) ⦃n : ℕ⦄ (hn : n₀ ≤ n) : u n ≤ (u n₀ + ∑ k ∈ Finset.Ico n₀ n, b k) * Real.exp (∑ i ∈ Finset.Ico n₀ n, c i)

Discrete Grönwall inequality, exponential form: if u (n+1) ≤ (1 + c n) * u n + b n with b, c, and u n₀ non-negative, then u n ≤ (u n₀ + ∑ b k) * exp (∑ c i).

theorem discrete_gronwall_Ico {u b c : ℕ → ℝ} {n₀ n₁ : ℕ} (hun₀ : 0 ≤ u n₀) (hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n) (hc : ∀ n ≥ n₀, 0 ≤ c n) (hb : ∀ n ≥ n₀, 0 ≤ b n) ⦃n : ℕ⦄ (hn : n ∈ Finset.Ico n₀ n₁) : u n ≤ (u n₀ + ∑ k ∈ Finset.Ico n₀ n₁, b k) * Real.exp (∑ i ∈ Finset.Ico n₀ n₁, c i)

Discrete Grönwall inequality, uniform bound: a single bound holding for all n ∈ [n₀, n₁).