Integral Grönwall Bound

This statement is an integral Grönwall inequality.

Let φ:ℝ→ℝ and a,K,T∈ℝ. Assume K≥0, φ is measurable, φ is bounded on $[0,T]$, and for every t∈[0,T],

Then for every t∈[0,T],

This provides a real-analysis form of Grönwall's inequality for a measurable bounded function and an arbitrary real initial coefficient a.

Formalization Note The integral is over Set.Ioc 0 t; the theorem does not assume T≥0 separately, although the interval hypotheses govern its scope.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem le_mul_exp_of_le_add_integral {φ : ℝ → ℝ} {a K T : ℝ} (hK : 0 ≤ K)
    (hφm : Measurable φ) (hφb : ∃ B, ∀ t ∈ Set.Icc (0 : ℝ) T, |φ t| ≤ B)
    (h : ∀ t ∈ Set.Icc (0 : ℝ) T, φ t ≤ a + K * ∫ s in Set.Ioc (0 : ℝ) t, φ s) :
    ∀ t ∈ Set.Icc (0 : ℝ) T, φ t ≤ a * Real.exp (K * t)

Module navigation

Module: Analysis/Gronwall.

Source excerpt, lines 19–22 · Frozen source 408915f.