feat(MeasureTheory): WithLp 2 (U × V) → U × V is measure preserving by wwylele · Pull Request #34859 · leanprover-community/mathlib4

wwylele · 2026-02-05T01:11:47Z

Intermediate lemmas towards #34826, and analogue to three existing lemma in the same file:

theorem EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp :
    MeasurePreserving (MeasurableEquiv.toLp 2 (ι → ℝ)).symm := by

theorem PiLp.volume_preserving_ofLp : MeasurePreserving (@ofLp 2 (ι → ℝ)) :=

theorem PiLp.volume_preserving_toLp : MeasurePreserving (@toLp 2 (ι → ℝ)) :=

I am not very good at working with measure theory directly, so this implementation just reduces the problem to known lemmas, but it is pretty cumbersome. Golfing is welcome!

github-actions · 2026-02-05T01:12:53Z

PR summary 1321470619

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace	2291	2292	+1 (+0.04%)

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.Instances` `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

Declarations diff

+ EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp_prod
+ Prod.volume_preserving_ofLp
+ Prod.volume_preserving_toLp
+ aux

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

Copilot

Pull request overview

This pull request adds measure-preserving lemmas for the equivalence between WithLp 2 (U × V) and U × V, extending similar existing results for EuclideanSpace and PiLp to product spaces. These results are intermediate lemmas needed for PR #34826 which aims to compute the volume of a simplex.

Changes:

Added import for Mathlib.Analysis.InnerProductSpace.ProdL2 to support inner product structure on products
Introduced EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp_prod theorem proving measure preservation
Added convenience theorems Prod.volume_preserving_ofLp and Prod.volume_preserving_toLp following the pattern of similar PiLp theorems

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

eric-wieser · 2026-02-05T07:45:30Z

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

+  ( -- WithLp 2 (U × V) ≃ₗᵢ[ℝ] WithLp 2 (WithLp 2 (Fin .. → ℝ) × WithLp 2 (Fin .. → ℝ)
+    (LinearIsometryEquiv.withLpProdCongr 2
+      (stdOrthonormalBasis ℝ U).repr
+      (stdOrthonormalBasis ℝ V).repr).trans <|
+    -- .. ≃ₗᵢ[ℝ] WithLp 2 (Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ)
+    (PiLp.sumPiLpEquivProdLpPiLp 2 (fun _ ↦ ℝ)).symm
+  ).toMeasurableEquiv.trans <|
+  -- .. ≃ᵐ Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ
+  (MeasurableEquiv.toLp 2 _).symm.trans <|
+  -- .. ≃ᵐ Fin (finrank ℝ U) → ℝ × Fin (finrank ℝ V) → ℝ
+  (MeasurableEquiv.sumPiEquivProdPi (fun _ ↦ ℝ)).trans <|
+  -- .. ≃ᵐ U × V
+  (MeasurableEquiv.prodCongr
+    ((MeasurableEquiv.toLp 2 _).trans (stdOrthonormalBasis ℝ U).repr.symm.toMeasurableEquiv)
+    ((MeasurableEquiv.toLp 2 _).trans (stdOrthonormalBasis ℝ V).repr.symm.toMeasurableEquiv))


Rather than writing these intermediate states as comments, you might be able to enter tactic mode and use trans.

or perhaps calc could work?

It looks like neither of these works.

When I do trans Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ, I got

transitivity lemmas only apply to binary relations and non-dependent arrows, not WithLp 2 (U × V) ≃ᵐ U × V

When I tried calc like

private noncomputable def aux2 : WithLp 2 (U × V) ≃ᵐ U × V := calc WithLp 2 (U × V) ≃ᵐ WithLp 2 (Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) := sorry WithLp 2 (Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) ≃ᵐ U × V := sorry

I got

invalid 'calc' step, failed to synthesize `Trans` instance Trans (@MeasurableEquiv (WithLp 2 (U × V)) (WithLp 2 (Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ))) (@MeasurableEquiv (WithLp 2 (Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ)) (U × V)) ?m.55

They do work if I downgrade ≃ᵐ to ≃. It looks like we need to register all the "advanced" equivalence to Trans?

wwylele mentioned this pull request Feb 5, 2026

feat(Geometry/Euclidean): volume of a simplex #34826

Draft

6 tasks

wwylele requested a review from Copilot February 5, 2026 01:12

github-actions bot added the t-measure-probability Measure theory / Probability theory label Feb 5, 2026

Copilot started reviewing on behalf of wwylele February 5, 2026 01:13 View session

Copilot AI reviewed Feb 5, 2026

View reviewed changes

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean Show resolved Hide resolved

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean Outdated Show resolved Hide resolved

feat(MeasureTheory): WithLp 2 (U × V) → U × V is measure preserving

57a4db2

wwylele force-pushed the prod-lp-measure branch from d473740 to 57a4db2 Compare February 5, 2026 01:21

eric-wieser reviewed Feb 5, 2026

View reviewed changes

wwylele requested a review from eric-wieser February 5, 2026 16:36

mathlib-triage bot assigned RemyDegenne Feb 9, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(MeasureTheory): WithLp 2 (U × V) → U × V is measure preserving#34859

feat(MeasureTheory): WithLp 2 (U × V) → U × V is measure preserving#34859
wwylele wants to merge 1 commit intoleanprover-community:masterfrom
wwylele:prod-lp-measure

wwylele commented Feb 5, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Feb 5, 2026 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

eric-wieser Feb 5, 2026

Uh oh!

b-mehta Feb 5, 2026

Uh oh!

wwylele Feb 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

wwylele commented Feb 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 1321470619

Import changes for modified files

Declarations diff

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

eric-wieser Feb 5, 2026

Choose a reason for hiding this comment

Uh oh!

b-mehta Feb 5, 2026

Choose a reason for hiding this comment

Uh oh!

wwylele Feb 5, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

wwylele commented Feb 5, 2026 •

edited

Loading

github-actions bot commented Feb 5, 2026 •

edited

Loading