Theorems · Theorem · difference equations

discrete_gronwall_prod_general

∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {u b c : ℕ → R} {n₀ : ℕ},
  (∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n) →
    (∀ n ≥ n₀, 0 ≤ c n) →
      ∀ ⦃n : ℕ⦄,
        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.

Defined in

Mathlib.Analysis.ODE.DiscreteGronwall

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringPartialOrderIsOrderedRing