Affine.Simplex.sum_pointWeightsWithCircumcenter
theorem Affine.Simplex.sum_pointWeightsWithCircumcenter :
∀ {n : ℕ} (i : Fin (n + 1)), (Finset.univ.sum fun j => Affine.Simplex.pointWeightsWithCircumcenter i j) = 1 := by
sorry
The theorem `Affine.Simplex.sum_pointWeightsWithCircumcenter` states that for any natural number `n` and for any `i` in the finite set `Fin (n + 1)`, the sum of the weights of points in a simplex (including its circumcenter), as given by the `Affine.Simplex.pointWeightsWithCircumcenter` function, over every `j` in the universal set `Finset.univ` (which includes all elements of the considered type, due to the `Fintype α` assumption), equals 1. Essentially, this is asserting that the weights of all points in the simplex (including its circumcenter) always sum up to 1.
More concisely: For any simplex of dimension `n`, the weights of all its points (including the circumcenter) sum up to 1.
|
Affine.Simplex.sum_reflectionCircumcenterWeightsWithCircumcenter
theorem Affine.Simplex.sum_reflectionCircumcenterWeightsWithCircumcenter :
∀ {n : ℕ} {i₁ i₂ : Fin (n + 1)},
i₁ ≠ i₂ → (Finset.univ.sum fun i => Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i) = 1
This theorem states that for any natural number `n` and any two distinct elements `i₁` and `i₂` of the finite set `Fin (n + 1)`, the sum of the weights of the reflection of the circumcenter in an edge of a simplex (as defined by the function `Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter`), taken over all elements of the universal finite set (as defined by `Finset.univ`), is equal to 1. In mathematical terms, for distinct `i₁` and `i₂` in the finite set, we have $\sum_{i \in \text{Finset.univ}} \text{Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter}(i₁, i₂, i) = 1$.
More concisely: For any distinct indices `i₁` and `i₂` in a finite set, the sum of the reflection circumcenter weights (as defined by `Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter)` over all indices in the universal finite set is equal to 1.
|
Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter
theorem Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : 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 theorem `Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter` states that the centroid of some vertices of a simplex, in the context of points with a circumcenter, is equivalent to an affine combination of the points of the simplex with the circumcenter. Here, the centroid is calculated with respect to the real number field ℝ. The simplex is defined in real-number space ℝ, in a normed additively commutative group V, an inner product space over ℝ, a metric space P, and a normed additive torsor over P. The simplex has a finite set of vertices represented by `Finset (Fin (n + 1))`, where `n` is the dimension of the simplex. The theorem holds for all these conditions.
More concisely: The centroid of a simplex in a real normed additive torsor with finite vertices is equal to an affine combination of the vertices with their circumcenter.
|
EuclideanGeometry.cospherical_iff_exists_mem_of_finiteDimensional
theorem EuclideanGeometry.cospherical_iff_exists_mem_of_finiteDimensional :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
ps ⊆ ↑s →
∀ [inst_4 : Nonempty ↥s] [inst_5 : FiniteDimensional ℝ ↥s.direction],
EuclideanGeometry.Cospherical ps ↔ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius
This theorem, named `EuclideanGeometry.cospherical_iff_exists_mem_of_finiteDimensional`, states the following:
Given a nonempty affine subspace, where the direction of the subspace is finite-dimensional and it contains a set of points, those points are cospherical (i.e., they are all equidistant from some point) if and only if there exists a point in the subspace from which all those points are equidistant. Here, the distance between any point from the set of points and the 'center' point is the same and is called the 'radius'.
In more technical terms, this theorem is applicable for a real inner product space over a normed add commutative group. The affine subspace and the set of points are within a metric space, with the affine subspace being a torsor under the normed add commutative group. The theorem basically connects the cospherical property of a set of points with their equidistant nature from a particular point in the given affine subspace.
More concisely: A nonempty finite-dimensional affine subspace of a real inner product space contains cospherical points if and only if there exists a point in the subspace such that all points in the subspace are equidistant from it.
|
EuclideanGeometry.exists_circumradius_eq_of_cospherical
theorem EuclideanGeometry.exists_circumradius_eq_of_cospherical :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [inst_4 : FiniteDimensional ℝ V],
FiniteDimensional.finrank ℝ V = n →
EuclideanGeometry.Cospherical ps →
∃ r, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
This theorem states that in an n-dimensional space, if a set of points are cospherical (meaning they are equidistant from some point), then all n-simplices (a generalization of triangles and tetrahedra to n dimensions) constructed from these points have the same circumradius. More formally, given a real inner product space and a set of cospherical points in this space, if the finite dimension of the space is equal to n, then there exists a radius such that for every n-simplex built from these points, the circumradius of the simplex is equal to this radius.
More concisely: In an n-dimensional real inner product space, if a set of points is cospherical, then all n-simplices formed by these points have the same circumradius.
|
Affine.Simplex.sum_circumcenterWeightsWithCircumcenter
theorem Affine.Simplex.sum_circumcenterWeightsWithCircumcenter :
∀ (n : ℕ), (Finset.univ.sum fun i => Affine.Simplex.circumcenterWeightsWithCircumcenter n i) = 1
The theorem `Affine.Simplex.sum_circumcenterWeightsWithCircumcenter` states that for any natural number `n`, the sum of the weights for the circumcenter of an `n`-simplex (where the weights are given by the function `Affine.Simplex.circumcenterWeightsWithCircumcenter` for each point in the universal finite set of type `Finset α`) is always equal to 1. The weights are either 0 for the points of the simplex or 1 for the circumcenter itself. This is essentially a normalization condition for the weights.
More concisely: The sum of the weights given by `Affine.Simplex.circumcenterWeightsWithCircumcenter` for all points of an `n`-simplex, including the circumcenter, is equal to 1.
|
AffineIndependent.existsUnique_dist_eq
theorem AffineIndependent.existsUnique_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {ι : Type u_3} [hne : Nonempty ι] [inst_4 : Finite ι]
{p : ι → P},
AffineIndependent ℝ p →
∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
This theorem states that given a finite nonempty set of points which are affinely independent, there exists a unique pair of circumcenter and circumradius for those points in the affine subspace they span. In other words, this theorem ensures the uniqueness of the circumcircle (defined by a center and a radius) for a given set of points in any finite, nonempty, affinely independent family. The circumcenter belongs to the affine span of the set of points, and all the points lie on the sphere or circle defined by the circumcenter and the circumradius.
More concisely: Given a finite, nonempty, affinely independent set of points in an affine space, there exists a unique circumcenter and circumradius such that all points lie on the circumcircle defined by this center and radius.
|
EuclideanGeometry.circumsphere_eq_of_cospherical_subset
theorem EuclideanGeometry.circumsphere_eq_of_cospherical_subset :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
ps ⊆ ↑s →
∀ [inst_4 : Nonempty ↥s] {n : ℕ} [inst_5 : FiniteDimensional ℝ ↥s.direction],
FiniteDimensional.finrank ℝ ↥s.direction = n →
EuclideanGeometry.Cospherical ps →
∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumsphere = sx₂.circumsphere
The theorem `EuclideanGeometry.circumsphere_eq_of_cospherical_subset` states that in a real-valued, n-dimensional subspace, if a set of points are all equidistant from a common center (cospherical), then any two n-dimensional simplices (generalizations of triangles) whose vertices are within this set of points will share the same circumsphere. In other words, the smallest sphere encompassing all vertices of these simplices will be the same for both. This is under the condition that the subspace's dimension is also n, indicated by `FiniteDimensional.finrank ℝ ↥s.direction = n`.
More concisely: In an n-dimensional real subspace, if a set of points is cospherical, then any two n-dimensional simplices with vertices in the set have the same circumsphere.
|
Affine.Simplex.circumcenter_reindex
theorem Affine.Simplex.circumcenter_reindex :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {m n : ℕ} (s : Affine.Simplex ℝ P m)
(e : Fin (m + 1) ≃ Fin (n + 1)), (s.reindex e).circumcenter = s.circumcenter
This theorem states that the circumcenter of a simplex, which is a geometric object in an affine space, remains unchanged if we reindex the simplex along an equivalence (`Equiv`) of index types. Specifically, for any given simplex `s` and equivalence `e`, the circumcenter of the reindexed simplex `(s.reindex e)` is equal to the circumcenter of the original simplex `s`. This holds true for any normed additively commutative group `V`, any inner product space over the reals constructed from `V`, any metric space `P`, and any normed additive torsor over `V` and `P`. The index types of the simplex `s` and the equivalence `e` are `Fin (m + 1)` and `Fin (n + 1)` respectively, where `m` and `n` are nonnegative integers.
More concisely: The circumcenter of a simplex is unchanged under reindexing by an equivalence of finite index types.
|
Affine.Simplex.circumcenter_eq_point
theorem Affine.Simplex.circumcenter_eq_point :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : Affine.Simplex ℝ P 0) (i : Fin 1),
s.circumcenter = s.points i
This theorem states that the circumcenter of a 0-simplex is equivalent to its single unique point. In the context of mathematical geometry, a 0-simplex is a point in a geometric space. The circumcenter is the center of the circumscribing circle that touches all the vertices of a shape. In this case, since a 0-simplex has only one vertex, the circumcenter is that same point. The theorem is universally quantified over the vector type `V`, point type `P`, normed additive commutative group `V`, inner product space over real numbers and `V`, metric space `P`, and normed additive torsor over `V` and `P`. The simplex is defined over the real numbers and point type `P`, and the index `i` is a finite number of size 1.
More concisely: The circumcenter of a 0-simplex (a point) is equivalent to that point itself.
|
EuclideanGeometry.circumcenter_eq_of_cospherical
theorem EuclideanGeometry.circumcenter_eq_of_cospherical :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [inst_4 : FiniteDimensional ℝ V],
FiniteDimensional.finrank ℝ V = n →
EuclideanGeometry.Cospherical ps →
∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumcenter = sx₂.circumcenter
This theorem states that in an n-dimensional space, if a set of points is cospherical, then any two n-simplices (generalizations of triangles to n dimensions) formed from this set of points will have the same circumcenter. This is under the condition that the dimension of the underlying vector space, which is a finite dimensional vector space over the real numbers, is equal to `n`. In simpler terms, if a collection of points in space are all equidistant from a certain point, the "center" of any two n-dimensional "triangles" formed from these points will be the same, provided the dimension of the space is `n`.
More concisely: In an n-dimensional real vector space, if a set of points is cospherical, then any two n-simplices formed by these points have the same circumcenter.
|
Affine.Simplex.circumradius_reindex
theorem Affine.Simplex.circumradius_reindex :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {m n : ℕ} (s : Affine.Simplex ℝ P m)
(e : Fin (m + 1) ≃ Fin (n + 1)), (s.reindex e).circumradius = s.circumradius
This theorem states that reindexing a simplex (a generalization of a triangle to arbitrary dimensions) along an equivalence (or "Equiv") of index types does not change the circumradius. The equivalence is between the finite sets `Fin (m + 1)` and `Fin (n + 1)`. Here, `m` and `n` are the dimensions of the original and reindexed simplexes respectively, `V` is a normed add commutative group, `P` is a metric space, and `P` is a normed add torsor over `V`, with the required assumptions that `V` is an inner product space over the real numbers and `P` is a metric space. The circumradius remains the same regardless of how the vertices of the simplex are relabeled.
More concisely: The circumradius of a simplex in an inner product space over the real numbers, metric space, or normed add torsor remains unchanged when reindexing its vertices through an equivalence between their index types.
|
Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq
theorem Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P},
(∃ r, ∀ (i : Fin (n + 1)), dist (s.points i) p = r) → ↑(s.orthogonalProjectionSpan p) = s.circumcenter
The theorem states that for a given point in space, if there is a specific distance that the point has from all vertices of a simplex, then the orthogonal projection of that point onto the subspace spanned by the simplex equals the circumcenter of the simplex. Here a simplex is a generalization of a triangle to n-dimensions, an orthogonal projection is a type of projection that drops a perpendicular from the point to the subspace, and a circumcenter is the center of a circumsphere that encloses all vertices of the simplex. The theorem holds in a normed add torsor over an inner product space and a metric space.
More concisely: For a given point in an n-dimensional normed add torsor over an inner product space and a metric space, if the point has the same distance to all vertices of a simplex, then its orthogonal projection onto the simplex's subspace equals the circumcenter of the simplex.
|
Affine.Simplex.circumcenter_eq_centroid
theorem Affine.Simplex.circumcenter_eq_centroid :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : Affine.Simplex ℝ P 1),
s.circumcenter = Finset.centroid ℝ Finset.univ s.points
This theorem states that the circumcenter of a 1-simplex is equal to its centroid. In more detail, for any 1-simplex `s` with the underlying Real number field and types `V` and `P` satisfying the conditions of a Normed Additive Commutative Group, an Inner Product Space, a Metric Space and a Normed Additive Torsor, the circumcenter of `s` is equal to the centroid of the set of all points in `s`. Here, a 1-simplex refers to the simplest type of simplex, a line segment. The centroid is the arithmetic mean position of all the points in the shape, and the circumcenter is the center of the circle defined by the simplex.
More concisely: The circumcenter and centroid of a 1-simplex in a normed additive commutative group with inner product space, metric space, and normed additive torsor properties are equal.
|
Affine.Simplex.circumcenter_eq_of_range_eq
theorem Affine.Simplex.circumcenter_eq_of_range_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} {s₁ s₂ : Affine.Simplex ℝ P n},
Set.range s₁.points = Set.range s₂.points → s₁.circumcenter = s₂.circumcenter
The theorem `Affine.Simplex.circumcenter_eq_of_range_eq` states that for any two simplices `s₁` and `s₂` in an affine space over the reals, with underlying normed additively commutative group `V`, inner product space over the reals, Metric space `P` and a normed additively commutative group with a torsor structure `V` acting on `P`, if the set of points defining `s₁` is the same as the set of points defining `s₂` (i.e., `Set.range s₁.points = Set.range s₂.points`), then the circumcenters of `s₁` and `s₂` are also the same (i.e., `s₁.circumcenter = s₂.circumcenter`).
In simpler terms, this theorem asserts that two geometric shapes (simplices) having the same set of vertices will also have the same circumcenter.
More concisely: If two simplices in an affine space with the same set of vertices have identical point ranges, then they have equal circumcenters.
|
Affine.Simplex.circumsphere_radius
theorem Affine.Simplex.circumsphere_radius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
s.circumsphere.radius = s.circumradius
The theorem `Affine.Simplex.circumsphere_radius` states that for any simplex `s` in a real affine space, the radius of the circumsphere of `s` is equal to the circumradius of `s`. The simplex `s` can be of any dimension `n`, and the space in which it lives, denoted by `P`, is endowed with a metric. The vector space `V` associated with `P` is assumed to be a normed additively commutative group and an inner product space over the real numbers.
More concisely: The radius of the circumsphere of a simplex in a real affine space endowed with a metric, whose associated vector space is a normed additively commutative group and inner product space over the real numbers, equals the circumradius of the simplex.
|
EuclideanGeometry.exists_circumcenter_eq_of_cospherical
theorem EuclideanGeometry.exists_circumcenter_eq_of_cospherical :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [inst_4 : FiniteDimensional ℝ V],
FiniteDimensional.finrank ℝ V = n →
EuclideanGeometry.Cospherical ps →
∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
This theorem states that in an n-dimensional Euclidean space, if a set of points is cospherical, then all n-simplices (n-dimensional generalization of a triangle) formed from these points have the same circumcenter. More technically, for a given normed add commutative group `V` and metric space `P` which is a normed add torsor over `V`, a set `ps` of points in `P`, and a natural number `n` such that the space `V` is finite-dimensional with dimension `n`, if `ps` is cospherical, then there exists a point `c` that is the circumcenter for every n-simplex whose vertices are all in `ps`.
More concisely: In an n-dimensional Euclidean space, if a set of points is cospherical, then all n-simplices formed from these points have the same circumcenter.
|
Affine.Simplex.sum_centroidWeightsWithCircumcenter
theorem Affine.Simplex.sum_centroidWeightsWithCircumcenter :
∀ {n : ℕ} {fs : Finset (Fin (n + 1))},
fs.Nonempty → (Finset.univ.sum fun i => Affine.Simplex.centroidWeightsWithCircumcenter fs i) = 1
The theorem `Affine.Simplex.sum_centroidWeightsWithCircumcenter` states that for any natural number `n` and for any non-empty finite set `fs` of elements of type `Fin (n + 1)`, the sum of the centroid weights with circumcenter, over all elements in the universal finite set (`Finset.univ`), equals 1. In other words, when considering a simplex (a generalization of a triangle to any dimension) with `n + 1` vertices, the weights assigned to each vertex, which are used to calculate the centroid (a kind of center) of a non-empty subset of these vertices, add up to 1 when summed over the entire set of possible vertices and their circumcenter (a point equidistant from all vertices).
More concisely: For any natural number `n` and finite set `fs` of `n+1` elements, the sum of centroid weights with circumcenter over all `Fin (n+1)` equals 1.
|
EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset
theorem EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
ps ⊆ ↑s →
∀ [inst_4 : Nonempty ↥s] {n : ℕ} [inst_5 : FiniteDimensional ℝ ↥s.direction],
FiniteDimensional.finrank ℝ ↥s.direction = n →
EuclideanGeometry.Cospherical ps →
∃ r, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
The theorem `EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset` states that for a set of points `ps` in an n-dimensional subspace `s`, if these points are cospherical (equidistant from some point), then all n-simplices (a simplex is a generalization of a triangle to n-dimensions) created from points in `ps` have the same circumradius. In other words, all these simplices fit in a sphere of the same radius. The theorem assumes that the set `ps` is in the subspace `s`, the subspace `s` is nonempty, and the dimension of the subspace (as a vector space) is `n`.
More concisely: Given a nonempty n-dimensional subspace s in a Euclidean space and a set of n+1 points in s that are equidistant from a point, all n-simplices formed by these points have the same circumradius.
|
Affine.Simplex.pointsWithCircumcenter_point
theorem Affine.Simplex.pointsWithCircumcenter_point :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
s.pointsWithCircumcenter (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex i) = s.points i
This theorem, `Affine.Simplex.pointsWithCircumcenter_point`, states that for any given affine simplex `s`, the function `pointsWithCircumcenter` applied to a `pointIndex` value equals the function `points` applied to that value. This is true for all spaces `V` and `P` where `V` is a Normed Additive Commutative Group, `P` is a Metric Space, `V` is an Inner Product Space over the real numbers, and `V` is a Normed Additive Torsor over `P`. The `pointIndex` is a value in the finite set `{0, 1, ..., n}` where `n` is the dimension of the simplex.
More concisely: For any affine simplex in a Normed Additive Commutative Group V, a Metric Space P, an Inner Product Space over the real numbers V, and a Normed Additive Torsor over P, the function `pointsWithCircumcenter` and `points` applied to a point index in {0, 1, ..., n} yield the same result.
|
Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter
theorem Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : 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)
This theorem states that for any real-valued affine simplex `s` in a metric space defined over a normed add torsor and an inner product space, the points of the simplex can be expressed as an affine combination of the points associated with the circumcenter. The weights for this affine combination are determined by the function `Affine.Simplex.pointWeightsWithCircumcenter`, which assigns 1 to each point indexed by `i` and 0 to the circumcenter.
More concisely: For any real-valued affine simplex in a metric space over a normed add torsor and an inner product space, its points can be represented as an affine combination of the circumcenter's points with weights given by `Affine.Simplex.pointWeightsWithCircumcenter`.
|
EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq
theorem EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {ps : Set P},
ps ⊆ ↑s →
∀ (p : P),
(∃ r, ∀ p1 ∈ ps, dist p1 p = r) ↔
∃ r, ∀ p1 ∈ ps, dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p) = r
The theorem states that for any normed add commutative group `V`, inner product space over the reals `V`, metric space `P`, and a normed add torsor `V` over `P`, given an affine subspace `s` of `P` over the reals with nonempty carrier set, and that has an orthogonal projection defined on its direction, and a set `ps` of points in `P` that is a subset of `s`, for any point `p` in `P`, there exists a real number `r` such that the distance between `p` and all points in `ps` equals `r` if and only if there exists a possibly different real number `r` such that the distance between the orthogonal projection of `p` onto `s` and every point in `ps` equals `r`.
More concisely: For any normed add commutative group `V` over the reals, inner product space `V`, metric space `P`, and normed add torsor `V` over `P`, if an affine subspace `s` of `P` with nonempty carrier set and orthogonal projection has a set `ps` of points such that the distance from any point `p` in `P` to `ps` equals the distance from the orthogonal projection of `p` to `s` to every point in `ps`, then these distances are equal to the same real number.
|
Affine.Simplex.dist_circumcenter_eq_circumradius
theorem Affine.Simplex.dist_circumcenter_eq_circumradius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
dist (s.points i) s.circumcenter = s.circumradius
The theorem `Affine.Simplex.dist_circumcenter_eq_circumradius` states that for any simplex `s` in a real inner product space, the distance between any of its points and the circumcenter of the simplex is equal to the circumradius of the simplex. In other words, all points of the simplex are located on the circumsphere defined by the simplex's circumcenter and circumradius.
More concisely: The circumradius of a simplex in a real inner product space is equal to the distance from any of its points to the circumcenter.
|
EuclideanGeometry.existsUnique_dist_eq_of_insert
theorem EuclideanGeometry.existsUnique_dist_eq_of_insert :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P}
[inst_4 : HasOrthogonalProjection s.direction] {ps : Set P},
ps.Nonempty →
∀ {p : P},
ps ⊆ ↑s →
p ∉ s →
(∃! cs, cs.center ∈ s ∧ ps ⊆ Metric.sphere cs.center cs.radius) →
∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
This theorem, named `EuclideanGeometry.existsUnique_dist_eq_of_insert`, states that for a given nonempty set of points within a nonempty affine subspace that is complete in direction, if there exists a unique pair of a circumcenter and a circumradius for those points within that subspace, and there is an additional point that is not within that subspace, then there exists a unique pair of a circumcenter and a circumradius for the set with the additional point added, in the span of the subspace with the additional point added.
More specifically, the theorem asserts that for a given point `p` outside of the subspace `s`, if the points in the set `ps` have a unique circumcenter and circumradius within the subspace `s`, then the union of the set `ps` and the point `p` will have a unique circumcenter and circumradius in the affine span of `s` and `p`. This circumcenter lies in the affine span of `s` and `p`, and the union of `ps` and `p` is contained within the sphere with the said circumcenter and circumradius.
More concisely: Given a nonempty set of points in a complete subspace of Euclidean geometry with unique circumcenter and circumradius, adding a point outside the subspace results in a new set with unique circumcenter and circumradius in the span of the original set and the new point.
|
EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq
theorem EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {ps : Set P},
ps ⊆ ↑s →
∀ (p : P),
(ps.Pairwise fun p1 p2 => dist p1 p = dist p2 p) ↔
ps.Pairwise fun p1 p2 =>
dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p) =
dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p)
The theorem states that for any normed additive commutative group `V`, inner product space `V` over real numbers `ℝ`, metric space `P`, and normed additive torsor `P` relative to `V`, given an affine subspace `s` of `P` over `ℝ` that is nonempty and has an orthogonal projection, and a set `ps` of points in `P` that is contained within `s`, a point `p` in `P` has the same distance from every point in the set `ps` if and only if the orthogonal projection of `p` onto the subspace `s` has the same distance from every point in the set `ps`. In other words, a point is equidistant from a set of points if and only if its orthogonal projection onto a given subspace is also equidistant from those points.
More concisely: For any normed additive commutative group `V`, inner product space `V` over real numbers `ℝ`, metric space `P`, and normed additive torsor `P` relative to `V`, a point `p` in `P` is equidistant from a set `ps` of points in an affine subspace `s` of `P` over `ℝ` with orthogonal projection, if and only if the orthogonal projection of `p` onto `s` has the same distance from every point in `ps`.
|
Affine.Simplex.circumsphere_center
theorem Affine.Simplex.circumsphere_center :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
s.circumsphere.center = s.circumcenter
This theorem states that for any simplex in an affine space - where the space supports operations like addition, subtraction, and scalar multiplication and is equipped with a metric to measure distances, and where the vectors in the space form a normed group with an inner product - the center of the circumsphere of the simplex is the same as the circumcenter of the simplex. Here, a circumsphere of a simplex is a sphere that passes through all the vertices of the simplex, and the circumcenter is the center of this circumsphere.
More concisely: For any simplex in an affine space with a normed group structure and inner product, the center of its circumsphere equals the circumcenter.
|
Affine.Simplex.orthogonalProjection_circumcenter
theorem Affine.Simplex.orthogonalProjection_circumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : 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
This theorem states that for any affine simplex, the orthogonal projection of the circumcenter of the simplex onto any face of the simplex is equal to the circumcenter of that face. Here, a simplex is a generalization of a triangle to n dimensions, a circumcenter is the center of the circumscribed circle (or sphere, or hypersphere in higher dimensions) of the simplex, and an orthogonal projection is a projection of a point onto a subspace such that the line from the point to its projection is perpendicular to the subspace. The theorem is valid in any metric space and inner product space.
More concisely: For any affine simplex in a metric or inner product space, the orthogonal projection of its circumcenter onto any face is equivalent to the circumcenter of that face.
|
Affine.Simplex.sum_pointsWithCircumcenter
theorem Affine.Simplex.sum_pointsWithCircumcenter :
∀ {α : Type u_3} [inst : AddCommMonoid α] {n : ℕ} (f : Affine.Simplex.PointsWithCircumcenterIndex n → α),
(Finset.univ.sum fun i => f i) =
(Finset.univ.sum fun i => f (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex i)) +
f Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex
This theorem states that for any type `α` that forms an additive commutative monoid, any natural number `n`, and any function `f` that maps points with a circumcenter index in an n-dimensional simplex to `α`, the sum of the function over all points can be expressed as the sum of the function over only the points, plus the function evaluated at the circumcenter index. The sets of points and the circumcenter index are considered as universal finite sets or `Finset.univ`, which are implied by the assumption `Fintype α`.
More concisely: For any additive commutative monoid type `α`, function `f` mapping points of a finite simplex to `α`, and natural number `n`, the sum of `f` over all points in a simplex equals the sum over points plus `f` evaluated at the circumcenter index.
|
EuclideanGeometry.circumsphere_eq_of_cospherical
theorem EuclideanGeometry.circumsphere_eq_of_cospherical :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [inst_4 : FiniteDimensional ℝ V],
FiniteDimensional.finrank ℝ V = n →
EuclideanGeometry.Cospherical ps →
∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumsphere = sx₂.circumsphere
The theorem `EuclideanGeometry.circumsphere_eq_of_cospherical` states that in a $n$-dimensional real inner product space (Euclidean space), given a set of cospherical points (points that are all equidistant from some point), if the finite dimension of the corresponding vector space equals $n$, then any two $n$-simplices (generalization of triangles to $n$ dimensions) formed from these points have the same circumsphere (the sphere that circumscribes the simplex). Specifically, if the range of the points of two such simplices are subsets of the given cospherical set, then these two simplices share the same circumsphere.
More concisely: In an n-dimensional Euclidean space, if a set of n points are cospherical, then any two n-simplices formed from these points have the same circumsphere.
|
EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subset
theorem EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subset :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
ps ⊆ ↑s →
∀ [inst_4 : Nonempty ↥s] {n : ℕ} [inst_5 : FiniteDimensional ℝ ↥s.direction],
FiniteDimensional.finrank ℝ ↥s.direction = n →
EuclideanGeometry.Cospherical ps →
∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
This theorem states that for any set of points 'ps' in an n-dimensional affine subspace 's', if all these points are cospherical (equidistant from some point), then all n-simplices formed from these points have the same circumcenter. In other words, if we take any subset of 'n+1' points from 'ps' and form an n-simplex, the circumcenter (the center of the smallest enclosing sphere) of this simplex is the same regardless of the simplex chosen. The theorem assures the existence of such a common circumcenter 'c'.
More concisely: Given a set of points in an n-dimensional affine subspace that are all cospherical, the circumcenters of any n-simplices formed from these points are equal.
|
EuclideanGeometry.circumradius_eq_of_cospherical
theorem EuclideanGeometry.circumradius_eq_of_cospherical :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [inst_4 : FiniteDimensional ℝ V],
FiniteDimensional.finrank ℝ V = n →
EuclideanGeometry.Cospherical ps →
∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumradius = sx₂.circumradius
This theorem states that for any set of cospherical points in an n-dimensional space, if two n-simplices (n-dimensional triangles) have their vertices within this set, then both simplices have the same circumradius. This is subject to the condition that the dimension of the space (as a real vector space) is also n. The circumradius of a simplex is defined as the radius of the smallest circumscribing sphere (or circle in 2D) of the simplex. The theorem is stated in the context of an n-dimensional Euclidean space equipped with an inner product and metric space structure.
More concisely: In an n-dimensional Euclidean space equipped with an inner product and metric, any two n-simplices with vertices in a set of cospherical points have the same circumradius.
|
Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter
theorem Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {i₁ i₂ : Fin (n + 1)},
i₁ ≠ i₂ →
(EuclideanGeometry.reflection (affineSpan ℝ (s.points '' {i₁, i₂}))) s.circumcenter =
(Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter)
(Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
This theorem states that for any real number simplex with a normed add commutative group, an inner product space, a metric space, and a normed add torsor, and for any two distinct vertices of the simplex, the reflection of the circumcenter of the simplex in the line spanned by these two vertices is equal to the affine combination of simplex points (including the circumcenter).
The weights for this affine combination are determined by the `reflectionCircumcenterWeightsWithCircumcenter` function; it assigns a weight of 1 to the specified vertices, -1 to the circumcenter, and 0 to all other points. The 'universe' of points considered for the affine combination is the complete `Finset` of simplex points, as implied by the `Fintype` assumption.
More concisely: For any real simplex with a normed add commutative group, inner product space, metric space, and normed add torsor, the reflection of the circumcenter in the line through two distinct vertices is equal to the affine combination of simplex points with weights determined by `reflectionCircumcenterWeightsWithCircumcenter`.
|
Affine.Simplex.dist_circumcenter_eq_circumradius'
theorem Affine.Simplex.dist_circumcenter_eq_circumradius' :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
dist s.circumcenter (s.points i) = s.circumradius
This theorem states that for any given simplex (a generalization of a triangle to arbitrary dimensions) in a real inner product space, the distance from any point of the simplex to the circumcenter of the simplex is equal to the circumradius of the simplex. This relationship holds true regardless of the dimension of the simplex.
More concisely: The theorem asserts that the distance from any point in a simplex to its circumcenter equals the circumradius in a real inner product space, for all simplex dimensions.
|
Affine.Simplex.circumradius_pos
theorem Affine.Simplex.circumradius_pos :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)),
0 < s.circumradius
This theorem asserts that for any simplex with at least two points, in a normed additive torsion space over a real inner product space, the circumradius (the radius of the smallest enclosing circle) is always positive. This is essentially stating that a simplex with more than one point cannot be collapsed into a single point, thus its circumradius is always greater than zero.
More concisely: In a normed additive torsion space over a real inner product space, the circumradius of any simplex with at least two points is positive.
|
Affine.Simplex.eq_circumcenter_of_dist_eq
theorem Affine.Simplex.eq_circumcenter_of_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P},
p ∈ affineSpan ℝ (Set.range s.points) →
∀ {r : ℝ}, (∀ (i : Fin (n + 1)), dist (s.points i) p = r) → p = s.circumcenter
This theorem is related to the geometry of a simplex in an inner product space. Specifically, it asserts that for any point 'p' lying in the affine span of the points of a given simplex 's', if 'p' is equidistant from all the vertices of the simplex (i.e., the distance from 'p' to every vertex is the same real number 'r'), then 'p' is the circumcenter of the simplex 's'. In simpler terms, the circumcenter of a simplex is the point equidistant from all vertices, and this theorem confirms it in the context of an affine span.
More concisely: If a point lies in the affine span of a simplex and is equidistant from all its vertices, then it is the circumcenter of the simplex.
|
EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq
theorem EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p1 p2 : P} (p3 : P),
p1 ∈ s →
p2 ∈ s →
(dist p1 p3 = dist p2 p3 ↔
dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p3) =
dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p3))
This theorem states that for any non-empty affine subspace `s` of a normed add torsor over a real inner product space, a point `p3` is equidistant from two points `p1` and `p2` in `s` if and only if the orthogonal projection of `p3` onto `s` is equidistant from `p1` and `p2`. In other words, the distance between `p1` and `p3` is equal to the distance between `p2` and `p3` if and only if the distance between `p1` and the orthogonal projection of `p3` onto `s` is equal to the distance between `p2` and the orthogonal projection of `p3` onto `s`.
More concisely: For any non-empty affine subspace of a real inner product space and any three points in it, a point is equidistant from two other points if and only if their orthogonal projections onto the subspace are equally distant from the first point.
|
Affine.Simplex.circumcenter_mem_affineSpan
theorem Affine.Simplex.circumcenter_mem_affineSpan :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
s.circumcenter ∈ affineSpan ℝ (Set.range s.points)
The theorem `Affine.Simplex.circumcenter_mem_affineSpan` states that for any real-affine simplex `s` (which is a `n`-dimensional generalization of a triangle) in an inner product space over reals, equipped with a metric, the circumcenter of the simplex lies in the affine span of the set of points of the simplex. In other words, the circumcenter of the simplex is a linear combination of the points of the simplex.
More concisely: The circumcenter of a real-affine simplex in an inner product space lies in the affine span of its points.
|
EuclideanGeometry.eq_or_eq_reflection_of_dist_eq
theorem EuclideanGeometry.eq_or_eq_reflection_of_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} {s : Affine.Simplex ℝ P n} {p p₁ p₂ : P} {r : ℝ},
p₁ ∈ affineSpan ℝ (insert p (Set.range s.points)) →
p₂ ∈ affineSpan ℝ (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₁ = (EuclideanGeometry.reflection (affineSpan ℝ (Set.range s.points))) p₂
The theorem `EuclideanGeometry.eq_or_eq_reflection_of_dist_eq` states that in a Euclidean space, given a simplex `s` of `n` dimensions, and three points `p`, `p₁`, and `p₂`, such that `p₁` and `p₂` are in the affine span of `p` and the vertices of `s`, and the distances from `p₁` and `p₂` to all vertices of the simplex are equal (say, `r`), then `p₁` and `p₂` must either be identical, or `p₁` is the reflection of `p₂` with respect to the affine span of the vertices of the simplex. In simpler terms, if two points have the same distances to all corners of a shape, they must be either the same point or mirror images of each other in the shape's plane.
More concisely: In a Euclidean space, if a simplex's vertex points and a point not in the simplex have the same distance to all simplex vertices, then they are either identical or mirror reflections across the affine hull of the simplex's vertices.
|
Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq
theorem Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P} {r : ℝ},
(∀ (i : Fin (n + 1)), dist (s.points i) p = r) → ↑(s.orthogonalProjectionSpan p) = s.circumcenter
This theorem states that if a point in a metric space has the same distance from all vertices of a simplex (a generalization of a triangle to any number of dimensions), then the orthogonal projection of this point onto the subspace spanned by the simplex is the circumcenter of the simplex. The circumcenter is the center of the circumsphere that circumscribes the simplex. The theorem assumes that the space is equipped with an inner product and norm operations.
More concisely: If a point in an n-dimensional metric space with an inner product and norm equidistantly lies to all simplex vertices, then it is the circumcenter of the simplex's circumcircle or circumcenter in the subspace spanned by the simplex vertices.
|
EuclideanGeometry.exists_circumsphere_eq_of_cospherical
theorem EuclideanGeometry.exists_circumsphere_eq_of_cospherical :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [inst_4 : FiniteDimensional ℝ V],
FiniteDimensional.finrank ℝ V = n →
EuclideanGeometry.Cospherical ps →
∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
The theorem `EuclideanGeometry.exists_circumsphere_eq_of_cospherical` states that in an $n$-dimensional real inner product space (a form of Euclidean space), if we have a set of points that are cospherical (equidistant from some point), then all $n$-simplices (generalizations of triangles to $n$ dimensions) formed from these points have the same circumsphere (the sphere that circumscribes the simplex). This is under the condition that the finite dimension of the vector space we are considering equals to $n$. The theorem concludes by stating that there exists such a common circumsphere.
More concisely: In an n-dimensional real inner product space, if a set of n points is cospherical, then all n-simplices formed from these points have the same circumsphere.
|
Affine.Simplex.mem_circumsphere
theorem Affine.Simplex.mem_circumsphere :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
s.points i ∈ s.circumsphere
The theorem `Affine.Simplex.mem_circumsphere` states that for any given simplex in an affine space, all of its vertices lie on the circumsphere of the simplex. Here, a simplex is defined in an affine space over the real numbers ℝ, which is equipped with a normed add commutative group structure, an inner product space structure, and a metric space structure. The simplex is indexed by a finite ordinal `n`, and each vertex of the simplex is represented by a point in the affine space. The theorem verifies that each vertex of the simplex is indeed a point on the circumsphere, which is defined to be the unique sphere that circumscribes the simplex.
More concisely: For any simplex of finite dimension in an affine space over the real numbers equipped with a norm, each vertex of the simplex lies on the circumscribing sphere of the simplex.
|
Affine.Simplex.eq_circumradius_of_dist_eq
theorem Affine.Simplex.eq_circumradius_of_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P},
p ∈ affineSpan ℝ (Set.range s.points) →
∀ {r : ℝ}, (∀ (i : Fin (n + 1)), dist (s.points i) p = r) → r = s.circumradius
This theorem states that for any given point within the affine span of an n-dimensional simplex's points, if the distance from this point to all the simplex's points is the same (i.e., each point is equidistant from the given point), then this equal distance is precisely the circumradius of the simplex. The simplex is defined over a real, inner product space, equipped with a metric and its points form a normed additive torsor.
More concisely: Given an n-dimensional simplex over a real inner product space with equal distances from a point to all its points, the common distance is equal to the circumradius of the simplex.
|
Affine.Simplex.circumsphere_reindex
theorem Affine.Simplex.circumsphere_reindex :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {m n : ℕ} (s : Affine.Simplex ℝ P m)
(e : Fin (m + 1) ≃ Fin (n + 1)), (s.reindex e).circumsphere = s.circumsphere
This theorem states that if we have a simplex (a generalization of a triangle to any dimension) in a real inner product space, reindexing its vertices using an equivalence between the index types does not change its circumsphere. More formally, for any simplex `s` of dimension `m` in a real inner product space, and any equivalence `e` between the finite sets `{0, 1, ..., m}` and `{0, 1, ..., n}`, the circumsphere of the simplex obtained by reindexing `s` using `e` is the same as the circumsphere of `s` itself. This holds true regardless of the dimensionality of the space, the metric space, or the normed additive torsor structure.
More concisely: The circumsphere of a simplex in a real inner product space is unchanged when its vertices are reindexed via an equivalence between their index sets.
|
Affine.Simplex.circumsphere_unique_dist_eq
theorem Affine.Simplex.circumsphere_unique_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : 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
This theorem states that for any n-dimensional affine simplex with a normed additive commutative group structure on the underlying vector space, an inner product space over real numbers, a metric space on the points, and a normed additive group action of vectors on points, the center of the circumsphere of the simplex is in the smallest affine subspace containing the points of the simplex, and all the points of the simplex are on the sphere with the center at the center of the circumsphere and radius equal to the radius of the circumsphere. Moreover, if there exists another sphere with the same properties i.e. its center is in the affine span of the simplex points and the simplex points are on this sphere, then this sphere must be the same as the circumsphere. This essentially guarantees the uniqueness of the circumsphere for a given simplex.
More concisely: For any n-dimensional affine simplex with a given normed vector space structure, inner product space over real numbers, metric space structure, and normed vector action, the center of its circumsphere is in the affine hull of its points, and all points lie on the sphere with this center and radius equal to the circumsphere's radius, making it the unique circumsphere for the simplex.
|
Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter
theorem Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
s.circumcenter =
(Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter)
(Affine.Simplex.circumcenterWeightsWithCircumcenter n)
The theorem `Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter` states that for any real-number simplex of arbitrary dimension `n`, defined in a normed additive commutative group `V` and a corresponding metric space `P` with `V` as the associated torsor, the circumcenter of the simplex can be represented as an affine combination of the points of the simplex along with the circumcenter. The weights for this affine combination are given by the `circumcenterWeightsWithCircumcenter` function, which sets the weight of the circumcenter as 1 and the weights of all other points as 0. This essentially means that the circumcenter of the simplex is the affine combination of all points of the simplex, with all the weights being zero except for the circumcenter itself.
More concisely: The circumcenter of a real-number simplex in a normed additive commutative group is representable as an affine combination of its points with weights given by the `circumcenterWeightsWithCircumcenter` function.
|
EuclideanGeometry.cospherical_iff_exists_mem_of_complete
theorem EuclideanGeometry.cospherical_iff_exists_mem_of_complete :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
ps ⊆ ↑s →
∀ [inst_4 : Nonempty ↥s] [inst_5 : HasOrthogonalProjection s.direction],
EuclideanGeometry.Cospherical ps ↔ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius
This theorem, titled `EuclideanGeometry.cospherical_iff_exists_mem_of_complete`, states that given an affine subspace that is nonempty and directionally complete, if it contains a set of points, then these points are cospherical (equidistant from a common point) if and only if there exists a point in the subspace such that all points in the set are equidistant from this point. In simpler terms, it's stating a condition for when a set of points in a certain subspace can be said to be cospherical.
More concisely: Given a nonempty, directionally complete affine subspace, points in it are cospherical if and only if there exists a point in the subspace such that all points have equal distance to it.
|
EuclideanGeometry.exists_circumsphere_eq_of_cospherical_subset
theorem EuclideanGeometry.exists_circumsphere_eq_of_cospherical_subset :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
ps ⊆ ↑s →
∀ [inst_4 : Nonempty ↥s] {n : ℕ} [inst_5 : FiniteDimensional ℝ ↥s.direction],
FiniteDimensional.finrank ℝ ↥s.direction = n →
EuclideanGeometry.Cospherical ps →
∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
The theorem `EuclideanGeometry.exists_circumsphere_eq_of_cospherical_subset` states that in any n-dimensional subspace, all n-simplices that are constructed from a set of cospherical points have the same circumsphere. More precisely, given a subspace `s` and a set of points `ps` which are cospherical and contained in `s`, if the finite rank of the direction of `s` is `n`, then there exists a circumsphere such that for any `n`-simplex `sx` whose points are in `ps`, the circumsphere of `sx` is the same as this circumsphere. It is assumed that the subspace `s` is nonempty and has a finite dimensional direction over the real numbers. The types `V` and `P` are assumed to form a normed add torsor with `V` being a normed add commutative group and an inner product space over real numbers, and `P` being a metric space.
More concisely: Given a nonempty n-dimensional subspace `s` over the real numbers with finite rank `n`, having a set `ps` of cospherical points contained in `s`, there exists a unique circumsphere for any n-simplex formed by points in `ps`, and all such simplices share this circumsphere.
|
Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection
theorem Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : 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⟩
This theorem states that for any normed additively commutative group `V`, inner product space over the real numbers `ℝ`, metric space `P`, and normed additive torsor `V P`, along with a natural number `n` representing a simplex `s`, and two points `p1` and `p2` in `P`, and a real number `r`, if `p1` is in the affine span of the range of the points of the simplex `s`, then adding `r` times the vector from the orthogonal projection of `p2` on the span of `s` to `p2` to `p1`, and then taking the orthogonal projection onto the span of `s`, gives back `p1`. In other words, within this context, this theorem describes a certain property of orthogonal projections in the affine geometry of a simplex.
More concisely: Given a normed additive torsor `V` over a metric space `P`, an inner product space `V` over the real numbers `ℝ`, a simplex `s` represented by a natural number `n`, and points `p1, p2` in `P`, if `p1` is in the affine span of `s` and `p2` is in the orthogonal complement of `s`, then `p1` is the orthogonal projection of `p1 + r(p2 - orthogonal_proj p2 s)` onto `s`, where `r` is a real number.
|
Affine.Simplex.pointsWithCircumcenter_eq_circumcenter
theorem Affine.Simplex.pointsWithCircumcenter_eq_circumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
s.pointsWithCircumcenter Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex = s.circumcenter
This theorem states that for any given affine simplex, when the function `pointsWithCircumcenter` is applied to the `circumcenterIndex`, it returns the circumcenter of that simplex. This is asserted for any simplex in a normed additively commutative group that is also an inner product space over the real numbers, and is a metric space under a normed additive torsor.
More concisely: For any affine simplex in a normed additively commutative group that is an inner product space over the real numbers and a metric space under a normed additive torsor, the `pointsWithCircumcenter` function returns the circumcenter of that simplex when applied to its circumcenter index.
|
Affine.Simplex.circumradius_nonneg
theorem Affine.Simplex.circumradius_nonneg :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n), 0 ≤ s.circumradius
This theorem states that the circumradius of an affine simplex is always non-negative. In the context of the theorem, an affine simplex is a generalization of a triangle or tetrahedron to arbitrary dimensions, defined in a space with a certain mathematical structure (a normed add torsor over an inner product space). The circumradius is the radius of the smallest enclosing ball (in three dimensions, a sphere) that contains all the vertices of the simplex. Regardless of the dimension of the simplex or the specifics of the vertices, the theorem assures that this circumradius can never be less than zero.
More concisely: The circumradius of an affine simplex in a normed additive torsor over an inner product space is non-negative.
|
EuclideanGeometry.circumradius_eq_of_cospherical_subset
theorem EuclideanGeometry.circumradius_eq_of_cospherical_subset :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
ps ⊆ ↑s →
∀ [inst_4 : Nonempty ↥s] {n : ℕ} [inst_5 : FiniteDimensional ℝ ↥s.direction],
FiniteDimensional.finrank ℝ ↥s.direction = n →
EuclideanGeometry.Cospherical ps →
∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumradius = sx₂.circumradius
This theorem states that if we have a set of points that are cospherical (equidistant from some common point) within an n-dimensional subspace, any two n-dimensional simplices (generalization of triangles and tetrahedrons) created from the set of those points will have the same circumradius. This holds regardless of the specific points used to form each simplex, as long as they are chosen from the aforementioned cospherical set of points.
More concisely: In an n-dimensional subspace, any two n-dimensional simplices formed by points that are equidistant from a common point have the same circumradius.
|
EuclideanGeometry.circumcenter_eq_of_cospherical_subset
theorem EuclideanGeometry.circumcenter_eq_of_cospherical_subset :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
ps ⊆ ↑s →
∀ [inst_4 : Nonempty ↥s] {n : ℕ} [inst_5 : FiniteDimensional ℝ ↥s.direction],
FiniteDimensional.finrank ℝ ↥s.direction = n →
EuclideanGeometry.Cospherical ps →
∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumcenter = sx₂.circumcenter
The theorem `EuclideanGeometry.circumcenter_eq_of_cospherical_subset` states that in an n-dimensional subspace, if a set of points are cospherical (meaning they are equidistant from some point), then any two n-simplices (n-dimensional triangles) formed from this set of points will have the same circumcenter. The circumcenter is the center of the circle that circumscribes the simplex. The subspace is defined over a space with an inner product and the points have a normed addition group structure. The proof of this theorem has been omitted.
More concisely: In an n-dimensional subspace endowed with an inner product, if a set of points is cospherical, then any two n-simplices formed by those points have the same circumcenter.
|