An integrated differential inequality (pure real analysis)

If E is continuous on [0,1], differentiable on (0,∞) with continuous derivative D, and D ≤ h almost everywhere on (0,1) for an integrable h, then E t - E 0 ≤ ∫₀ᵗ h for every t ∈ [0,1].

theorem AVenhance.Infra.Section5.Integration.Energy.sub_le_integral_of_deriv_le {E D h : ℝ → ℝ} {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) (ht : t ≤ 1) (hEd : ∀ (x : ℝ), 0 < x → HasDerivAt E (D x) x) (hDc : ContinuousOn D (Set.Ioi 0)) (hh : MeasureTheory.IntegrableOn h (Set.Ioo 0 1) MeasureTheory.volume) (hineq : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), D x ≤ h x) : E t - E s ≤ ∫ (x : ℝ) in s..t, h x

On a compact subinterval of (0,1] the fundamental theorem gives the integrated inequality.

theorem AVenhance.Infra.Section5.Integration.Energy.sub_le_integral_of_deriv_le_ae {E D h : ℝ → ℝ} (hEc : ContinuousOn E (Set.Icc 0 1)) (hEd : ∀ (x : ℝ), 0 < x → HasDerivAt E (D x) x) (hDc : ContinuousOn D (Set.Ioi 0)) (hh : MeasureTheory.IntegrableOn h (Set.Ioo 0 1) MeasureTheory.volume) (hineq : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), D x ≤ h x) (t : ℝ) : t ∈ Set.Icc 0 1 → E t - E 0 ≤ ∫ (x : ℝ) in 0..t, h x

The integrated differential inequality on [0,1].