English
Let E be a real inner product space and v ∈ E. Denote by i the canonical inclusion of the orthogonal complement (ℝ·v)⊥ into E. Then the Fréchet derivative at 0 of the composite stereoInvFun v ∘ i is the inclusion i; i.e., the derivative map equals the natural inclusion from (ℝ·v)⊥ to E.
Русский
Пусть E — вещественное пространство с скалярным произведением, и возьмём вектор v. Обозначим i естественное вложение из ортогонального дополнения (ℝ·v)⊥ в E. Тогда производная Фреше в точке 0 композиции stereoInvFun v ∘ i равна этому вложению, то есть производная есть включение.
LaTeX
$$$\\text{HasFDerivAt} \\bigl(\\text{stereoInvFun } v \\circ ((\\uparrow) : (\\mathbb{R} \\cdot v)^{\\perp} \\to E)\\bigr)\\; ((\\mathbb{R} \\cdot v)^{\\perp}.\\text{subtypeL})\\;0$$$
Lean4
theorem hasFDerivAt_stereoInvFunAux_comp_coe (v : E) :
HasFDerivAt (stereoInvFunAux v ∘ ((↑) : (ℝ ∙ v)ᗮ → E)) (ℝ ∙ v)ᗮ.subtypeL 0 :=
by
have : HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) ((ℝ ∙ v)ᗮ.subtypeL 0) :=
hasFDerivAt_stereoInvFunAux v
refine this.comp (0 : (ℝ ∙ v)ᗮ) (by apply ContinuousLinearMap.hasFDerivAt)
