hasFDerivAt_exp_smul_const — Mathlib

English

Let 𝕂 be a complex-like field, and consider x ∈ 𝔸 and t ∈ 𝕊; the strict Fréchet derivative of u ↦ exp 𝕂 (u • x) at t is the linear map h ↦ exp 𝕂 (t • x) (h • x).

Русский

Пусть 𝕂 подобна комплексному полю, и x ∈ 𝔸, t ∈ 𝕊; строгая Фреше-производная от u ↦ exp 𝕂 (u • x) в t равна отображению h ↦ exp 𝕂 (t • x) (h • x).

LaTeX

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

Lean4

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

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