Inversion: the punctured space, analyticity, isometries, and orientation

Inversion in a sphere of positive radius exchanges the punctured open ball with the exterior of the closed ball (TauCeti.dist_inversion_center_lt_iff, TauCeti.lt_dist_inversion_center_iff). For a nonzero radius it restricts to an involutive self-homeomorphism of the complement of its centre (TauCeti.inversionHomeomorph). In an RCLike field it is given by the conjugate-reciprocal formula c + R ^ 2 / conj (z - c), which in ℂ is the classical formula for reflection in a circle.

Inversion is analytic away from its centre (EuclideanGeometry.contDiffAt_inversion). This extends the smooth regularity provided by Mathlib's ContDiffAt.inversion to the analytic order.

Inversion in a sphere (EuclideanGeometry.inversion c R) is defined from the distance to the centre and the vector from the centre, both of which an affine isometry preserves. So an affine isometry carries the inversion in a sphere to the inversion in the image sphere, and a linear isometry fixing the centre commutes with the inversion. This is the compatibility used to compare inversion charts of the closed unit balls of two inner product spaces along a linear isometry.

For a nonzero radius R, the derivative of the inversion at a point x ≠ c is a positive multiple of the reflection in the hyperplane orthogonal to x - c (hasFDerivAt_inversion). So inversion is conformal, and it preserves the metric ⟪u, v⟫ / dist x c ^ 2 on the complement of c, the product metric of a cylinder in polar coordinates about c. In finite dimension the determinant of the derivative is negative: inversion reverses orientation. A transition between two inversion charts whose linear isometries lie in the same orientation class is a composite of two inversions and a linear isometry of positive determinant, so it preserves orientation. This is how the inversion charts of the closed unit ball attached to the isometries of one orientation class give an oriented atlas.

Main results

• TauCeti.inversionHomeomorph: inversion as a self-homeomorphism of the complement of its centre.
• TauCeti.inversion_eq_conj_reciprocal: inversion in an RCLike field is z ↦ c + R ^ 2 / conj (z - c).
• EuclideanGeometry.contDiffAt_inversion: inversion is analytic away from its centre.
• TauCeti.snd_inversion: the last coordinate of inversion about a centre in E × {0}.
• AffineIsometry.map_inversion: an affine isometry carries inversion in the sphere of centre c and radius R to inversion in the sphere of centre f c and radius R.
• LinearIsometry.map_inversion: the same for a linear isometry.
• EuclideanGeometry.norm_inversion_zero, EuclideanGeometry.norm_inversion_zero_one: the norm of the inversion about the origin.
• EuclideanGeometry.inv_lt_norm_inversion_iff, EuclideanGeometry.norm_inversion_lt_inv_iff: the inversion about the origin in the unit sphere exchanges the regions ‖v‖ < r and r⁻¹ < ‖w‖.
• EuclideanGeometry.inner_fderiv_inversion: inversion is conformal, its derivative scales inner products by (R / dist x c) ^ 4.
• EuclideanGeometry.inner_fderiv_inversion_div_dist_sq: inversion preserves the cylinder metric ⟪u, v⟫ / dist x c ^ 2.
• LinearIsometryEquiv.map_inversion_zero: a linear isometry equivalence commutes with inversion in a sphere about 0.
• EuclideanGeometry.det_fderiv_inversion_neg: the derivative of an inversion has negative determinant.

theorem EuclideanGeometry.contDiffAt_inversion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {c x : E} {R : ℝ} {n : WithTop ℕ∞} (hx : x ≠ c) : ContDiffAt ℝ n (inversion c R) x

Inversion in a sphere is C^n, including analytic, away from its centre.

theorem AffineIsometry.map_inversion {V : Type u_1} {V₂ : Type u_2} {P : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] [MetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[ℝ] P₂) (c : P) (R : ℝ) (x : P) : f (EuclideanGeometry.inversion c R x) = EuclideanGeometry.inversion (f c) R (f x)

An affine isometry carries the inversion in the sphere of centre c and radius R to the inversion in the sphere of centre f c and radius R.

theorem LinearIsometry.map_inversion {V : Type u_1} {V₂ : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] (f : V →ₗᵢ[ℝ] V₂) (c : V) (R : ℝ) (x : V) : f (EuclideanGeometry.inversion c R x) = EuclideanGeometry.inversion (f c) R (f x)

A linear isometry carries the inversion in the sphere of centre c and radius R to the inversion in the sphere of centre f c and radius R.

theorem LinearIsometryEquiv.map_inversion_zero {V : Type u_1} {V₂ : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] (f : V ≃ₗᵢ[ℝ] V₂) (R : ℝ) (x : V) : f (EuclideanGeometry.inversion 0 R x) = EuclideanGeometry.inversion 0 R (f x)

A linear isometry equivalence fixes 0, so it commutes with the inversion in a sphere about 0.

noncomputable def EuclideanGeometry.inversionFDerivEquiv {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (c z : V) (R : ℝ) (hR : R ≠ 0) (hz : z ≠ c) : V ≃L[ℝ] V

The derivative of inversion away from its centre is a continuous linear equivalence.

theorem EuclideanGeometry.hasFDerivAt_inversionFDerivEquiv {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (c z : V) (R : ℝ) (hR : R ≠ 0) (hz : z ≠ c) : HasFDerivAt (inversion c R) (↑(inversionFDerivEquiv c z R hR hz)) z

The inversion derivative equivalence represents the actual Fréchet derivative.

@[simp]

theorem EuclideanGeometry.norm_inversion_zero {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (R : ℝ) (x : V) : ‖inversion 0 R x‖ = R ^ 2 / ‖x‖

The norm of the inversion about the origin in a sphere of radius R.

theorem EuclideanGeometry.norm_inversion_zero_one {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) : ‖inversion 0 1 x‖ = ‖x‖⁻¹

The norm of the inversion about the origin in the unit sphere is the inverse norm.

theorem EuclideanGeometry.inv_lt_norm_inversion_iff {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {r : ℝ} (hr : 0 < r) {v : V} (hv : v ≠ 0) : r⁻¹ < ‖inversion 0 1 v‖ ↔ ‖v‖ < r

The inversion about the origin in the unit sphere carries the region ‖v‖ < r onto r⁻¹ < ‖w‖.

theorem EuclideanGeometry.norm_inversion_lt_inv_iff {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {r : ℝ} (hr : 0 < r) {v : V} (hv : v ≠ 0) : ‖inversion 0 1 v‖ < r⁻¹ ↔ r < ‖v‖

The inversion about the origin in the unit sphere carries the region r < ‖v‖ onto ‖w‖ < r⁻¹.

theorem EuclideanGeometry.inner_fderiv_inversion {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (c x : V) (R : ℝ) (u v : V) : inner ℝ ((fderiv ℝ (inversion c R) x) u) ((fderiv ℝ (inversion c R) x) v) = (R / dist x c) ^ 4 * inner ℝ u v

Inversion is conformal: its derivative at x multiplies inner products by (R / dist x c) ^ 4. At the centre both sides vanish.

theorem EuclideanGeometry.inner_fderiv_inversion_div_dist_sq {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (c x : V) {R : ℝ} (hR : R ≠ 0) (u v : V) : inner ℝ ((fderiv ℝ (inversion c R) x) u) ((fderiv ℝ (inversion c R) x) v) / dist (inversion c R x) c ^ 2 = inner ℝ u v / dist x c ^ 2

Inversion preserves the cylinder metric. The metric ⟪u, v⟫ / dist x c ^ 2 on the complement of c, which in polar coordinates about c is the product metric of the cylinder ℝ × S, is invariant under the inversion in a sphere of nonzero radius about c.

theorem EuclideanGeometry.det_fderiv_inversion_neg {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {c x : F} {R : ℝ} (hR : R ≠ 0) (hx : x ≠ c) : LinearMap.det ↑(fderiv ℝ (inversion c R) x) < 0

Inversion reverses orientation: away from its centre, the derivative of the inversion in a sphere of nonzero radius has negative determinant. The derivative is (R / dist x c) ^ 2 times the reflection in the hyperplane orthogonal to x - c, whose determinant is -1.

theorem TauCeti.snd_inversion {E : Type u_5} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E) (R : ℝ) (p : WithLp 2 (E × ℝ)) : (EuclideanGeometry.inversion (WithLp.toLp 2 (a, 0)) R p).snd = (R / dist p (WithLp.toLp 2 (a, 0))) ^ 2 * p.snd

The last coordinate of the inversion in a sphere centred on the boundary hyperplane.

@[simp]

theorem TauCeti.dist_inversion_center_lt_iff {V : Type u_1} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c x : P} {R : ℝ} (hR : 0 < R) (hx : x ≠ c) : dist (EuclideanGeometry.inversion c R x) c < R ↔ R < dist x c

Inversion in a sphere of positive radius sends a point other than the centre into the open ball exactly when the point lies outside the closed ball.

@[simp]

theorem TauCeti.lt_dist_inversion_center_iff {V : Type u_1} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c x : P} {R : ℝ} (hR : 0 < R) (hx : x ≠ c) : R < dist (EuclideanGeometry.inversion c R x) c ↔ dist x c < R

Inversion in a sphere of positive radius sends a point other than the centre outside the closed ball exactly when the point lies in the open ball.

noncomputable def TauCeti.inversionHomeomorph {V : Type u_1} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) : ↑{c}ᶜ ≃ₜ ↑{c}ᶜ

Inversion in a sphere of nonzero radius restricts to a self-homeomorphism of the complement of its centre.

@[simp]

theorem TauCeti.coe_inversionHomeomorph_apply {V : Type u_1} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) (x : ↑{c}ᶜ) : ↑((inversionHomeomorph c hR) x) = EuclideanGeometry.inversion c R ↑x

The restricted inversion homeomorphism acts by inversion.

@[simp]

theorem TauCeti.inversionHomeomorph_symm {V : Type u_1} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) : (inversionHomeomorph c hR).symm = inversionHomeomorph c hR

The restricted inversion homeomorphism is its own inverse.

theorem TauCeti.inversion_eq_conj_reciprocal {𝕜 : Type u_6} [RCLike 𝕜] (c : 𝕜) (R : ℝ) (z : 𝕜) : EuclideanGeometry.inversion c R z = c + ↑R ^ 2 / (starRingEnd 𝕜) (z - c)

In an RCLike field, inversion in the sphere of centre c and radius R is given by the conjugate-reciprocal formula; in ℂ this is the standard formula for reflection in a circle.