Uniform bound from a differential energy inequality with an integrable coefficient

prop:lps-smoothing: the real-variable step of the time-difference estimate. An energy E ≥ 0 with E' ≤ -D + κ E (in integral form), whose mean over an initial layer of length δ is at most Θ and whose coefficient has integral at most Λ, is bounded by (Θ/δ) e^Λ after the layer.

theorem ESS.LPS.lps_exists_le_average {a δ Θ : ℝ} (hδ : 0 < δ) {E : ℝ → ℝ} (hE : ContinuousOn E (Set.Icc a (a + δ))) (hΘ : ∫ (τ : ℝ) in a..a + δ, E τ ≤ Θ) : ∃ s ∈ Set.Icc a (a + δ), E s ≤ Θ / δ

A continuous nonnegative function with integral at most Θ over [a,a+δ] takes a value at most Θ/δ there.

theorem ESS.LPS.lps_energy_uniform_bound {a T' δ Θ Λ : ℝ} (hδ : 0 < δ) (haδ : a + δ ≤ T') {E g Dd κ : ℝ → ℝ} (hE : ContinuousOn E (Set.Icc a T')) (hE0 : ∀ r ∈ Set.Icc a T', 0 ≤ E r) (hg : IntervalIntegrable g MeasureTheory.volume a T') (hDd : IntervalIntegrable Dd MeasureTheory.volume a T') (hκ : IntervalIntegrable κ MeasureTheory.volume a T') (hDd0 : ∀ r ∈ Set.Icc a T', 0 ≤ Dd r) (hκ0 : ∀ r ∈ Set.Icc a T', 0 ≤ κ r) (hid : ∀ s ∈ Set.Icc a T', ∀ t ∈ Set.Icc a T', s ≤ t → E t - E s = ∫ (τ : ℝ) in s..t, g τ) (hineq : ∀ᵐ (τ : ℝ), τ ∈ Set.Icc a T' → g τ ≤ -Dd τ + κ τ * E τ) (hΘ : ∫ (τ : ℝ) in a..a + δ, E τ ≤ Θ) (hΛ : ∫ (τ : ℝ) in a..T', κ τ ≤ Λ) : ∃ s ∈ Set.Icc a (a + δ), E s ≤ Θ / δ ∧ (∀ t ∈ Set.Icc (a + δ) T', E t ≤ Θ / δ * Real.exp Λ) ∧ ∀ t ∈ Set.Icc (a + δ) T', ∫ (τ : ℝ) in a + δ..t, Dd τ ≤ Θ / δ * (1 + Λ * Real.exp Λ)

Uniform bound from an energy inequality with an integrable coefficient.