Commit 2025-06-01 16:11 8931981d

View on Github →

feat: generalize the Integral.Pi file from volume to other measures (#25329)

Estimated changes

Modified Mathlib/Analysis/Fourier/AddCircleMulti.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

Modified Mathlib/MeasureTheory/Integral/Pi.lean

modified theorem MeasureTheory.Integrable.fintype_prod

modified theorem MeasureTheory.Integrable.fintype_prod_dep

added theorem MeasureTheory.integral_fin_nat_prod_volume_eq_prod

added theorem MeasureTheory.integral_fintype_prod_volume_eq_pow

added theorem MeasureTheory.integral_fintype_prod_volume_eq_prod

Modified Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean