Derivative of the inversion #
In this file we prove a formula for the derivative of EuclideanGeometry.inversion c R.
Implementation notes #
Since fderiv and related definitions do not work for affine spaces, we deal with an inner product
space in this file.
Keywords #
inversion, derivative
theorem
ContDiffWithinAt.inversion
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace โ E]
[NormedAddCommGroup F]
[InnerProductSpace โ F]
{c x : E โ F}
{R : E โ โ}
{s : Set E}
{a : E}
{n : โโ}
(hc : ContDiffWithinAt โ (โn) c s a)
(hR : ContDiffWithinAt โ (โn) R s a)
(hx : ContDiffWithinAt โ (โn) x s a)
(hne : x a โ c a)
:
ContDiffWithinAt โ (โn) (fun (a : E) => EuclideanGeometry.inversion (c a) (R a) (x a)) s a
theorem
ContDiffOn.inversion
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace โ E]
[NormedAddCommGroup F]
[InnerProductSpace โ F]
{c x : E โ F}
{R : E โ โ}
{s : Set E}
{n : โโ}
(hc : ContDiffOn โ (โn) c s)
(hR : ContDiffOn โ (โn) R s)
(hx : ContDiffOn โ (โn) x s)
(hne : โ a โ s, x a โ c a)
:
ContDiffOn โ (โn) (fun (a : E) => EuclideanGeometry.inversion (c a) (R a) (x a)) s
theorem
ContDiffAt.inversion
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace โ E]
[NormedAddCommGroup F]
[InnerProductSpace โ F]
{c x : E โ F}
{R : E โ โ}
{a : E}
{n : โโ}
(hc : ContDiffAt โ (โn) c a)
(hR : ContDiffAt โ (โn) R a)
(hx : ContDiffAt โ (โn) x a)
(hne : x a โ c a)
:
ContDiffAt โ (โn) (fun (a : E) => EuclideanGeometry.inversion (c a) (R a) (x a)) a
theorem
ContDiff.inversion
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace โ E]
[NormedAddCommGroup F]
[InnerProductSpace โ F]
{c x : E โ F}
{R : E โ โ}
{n : โโ}
(hc : ContDiff โ (โn) c)
(hR : ContDiff โ (โn) R)
(hx : ContDiff โ (โn) x)
(hne : โ (a : E), x a โ c a)
:
ContDiff โ โn fun (a : E) => EuclideanGeometry.inversion (c a) (R a) (x a)
theorem
DifferentiableWithinAt.inversion
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace โ E]
[NormedAddCommGroup F]
[InnerProductSpace โ F]
{c x : E โ F}
{R : E โ โ}
{s : Set E}
{a : E}
(hc : DifferentiableWithinAt โ c s a)
(hR : DifferentiableWithinAt โ R s a)
(hx : DifferentiableWithinAt โ x s a)
(hne : x a โ c a)
:
DifferentiableWithinAt โ (fun (a : E) => EuclideanGeometry.inversion (c a) (R a) (x a)) s a
theorem
DifferentiableOn.inversion
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace โ E]
[NormedAddCommGroup F]
[InnerProductSpace โ F]
{c x : E โ F}
{R : E โ โ}
{s : Set E}
(hc : DifferentiableOn โ c s)
(hR : DifferentiableOn โ R s)
(hx : DifferentiableOn โ x s)
(hne : โ a โ s, x a โ c a)
:
DifferentiableOn โ (fun (a : E) => EuclideanGeometry.inversion (c a) (R a) (x a)) s
theorem
DifferentiableAt.inversion
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace โ E]
[NormedAddCommGroup F]
[InnerProductSpace โ F]
{c x : E โ F}
{R : E โ โ}
{a : E}
(hc : DifferentiableAt โ c a)
(hR : DifferentiableAt โ R a)
(hx : DifferentiableAt โ x a)
(hne : x a โ c a)
:
DifferentiableAt โ (fun (a : E) => EuclideanGeometry.inversion (c a) (R a) (x a)) a
theorem
Differentiable.inversion
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace โ E]
[NormedAddCommGroup F]
[InnerProductSpace โ F]
{c x : E โ F}
{R : E โ โ}
(hc : Differentiable โ c)
(hR : Differentiable โ R)
(hx : Differentiable โ x)
(hne : โ (a : E), x a โ c a)
:
Differentiable โ fun (a : E) => EuclideanGeometry.inversion (c a) (R a) (x a)
theorem
EuclideanGeometry.hasFDerivAt_inversion
{F : Type u_2}
[NormedAddCommGroup F]
[InnerProductSpace โ F]
{c x : F}
{R : โ}
(hx : x โ c)
:
HasFDerivAt (inversion c R) ((R / dist x c) ^ 2 โข โ(โ โ (x - c))แฎ.reflection.toContinuousLinearEquiv) x
Formula for the Frรฉchet derivative of EuclideanGeometry.inversion c R.