hasDerivAt_exp_smul_const — Mathlib

English

The derivative formula extends to the Frechet derivative: the derivative of u ↦ exp 𝕂 (u • x) at t acts by h ↦ exp 𝕂 (t • x) (h • x).

Русский

Формула производной распространяется на Фреше-производную: производная от u ↦ exp 𝕂 (u • x) в t действует как h ↦ exp 𝕂 (t • x) (h • x).

LaTeX

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

Lean4

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

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