Spaces orthogonal to the radius vector in spheres.

This file defines the affine subspace orthogonal to the radius vector at a point.

Main definitions

• EuclideanGeometry.Sphere.orthRadius: the affine subspace orthogonal to the radius vector at a point (the tangent space, if that point lies in the sphere; more generally, the polar of the inversion of that point in the sphere).

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

The affine subspace orthogonal to the radius vector of the sphere s at the point p (if p lies in s, this is the tangent space; generally, this is the polar of the inversion of p in s).

Equations

• s.orthRadius p = AffineSubspace.mk' p (Submodule.span ℝ {p -ᵥ s.center})ᗮ

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

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

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

@[simp]

theorem EuclideanGeometry.Sphere.direction_orthRadius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) : (s.orthRadius p).direction = (Submodule.span ℝ {p -ᵥ s.center})ᗮ

@[simp]

theorem EuclideanGeometry.Sphere.orthRadius_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) : s.orthRadius s.center = ⊤

@[simp]

theorem EuclideanGeometry.Sphere.center_mem_orthRadius_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} : s.center ∈ s.orthRadius p ↔ p = s.center

theorem EuclideanGeometry.Sphere.orthRadius_le_orthRadius_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} : s.orthRadius p ≤ s.orthRadius q ↔ p = q ∨ q = s.center

@[simp]

theorem EuclideanGeometry.Sphere.orthRadius_eq_orthRadius_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} : s.orthRadius p = s.orthRadius q ↔ p = q

theorem EuclideanGeometry.Sphere.finrank_orthRadius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [FiniteDimensional ℝ V] {s : Sphere P} {p : P} (hp : p ≠ s.center) : Module.finrank ℝ ↥(s.orthRadius p).direction + 1 = Module.finrank ℝ V

theorem EuclideanGeometry.Sphere.orthRadius_map {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} (p : P) {f : P ≃ᵃⁱ[ℝ] P} (h : f s.center = s.center) : AffineSubspace.map (↑f.toAffineEquiv) (s.orthRadius p) = s.orthRadius (f p)

theorem EuclideanGeometry.Sphere.direction_orthRadius_le_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} : (s.orthRadius p).direction ≤ (s.orthRadius q).direction ↔ ∃ (r : ℝ), q -ᵥ s.center = r • (p -ᵥ s.center)

theorem EuclideanGeometry.Sphere.orthRadius_parallel_orthRadius_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} : (s.orthRadius p).Parallel (s.orthRadius q) ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)