gronwallBound_K0

Mathlib.Analysis.ODE.Gronwall

URI: https://scilib.ai/kg/mathlib#gronwallBound_K0

English

If K = 0, the Grönwall bound simplifies to gronwallBound(δ,0,ε,x) = δ + ε x.

Русский

Если K = 0, граничащая функция Гронвалля упрощается до gronwallBound(δ,0,ε,x) = δ + ε x.

LaTeX

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

Lean4

theorem gronwallBound_K0 (δ ε : ℝ) : gronwallBound δ 0 ε = fun x => δ + ε * x :=
  funext fun _ => if_pos rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru