Grönwall estimate with an integrable coefficient

An absolutely continuous energy satisfying a differential inequality with a nonnegative integrable coefficient is bounded by the corresponding exponential factor (lem:lps-H1-estimate).

theorem ESS.LPS.lps_ac_gronwall {a b : ℝ} {f g : ℝ → ℝ} (hab : a ≤ b) (hf : AbsolutelyContinuousOnInterval f a b) (hg : MeasureTheory.IntegrableOn g (Set.Icc a b) MeasureTheory.volume) (hgpos : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), 0 ≤ g t) (hderiv : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), deriv f t ≤ g t * f t) (t : ℝ) : t ∈ Set.Icc a b → f t ≤ f a * Real.exp (∫ (s : ℝ) in a..t, g s)

The absolutely continuous form of Grönwall's inequality used to integrate the finite and endpoint differential estimates in lem:lps-H1-estimate.

theorem ESS.LPS.lps_ac_gronwall_dissipation {a b : ℝ} {f d g : ℝ → ℝ} (hab : a ≤ b) (hf : AbsolutelyContinuousOnInterval f a b) (hd : MeasureTheory.IntegrableOn d (Set.Icc a b) MeasureTheory.volume) (hdpos : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), 0 ≤ d t) (hg : MeasureTheory.IntegrableOn g (Set.Icc a b) MeasureTheory.volume) (hgpos : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), 0 ≤ g t) (hfpos : ∀ t ∈ Set.Icc a b, 0 ≤ f t) (hdiff : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), deriv f t + d t ≤ g t * f t) (t : ℝ) : t ∈ Set.Icc a b → f t + ∫ (s : ℝ) in a..t, d s ≤ f a * Real.exp (∫ (s : ℝ) in a..t, g s)

Grönwall with a nonnegative dissipation term carried on the left. If the derivative of the energy plus the dissipation is controlled by an integrable coefficient times the energy, the time integral of the dissipation obeys the same exponential bound (lem:lps-H1-estimate).

theorem ESS.LPS.lps_h1_finite_branch_gronwall {a b C : ℝ} {f d m : ℝ → ℝ} (hab : a ≤ b) (hf : AbsolutelyContinuousOnInterval f a b) (hd : MeasureTheory.IntegrableOn d (Set.Icc a b) MeasureTheory.volume) (hdpos : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), 0 ≤ d t) (hm : MeasureTheory.IntegrableOn m (Set.Icc a b) MeasureTheory.volume) (hmpos : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), 0 ≤ m t) (hC : 0 ≤ C) (hfpos : ∀ t ∈ Set.Icc a b, 0 ≤ f t) (hDiff : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), deriv f t + d t ≤ C * m t * f t) (t : ℝ) : t ∈ Set.Icc a b → f t + ∫ (s : ℝ) in a..t, d s ≤ f a * Real.exp (C * ∫ (s : ℝ) in a..t, m s)

The finite Serrin branch integrates the differential inequality with its critical L^s time coefficient (lem:lps-H1-estimate).

theorem ESS.LPS.lps_h1_endpoint_branch_gronwall {a b : ℝ} {f d m : ℝ → ℝ} (hab : a ≤ b) (hf : AbsolutelyContinuousOnInterval f a b) (hd : MeasureTheory.IntegrableOn d (Set.Icc a b) MeasureTheory.volume) (hdpos : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), 0 ≤ d t) (hm : MeasureTheory.IntegrableOn m (Set.Icc a b) MeasureTheory.volume) (hmpos : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), 0 ≤ m t) (hfpos : ∀ t ∈ Set.Icc a b, 0 ≤ f t) (hDiff : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), deriv f t + d t ≤ m t * f t) (t : ℝ) : t ∈ Set.Icc a b → f t + ∫ (s : ℝ) in a..t, d s ≤ f a * Real.exp (∫ (s : ℝ) in a..t, m s)

The endpoint Serrin branch integrates with the square of the spatial essential supremum (lem:lps-H1-estimate).