Theorems · Theorem · difference equations

discrete_gronwall_Ico

∀ {u b c : ℕ → ℝ} {n₀ 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 ∈ 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₁).

Defined in

Mathlib.Analysis.ODE.DiscreteGronwall

Cited by

0 results in Mathlib

Foundations

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