gronwallBound_of_K_ne_0 — Mathlib

English

If K ≠ 0, then gronwallBound(δ,K,ε,x) = δ e^{Kx} + (ε/K)(e^{Kx} − 1).

Русский

Если K ≠ 0, то gronwallBound(δ,K,ε,x) = δ e^{Kx} + (ε/K)(e^{Kx} − 1).

LaTeX

$$$\operatorname{gronwallBound}(\delta,K,\varepsilon,x)=\delta e^{Kx}+\frac{\varepsilon}{K}(e^{Kx}-1),\quad K\neq 0$$$

Lean4

theorem gronwallBound_of_K_ne_0 {δ K ε : ℝ} (hK : K ≠ 0) :
    gronwallBound δ K ε = fun x => δ * exp (K * x) + ε / K * (exp (K * x) - 1) :=
  funext fun _ => if_neg hK

Похожие утверждения