Poles and polars

This file defines poles and polars for spheres in Euclidean spaces.

Main definitions

• EuclideanGeometry.Sphere.pole: the inversion in the sphere of the point in an affine subspace closest to the center. This maps an affine subspace (typically of codimension one) to a point.

• EuclideanGeometry.Sphere.polar: the affine subspace orthogonal to the radius vector at a point and passing through its inversion in the sphere. This maps a point to an affine subspace (typically of codimension one, for a point not the center of the sphere).

Main theorems

• EuclideanGeometry.Sphere.mem_polar_iff_mem_polar: La Hire's theorem.

noncomputable def EuclideanGeometry.Sphere.pole {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (as : AffineSubspace ℝ P) [Nonempty ↥as] [as.direction.HasOrthogonalProjection] : P

The pole of an affine subspace is the inversion in the sphere of the point in that subspace closest to the center.

Equations

• s.pole as = EuclideanGeometry.inversion s.center s.radius ↑((EuclideanGeometry.orthogonalProjection as) s.center)

noncomputable def EuclideanGeometry.Sphere.polar {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 polar of a point is the affine subspace orthogonal to the radius vector at that point and passing through its inversion in the sphere.

Equations

• s.polar p = s.orthRadius (EuclideanGeometry.inversion s.center s.radius p)

instance EuclideanGeometry.Sphere.instHasOrthogonalProjectionRealDirectionPolar {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) : (s.polar p).direction.HasOrthogonalProjection

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

@[simp]

theorem EuclideanGeometry.Sphere.direction_polar {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} (hs : s.radius ≠ 0) (p : P) : (s.polar p).direction = (ℝ ∙ (p -ᵥ s.center))ᗮ

@[simp]

theorem EuclideanGeometry.Sphere.pole_polar {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} (hs : s.radius ≠ 0) (p : P) : s.pole (s.polar p) = p

theorem EuclideanGeometry.Sphere.orthRadius_eq_polar_inversion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} (hs : s.radius ≠ 0) (p : P) : s.orthRadius p = s.polar (inversion s.center s.radius p)

@[simp]

theorem EuclideanGeometry.Sphere.polar_pole_orthRadius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} (hs : s.radius ≠ 0) (p : P) : s.polar (s.pole (s.orthRadius p)) = s.orthRadius p

@[simp]

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

@[simp]

theorem EuclideanGeometry.Sphere.polar_zero_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} (hs : s.radius = 0) (p : P) : s.polar p = ⊤

@[simp]

theorem EuclideanGeometry.Sphere.polar_eq_orthRadius_self_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} (hs : 0 ≤ s.radius) {p : P} : s.polar p = s.orthRadius p ↔ p ∈ s ∨ p = s.center

theorem EuclideanGeometry.Sphere.mem_polar_iff_inner {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} : p₁ ∈ s.polar p₂ ↔ s.radius = 0 ∨ p₂ = s.center ∨ inner ℝ (p₁ -ᵥ s.center) (p₂ -ᵥ s.center) = s.radius ^ 2

theorem EuclideanGeometry.Sphere.mem_polar_iff_mem_polar {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.center) (hp₂ : p₂ ≠ s.center) : p₁ ∈ s.polar p₂ ↔ p₂ ∈ s.polar p₁

La Hire's theorem: p₁ lies on the polar of p₂ if and only if p₂ lies on the polar of p₁.

theorem EuclideanGeometry.Sphere.mem_orthRadius_iff_mem_polar_of_mem {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.center) (hp₂ : p₂ ∈ s) : p₁ ∈ s.orthRadius p₂ ↔ p₂ ∈ s.polar p₁

theorem EuclideanGeometry.Sphere.mem_polar_of_mem_of_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} (hp₂ : p₂ ∈ s) (h : p₁ ∈ s.orthRadius p₂) : p₂ ∈ s.polar p₁

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