mathlib documentation

geometry.euclidean.circumcenter

Circumcenter and circumradius

This file proves some lemmas on points equidistant from a set of points, and defines the circumradius and circumcenter of a simplex. There are also some definitions for use in calculations where it is convenient to work with affine combinations of vertices together with the circumcenter.

Main definitions

References

p is equidistant from two points in s if and only if its orthogonal_projection is.

theorem euclidean_geometry.dist_set_eq_iff_dist_orthogonal_projection_eq {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace P} {ps : set P} (hps : ps s) (p : P) :

p is equidistant from a set of points in s if and only if its orthogonal_projection is.

theorem euclidean_geometry.exists_dist_eq_iff_exists_dist_orthogonal_projection_eq {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace P} {ps : set P} (hps : ps s) (p : P) :
(∃ (r : ), ∀ (p1 : P), p1 psdist p1 p = r) ∃ (r : ), ∀ (p1 : P), p1 psdist p1 ((euclidean_geometry.orthogonal_projection s) p) = r

There exists r such that p has distance r from all the points of a set of points in s if and only if there exists (possibly different) r such that its orthogonal_projection has that distance from all the points in that set.

theorem euclidean_geometry.exists_unique_dist_eq_of_insert {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace P} (hc : is_complete (s.direction)) {ps : set P} (hnps : ps.nonempty) {p : P} :
ps sp s(∃! (cccr : P × ), cccr.fst s ∀ (p1 : P), p1 psdist p1 cccr.fst = cccr.snd)(∃! (cccr₂ : P × ), cccr₂.fst affine_span (insert p s) ∀ (p1 : P), p1 insert p psdist p1 cccr₂.fst = cccr₂.snd)

The induction step for the existence and uniqueness of the circumcenter. Given a nonempty set of points in a nonempty affine subspace whose direction is complete, such that there is a unique (circumcenter, circumradius) pair for those points in that subspace, and a point p not in that subspace, there is a unique (circumcenter, circumradius) pair for the set with p added, in the span of the subspace with p added.

theorem euclidean_geometry.exists_unique_dist_eq_of_affine_independent {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {ι : Type u_3} [hne : nonempty ι] [fintype ι] {p : ι → P} :
affine_independent p(∃! (cccr : P × ), cccr.fst affine_span (set.range p) ∀ (i : ι), dist (p i) cccr.fst = cccr.snd)

Given a finite nonempty affinely independent family of points, there is a unique (circumcenter, circumradius) pair for those points in the affine subspace they span.

def affine.simplex.circumcenter_circumradius {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } :

The pair (circumcenter, circumradius) of a simplex.

Equations

The property satisfied by the (circumcenter, circumradius) pair.

def affine.simplex.circumcenter {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } :

The circumcenter of a simplex.

Equations
def affine.simplex.circumradius {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } :

The circumradius of a simplex.

Equations

The circumcenter lies in the affine span.

@[simp]
theorem affine.simplex.dist_circumcenter_eq_circumradius {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } (s : affine.simplex P n) (i : fin (n + 1)) :

All points have distance from the circumcenter equal to the circumradius.

@[simp]
theorem affine.simplex.dist_circumcenter_eq_circumradius' {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } (s : affine.simplex P n) (i : fin (n + 1)) :

All points have distance to the circumcenter equal to the circumradius.

theorem affine.simplex.eq_circumcenter_of_dist_eq {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } (s : affine.simplex P n) {p : P} (hp : p affine_span (set.range s.points)) {r : } :
(∀ (i : fin (n + 1)), dist (s.points i) p = r)p = s.circumcenter

Given a point in the affine span from which all the points are equidistant, that point is the circumcenter.

theorem affine.simplex.eq_circumradius_of_dist_eq {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } (s : affine.simplex P n) {p : P} (hp : p affine_span (set.range s.points)) {r : } :
(∀ (i : fin (n + 1)), dist (s.points i) p = r)r = s.circumradius

Given a point in the affine span from which all the points are equidistant, that distance is the circumradius.

theorem affine.simplex.circumradius_nonneg {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } (s : affine.simplex P n) :

The circumradius is non-negative.

theorem affine.simplex.circumradius_pos {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } (s : affine.simplex P (n + 1)) :

The circumradius of a simplex with at least two points is positive.

theorem affine.simplex.circumcenter_eq_point {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (s : affine.simplex P 0) (i : fin 1) :

The circumcenter of a 0-simplex equals its unique point.

The circumcenter of a 1-simplex equals its centroid.

If there exists a distance that a point has from all vertices of a simplex, the orthogonal projection of that point onto the subspace spanned by that simplex is its circumcenter.

If a point has the same distance from all vertices of a simplex, the orthogonal projection of that point onto the subspace spanned by that simplex is its circumcenter.

The orthogonal projection of the circumcenter onto a face is the circumcenter of that face.

theorem affine.simplex.circumcenter_eq_of_range_eq {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } {s₁ s₂ : affine.simplex P n} :

Two simplices with the same points have the same circumcenter.

An index type for the vertices of a simplex plus its circumcenter. This is for use in calculations where it is convenient to work with affine combinations of vertices together with the circumcenter. (An equivalent form sometimes used in the literature is placing the circumcenter at the origin and working with vectors for the vertices.)

@[simp]

points_with_circumcenter, applied to a point_index value, equals points applied to that value.

@[simp]

points_with_circumcenter, applied to circumcenter_index, equals the circumcenter.

@[simp]

point_weights_with_circumcenter sums to 1.

@[simp]

centroid_weights_with_circumcenter sums to 1, if the finset is nonempty.

The centroid of some vertices of a simplex, in terms of points_with_circumcenter.

@[simp]

reflection_circumcenter_weights_with_circumcenter sums to 1.

The reflection of the circumcenter of a simplex in an edge, in terms of points_with_circumcenter.

theorem euclidean_geometry.cospherical_iff_exists_mem_of_complete {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace P} {ps : set P} :
ps ss.nonemptyis_complete (s.direction)(euclidean_geometry.cospherical ps ∃ (center : P) (H : center s) (radius : ), ∀ (p : P), p psdist p center = radius)

Given a nonempty affine subspace, whose direction is complete, that contains a set of points, those points are cospherical if and only if they are equidistant from some point in that subspace.

theorem euclidean_geometry.cospherical_iff_exists_mem_of_finite_dimensional {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace P} {ps : set P} (h : ps s) (hn : s.nonempty) [finite_dimensional (s.direction)] :
euclidean_geometry.cospherical ps ∃ (center : P) (H : center s) (radius : ), ∀ (p : P), p psdist p center = radius

Given a nonempty affine subspace, whose direction is finite-dimensional, that contains a set of points, those points are cospherical if and only if they are equidistant from some point in that subspace.

All n-simplices among cospherical points in an n-dimensional subspace have the same circumradius.

Two n-simplices among cospherical points in an n-dimensional subspace have the same circumradius.

All n-simplices among cospherical points in n-space have the same circumradius.

theorem euclidean_geometry.circumradius_eq_of_cospherical {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {ps : set P} {n : } [finite_dimensional V] (hd : finite_dimensional.findim V = n) (hc : euclidean_geometry.cospherical ps) {sx₁ sx₂ : affine.simplex P n} :
set.range sx₁.points psset.range sx₂.points pssx₁.circumradius = sx₂.circumradius

Two n-simplices among cospherical points in n-space have the same circumradius.

All n-simplices among cospherical points in an n-dimensional subspace have the same circumcenter.

Two n-simplices among cospherical points in an n-dimensional subspace have the same circumcenter.

All n-simplices among cospherical points in n-space have the same circumcenter.

theorem euclidean_geometry.circumcenter_eq_of_cospherical {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {ps : set P} {n : } [finite_dimensional V] (hd : finite_dimensional.findim V = n) (hc : euclidean_geometry.cospherical ps) {sx₁ sx₂ : affine.simplex P n} :
set.range sx₁.points psset.range sx₂.points pssx₁.circumcenter = sx₂.circumcenter

Two n-simplices among cospherical points in n-space have the same circumcenter.

theorem euclidean_geometry.eq_or_eq_reflection_of_dist_eq {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : } {s : affine.simplex P n} {p p₁ p₂ : P} {r : } :
p₁ affine_span (insert p (set.range s.points))p₂ affine_span (insert p (set.range s.points))(∀ (i : fin (n + 1)), dist (s.points i) p₁ = r)(∀ (i : fin (n + 1)), dist (s.points i) p₂ = r)p₁ = p₂ p₁ = (euclidean_geometry.reflection (affine_span (set.range s.points))) p₂

Suppose all distances from p₁ and p₂ to the points of a simplex are equal, and that p₁ and p₂ lie in the affine span of p with the vertices of that simplex. Then p₁ and p₂ are equal or reflections of each other in the affine span of the vertices of the simplex.