feat(Order/PartialSups): allow general orders as domain

[loefflerd]

Currently PartialSups is only defined for Nat-indexed sequences. This generalises it to arbitrary preorders satisfying suitable typeclass assumptions.

---

• depends on: chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs #20235

[github-actions]

PR summary 8fa907de54

Import changes exceeding 2%

%	File
+4.27%	Mathlib.LinearAlgebra.Prod
+16.14%	Mathlib.Order.Disjointed
+4.19%	Mathlib.Order.PartialSups

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.Disjointed	502	583	+81 (+16.14%)
Mathlib.LinearAlgebra.Prod	749	781	+32 (+4.27%)
Mathlib.Order.PartialSups	501	522	+21 (+4.19%)
Mathlib.Topology.Order.PartialSups	635	642	+7 (+1.10%)
Mathlib.Topology.Instances.Int	995	992	-3 (-0.30%)
Mathlib.Topology.Instances.Discrete	776	778	+2 (+0.26%)

Import changes for all files

Files	Import difference
4 files Mathlib.Topology.Instances.Nat Mathlib.Topology.Instances.PNat Mathlib.Topology.Instances.Int Mathlib.Analysis.Normed.Group.Int	-3
495 files Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Analysis.MeanInequalitiesPow Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.Probability.Variance Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.MulChar.Lemmas Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.NumberTheory.GaussSum Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Complex.AbsMax Mathlib.RingTheory.Flat.Basic Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Geometry.Manifold.Instances.Real Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Geometry.Manifold.Complex Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.RingTheory.Regular.RegularSequence Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.RingTheory.TensorProduct.Nontrivial 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.AlgebraicGeometry.PrimeSpectrum.FreeLocus Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan 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.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Analysis.RCLike.Inner Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.SiegelsLemma Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.RingTheory.RingHom.Flat Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.PSeries Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Analysis.InnerProductSpace.NormPow 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.RingTheory.Unramified.Field Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.RingTheory.Flat.Localization Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.Topology.Instances.AddCircle Mathlib.NumberTheory.NumberField.Completion Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.MeasureTheory.Group.AddCircle Mathlib.Probability.Independence.ZeroOne Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment 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.SpecificLimits.FloorPow 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.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.RingTheory.Etale.Field Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Probability.Kernel.Composition.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.MeasureTheory.Order.UpperLower Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Probability.Martingale.Convergence Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.RingTheory.LittleWedderburn Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.Analysis.PSeriesComplex Mathlib.Probability.Kernel.Disintegration.Density Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.Analysis.Convex.Integral Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.AlgebraicGeometry.RationalMap Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.FieldTheory.LinearDisjoint 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.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Data.Real.Pi.Leibniz Mathlib.NumberTheory.FLT.Three Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Analysis.InnerProductSpace.Positive Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Probability.Kernel.Invariance Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Probability.Distributions.Uniform Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Topology.CWComplex Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.Ostrowski Mathlib.MeasureTheory.Measure.Doubling Mathlib.Analysis.MeanInequalities Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Combinatorics.Additive.Randomisation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.NumberTheory.Fermat Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.Quaternion Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.NumberTheory.ClassNumber.Finite Mathlib.Topology.MetricSpace.GromovHausdorff 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.RingTheory.AdicCompletion.AsTensorProduct Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle 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.InnerProductSpace.EuclideanDist Mathlib.MeasureTheory.Function.LpOrder Mathlib.Analysis.Convex.Measure Mathlib.Probability.Moments Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Algebra.Module.CharacterModule Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Data.Real.Pi.Bounds Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Topology.Algebra.PontryaginDual Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.Topology.MetricSpace.Holder Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Probability.Process.Stopping Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.RingTheory.Polynomial.Cyclotomic.Expand 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.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.LinearAlgebra.Matrix.Hermitian 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.NumberTheory.Cyclotomic.Basic Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Analysis.Complex.Positivity Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.Fourier.FourierTransform Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Probability.Independence.Integrable Mathlib.Analysis.Matrix Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Analysis.Convolution Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.Analysis.Complex.Arg Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Analysis.MellinInversion Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.MeasureTheory.Covering.Differentiation Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.Analysis.Complex.Hadamard Mathlib.RingTheory.LinearDisjoint Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.NumberTheory.PrimesCongruentOne Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Algebra.Order.CompleteField Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.NumberTheory.WellApproximable Mathlib.RingTheory.LocalRing.Module Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Probability.Process.Adapted Mathlib.Analysis.Convex.Cone.Proper Mathlib.Probability.Distributions.Pareto Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.MeasureTheory.Integral.Pi Mathlib.NumberTheory.NumberField.House Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Probability.Process.Filtration Mathlib.MeasureTheory.Integral.Periodic Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Analysis.MellinTransform Mathlib.RingTheory.Flat.Equalizer Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.NumberTheory.LSeries.Linearity Mathlib.MeasureTheory.Integral.Gamma Mathlib.Analysis.VonNeumannAlgebra.Basic 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.NumberTheory.LSeries.PrimesInAP Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Martingale.OptionalStopping Mathlib.RingTheory.Flat.Stability 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.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.RingTheory.Unramified.Finite Mathlib.Probability.Integration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.NumberTheory.Bertrand Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.LSeries.Convolution Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Probability.Kernel.Integral Mathlib.MeasureTheory.Integral.Average Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Probability.Independence.Conditional Mathlib.NumberTheory.AbelSummation Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.RingTheory.Perfection Mathlib.Data.Real.Pi.Wallis Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.Probability.CDF Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.Probability.Martingale.Centering Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Analysis.Normed.Algebra.UnitizationL1	1
13 files Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.Topology.Instances.Discrete Mathlib.Topology.Instances.ENat Mathlib.LinearAlgebra.Dimension.Basic Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.Algebra.Colimit.Module Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.Topology.Category.Sequential Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors	2
8 files Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.Analysis.LocallyConvex.Polar Mathlib.Topology.Algebra.MvPolynomial Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Affine Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Normed.Group.AddTorsor	3
146 files Mathlib.Algebra.Star.Module Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.AlgebraTower Mathlib.Data.Matrix.Auto Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.Algebra.Module.Bimodule Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.Data.Matrix.Invertible Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.MvPolynomial.Counit Mathlib.Algebra.MvPolynomial.Basic Mathlib.GroupTheory.Coxeter.Matrix Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.RingTheory.Localization.BaseChange Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.MvPolynomial.Expand Mathlib.Algebra.Star.Subalgebra Mathlib.GroupTheory.Coxeter.Basic Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Analysis.Convex.Slope Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.Algebra.DirectSum.Internal Mathlib.Data.Matrix.Block Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal Mathlib.RingTheory.DividedPowers.Basic Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.RingTheory.PolynomialAlgebra Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.Algebra.Algebra.Unitization Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.Algebra.DirectSum.Decomposition Mathlib.RingTheory.Polynomial.Bernstein Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.Analysis.Convex.Cone.Extension Mathlib.Algebra.MvPolynomial.Rename Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.Data.Matrix.Reflection Mathlib.Algebra.Module.Projective Mathlib.Analysis.Convex.Join Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.Algebra.MvPolynomial.Derivation Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.Algebra.CharP.Subring Mathlib.Algebra.MvPolynomial.Variables Mathlib.Algebra.MvPolynomial.Supported Mathlib.RingTheory.MvPolynomial.Tower Mathlib.Algebra.DirectSum.Finsupp Mathlib.LinearAlgebra.LinearIndependent Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.Algebra.Algebra.Spectrum Mathlib.MeasureTheory.MeasurableSpace.NCard Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.SesquilinearForm Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.RingTheory.IsTensorProduct Mathlib.Algebra.MvPolynomial.Comap Mathlib.RingTheory.Polynomial.Wronskian Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.LinearAlgebra.Ray Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.Segment Mathlib.RingTheory.Adjoin.Polynomial Mathlib.MeasureTheory.MeasurableSpace.Card Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.Algebra.Algebra.Quasispectrum Mathlib.Algebra.Star.Free Mathlib.Algebra.MvPolynomial.Monad Mathlib.LinearAlgebra.Alternating.Basic Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Analysis.Convex.Function Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.RingTheory.MatrixAlgebra Mathlib.Analysis.Convex.Cone.Basic Mathlib.Algebra.Category.AlgebraCat.Basic Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.Algebra.MvPolynomial.Division Mathlib.Data.Complex.Module Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.RingTheory.TensorProduct.Pi Mathlib.Algebra.CharP.LinearMaps Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Star Mathlib.LinearAlgebra.Basis.Basic Mathlib.Analysis.Convex.Basic Mathlib.Algebra.CharP.Algebra Mathlib.RingTheory.Localization.Module Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Data.Matrix.RowCol Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Analysis.Convex.Extreme Mathlib.LinearAlgebra.TensorPower Mathlib.Data.Matrix.Hadamard Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.Algebra.CharP.IntermediateField Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.Analysis.Convex.Quasiconvex Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Algebra.DirectSum.Algebra Mathlib.RingTheory.TensorProduct.Free Mathlib.Algebra.MvPolynomial.Invertible Mathlib.Data.Matrix.ConjTranspose Mathlib.Algebra.Star.Unitary Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.Data.Matrix.Notation Mathlib.RingTheory.TensorProduct.Basic Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.Algebra.Module.GradedModule Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.Algebra.FreeAlgebra Mathlib.RingTheory.PowerSeries.Trunc Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.FieldTheory.Differential.Basic Mathlib.LinearAlgebra.AffineSpace.AffineSubspace Mathlib.LinearAlgebra.FreeProduct.Basic	4
Mathlib.Topology.Order.PartialSups	7
Mathlib.Order.Interval.Finset.Box	8
Mathlib.MeasureTheory.Measure.AddContent	10
3 files Mathlib.Algebra.TrivSqZeroExt Mathlib.Data.Matrix.DualNumber Mathlib.Algebra.DualNumber	18
Mathlib.Order.PartialSups	21
5 files Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.Algebra.Module.Injective Mathlib.MeasureTheory.Constructions.SubmoduleQuotient Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Prod	32
Mathlib.MeasureTheory.Constructions.AddChar	38
Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict	39
5 files Mathlib.MeasureTheory.MeasurableSpace.Embedding Mathlib.MeasureTheory.MeasurableSpace.Basic Mathlib.MeasureTheory.Constructions.Cylinders Mathlib.MeasureTheory.MeasurableSpace.Prod Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated	41
Mathlib.MeasureTheory.MeasurableSpace.Instances	67
7 files Mathlib.Order.Disjointed Mathlib.MeasureTheory.MeasurableSpace.Defs Mathlib.MeasureTheory.SetAlgebra Mathlib.MeasureTheory.Constructions.EventuallyMeasurable Mathlib.MeasureTheory.MeasurableSpace.Invariants Mathlib.MeasureTheory.PiSystem Mathlib.MeasureTheory.SetSemiring	81

---

Declarations diff

+ OrderTopology.of_linearLocallyFinite
+ Pi.partialSups_apply
+ ciSup_partialSups_eq'
+ instance (priority := 100) Countable.of_linearOrder_locallyFiniteOrder [LocallyFiniteOrder ι] :
+ instance (priority := 100) [LocallyFiniteOrder ι] [PredOrder ι] : IsPredArchimedean ι
+ instance (priority := 100) [LocallyFiniteOrder ι] [SuccOrder ι] : IsSuccArchimedean ι
+ partialSups_add_one
+ partialSups_bot
+ predOrder
+ succOrder
- instance (priority := 100) [LocallyFiniteOrder ι] : IsPredArchimedean ι
- instance (priority := 100) [LocallyFiniteOrder ι] : IsSuccArchimedean ι
- instance (priority := 100) [LocallyFiniteOrder ι] : PredOrder ι
- instance (priority := 100) [LocallyFiniteOrder ι] : SuccOrder ι

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

[loefflerd]

Note to reviewers: I tried to make the generalisation "backward-compatible" as much as possible. However, some of the files which use partialSups were relying (abusively, IMHO) on partialSups f (n + 1) being definitionally equal to partialSups f n ⊔ f (n + 1). In the new version, this is still true, but no longer a defeq.

[YaelDillies]

Thank you for taking this on!

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs #20235
  By Dependent Issues (🤖). Happy coding!

[urkud]

This PR could use a file about Finset intervals in a SuccOrder. Also, partialSups_natSucc could be generalized to partialSups_add_one in a SuccAddOrder.

[YaelDillies]

This PR could use a file about Finset intervals in a SuccOrder.

I have one such file in the works. Give me a few days and it will be PRed

[loefflerd]

This PR could use a file about Finset intervals in a SuccOrder.

I have one such file in the works. Give me a few days and it will be PRed

@urkud could you perhaps clarify what this new file would be used for? The purpose of the present PR is to reformulate all the lemmas about partialSups under the minimal possible assumptions on the domain type. So lemmas about SuccOrder would not be applicable for most results here.

[urkud]

E.g., partialSups_succ has a goal about Finset.Iic (Order.succ a) which should become a lemmas in this new file. Probably, we shouldn't block this PR on the not yet ready PR, but when you add this new file, please use the new lemmas to golf a couple of proofs here.