hasStrictFDerivAt_exp_smul_const'

English

Let 𝕂, 𝕊, 𝔸 be as above and x ∈ 𝔸, t ∈ 𝕊; 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 hasStrictFDerivAt_exp_smul_const' (x : 𝔸) (t : 𝕊) :
    HasStrictFDerivAt (fun u : 𝕊 => exp 𝕂 (u • x)) (((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).smulRight (exp 𝕂 (t • x))) t :=
  hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

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