Second intersection of a sphere and a line

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

• EuclideanGeometry.Sphere.secondInter is the second intersection of a sphere with a line through a point on that sphere.

def EuclideanGeometry.Sphere.secondInter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) (v : V) : P

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.

@[simp]

theorem EuclideanGeometry.Sphere.secondInter_map {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] [MetricSpace P₂] [NormedAddTorsor V₂ P₂] (s : Sphere P) (p : P) (v : V) (f : P →ᵃⁱ[ℝ] P₂) : { center := f s.center, radius := s.radius }.secondInter (f p) (f.linearIsometry v) = f (s.secondInter p v)

theorem EuclideanGeometry.Sphere.coe_secondInter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (as : AffineSubspace ℝ P) [Nonempty ↥as] (s : Sphere ↥as) (p : ↥as) (v : ↥as.direction) : ↑(s.secondInter p v) = { center := ↑s.center, radius := s.radius }.secondInter ↑p ↑v

@[simp]

theorem EuclideanGeometry.Sphere.secondInter_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) (v : V) : dist (s.secondInter p v) s.center = dist p s.center

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

@[simp]

theorem EuclideanGeometry.Sphere.secondInter_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} (v : V) : s.secondInter p v ∈ s ↔ p ∈ s

The point given by secondInter lies on the sphere.

@[simp]

theorem EuclideanGeometry.Sphere.secondInter_zero (V : Type u_1) {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) : s.secondInter p 0 = p

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

theorem EuclideanGeometry.Sphere.secondInter_eq_self_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} {v : V} : s.secondInter p v = p ↔ inner ℝ v (p -ᵥ s.center) = 0

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

theorem EuclideanGeometry.Sphere.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} (hp : p ∈ s) {v : V} {p' : P} (hp' : p' ∈ AffineSubspace.mk' p (ℝ ∙ v)) : p' = p ∨ p' = s.secondInter p v ↔ p' ∈ s

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

theorem EuclideanGeometry.Sphere.eq_or_eq_secondInter_iff_mem_of_mem_affineSpan_pair {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} (hp : p ∈ s) {p' : P} (hp' : p' ∈ affineSpan ℝ {p, q}) : p' = p ∨ p' = s.secondInter p (q -ᵥ p) ↔ p' ∈ s

A point on a line through a point on a sphere and a second point equals that point or secondInter.

@[simp]

theorem EuclideanGeometry.Sphere.secondInter_smul {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) (v : V) {r : ℝ} (hr : r ≠ 0) : s.secondInter p (r • v) = s.secondInter p v

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

@[simp]

theorem EuclideanGeometry.Sphere.secondInter_neg {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) (v : V) : s.secondInter p (-v) = s.secondInter p v

secondInter is unchanged by negating the vector.

@[simp]

theorem EuclideanGeometry.Sphere.secondInter_secondInter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) (v : V) : s.secondInter (s.secondInter p v) v = p

Applying secondInter twice returns the original point.

theorem EuclideanGeometry.Sphere.secondInter_eq_lineMap {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p p' : P) : s.secondInter p (p' -ᵥ p) = (AffineMap.lineMap p p') (-2 * inner ℝ (p' -ᵥ p) (p -ᵥ s.center) / inner ℝ (p' -ᵥ p) (p' -ᵥ p))

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

theorem EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p₁ p₂ : P) : s.secondInter p₁ (p₂ -ᵥ p₁) ∈ affineSpan ℝ {p₁, p₂}

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

theorem EuclideanGeometry.Sphere.secondInter_collinear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p p' : P) : Collinear ℝ {p, p', s.secondInter p (p' -ᵥ p)}

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

theorem EuclideanGeometry.Sphere.wbtw_secondInter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p p' : P} (hp : p ∈ s) (hp' : dist p' s.center ≤ s.radius) : Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

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

theorem EuclideanGeometry.Sphere.sbtw_secondInter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p p' : P} (hp : p ∈ s) (hp' : dist p' s.center < s.radius) : Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

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

theorem EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {n : ℕ} [NeZero n] {sx : Affine.Simplex ℝ P n} {i : Fin (n + 1)} (hi : sx.points i ∈ s) (hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius) {p : P} (hp : p ∈ (sx.faceOpposite i).interior) : (affineSpan ℝ (Set.range (sx.faceOpposite i).points)).SOppSide (sx.points i) (s.secondInter (sx.points i) (p -ᵥ sx.points i))

If the point passed to secondInter is a vertex of a simplex, lying on the sphere, and all vertices lie on or inside the sphere, and the vector passed to secondInter is given by a subtraction involving that vertex and a point in the interior of the opposite face, the given vertex and the result of secondInter are on opposite sides of that face.

theorem EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {n : ℕ} [n.AtLeastTwo] {sx : Affine.Simplex ℝ P n} {i : Fin (n + 1)} (hi : sx.points i ∈ s) (hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius) {p : P} (hp : p ∈ sx.interior) : (affineSpan ℝ (Set.range (sx.faceOpposite i).points)).SOppSide (sx.points i) (s.secondInter (sx.points i) (p -ᵥ sx.points i))

If the point passed to secondInter is a vertex of a simplex, lying on the sphere, and all vertices lie on or inside the sphere, and the vector passed to secondInter is given by a subtraction involving that vertex and a point in the interior of the simplex, the given vertex and the result of secondInter are on opposite sides of the face opposite that vertex.