gronwallBound_ε0 — Mathlib

English

When ε = 0, gronwallBound reduces to gronwallBound(δ,K,0,x) = δ e^{Kx}.

Русский

При ε = 0 граница Гронвалла принимает вид δ e^{Kx}.

LaTeX

$$$\operatorname{gronwallBound}(\delta,K,0,x)=\delta e^{Kx}$$$

Lean4

theorem gronwallBound_ε0 (δ K x : ℝ) : gronwallBound δ K 0 x = δ * exp (K * x) :=
  by
  by_cases hK : K = 0
  · simp only [gronwallBound_K0, hK, zero_mul, exp_zero, add_zero, mul_one]
  · simp only [gronwallBound_of_K_ne_0 hK, zero_div, zero_mul, add_zero]

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