Integral Grönwall inequality with an integrable coefficient #
A continuous function bounded by a constant plus the integral of an
integrable nonnegative coefficient times itself is bounded by the
corresponding exponential factor. A variant carries a nonnegative
dissipation term on the left-hand side. Both are used to close the
high-order energy estimates of the smoothing argument (prop:lps-smoothing).
theorem
ESS.LPS.lps_integral_gronwall
{s t : ℝ}
(hst : s ≤ t)
{Φ c : ℝ → ℝ}
{A : ℝ}
(hΦ : ContinuousOn Φ (Set.Icc s t))
(hc : IntervalIntegrable c MeasureTheory.volume s t)
(hc0 : ∀ r ∈ Set.Icc s t, 0 ≤ c r)
(h : ∀ r ∈ Set.Icc s t, Φ r ≤ A + ∫ (τ : ℝ) in s..r, c τ * Φ τ)
(r : ℝ)
:
Integral form of Grönwall's inequality with an integrable nonnegative
coefficient: if Φ r ≤ A + ∫_s^r c Φ for every r ∈ [s, t], then
Φ r ≤ A exp (∫_s^r c) on [s, t] (prop:lps-smoothing).
theorem
ESS.LPS.lps_integral_gronwall_dissipation
{s t : ℝ}
(hst : s ≤ t)
{Φ c D : ℝ → ℝ}
{A : ℝ}
(hΦ : ContinuousOn Φ (Set.Icc s t))
(hc : IntervalIntegrable c MeasureTheory.volume s t)
(hc0 : ∀ r ∈ Set.Icc s t, 0 ≤ c r)
(hΦ0 : ∀ r ∈ Set.Icc s t, 0 ≤ Φ r)
(hD0 : ∀ r ∈ Set.Icc s t, 0 ≤ D r)
(h : ∀ r ∈ Set.Icc s t, Φ r + D r ≤ A + ∫ (τ : ℝ) in s..r, c τ * Φ τ)
:
Integral Grönwall inequality with a nonnegative dissipation term on the
left: if Φ r + D r ≤ A + ∫_s^r c Φ on [s, t] with Φ, D ≥ 0, then
D t ≤ A (1 + (∫_s^t c) exp (∫_s^t c)) (prop:lps-smoothing).