hasStrictDerivAt_exp_smul_const' — Mathlib

English

For the setting with 𝕂, 𝕊, 𝔸, the derivative of u ↦ exp 𝕂 (u • x) at t is the linear map 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 hasStrictDerivAt_exp_smul_const' (x : 𝔸) (t : 𝕂) :
    HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t :=
  hasStrictDerivAt_exp_smul_const_of_mem_ball' _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

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