hasStrictFDerivAt_exp_smul_const — Mathlib

English

For the general setting the strict Fréchet derivative of u ↦ exp 𝕂 (u • x) is the linear map h ↦ exp 𝕂 (t • x) (h • x).

Русский

В общем случае строгая Фреше-производная от u ↦ exp 𝕂 (u • x) равна отображению h ↦ exp 𝕂 (t • x) (h • x).

LaTeX

$$$$ \text{HasStrictFDerivAt}\ (u \mapsto \exp 𝕂 (u • x))\ (t) = \exp 𝕂 (t • x) \; (\mathrm{smulRight}\; x). $$$$

Lean4

theorem hasStrictFDerivAt_exp_smul_const (x : 𝔸) (t : 𝕊) :
    HasStrictFDerivAt (fun u : 𝕊 => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smulRight x) t :=
  hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

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