Variable-coefficient Grönwall estimate

The scalar comparison argument below allows an integrable, time-dependent coefficient. This is the form needed when the linear operator is merely measurable: replacing its integral by a uniform bound would lose information.

theorem AVenhance.Infra.ODE.Gronwall.integral_gronwall_endpoint {a b C : ℝ} (hab : a ≤ b) {c z : ℝ → ℝ} (hc : IntervalIntegrable c MeasureTheory.volume a b) (hcz : IntervalIntegrable (fun (t : ℝ) => c t * z t) MeasureTheory.volume a b) (hc_nonneg : ∀ t ∈ Set.Icc a b, 0 ≤ c t) (hineq : ∀ t ∈ Set.Icc a b, z t ≤ C + ∫ (s : ℝ) in a..t, c s * z s) : z b ≤ C * Real.exp (∫ (t : ℝ) in a..b, c t)

theorem AVenhance.Infra.ODE.integral_gronwall_bound {a b C : ℝ} (hab : a ≤ b) {c z : ℝ → ℝ} (hc : IntervalIntegrable c MeasureTheory.volume a b) (hcz : IntervalIntegrable (fun (t : ℝ) => c t * z t) MeasureTheory.volume a b) (hc_nonneg : ∀ t ∈ Set.Icc a b, 0 ≤ c t) (hineq : ∀ t ∈ Set.Icc a b, z t ≤ C + ∫ (s : ℝ) in a..t, c s * z s) (t : ℝ) : t ∈ Set.Icc a b → z t ≤ C * Real.exp (∫ (s : ℝ) in a..t, c s)

Integral Grönwall inequality with a nonnegative integrable time-dependent coefficient. The additive constant may already include an integral of an inhomogeneous forcing term.

theorem AVenhance.Infra.ODE.LinearODEData.IsSolution.norm_le_gronwall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) (hu : D.IsSolution u) (t : ℝ) : t ∈ Set.Icc a b → ‖extendCurve hab u t‖ ≤ (‖D.y₀‖ + ∫ (s : ℝ) in a..b, ‖D.f s‖) * Real.exp (∫ (s : ℝ) in a..t, ‖D.A s‖)

The norm of the unique integral solution is controlled by the L¹ norms of the forcing and operator coefficient.