refactor(Analysis/Convex): use the new convexity concepts

[YaelDillies]

Deprecate all the Module-specific convexity concepts in favor of the more general ConvexSpace ones.

---

• depends on: [Merged by Bors] - feat(Geometry/Convex): star-convex sets in a convex space #40230

[github-actions]

PR summary 3023298665

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Convex.Star	1061	1077	+16 (+1.51%)
Mathlib.Analysis.Convex.Basic	1076	1091	+15 (+1.39%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.Convex.MetricSpace Mathlib.Geometry.Convex.ConvexSpace.Module	1
865 files Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Algebra.Module.ZLattice.Summable Mathlib.AlgebraicGeometry.EllipticCurve.LFunction Mathlib.Analysis.Analytic.Binomial Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Analysis.Analytic.WithLp Mathlib.Analysis.BoundedVariation Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.Extreme Mathlib.Analysis.CStarAlgebra.Fuglede Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.CStarAlgebra.PositiveLinearMap Mathlib.Analysis.CStarAlgebra.Projection Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.Unitary.Connected Mathlib.Analysis.CStarAlgebra.Unitary.Span Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox Mathlib.Analysis.Calculus.ContDiff.Convolution Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.ImplicitContDiff Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.LogDerivUniformlyOn Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.Taylor Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.Angle Mathlib.Analysis.Complex.BorelCaratheodory Mathlib.Analysis.Complex.BranchLogRoot Mathlib.Analysis.Complex.CanonicalDecomposition Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Complex.CoveringMap Mathlib.Analysis.Complex.ExponentialBounds Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.Harmonic.Analytic Mathlib.Analysis.Complex.Harmonic.Liouville Mathlib.Analysis.Complex.Harmonic.MeanValue Mathlib.Analysis.Complex.Harmonic.Poisson Mathlib.Analysis.Complex.HasPrimitives Mathlib.Analysis.Complex.JensenFormula Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.MeanValue Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Complex.OperatorNorm Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Poisson Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Complex.Polynomial.GaussLucas Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.RiemannMapping Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.SqrtDeriv Mathlib.Analysis.Complex.SummableUniformlyOn Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Complex.UpperHalfPlane.Measure Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.ValueDistribution.Cartan Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic Mathlib.Analysis.Convex.Approximation Mathlib.Analysis.Convex.BetweenList Mathlib.Analysis.Convex.Between Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.Cone.Dual Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Cone.TensorProduct Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.DoublyStochasticMatrix Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.Radon Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.Visible Mathlib.Analysis.Convolution Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.ContDiffMapSupportedIn Mathlib.Analysis.Distribution.DerivNotation Mathlib.Analysis.Distribution.Distribution Mathlib.Analysis.Distribution.FourierMultiplier Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace.Basic Mathlib.Analysis.Distribution.SchwartzSpace.Deriv Mathlib.Analysis.Distribution.SchwartzSpace.Fourier Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.Distribution.Sobolev Mathlib.Analysis.Distribution.Support Mathlib.Analysis.Distribution.TemperateGrowth Mathlib.Analysis.Distribution.TemperedDistribution Mathlib.Analysis.Distribution.TestFunction Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.Fourier.Convolution Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Fourier.FourierTransform Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.LpSpace Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.InnerProductSpace.CanonicalTensor Mathlib.Analysis.InnerProductSpace.Coalgebra Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.InnerProductSpace.GramMatrix Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.InnerProductSpace.Harmonic.Basic Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.Laplacian Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.MulOpposite Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Analysis.InnerProductSpace.Projection.Basic Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional Mathlib.Analysis.InnerProductSpace.Projection.Reflection Mathlib.Analysis.InnerProductSpace.Projection.Submodule Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Reproducing Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Analysis.InnerProductSpace.SingularValues Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.StandardSubspace Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.InnerProductSpace.TensorProduct Mathlib.Analysis.InnerProductSpace.Trace Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.LocallyConvex.Montel Mathlib.Analysis.LocallyConvex.SeparatingDual Mathlib.Analysis.LocallyConvex.Separation Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.Matrix.Hermitian Mathlib.Analysis.Matrix.LDL Mathlib.Analysis.Matrix.Normed Mathlib.Analysis.Matrix.Order Mathlib.Analysis.Matrix.PosDef Mathlib.Analysis.Matrix.Spectrum Mathlib.Analysis.Matrix Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.MeanInequalities Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Meromorphic.Complex Mathlib.Analysis.Meromorphic.FactorizedRational Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Affine.AsymptoticCone Mathlib.Analysis.Normed.Affine.Convex Mathlib.Analysis.Normed.Algebra.Basic Mathlib.Analysis.Normed.Algebra.DualNumber Mathlib.Analysis.Normed.Algebra.GelfandFormula Mathlib.Analysis.Normed.Algebra.GelfandMazur Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Analysis.Normed.Field.Dense Mathlib.Analysis.Normed.Field.Krasner Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Analysis.Normed.Lp.Matrix Mathlib.Analysis.Normed.Lp.MeasurableSpace Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.Analysis.Normed.Lp.SmoothApprox Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Analysis.Normed.Module.Bases Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.ContinuousInverse Mathlib.Analysis.Normed.Module.DoubleDual Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.HahnBanach Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.Operator.CompleteCodomain Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv Mathlib.Analysis.Normed.Ring.InfiniteProd Mathlib.Analysis.Normed.Unbundled.SpectralNorm Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn Mathlib.Analysis.ODE.ExistUnique Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.PSeries Mathlib.Analysis.Polynomial.Factorization Mathlib.Analysis.Polynomial.Fourier Mathlib.Analysis.Polynomial.MahlerMeasure Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.RCLike.Lemmas Mathlib.Analysis.Real.Pi.Bounds Mathlib.Analysis.Real.Pi.Chudnovsky Mathlib.Analysis.Real.Pi.Irrational Mathlib.Analysis.Real.Pi.Leibniz Mathlib.Analysis.Real.Pi.Wallis Mathlib.Analysis.SpecialFunctions.Arcosh Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.SpecialFunctions.Gamma.Digamma Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Integrability.Basic Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic Mathlib.Analysis.SpecialFunctions.Integrals.Basic Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.Analysis.SpecialFunctions.Log.InvLog Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.SpecialFunctions.Log.Summable Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.Sigmoid Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc Mathlib.Analysis.SumIntegralComparisons Mathlib.Analysis.SumIntegralExpDecay Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Computability.AkraBazzi.SumTransform Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircleAdd Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Dynamics.Ergodic.Extreme Mathlib.Dynamics.Ergodic.RadonNikodym Mathlib.Geometry.Diffeology.Basic Mathlib.Geometry.Euclidean.Altitude Mathlib.Geometry.Euclidean.Angle.Bisector Mathlib.Geometry.Euclidean.Angle.Incenter Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.Projection Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Congruence Mathlib.Geometry.Euclidean.Incenter Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.NinePointCircle Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Geometry.Euclidean.Projection Mathlib.Geometry.Euclidean.SignedDist Mathlib.Geometry.Euclidean.Similarity Mathlib.Geometry.Euclidean.Simplex Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Sphere.OrthRadius Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Sphere.Tangent Mathlib.Geometry.Euclidean.Triangle Mathlib.Geometry.Euclidean.Volume.Measure Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Geometry.Manifold.Algebra.SMul Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.Bordism Mathlib.Geometry.Manifold.BumpFunction Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Geometry.Manifold.ContMDiff.Constructions Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Geometry.Manifold.DerivationBundle Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Geometry.Manifold.GroupLieAlgebra Mathlib.Geometry.Manifold.Immersion Mathlib.Geometry.Manifold.Instances.Icc Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Geometry.Manifold.IsManifold.ExtChartAt Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Geometry.Manifold.Metrizable Mathlib.Geometry.Manifold.Notation Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Geometry.Manifold.Riemannian.Basic Mathlib.Geometry.Manifold.Riemannian.PathELength Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.SmoothApprox Mathlib.Geometry.Manifold.SmoothEmbedding Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.VectorBundle.LocalFrame Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.Geometry.Manifold.VectorBundle.Riemannian Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Geometry.Manifold.VectorBundle.Tensoriality Mathlib.Geometry.Manifold.VectorField.LieBracket Mathlib.Geometry.Manifold.VectorField.Pullback Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.Geometry.Polygon.Basic Mathlib.InformationTheory.KullbackLeibler.Basic Mathlib.InformationTheory.KullbackLeibler.ChainRule Mathlib.InformationTheory.KullbackLeibler.KLFun Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.Stochastic Mathlib.LinearAlgebra.Matrix.Swap Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Covering.OneDim Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.AbsolutelyContinuous Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.MeasureTheory.Function.ConditionalLExpectation Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.MeasureTheory.Function.ConvergenceInDistribution Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.MeasureTheory.Function.FactorsThrough Mathlib.MeasureTheory.Function.Holder Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.JacobianOneDim Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L1Space.AEEqFun Mathlib.MeasureTheory.Function.L1Space.Integrable Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.MeasureTheory.Function.LpOrder Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.MeasureTheory.Function.LpSpace.Basic Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp Mathlib.MeasureTheory.Function.LpSpace.Complete Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.LpSpace.Indicator Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Function.UnifTight Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Group.IntegralConvolution Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Group.ModularCharacter Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average Mathlib.MeasureTheory.Integral.Bochner.Basic Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus Mathlib.MeasureTheory.Integral.Bochner.L1 Mathlib.MeasureTheory.Integral.Bochner.Set Mathlib.MeasureTheory.Integral.Bochner.SumMeasure Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.MeasureTheory.Integral.CircleAverage Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.CompactlySupported Mathlib.MeasureTheory.Integral.CurveIntegral.Basic Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.FinMeasAdditive Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.MeasureTheory.Integral.MeanValue Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.Regular Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion Mathlib.MeasureTheory.Measure.CharacteristicFunction Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.FiniteMeasureExt Mathlib.MeasureTheory.Measure.FiniteMeasurePi Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.Haar.DistribChar Mathlib.MeasureTheory.Measure.Haar.Extension Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.MeasureTheory.Measure.IntegralCharFun Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Measure.LevyConvergence Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.Prokhorov Mathlib.MeasureTheory.Measure.ResolventTransform Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Measure.TightNormed Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Order.UpperLower Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap Mathlib.MeasureTheory.SpecificCodomains.Pi Mathlib.MeasureTheory.SpecificCodomains.WithLp Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym Mathlib.MeasureTheory.VectorMeasure.Integral Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.Bertrand Mathlib.NumberTheory.Chebyshev Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.Injectivity Mathlib.NumberTheory.LSeries.Linearity Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LSeries.ZetaZeros Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.Complex Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.MahlerMeasure Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.BoundedAtCusp Mathlib.NumberTheory.ModularForms.Bounds Mathlib.NumberTheory.ModularForms.CuspFormSubmodule Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne Mathlib.NumberTheory.ModularForms.Discriminant Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.ModularForms.LevelOne.Basic Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.NumberTheory.ModularForms.NormTrace Mathlib.NumberTheory.ModularForms.Petersson Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.NumberTheory.Modular Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion.FinitePlace Mathlib.NumberTheory.NumberField.Completion.InfinitePlace Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances Mathlib.NumberTheory.NumberField.Completion.Ramification Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.ExistsRamified Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.InfiniteAdeleRing Mathlib.NumberTheory.NumberField.InfinitePlace.Basic Mathlib.NumberTheory.NumberField.InfinitePlace.Completion Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.Padics.AddChar Mathlib.NumberTheory.Padics.Complex Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.NumberTheory.WellApproximable Mathlib.NumberTheory.ZetaValues Mathlib.Probability.BorelCantelli Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily Mathlib.Probability.CDF Mathlib.Probability.CentralLimitTheorem Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.Density Mathlib.Probability.Distributions.Bernoulli Mathlib.Probability.Distributions.Beta Mathlib.Probability.Distributions.Binomial Mathlib.Probability.Distributions.Cauchy Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Fernique Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian.Basic Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Distributions.Gaussian.Fernique Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence Mathlib.Probability.Distributions.Gaussian.Multivariate Mathlib.Probability.Distributions.Gaussian.Real Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Poisson.Basic Mathlib.Probability.Distributions.Poisson.PoissonLimitThm Mathlib.Probability.Distributions.SetBernoulli Mathlib.Probability.Distributions.TwoValued Mathlib.Probability.Distributions.Uniform Mathlib.Probability.HasLawExists Mathlib.Probability.HasLaw Mathlib.Probability.IdentDistribIndep Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.BoundedContinuousFunction Mathlib.Probability.Independence.CharacteristicFunction Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.InfinitePi Mathlib.Probability.Independence.Integrable Mathlib.Probability.Independence.Integration Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess Mathlib.Probability.Independence.Process.HasIndepIncrements Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Kernel.CompProdEqIff Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Probability.Kernel.Composition.RadonNikodym Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.IonescuTulcea.Traj Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.Posterior Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Kernel.Representation Mathlib.Probability.Kernel.SetIntegral Mathlib.Probability.Kernel.WithDensity Mathlib.Probability.Martingale.Basic Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Martingale.Centering Mathlib.Probability.Martingale.Convergence Mathlib.Probability.Martingale.OptionalSampling Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.Upcrossing Mathlib.Probability.Moments.Basic Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.CovarianceBilinDual Mathlib.Probability.Moments.CovarianceBilin Mathlib.Probability.Moments.Covariance Mathlib.Probability.Moments.IntegrableExpMul Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Moments.SubGaussian Mathlib.Probability.Moments.Tilted Mathlib.Probability.Moments.Variance Mathlib.Probability.Notation Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.FiniteDimensionalLaws Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.LocalProperty Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Predictable Mathlib.Probability.Process.Stopping Mathlib.Probability.ProductMeasure Mathlib.Probability.StrongLaw Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Selmer Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic Mathlib.Topology.Algebra.AsymptoticCone Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.Compactification.OnePoint.Sphere Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Topology.MetricSpace.Snowflaking	5
10 files Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Topology.VectorBundle.FiniteDimensional	6
225 files Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.CPolynomialDef Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Analytic.Constructions Mathlib.Analysis.Analytic.ConvergenceRadius Mathlib.Analysis.Analytic.Inverse Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.Analytic.OfScalars Mathlib.Analysis.Analytic.Order Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.Within Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.Calculus.AbsolutelyMonotone Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.Analysis.Calculus.ContDiff.Comp Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.Calculus.ContDiff.Deriv Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Analysis.Calculus.ContDiff.Operations Mathlib.Analysis.Calculus.ContDiff.Polynomial Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.Calculus.ContDiff.RestrictScalars Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Calculus.Deriv.CompMul Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.Analysis.Calculus.Deriv.MeanValue Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.DerivativeTest Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Calculus.DifferentialForm.Basic Mathlib.Analysis.Calculus.DifferentialForm.VectorField Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.Calculus.FDeriv.Affine Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Analysis.Calculus.FDeriv.CompCLM Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Calculus.FDeriv.Congr Mathlib.Analysis.Calculus.FDeriv.Const Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Calculus.FDeriv.OfCompLeft Mathlib.Analysis.Calculus.FDeriv.Partial Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.Calculus.FDeriv.Pow Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Analysis.Calculus.IteratedDeriv.Analytic Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.TangentCone Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.Calculus.VectorField Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.Convex.GaugeRescale Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar Mathlib.Analysis.InnerProductSpace.Affine Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.InnerProductSpace.Continuous Mathlib.Analysis.InnerProductSpace.Convex Mathlib.Analysis.InnerProductSpace.Defs Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.Analysis.InnerProductSpace.Projection.Minimal Mathlib.Analysis.LocallyConvex.AbsConvexOpen Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.LocallyConvex.PointwiseConvergence Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.Meromorphic.Basic Mathlib.Analysis.Meromorphic.Divisor Mathlib.Analysis.Meromorphic.IsolatedZeros Mathlib.Analysis.Meromorphic.NormalForm Mathlib.Analysis.Meromorphic.Order Mathlib.Analysis.Meromorphic.RCLike Mathlib.Analysis.Meromorphic.TrailingCoefficient Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.Normed.Module.Alternating.Basic Mathlib.Analysis.Normed.Module.Alternating.Curry Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin Mathlib.Analysis.Normed.Module.Completion Mathlib.Analysis.Normed.Module.Multilinear.Basic Mathlib.Analysis.Normed.Module.Multilinear.Curry Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm Mathlib.Analysis.Normed.Module.RCLike.Basic Mathlib.Analysis.Normed.Module.RCLike.Extend Mathlib.Analysis.Normed.Module.RieszLemma Mathlib.Analysis.Normed.Operator.Asymptotics Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Analysis.Normed.Operator.Banach Mathlib.Analysis.Normed.Operator.Basic Mathlib.Analysis.Normed.Operator.Bilinear Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension Mathlib.Analysis.Normed.Operator.Completeness Mathlib.Analysis.Normed.Operator.Extend Mathlib.Analysis.Normed.Operator.Mul Mathlib.Analysis.Normed.Operator.NNNorm Mathlib.Analysis.Normed.Operator.NormedSpace Mathlib.Analysis.Normed.Operator.Prod Mathlib.Analysis.Normed.Unbundled.AlgebraNorm Mathlib.Analysis.Normed.Unbundled.FiniteExtension Mathlib.Analysis.Normed.Unbundled.InvariantExtension Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful Mathlib.Analysis.ODE.Basic Mathlib.Analysis.ODE.DiscreteGronwall Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.ODE.Transform Mathlib.Analysis.RCLike.BoundedContinuous Mathlib.Analysis.RCLike.ContinuousMap Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Analysis.SpecialFunctions.Pochhammer Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Combinatorics.Derangements.Exponential Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.Geometry.Manifold.IsManifold.Basic Mathlib.Geometry.Manifold.LocalSourceTargetProperty Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.Algebra.Module.TopDualPairing Mathlib.Topology.Algebra.PontryaginDual Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.ContinuousMap.Bounded.Normed Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Topology.ContinuousMap.Compact Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Topology.ContinuousMap.ContinuousSqrt Mathlib.Topology.ContinuousMap.Ideals Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Topology.MetricSpace.Holder Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.Topology.MetricSpace.UniformConvergence Mathlib.Topology.TietzeExtension Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.VectorBundle.Constructions Mathlib.Topology.VectorBundle.ContinuousAlternatingMap Mathlib.Topology.VectorBundle.Hom Mathlib.Topology.VectorBundle.Riemannian	7
3 files Mathlib.Analysis.Convex.AmpleSet Mathlib.Analysis.Normed.Module.Connected Mathlib.Geometry.Convex.Cone.TensorProduct	8
28 files Mathlib.AlgebraicTopology.SimplicialSet.TopAdj Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularHomology.HomologyZero Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.Calculus.TangentCone.Real Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Convex.LinearIsometry Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Analysis.Convex.StdSimplex Mathlib.Analysis.Convex.Strict.Extreme Mathlib.Analysis.Convex.StrictCombination Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Analysis.Convex.Topology Mathlib.Analysis.Convex.TotallyBounded Mathlib.Analysis.Convex.Uniform Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Analysis.Normed.Module.Convex Mathlib.Analysis.RCLike.TangentCone Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.ContinuousMap.LocallyConvex Mathlib.Topology.Homotopy.TopCat.ToSSet Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy Mathlib.Topology.MetricSpace.PartitionOfUnity	9
8 files Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.Calculus.FDeriv.Defs Mathlib.Analysis.Normed.Operator.Compact.Basic Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM Mathlib.Topology.Algebra.Module.StrongTopology	10
13 files Mathlib.Analysis.Calculus.TangentCone.ProperSpace Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Convex.Combination Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.Convex.Independent Mathlib.Analysis.Convex.Jensen Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.Analysis.Convex.StoneSeparation Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Analysis.Seminorm Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.UniformConvergence	11
Mathlib.Analysis.Convex.Body Mathlib.Topology.Sion	12
26 files Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.Analysis.Convex.Cone.Basic Mathlib.Analysis.Convex.Cone.Closure Mathlib.Analysis.Convex.ContinuousLinearEquiv Mathlib.Analysis.Convex.Contractible Mathlib.Analysis.Convex.Exposed Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.FunctionTopology Mathlib.Analysis.Convex.PathConnected Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Convex.Strict Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Basic Mathlib.Topology.Homotopy.Affine Mathlib.Topology.Homotopy.Contractible Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Topology.Homotopy.Lifting Mathlib.Topology.Homotopy.LocallyContractible Mathlib.Topology.Homotopy.Path Mathlib.Topology.Homotopy.Product Mathlib.Topology.Subpath	13
15 files Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.NNReal Mathlib.Analysis.Convex.Piecewise Mathlib.Analysis.Convex.Slope Mathlib.Geometry.Convex.Cone.Basic Mathlib.Geometry.Convex.Cone.DualFinite Mathlib.Geometry.Convex.Cone.Dual Mathlib.Geometry.Convex.Cone.Pointed Mathlib.Geometry.Convex.Cone.Simplicial	15
Mathlib.Analysis.Convex.Star	16
Mathlib.Geometry.Convex.Star (new file)	876

---

Declarations diff (regex)

+ AffineSubspace.isconvexset
+ Antitone.isconvexset_ge
+ Antitone.isconvexset_gt
+ Antitone.isconvexset_le
+ Antitone.isconvexset_lt
+ AntitoneOn.isconvexset_ge
+ AntitoneOn.isconvexset_gt
+ AntitoneOn.isconvexset_le
+ AntitoneOn.isconvexset_lt
+ Convex
+ Directed.isconvexset_iUnion
+ DirectedOn.isconvexset_sUnion
+ IsAffineMap.add
+ IsAffineMap.map_smul_add_smul
+ IsAffineMap.map_sum_weights
+ IsAffineMap.neg
+ IsAffineMap.sub
+ IsConvexSet.add
+ IsConvexSet.add_half_self_eq_self
+ IsConvexSet.add_smul
+ IsConvexSet.add_smul_mem
+ IsConvexSet.add_smul_sub_mem
+ IsConvexSet.affine_image
+ IsConvexSet.affine_preimage
+ IsConvexSet.affinity
+ IsConvexSet.exists_mem_add_smul_eq
+ IsConvexSet.inter
+ IsConvexSet.isStarConvexSet
+ IsConvexSet.is_linear_image
+ IsConvexSet.is_linear_preimage
+ IsConvexSet.lift
+ IsConvexSet.lineMap_mem
+ IsConvexSet.linear_image
+ IsConvexSet.linear_preimage
+ IsConvexSet.mapsTo_lineMap
+ IsConvexSet.mem_smul_of_zero_mem
+ IsConvexSet.midpoint_mem
+ IsConvexSet.neg
+ IsConvexSet.openSegment_subset
+ IsConvexSet.ordConnected
+ IsConvexSet.prod
+ IsConvexSet.segment_subset
+ IsConvexSet.semilinear_image
+ IsConvexSet.semilinear_range
+ IsConvexSet.setOf_const_imp
+ IsConvexSet.set_combo_subset
+ IsConvexSet.smul
+ IsConvexSet.smul_mem_of_zero_mem
+ IsConvexSet.smul_preimage
+ IsConvexSet.starConvex_iff
+ IsConvexSet.sub
+ IsConvexSet.translate
+ IsConvexSet.translate_preimage_left
+ IsConvexSet.translate_preimage_right
+ IsConvexSet.vadd
+ IsConvexSet_subadditive_le
+ IsStarConvexSet
+ IsStarConvexSet.add
+ IsStarConvexSet.empty
+ IsStarConvexSet.iInter
+ IsStarConvexSet.iInter₂
+ IsStarConvexSet.iUnion
+ IsStarConvexSet.iUnion₂
+ IsStarConvexSet.image
+ IsStarConvexSet.inter
+ IsStarConvexSet.mem
+ IsStarConvexSet.neg
+ IsStarConvexSet.pi
+ IsStarConvexSet.preimage
+ IsStarConvexSet.prod
+ IsStarConvexSet.sInter
+ IsStarConvexSet.sUnion
+ IsStarConvexSet.singleton
+ IsStarConvexSet.sub
+ IsStarConvexSet.union
+ IsStarConvexSet.univ
+ Monotone.isconvexset_ge
+ Monotone.isconvexset_gt
+ Monotone.isconvexset_le
+ Monotone.isconvexset_lt
+ MonotoneOn.isconvexset_ge
+ MonotoneOn.isconvexset_gt
+ MonotoneOn.isconvexset_le
+ MonotoneOn.isconvexset_lt
+ Set.OrdConnected.isconvexset
+ Set.OrdConnected.isconvexset_of_chain
+ Set.Subsingleton.isconvexset
+ coe_isconvexsetAddSubmonoid
+ instance : IsModuleConvexSpace R (M × N)
+ isconvexset
+ isconvexsetAddSubmonoid
+ isconvexset_Icc
+ isconvexset_Ici
+ isconvexset_Ico
+ isconvexset_Iic
+ isconvexset_Iio
+ isconvexset_Ioc
+ isconvexset_Ioi
+ isconvexset_Ioo
+ isconvexset_empty
+ isconvexset_halfSpace_ge
+ isconvexset_halfSpace_gt
+ isconvexset_halfSpace_le
+ isconvexset_halfSpace_lt
+ isconvexset_hyperplane
+ isconvexset_iInter
+ isconvexset_iInter₂
+ isconvexset_iff_add_mem
+ isconvexset_iff_div
+ isconvexset_iff_forall_pos
+ isconvexset_iff_openSegment_subset
+ isconvexset_iff_ordConnected
+ isconvexset_iff_pairwise_pos
+ isconvexset_iff_pointwise_add_subset
+ isconvexset_iff_segment_subset
+ isconvexset_list_sum
+ isconvexset_multiset_sum
+ isconvexset_of_nonneg_surjective_algebraMap
+ isconvexset_openSegment
+ isconvexset_pi
+ isconvexset_sInter
+ isconvexset_segment
+ isconvexset_singleton
+ isconvexset_sum
+ isconvexset_uIcc
+ isconvexset_univ
+ isconvexset_vadd
+ isconvexset_zero
+ mem_isconvexsetAddSubmonoid
+ starConvex
+++ IsConvexSet.starConvex
- instance [ConvexSpace R N] [IsModuleConvexSpace R N] : IsModuleConvexSpace R (M × N)

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 3023298665
Reference commit bb482f116b

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(Geometry/Convex): star-convex sets in a convex space #40230
  By Dependent Issues (🤖). Happy coding!