English
For any v ∈ E, the map stereoInvFunAux v has derivative at 0 equal to the identity on E, i.e., its Frechet derivative at 0 is the identity map.
Русский
Для любого v ∈ E производная по Фреше у stereoInvFunAux v в точке 0 равна тождественному отображению на E.
LaTeX
$$HasFDerivAt\ (stereoInvFunAux v)\ (ContinuousLinearMap.id\; \mathbb{R}\; E)\ 0$$
Lean4
theorem hasFDerivAt_stereoInvFunAux (v : E) : HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0 :=
by
have h₀ : HasFDerivAt (fun w : E => ‖w‖ ^ 2) (0 : StrongDual ℝ E) 0 :=
by
convert (hasStrictFDerivAt_norm_sq (0 : E)).hasFDerivAt
simp only [map_zero, smul_zero]
have h₁ : HasFDerivAt (fun w : E => (‖w‖ ^ 2 + 4)⁻¹) (0 : StrongDual ℝ E) 0 := by
convert (hasFDerivAt_inv _).comp _ (h₀.add (hasFDerivAt_const 4 0)) <;> simp
have h₂ : HasFDerivAt (fun w => (4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v) ((4 : ℝ) • ContinuousLinearMap.id ℝ E) 0 :=
by
convert
((hasFDerivAt_const (4 : ℝ) 0).smul (hasFDerivAt_id 0)).add
((h₀.sub (hasFDerivAt_const (4 : ℝ) 0)).smul (hasFDerivAt_const v 0)) using
1
ext w
simp
convert h₁.smul h₂ using 1
ext w
simp
