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 definitions

• Sphere.power: The power of a point with respect to a sphere.

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.
• Sphere.mul_dist_eq_abs_power: The product of distances equals the absolute value of power.
• Sphere.dist_sq_eq_mul_dist_of_tangent_and_secant: Tangent-Secant 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 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 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 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 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 b c d p : P} (h : 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 b c d p : P} (h : Cospherical {a, b, c, d}) (hapb : angle a p b = Real.pi) (hcpd : 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 b c d p : P} (h : Cospherical {a, b, c, d}) (hab : a ≠ b) (hcd : c ≠ d) (hapb : angle a p b = 0) (hcpd : angle c p d = 0) : dist a p * dist b p = dist c p * dist d p

Intersecting Secants Theorem.

def EuclideanGeometry.Sphere.power {P : Type u_2} [MetricSpace P] (s : Sphere P) (p : P) : ℝ

The power of a point with respect to a sphere. For a point and a sphere, this is defined as the square of the distance from the point to the center minus the square of the radius. This value is positive if the point is outside the sphere, negative if inside, and zero if on the sphere.

Equations

• s.power p = dist p s.center ^ 2 - s.radius ^ 2

theorem EuclideanGeometry.Sphere.power_eq_zero_iff_mem_sphere {P : Type u_2} [MetricSpace P] {s : Sphere P} {p : P} (hr : 0 ≤ s.radius) : s.power p = 0 ↔ p ∈ s

A point lies on the sphere if and only if its power with respect to the sphere is zero.

theorem EuclideanGeometry.Sphere.power_pos_iff_radius_lt_dist_center {P : Type u_2} [MetricSpace P] {s : Sphere P} {p : P} (hr : 0 ≤ s.radius) : 0 < s.power p ↔ s.radius < dist p s.center

The power of a point is positive if and only if the point lies outside the sphere.

theorem EuclideanGeometry.Sphere.power_neg_iff_dist_center_lt_radius {P : Type u_2} [MetricSpace P] {s : Sphere P} {p : P} (hr : 0 ≤ s.radius) : s.power p < 0 ↔ dist p s.center < s.radius

The power of a point is negative if and only if the point lies inside the sphere.

theorem EuclideanGeometry.Sphere.power_nonneg_iff_radius_le_dist_center {P : Type u_2} [MetricSpace P] {s : Sphere P} {p : P} (hr : 0 ≤ s.radius) : 0 ≤ s.power p ↔ s.radius ≤ dist p s.center

The power of a point is nonnegative if and only if the point lies outside or on the sphere.

theorem EuclideanGeometry.Sphere.power_nonpos_iff_dist_center_le_radius {P : Type u_2} [MetricSpace P] {s : Sphere P} {p : P} (hr : 0 ≤ s.radius) : s.power p ≤ 0 ↔ dist p s.center ≤ s.radius

The power of a point is nonpositive if and only if the point lies inside or on the sphere.

theorem EuclideanGeometry.Sphere.mul_dist_eq_abs_power {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p a b : P} (hp : ∃ (k : ℝ), k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)) (ha : a ∈ s) (hb : b ∈ s) : dist p a * dist p b = |s.power p|

For any point, the product of distances to two intersection points on a line through the point equals the absolute value of the power of the point.

theorem EuclideanGeometry.Sphere.mul_dist_eq_zero_of_mem_sphere {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p a b : P} (hp : ∃ (k : ℝ), k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)) (ha : a ∈ s) (hb : b ∈ s) (hp_on : p ∈ s) : dist p a * dist p b = 0

For a point on the sphere, the product of distances to two other intersection points on a line through the point is zero.

theorem EuclideanGeometry.Sphere.mul_dist_eq_power_of_radius_le_dist_center {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p a b : P} (hr : 0 ≤ s.radius) (hp : ∃ (k : ℝ), k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)) (ha : a ∈ s) (hb : b ∈ s) (hle : s.radius ≤ dist p s.center) : dist p a * dist p b = s.power p

For a point outside or on the sphere, the product of distances to two intersection points on a line through the point equals the power of the point.

theorem EuclideanGeometry.Sphere.mul_dist_eq_neg_power_of_dist_center_le_radius {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p a b : P} (hr : 0 ≤ s.radius) (hp : ∃ (k : ℝ), k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)) (ha : a ∈ s) (hb : b ∈ s) (hle : dist p s.center ≤ s.radius) : dist p a * dist p b = -s.power p

For a point inside or on the sphere, the product of distances to two intersection points on a line through the point equals the negative of the power of the point.

theorem EuclideanGeometry.Sphere.dist_sq_eq_mul_dist_of_tangent_and_secant {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a b t p : P} {s : Sphere P} (ha : a ∈ s) (hb : b ∈ s) (h_secant : ∃ (k : ℝ), k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)) (h_tangent : s.IsTangentAt t (affineSpan ℝ {p, t})) : dist p t ^ 2 = dist p a * dist p b

Tangent-Secant Theorem. The square of the tangent length equals the product of secant segment lengths.