Second intersection of a sphere and a line #

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

This file defines and proves basic results about the second intersection of a sphere with a line through a point on that sphere.

Main definitions #

euclidean_geometry.sphere.second_inter is the second intersection of a sphere with a line through a point on that sphere.

source

noncomputable def euclidean_geometry.sphere.second_inter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : euclidean_geometry.sphere P) (p : P) (v : V) :

The second intersection of a sphere with a line through a point on that sphere; that point if it is the only point of intersection of the line with the sphere. The intended use of this definition is when p ∈ s; the definition does not use s.radius, so in general it returns the second intersection with the sphere through p and with center s.center.

Equations

s.second_inter p v = ((-2) * has_inner.inner v (p -ᵥ s.center) / has_inner.inner v v) • v +ᵥ p

source

@[simp]

theorem euclidean_geometry.sphere.second_inter_dist {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : euclidean_geometry.sphere P) (p : P) (v : V) :

has_dist.dist (s.second_inter p v) s.center = has_dist.dist p s.center

The distance between second_inter and the center equals the distance between the original point and the center.

source

@[simp]

theorem euclidean_geometry.sphere.second_inter_mem {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : euclidean_geometry.sphere P} {p : P} (v : V) :

s.second_inter p v ∈ s ↔ p ∈ s

The point given by second_inter lies on the sphere.

source

@[simp]

theorem euclidean_geometry.sphere.second_inter_zero (V : Type u_1) {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : euclidean_geometry.sphere P) (p : P) :

s.second_inter p 0 = p

If the vector is zero, second_inter gives the original point.

source

theorem euclidean_geometry.sphere.second_inter_eq_self_iff {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : euclidean_geometry.sphere P} {p : P} {v : V} :

s.second_inter p v = p ↔ has_inner.inner v (p -ᵥ s.center) = 0

The point given by second_inter equals the original point if and only if the line is orthogonal to the radius vector.

source

theorem euclidean_geometry.sphere.eq_or_eq_second_inter_of_mem_mk'_span_singleton_iff_mem {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : euclidean_geometry.sphere P} {p : P} (hp : p ∈ s) {v : V} {p' : P} (hp' : p' ∈ affine_subspace.mk' p (Span {v})) :

p' = p ∨ p' = s.second_inter p v ↔ p' ∈ s

A point on a line through a point on a sphere equals that point or second_inter.

source

@[simp]

theorem euclidean_geometry.sphere.second_inter_smul {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : euclidean_geometry.sphere P) (p : P) (v : V) {r : ℝ} (hr : r ≠ 0) :

s.second_inter p (r • v) = s.second_inter p v

second_inter is unchanged by multiplying the vector by a nonzero real.

source

@[simp]

theorem euclidean_geometry.sphere.second_inter_neg {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : euclidean_geometry.sphere P) (p : P) (v : V) :

s.second_inter p (-v) = s.second_inter p v

second_inter is unchanged by negating the vector.

source

@[simp]

theorem euclidean_geometry.sphere.second_inter_second_inter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : euclidean_geometry.sphere P) (p : P) (v : V) :

s.second_inter (s.second_inter p v) v = p

Applying second_inter twice returns the original point.

source

theorem euclidean_geometry.sphere.second_inter_eq_line_map {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : euclidean_geometry.sphere P) (p p' : P) :

s.second_inter p (p' -ᵥ p) = ⇑(affine_map.line_map p p') ((-2) * has_inner.inner (p' -ᵥ p) (p -ᵥ s.center) / has_inner.inner (p' -ᵥ p) (p' -ᵥ p))

If the vector passed to second_inter is given by a subtraction involving the point in second_inter, the result of second_inter may be expressed using line_map.

source

theorem euclidean_geometry.sphere.second_inter_vsub_mem_affine_span {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : euclidean_geometry.sphere P) (p₁ p₂ : P) :

s.second_inter p₁ (p₂ -ᵥ p₁) ∈ affine_span ℝ {p₁, p₂}

If the vector passed to second_inter is given by a subtraction involving the point in second_inter, the result lies in the span of the two points.

source

theorem euclidean_geometry.sphere.second_inter_collinear {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : euclidean_geometry.sphere P) (p p' : P) :

collinear ℝ {p, p', s.second_inter p (p' -ᵥ p)}

If the vector passed to second_inter is given by a subtraction involving the point in second_inter, the three points are collinear.

source

theorem euclidean_geometry.sphere.wbtw_second_inter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : euclidean_geometry.sphere P} {p p' : P} (hp : p ∈ s) (hp' : has_dist.dist p' s.center ≤ s.radius) :

wbtw ℝ p p' (s.second_inter p (p' -ᵥ p))

If the vector passed to second_inter is given by a subtraction involving the point in second_inter, and the second point is not outside the sphere, the second point is weakly between the first point and the result of second_inter.

source

theorem euclidean_geometry.sphere.sbtw_second_inter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : euclidean_geometry.sphere P} {p p' : P} (hp : p ∈ s) (hp' : has_dist.dist p' s.center < s.radius) :

sbtw ℝ p p' (s.second_inter p (p' -ᵥ p))

If the vector passed to second_inter is given by a subtraction involving the point in second_inter, and the second point is inside the sphere, the second point is strictly between the first point and the result of second_inter.