English
The derivative of gronwallBound with respect to its argument equals K·gronwallBound(δ,K,ε,x) + ε; i.e., the instantaneous rate of growth is proportional to the current bound plus a constant ε.
Русский
Производная функции Гронвалла по аргументу равна K·gronwallBound(δ,K,ε,x) + ε; тем самым мгновенная скорость роста пропорциональна текущей границе плюс константа ε.
LaTeX
$$$\dfrac{d}{dx}\operatorname{gronwallBound}(\delta,K,\varepsilon,x)=K\,\operatorname{gronwallBound}(\delta,K,\varepsilon,x)+\varepsilon$; equivalently, HasDerivAt(...).$$
Lean4
theorem hasDerivAt_gronwallBound (δ K ε x : ℝ) : HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x :=
by
by_cases hK : K = 0
· subst K
simp only [gronwallBound_K0, zero_mul, zero_add]
convert ((hasDerivAt_id x).const_mul ε).const_add δ
rw [mul_one]
· simp only [gronwallBound_of_K_ne_0 hK]
convert
(((hasDerivAt_id x).const_mul K).exp.const_mul δ).add
((((hasDerivAt_id x).const_mul K).exp.sub_const 1).const_mul (ε / K)) using
1
simp only [id, mul_add, (mul_assoc _ _ _).symm, mul_comm _ K, mul_div_cancel₀ _ hK]
ring
