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).

noncomputable 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).

instance EuclideanGeometry.Sphere.instNonemptySubtypeMemAffineSubspaceRealOrthRadius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) : Nonempty ↥(s.orthRadius p)

@[simp]

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 = (ℝ ∙ (p -ᵥ s.center))ᗮ

instance EuclideanGeometry.Sphere.instHasOrthogonalProjectionRealDirectionOrthRadius {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.HasOrthogonalProjection

@[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

@[simp]

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

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.orthRadius_injective {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) : Function.Injective s.orthRadius

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)

theorem EuclideanGeometry.Sphere.dist_sq_eq_iff_mem_orthRadius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} : dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2 ↔ q ∈ s.orthRadius p

theorem EuclideanGeometry.Sphere.dist_sq_eq_of_mem_orthRadius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} : q ∈ s.orthRadius p → dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2

Alias of the reverse direction of EuclideanGeometry.Sphere.dist_sq_eq_iff_mem_orthRadius.

theorem EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} : q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) ↔ 0 ≤ s.radius ∧ q -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2

theorem EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_vsub_mem_and_norm_sq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} (h : 0 ≤ s.radius) : q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) ↔ q -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2

theorem EuclideanGeometry.Sphere.vadd_mem_inter_orthRadius_iff_norm_sq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} {v : V} (h : 0 ≤ s.radius) (hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ) : v +ᵥ p ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) ↔ ‖v‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2

theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_singleton_of_dist_eq_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} (hp : dist p s.center = s.radius) : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {p}

theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_singleton_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q} ↔ q = p ∧ dist p s.center = s.radius

theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_of_radius_lt_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} (hp : s.radius < dist p s.center) : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅

theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_of_finrank_eq_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} (hpc : p ≠ s.center) (hp : dist p s.center ≠ s.radius) (hf : Module.finrank ℝ V = 1) : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅

theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔ s.radius < dist p s.center ∨ Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0

theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hf2 : Fact (Module.finrank ℝ V = 2)] {s : Sphere P} {p : P} (hp : dist p s.center ≤ s.radius) (hpc : p ≠ s.center) {v : V} (hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ) (hv1 : ‖v‖ = 1) : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p, -√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p}

In 2D, the line defined by s.orthRadius p intersects s at at most two points so long as p lies within s and not at its center.

This version provides expressions for those points in terms of an arbitrary vector in s.orthRadius p with norm 1.

theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_of_dist_le_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hf2 : Fact (Module.finrank ℝ V = 2)] {s : Sphere P} {p : P} (hp : dist p s.center ≤ s.radius) (hpc : p ≠ s.center) {v : V} (hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ) (hv0 : v ≠ 0) : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • v +ᵥ p, -(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • v +ᵥ p}

In 2D, the line defined by s.orthRadius p intersects s at at most two points so long as p lies within s and not at its center.

This version provides expressions for those points in terms of an arbitrary vector in s.orthRadius p.

theorem EuclideanGeometry.Sphere.ncard_inter_orthRadius_eq_two_of_dist_lt_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hf2 : Fact (Module.finrank ℝ V = 2)] {s : Sphere P} {p : P} (hp : dist p s.center < s.radius) (hpc : p ≠ s.center) : (Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)).ncard = 2

In 2D, the line defined by s.orthRadius p intersects s at exactly two points so long as p lies strictly within s and not at its center.

theorem EuclideanGeometry.Sphere.ncard_inter_orthRadius_le_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hf2 : Fact (Module.finrank ℝ V = 2)] {s : Sphere P} {p : P} (hpc : p ≠ s.center) : (Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)).ncard ≤ 2