hasStrictDerivAt_exp_smul_const — Mathlib

English

Let 𝕂, 𝕊, 𝔸, x ∈ 𝔸, t ∈ 𝕂 with ball condition; the strict Fréchet derivative of u ↦ exp 𝕂 (u • x) at t is exp 𝕂 (t • x) times the smulRight x operator.

Русский

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

LaTeX

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

Lean4

theorem hasStrictDerivAt_exp_smul_const (x : 𝔸) (t : 𝕂) :
    HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t :=
  hasStrictDerivAt_exp_smul_const_of_mem_ball _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

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