hasDerivAt_gronwallBound_shift — Mathlib

English

For any a ∈ ℝ, the derivative of the shifted Grönwall bound gronwallBound(δ,K,ε)(y−a) at y = x is again given by K·gronwallBound(δ,K,ε)(x−a)+ε.

Русский

Для перемещённой по сдвигу функции Гронвалла граница производной в точке x равна K·gronwallBound(δ,K,ε)(x−a)+ε.

LaTeX

$$$\operatorname{HasDerivAt}(y\mapsto\operatorname{gronwallBound}(\delta,K,\varepsilon)(y-a),\; K\operatorname{gronwallBound}(\delta,K,\varepsilon)(x-a)+\varepsilon, x)$.$$

Lean4

theorem hasDerivAt_gronwallBound_shift (δ K ε x a : ℝ) :
    HasDerivAt (fun y => gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x :=
  by
  convert (hasDerivAt_gronwallBound δ K ε _).comp x ((hasDerivAt_id x).sub_const a) using 1
  rw [id, mul_one]

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