Power of a point (intersecting chords and secants) #

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

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.

source

theorem inner_product_geometry.mul_norm_eq_abs_sub_sq_norm {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] {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.

source

theorem euclidean_geometry.mul_dist_eq_abs_sub_sq_dist {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] {P : Type u_2} [metric_space P] [normed_add_torsor V P] {a b p q : P} (hp : ∃ (k : ℝ), k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)) (hq : has_dist.dist a q = has_dist.dist b q) :

has_dist.dist a p * has_dist.dist b p = |has_dist.dist b q ^ 2 - has_dist.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).

source

theorem euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] {P : Type u_2} [metric_space P] [normed_add_torsor V 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)) :

has_dist.dist a p * has_dist.dist b p = has_dist.dist c p * has_dist.dist d p

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

source

theorem euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] {P : Type u_2} [metric_space P] [normed_add_torsor V P] {a b c d p : P} (h : euclidean_geometry.cospherical {a, b, c, d}) (hapb : euclidean_geometry.angle a p b = real.pi) (hcpd : euclidean_geometry.angle c p d = real.pi) :

has_dist.dist a p * has_dist.dist b p = has_dist.dist c p * has_dist.dist d p

Intersecting Chords Theorem.

source

theorem euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] {P : Type u_2} [metric_space P] [normed_add_torsor V P] {a b c d p : P} (h : euclidean_geometry.cospherical {a, b, c, d}) (hab : a ≠ b) (hcd : c ≠ d) (hapb : euclidean_geometry.angle a p b = 0) (hcpd : euclidean_geometry.angle c p d = 0) :

has_dist.dist a p * has_dist.dist b p = has_dist.dist c p * has_dist.dist d p

Intersecting Secants Theorem.