[Merged by Bors] - chore: extract 3 new files out of MeasureSpace by RemyDegenne · Pull Request #20509 · leanprover-community/mathlib4

RemyDegenne · 2025-01-06T09:14:47Z

The MeasureSpace file contains many definitions about measures and is 2000 lines long.
This PR splits 3 files by taking material from the bottom of MeasureSpace:

Map: map of a measure by a function
AbsolutelyContinuous: absolute continuity of measures
QuasiMeasurePreserving: quasi measure preserving functions

github-actions · 2025-01-06T09:15:37Z

PR summary 4cc2077e63

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Measure.MeasureSpace	1329	1327	-2 (-0.15%)

Import changes for all files

Files	Import difference
`Mathlib.MeasureTheory.Measure.MeasureSpace`	-2
`Mathlib.MeasureTheory.Covering.VitaliFamily`	1
398 files `Mathlib.MeasureTheory.Integral.VitaliCaratheodory` `Mathlib.Analysis.BoxIntegral.UnitPartition` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Probability.Process.HittingTime` `Mathlib.Probability.BorelCantelli` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.Probability.Kernel.Defs` `Mathlib.Probability.Variance` `Mathlib.Analysis.SpecialFunctions.Integrals` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.Analysis.Calculus.BumpFunction.Convolution` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Probability.Distributions.Geometric` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.MeasureTheory.Integral.Marginal` `Mathlib.MeasureTheory.Measure.FiniteMeasure` `Mathlib.MeasureTheory.Function.SpecialFunctions.Basic` `Mathlib.MeasureTheory.Integral.IntervalAverage` `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.MeasureTheory.Measure.ProbabilityMeasure` `Mathlib.MeasureTheory.Function.UnifTight` `Mathlib.NumberTheory.GaussSum` `Mathlib.MeasureTheory.Function.LpSeminorm.Basic` `Mathlib.MeasureTheory.Measure.Lebesgue.Complex` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.Probability.ProbabilityMassFunction.Monad` `Mathlib.MeasureTheory.Measure.Regular` `Mathlib.MeasureTheory.Integral.IntervalIntegral` `Mathlib.MeasureTheory.Group.MeasurableEquiv` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Probability.Kernel.Disintegration.CDFToKernel` `Mathlib.MeasureTheory.Order.Lattice` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Geometry.Manifold.Complex` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.Probability.StrongLaw` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Probability.Kernel.Composition.MeasureCompProd` `Mathlib.Probability.Kernel.Composition.IntegralCompProd` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Function.L2Space` `Mathlib.MeasureTheory.Measure.LevyProkhorovMetric` `Mathlib.Algebra.Module.ZLattice.Covolume` `Mathlib.MeasureTheory.Function.ContinuousMapDense` `Mathlib.Analysis.Complex.Periodic` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.MeasureTheory.Order.Group.Lattice` `Mathlib.Analysis.BoxIntegral.Partition.Measure` `Mathlib.MeasureTheory.Group.Measure` `Mathlib.Analysis.Fourier.AddCircleMulti` `Mathlib.Probability.Martingale.Upcrossing` `Mathlib.MeasureTheory.Function.SimpleFuncDenseLp` `Mathlib.Probability.Martingale.OptionalSampling` `Mathlib.MeasureTheory.Integral.DivergenceTheorem` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.MeasureTheory.Measure.LogLikelihoodRatio` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.MeasureTheory.Measure.ContinuousPreimage` `Mathlib.MeasureTheory.Function.LpSeminorm.Trim` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.MeasureTheory.Function.LpSpace` `Mathlib.MeasureTheory.Group.Arithmetic` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.Probability.Kernel.Composition.ParallelComp` `Mathlib.Dynamics.Ergodic.MeasurePreserving` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.MeasureTheory.Function.AEMeasurableOrder` `Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls` `Mathlib.MeasureTheory.Integral.FundThmCalculus` `Mathlib.MeasureTheory.Category.MeasCat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.MeasureTheory.Measure.Portmanteau` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.MeasureTheory.Constructions.Pi` `Mathlib.MeasureTheory.Measure.Haar.NormedSpace` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.MeasureTheory.Decomposition.UnsignedHahn` `Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality` `Mathlib.Dynamics.Ergodic.Conservative` `Mathlib.NumberTheory.NumberField.Completion` `Mathlib.Probability.Kernel.WithDensity` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable` `Mathlib.MeasureTheory.Group.AddCircle` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.MeasureTheory.Function.UniformIntegrable` `Mathlib.MeasureTheory.Measure.Hausdorff` `Mathlib.Probability.Distributions.Gaussian` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Analysis.Calculus.FDeriv.Measurable` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.MeasureTheory.Integral.Bochner` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.MeasureTheory.Measure.Haar.Unique` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Probability.Martingale.Basic` `Mathlib.MeasureTheory.Measure.Content` `Mathlib.MeasureTheory.Decomposition.RadonNikodym` `Mathlib.Probability.Kernel.RadonNikodym` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.MeasureTheory.Decomposition.SignedLebesgue` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.MeasureTheory.Decomposition.Exhaustion` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.MeasureTheory.Measure.Sub` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosed` `Mathlib.MeasureTheory.Group.GeometryOfNumbers` `Mathlib.MeasureTheory.Measure.GiryMonad` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.MeasureTheory.Covering.LiminfLimsup` `Mathlib.Probability.ProbabilityMassFunction.Constructions` `Mathlib.Probability.Kernel.Composition.Basic` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.MeasureTheory.Function.AEEqFun.DomAct` `Mathlib.Probability.Martingale.Convergence` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.Analysis.Convex.Integral` `Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace` `Mathlib.Probability.Kernel.Proper` `Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan` `Mathlib.MeasureTheory.Measure.Trim` `Mathlib.MeasureTheory.Integral.Prod` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.MeasureTheory.Integral.Layercake` `Mathlib.MeasureTheory.Decomposition.Jordan` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Analysis.Fourier.FourierTransformDeriv` `Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.MeasureTheory.Covering.OneDim` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.MeasureTheory.Group.LIntegral` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.Probability.Kernel.Invariance` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Probability.Distributions.Uniform` `Mathlib.MeasureTheory.Covering.DensityTheorem` `Mathlib.MeasureTheory.Integral.LebesgueNormedSpace` `Mathlib.Probability.ProbabilityMassFunction.Binomial` `Mathlib.MeasureTheory.Constructions.UnitInterval` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.Probability.Kernel.MeasurableIntegral` `Mathlib.MeasureTheory.Group.Pointwise` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.Probability.Distributions.Poisson` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.Fermat` `Mathlib.MeasureTheory.Integral.Asymptotics` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Probability.ConditionalProbability` `Mathlib.Analysis.BoxIntegral.Basic` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani` `Mathlib.Analysis.BoxIntegral.Integrability` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic` `Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving` `Mathlib.MeasureTheory.Function.L1Space` `Mathlib.MeasureTheory.Measure.Count` `Mathlib.Probability.Kernel.Disintegration.Basic` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.Probability.Kernel.Basic` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.Analysis.Complex.Liouville` `Mathlib.MeasureTheory.Group.AEStabilizer` `Mathlib.NumberTheory.Transcendental.Liouville.Measure` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.Probability.ProbabilityMassFunction.Basic` `Mathlib.MeasureTheory.Function.Jacobian` `Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.NumberTheory.LSeries.Positivity` `Mathlib.MeasureTheory.Function.LpOrder` `Mathlib.Analysis.Convex.Measure` `Mathlib.Probability.Moments` `Mathlib.Topology.Baire.BaireMeasurable` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.Topology.MetricSpace.HausdorffDimension` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.MeasureTheory.Group.FundamentalDomain` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.MeasureTheory.Group.Convolution` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.MeasureTheory.Decomposition.Lebesgue` `Mathlib.Dynamics.Ergodic.Ergodic` `Mathlib.MeasureTheory.Measure.OpenPos` `Mathlib.MeasureTheory.Function.LocallyIntegrable` `Mathlib.MeasureTheory.Measure.Dirac` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.MeasureTheory.Decomposition.SignedHahn` `Mathlib.Probability.Process.Stopping` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.MeasureTheory.Integral.MeanInequalities` `Mathlib.MeasureTheory.Integral.BoundedContinuousFunction` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.Dynamics.Ergodic.Action.OfMinimal` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.MeasureTheory.Measure.Stieltjes` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Dynamics.Ergodic.Action.Regular` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.MeasureTheory.VectorMeasure.WithDensity` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.MeasureTheory.Integral.DominatedConvergence` `Mathlib.NumberTheory.ZetaValues` `Mathlib.MeasureTheory.Function.Egorov` `Mathlib.Probability.Independence.Basic` `Mathlib.Analysis.Complex.Positivity` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas` `Mathlib.MeasureTheory.Function.ConvergenceInMeasure` `Mathlib.Analysis.Fourier.FourierTransform` `Mathlib.Probability.Independence.Integrable` `Mathlib.MeasureTheory.Function.AEEqOfLIntegral` `Mathlib.Probability.IdentDistrib` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.Convolution` `Mathlib.MeasureTheory.Covering.Vitali` `Mathlib.MeasureTheory.VectorMeasure.Basic` `Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Geometry.Manifold.PartitionOfUnity` `Mathlib.Dynamics.Ergodic.Function` `Mathlib.MeasureTheory.Measure.SeparableMeasure` `Mathlib.MeasureTheory.Covering.Differentiation` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Analysis.BoundedVariation` `Mathlib.MeasureTheory.Measure.Restrict` `Mathlib.NumberTheory.WellApproximable` `Mathlib.MeasureTheory.Measure.Lebesgue.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Distributions.Pareto` `Mathlib.MeasureTheory.Measure.Lebesgue.Integral` `Mathlib.MeasureTheory.Measure.MutuallySingular` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Probability.Independence.Kernel` `Mathlib.MeasureTheory.Group.Prod` `Mathlib.MeasureTheory.Integral.Pi` `Mathlib.NumberTheory.NumberField.House` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.MeasureTheory.Function.Intersectivity` `Mathlib.MeasureTheory.Measure.Typeclasses` `Mathlib.Probability.Process.Filtration` `Mathlib.MeasureTheory.Integral.Periodic` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Integral.IntegrableOn` `Mathlib.MeasureTheory.Measure.Prod` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.MeasureTheory.Integral.SetToL1` `Mathlib.Probability.Kernel.Condexp` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator` `Mathlib.MeasureTheory.Measure.AEMeasurable` `Mathlib.MeasureTheory.Measure.WithDensity` `Mathlib.MeasureTheory.Function.AEEqFun` `Mathlib.MeasureTheory.Function.SimpleFuncDense` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.Probability.Kernel.MeasurableLIntegral` `Mathlib.MeasureTheory.Covering.Besicovitch` `Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Dynamics.Ergodic.Action.Basic` `Mathlib.Probability.Martingale.OptionalStopping` `Mathlib.Probability.Martingale.BorelCantelli` `Mathlib.MeasureTheory.Constructions.Projective` `Mathlib.MeasureTheory.Group.Action` `Mathlib.Probability.Density` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Probability.ProbabilityMassFunction.Integrals` `Mathlib.Analysis.Calculus.BumpFunction.Normed` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.Probability.ConditionalExpectation` `Mathlib.MeasureTheory.Measure.Haar.Basic` `Mathlib.MeasureTheory.Integral.SetIntegral` `Mathlib.MeasureTheory.Constructions.BorelSpace.Real` `Mathlib.MeasureTheory.Constructions.BorelSpace.Order` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.Tactic` `Mathlib.MeasureTheory.Integral.Indicator` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.MeasureTheory.Group.Integral` `Mathlib.MeasureTheory.Measure.Haar.Disintegration` `Mathlib.MeasureTheory.Measure.EverywherePos` `Mathlib.Probability.Integration` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.MeasureTheory.Function.EssSup` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.Analysis.SpecialFunctions.Gamma.Deriv` `Mathlib.Analysis.BoxIntegral.DivergenceTheorem` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.Probability.UniformOn` `Mathlib.Probability.Kernel.Integral` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.Probability.Independence.Conditional` `Mathlib.NumberTheory.AbelSummation` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.MeasureTheory.Integral.Lebesgue` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Real` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Notation` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.Probability.CDF` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal` `Mathlib.MeasureTheory.Measure.Haar.OfBasis` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.Probability.Martingale.Centering` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.MeasureTheory.Measure.Haar.Quotient`	3
`Mathlib.MeasureTheory.Measure.Map` (new file)	1329
`Mathlib.MeasureTheory.Measure.AbsolutelyContinuous` (new file)	1330
`Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving` (new file)	1332

Declarations diff

+ AEDisjoint.of_absolutelyContinuous
+ AEDisjoint.of_le
- _root_.MeasureTheory.AEDisjoint.of_absolutelyContinuous
- _root_.MeasureTheory.AEDisjoint.of_le

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.

Decrease in tech debt: (relative, absolute) = (1.00, 0.02)

Current number	Change	Type
57	-1	large files

Current commit 4cc2077e63
Reference commit 2590de306b

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

loefflerd

Splitting files is always an unpleasant job, thanks for taking this on!

Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean

Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean

Mathlib/MeasureTheory/Measure/Map.lean

loefflerd · 2025-01-07T16:19:22Z

LGTM

maintainer merge

github-actions · 2025-01-07T16:19:42Z

🚀 Pull request has been placed on the maintainer queue by loefflerd.

sgouezel · 2025-01-07T20:20:38Z

bors r+
Thanks!

The MeasureSpace file contains many definitions about measures and is 2000 lines long. This PR splits 3 files by taking material from the bottom of MeasureSpace: - Map: map of a measure by a function - AbsolutelyContinuous: absolute continuity of measures - QuasiMeasurePreserving: quasi measure preserving functions Co-authored-by: Remy Degenne <remydegenne@gmail.com>

mathlib-bors · 2025-01-07T21:11:01Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (642 commits) feat: the Boolean subalgebra generated by the lattice generated by a set (#20440) feat: misc. lemmas about moments, tilted measures (#20150) chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556) feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373) feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377) chore: scope 'on' notation to Function (#20562) chore: disable docPrime linter (#20559) chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557) fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539) chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551) feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542) chore(Noetherian/Artinian): generalize to Semiring (#20534) chore: protect `Filter.nhds_{iInf,inf}` (#20530) chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511) chore: extract 3 new files out of MeasureSpace (#20509) feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326) doc(RingTheory/Flat): add reference to Lambek's paper (#20266) feat(NumberTheory/AbelSummation): add more results (#19942) chore(Multilinear/Basic): generalize the `SMul` instance (#20536) feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516) feat(ContDiff): add `iteratedFDeriv_comp` (#20472) feat(LowerUpperTopology): add lemmas (#20465) feat(ContDiff): weaken some assumptions (#20368) fix(scripts/technical-debt-metric): avoid division by 0 (#20537) chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528) feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089) feat: results on inner regularity of finite measures (#19780) chore: to_additive various results on groups, group actions (#20547) feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466) chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553) perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524) fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529) chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535) feat(RingTheory): being unramified is a local property (#20323) chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439) feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970) chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255) chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235) chore: don't import algebra in `Data.Finset.Basic` (#19779) feat: initial segment commutes with `Iio` (#20503) chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215) chore: smile more often (#20436) chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416) feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007) doc: change "module homomorphism" to "linear map" (#20481) perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519) fix: do not keep only the first line of hints (#19756) feat(Analysis/Analytic): lemmas about `smul` for power series (#19816) chore: don't import algebra in `Data.Multiset.Basic` (#19775) ...

* origin/master: (80 commits) chore(CategoryTheory): remove data produced by tactic block (#20565) feat: `|∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ` (#20540) feat: the Boolean subalgebra generated by the lattice generated by a set (#20440) feat: misc. lemmas about moments, tilted measures (#20150) chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556) feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373) feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377) chore: scope 'on' notation to Function (#20562) chore: disable docPrime linter (#20559) chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557) fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539) chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551) feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542) chore(Noetherian/Artinian): generalize to Semiring (#20534) chore: protect `Filter.nhds_{iInf,inf}` (#20530) chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511) chore: extract 3 new files out of MeasureSpace (#20509) feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326) doc(RingTheory/Flat): add reference to Lambek's paper (#20266) feat(NumberTheory/AbelSummation): add more results (#19942) chore(Multilinear/Basic): generalize the `SMul` instance (#20536) feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516) feat(ContDiff): add `iteratedFDeriv_comp` (#20472) feat(LowerUpperTopology): add lemmas (#20465) feat(ContDiff): weaken some assumptions (#20368) fix(scripts/technical-debt-metric): avoid division by 0 (#20537) chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528) feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089) feat: results on inner regularity of finite measures (#19780) chore: to_additive various results on groups, group actions (#20547) feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466) chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553) perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524) fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529) chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535) feat(RingTheory): being unramified is a local property (#20323) chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439) feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970) chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255) chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235) chore: don't import algebra in `Data.Finset.Basic` (#19779) feat: initial segment commutes with `Iio` (#20503) chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215) chore: smile more often (#20436) chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416) feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007) doc: change "module homomorphism" to "linear map" (#20481) perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519) fix: do not keep only the first line of hints (#19756) ...

RemyDegenne and others added 13 commits January 4, 2025 14:05

wip

3aa7e58

done

cbb6d04

split MeasureSpace

2bede71

fix long file length

8336423

fix imports

5204590

unsimp

7205252

split Map

fc49551

file docstrings

6d206e8

Merge remote-tracking branch 'origin/RD_measureSpace' into RD_split

9fc58ef

delete

1a50316

Merge remote-tracking branch 'origin/master' into RD_split

972bc66

mk_all

ad45ced

imports

6e726bf

RemyDegenne added the t-measure-probability Measure theory / Probability theory label Jan 6, 2025

loefflerd reviewed Jan 7, 2025

View reviewed changes

RemyDegenne added 2 commits January 7, 2025 16:22

review

b752adf

remove delta

4cc2077

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 7, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Jan 7, 2025

mathlib-bors bot changed the title ~~chore: extract 3 new files out of MeasureSpace~~ [Merged by Bors] - chore: extract 3 new files out of MeasureSpace Jan 7, 2025

mathlib-bors bot closed this Jan 7, 2025

mathlib-bors bot deleted the RD_split branch January 7, 2025 21:11

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: extract 3 new files out of MeasureSpace#20509

[Merged by Bors] - chore: extract 3 new files out of MeasureSpace#20509
RemyDegenne wants to merge 15 commits intomasterfrom
RD_split

RemyDegenne commented Jan 6, 2025

Uh oh!

github-actions bot commented Jan 6, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

loefflerd left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

loefflerd commented Jan 7, 2025

Uh oh!

github-actions bot commented Jan 7, 2025

Uh oh!

sgouezel commented Jan 7, 2025

Uh oh!

mathlib-bors bot commented Jan 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

RemyDegenne commented Jan 6, 2025

Uh oh!

github-actions bot commented Jan 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 4cc2077e63

Import changes for modified files

Declarations diff

Uh oh!

loefflerd left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

loefflerd commented Jan 7, 2025

Uh oh!

github-actions bot commented Jan 7, 2025

Uh oh!

sgouezel commented Jan 7, 2025

Uh oh!

mathlib-bors bot commented Jan 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions bot commented Jan 6, 2025 •

edited

Loading