English
Let f and f' satisfy suitable continuity and liminf-right-derivative bounds on [a,b], with f(a) ≤ δ and f' ≤ K f + ε. Then f(x) ≤ gronwallBound(δ,K,ε,(x−a)) for all x ∈ [a,b].
Русский
Пусть f и f' удовлетворяют условиям непрерывности и оценкам лиминф справа на интервале [a,b], при этом f(a) ≤ δ и f' ≤ K f + ε. Тогда для всех x ∈ [a,b] выполняется f(x) ≤ gronwallBound(δ,K,ε, x−a).
LaTeX
$$$\text{If } f\text{ is continuous on }[a,b],\; f(a)\le δ,\; f'\le Kf+ε\text{ and the liminf right derivative bound holds, then } f(x)\le \operatorname{gronwallBound}(δ,K,ε,(x-a)).$$$
Lean4
/-- A Grönwall-like inequality: if `f : ℝ → ℝ` is continuous on `[a, b]` and satisfies
the inequalities `f a ≤ δ` and
`∀ x ∈ [a, b), liminf_{z→x+0} (f z - f x)/(z - x) ≤ K * (f x) + ε`, then `f x`
is bounded by `gronwallBound δ K ε (x - a)` on `[a, b]`.
See also `norm_le_gronwallBound_of_norm_deriv_right_le` for a version bounding `‖f x‖`,
`f : ℝ → E`. -/
theorem le_gronwallBound_of_liminf_deriv_right_le {f f' : ℝ → ℝ} {δ K ε : ℝ} {a b : ℝ} (hf : ContinuousOn f (Icc a b))
(hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r → ∃ᶠ z in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r) (ha : f a ≤ δ)
(bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε) : ∀ x ∈ Icc a b, f x ≤ gronwallBound δ K ε (x - a) :=
by
have H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a) :=
by
intro x hx ε' hε'
apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'
· rwa [sub_self, gronwallBound_x0]
· exact fun x => hasDerivAt_gronwallBound_shift δ K ε' x a
· intro x hx hfB
rw [← hfB]
apply lt_of_le_of_lt (bound x hx)
exact add_lt_add_left (mem_Ioi.1 hε') _
· exact hx
intro x hx
change f x ≤ (fun ε' => gronwallBound δ K ε' (x - a)) ε
convert continuousWithinAt_const.closure_le _ _ (H x hx)
· simp only [closure_Ioi, left_mem_Ici]
exact (gronwallBound_continuous_ε δ K (x - a)).continuousWithinAt
