Theorems · Theorem · difference equations

discrete_gronwall

∀ {u b c : ℕ → ℝ} {n₀ : ℕ},
  0 ≤ u n₀ →
    (∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n) →
      (∀ n ≥ n₀, 0 ≤ c n) →
        (∀ n ≥ n₀, 0 ≤ b n) →
          ∀ ⦃n : ℕ⦄, 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).

Defined in

Mathlib.Analysis.ODE.DiscreteGronwall

Cited by

1 results in Mathlib

Foundations

Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound