The derivative of an inner product of vector-valued functions on a manifold #
For two functions g, g' : M → F from a real manifold to an RCLike inner product space, both
differentiable at x, the derivative of y ↦ ⟪g y, g' y⟫ obeys the product rule
d⟪g, g'⟫ = ⟪dg, g'⟫ + ⟪g, dg'⟫. This is the manifold counterpart of Mathlib's
fderiv_inner_apply, stated for mvfderiv.
On an open subset of a real inner product space, the derivative of the squared distance
y ↦ ‖y - a‖ ^ 2 vanishes exactly at the centre a.
Main results #
TauCeti.mvfderiv_inner_apply: the product rule for the inner product.TauCeti.mvfderiv_norm_sq_sub_subtypeVal_eq_zero_iff: along the inclusion of an open subset, the only critical point of squared distance is the centre.
theorem
TauCeti.mvfderiv_inner_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{𝕜 : Type u_4}
[RCLike 𝕜]
{F : Type u_5}
[NormedAddCommGroup F]
[InnerProductSpace 𝕜 F]
[NormedSpace ℝ F]
{g g' : M → F}
{x : M}
(hg : MDiffAt g x)
(hg' : MDiffAt g' x)
(v : TangentSpace I x)
:
The product rule for the inner product of two vector-valued functions on a manifold.
@[simp]
theorem
TauCeti.mvfderiv_norm_sq_sub_subtypeVal_eq_zero_iff
{G : Type u_6}
[NormedAddCommGroup G]
[InnerProductSpace ℝ G]
(U : TopologicalSpace.Opens G)
(a : G)
(x : ↥U)
:
Along the inclusion of an open subset of a real inner product space, the squared distance
from a has a critical point exactly at a.