hasDerivAt_exp_smul_const_of_mem_ball

English

In the same framework, the strict 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

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

Lean4

theorem hasDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕂)
    (htx : t • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasDerivAt (fun u : 𝕂 => exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t :=
  (hasStrictDerivAt_exp_smul_const_of_mem_ball x t htx).hasDerivAt

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