South and north poles of simplices.

This file defines the south and (generalized) north poles of a simplex, with respect to a vertex of that simplex: the second intersection with the circumsphere of a line through that vertex and the incenter or an excenter.

Main definitions

• Affine.Simplex.nsPole for the second intersection with the circumsphere of a line through a vertex and the excenter with the given set of indices
• Affine.Simplex.southPole for the second intersection with the circumsphere of a line through a vertex and the incenter
• Affine.Triangle.northPole for the second intersection with the circumsphere of a line through a vertex and an excenter other than the one opposite that vertex

References

• Paul Averous, Problèmes du Club de Maths

noncomputable def Affine.Simplex.nsPole {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) (i : Fin (n + 1)) : P

The generalized north pole of a simplex with respect to a given vertex and excenter is the second intersection with the circumsphere of the line through that vertex and excenter.

Equations

• s.nsPole signs i = s.circumsphere.secondInter (s.points i) (s.excenter signs -ᵥ s.points i)

theorem Affine.Simplex.nsPole_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))) (i : Fin (m + 1)) : (s.reindex e).nsPole signs i = s.nsPole (Finset.map e.symm.toEmbedding signs) (e.symm i)

@[simp]

theorem Affine.Simplex.ExcenterExists.nsPole_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₂] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)) : (s.map f.toAffineMap ⋯).nsPole signs i = f (s.nsPole signs i)

@[simp]

theorem Affine.Simplex.ExcenterExists.nsPole_restrict {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)) : ↑((s.restrict S hS).nsPole signs i) = s.nsPole signs i

noncomputable def Affine.Simplex.southPole {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : P

The south pole of a simplex with respect to a given vertex is the second intersection with the circumsphere of the line through that vertex and the incenter.

Equations

• s.southPole i = s.circumsphere.secondInter (s.points i) (s.incenter -ᵥ s.points i)

theorem Affine.Simplex.southPole_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) (i : Fin (m + 1)) : (s.reindex e).southPole i = s.southPole (e.symm i)

@[simp]

theorem Affine.Simplex.southPole_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₂] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)) : (s.map f.toAffineMap ⋯).southPole i = f (s.southPole i)

@[simp]

theorem Affine.Simplex.southPole_restrict {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)) : ↑((s.restrict S hS).southPole i) = s.southPole i

@[simp]

theorem Affine.Simplex.nsPole_empty {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.nsPole ∅ i = s.southPole i

@[simp]

theorem Affine.Simplex.nsPole_compl {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) (i : Fin (n + 1)) : s.nsPole signsᶜ i = s.nsPole signs i

@[simp]

theorem Affine.Simplex.ExcenterExists.nsPole_insert {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) {i : Fin (n + 1)} (hi : s.ExcenterExists (insert i signs)) : s.nsPole (insert i signs) i = s.nsPole signs i

@[simp]

theorem Affine.Simplex.ExcenterExists.nsPole_erase {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) {i : Fin (n + 1)} (hi : s.ExcenterExists (signs.erase i)) : s.nsPole (signs.erase i) i = s.nsPole signs i

@[simp]

theorem Affine.Simplex.nsPole_singleton_self {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] (i : Fin (n + 1)) : s.nsPole {i} i = s.southPole i

theorem Affine.Simplex.nsPole_mem_affineSpan_pair {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) (i : Fin (n + 1)) : s.nsPole signs i ∈ line[ℝ, s.points i, s.excenter signs]

theorem Affine.Simplex.southPole_mem_affineSpan_pair {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.southPole i ∈ line[ℝ, s.points i, s.incenter]

theorem Affine.Simplex.ExcenterExists.nsPole_mem_affineSpan_range {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i : Fin (n + 1)) : s.nsPole signs i ∈ affineSpan ℝ (Set.range s.points)

theorem Affine.Simplex.southPole_mem_affineSpan_range {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.southPole i ∈ affineSpan ℝ (Set.range s.points)

theorem Affine.Simplex.nsPole_mem_circumsphere {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) (i : Fin (n + 1)) : s.nsPole signs i ∈ s.circumsphere

theorem Affine.Simplex.southPole_mem_circumsphere {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.southPole i ∈ s.circumsphere

theorem Affine.Triangle.nsPole_singleton_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) : Simplex.nsPole t {i₂} i₁ = Simplex.nsPole t {i₃} i₁

noncomputable def Affine.Triangle.northPole {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (i : Fin 3) : P

The north pole of a triangle with respect to a given vertex is the second intersection with the circumsphere of the line through that vertex and an excenter other than the one opposite that vertex.

Equations

• t.northPole i = Affine.Simplex.nsPole t {i + 1} i

theorem Affine.Triangle.nsPole_singleton_eq_northPole {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i j : Fin 3} (h : i ≠ j) : Simplex.nsPole t {j} i = t.northPole i

theorem Affine.Triangle.northPole_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (e : Fin 3 ≃ Fin 3) (i : Fin 3) : northPole (Simplex.reindex t e) i = t.northPole (e.symm i)

@[simp]

theorem Affine.Triangle.northPole_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₂] (t : Triangle ℝ P) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin 3) : northPole (Simplex.map t f.toAffineMap ⋯) i = f (t.northPole i)

@[simp]

theorem Affine.Triangle.northPole_restrict {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range t.points) ≤ S) (i : Fin 3) : ↑(northPole (Simplex.restrict t S hS) i) = t.northPole i

theorem Affine.Triangle.northPole_mem_affineSpan_pair {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i j : Fin 3} (h : i ≠ j) : t.northPole i ∈ line[ℝ, t.points i, Simplex.excenter t {j}]

theorem Affine.Triangle.northPole_mem_affineSpan_range {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (i : Fin 3) : t.northPole i ∈ affineSpan ℝ (Set.range t.points)

theorem Affine.Triangle.northPole_mem_circumsphere {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (i : Fin 3) : t.northPole i ∈ Simplex.circumsphere t