hasStrictDerivAt_exp_smul_const_of_mem_ball'

English

For the general setting, the strict Fréchet derivative of u ↦ exp 𝕂 (u • x) at t is exp 𝕂 (t • x) times smulRight x.

Русский

Для общей конфигурации строгая Фреше-производная от u ↦ exp 𝕂 (u • x) в t равна exp 𝕂 (t • x) умноженному на smulRight x.

LaTeX

$$$$ D\big(u \mapsto \exp 𝕂 (u • x)\big)(t) = \exp 𝕂 (t • x) \; (\mathrm{smulRight}\, x). $$$$

Lean4

theorem hasStrictDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕂)
    (htx : t • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t := by
  simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 x t htx).hasStrictDerivAt

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