mathlib4 feat: Prokhorov theorem

We prove a version of Prokhorov theorem: given a sequence of compact sets Kₙ and a sequence uₙ tending to zero, the probability measures giving mass at most uₙ to the complement of Kₙ form a compact set. We deduce that a tight set of probability measures has compact closure. We only assume that the space is T2 (no metrizability, no second-countability).

The PR is somewhat long, but to me it looks like a coherent unit, so it makes sense to keep it like that. If you think it's too long to review and you'd rather have smaller chunks, just tell me and I'll split it.

[x] depends on: #32778
[x] depends on: #32779
[x] depends on: #32783
[x] depends on: #32784
[x] depends on: #32785
[x] depends on: #32786

Dec 10 '25 20:12 sgouezel

PR summary 1119dd2d7c

Import changes exceeding 2%

%	File
+5.15%	`Mathlib.Order.Disjointed`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.Disjointed	388	408	+20 (+5.15%)

Import changes for all files

Files	Import difference
12 files `Mathlib.Algebra.CharP.LinearMaps` `Mathlib.Algebra.Module.Torsion.Basic` `Mathlib.LinearAlgebra.Reflection` `Mathlib.RepresentationTheory.Maschke` `Mathlib.RingTheory.AdicCompletion.Algebra` `Mathlib.RingTheory.AdicCompletion.Functoriality` `Mathlib.RingTheory.AdicCompletion.RingHom` `Mathlib.RingTheory.Jacobson.Semiprimary` `Mathlib.RingTheory.SimpleModule.Basic` `Mathlib.RingTheory.SimpleModule.InjectiveProjective` `Mathlib.RingTheory.SimpleModule.Isotypic` `Mathlib.Topology.Algebra.Module.Simple`	1
179 files `Mathlib.Algebra.Category.CommAlgCat.Basic` `Mathlib.Algebra.Category.CommAlgCat.Monoidal` `Mathlib.Algebra.Category.CommBialgCat` `Mathlib.Algebra.Category.Grp.EnoughInjectives` `Mathlib.Algebra.Category.Grp.LargeColimits` `Mathlib.Algebra.Category.Grp.Ulift` `Mathlib.Algebra.Category.ModuleCat.EnoughInjectives` `Mathlib.Algebra.Category.Ring.Constructions` `Mathlib.Algebra.Category.Ring.Epi` `Mathlib.Algebra.Category.Ring.Instances` `Mathlib.Algebra.Category.Ring.Topology` `Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Algebra.CharP.CharAndCard` `Mathlib.Algebra.CharP.LocalRing` `Mathlib.Algebra.CharP.MixedCharZero` `Mathlib.Algebra.CharP.Quotient` `Mathlib.Algebra.CharP.Two` `Mathlib.Algebra.DirectSum.Idempotents` `Mathlib.Algebra.FreeAlgebra.Cardinality` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.Algebra.Module.CharacterModule` `Mathlib.Algebra.Module.ZMod` `Mathlib.Algebra.MvPolynomial.Cardinal` `Mathlib.Algebra.MvPolynomial.Expand` `Mathlib.Algebra.MvPolynomial.Nilpotent` `Mathlib.Algebra.Order.Group.Cyclic` `Mathlib.Algebra.Polynomial.GroupRingAction` `Mathlib.Algebra.Polynomial.Homogenize` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.Analysis.Polynomial.CauchyBound` `Mathlib.Combinatorics.Nullstellensatz` `Mathlib.Data.Nat.Totient` `Mathlib.Data.ZMod.Coprime` `Mathlib.Data.ZMod.QuotientRing` `Mathlib.Dynamics.Newton` `Mathlib.FieldTheory.PrimeField` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace` `Mathlib.Geometry.RingedSpace.OpenImmersion` `Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing` `Mathlib.GroupTheory.ArchimedeanDensely` `Mathlib.GroupTheory.CommutingProbability` `Mathlib.GroupTheory.Frattini` `Mathlib.GroupTheory.Nilpotent` `Mathlib.GroupTheory.PGroup` `Mathlib.GroupTheory.Perm.MaximalSubgroups` `Mathlib.GroupTheory.RegularWreathProduct` `Mathlib.GroupTheory.Schreier` `Mathlib.GroupTheory.SchurZassenhaus` `Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour` `Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups` `Mathlib.GroupTheory.SpecificGroups.Cyclic` `Mathlib.GroupTheory.SpecificGroups.Dihedral` `Mathlib.GroupTheory.SpecificGroups.KleinFour` `Mathlib.GroupTheory.SpecificGroups.Quaternion` `Mathlib.GroupTheory.Sylow` `Mathlib.GroupTheory.Torsion` `Mathlib.GroupTheory.Transfer` `Mathlib.LinearAlgebra.Dual.BaseChange` `Mathlib.LinearAlgebra.Matrix.Adjugate` `Mathlib.LinearAlgebra.Matrix.FixedDetMatrices` `Mathlib.LinearAlgebra.Matrix.Ideal` `Mathlib.LinearAlgebra.Matrix.Nondegenerate` `Mathlib.LinearAlgebra.Matrix.Polynomial` `Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup` `Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup` `Mathlib.LinearAlgebra.Transvection` `Mathlib.ModelTheory.Algebra.Field.CharP` `Mathlib.ModelTheory.Algebra.Ring.FreeCommRing` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.NumberTheory.Bernoulli` `Mathlib.NumberTheory.DirichletCharacter.Basic` `Mathlib.NumberTheory.FLT.Four` `Mathlib.NumberTheory.LegendreSymbol.ZModChar` `Mathlib.NumberTheory.LucasPrimality` `Mathlib.NumberTheory.MulChar.Basic` `Mathlib.NumberTheory.PrimeCounting` `Mathlib.NumberTheory.PythagoreanTriples` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.RingTheory.AdicCompletion.LocalRing` `Mathlib.RingTheory.AdicCompletion.Topology` `Mathlib.RingTheory.Algebraic.Cardinality` `Mathlib.RingTheory.AlgebraicIndependent.Basic` `Mathlib.RingTheory.Binomial` `Mathlib.RingTheory.Derivation.ToSquareZero` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.RingTheory.DividedPowers.SubDPIdeal` `Mathlib.RingTheory.DualNumber` `Mathlib.RingTheory.Finiteness.NilpotentKer` `Mathlib.RingTheory.HahnSeries.Binomial` `Mathlib.RingTheory.Henselian` `Mathlib.RingTheory.Ideal.AssociatedPrime.Basic` `Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient` `Mathlib.RingTheory.Ideal.MinimalPrime.Basic` `Mathlib.RingTheory.Ideal.MinimalPrime.Localization` `Mathlib.RingTheory.Ideal.Over` `Mathlib.RingTheory.Ideal.Quotient.Basic` `Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder` `Mathlib.RingTheory.Ideal.Quotient.Index` `Mathlib.RingTheory.Ideal.Quotient.Nilpotent` `Mathlib.RingTheory.Ideal.Quotient.Operations` `Mathlib.RingTheory.Idempotents` `Mathlib.RingTheory.IntegralDomain` `Mathlib.RingTheory.Jacobson.Ideal` `Mathlib.RingTheory.LocalProperties.Exactness` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.RingTheory.LocalRing.LocalSubring` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.RingTheory.LocalRing.NonLocalRing` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.RingTheory.LocalRing.ResidueField.Ideal` `Mathlib.RingTheory.LocalRing.RingHom.Basic` `Mathlib.RingTheory.Localization.Algebra` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.AtPrime.Basic` `Mathlib.RingTheory.Localization.AtPrime` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.RingTheory.MatrixPolynomialAlgebra` `Mathlib.RingTheory.MvPolynomial.EulerIdentity` `Mathlib.RingTheory.MvPolynomial.Expand` `Mathlib.RingTheory.MvPolynomial.Groebner` `Mathlib.RingTheory.MvPolynomial.Homogeneous` `Mathlib.RingTheory.MvPolynomial.Ideal` `Mathlib.RingTheory.MvPolynomial.Localization` `Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex` `Mathlib.RingTheory.MvPolynomial.MonomialOrder` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.Polynomial.Chebyshev` `Mathlib.RingTheory.Polynomial.ContentIdeal` `Mathlib.RingTheory.Polynomial.Dickson` `Mathlib.RingTheory.Polynomial.Eisenstein.Basic` `Mathlib.RingTheory.Polynomial.Eisenstein.Criterion` `Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished` `Mathlib.RingTheory.Polynomial.IrreducibleRing` `Mathlib.RingTheory.Polynomial.Nilpotent` `Mathlib.RingTheory.PowerSeries.Binomial` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.RingTheory.PowerSeries.WeierstrassPreparation` `Mathlib.RingTheory.Regular.Category` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.RingHomProperties` `Mathlib.RingTheory.RootsOfUnity.Basic` `Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits` `Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity` `Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots` `Mathlib.RingTheory.SimpleRing.Matrix` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.RingTheory.TensorProduct.Finite` `Mathlib.RingTheory.TensorProduct.IsBaseChangeHom` `Mathlib.RingTheory.TensorProduct.Quotient` `Mathlib.RingTheory.Valuation.Archimedean` `Mathlib.RingTheory.Valuation.Extension` `Mathlib.RingTheory.Valuation.Quotient` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.RingTheory.WittVector.WittPolynomial` `Mathlib.RingTheory.ZMod` `Mathlib.SetTheory.Cardinal.Free` `Mathlib.SetTheory.Nimber.Field` `Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean` `Mathlib.Topology.Algebra.InfiniteSum.Ring` `Mathlib.Topology.Algebra.IntermediateField` `Mathlib.Topology.Algebra.IsOpenUnits` `Mathlib.Topology.Algebra.Module.CharacterSpace` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete` `Mathlib.Topology.Algebra.Star.Unitary` `Mathlib.Topology.Algebra.TopologicallyNilpotent` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuativeRel` `Mathlib.Topology.Algebra.Valued.ValuedField` `Mathlib.Topology.Algebra.Valued.WithZeroMulInt` `Mathlib.Topology.Instances.AddCircle.Defs` `Mathlib.Topology.Sheaves.CommRingCat` `Mathlib.Topology.UniformSpace.ProdApproximation`	2
49 files `Mathlib.Algebra.CubicDiscriminant` `Mathlib.Algebra.MvPolynomial.Funext` `Mathlib.Algebra.MvPolynomial.SchwartzZippel` `Mathlib.Algebra.Polynomial.CoeffMem` `Mathlib.Algebra.Polynomial.Degree.CardPowDegree` `Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree` `Mathlib.Algebra.Polynomial.Factors` `Mathlib.Algebra.Polynomial.FieldDivision` `Mathlib.Algebra.Polynomial.Laurent` `Mathlib.Algebra.Polynomial.Lifts` `Mathlib.Algebra.Polynomial.PartialFractions` `Mathlib.Algebra.Polynomial.RingDivision` `Mathlib.Algebra.Polynomial.Roots` `Mathlib.Algebra.Polynomial.RuleOfSigns` `Mathlib.Algebra.Polynomial.Sequence` `Mathlib.Algebra.Polynomial.SpecificDegree` `Mathlib.Algebra.Polynomial.Splits` `Mathlib.Algebra.Polynomial.SumIteratedDerivative` `Mathlib.Algebra.Polynomial.Taylor` `Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ` `Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms` `Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange` `Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass` `Mathlib.MeasureTheory.MeasurableSpace.NCard` `Mathlib.NumberTheory.FLT.MasonStothers` `Mathlib.NumberTheory.Multiplicity` `Mathlib.RingTheory.Bialgebra.MonoidAlgebra` `Mathlib.RingTheory.Coalgebra.MonoidAlgebra` `Mathlib.RingTheory.HahnSeries.PowerSeries` `Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra` `Mathlib.RingTheory.Localization.Away.Basic` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.RingTheory.Localization.Rat` `Mathlib.RingTheory.Polynomial.Content` `Mathlib.RingTheory.Polynomial.GaussNorm` `Mathlib.RingTheory.Polynomial.HilbertPoly` `Mathlib.RingTheory.Polynomial.Ideal` `Mathlib.RingTheory.Polynomial.IntegralNormalization` `Mathlib.RingTheory.Polynomial.Radical` `Mathlib.RingTheory.Polynomial.ScaleRoots` `Mathlib.RingTheory.Polynomial.SmallDegreeVieta` `Mathlib.RingTheory.Polynomial.Vieta` `Mathlib.RingTheory.PowerSeries.GaussNorm` `Mathlib.RingTheory.PowerSeries.NoZeroDivisors` `Mathlib.RingTheory.PowerSeries.Order` `Mathlib.RingTheory.TensorProduct.IsBaseChangeFree` `Mathlib.RingTheory.TensorProduct.IsBaseChangePi` `Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky` `Mathlib.RingTheory.Valuation.PrimeMultiplicity`	3
98 files `Mathlib.Algebra.Algebra.Spectrum.Basic` `Mathlib.Algebra.Algebra.Spectrum.Pi` `Mathlib.Algebra.Algebra.Spectrum.Quasispectrum` `Mathlib.Algebra.Algebra.StrictPositivity` `Mathlib.Algebra.Algebra.Subalgebra.Operations` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.Algebra.CharP.IntermediateField` `Mathlib.Algebra.Colimit.Ring` `Mathlib.Algebra.MvPolynomial.Derivation` `Mathlib.Algebra.MvPolynomial.Equiv` `Mathlib.Algebra.MvPolynomial.PDeriv` `Mathlib.Algebra.MvPolynomial.Polynomial` `Mathlib.Algebra.Order.Ring.Archimedean` `Mathlib.Algebra.Polynomial.AlgebraMap` `Mathlib.Algebra.Polynomial.Derivation` `Mathlib.Algebra.Polynomial.Module.AEval` `Mathlib.Algebra.Polynomial.Module.Basic` `Mathlib.Algebra.Polynomial.Module.TensorProduct` `Mathlib.Algebra.Polynomial.OfFn` `Mathlib.Algebra.Polynomial.Smeval` `Mathlib.Algebra.Ring.Subring.IntPolynomial` `Mathlib.Algebra.Star.UnitaryStarAlgAut` `Mathlib.Algebra.Star.Unitary` `Mathlib.FieldTheory.IntermediateField.Adjoin.Defs` `Mathlib.FieldTheory.IntermediateField.Basic` `Mathlib.LinearAlgebra.TensorProduct.Quotient` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.LinearAlgebra.TensorProduct.Vanishing` `Mathlib.NumberTheory.Basic` `Mathlib.NumberTheory.Dioph` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.RingTheory.Adjoin.Polynomial` `Mathlib.RingTheory.Algebraic.Defs` `Mathlib.RingTheory.Algebraic.LinearIndependent` `Mathlib.RingTheory.Algebraic.Pi` `Mathlib.RingTheory.Bezout` `Mathlib.RingTheory.Coprime.Ideal` `Mathlib.RingTheory.Derivation.Basic` `Mathlib.RingTheory.Derivation.DifferentialRing` `Mathlib.RingTheory.DividedPowers.Basic` `Mathlib.RingTheory.DividedPowers.DPMorphism` `Mathlib.RingTheory.DividedPowers.RatAlgebra` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.RingTheory.Finiteness.Ideal` `Mathlib.RingTheory.Finiteness.Nakayama` `Mathlib.RingTheory.Finiteness.Nilpotent` `Mathlib.RingTheory.FreeCommRing` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal` `Mathlib.RingTheory.GradedAlgebra.Radical` `Mathlib.RingTheory.HahnSeries.HEval` `Mathlib.RingTheory.HahnSeries.Valuation` `Mathlib.RingTheory.Ideal.Basic` `Mathlib.RingTheory.Ideal.Colon` `Mathlib.RingTheory.Ideal.IdempotentFG` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.RingTheory.Ideal.Maps` `Mathlib.RingTheory.Ideal.Oka` `Mathlib.RingTheory.Ideal.Operations` `Mathlib.RingTheory.Ideal.Pointwise` `Mathlib.RingTheory.Ideal.Prod` `Mathlib.RingTheory.Ideal.Quotient.PowTransition` `Mathlib.RingTheory.Int.Basic` `Mathlib.RingTheory.IsPrimary` `Mathlib.RingTheory.Jacobson.Radical` `Mathlib.RingTheory.Lasker` `Mathlib.RingTheory.MvPolynomial.FreeCommRing` `Mathlib.RingTheory.Nilpotent.Exp` `Mathlib.RingTheory.Nilpotent.Lemmas` `Mathlib.RingTheory.Noetherian.Nilpotent` `Mathlib.RingTheory.Noetherian.OfPrime` `Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain` `Mathlib.RingTheory.Polynomial.Bernstein` `Mathlib.RingTheory.Polynomial.ShiftedLegendre` `Mathlib.RingTheory.Polynomial.Tower` `Mathlib.RingTheory.Polynomial.Wronskian` `Mathlib.RingTheory.PolynomialAlgebra` `Mathlib.RingTheory.PowerSeries.Basic` `Mathlib.RingTheory.PowerSeries.Catalan` `Mathlib.RingTheory.PowerSeries.CoeffMulMem` `Mathlib.RingTheory.PowerSeries.Trunc` `Mathlib.RingTheory.PowerSeries.WellKnown` `Mathlib.RingTheory.PrincipalIdealDomainOfPrime` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.RingTheory.QuotSMulTop` `Mathlib.RingTheory.SimpleRing.Principal` `Mathlib.RingTheory.TensorProduct.MvPolynomial` `Mathlib.RingTheory.UniqueFactorizationDomain.Ideal` `Mathlib.RingTheory.Valuation.Basic` `Mathlib.RingTheory.Valuation.ExtendToLocalization` `Mathlib.RingTheory.Valuation.Integers` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.RingTheory.Valuation.ValuativeRel.Basic` `Mathlib.RingTheory.Valuation.ValuativeRel.Trivial` `Mathlib.RingTheory.Valuation.ValuativeRel`	4
`Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated` `Mathlib.Topology.Separation.DisjointCover`	5
3 files `Mathlib.MeasureTheory.Constructions.Cylinders` `Mathlib.MeasureTheory.SetAlgebra` `Mathlib.MeasureTheory.SetSemiring`	6
16 files `Mathlib.Algebra.CharP.Frobenius` `Mathlib.Algebra.CharP.Lemmas` `Mathlib.Algebra.CharP.Reduced` `Mathlib.Data.Nat.Choose.Factorization` `Mathlib.Data.Nat.Multiplicity` `Mathlib.MeasureTheory.Constructions.SubmoduleQuotient` `Mathlib.MeasureTheory.MeasurableSpace.Constructions` `Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated` `Mathlib.MeasureTheory.MeasurableSpace.Embedding` `Mathlib.MeasureTheory.MeasurableSpace.Pi` `Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict` `Mathlib.MeasureTheory.MeasurableSpace.Prod` `Mathlib.MeasureTheory.PiSystem` `Mathlib.NumberTheory.Padics.PadicNorm` `Mathlib.NumberTheory.Padics.PadicVal.Basic` `Mathlib.Probability.Kernel.IonescuTulcea.Maps`	7
`Mathlib.Algebra.Order.Antidiag.Nat`	8
8 files `Mathlib.Data.Nat.Squarefree` `Mathlib.NumberTheory.ArithmeticFunction.Defs` `Mathlib.NumberTheory.ArithmeticFunction.Misc` `Mathlib.NumberTheory.ArithmeticFunction.Moebius` `Mathlib.NumberTheory.ArithmeticFunction.Zeta` `Mathlib.NumberTheory.MaricaSchoenheim` `Mathlib.NumberTheory.SelbergSieve` `Mathlib.NumberTheory.SmoothNumbers`	9
8 files `Mathlib.Algebra.Polynomial.BigOperators` `Mathlib.Algebra.Polynomial.Degree.TrailingDegree` `Mathlib.Algebra.Polynomial.Div` `Mathlib.Algebra.Polynomial.HasseDeriv` `Mathlib.Algebra.Polynomial.Mirror` `Mathlib.Algebra.Polynomial.Monic` `Mathlib.Algebra.Polynomial.Reverse` `Mathlib.Algebra.Polynomial.UnitTrinomial`	10
30 files `Mathlib.Algebra.Group.ForwardDiff` `Mathlib.Algebra.Order.CauSeq.BigOperators` `Mathlib.Algebra.Polynomial.CancelLeads` `Mathlib.Algebra.Polynomial.CoeffList` `Mathlib.Algebra.Polynomial.Coeff` `Mathlib.Algebra.Polynomial.Degree.Domain` `Mathlib.Algebra.Polynomial.Degree.Lemmas` `Mathlib.Algebra.Polynomial.Degree.Operations` `Mathlib.Algebra.Polynomial.Degree.SmallDegree` `Mathlib.Algebra.Polynomial.Degree.Support` `Mathlib.Algebra.Polynomial.Degree.Units` `Mathlib.Algebra.Polynomial.DenomsClearable` `Mathlib.Algebra.Polynomial.Derivative` `Mathlib.Algebra.Polynomial.EraseLead` `Mathlib.Algebra.Polynomial.Eval.Coeff` `Mathlib.Algebra.Polynomial.Eval.Degree` `Mathlib.Algebra.Polynomial.Eval.Irreducible` `Mathlib.Algebra.Polynomial.Eval.SMul` `Mathlib.Algebra.Polynomial.Eval.Subring` `Mathlib.Algebra.Polynomial.Identities` `Mathlib.Algebra.Polynomial.Inductions` `Mathlib.Combinatorics.Colex` `Mathlib.Combinatorics.Enumerative.Bell` `Mathlib.Combinatorics.SetFamily.KruskalKatona` `Mathlib.Data.Nat.Choose.Multinomial` `Mathlib.Data.Nat.Choose.Vandermonde` `Mathlib.RingTheory.Polynomial.Hermite.Basic` `Mathlib.RingTheory.Polynomial.Opposites` `Mathlib.RingTheory.Polynomial.Pochhammer` `Mathlib.RingTheory.Radical`	11
`Mathlib.Algebra.Squarefree.Basic` `Mathlib.NumberTheory.FactorisationProperties`	12
13 files `Mathlib.Algebra.Field.GeomSum` `Mathlib.Algebra.GeomSum` `Mathlib.Algebra.Order.Field.GeomSum` `Mathlib.Algebra.Order.Ring.GeomSum` `Mathlib.Algebra.Order.Ring.IsNonarchimedean` `Mathlib.Algebra.Ring.Divisibility.Lemmas` `Mathlib.Algebra.Ring.GeomSum` `Mathlib.Combinatorics.Enumerative.IncidenceAlgebra` `Mathlib.Combinatorics.Enumerative.Schroder` `Mathlib.Combinatorics.SetFamily.AhlswedeZhang` `Mathlib.Data.Nat.Choose.Sum` `Mathlib.NumberTheory.Primorial` `Mathlib.RingTheory.Nilpotent.Basic`	13
`Mathlib.Data.Nat.Digits.Div` `Mathlib.Data.Nat.Digits.Lemmas`	14
4 files `Mathlib.Algebra.BigOperators.Intervals` `Mathlib.Algebra.BigOperators.Module` `Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite` `Mathlib.Data.Nat.Factorial.SuperFactorial`	16
`Mathlib.Order.Disjointed`	20
`Mathlib.MeasureTheory.Measure.Prokhorov` (new file)	2192

Declarations diff

+ R1Space + biUnion_Iic_disjointed + biUnion_Ioc_disjointed_of_monotone + biUnion_range_succ_disjointed + instance : R1Space (FiniteMeasure Ω) := IsInducing.r1Space (f := toWeakDualBCNN) ⟨rfl⟩ + instance [CompactSpace E] : CompactSpace (ProbabilityMeasure E) := by + isCompact_closure_of_isTightMeasureSet + isCompact_setOf_finiteMeasure_eq_of_compactSpace + isCompact_setOf_finiteMeasure_le_of_compactSpace + isCompact_setOf_finiteMeasure_le_of_isCompact + isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le + isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le + isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le + mono_null + pos_mono + range_succ_eq_Iic + restrict_biUnion_finset + sup_Ioc_disjointed_of_monotone

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

Dec 10 '25 20:12 github-actions[bot]

This pull request has conflicts, please merge master and resolve them.

Dec 12 '25 21:12 mathlib4-merge-conflict-bot

This PR/issue depends on:

~~leanprover-community/mathlib4#32778~~
~~leanprover-community/mathlib4#32779~~
~~leanprover-community/mathlib4#32783~~
~~leanprover-community/mathlib4#32784~~
~~leanprover-community/mathlib4#32785~~
~~leanprover-community/mathlib4#32786~~ By Dependent Issues (🤖). Happy coding!