# 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} [] [] {c : EF} {x : EF} {R : E} {s : Set E} {a : E} {n : ℕ∞} (hc : ) (hR : ) (hx : ) (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} [] [] {c : EF} {x : EF} {R : E} {s : Set E} {n : ℕ∞} (hc : ContDiffOn n c s) (hR : ContDiffOn n R s) (hx : ContDiffOn n x s) (hne : as, 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} [] [] {c : EF} {x : EF} {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} [] [] {c : EF} {x : EF} {R : E} {n : ℕ∞} (hc : ) (hR : ) (hx : ) (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} [] [] {c : EF} {x : EF} {R : E} {s : Set E} {a : E} (hc : ) (hR : ) (hx : ) (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} [] [] {c : EF} {x : EF} {R : E} {s : Set E} (hc : ) (hR : ) (hx : ) (hne : as, 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} [] [] {c : EF} {x : EF} {R : E} {a : E} (hc : ) (hR : ) (hx : ) (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} [] [] {c : EF} {x : EF} {R : E} (hc : ) (hR : ) (hx : ) (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} [] {c : F} {x : F} {R : } (hx : x c) :
HasFDerivAt ((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.