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 (EuclideanGeometry.inversion c R)
((R / dist x c) ^ 2 • ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {x - c})ᗮ).toLinearEquiv, continuous_toFun := ⋯,
continuous_invFun := ⋯ })
x
Formula for the Fréchet derivative of EuclideanGeometry.inversion c R.