Comparison Gronwall #
A nonnegative relative energy that is bounded in time and satisfies an
integral inequality with an integrable nonnegative coefficient vanishes almost
everywhere (lem:lps-comparison).
theorem
ESS.lps_comparison_grow_zero
{T C : ℝ}
{m E : ℝ → ℝ}
(hT : 0 < T)
(hC : 0 ≤ C)
(hm : MeasureTheory.IntegrableOn m (Set.Ioo 0 T) MeasureTheory.volume)
(hmNonneg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), 0 ≤ m t)
(hENonneg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), 0 ≤ E t)
(hmE : MeasureTheory.IntegrableOn (fun (t : ℝ) => m t * E t) (Set.Ioo 0 T) MeasureTheory.volume)
(hmENonneg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), 0 ≤ m t * E t)
(hineq : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), E t ≤ C * ∫ (s : ℝ) in 0..t, m s * E s)
:
A nonnegative relative energy that is bounded in time and satisfies an
integral inequality with an integrable nonnegative coefficient vanishes almost
everywhere (lem:lps-comparison).