feat(LinearAlgebra/AffineSpace/Simplex/Centroid): define centroid and medians

[zcyemi]

---

This file proves several lemmas involving the centroids and medians of a simplex in affine space.

definitions:

• centroid is the centroid of a simplex, defined as abbreviation of the Finset.univ.centroid.
• faceOppositeCentroid is the centroid of the facet obtained as (Simplex.faceOpposite i).centroid
• median is the line connecting a vertex to the faceOppositeCentroid.

Main Results:

• Commandino's theorem

• The medians of a simplex are concurrent at the centroid

• [ ] depends on #29128

[github-actions[bot]]

PR summary 4d33172004

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional	1092	1093	+1 (+0.09%)
Mathlib.Geometry.Euclidean.Simplex	1644	1645	+1 (+0.06%)

Import changes for all files

Files

Import difference

67 files Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Convex.BetweenList Mathlib.Analysis.Convex.Between Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.Radon Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.Visible Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Affine.AsymptoticCone Mathlib.Analysis.Normed.Affine.Convex Mathlib.Geometry.Euclidean.Altitude Mathlib.Geometry.Euclidean.Angle.Bisector Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Projection Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.Congruence Mathlib.Geometry.Euclidean.Incenter Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Geometry.Euclidean.Projection Mathlib.Geometry.Euclidean.SignedDist Mathlib.Geometry.Euclidean.Similarity Mathlib.Geometry.Euclidean.Simplex Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Sphere.OrthRadius Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Sphere.Tangent Mathlib.Geometry.Euclidean.Triangle Mathlib.InformationTheory.KullbackLeibler.Basic Mathlib.InformationTheory.KullbackLeibler.KLFun Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Ideal Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Topology.Algebra.AsymptoticCone Mathlib.Topology.MetricSpace.HausdorffDimension

1

---

Declarations diff

+ Affine.Simplex.collinear_point_centroid_faceOppositeCentroid + affineIndependent_points_update_centroid + centroid + centroid_eq_affine_combination + centroid_eq_smul_sum_vsub_vadd + centroid_eq_smul_vsub_vadd_point + centroid_map + centroid_mem_affineSpan + centroid_mem_median + centroid_notMem_affineSpan_compl + centroid_reindex + centroid_restrict + centroid_vsub_eq + centroid_vsub_faceOppositeCentroid_eq_smul_vsub + centroid_vsub_point_eq_smul_sum_vsub + centroid_vsub_point_eq_smul_vsub + centroid_weighted_vsub_eq_zero + eq_centroid_iff_sum_vsub_eq_zero + eq_centroid_of_forall_mem_median + faceOppositeCentroid + faceOppositeCentroid_eq_affineCombination + faceOppositeCentroid_eq_smul_vsub_vadd_point + faceOppositeCentroid_eq_sum_vsub_vadd + faceOppositeCentroid_map + faceOppositeCentroid_mem_affineSpan + faceOppositeCentroid_mem_median + faceOppositeCentroid_reindex + faceOppositeCentroid_restrict + faceOppositeCentroid_vsub_centroid_eq_smul_vsub + faceOppositeCentroid_vsub_faceOppositeCentroid + faceOppositeCentroid_vsub_point_eq_smul_sum_vsub + faceOppositeCentroid_vsub_point_eq_smul_vsub + finset_centroid_eq + median + median_eq_affineSpan_point_centroid + median_reindex + point_mem_median + point_vsub_centroid_eq_smul_vsub + point_vsub_faceOppositeCentroid_eq_smul_sum_vsub + point_vsub_faceOppositeCentroid_eq_smul_vsub + smul_centroid_vsub_point_eq_smul_faceOppositeCentroid_vsub_point + smul_centroid_vsub_point_eq_sum_vsub + smul_faceOppositeCentroid_vsub_point_eq_sum_vsub ++ dist_point_centroid ++ dist_point_faceOppositeCentroid

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[jsm28]

What results in the large-import warning from CI? If it's the FiniteDimensional import and that's only needed for Collinear, it might be better to switch the import direction and move that one lemma to Collinear.lean.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[jsm28]

My previous comment about avoiding the large import still applies. In addition, I think the new simplex definitions should have lemmas about how they apply to a simplex constructed with reindex, map or restrict, similar to such lemmas I've been adding for other simplex definitions.

[zcyemi]

What results in the large-import warning from CI? If it's the FiniteDimensional import and that's only needed for Collinear, it might be better to switch the import direction and move that one lemma to Collinear.lean.

This lemma requirea collinear definition:

theorem collinear_point_centroid_faceOppositeCentroid [CharZero k] (s : Simplex k P n)
    (i : Fin (n + 1)) :
    Collinear k {s.points i, s.centroid, s.faceOppositeCentroid i} := by

Is it reasonable to move collinear_point_centroid_faceOppositeCentroid to a new file LinearAlgebra/AffineSpace/Simplex/Collinear.lean or is there a better place for it?

[jsm28]

I'd actually say it's reasonable to use the existing LinearAlgebra/AffineSpace/FiniteDimensional.lean for this (that is, make that existing file import the new file) rather than creating a new file for the one lemma.

[zcyemi]

-awaiting-author