feat: essSup of the uniform measure

[YaelDillies]

I don't care about how to spell the uniform measure, but I need something.

From LeanAPAP

---

• depends on: chore: rename condCount to uniformOn #17571

[github-actions]

PR summary 24d6456c53

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Function.EssSup	1243	1244	+1 (+0.08%)

Import changes for all files

Files

Import difference

269 files Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.Probability.BorelCantelli Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic 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.NumberTheory.Cyclotomic.Discriminant Mathlib.MeasureTheory.Measure.FiniteMeasure 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.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.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral 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.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.SpecialFunctions.Complex.Arctan Mathlib.Probability.Kernel.Composition Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Probability.Martingale.OptionalSampling Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.NumberTheory.NumberField.Discriminant Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.Analysis.SpecialFunctions.Gamma.Deligne 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.Measure.Haar.NormedSpace Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.Fourier.Inversion Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable 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.Probability.Distributions.Gaussian Mathlib.Probability.Kernel.CondDistrib Mathlib.MeasureTheory.Integral.Bochner Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Probability.Martingale.Basic Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Order.UpperLower Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Probability.Martingale.Convergence Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.Probability.Kernel.IntegralCompProd 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.MeasureTheory.Constructions.Prod.Integral Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Fourier.FourierTransformDeriv 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.Covering.DensityTheorem Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.BoxIntegral.Integrability Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.L1Space Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Analysis.Complex.RemovableSingularity Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Complex.Liouville Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.MeasureTheory.Function.Jacobian Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.MeasureTheory.Function.LpOrder Mathlib.Probability.Moments Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Probability.Process.Stopping Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.Geometry.Manifold.IntegralCurve Mathlib.Analysis.SumIntegralComparisons Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.Probability.Kernel.MeasureCompProd Mathlib.NumberTheory.ZetaValues Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.Fourier.FourierTransform Mathlib.Probability.Independence.Integrable Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.Convolution Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.Analysis.MellinInversion Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Covering.Differentiation Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.BoundedVariation Mathlib.NumberTheory.WellApproximable Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Probability.Process.Adapted 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.Function.Intersectivity 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.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.Probability.Kernel.Condexp Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.BorelCantelli 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.Integral.SetIntegral Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Probability.Integration Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Probability.Kernel.Integral Mathlib.MeasureTheory.Integral.Average Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Probability.Independence.Conditional Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic 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.Probability.Martingale.Centering Mathlib.MeasureTheory.Measure.Haar.Quotient

1

---

Declarations diff

+ essInf_cond_count_eq_ciInf
+ essSup_cond_count_eq_ciSup

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.

[RemyDegenne]

Same comment as on the other PR that included that code: I'd be sad if the standard way to write the uniform distribution in Mathlib was .count[|.univ] and the standard way to talk about it in a name was cond_count. Nodoby but the initiated would find those.

You should introduce a definition named discreteUniform or finiteUniform or something similar, defined with .count[|.univ] or directly with count and a smul. Add the minimal amount of API to make it usable, then use it in this PR. A uniform distribution on a finite type is common and useful enough to warrant a definition.

[YaelDillies]

The good thing about Yury's proposal is that sometimes we consider uniform distributions over a subset of the full type. This happens in additive combinatorics at least.

Is that an argument for renaming ProbabilityTheory.condCount to ProbabilityTheory.discreteUniform?

[RemyDegenne]

I think you are right, renaming condCount would be a simple and effective solution to the issue.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• chore: rename condCount to uniformOn #17571
  By Dependent Issues (🤖). Happy coding!