RelativeError item 11: the scalar dissipation lower bound #
If e(t) + 2κ ∫_0^t D = N on [0,1] and D ≥ 4π² e (Poincaré) with D ≥ 0 continuous, then
κ ∫_0^1 D ≥ min (1/4) (2π²κ) N.
theorem
AVenhance.Infra.Section5.RelativeError.dissipation_lower_scalar
{κ N : ℝ}
{e D : ℝ → ℝ}
(hκ : 0 < κ)
(hN : 0 ≤ N)
(hD0 : ∀ s ∈ Set.Icc 0 1, 0 ≤ D s)
(hDc : ContinuousOn D (Set.Icc 0 1))
(hid : ∀ t ∈ Set.Icc 0 1, e t + 2 * κ * ∫ (s : ℝ) in 0..t, D s = N)
(hP : ∀ s ∈ Set.Icc 0 1, 4 * Real.pi ^ 2 * e s ≤ D s)
: