hasDerivAt_exp_smul_const' — Mathlib

English

In the same general framework, the derivative of the map u ↦ exp 𝕂 (u • x) with respect to u is given by the linear map h ↦ exp 𝕂 (u0 • x) h • x at any base point u0.

Русский

В той же общей конфигурации производная от u ↦ exp 𝕂 (u • x) по переменной u в точке u0 равна отображению h ↦ exp 𝕂 (u0 • x) (h • x).

LaTeX

$$$$ D\big(u \mapsto \exp 𝕂 (u • x)\big)(u_0)[h] = \exp 𝕂 (u_0 • x) (h • x). $$$$

Lean4

theorem hasDerivAt_exp_smul_const' (x : 𝔸) (t : 𝕂) : HasDerivAt (fun u : 𝕂 => exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t :=
  hasDerivAt_exp_smul_const_of_mem_ball' _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

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