English
Define the Grönwall bound Gr(δ,K,ε,x) by Gr(δ,K,ε,x) = δ if K = 0, and Gr(δ,K,ε,x) = δ e^{Kx} + (ε/K)(e^{Kx} − 1) if K ≠ 0. This bound provides an upper envelope for solutions of differential inequalities with linear growth in the derivative.
Русский
Заданная функция границии Гронвалля Gr(δ,K,ε,x) задаёт верхнюю огибающую для решений дифференциальных неравенств с линейным ростом производной.
LaTeX
$$$\operatorname{gronwallBound}(\delta,K,\varepsilon,x)=\begin{cases} \delta+\varepsilon x, & K=0, \\ \delta e^{Kx}+\frac{\varepsilon}{K}(e^{Kx}-1), & K\neq 0. \end{cases}$$$
Lean4
/-- Upper bound used in several Grönwall-like inequalities. -/
noncomputable def gronwallBound (δ K ε x : ℝ) : ℝ :=
if K = 0 then δ + ε * x else δ * exp (K * x) + ε / K * (exp (K * x) - 1)
