English
In the same framework, the strict Fréchet derivative of u ↦ exp 𝕂 (u • x) at t is given by the same linear map as above, i.e., 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) = \big(h \mapsto \exp 𝕂 (t • x) (h • x)\big). $$$$
Lean4
theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕊)
(htx : t • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
HasStrictFDerivAt (fun u : 𝕊 => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smulRight x) t :=
let ⟨_, hp⟩ := analyticAt_exp_of_mem_ball (t • x) htx
have deriv₁ : HasStrictFDerivAt (fun u : 𝕊 => exp 𝕂 (u • x)) _ t :=
hp.hasStrictFDerivAt.comp t ((ContinuousLinearMap.id 𝕂 𝕊).smulRight x).hasStrictFDerivAt
have deriv₂ : HasFDerivAt (fun u : 𝕊 => exp 𝕂 (u • x)) _ t := hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx
deriv₁.hasFDerivAt.unique deriv₂ ▸ deriv₁
