hasStrictDerivAt_exp_smul_const_of_mem_ball

English

Real.exp agrees with the real normed-space exponential on ℝ.

Русский

Real.exp совпадает с экспонентой в рамках нормированного пространства на ℝ.

LaTeX

$$$$ \text{Real.exp} = \text{NormedSpace.exp } \mathbb{R}. $$$$

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)) (exp 𝕂 (t • x) * x) t := by
  simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx).hasStrictDerivAt

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