feat(Geometry/Euclidean): volume of a simplex

[wwylele]

WIP. sorry-free but still need cleaning up and breaking into smaller PRs

---

• depends on: feat(Geometry/Euclidean): the Euclidean volume measure #34697
• depends on: [Merged by Bors] - feat(LinearAlgebra/AffineSpace): more lemma about simplex face and interior #34858
• depends on: feat(MeasureTheory): WithLp 2 (U × V) → U × V is measure preserving #34859
• depends on: feat(LinearAlgebra/AffineSpace): small lemmas about lineMap and homothety #35039
• depends on: feat(Geometry/Euclidean): Simplex.closedInterior is closed #35358
• depends on: feat(LinearAlgebra/Simplex): closedInterior = interior + face.closedInterior #35365

[github-actions]

PR summary 99884c2730

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
176 files Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Analysis.Analytic.Binomial Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.PositiveLinearMap Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.Unitary.Connected Mathlib.Analysis.CStarAlgebra.Unitary.Span Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LogDerivUniformlyOn Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.BorelCaratheodory Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.Harmonic.Analytic Mathlib.Analysis.Complex.Harmonic.MeanValue Mathlib.Analysis.Complex.HasPrimitives Mathlib.Analysis.Complex.JensenFormula Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.MeanValue Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Complex.Polynomial.GaussLucas Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.SummableUniformlyOn Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace.Basic Mathlib.Analysis.Distribution.SchwartzSpace.Deriv Mathlib.Analysis.Distribution.SchwartzSpace.Fourier Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.Distribution.TemperedDistribution Mathlib.Analysis.Fourier.Convolution Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Fourier.FourierTransform Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.LpSpace Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Meromorphic.Complex Mathlib.Analysis.Normed.Algebra.GelfandFormula Mathlib.Analysis.Normed.Algebra.GelfandMazur Mathlib.Analysis.Normed.Lp.SmoothApprox Mathlib.Analysis.Polynomial.Factorization Mathlib.Analysis.Polynomial.MahlerMeasure Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.SpecialFunctions.Gamma.Digamma Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Geometry.Manifold.BumpFunction Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.SmoothApprox Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.Chebyshev Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.MahlerMeasure Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.Bounds Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.NumberTheory.ModularForms.NormTrace Mathlib.NumberTheory.ModularForms.Petersson Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.InfinitePlace.Basic Mathlib.NumberTheory.NumberField.InfinitePlace.Completion Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Probability.Distributions.Beta Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Pareto Mathlib.RingTheory.Polynomial.Selmer Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic	1
Mathlib.Geometry.Euclidean.Volume.Measure (new file)	2412
Mathlib.Geometry.Euclidean.Volume.Integral (new file)	2548

---

Declarations diff

+ Affine.Simplex.closedInterior_eq_convexHull
+ Affine.Simplex.closedInterior_eq_interior_union
+ Affine.Simplex.closedInterior_face_subset_closedInterior
+ Affine.Simplex.closedInterior_inter_mapHomothety_eq_empty
+ Affine.Simplex.closedInterior_inter_shift
+ Affine.Simplex.euclideanHausdorffMeasure_closedInterior
+ Affine.Simplex.euclideanHausdorffMeasure_closedInterior'
+ Affine.Simplex.euclideanHausdorffMeasure_closedInterior_eq_one
+ Affine.Simplex.euclideanHausdorffMeasure_closedInterior_ne_top
+ Affine.Simplex.euclideanHausdorffMeasure_closedInterior_real_eq_one
+ Affine.Simplex.euclideanHausdorffMeasure_interior
+ Affine.Simplex.euclideanHausdorffMeasure_interior_eq_zero
+ Affine.Simplex.euclideanHausdorffMeasure_real_closedInterior
+ Affine.Simplex.height_eq_dist
+ Affine.Simplex.isClosed_closedInterior
+ Affine.Simplex.measurable_closedInterior
+ Affine.Simplex.volume
+ Affine.Simplex.volume_eq
+ Affine.Simplex.volume_eq'
+ Affine.Simplex.volume_eq_dist
+ Affine.Simplex.volume_eq_euclideanHausdorffMeasure_real_closedInterior
+ AffineMap.euclideanHausdorffMeasure_homothety
+ AffineSubspace.direction_shift
+ AffineSubspace.euclideanHausdorffMeasure_coe_image
+ AffineSubspace.euclideanHausdorffMeasure_eq_lintegral
+ AffineSubspace.homothety_mem
+ AffineSubspace.measurableEquivProd
+ AffineSubspace.measurePreserving_measurableEquivProd
+ AffineSubspace.shift
+ AffineSubspace.shift_eq
+ AffineSubspace.shift_eq_map_homothety
+ AffineSubspace.shift_zero
+ EuclideanGeometry.euclideanHausdorffMeasure_eq
+ EuclideanGeometry.euclideanHausdorffMeasure_eq_lintegral
+ EuclideanGeometry.measurePreserving_vaddConst
+ EuclideanSpace.euclideanHausdorffMeasure_eq_volume
+ EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp_prod
+ Finset.homothety_affineCombination
+ Finset.lineMap_affineCombination
+ InnerProductSpace.euclideanHausdorffMeasure_eq_volume
+ Isometry.euclideanHausdorffMeasure_image
+ Isometry.euclideanHausdorffMeasure_preimage
+ Isometry.map_euclideanHausdorffMeasure
+ IsometryEquiv.measurePreserving_euclideanHausdorffMeasure
+ MeasurableEquiv.trans_symm
+ MeasureTheory.Measure.addHaarScalarFactor_volume_hausdorffMeasure_ne_zero
+ MeasureTheory.Measure.euclideanHausdorffMeasure
+ MeasureTheory.Measure.euclideanHausdorffMeasure_def
+ MeasureTheory.Measure.euclideanHausdorffMeasure_smul₀
+ MeasureTheory.Measure.euclideanHausdorffMeasure_zero
+ MeasureTheory.Measure.euclideanHausdorffMeasure_zero_or_top
+ Prod.volume_preserving_ofLp
+ Prod.volume_preserving_toLp
+ aux
+ instance (d : ℕ) : (μH[d] : Measure (EuclideanSpace ℝ (Fin d))).IsAddHaarMeasure := by
+ volume_eq_of_finrank_eq_one

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

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Geometry/Euclidean): the Euclidean volume measure #34697
• [Merged by Bors] - feat(LinearAlgebra/AffineSpace): more lemma about simplex face and interior #34858
• feat(MeasureTheory): WithLp 2 (U × V) → U × V is measure preserving #34859
• feat(LinearAlgebra/AffineSpace): small lemmas about lineMap and homothety #35039
• feat(Geometry/Euclidean): Simplex.closedInterior is closed #35358
• feat(LinearAlgebra/Simplex): closedInterior = interior + face.closedInterior #35365
  By Dependent Issues (🤖). Happy coding!