WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Centroid

Revision #1070 → #1981 · back to history

modifiedCentroid (general definition)25471dc59b55
FieldFrom #1070To #1981
mathlib.decl—Finset.centroid
mathlib.match_kind—special_case
mathlib.module—Mathlib.LinearAlgebra.AffineSpace.Centroid
note—Mathlib formalizes only the discrete `Finset.centroid` (mean of finitely many points), not the general 'mean position of all points in a figure'.
status—partial
modifiedBarycenter / center of mass7aacdc3937ca
FieldFrom #1070To #1981
mathlib.decl—Finset.centerMass
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.Convex.Combination
note—`Finset.centerMass` is the discrete weighted barycenter; continuous uniform-density barycenter of a figure is not formalized.
status—partial
modifiedCenter of gravity2dd338edf606
FieldFrom #1070To #1981
mathlib.decl—Finset.centerMass
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.Convex.Combination
note—Mathlib has the discrete weighted-mean `Finset.centerMass`; the gravity-field / continuous version is not present.
status—partial
modifiedGeographical centerf02e03d6fb5b
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No geography-specific centroid construction is in Mathlib.
status—not_formalized
modifiedCentroid of convex object lies inside92244eab8206
FieldFrom #1070To #1981
mathlib.decl—Finset.centroid_mem_convexHull
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.Convex.Combination
note—Mathlib proves the discrete centroid of a finite point set lies in its convex hull, but not the analogous statement for a general convex body's geometric centroid.
status—partial
modifiedCentroid is fixed point of symmetry group24be9686b471
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No theorem in Mathlib asserts that the centroid is preserved by every isometry of a figure's symmetry group.
status—not_formalized
modifiedCentroid of a parallelograme3a8ebccada2
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no `Parallelogram` structure nor a theorem identifying its centroid with the diagonals' intersection.
status—not_formalized
modifiedCentroid undefined under translational symmetryff2910333ce6
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No corresponding lemma in Mathlib.
status—not_formalized
modifiedCentroid of a triangle (medians)0a1414965d5f
FieldFrom #1070To #1981
mathlib.decl—Affine.Simplex.eq_centroid_of_forall_mem_median
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
note—Stated in arbitrary dimension (1 < n): the unique point lying on every median of a simplex is the centroid; specializes to the triangle case.
status—formalized
modifiedCentroid of a finite set of pointsca3ceacfe2bf
FieldFrom #1070To #1981
mathlib.decl—Finset.centroid
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.AffineSpace.Centroid
note—`Finset.centroid` is exactly the affine combination with uniform weights 1/#s.
status—formalized
modifiedMinimizes sum of squared distances2730f6b4356e
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Mathlib lemma identifies the centroid as the minimizer of the sum of squared Euclidean distances to a finite point set.
status—not_formalized
modifiedCentroid by geometric decomposition4b9226315d2e
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The decomposition formula for computing centroids of figures is not formalized.
status—not_formalized
modifiedSquare, triangle, and circular hole decomposition3df5f7d374c9
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No such worked example exists in Mathlib.
status—not_formalized
modifiedGeneralization to higher dimensions34511a5a23bb
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not formalize the geometric-decomposition formula for centroids of 3D objects.
status—not_formalized
modifiedCentroid by integral formula (vector)f2ccb19e0b77
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No definition of a region's centroid as ∫x dA / ∫dA appears in Mathlib.
status—not_formalized
modifiedCoordinate-wise centroid formulaf2d80ed24744
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Continuous coordinate-wise integral centroid formula is not in Mathlib.
status—not_formalized
modifiedBarycentric coordinates of plane figure60e9eb213ce9
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has abstract `AffineBasis.coord` barycentric coordinates but no integral barycentric formula for a plane region.
status—not_formalized
modifiedCentroid of bounded region between two curvesd376e48c4004
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formalization of the centroid of a region between two graphs.
status—not_formalized
modifiedIntegraph and Green's theoremc5420b80ac9c
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib lacks both the integraph centroid construction and Green's-theorem-based centroid formula.
status—not_formalized
modifiedCentroid of an L-shaped object69e85140c728
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No such worked example exists in Mathlib.
status—not_formalized
modifiedCentroid of a triangle (medians and 2:1 ratio)5693c0551af8
FieldFrom #1070To #1981
mathlib.decl—Affine.Triangle.dist_point_centroid
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Euclidean.Simplex
note—Combined with `Affine.Simplex.eq_centroid_of_forall_mem_median`, this gives the medians' intersection and the 2:1 distance ratio for triangles.
status—formalized
modifiedCentroid in barycentric coordinates054460a4d784
FieldFrom #1070To #1981
mathlib.decl—Finset.centroidWeights
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.AffineSpace.Centroid
note—`centroidWeights` assigns equal weight 1/n to each vertex, which is the (1/3,1/3,1/3) barycentric statement for a triangle, but no triangle-specific lemma stating this in barycentric form is present.
status—partial
modifiedCentroid in trilinear coordinatesb8b84f369030
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Trilinear coordinates are not formalized in Mathlib.
status—not_formalized
modifiedCentroid as physical center of mass1f00a082cb33
FieldFrom #1070To #1981
mathlib.decl—Finset.centroid_eq_centerMass
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.Convex.Combination
note—Discrete `centroid = centerMass` is proved; the physical center-of-mass interpretation for a uniform triangular lamina is not separately formalized.
status—partial
addedSpieker center for perimeter-distributed massc04fc3d74c0b
modifiedArea via centroid distanceeefe7c5efb27
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No area-via-centroid-distance formula is in Mathlib.
status—not_formalized
modifiedCentroid on Euler line06683e53dfe6
FieldFrom #1070To #1981
mathlib.decl—Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Euclidean.MongePoint
note—Mathlib proves the collinearity formula H = 3(G − O) + O directly but does not define `EulerLine` as a named object.
status—partial
modifiedRelation with incenter and nine-point centerdb36c8e0be6b
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has incenter and nine-point-circle, but no centroid distance relations among them are formalized.
status—not_formalized
modifiedIsogonal conjugate of centroid957e94750ee4
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither isogonal conjugate nor symmedian point are in Mathlib.
status—not_formalized
modifiedMedians bisect triangle areaab31071291da
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Triangle-area lemmas in Mathlib do not include the median-bisection property.
status—not_formalized
modifiedSum of squared distances from a pointa74f6f4f9d5c
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Leibniz-style identity relating sum of squared distances to the centroid is not in Mathlib.
status—not_formalized
modifiedSum of squares of sides equals three times sum from centroidb47005b7d6f9
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No such identity is formalized.
status—not_formalized
modifiedCentroid maximizes product of directed distances9ffe0a3b5999
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No such optimization characterization of the centroid is in Mathlib.
status—not_formalized
modifiedMidpoint identity for any point in plane91409d23e5aa
FieldFrom #1070To #1981
anchor.snippetlet [MATH] be the midpoints of segmentsbe the midpoints of segments
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Snippet trimmed to remove [MATH] token.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedCentroid of a polygon734f4f46f918
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—`Mathlib/Geometry/Polygon/Basic.lean` defines `Polygon` but no centroid construction for it.
status—not_formalized
modifiedSigned area via shoelace formula3d60f6e90c39
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The shoelace formula for polygon signed area is not formalized in Mathlib.
status—not_formalized
modifiedPolygon centroid vs vertex centroid0467dfeae40a
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No comparison of polygon centroid and vertex centroid in Mathlib.
status—not_formalized
modifiedCentroid of a cone or pyramidad6c9d5d112d
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Cones and pyramids are not present as geometric figures in Mathlib.
status—not_formalized
modifiedMedians and bimedians of tetrahedron concur at centroid5ac0790274b7
FieldFrom #1070To #1981
mathlib.decl—Affine.Simplex.eq_centroid_of_forall_mem_median
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
note—Concurrence of the four medians at the centroid is proven for all simplices with 1 < n; bimedians are not formalized as such.
status—partial
addedTetrahedron medians divided in 3:1 ratio at centroid42201f788e44
modifiedTetrahedron centroid as midpoint of Monge point and circumcentercda8b0ffa5af
FieldFrom #1070To #1981
mathlib.decl—Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Euclidean.MongePoint
note—The general Monge-point/circumcenter/centroid relation for n-simplices is in Mathlib; the specialized 'midpoint' phrasing for tetrahedra is not separately stated.
status—partial
modifiedCentroid of an n-dimensional simplexa8b8aa30cf6b
FieldFrom #1070To #1981
mathlib.decl—Affine.Simplex.centroid
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
note—`Affine.Simplex.centroid` is the centroid of the simplex's vertices for arbitrary n.
status—formalized
modifiedSimplex centroid as center of massb2d1676e39ff
FieldFrom #1070To #1981
mathlib.decl—Finset.centroid_eq_centerMass
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.Convex.Combination
note—Discrete equivalence of `centroid` and `centerMass` is proved; uniform mass distribution over a continuous simplex is not formalized.
status—partial
modifiedCentroid of a solid hemisphereb95e4ad8cc17
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No hemisphere centroid computation appears in Mathlib.
status—not_formalized
modifiedCentroid of a hollow hemisphere749534b29fa2
FieldFrom #1070To #1981
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No hollow-hemisphere centroid computation appears in Mathlib.
status—not_formalized