Inversion in an affine space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 euclidean_geometry.mul_dist_le_mul_dist_add_mul_dist.

source

noncomputable def euclidean_geometry.inversion {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c : P) (R : ℝ) (x : 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

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

source

theorem euclidean_geometry.inversion_vsub_center {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c : P) (R : ℝ) (x : P) :

euclidean_geometry.inversion c R x -ᵥ c = (R / has_dist.dist x c) ^ 2 • (x -ᵥ c)

source

@[simp]

theorem euclidean_geometry.inversion_self {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c : P) (R : ℝ) :

euclidean_geometry.inversion c R c = c

source

@[simp]

theorem euclidean_geometry.inversion_dist_center {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c x : P) :

euclidean_geometry.inversion c (has_dist.dist x c) x = x

source

theorem euclidean_geometry.inversion_of_mem_sphere {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {c x : P} {R : ℝ} (h : x ∈ metric.sphere c R) :

euclidean_geometry.inversion c R x = x

source

theorem euclidean_geometry.dist_inversion_center {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c x : P) (R : ℝ) :

has_dist.dist (euclidean_geometry.inversion c R x) c = R ^ 2 / has_dist.dist x c

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

source

theorem euclidean_geometry.dist_center_inversion {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c x : P) (R : ℝ) :

has_dist.dist c (euclidean_geometry.inversion c R x) = R ^ 2 / has_dist.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.

source

@[simp]

theorem euclidean_geometry.inversion_inversion {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) (x : P) :

euclidean_geometry.inversion c R (euclidean_geometry.inversion c R x) = x

source

theorem euclidean_geometry.inversion_involutive {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) :

function.involutive (euclidean_geometry.inversion c R)

source

theorem euclidean_geometry.inversion_surjective {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) :

function.surjective (euclidean_geometry.inversion c R)

source

theorem euclidean_geometry.inversion_injective {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) :

function.injective (euclidean_geometry.inversion c R)

source

theorem euclidean_geometry.inversion_bijective {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (c : P) {R : ℝ} (hR : R ≠ 0) :

function.bijective (euclidean_geometry.inversion c R)

source

theorem euclidean_geometry.dist_inversion_inversion {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {c x y : P} (hx : x ≠ c) (hy : y ≠ c) (R : ℝ) :

has_dist.dist (euclidean_geometry.inversion c R x) (euclidean_geometry.inversion c R y) = R ^ 2 / (has_dist.dist x c * has_dist.dist y c) * has_dist.dist x y

Distance between the images of two points under an inversion.

source

theorem euclidean_geometry.mul_dist_le_mul_dist_add_mul_dist {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (a b c d : P) :

has_dist.dist a c * has_dist.dist b d ≤ has_dist.dist a b * has_dist.dist c d + has_dist.dist b c * has_dist.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 euclidean_geometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical.