[Merged by Bors] - chore(Measure/Pi): move parts to MeasurableSpace/#20215
Closed
[Merged by Bors] - chore(Measure/Pi): move parts to MeasurableSpace/#20215
MeasurableSpace/#20215Conversation
PR summary 2df3b8fa33
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Probability.Independence.Kernel | 1388 | 1372 | -16 (-1.15%) |
| Mathlib.Probability.Independence.Basic | 1389 | 1375 | -14 (-1.01%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Probability.Independence.Kernel |
-16 |
Mathlib.Probability.Independence.Basic |
-14 |
7 filesMathlib.Probability.BorelCantelli Mathlib.Probability.Variance Mathlib.Probability.Moments Mathlib.Probability.Independence.Integrable Mathlib.Probability.IdentDistrib Mathlib.Probability.ConditionalExpectation Mathlib.Probability.Integration |
-7 |
223 filesMathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.MeasureTheory.Integral.Marginal Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.NumberTheory.GaussSum Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Complex.AbsMax Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Geometry.Manifold.Complex Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw 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.Measure.LevyProkhorovMetric Mathlib.Algebra.Module.ZLattice.Covolume 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.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Algebra.Module.ZLattice.Basic Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Integral.FundThmCalculus 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.Measure.Lebesgue.EqHaar Mathlib.Analysis.Fourier.Inversion Mathlib.NumberTheory.NumberField.Completion Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.SpecialFunctions.NonIntegrable 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.Measure.Hausdorff Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Kernel.CondDistrib Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Probability.Kernel.RadonNikodym Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Probability.Kernel.Composition.Basic Mathlib.MeasureTheory.Order.UpperLower Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Disintegration.Density Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Integral.Prod Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake 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.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Probability.Kernel.Invariance Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.Fermat Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.Integrability Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Liouville Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.MeasureTheory.Function.Jacobian Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.NumberTheory.LSeries.Positivity Mathlib.Analysis.Convex.Measure Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Units.DirichletTheorem 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.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.Calculus.Monotone 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.Analysis.Fourier.FourierTransform Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.Convolution Mathlib.Analysis.MellinInversion Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.BoundedVariation Mathlib.NumberTheory.WellApproximable Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Probability.Distributions.Pareto Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.Analysis.Calculus.Rademacher Mathlib.MeasureTheory.Integral.Pi Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Integral.Periodic Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Analysis.MellinTransform Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.MeasureTheory.Integral.Gamma Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Probability.Kernel.Condexp Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Probability.Distributions.Gamma Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.ODE.PicardLindelof Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Probability.Independence.Conditional Mathlib.NumberTheory.AbelSummation Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Data.Real.Pi.Wallis Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.Probability.CDF Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient |
1 |
Mathlib.MeasureTheory.MeasurableSpace.Pi (new file) |
667 |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
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.
Increase in tech debt: (relative, absolute) = (1.00, 0.01)
| Current number | Change | Type |
|---|---|---|
| 106 | 1 | bare open (scoped) Classical |
Current commit 2df3b8fa33
Reference commit 0571c82877
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).
Contributor
|
Can you fix the merge conflict and add the missing module docstring? |
Member
Author
|
@RemyDegenne Done. |
Contributor
|
Thanks! |
Contributor
|
Pull request successfully merged into master. Build succeeded: |
MeasurableSpace/MeasurableSpace/
Julian
added a commit
that referenced
this pull request
Jan 8, 2025
* 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) ...
Julian
added a commit
that referenced
this pull request
Jan 8, 2025
* 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) ...
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
3 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.
New file needs a module docstring, otherwise should be ready.