A variable-coefficient Gronwall estimate from a genuine one-sided time derivative. The integrating factor uses the actual time integral.
theorem
EulerOrdinarySobolev.variable_linear_stability
(T : ℝ)
(hT : 0 ≤ T)
(X X' : ℝ → ℝ)
(C : ℝ)
(K : C(↑(Set.Icc 0 T), ℝ))
(hcont : ContinuousOn X (Set.Icc 0 T))
(hder : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt X (X' t) (Set.Icc 0 T) t)
(hineq : ∀ t ∈ Set.Ico 0 T, X' t ≤ C * EulerVolterraConvolution.extendPath T hT K t * X t)
(t : ↑(Set.Icc 0 T))
: