hasFDerivAt_exp_smul_const_of_mem_ball'

English

In the same general setting, the strict Fréchet 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), \quad h \in 𝕊. $$$$

Lean4

theorem hasFDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕊)
    (htx : t • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasFDerivAt (fun u : 𝕊 => exp 𝕂 (u • x)) (((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).smulRight (exp 𝕂 (t • x))) t :=
  by
  convert hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1
  ext t'
  change Commute (t' • x) (exp 𝕂 (t • x))
  exact (((Commute.refl x).smul_left t').smul_right t).exp_right 𝕂

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