# mathlibdocumentation

geometry.euclidean.sphere

# Spheres #

This file proves basic geometrical results about distances and angles in spheres in real inner product spaces and Euclidean affine spaces.

## Main theorems #

• mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi: Intersecting Chords Theorem (Freek No. 55).
• mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero: Intersecting Secants Theorem.
• mul_dist_add_mul_dist_eq_mul_dist_of_cospherical: Ptolemy’s Theorem (Freek No. 95).

TODO: The current statement of Ptolemy’s theorem works around the lack of a "cyclic polygon" concept in mathlib, which is what the theorem statement would naturally use (or two such concepts, since both a strict version, where all vertices must be distinct, and a weak version, where consecutive vertices may be equal, would be useful; Ptolemy's theorem should then use the weak one).

An API needs to be built around that concept, which would include:

• strict cyclic implies weak cyclic,
• weak cyclic and consecutive points distinct implies strict cyclic,
• weak/strict cyclic implies weak/strict cyclic for any subsequence,
• any three points on a sphere are weakly or strictly cyclic according to whether they are distinct,
• any number of points on a sphere intersected with a two-dimensional affine subspace are cyclic in some order,
• a list of points is cyclic if and only if its reversal is,
• a list of points is cyclic if and only if any cyclic permutation is, while other permutations are not when the points are distinct,
• a point P where the diagonals of a cyclic polygon cross exists (and is unique) with weak/strict betweenness depending on weak/strict cyclicity,
• four points on a sphere with such a point P are cyclic in the appropriate order, and so on.

### Geometrical results on spheres in real inner product spaces #

This section develops some results on spheres in real inner product spaces, which are used to deduce corresponding results for Euclidean affine spaces.

theorem inner_product_geometry.mul_norm_eq_abs_sub_sq_norm {V : Type u_1} {x y z : V} (h₁ : ∃ (k : ), k 1 x + y = k (x - y)) (h₂ : z - y = z + y) :
x - y * x + y = |z + y ^ 2 - z - x ^ 2|

### Geometrical results on spheres in Euclidean affine spaces #

This section develops some results on spheres in Euclidean affine spaces.

theorem euclidean_geometry.mul_dist_eq_abs_sub_sq_dist {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {a b p q : P} (hp : ∃ (k : ), k 1 b -ᵥ p = k (a -ᵥ p)) (hq : dist a q = dist b q) :
(dist a p) * dist b p = |dist b q ^ 2 - dist p q ^ 2|

If P is a point on the line AB and Q is equidistant from A and B, then AP * BP = abs (BQ ^ 2 - PQ ^ 2).

theorem euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {a b c d p : P} (h : euclidean_geometry.cospherical {a, b, c, d}) (hapb : ∃ (k₁ : ), k₁ 1 b -ᵥ p = k₁ (a -ᵥ p)) (hcpd : ∃ (k₂ : ), k₂ 1 d -ᵥ p = k₂ (c -ᵥ p)) :
(dist a p) * dist b p = (dist c p) * dist d p

If A, B, C, D are cospherical and P is on both lines AB and CD, then AP * BP = CP * DP.

theorem euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {a b c d p : P} (h : euclidean_geometry.cospherical {a, b, c, d}) (hapb : a p b = π) (hcpd : c p d = π) :
(dist a p) * dist b p = (dist c p) * dist d p

Intersecting Chords Theorem.

theorem euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {a b c d p : P} (h : euclidean_geometry.cospherical {a, b, c, d}) (hab : a b) (hcd : c d) (hapb : a p b = 0) (hcpd : c p d = 0) :
(dist a p) * dist b p = (dist c p) * dist d p

Intersecting Secants Theorem.

theorem euclidean_geometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {a b c d p : P} (h : euclidean_geometry.cospherical {a, b, c, d}) (hapc : a p c = π) (hbpd : b p d = π) :
(dist a b) * dist c d + (dist b c) * dist d a = (dist a c) * dist b d

Ptolemy’s Theorem.