Integral Gronwall inequality with a time dependent coefficient

An integral inequality with an integrable nonnegative coefficient forces a nonnegative function to vanish when its initial contribution is zero.

theorem ESS.serrin_integral_gronwall_zero {T C : ℝ} {b q : ℝ → ℝ} (hT : 0 ≤ T) (hC : 0 ≤ C) (hb : MeasureTheory.IntegrableOn b (Set.Icc 0 T) MeasureTheory.volume) (hbNonneg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 T), 0 ≤ b t) (hqNonneg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 T), 0 ≤ q t) (hprod : MeasureTheory.Integrable (fun (t : ℝ) => b t * q t) (MeasureTheory.volume.restrict (Set.Icc 0 T))) (hprodNonneg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 T), 0 ≤ b t * q t) (hineq : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 T), q t ≤ C * ∫ (s : ℝ) in 0..t, b s * q s) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 T), q t = 0

Integral Gronwall with an integrable, time dependent coefficient.