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

• circumcenter and circumradius are the circumcenter and circumradius of a simplex.

References

• https://en.wikipedia.org/wiki/Circumscribed_circle

theorem EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection s.direction] {p1 : P} {p2 : P} (p3 : P) (hp1 : p1 ∈ s) (hp2 : p2 ∈ s) : dist p1 p3 = dist p2 p3 ↔ dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p3) = dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p3)

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

theorem EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection s.direction] {ps : Set P} (hps : ps ⊆ ↑s) (p : P) : (ps.Pairwise fun (p1 p2 : P) => dist p1 p = dist p2 p) ↔ ps.Pairwise fun (p1 p2 : P) => dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p) = dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p)

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

theorem EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection s.direction] {ps : Set P} (hps : ps ⊆ ↑s) (p : P) : (∃ (r : ℝ), ∀ p1 ∈ ps, dist p1 p = r) ↔ ∃ (r : ℝ), ∀ p1 ∈ ps, dist p1 ↑((EuclideanGeometry.orthogonalProjection 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 orthogonalProjection has that distance from all the points in that set.

theorem EuclideanGeometry.existsUnique_dist_eq_of_insert {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [HasOrthogonalProjection s.direction] {ps : Set P} (hnps : ps.Nonempty) {p : P} (hps : ps ⊆ ↑s) (hp : p ∉ s) (hu : ∃! cs : EuclideanGeometry.Sphere P, cs.center ∈ s ∧ ps ⊆ Metric.sphere cs.center cs.radius) : ∃! cs₂ : EuclideanGeometry.Sphere P, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius

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 AffineIndependent.existsUnique_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) : ∃! cs : EuclideanGeometry.Sphere P, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius

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.circumsphere {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : EuclideanGeometry.Sphere P

The circumsphere of a simplex.

Equations

• s.circumsphere = Exists.choose ⋯

theorem Affine.Simplex.circumsphere_unique_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : (s.circumsphere.center ∈ affineSpan ℝ (Set.range s.points) ∧ Set.range s.points ⊆ Metric.sphere s.circumsphere.center s.circumsphere.radius) ∧ ∀ (cs : EuclideanGeometry.Sphere P), cs.center ∈ affineSpan ℝ (Set.range s.points) ∧ Set.range s.points ⊆ Metric.sphere cs.center cs.radius → cs = s.circumsphere

The property satisfied by the circumsphere.

def Affine.Simplex.circumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : P

The circumcenter of a simplex.

Equations

• s.circumcenter = s.circumsphere.center

def Affine.Simplex.circumradius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : ℝ

The circumradius of a simplex.

Equations

• s.circumradius = s.circumsphere.radius

@[simp]

theorem Affine.Simplex.circumsphere_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : s.circumsphere.center = s.circumcenter

The center of the circumsphere is the circumcenter.

@[simp]

theorem Affine.Simplex.circumsphere_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : s.circumsphere.radius = s.circumradius

The radius of the circumsphere is the circumradius.

theorem Affine.Simplex.circumcenter_mem_affineSpan {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : s.circumcenter ∈ affineSpan ℝ (Set.range s.points)

The circumcenter lies in the affine span.

@[simp]

theorem Affine.Simplex.dist_circumcenter_eq_circumradius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)) : dist (s.points i) s.circumcenter = s.circumradius

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

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

All points lie in the circumsphere.

@[simp]

theorem Affine.Simplex.dist_circumcenter_eq_circumradius' {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)) : dist s.circumcenter (s.points i) = s.circumradius

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P} (hp : p ∈ affineSpan ℝ (Set.range s.points)) {r : ℝ} (hr : ∀ (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P} (hp : p ∈ affineSpan ℝ (Set.range s.points)) {r : ℝ} (hr : ∀ (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : 0 ≤ s.circumradius

The circumradius is non-negative.

theorem Affine.Simplex.circumradius_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) : 0 < s.circumradius

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Affine.Simplex ℝ P 0) (i : Fin 1) : s.circumcenter = s.points i

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

theorem Affine.Simplex.circumcenter_eq_centroid {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Affine.Simplex ℝ P 1) : s.circumcenter = Finset.centroid ℝ Finset.univ s.points

The circumcenter of a 1-simplex equals its centroid.

@[simp]

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

Reindexing a simplex along an Equiv of index types does not change the circumsphere.

@[simp]

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

Reindexing a simplex along an Equiv of index types does not change the circumcenter.

@[simp]

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

Reindexing a simplex along an Equiv of index types does not change the circumradius.

def Affine.Simplex.orthogonalProjectionSpan {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : P →ᵃ[ℝ] ↥(affineSpan ℝ (Set.range s.points))

The orthogonal projection of a point p onto the hyperplane spanned by the simplex's points.

Equations

• s.orthogonalProjectionSpan = EuclideanGeometry.orthogonalProjection (affineSpan ℝ (Set.range s.points))

theorem Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p1 : P} (p2 : P) (r : ℝ) (hp : p1 ∈ affineSpan ℝ (Set.range s.points)) : s.orthogonalProjectionSpan (r • (p2 -ᵥ ↑(s.orthogonalProjectionSpan p2)) +ᵥ p1) = ⟨p1, hp⟩

Adding a vector to a point in the given subspace, then taking the orthogonal projection, produces the original point if the vector is a multiple of the result of subtracting a point's orthogonal projection from that point.

theorem Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} {r₁ : ℝ} (s : Affine.Simplex ℝ P n) {p : P} {p₁o : P} (hp₁o : p₁o ∈ affineSpan ℝ (Set.range s.points)) : ↑(s.orthogonalProjectionSpan (r₁ • (p -ᵥ ↑(s.orthogonalProjectionSpan p)) +ᵥ p₁o)) = p₁o

theorem Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p1 : P} (p2 : P) (hp1 : p1 ∈ affineSpan ℝ (Set.range s.points)) : dist p1 p2 * dist p1 p2 = dist p1 ↑(s.orthogonalProjectionSpan p2) * dist p1 ↑(s.orthogonalProjectionSpan p2) + dist p2 ↑(s.orthogonalProjectionSpan p2) * dist p2 ↑(s.orthogonalProjectionSpan p2)

theorem Affine.Simplex.dist_circumcenter_sq_eq_sq_sub_circumradius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} {r : ℝ} (s : Affine.Simplex ℝ P n) {p₁ : P} (h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r) (h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter) (h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)) : dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius

theorem Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P} (hr : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), dist (s.points i) p = r) : ↑(s.orthogonalProjectionSpan p) = s.circumcenter

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.

theorem Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P} {r : ℝ} (hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r) : ↑(s.orthogonalProjectionSpan p) = s.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.

theorem Affine.Simplex.orthogonalProjection_circumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) : ↑((s.face h).orthogonalProjectionSpan s.circumcenter) = (s.face h).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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} {s₁ : Affine.Simplex ℝ P n} {s₂ : Affine.Simplex ℝ P n} (h : Set.range s₁.points = Set.range s₂.points) : s₁.circumcenter = s₂.circumcenter

Two simplices with the same points have the same circumcenter.

inductive Affine.Simplex.PointsWithCircumcenterIndex (n : ℕ) : Type

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

• pointIndex: {n : ℕ} → Fin (n + 1) → Affine.Simplex.PointsWithCircumcenterIndex n
• circumcenterIndex: {n : ℕ} → Affine.Simplex.PointsWithCircumcenterIndex n

instance Affine.Simplex.instFintypePointsWithCircumcenterIndex : {n : ℕ} → Fintype (Affine.Simplex.PointsWithCircumcenterIndex n)

Equations

• Affine.Simplex.instFintypePointsWithCircumcenterIndex = Fintype.ofEquiv (Fin (n + 1) ⊕ Unit) (Affine.Simplex.PointsWithCircumcenterIndex.proxyTypeEquiv n)

instance Affine.Simplex.pointsWithCircumcenterIndexInhabited (n : ℕ) : Inhabited (Affine.Simplex.PointsWithCircumcenterIndex n)

Equations

• Affine.Simplex.pointsWithCircumcenterIndexInhabited n = { default := Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex }

def Affine.Simplex.pointIndexEmbedding (n : ℕ) : Fin (n + 1) ↪ Affine.Simplex.PointsWithCircumcenterIndex n

pointIndex as an embedding.

Equations

• Affine.Simplex.pointIndexEmbedding n = { toFun := fun (i : Fin (n + 1)) => Affine.Simplex.PointsWithCircumcenterIndex.pointIndex i, inj' := ⋯ }

theorem Affine.Simplex.sum_pointsWithCircumcenter {α : Type u_3} [AddCommMonoid α] {n : ℕ} (f : Affine.Simplex.PointsWithCircumcenterIndex n → α) : (Finset.univ.sum fun (i : Affine.Simplex.PointsWithCircumcenterIndex n) => f i) = (Finset.univ.sum fun (i : Fin (n + 1)) => f (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex i)) + f Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex

The sum of a function over PointsWithCircumcenterIndex.

def Affine.Simplex.pointsWithCircumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : Affine.Simplex.PointsWithCircumcenterIndex n → P

The vertices of a simplex plus its circumcenter.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Affine.Simplex.pointsWithCircumcenter_point {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)) : s.pointsWithCircumcenter (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex i) = s.points i

pointsWithCircumcenter, applied to a pointIndex value, equals points applied to that value.

@[simp]

theorem Affine.Simplex.pointsWithCircumcenter_eq_circumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : s.pointsWithCircumcenter Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex = s.circumcenter

pointsWithCircumcenter, applied to circumcenterIndex, equals the circumcenter.

def Affine.Simplex.pointWeightsWithCircumcenter {n : ℕ} (i : Fin (n + 1)) : Affine.Simplex.PointsWithCircumcenterIndex n → ℝ

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Affine.Simplex.sum_pointWeightsWithCircumcenter {n : ℕ} (i : Fin (n + 1)) : (Finset.univ.sum fun (j : Affine.Simplex.PointsWithCircumcenterIndex n) => Affine.Simplex.pointWeightsWithCircumcenter i j) = 1

point_weights_with_circumcenter sums to 1.

theorem Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)) : s.points i = (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter) (Affine.Simplex.pointWeightsWithCircumcenter i)

A single vertex, in terms of pointsWithCircumcenter.

def Affine.Simplex.centroidWeightsWithCircumcenter {n : ℕ} (fs : Finset (Fin (n + 1))) : Affine.Simplex.PointsWithCircumcenterIndex n → ℝ

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Affine.Simplex.sum_centroidWeightsWithCircumcenter {n : ℕ} {fs : Finset (Fin (n + 1))} (h : fs.Nonempty) : (Finset.univ.sum fun (i : Affine.Simplex.PointsWithCircumcenterIndex n) => Affine.Simplex.centroidWeightsWithCircumcenter fs i) = 1

centroidWeightsWithCircumcenter sums to 1, if the Finset is nonempty.

theorem Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (fs : Finset (Fin (n + 1))) : Finset.centroid ℝ fs s.points = (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter) (Affine.Simplex.centroidWeightsWithCircumcenter fs)

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

def Affine.Simplex.circumcenterWeightsWithCircumcenter (n : ℕ) : Affine.Simplex.PointsWithCircumcenterIndex n → ℝ

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Affine.Simplex.sum_circumcenterWeightsWithCircumcenter (n : ℕ) : (Finset.univ.sum fun (i : Affine.Simplex.PointsWithCircumcenterIndex n) => Affine.Simplex.circumcenterWeightsWithCircumcenter n i) = 1

circumcenterWeightsWithCircumcenter sums to 1.

theorem Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : s.circumcenter = (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter) (Affine.Simplex.circumcenterWeightsWithCircumcenter n)

The circumcenter of a simplex, in terms of pointsWithCircumcenter.

def Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter {n : ℕ} (i₁ : Fin (n + 1)) (i₂ : Fin (n + 1)) : Affine.Simplex.PointsWithCircumcenterIndex n → ℝ

The weights for the reflection of the circumcenter in an edge of a simplex. This definition is only valid with i₁ ≠ i₂.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Affine.Simplex.sum_reflectionCircumcenterWeightsWithCircumcenter {n : ℕ} {i₁ : Fin (n + 1)} {i₂ : Fin (n + 1)} (h : i₁ ≠ i₂) : (Finset.univ.sum fun (i : Affine.Simplex.PointsWithCircumcenterIndex n) => Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i) = 1

reflectionCircumcenterWeightsWithCircumcenter sums to 1.

theorem Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {i₁ : Fin (n + 1)} {i₂ : Fin (n + 1)} (h : i₁ ≠ i₂) : (EuclideanGeometry.reflection (affineSpan ℝ (s.points '' {i₁, i₂}))) s.circumcenter = (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter) (Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)

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

theorem EuclideanGeometry.cospherical_iff_exists_mem_of_complete {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ ↑s) [Nonempty ↥s] [HasOrthogonalProjection s.direction] : EuclideanGeometry.Cospherical ps ↔ ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist 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 EuclideanGeometry.cospherical_iff_exists_mem_of_finiteDimensional {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ ↑s) [Nonempty ↥s] [FiniteDimensional ℝ ↥s.direction] : EuclideanGeometry.Cospherical ps ↔ ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist 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.

theorem EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ ↑s) [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction] (hd : FiniteDimensional.finrank ℝ ↥s.direction = n) (hc : EuclideanGeometry.Cospherical ps) : ∃ (r : ℝ), ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r

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

theorem EuclideanGeometry.circumradius_eq_of_cospherical_subset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ ↑s) [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction] (hd : FiniteDimensional.finrank ℝ ↥s.direction = n) (hc : EuclideanGeometry.Cospherical ps) {sx₁ : Affine.Simplex ℝ P n} {sx₂ : Affine.Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps) (hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumradius = sx₂.circumradius

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

theorem EuclideanGeometry.exists_circumradius_eq_of_cospherical {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : FiniteDimensional.finrank ℝ V = n) (hc : EuclideanGeometry.Cospherical ps) : ∃ (r : ℝ), ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r

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

theorem EuclideanGeometry.circumradius_eq_of_cospherical {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : FiniteDimensional.finrank ℝ V = n) (hc : EuclideanGeometry.Cospherical ps) {sx₁ : Affine.Simplex ℝ P n} {sx₂ : Affine.Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps) (hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumradius = sx₂.circumradius

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

theorem EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ ↑s) [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction] (hd : FiniteDimensional.finrank ℝ ↥s.direction = n) (hc : EuclideanGeometry.Cospherical ps) : ∃ (c : P), ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

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

theorem EuclideanGeometry.circumcenter_eq_of_cospherical_subset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ ↑s) [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction] (hd : FiniteDimensional.finrank ℝ ↥s.direction = n) (hc : EuclideanGeometry.Cospherical ps) {sx₁ : Affine.Simplex ℝ P n} {sx₂ : Affine.Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps) (hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumcenter = sx₂.circumcenter

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

theorem EuclideanGeometry.exists_circumcenter_eq_of_cospherical {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : FiniteDimensional.finrank ℝ V = n) (hc : EuclideanGeometry.Cospherical ps) : ∃ (c : P), ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

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

theorem EuclideanGeometry.circumcenter_eq_of_cospherical {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : FiniteDimensional.finrank ℝ V = n) (hc : EuclideanGeometry.Cospherical ps) {sx₁ : Affine.Simplex ℝ P n} {sx₂ : Affine.Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps) (hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumcenter = sx₂.circumcenter

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

theorem EuclideanGeometry.exists_circumsphere_eq_of_cospherical_subset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ ↑s) [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction] (hd : FiniteDimensional.finrank ℝ ↥s.direction = n) (hc : EuclideanGeometry.Cospherical ps) : ∃ (c : EuclideanGeometry.Sphere P), ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

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

theorem EuclideanGeometry.circumsphere_eq_of_cospherical_subset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ ↑s) [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction] (hd : FiniteDimensional.finrank ℝ ↥s.direction = n) (hc : EuclideanGeometry.Cospherical ps) {sx₁ : Affine.Simplex ℝ P n} {sx₂ : Affine.Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps) (hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumsphere = sx₂.circumsphere

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

theorem EuclideanGeometry.exists_circumsphere_eq_of_cospherical {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : FiniteDimensional.finrank ℝ V = n) (hc : EuclideanGeometry.Cospherical ps) : ∃ (c : EuclideanGeometry.Sphere P), ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

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

theorem EuclideanGeometry.circumsphere_eq_of_cospherical {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : FiniteDimensional.finrank ℝ V = n) (hc : EuclideanGeometry.Cospherical ps) {sx₁ : Affine.Simplex ℝ P n} {sx₂ : Affine.Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps) (hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumsphere = sx₂.circumsphere

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

theorem EuclideanGeometry.eq_or_eq_reflection_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} {s : Affine.Simplex ℝ P n} {p : P} {p₁ : P} {p₂ : P} {r : ℝ} (hp₁ : p₁ ∈ affineSpan ℝ (insert p (Set.range s.points))) (hp₂ : p₂ ∈ affineSpan ℝ (insert p (Set.range s.points))) (h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r) (h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r) : p₁ = p₂ ∨ p₁ = (EuclideanGeometry.reflection (affineSpan ℝ (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.