mathlib3 documentation

geometry.euclidean.sphere.power

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 #

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} [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.

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} [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)) :

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

Intersecting Secants Theorem.