gronwallBound_x0 — Mathlib

English

The Grönwall bound evaluated at zero is the initial value: gronwallBound(δ,K,ε,0) = δ.

Русский

Значение граничающей функции Гронвалла при x=0 равно начальному значению: gronwallBound(δ,K,ε,0) = δ.

LaTeX

$$$\operatorname{gronwallBound}(\delta,K,\varepsilon,0)=\delta$$$

Lean4

theorem gronwallBound_x0 (δ K ε : ℝ) : gronwallBound δ K ε 0 = δ :=
  by
  by_cases hK : K = 0
  · simp only [gronwallBound, if_pos hK, mul_zero, add_zero]
  · simp only [gronwallBound, if_neg hK, mul_zero, exp_zero, sub_self, mul_one, add_zero]

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