chore(MeasureTheory): remove the dependence of the Lebesgue decomposition on Bochner integrals#19278
Closed
RemyDegenne wants to merge 18 commits intomasterfrom
Closed
chore(MeasureTheory): remove the dependence of the Lebesgue decomposition on Bochner integrals#19278RemyDegenne wants to merge 18 commits intomasterfrom
RemyDegenne wants to merge 18 commits intomasterfrom
Conversation
PR summary 15186c2643
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Probability.Kernel.Composition | 1931 | 1344 | -587 (-30.40%) |
| Mathlib.MeasureTheory.Decomposition.RadonNikodym | 1905 | 1384 | -521 (-27.35%) |
| Mathlib.MeasureTheory.Decomposition.Lebesgue | 1900 | 1383 | -517 (-27.21%) |
| Mathlib.Probability.Kernel.WithDensity | 1931 | 1881 | -50 (-2.59%) |
| Mathlib.MeasureTheory.Measure.Tilted | 1906 | 1898 | -8 (-0.42%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Probability.Kernel.Composition Mathlib.Probability.Kernel.Invariance |
-587 |
Mathlib.MeasureTheory.Decomposition.RadonNikodym |
-521 |
Mathlib.MeasureTheory.Measure.WithDensityFinite |
-520 |
Mathlib.MeasureTheory.Decomposition.Lebesgue |
-517 |
Mathlib.Probability.Kernel.WithDensity |
-50 |
Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.CDF |
-34 |
Mathlib.Probability.Kernel.Disintegration.CDFToKernel |
-31 |
Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Kernel.Disintegration.Density |
-21 |
4 filesMathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Covering.Besicovitch |
-19 |
Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Tilted |
-8 |
11 filesMathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.MeasureTheory.Order.UpperLower Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Covering.OneDim Mathlib.MeasureTheory.Function.Jacobian Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.BoundedVariation Mathlib.NumberTheory.WellApproximable |
-4 |
53 filesMathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Analysis.Fourier.PoissonSummation Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.NumberTheory.LSeries.ZMod Mathlib.Probability.Distributions.Exponential Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.Fourier.Inversion Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.Cyclotomic.PID Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Analysis.MellinInversion Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Probability.Distributions.Pareto Mathlib.Analysis.MellinTransform Mathlib.MeasureTheory.Integral.Gamma Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Probability.Distributions.Gamma Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.NumberTheory.LSeries.AbstractFuncEq |
-1 |
148 filesMathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Function.UnifTight Mathlib.NumberTheory.GaussSum Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Geometry.Manifold.Complex Mathlib.MeasureTheory.Integral.CircleIntegral 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.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Algebra.Module.ZLattice.Basic Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.Analysis.Fourier.AddCircle Mathlib.NumberTheory.NumberField.Completion Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.MeasureTheory.Group.AddCircle Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Integral.Bochner Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Integral.Prod Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Complex.Schwarz Mathlib.Data.Real.Pi.Leibniz Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.Fermat Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.BoxIntegral.Integrability Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.L1Space Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Liouville Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.JacobiSum.Basic Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Analysis.Normed.Algebra.Basic Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.RingTheory.Polynomial.Selmer Mathlib.Analysis.SumIntegralComparisons Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.NumberTheory.ZetaValues Mathlib.Analysis.Complex.Positivity Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.Analysis.Fourier.FourierTransform Mathlib.Probability.Independence.Integrable Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.Convolution Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.MeasureTheory.Integral.Pi Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Integral.Periodic Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Measure.WithDensity Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Complex.OpenMapping Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.ODE.PicardLindelof Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.Tactic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Probability.Integration Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.MeasureTheory.Integral.Average Mathlib.Probability.Kernel.Integral Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Data.Real.Pi.Wallis Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient |
1 |
13 filesMathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.Probability.Kernel.IntegralCompProd Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Analysis.Convex.Integral Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.Probability.Kernel.MeasureCompProd Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator |
2 |
8 filesMathlib.Probability.Variance Mathlib.Probability.StrongLaw Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Moments Mathlib.Probability.IdentDistrib Mathlib.Analysis.Calculus.Rademacher Mathlib.Probability.ConditionalExpectation Mathlib.Probability.Notation |
3 |
Mathlib.MeasureTheory.Decomposition.SignedLebesgue |
5 |
16 filesMathlib.Probability.Process.HittingTime Mathlib.Probability.BorelCantelli Mathlib.Probability.Martingale.Upcrossing Mathlib.Probability.Martingale.OptionalSampling Mathlib.Probability.Martingale.Basic Mathlib.Probability.Martingale.Convergence Mathlib.Probability.Distributions.Uniform Mathlib.Probability.Process.Stopping Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Density Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Martingale.Centering |
7 |
7 filesMathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Independence.Conditional |
8 |
Mathlib.MeasureTheory.Decomposition.SigmaFiniteSet |
1308 |
Mathlib.MeasureTheory.Decomposition.ExhaustionFun |
1337 |
Mathlib.Probability.Kernel.MeasurableLIntegral |
1341 |
Mathlib.MeasureTheory.Decomposition.LebesgueDecomposition |
1343 |
Mathlib.MeasureTheory.Function.AEEqOfLIntegral |
1378 |
Mathlib.MeasureTheory.Decomposition.IntegralRNDeriv |
1898 |
Mathlib.MeasureTheory.Decomposition.SignedRadonNikodym |
1912 |
Declarations diff
+ ENNReal.aefinStronglyMeasurable_of_aemeasurable
+ ENNReal.finStronglyMeasurable_of_measurable
+ Measure.funGE
+ Measure.maximalFun
+ Measure.maximalSet
+ Measure.pSetGE
+ SimpleFunc.lintegral_le_lintegral
+ SimpleFunc.measure_support_eapprox_lt_top
+ SimpleFunc.measure_support_lt_top'
+ SimpleFunc.measure_support_lt_top_of_lintegral_ne_top
+ SimpleFunc.tendsto_eapprox
+ exists_fun_lintegral_ge
+ exists_set_measure_ge
+ lintegral_funGE_ge
+ lintegral_funGE_le
+ lintegral_maximalFun
+ measurableSet_maximalSet
+ measurableSet_pSetGE
+ measurable_funGE
+ measurable_maximalFun
+ measure_maximalSet
+ measure_pSetGE_ge
+ measure_pSetGE_le
+ not_prop_of_subset_compl_maximalSet
+ prop_funGE
+ prop_maximalFun
+ prop_maximalSet
+ prop_pSetGE
+ sigmaFinite_iUnion
+ tendsto_lintegral_funGE
+ tendsto_measure_pSetGE
- Measure.sigmaFiniteSetGE
- exists_isSigmaFiniteSet_measure_ge
- measurableSet_sigmaFiniteSetGE
- measure_sigmaFiniteSetGE_ge
- measure_sigmaFiniteSetGE_le
- sigmaFinite_restrict_sigmaFiniteSetGE
- tendsto_measure_sigmaFiniteSetGE
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.00)
| Current number | Change | Type |
|---|---|---|
| 219 | -1 | bare open (scoped) Classical |
Current commit 15186c2643
Reference commit d6d7113602
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
This was referenced Jan 2, 2025
Contributor
Author
|
This is not useful anymore. Closing. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
WIP. This PR has become a huge mess. I will open other PRs for the useful parts and then close it.