Integral Grönwall inequality with variable coefficient #
If φ is continuous on [a, b], k is continuous and nonnegative on [a, b],
and φ has right derivative φ' on [a, b) satisfying φ' ≤ k·φ,
then φ t ≤ φ a * exp(∫_a^t k s ds) for all t ∈ [a, b].
The proof defines Φ(t) = φ(t) * exp(-∫_a^t k s ds) and shows Φ is continuous on [a, b]
and has right derivative ≤ 0 on [a, b). The fencing lemma
image_le_of_deriv_right_le_deriv_boundary then yields Φ t ≤ Φ a = φ a, and the
inequality follows by multiplying by exp(∫_a^t k s ds).
theorem
CIV.le_mul_exp_integral_of_deriv_le
{φ k : ℝ → ℝ}
{a b : ℝ}
(hab : a ≤ b)
(hcont : ContinuousOn φ (Set.Icc a b))
(hk : ContinuousOn k (Set.Icc a b))
(hk0 : ∀ t ∈ Set.Icc a b, 0 ≤ k t)
(hderiv : ∀ t ∈ Set.Ico a b, HasDerivWithinAt φ (deriv φ t) (Set.Ici t) t)
(hineq : ∀ t ∈ Set.Ico a b, deriv φ t ≤ k t * φ t)
(t : ℝ)
: