hasStrictFDerivAt_exp_smul_const_of_mem_ball'

English

The Complex.exp function coincides with the exponential map coming from NormedSpace.exp on ℂ.

Русский

Функция Complex.exp совпадает с экспонентой, задаваемой через NormedSpace.exp на ℂ.

LaTeX

$$$$ \text{Complex.exp} = \text{NormedSpace.exp } \mathbb{C}. $$$$

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)) (((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).smulRight (exp 𝕂 (t • x))) t :=
  by
  let ⟨_, _⟩ := analyticAt_exp_of_mem_ball (t • x) htx
  convert hasStrictFDerivAt_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 𝕂

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