Inversion in an affine space

In this file we define inversion in a sphere in an affine space. This map sends each point x to the point y such that y -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c), where c and R are the center and the radius the sphere.

In many applications, it is convenient to assume that the inversions swaps the center and the point at infinity. In order to stay in the original affine space, we define the map so that it sends center to itself.

Currently, we prove only a few basic lemmas needed to prove Ptolemy's inequality, see EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist.

def EuclideanGeometry.inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) (R : ℝ) (x : P) : P

Inversion in a sphere in an affine space. This map sends each point x to the point y such that y -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c), where c and R are the center and the radius the sphere.

Equations

• EuclideanGeometry.inversion c R x = (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c

theorem EuclideanGeometry.inversion_def {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] : EuclideanGeometry.inversion = fun (c : P) (R : ℝ) (x : P) => (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c

Basic properties

In this section we prove that EuclideanGeometry.inversion c R is involutive and preserves the sphere Metric.sphere c R. We also prove that the distance to the center of the image of x under this inversion is given by R ^ 2 / dist x c.

theorem EuclideanGeometry.inversion_eq_lineMap {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) (R : ℝ) (x : P) : EuclideanGeometry.inversion c R x = (AffineMap.lineMap c x) ((R / dist x c) ^ 2)

theorem EuclideanGeometry.inversion_vsub_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) (R : ℝ) (x : P) : EuclideanGeometry.inversion c R x -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c)

@[simp]

theorem EuclideanGeometry.inversion_self {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) (R : ℝ) : EuclideanGeometry.inversion c R c = c

@[simp]

theorem EuclideanGeometry.inversion_zero_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) (x : P) : EuclideanGeometry.inversion c 0 x = c

theorem EuclideanGeometry.inversion_mul {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) (a : ℝ) (R : ℝ) (x : P) : EuclideanGeometry.inversion c (a * R) x = (AffineMap.homothety c (a ^ 2)) (EuclideanGeometry.inversion c R x)

@[simp]

theorem EuclideanGeometry.inversion_dist_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) (x : P) : EuclideanGeometry.inversion c (dist x c) x = x

@[simp]

theorem EuclideanGeometry.inversion_dist_center' {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) (x : P) : EuclideanGeometry.inversion c (dist c x) x = x

theorem EuclideanGeometry.inversion_of_mem_sphere {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {x : P} {R : ℝ} (h : x ∈ Metric.sphere c R) : EuclideanGeometry.inversion c R x = x

theorem EuclideanGeometry.dist_inversion_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) (x : P) (R : ℝ) : dist (EuclideanGeometry.inversion c R x) c = R ^ 2 / dist x c

Distance from the image of a point under inversion to the center. This formula accidentally works for x = c.

theorem EuclideanGeometry.dist_center_inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) (x : P) (R : ℝ) : dist c (EuclideanGeometry.inversion c R x) = R ^ 2 / dist c x

Distance from the center of an inversion to the image of a point under the inversion. This formula accidentally works for x = c.

@[simp]

theorem EuclideanGeometry.inversion_inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) (x : P) : EuclideanGeometry.inversion c R (EuclideanGeometry.inversion c R x) = x

theorem EuclideanGeometry.inversion_involutive {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) : Function.Involutive (EuclideanGeometry.inversion c R)

theorem EuclideanGeometry.inversion_surjective {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) : Function.Surjective (EuclideanGeometry.inversion c R)

theorem EuclideanGeometry.inversion_injective {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) : Function.Injective (EuclideanGeometry.inversion c R)

theorem EuclideanGeometry.inversion_bijective {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) : Function.Bijective (EuclideanGeometry.inversion c R)

theorem EuclideanGeometry.inversion_eq_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {x : P} {R : ℝ} (hR : R ≠ 0) : EuclideanGeometry.inversion c R x = c ↔ x = c

@[simp]

theorem EuclideanGeometry.inversion_eq_center' {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {x : P} {R : ℝ} : EuclideanGeometry.inversion c R x = c ↔ x = c ∨ R = 0

theorem EuclideanGeometry.center_eq_inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {x : P} {R : ℝ} (hR : R ≠ 0) : c = EuclideanGeometry.inversion c R x ↔ x = c

@[simp]

theorem EuclideanGeometry.center_eq_inversion' {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {x : P} {R : ℝ} : c = EuclideanGeometry.inversion c R x ↔ x = c ∨ R = 0

Similarity of triangles

If inversion with center O sends A to A' and B to B', then the triangle OB'A' is similar to the triangle OAB with coefficient R ^ 2 / (|OA|*|OB|) and the triangle OA'B is similar to the triangle OAB' with coefficient |OB|/|OA|. We formulate these statements in terms of ratios of the lengths of their sides.

theorem EuclideanGeometry.dist_inversion_inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {x : P} {y : P} (hx : x ≠ c) (hy : y ≠ c) (R : ℝ) : dist (EuclideanGeometry.inversion c R x) (EuclideanGeometry.inversion c R y) = R ^ 2 / (dist x c * dist y c) * dist x y

Distance between the images of two points under an inversion.

theorem EuclideanGeometry.dist_inversion_mul_dist_center_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {x : P} {y : P} {R : ℝ} (hx : x ≠ c) (hy : y ≠ c) : dist (EuclideanGeometry.inversion c R x) y * dist x c = dist x (EuclideanGeometry.inversion c R y) * dist y c

Ptolemy's inequality

theorem EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (a : P) (b : P) (c : P) (d : P) : dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Ptolemy's inequality: in a quadrangle ABCD, |AC| * |BD| ≤ |AB| * |CD| + |BC| * |AD|. If ABCD is a convex cyclic polygon, then this inequality becomes an equality, see EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical.

Continuity of inversion

theorem Filter.Tendsto.inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {α : Type u_3} {x : P} {c : P} {R : ℝ} {l : Filter α} {fc : α → P} {fx : α → P} {fR : α → ℝ} (hc : Filter.Tendsto fc l (nhds c)) (hR : Filter.Tendsto fR l (nhds R)) (hx : Filter.Tendsto fx l (nhds x)) (hne : x ≠ c) : Filter.Tendsto (fun (a : α) => EuclideanGeometry.inversion (fc a) (fR a) (fx a)) l (nhds (EuclideanGeometry.inversion c R x))

theorem ContinuousWithinAt.inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {X : Type u_3} [TopologicalSpace X] {c : X → P} {x : X → P} {R : X → ℝ} {a₀ : X} {s : Set X} (hc : ContinuousWithinAt c s a₀) (hR : ContinuousWithinAt R s a₀) (hx : ContinuousWithinAt x s a₀) (hne : x a₀ ≠ c a₀) : ContinuousWithinAt (fun (a : X) => EuclideanGeometry.inversion (c a) (R a) (x a)) s a₀

theorem ContinuousAt.inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {X : Type u_3} [TopologicalSpace X] {c : X → P} {x : X → P} {R : X → ℝ} {a₀ : X} (hc : ContinuousAt c a₀) (hR : ContinuousAt R a₀) (hx : ContinuousAt x a₀) (hne : x a₀ ≠ c a₀) : ContinuousAt (fun (a : X) => EuclideanGeometry.inversion (c a) (R a) (x a)) a₀

theorem ContinuousOn.inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {X : Type u_3} [TopologicalSpace X] {c : X → P} {x : X → P} {R : X → ℝ} {s : Set X} (hc : ContinuousOn c s) (hR : ContinuousOn R s) (hx : ContinuousOn x s) (hne : ∀ a ∈ s, x a ≠ c a) : ContinuousOn (fun (a : X) => EuclideanGeometry.inversion (c a) (R a) (x a)) s

theorem Continuous.inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {X : Type u_3} [TopologicalSpace X] {c : X → P} {x : X → P} {R : X → ℝ} (hc : Continuous c) (hR : Continuous R) (hx : Continuous x) (hne : ∀ (a : X), x a ≠ c a) : Continuous fun (a : X) => EuclideanGeometry.inversion (c a) (R a) (x a)