mathlib docs: geometry.euclidean.circumcenter

source

theorem euclidean_geometry.dist_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} (hn : ↑s.nonempty) (hc : is_complete ↑(s.direction)) {p1 p2 : P} (p3 : P) :

p1 ∈ s → p2 ∈ s → (has_dist.dist p1 p3 = has_dist.dist p2 p3 ↔ has_dist.dist p1 (⇑(euclidean_geometry.orthogonal_projection hn hc) p3) = has_dist.dist p2 (⇑(euclidean_geometry.orthogonal_projection hn hc) p3))

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

source

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} (hn : ↑s.nonempty) (hc : is_complete ↑(s.direction)) {ps : set P} (hps : ps ⊆ ↑s) (p : P) :

ps.pairwise_on (λ (p1 p2 : P), has_dist.dist p1 p = has_dist.dist p2 p) ↔ ps.pairwise_on (λ (p1 p2 : P), has_dist.dist p1 (⇑(euclidean_geometry.orthogonal_projection hn hc) p) = has_dist.dist p2 (⇑(euclidean_geometry.orthogonal_projection hn hc) p))

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

source

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} (hn : ↑s.nonempty) (hc : is_complete ↑(s.direction)) {ps : set P} (hps : ps ⊆ ↑s) (p : P) :

(∃ (r : ℝ), ∀ (p1 : P), p1 ∈ ps → has_dist.dist p1 p = r) ↔ ∃ (r : ℝ), ∀ (p1 : P), p1 ∈ ps → has_dist.dist p1 (⇑(euclidean_geometry.orthogonal_projection hn hc) 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.

source

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} (hn : ↑s.nonempty) (hc : is_complete ↑(s.direction)) {ps : set P} (hnps : ps.nonempty) {p : P} :

ps ⊆ ↑s → p ∉ s → (∃! (cccr : P × ℝ), cccr.fst ∈ s ∧ ∀ (p1 : P), p1 ∈ ps → has_dist.dist p1 cccr.fst = cccr.snd) → (∃! (cccr₂ : P × ℝ), cccr₂.fst ∈ affine_span ℝ (has_insert.insert p ↑s) ∧ ∀ (p1 : P), p1 ∈ has_insert.insert p ps → has_dist.dist 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.

source

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 : ι), has_dist.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.

source

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 : ℕ} :

affine.simplex ℝ P n → P × ℝ

The pair (circumcenter, circumradius) of a simplex.

Equations

s.circumcenter_circumradius = Exists.some _

source

theorem affine.simplex.circumcenter_circumradius_unique_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) :

(s.circumcenter_circumradius.fst ∈ affine_span ℝ (set.range s.points) ∧ ∀ (i : fin (n + 1)), has_dist.dist (s.points i) s.circumcenter_circumradius.fst = s.circumcenter_circumradius.snd) ∧ ∀ (cccr : P × ℝ), (cccr.fst ∈ affine_span ℝ (set.range s.points) ∧ ∀ (i : fin (n + 1)), has_dist.dist (s.points i) cccr.fst = cccr.snd) → cccr = s.circumcenter_circumradius

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

source

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 : ℕ} :

affine.simplex ℝ P n → P

The circumcenter of a simplex.

Equations

s.circumcenter = s.circumcenter_circumradius.fst

source

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 : ℕ} :

affine.simplex ℝ P n → ℝ

The circumradius of a simplex.

Equations

s.circumradius = s.circumcenter_circumradius.snd

source

theorem affine.simplex.circumcenter_mem_affine_span {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) :

s.circumcenter ∈ affine_span ℝ (set.range s.points)

The circumcenter lies in the affine span.

source

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

has_dist.dist (s.points i) s.circumcenter = s.circumradius

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

source

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

has_dist.dist s.circumcenter (s.points i) = s.circumradius

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

source

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

source

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

source

inductive affine.simplex.points_with_circumcenter_index :

ℕ → Type

point_index : Π (n : ℕ), fin (n + 1) → affine.simplex.points_with_circumcenter_index n
circumcenter_index : Π (n : ℕ), affine.simplex.points_with_circumcenter_index n

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

source

@[instance]

def affine.simplex.points_with_circumcenter_index.fintype (n : ℕ) :

fintype (affine.simplex.points_with_circumcenter_index n)

source

@[instance]

def affine.simplex.points_with_circumcenter_index_inhabited (n : ℕ) :

inhabited (affine.simplex.points_with_circumcenter_index n)

Equations

affine.simplex.points_with_circumcenter_index_inhabited n = {default := affine.simplex.points_with_circumcenter_index.circumcenter_index n}

source

def affine.simplex.point_index_embedding (n : ℕ) :

fin (n + 1) ↪ affine.simplex.points_with_circumcenter_index n

point_index as an embedding.

Equations

affine.simplex.point_index_embedding n = {to_fun := λ (i : fin (n + 1)), affine.simplex.points_with_circumcenter_index.point_index i, inj' := _}

source

theorem affine.simplex.sum_points_with_circumcenter {α : Type u_1} [add_comm_monoid α] {n : ℕ} (f : affine.simplex.points_with_circumcenter_index n → α) :

finset.univ.sum (λ (i : affine.simplex.points_with_circumcenter_index n), f i) = finset.univ.sum (λ (i : fin (n + 1)), f (affine.simplex.points_with_circumcenter_index.point_index i)) + f affine.simplex.points_with_circumcenter_index.circumcenter_index

The sum of a function over points_with_circumcenter_index.

source

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

affine.simplex ℝ P n → affine.simplex.points_with_circumcenter_index n → P

The vertices of a simplex plus its circumcenter.

Equations

source

@[simp]

theorem affine.simplex.points_with_circumcenter_point {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)) :

s.points_with_circumcenter (affine.simplex.points_with_circumcenter_index.point_index i) = s.points i

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

source

@[simp]

theorem affine.simplex.points_with_circumcenter_eq_circumcenter {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) :

s.points_with_circumcenter affine.simplex.points_with_circumcenter_index.circumcenter_index = s.circumcenter

points_with_circumcenter, applied to circumcenter_index, equals the circumcenter.

source

def affine.simplex.point_weights_with_circumcenter {n : ℕ} :

fin (n + 1) → affine.simplex.points_with_circumcenter_index n → ℝ

The weights for a single vertex of a simplex, in terms of points_with_circumcenter.

Equations

source

@[simp]

theorem affine.simplex.sum_point_weights_with_circumcenter {n : ℕ} (i : fin (n + 1)) :

finset.univ.sum (λ (j : affine.simplex.points_with_circumcenter_index n), affine.simplex.point_weights_with_circumcenter i j) = 1

point_weights_with_circumcenter sums to 1.

source

theorem affine.simplex.point_eq_affine_combination_of_points_with_circumcenter {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)) :

s.points i = ⇑(finset.univ.affine_combination s.points_with_circumcenter) (affine.simplex.point_weights_with_circumcenter i)

A single vertex, in terms of points_with_circumcenter.

source

def affine.simplex.centroid_weights_with_circumcenter {n : ℕ} :

finset (fin (n + 1)) → affine.simplex.points_with_circumcenter_index n → ℝ

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

Equations

source

@[simp]

theorem affine.simplex.sum_centroid_weights_with_circumcenter {n : ℕ} {fs : finset (fin (n + 1))} :

fs.nonempty → finset.univ.sum (λ (i : affine.simplex.points_with_circumcenter_index n), affine.simplex.centroid_weights_with_circumcenter fs i) = 1

centroid_weights_with_circumcenter sums to 1, if the finset is nonempty.

source

theorem affine.simplex.centroid_eq_affine_combination_of_points_with_circumcenter {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) (fs : finset (fin (n + 1))) :

finset.centroid ℝ fs s.points = ⇑(finset.univ.affine_combination s.points_with_circumcenter) (affine.simplex.centroid_weights_with_circumcenter fs)

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

source

def affine.simplex.circumcenter_weights_with_circumcenter (n : ℕ) :

affine.simplex.points_with_circumcenter_index n → ℝ

The weights for the circumcenter of a simplex, in terms of points_with_circumcenter.

Equations

source

@[simp]

theorem affine.simplex.sum_circumcenter_weights_with_circumcenter (n : ℕ) :

finset.univ.sum (λ (i : affine.simplex.points_with_circumcenter_index n), affine.simplex.circumcenter_weights_with_circumcenter n i) = 1

circumcenter_weights_with_circumcenter sums to 1.

source

theorem affine.simplex.circumcenter_eq_affine_combination_of_points_with_circumcenter {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) :

s.circumcenter = ⇑(finset.univ.affine_combination s.points_with_circumcenter) (affine.simplex.circumcenter_weights_with_circumcenter n)

The circumcenter of a simplex, in terms of points_with_circumcenter.

mathlib documentation

geometry.euclidean.circumcenter

Circumcenter and circumradius

Main definitions

References

General documentation

Additional documentation

Library

mathlib documentation

geometry.​euclidean.​circumcenter

Circumcenter and circumradius

Main definitions

References

General documentation

Additional documentation

Library

geometry.euclidean.circumcenter