Power of a point (intersecting chords and secants)

This file proves basic geometrical results about power of a point (intersecting chords and secants) 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.

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 InnerProductGeometry.mul_norm_eq_abs_sub_sq_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} {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 EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a : P} {b : P} {p : 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 EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a : P} {b : P} {c : P} {d : P} {p : P} (h : EuclideanGeometry.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 EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a : P} {b : P} {c : P} {d : P} {p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hapb : EuclideanGeometry.angle a p b = Real.pi) (hcpd : EuclideanGeometry.angle c p d = Real.pi) : dist a p * dist b p = dist c p * dist d p

Intersecting Chords Theorem.

theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a : P} {b : P} {c : P} {d : P} {p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hab : a ≠ b) (hcd : c ≠ d) (hapb : EuclideanGeometry.angle a p b = 0) (hcpd : EuclideanGeometry.angle c p d = 0) : dist a p * dist b p = dist c p * dist d p

Intersecting Secants Theorem.