EuclideanGeometry.hasFDerivAt_inversion

theorem EuclideanGeometry.hasFDerivAt_inversion : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {c x : F} {R : ℝ}, x ≠ c → HasFDerivAt (EuclideanGeometry.inversion c R) ((R / dist x c) ^ 2 • ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {x - c}).orthogonal).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x

This theorem describes the Fréchet derivative of the inversion function in Euclidean geometry. Specifically, given a normed add commutative group `F` with an inner product space over the reals, points `c` and `x` in `F`, and a real number `R`, if `x` is not equal to `c`, the derivative of the inversion function at `x` with respect to `c` and `R` exists. The derivative is a constant scalar, `(R / dist x c) ^ 2`, times the linear map which represents reflection through the orthogonal complement of the line spanned by `x - c`. The linearity and continuity properties of this map are omitted for brevity.

More concisely: Given a normed add commutative group `F` with an inner product, for `c` and `x` in `F` not equal, the inversion function's Fréchet derivative at `x` with respect to `c` and `R` is `(R / dist(x, c)) ^ 2 * π_(OrthogonalComplement {x - c})`, where `π_` denotes the projection onto the orthogonal complement.