chore(Topology/Instance/ENNReal): reduce `Defs` even more by grunweg · Pull Request #22093 · leanprover-community/mathlib4

grunweg · 2025-02-19T17:10:27Z

In #21670, I'm adding a new import of Topology/Instances/ENNReal/Defs.lean to Analysis/Normed/Group/Basic.lean.
To avoid a large imports increase, I have reduced the imports and contents of ENNReal/Defs.lean even more:
everything that is not strictly needed to prove that the coercion to NNReal is continuous is moved
into a new file Basic.lean.

Please land #22094 first, to preserve the diff.

github-actions · 2025-02-19T17:11:26Z

PR summary 1c31980474

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Instances.ENNReal.Defs	1121	1117	-4 (-0.36%)

Import changes for all files

Files	Import difference
`Mathlib.MeasureTheory.OuterMeasure.Defs` `Mathlib.Topology.Instances.ENNReal.Defs`	-4
1104 files `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.Algebra.Module.ZLattice.Covolume` `Mathlib.Analysis.AbsoluteValue.Equivalence` `Mathlib.Analysis.Analytic.Basic` `Mathlib.Analysis.Analytic.CPolynomial` `Mathlib.Analysis.Analytic.ChangeOrigin` `Mathlib.Analysis.Analytic.Composition` `Mathlib.Analysis.Analytic.Constructions` `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.Polynomial` `Mathlib.Analysis.Analytic.RadiusLiminf` `Mathlib.Analysis.Analytic.Uniqueness` `Mathlib.Analysis.Analytic.Within` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.SpecificAsymptotics` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Asymptotics.TVS` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Analysis.BoundedVariation` `Mathlib.Analysis.BoxIntegral.Basic` `Mathlib.Analysis.BoxIntegral.Box.SubboxInduction` `Mathlib.Analysis.BoxIntegral.DivergenceTheorem` `Mathlib.Analysis.BoxIntegral.Integrability` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.BoxIntegral.Partition.Filter` `Mathlib.Analysis.BoxIntegral.Partition.Measure` `Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction` `Mathlib.Analysis.BoxIntegral.UnitPartition` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.Analysis.CStarAlgebra.CStarMatrix` `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `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.Restrict` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `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.SpecialFunctions.PosPart` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.CStarAlgebra.lpSpace` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `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.Conformal.InnerProduct` `Mathlib.Analysis.Calculus.Conformal.NormedSpace` `Mathlib.Analysis.Calculus.ContDiff.Basic` `Mathlib.Analysis.Calculus.ContDiff.Bounds` `Mathlib.Analysis.Calculus.ContDiff.CPolynomial` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries` `Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno` `Mathlib.Analysis.Calculus.ContDiff.FiniteDimension` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.Analysis.Calculus.ContDiff.WithLp` `Mathlib.Analysis.Calculus.DSlope` `Mathlib.Analysis.Calculus.Darboux` `Mathlib.Analysis.Calculus.Deriv.Abs` `Mathlib.Analysis.Calculus.Deriv.Add` `Mathlib.Analysis.Calculus.Deriv.AffineMap` `Mathlib.Analysis.Calculus.Deriv.Basic` `Mathlib.Analysis.Calculus.Deriv.Comp` `Mathlib.Analysis.Calculus.Deriv.Inv` `Mathlib.Analysis.Calculus.Deriv.Inverse` `Mathlib.Analysis.Calculus.Deriv.Linear` `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.DiffContOnCl` `Mathlib.Analysis.Calculus.FDeriv.Add` `Mathlib.Analysis.Calculus.FDeriv.Analytic` `Mathlib.Analysis.Calculus.FDeriv.Basic` `Mathlib.Analysis.Calculus.FDeriv.Bilinear` `Mathlib.Analysis.Calculus.FDeriv.Comp` `Mathlib.Analysis.Calculus.FDeriv.Equiv` `Mathlib.Analysis.Calculus.FDeriv.Extend` `Mathlib.Analysis.Calculus.FDeriv.Linear` `Mathlib.Analysis.Calculus.FDeriv.Measurable` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.Analysis.Calculus.FDeriv.Pi` `Mathlib.Analysis.Calculus.FDeriv.Prod` `Mathlib.Analysis.Calculus.FDeriv.RestrictScalars` `Mathlib.Analysis.Calculus.FDeriv.Star` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.Analysis.Calculus.FDeriv.WithLp` `Mathlib.Analysis.Calculus.FirstDerivativeTest` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.Analysis.Calculus.Implicit` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.Analysis.Calculus.LHopital` `Mathlib.Analysis.Calculus.LagrangeMultipliers` `Mathlib.Analysis.Calculus.LineDeriv.Basic` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap` `Mathlib.Analysis.Calculus.LocalExtr.Basic` `Mathlib.Analysis.Calculus.LocalExtr.LineDeriv` `Mathlib.Analysis.Calculus.LocalExtr.Polynomial` `Mathlib.Analysis.Calculus.LocalExtr.Rolle` `Mathlib.Analysis.Calculus.LogDeriv` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.Analysis.Calculus.TangentCone` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.Complex.Angle` `Mathlib.Analysis.Complex.Arg` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Analysis.Complex.Circle` `Mathlib.Analysis.Complex.Conformal` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.IsIntegral` `Mathlib.Analysis.Complex.Isometry` `Mathlib.Analysis.Complex.Liouville` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.OperatorNorm` `Mathlib.Analysis.Complex.Periodic` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Analysis.Complex.Positivity` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Complex.Tietze` `Mathlib.Analysis.Complex.UnitDisc.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Complex.UpperHalfPlane.Metric` `Mathlib.Analysis.Complex.UpperHalfPlane.Topology` `Mathlib.Analysis.ConstantSpeed` `Mathlib.Analysis.Convex.AmpleSet` `Mathlib.Analysis.Convex.Body` `Mathlib.Analysis.Convex.Cone.Closure` `Mathlib.Analysis.Convex.Cone.InnerDual` `Mathlib.Analysis.Convex.Cone.Pointed` `Mathlib.Analysis.Convex.Cone.Proper` `Mathlib.Analysis.Convex.Continuous` `Mathlib.Analysis.Convex.Deriv` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.Convex.GaugeRescale` `Mathlib.Analysis.Convex.Gauge` `Mathlib.Analysis.Convex.Integral` `Mathlib.Analysis.Convex.Intrinsic` `Mathlib.Analysis.Convex.KreinMilman` `Mathlib.Analysis.Convex.Measure` `Mathlib.Analysis.Convex.Normed` `Mathlib.Analysis.Convex.PartitionOfUnity` `Mathlib.Analysis.Convex.Side` `Mathlib.Analysis.Convex.SpecificFunctions.Basic` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Analysis.Convex.SpecificFunctions.Pow` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Convex.Uniform` `Mathlib.Analysis.Convolution` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.Analysis.Fourier.AddCircleMulti` `Mathlib.Analysis.Fourier.AddCircle` `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.PoissonSummation` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.Analysis.Hofer` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Analysis.InnerProductSpace.Completion` `Mathlib.Analysis.InnerProductSpace.ConformalLinearMap` `Mathlib.Analysis.InnerProductSpace.Continuous` `Mathlib.Analysis.InnerProductSpace.Convex` `Mathlib.Analysis.InnerProductSpace.Defs` `Mathlib.Analysis.InnerProductSpace.Dual` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Analysis.InnerProductSpace.LaxMilgram` `Mathlib.Analysis.InnerProductSpace.LinearMap` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.Analysis.InnerProductSpace.MeanErgodic` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Analysis.InnerProductSpace.OfNorm` `Mathlib.Analysis.InnerProductSpace.Orientation` `Mathlib.Analysis.InnerProductSpace.Orthogonal` `Mathlib.Analysis.InnerProductSpace.Orthonormal` `Mathlib.Analysis.InnerProductSpace.PiL2` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Analysis.InnerProductSpace.ProdL2` `Mathlib.Analysis.InnerProductSpace.Projection` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.InnerProductSpace.Semisimple` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.InnerProductSpace.Subspace` `Mathlib.Analysis.InnerProductSpace.Symmetric` `Mathlib.Analysis.InnerProductSpace.TwoDim` `Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology` `Mathlib.Analysis.InnerProductSpace.l2Space` `Mathlib.Analysis.LocallyConvex.AbsConvexOpen` `Mathlib.Analysis.LocallyConvex.AbsConvex` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.Analysis.LocallyConvex.Barrelled` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.Analysis.LocallyConvex.ContinuousOfBounded` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.Analysis.LocallyConvex.WeakOperatorTopology` `Mathlib.Analysis.LocallyConvex.WeakSpace` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.Analysis.Matrix` `Mathlib.Analysis.MeanInequalitiesPow` `Mathlib.Analysis.MeanInequalities` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.Meromorphic.Basic` `Mathlib.Analysis.Meromorphic.Order` `Mathlib.Analysis.Normed.Affine.AddTorsorBases` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.Analysis.Normed.Algebra.Norm` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt` `Mathlib.Analysis.Normed.Algebra.Ultra` `Mathlib.Analysis.Normed.Algebra.UnitizationL1` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Analysis.Normed.Field.InfiniteSum` `Mathlib.Analysis.Normed.Field.Instances` `Mathlib.Analysis.Normed.Field.Lemmas` `Mathlib.Analysis.Normed.Field.ProperSpace` `Mathlib.Analysis.Normed.Field.Ultra` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Normed.Group.AddCircle` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Analysis.Normed.Group.Completeness` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.Normed.Group.Continuity` `Mathlib.Analysis.Normed.Group.ControlledClosure` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.Analysis.Normed.Group.NullSubmodule` `Mathlib.Analysis.Normed.Group.Pointwise` `Mathlib.Analysis.Normed.Group.Quotient` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.Analysis.Normed.Group.SeparationQuotient` `Mathlib.Analysis.Normed.Group.Tannery` `Mathlib.Analysis.Normed.Group.Ultra` `Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.Analysis.Normed.Lp.LpEquiv` `Mathlib.Analysis.Normed.Lp.PiLp` `Mathlib.Analysis.Normed.Lp.ProdLp` `Mathlib.Analysis.Normed.Lp.lpSpace` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Normed.Module.Complemented` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Analysis.Normed.Module.Dual` `Mathlib.Analysis.Normed.Module.FiniteDimension` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.Module.WeakDual` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Analysis.Normed.Operator.BoundedLinearMaps` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.Analysis.Normed.Ring.IsPowMulFaithful` `Mathlib.Analysis.Normed.Ring.SeminormFromBounded` `Mathlib.Analysis.Normed.Ring.SeminormFromConst` `Mathlib.Analysis.Normed.Ring.Seminorm` `Mathlib.Analysis.Normed.Ring.SmoothingSeminorm` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Analysis.Normed.Ring.Units` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.NormedSpace.BallAction` `Mathlib.Analysis.NormedSpace.ConformalLinearMap` `Mathlib.Analysis.NormedSpace.Connected` `Mathlib.Analysis.NormedSpace.DualNumber` `Mathlib.Analysis.NormedSpace.ENormedSpace` `Mathlib.Analysis.NormedSpace.Extend` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.Analysis.NormedSpace.FunctionSeries` `Mathlib.Analysis.NormedSpace.HahnBanach.Extension` `Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual` `Mathlib.Analysis.NormedSpace.HahnBanach.Separation` `Mathlib.Analysis.NormedSpace.HomeomorphBall` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics` `Mathlib.Analysis.NormedSpace.OperatorNorm.Basic` `Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.Analysis.NormedSpace.OperatorNorm.Mul` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Analysis.NormedSpace.Pointwise` `Mathlib.Analysis.NormedSpace.RCLike` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.Analysis.NormedSpace.RieszLemma` `Mathlib.Analysis.NormedSpace.SphereNormEquiv` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.Analysis.PSeriesComplex` `Mathlib.Analysis.PSeries` `Mathlib.Analysis.Polynomial.Basic` `Mathlib.Analysis.Quaternion` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Analysis.RCLike.Inner` `Mathlib.Analysis.RCLike.Lemmas` `Mathlib.Analysis.Seminorm` `Mathlib.Analysis.SpecialFunctions.Arsinh` `Mathlib.Analysis.SpecialFunctions.Bernstein` `Mathlib.Analysis.SpecialFunctions.BinaryEntropy` `Mathlib.Analysis.SpecialFunctions.Choose` `Mathlib.Analysis.SpecialFunctions.CompareExp` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.SpecialFunctions.Complex.Arg` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.Complex.Circle` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv` `Mathlib.Analysis.SpecialFunctions.Complex.Log` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.Analysis.SpecialFunctions.Exp` `Mathlib.Analysis.SpecialFunctions.Exponential` `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.Gaussian.FourierTransform` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.Analysis.SpecialFunctions.Integrals` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.Analysis.SpecialFunctions.Log.Base` `Mathlib.Analysis.SpecialFunctions.Log.Basic` `Mathlib.Analysis.SpecialFunctions.Log.Deriv` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog` `Mathlib.Analysis.SpecialFunctions.Log.Monotone` `Mathlib.Analysis.SpecialFunctions.Log.NegMulLog` `Mathlib.Analysis.SpecialFunctions.Log.PosLog` `Mathlib.Analysis.SpecialFunctions.Log.Summable` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.Analysis.SpecialFunctions.PolynomialExp` `Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics` `Mathlib.Analysis.SpecialFunctions.Pow.Complex` `Mathlib.Analysis.SpecialFunctions.Pow.Continuity` `Mathlib.Analysis.SpecialFunctions.Pow.Deriv` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Analysis.SpecialFunctions.Pow.NNReal` `Mathlib.Analysis.SpecialFunctions.Pow.Real` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Analysis.SpecificLimits.Basic` `Mathlib.Analysis.SpecificLimits.FloorPow` `Mathlib.Analysis.SpecificLimits.Normed` `Mathlib.Analysis.SpecificLimits.RCLike` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.Analysis.SumOverResidueClass` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.Combinatorics.Additive.Randomisation` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.Combinatorics.Extremal.RuzsaSzemeredi` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Combinatorics.SimpleGraph.Regularity.Bound` `Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk` `Mathlib.Combinatorics.SimpleGraph.Regularity.Increment` `Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma` `Mathlib.Combinatorics.SimpleGraph.Triangle.Removal` `Mathlib.Computability.AkraBazzi.AkraBazzi` `Mathlib.Computability.AkraBazzi.GrowsPolynomially` `Mathlib.Condensed.AB` `Mathlib.Condensed.Basic` `Mathlib.Condensed.CartesianClosed` `Mathlib.Condensed.Discrete.Basic` `Mathlib.Condensed.Discrete.Characterization` `Mathlib.Condensed.Discrete.Colimit` `Mathlib.Condensed.Discrete.LocallyConstant` `Mathlib.Condensed.Discrete.Module` `Mathlib.Condensed.Epi` `Mathlib.Condensed.Equivalence` `Mathlib.Condensed.Explicit` `Mathlib.Condensed.Functors` `Mathlib.Condensed.Light.AB` `Mathlib.Condensed.Light.Basic` `Mathlib.Condensed.Light.CartesianClosed` `Mathlib.Condensed.Light.Epi` `Mathlib.Condensed.Light.Explicit` `Mathlib.Condensed.Light.Functors` `Mathlib.Condensed.Light.Limits` `Mathlib.Condensed.Light.Module` `Mathlib.Condensed.Light.TopCatAdjunction` `Mathlib.Condensed.Light.TopComparison` `Mathlib.Condensed.Limits` `Mathlib.Condensed.Module` `Mathlib.Condensed.Solid` `Mathlib.Condensed.TopCatAdjunction` `Mathlib.Condensed.TopComparison` `Mathlib.Data.Complex.Cardinality` `Mathlib.Data.Complex.ExponentialBounds` `Mathlib.Data.Complex.FiniteDimensional` `Mathlib.Data.Real.Cardinality` `Mathlib.Data.Real.Hyperreal` `Mathlib.Data.Real.IsNonarchimedean` `Mathlib.Data.Real.Pi.Bounds` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber` `Mathlib.Dynamics.Ergodic.Action.Basic` `Mathlib.Dynamics.Ergodic.Action.OfMinimal` `Mathlib.Dynamics.Ergodic.Action.Regular` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.Dynamics.Ergodic.Conservative` `Mathlib.Dynamics.Ergodic.Ergodic` `Mathlib.Dynamics.Ergodic.Function` `Mathlib.Dynamics.Ergodic.MeasurePreserving` `Mathlib.Dynamics.TopologicalEntropy.CoverEntropy` `Mathlib.Dynamics.TopologicalEntropy.NetEntropy` `Mathlib.Dynamics.TopologicalEntropy.Semiconj` `Mathlib.FieldTheory.Galois.Profinite` `Mathlib.Geometry.Euclidean.Angle.Oriented.Affine` `Mathlib.Geometry.Euclidean.Angle.Oriented.Basic` `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.Basic` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal` `Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct` `Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle` `Mathlib.Geometry.Euclidean.Basic` `Mathlib.Geometry.Euclidean.Circumcenter` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane` `Mathlib.Geometry.Euclidean.MongePoint` `Mathlib.Geometry.Euclidean.PerpBisector` `Mathlib.Geometry.Euclidean.Sphere.Basic` `Mathlib.Geometry.Euclidean.Sphere.Power` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.Geometry.Euclidean.Sphere.SecondInter` `Mathlib.Geometry.Euclidean.Triangle` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.Geometry.Manifold.Algebra.LieGroup` `Mathlib.Geometry.Manifold.Algebra.Monoid` `Mathlib.Geometry.Manifold.Algebra.SmoothFunctions` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Geometry.Manifold.AnalyticManifold` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Geometry.Manifold.Complex` `Mathlib.Geometry.Manifold.ConformalGroupoid` `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.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.Basic` `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.PartitionOfUnity` `Mathlib.Geometry.Manifold.PoincareConjecture` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.Manifold.VectorBundle.Basic` `Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear` `Mathlib.Geometry.Manifold.VectorBundle.Hom` `Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable` `Mathlib.Geometry.Manifold.VectorBundle.Pullback` `Mathlib.Geometry.Manifold.VectorBundle.SmoothSection` `Mathlib.Geometry.Manifold.VectorBundle.Tangent` `Mathlib.Geometry.Manifold.VectorField` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.LinearAlgebra.Matrix.Hermitian` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.LinearAlgebra.Matrix.Spectrum` `Mathlib.LinearAlgebra.QuadraticForm.Complex` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.MeasureTheory.Category.MeasCat` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable` `Mathlib.MeasureTheory.Constructions.BorelSpace.Order` `Mathlib.MeasureTheory.Constructions.BorelSpace.Real` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.MeasureTheory.Constructions.Pi` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `Mathlib.MeasureTheory.Constructions.Projective` `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.Covering.VitaliFamily` `Mathlib.MeasureTheory.Covering.Vitali` `Mathlib.MeasureTheory.Decomposition.Exhaustion` `Mathlib.MeasureTheory.Decomposition.IntegralRNDeriv` `Mathlib.MeasureTheory.Decomposition.Jordan` `Mathlib.MeasureTheory.Decomposition.Lebesgue` `Mathlib.MeasureTheory.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.Decomposition.SignedHahn` `Mathlib.MeasureTheory.Decomposition.SignedLebesgue` `Mathlib.MeasureTheory.Decomposition.UnsignedHahn` `Mathlib.MeasureTheory.Function.AEEqFun.DomAct` `Mathlib.MeasureTheory.Function.AEEqFun` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.MeasureTheory.Function.AEEqOfLIntegral` `Mathlib.MeasureTheory.Function.AEMeasurableOrder` `Mathlib.MeasureTheory.Function.AEMeasurableSequence` `Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Real` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique` `Mathlib.MeasureTheory.Function.ContinuousMapDense` `Mathlib.MeasureTheory.Function.ConvergenceInMeasure` `Mathlib.MeasureTheory.Function.Egorov` `Mathlib.MeasureTheory.Function.EssSup` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.MeasureTheory.Function.Intersectivity` `Mathlib.MeasureTheory.Function.Jacobian` `Mathlib.MeasureTheory.Function.L1Space.AEEqFun` `Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral` `Mathlib.MeasureTheory.Function.L1Space.Integrable` `Mathlib.MeasureTheory.Function.L2Space` `Mathlib.MeasureTheory.Function.LocallyIntegrable` `Mathlib.MeasureTheory.Function.LpOrder` `Mathlib.MeasureTheory.Function.LpSeminorm.Basic` `Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov` `Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp` `Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality` `Mathlib.MeasureTheory.Function.LpSeminorm.Trim` `Mathlib.MeasureTheory.Function.LpSpace.Basic` `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.SimpleFuncDenseLp` `Mathlib.MeasureTheory.Function.SimpleFuncDense` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan` `Mathlib.MeasureTheory.Function.SpecialFunctions.Basic` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp` `Mathlib.MeasureTheory.Function.UnifTight` `Mathlib.MeasureTheory.Function.UniformIntegrable` `Mathlib.MeasureTheory.Group.AEStabilizer` `Mathlib.MeasureTheory.Group.Action` `Mathlib.MeasureTheory.Group.AddCircle` `Mathlib.MeasureTheory.Group.Arithmetic` `Mathlib.MeasureTheory.Group.Convolution` `Mathlib.MeasureTheory.Group.Defs` `Mathlib.MeasureTheory.Group.FundamentalDomain` `Mathlib.MeasureTheory.Group.GeometryOfNumbers` `Mathlib.MeasureTheory.Group.Integral` `Mathlib.MeasureTheory.Group.LIntegral` `Mathlib.MeasureTheory.Group.MeasurableEquiv` `Mathlib.MeasureTheory.Group.Measure` `Mathlib.MeasureTheory.Group.Pointwise` `Mathlib.MeasureTheory.Group.Prod` `Mathlib.MeasureTheory.Integral.Asymptotics` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.MeasureTheory.Integral.BochnerL1` `Mathlib.MeasureTheory.Integral.Bochner` `Mathlib.MeasureTheory.Integral.BoundedContinuousFunction` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.MeasureTheory.Integral.DivergenceTheorem` `Mathlib.MeasureTheory.Integral.DominatedConvergence` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.MeasureTheory.Integral.FundThmCalculus` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.MeasureTheory.Integral.Indicator` `Mathlib.MeasureTheory.Integral.IntegrableOn` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.MeasureTheory.Integral.IntervalAverage` `Mathlib.MeasureTheory.Integral.IntervalIntegral` `Mathlib.MeasureTheory.Integral.Layercake` `Mathlib.MeasureTheory.Integral.LebesgueNormedSpace` `Mathlib.MeasureTheory.Integral.Lebesgue` `Mathlib.MeasureTheory.Integral.Marginal` `Mathlib.MeasureTheory.Integral.MeanInequalities` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.MeasureTheory.Integral.Periodic` `Mathlib.MeasureTheory.Integral.Pi` `Mathlib.MeasureTheory.Integral.Prod` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic` `Mathlib.MeasureTheory.Integral.SetIntegral` `Mathlib.MeasureTheory.Integral.SetToL1` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Integral.VitaliCaratheodory` `Mathlib.MeasureTheory.Measure.AEDisjoint` `Mathlib.MeasureTheory.Measure.AEMeasurable` `Mathlib.MeasureTheory.Measure.AbsolutelyContinuous` `Mathlib.MeasureTheory.Measure.AddContent` `Mathlib.MeasureTheory.Measure.Comap` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.MeasureTheory.Measure.Content` `Mathlib.MeasureTheory.Measure.ContinuousPreimage` `Mathlib.MeasureTheory.Measure.Count` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Measure.Dirac` `Mathlib.MeasureTheory.Measure.Doubling` `Mathlib.MeasureTheory.Measure.EverywherePos` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.MeasureTheory.Measure.FiniteMeasure` `Mathlib.MeasureTheory.Measure.GiryMonad` `Mathlib.MeasureTheory.Measure.Haar.Basic` `Mathlib.MeasureTheory.Measure.Haar.Disintegration` `Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace` `Mathlib.MeasureTheory.Measure.Haar.NormedSpace` `Mathlib.MeasureTheory.Measure.Haar.OfBasis` `Mathlib.MeasureTheory.Measure.Haar.Quotient` `Mathlib.MeasureTheory.Measure.Haar.Unique` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosed` `Mathlib.MeasureTheory.Measure.Hausdorff` `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.LevyProkhorovMetric` `Mathlib.MeasureTheory.Measure.LogLikelihoodRatio` `Mathlib.MeasureTheory.Measure.Map` `Mathlib.MeasureTheory.Measure.MeasureSpaceDef` `Mathlib.MeasureTheory.Measure.MeasureSpace` `Mathlib.MeasureTheory.Measure.MutuallySingular` `Mathlib.MeasureTheory.Measure.NullMeasurable` `Mathlib.MeasureTheory.Measure.OpenPos` `Mathlib.MeasureTheory.Measure.Portmanteau` `Mathlib.MeasureTheory.Measure.ProbabilityMeasure` `Mathlib.MeasureTheory.Measure.Prod` `Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving` `Mathlib.MeasureTheory.Measure.Regular` `Mathlib.MeasureTheory.Measure.RegularityCompacts` `Mathlib.MeasureTheory.Measure.Restrict` `Mathlib.MeasureTheory.Measure.SeparableMeasure` `Mathlib.MeasureTheory.Measure.Stieltjes` `Mathlib.MeasureTheory.Measure.Sub` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.MeasureTheory.Measure.Trim` `Mathlib.MeasureTheory.Measure.Typeclasses` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.MeasureTheory.Measure.WithDensity` `Mathlib.MeasureTheory.Order.Group.Lattice` `Mathlib.MeasureTheory.Order.Lattice` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.MeasureTheory.OuterMeasure.AE` `Mathlib.MeasureTheory.OuterMeasure.Basic` `Mathlib.MeasureTheory.OuterMeasure.BorelCantelli` `Mathlib.MeasureTheory.OuterMeasure.Caratheodory` `Mathlib.MeasureTheory.OuterMeasure.Induced` `Mathlib.MeasureTheory.OuterMeasure.OfAddContent` `Mathlib.MeasureTheory.OuterMeasure.OfFunction` `Mathlib.MeasureTheory.OuterMeasure.Operations` `Mathlib.MeasureTheory.VectorMeasure.Basic` `Mathlib.MeasureTheory.VectorMeasure.WithDensity` `Mathlib.NumberTheory.AbelSummation` `Mathlib.NumberTheory.Bertrand` `Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.EulerProduct.Basic` `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.Int` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `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.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.MulChar.Lemmas` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.Ostrowski` `Mathlib.NumberTheory.Padics.Hensel` `Mathlib.NumberTheory.Padics.MahlerBasis` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.NumberTheory.Padics.ProperSpace` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.SiegelsLemma` `Mathlib.NumberTheory.SumPrimeReciprocals` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.NumberTheory.Transcendental.Lindemann.Init.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.VonMangoldt` `Mathlib.NumberTheory.WellApproximable` `Mathlib.NumberTheory.ZetaValues` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.Order.Filter.ENNReal` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.Probability.BorelCantelli` `Mathlib.Probability.CDF` `Mathlib.Probability.CondVar` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Probability.ConditionalProbability` `Mathlib.Probability.Density` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Probability.Distributions.Gaussian` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Probability.Distributions.Pareto` `Mathlib.Probability.Distributions.Poisson` `Mathlib.Probability.Distributions.Uniform` `Mathlib.Probability.IdentDistrib` `Mathlib.Probability.Independence.Basic` `Mathlib.Probability.Independence.Conditional` `Mathlib.Probability.Independence.Integrable` `Mathlib.Probability.Independence.Kernel` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Probability.Integration` `Mathlib.Probability.Kernel.Basic` `Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous` `Mathlib.Probability.Kernel.Composition.Basic` `Mathlib.Probability.Kernel.Composition.CompNotation` `Mathlib.Probability.Kernel.Composition.IntegralCompProd` `Mathlib.Probability.Kernel.Composition.Lemmas` `Mathlib.Probability.Kernel.Composition.MeasureCompProd` `Mathlib.Probability.Kernel.Composition.MeasureComp` `Mathlib.Probability.Kernel.Composition.ParallelComp` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Probability.Kernel.Condexp` `Mathlib.Probability.Kernel.Defs` `Mathlib.Probability.Kernel.Disintegration.Basic` `Mathlib.Probability.Kernel.Disintegration.CDFToKernel` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.Probability.Kernel.Integral` `Mathlib.Probability.Kernel.Invariance` `Mathlib.Probability.Kernel.MeasurableIntegral` `Mathlib.Probability.Kernel.MeasurableLIntegral` `Mathlib.Probability.Kernel.Proper` `Mathlib.Probability.Kernel.RadonNikodym` `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.IntegrableExpMul` `Mathlib.Probability.Moments.MGFAnalytic` `Mathlib.Probability.Notation` `Mathlib.Probability.ProbabilityMassFunction.Basic` `Mathlib.Probability.ProbabilityMassFunction.Binomial` `Mathlib.Probability.ProbabilityMassFunction.Constructions` `Mathlib.Probability.ProbabilityMassFunction.Integrals` `Mathlib.Probability.ProbabilityMassFunction.Monad` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Process.Filtration` `Mathlib.Probability.Process.HittingTime` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Process.Stopping` `Mathlib.Probability.StrongLaw` `Mathlib.Probability.UniformOn` `Mathlib.Probability.Variance` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.Perfection` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.Polynomial.Hermite.Gaussian` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Complex` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.Tactic.FunProp.ContDiff` `Mathlib.Tactic.FunProp.Differentiable` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.InfiniteSum.Real` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.Cardinality` `Mathlib.Topology.Algebra.Module.FiniteDimension` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Topology.Algebra.Polynomial` `Mathlib.Topology.Algebra.PontryaginDual` `Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous` `Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Topology.Baire.BaireMeasurable` `Mathlib.Topology.Baire.CompleteMetrizable` `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.Topology.CWComplex.Abstract.Basic` `Mathlib.Topology.CWComplex.Classical.Basic` `Mathlib.Topology.Category.CompHaus.Basic` `Mathlib.Topology.Category.CompHaus.EffectiveEpi` `Mathlib.Topology.Category.CompHaus.Frm` `Mathlib.Topology.Category.CompHaus.Limits` `Mathlib.Topology.Category.CompHaus.Projective` `Mathlib.Topology.Category.CompactlyGenerated` `Mathlib.Topology.Category.Compactum` `Mathlib.Topology.Category.DeltaGenerated` `Mathlib.Topology.Category.LightProfinite.AsLimit` `Mathlib.Topology.Category.LightProfinite.Basic` `Mathlib.Topology.Category.LightProfinite.EffectiveEpi` `Mathlib.Topology.Category.LightProfinite.Extend` `Mathlib.Topology.Category.LightProfinite.Limits` `Mathlib.Topology.Category.LightProfinite.Sequence` `Mathlib.Topology.Category.Locale` `Mathlib.Topology.Category.Profinite.AsLimit` `Mathlib.Topology.Category.Profinite.Basic` `Mathlib.Topology.Category.Profinite.CofilteredLimit` `Mathlib.Topology.Category.Profinite.EffectiveEpi` `Mathlib.Topology.Category.Profinite.Extend` `Mathlib.Topology.Category.Profinite.Limits` `Mathlib.Topology.Category.Profinite.Nobeling` `Mathlib.Topology.Category.Profinite.Product` `Mathlib.Topology.Category.Profinite.Projective` `Mathlib.Topology.Category.Stonean.Adjunctions` `Mathlib.Topology.Category.Stonean.Basic` `Mathlib.Topology.Category.Stonean.EffectiveEpi` `Mathlib.Topology.Category.Stonean.Limits` `Mathlib.Topology.Category.TopCat.Sphere` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.Topology.Compactness.DeltaGeneratedSpace` `Mathlib.Topology.ContinuousMap.Bounded.Basic` `Mathlib.Topology.ContinuousMap.Bounded.Star` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Topology.ContinuousMap.Ideals` `Mathlib.Topology.ContinuousMap.Polynomial` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.StoneWeierstrass` `Mathlib.Topology.ContinuousMap.Units` `Mathlib.Topology.ContinuousMap.Weierstrass` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.EMetricSpace.BoundedVariation` `Mathlib.Topology.Germ` `Mathlib.Topology.Instances.Complex` `Mathlib.Topology.Instances.ENNReal.Lemmas` `Mathlib.Topology.Instances.EReal.Lemmas` `Mathlib.Topology.Maps.Proper.CompactlyGenerated` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Topology.MetricSpace.Closeds` `Mathlib.Topology.MetricSpace.Contracting` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Topology.MetricSpace.GromovHausdorff` `Mathlib.Topology.MetricSpace.HausdorffDimension` `Mathlib.Topology.MetricSpace.HausdorffDistance` `Mathlib.Topology.MetricSpace.HolderNorm` `Mathlib.Topology.MetricSpace.Holder` `Mathlib.Topology.MetricSpace.Kuratowski` `Mathlib.Topology.MetricSpace.PartitionOfUnity` `Mathlib.Topology.MetricSpace.Perfect` `Mathlib.Topology.MetricSpace.PiNat` `Mathlib.Topology.MetricSpace.Polish` `Mathlib.Topology.MetricSpace.ThickenedIndicator` `Mathlib.Topology.MetricSpace.Thickening` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.Topology.Metrizable.Urysohn` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Topology.Semicontinuous` `Mathlib.Topology.Separation.CompletelyRegular` `Mathlib.Topology.Separation.NotNormal` `Mathlib.Topology.TietzeExtension` `Mathlib.Topology.UniformSpace.Dini` `Mathlib.Topology.UrysohnsBounded` `Mathlib.Topology.UrysohnsLemma` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.Topology.VectorBundle.Hom`	1
`Mathlib.Topology.Instances.ENNReal.Basic` (new file)	1122

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

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

To make room for a new Defs file in #22093.

grunweg · 2025-02-19T17:35:36Z

~~If this PR is to land, please land #22094 first, then rebase master and just apply 2560da2 instead. I can still do that tomorrow, starting Saturday, I'll be on holiday.~~ Just did so.

YaelDillies · 2025-02-19T17:58:38Z

The import decrease is quite small 😞. I wonder whether we can reduce imports even more by tweaking earlier files. @Vierkantor, I am sure you would be interested by this question

Vierkantor · 2025-02-19T20:43:51Z

I am definitely interested! I have been looking at some files downstream from here in the MeasureTheory hierarchy.

Vierkantor · 2025-02-19T20:44:08Z

I'll check it out when I have some time tomorrow.

To make room for a new Defs file in #22093.

Vierkantor · 2025-02-20T08:10:41Z

Mathlib/Analysis/Normed/Group/Continuity.lean

 -/
 import Mathlib.Analysis.Normed.Group.Basic
-import Mathlib.Topology.Instances.ENNReal.Defs
+import Mathlib.Topology.Instances.ENNReal.Basic


If I perform the shake here as instructed, then I do get a bit of reduction:

Files Import difference

Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.Topology.Instances.ENNReal.Defs -4

78 files
Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Analysis.Asymptotics.Lemmas Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Analysis.Asymptotics.Theta Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.Analysis.Normed.Field.Instances Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.Ultra Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.Continuity Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Analysis.Normed.Group.NullSubmodule Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.Normed.Group.SeparationQuotient Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Operator.Compact Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.Normed.Ring.Ultra Mathlib.Analysis.NormedSpace.BallAction Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.Analysis.NormedSpace.ENormedSpace Mathlib.Analysis.NormedSpace.Extr Mathlib.Analysis.NormedSpace.Int Mathlib.Analysis.NormedSpace.Real Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Analysis.Seminorm Mathlib.Data.Real.IsNonarchimedean Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.SumTwoSquares Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.RingTheory.WittVector.Compare Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.Polynomial Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Bornology.BoundedOperation Mathlib.Topology.CWComplex.Classical.Basic Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Topology.Germ Mathlib.Topology.UniformSpace.Dini
-1

963 files
Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Analysis.AbsoluteValue.Equivalence Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Analytic.Constructions 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.Polynomial Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.BoundedVariation Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Analysis.CStarAlgebra.GelfandDuality 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.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Analysis.Calculus.AddTorsor.AffineMap 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.Conformal.InnerProduct Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Calculus.Deriv.Linear 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.DiffContOnCl Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.TangentCone Mathlib.Analysis.Calculus.Taylor Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.Calculus.VectorField Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.Angle Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Circle Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.Complex.Isometry Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Convex.AmpleSet Mathlib.Analysis.Convex.Body Mathlib.Analysis.Convex.Cone.Closure Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Analysis.Convex.Cone.Proper Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.Convex.GaugeRescale Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.Normed Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Analysis.Convex.Uniform Mathlib.Analysis.Convolution Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle 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.PoissonSummation Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.Hofer Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.InnerProductSpace.Continuous Mathlib.Analysis.InnerProductSpace.Convex Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Analysis.InnerProductSpace.Projection Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.LocallyConvex.AbsConvexOpen Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Matrix Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.MeanInequalities Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Meromorphic.Basic Mathlib.Analysis.Meromorphic.Order Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Algebra.Basic Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Analysis.Normed.Field.ProperSpace Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Analysis.Normed.Group.Pointwise Mathlib.Analysis.Normed.Group.Quotient Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Analysis.Normed.Operator.Banach Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Normed.Order.UpperLower Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Analysis.Normed.Ring.SmoothingSeminorm Mathlib.Analysis.Normed.Ring.Units Mathlib.Analysis.NormedSpace.Connected Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.NormedSpace.RCLike Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.PSeries Mathlib.Analysis.Polynomial.Basic Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.RCLike.Lemmas Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.SpecialFunctions.Choose Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Analysis.SpecialFunctions.Exponential 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.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.SpecialFunctions.Log.PosLog Mathlib.Analysis.SpecialFunctions.Log.Summable Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Analysis.SpecificLimits.Basic Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.SpecificLimits.Normed Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.SumIntegralComparisons Mathlib.Analysis.SumOverResidueClass Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Condensed.AB Mathlib.Condensed.Basic Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.Data.Complex.Cardinality Mathlib.Data.Complex.ExponentialBounds Mathlib.Data.Complex.FiniteDimensional Mathlib.Data.Real.Cardinality Mathlib.Data.Real.Hyperreal Mathlib.Data.Real.Pi.Bounds Mathlib.Data.Real.Pi.Irrational Mathlib.Data.Real.Pi.Leibniz Mathlib.Data.Real.Pi.Wallis Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Dynamics.Ergodic.Conservative Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Dynamics.Ergodic.Function Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.FieldTheory.Galois.Profinite Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Basic 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.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Triangle Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Geometry.Manifold.BumpFunction Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.ConformalGroupoid 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.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.Basic 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.PartitionOfUnity Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Geometry.Manifold.VectorField Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.LinearAlgebra.Matrix.LDL Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Category.MeasCat Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Constructions.Pi Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.MeasureTheory.Constructions.Projective 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.Covering.VitaliFamily Mathlib.MeasureTheory.Covering.Vitali Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.MeasureTheory.Decomposition.IntegralRNDeriv Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.AEEqFun Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.AEEqOfLIntegral Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.MeasureTheory.Function.Egorov Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.Function.Floor Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L1Space.AEEqFun Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral Mathlib.MeasureTheory.Function.L1Space.Integrable Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.MeasureTheory.Function.LpOrder Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.MeasureTheory.Function.LpSpace.Basic 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.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Function.UnifTight Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Group.Action Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.Arithmetic Mathlib.MeasureTheory.Group.Convolution Mathlib.MeasureTheory.Group.Defs Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Group.LIntegral Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.MeasureTheory.Group.Measure Mathlib.MeasureTheory.Group.Pointwise Mathlib.MeasureTheory.Group.Prod Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average Mathlib.MeasureTheory.Integral.BochnerL1 Mathlib.MeasureTheory.Integral.Bochner Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.Indicator Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Integral.Marginal Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.MeasureTheory.Measure.AbsolutelyContinuous Mathlib.MeasureTheory.Measure.AddContent Mathlib.MeasureTheory.Measure.Comap Mathlib.MeasureTheory.Measure.Complex Mathlib.MeasureTheory.Measure.Content Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Measure.Count Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.Dirac Mathlib.MeasureTheory.Measure.Doubling Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.MeasureTheory.Measure.Hausdorff 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.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Map Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.Prod Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Measure.RegularityCompacts Mathlib.MeasureTheory.Measure.Restrict Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.MeasureTheory.Measure.Sub Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Measure.Trim Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Measure.WithDensity Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.MeasureTheory.Order.Lattice Mathlib.MeasureTheory.Order.UpperLower Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.MeasureTheory.OuterMeasure.BorelCantelli Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.MeasureTheory.OuterMeasure.OfAddContent Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.Bertrand Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.NumberTheory.ClassNumber.Finite Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.EulerProduct.Basic 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.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.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable 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 Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.NumberTheory.MulChar.Lemmas Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Embeddings Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.Ostrowski Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.NumberTheory.Transcendental.Lindemann.Init.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.VonMangoldt Mathlib.NumberTheory.WellApproximable Mathlib.NumberTheory.ZetaValues Mathlib.Order.Filter.ENNReal Mathlib.Probability.BorelCantelli Mathlib.Probability.CDF Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.ConditionalProbability Mathlib.Probability.Density Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Poisson Mathlib.Probability.Distributions.Uniform Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.Basic Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.Integrable Mathlib.Probability.Independence.Kernel Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Integration Mathlib.Probability.Kernel.Basic Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous Mathlib.Probability.Kernel.Composition.Basic Mathlib.Probability.Kernel.Composition.CompNotation Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Probability.Kernel.Composition.Lemmas Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Probability.Kernel.Composition.MeasureComp Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Defs Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.Invariance Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Probability.Kernel.Proper Mathlib.Probability.Kernel.RadonNikodym 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.IntegrableExpMul Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Notation Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Stopping Mathlib.Probability.StrongLaw Mathlib.Probability.UniformOn Mathlib.Probability.Variance Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.Perfection Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.Tactic.FunProp.ContDiff Mathlib.Tactic.FunProp.Differentiable Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Topology.Algebra.PontryaginDual Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Baire.BaireMeasurable Mathlib.Topology.Baire.CompleteMetrizable Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.CompHaus.Frm Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Locale Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.ContinuousMap.Ideals Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Topology.ContinuousMap.Units Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Topology.EMetricSpace.BoundedVariation Mathlib.Topology.Instances.Complex Mathlib.Topology.Instances.ENNReal.Lemmas Mathlib.Topology.Instances.EReal.Lemmas Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Topology.MetricSpace.Closeds Mathlib.Topology.MetricSpace.Contracting Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Topology.MetricSpace.Holder Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.Topology.MetricSpace.Perfect Mathlib.Topology.MetricSpace.PiNat Mathlib.Topology.MetricSpace.Polish Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.Topology.MetricSpace.Thickening Mathlib.Topology.Metrizable.Urysohn Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.PartitionOfUnity Mathlib.Topology.Semicontinuous Mathlib.Topology.Separation.CompletelyRegular Mathlib.Topology.Separation.NotNormal Mathlib.Topology.TietzeExtension Mathlib.Topology.UrysohnsBounded Mathlib.Topology.UrysohnsLemma Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.VectorBundle.Constructions Mathlib.Topology.VectorBundle.Hom
1

Mathlib.Topology.Instances.ENNReal.Basic (new file) 1122

Vierkantor · 2025-02-20T08:28:17Z

Looking at the import graph for Mathlib.Topology.Instances.ENNReal.Defs now, I see Mathlib.Topology.Instances.Real.Defs and its (transitive) dependencies are marked in grey, but the import chain Instances.Real.Defs -> Instances.NNReal.Defs -> Instances.ENNReal.Defs makes a lot of local sense. So indeed some upstream import refactoring might help out a lot here.

One thing I'm noticing is that the preceding TopologicalSpace.Instances._.Defs files contain quite a few imports because they provide many topological structures on the (E)(NN)Reals all at once. I think I prefer to place instances in the folder of the class, (as we tend to do it in Mathlib.Algebra): we might have a Topology.MetricSpace.Real file and a Topology.Algebra.Ring.Real file. Would that be a viable way to go forward here?

YaelDillies · 2025-02-20T10:23:30Z

Yes, that would make a lot of sense. Simultaneously, I am of the opinion that the difference between Real, NNReal, ENNReal is quite tenuous, so I would be happy to see the files merged in this direction (so only one .Real file per folder, instead of .Real, .NNReal, .ENNReal).

grunweg · 2025-02-20T17:13:46Z

I have started a zulip thread about the import question. Perhaps it's best to continue the discussion there.

grunweg · 2025-02-20T17:16:57Z

Let me add one last thing, though: thanks a lot for investigating! I'll be on holiday next week, but could help with any follow-up when I'm back.

Currently, `Topology/Instances` has files defining topological instances on various types, organized by the type the instance is defined on. This PR takes the `E?(NN)?Real` instances and organizes them instead by the class that the instance belongs to (and puts all the Real-derived types together). Restructuring in this way should hopefully allow us to work with simpler concepts while not having to define more advanced concepts at the same time. I want to make a follow-up PR reorganizing the lemmas in similar ways. This change was discussed in the comments for #22093: #22093 (comment) Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Importing.20ENNReal.20in.20normed.20groups

grunweg · 2025-03-05T11:08:58Z

#22562 is a much better import re-organisation: closing in favour of that one.

Currently, `Topology/Instances` has files defining topological instances on various types, organized by the type the instance is defined on. This PR takes the `E?(NN)?Real` instances and organizes them instead by the class that the instance belongs to (and puts all the Real-derived types together). Restructuring in this way should hopefully allow us to work with simpler concepts while not having to define more advanced concepts at the same time. I want to make a follow-up PR reorganizing the lemmas in similar ways. This change was discussed in the comments for #22093: #22093 (comment) Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Importing.20ENNReal.20in.20normed.20groups Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

grunweg added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 19, 2025

grunweg mentioned this pull request Feb 19, 2025

[Merged by Bors] - feat: add classes ContinuousENorm and ENormed(Add)(Comm)Monoid #21670

Closed

2 tasks

grunweg added a commit that referenced this pull request Feb 19, 2025

chore(Topology/Instances/ENNReal): rename Defs to Basic.lean

b96a674

To make room for a new Defs file in #22093.

grunweg mentioned this pull request Feb 19, 2025

chore(Topology/Instances/ENNReal): rename Defs to Basic.lean #22094

Closed

grunweg added a commit that referenced this pull request Feb 19, 2025

chore(Topology/Instances/ENNReal): rename Defs to Basic.lean

013edf8

To make room for a new Defs file in #22093.

grunweg requested a review from YaelDillies February 19, 2025 17:34

grunweg added 2 commits February 19, 2025 22:04

chore(Topology/Instances/ENNReal): rename Defs to Basic.lean

f322d99

To make room for a new Defs file in #22093.

chore: split out Defs.lean

1c31980

grunweg force-pushed the MR-split-ennreal-defs branch from c0cd5a4 to 1c31980 Compare February 19, 2025 21:04

Vierkantor reviewed Feb 20, 2025

View reviewed changes

Vierkantor mentioned this pull request Mar 4, 2025

[Merged by Bors] - chore(Topology/Instances/*Real): organize instances by class #22562

Closed

grunweg closed this Mar 5, 2025

grunweg deleted the MR-split-ennreal-defs branch March 5, 2025 11:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore(Topology/Instance/ENNReal): reduce `Defs` even more#22093

chore(Topology/Instance/ENNReal): reduce `Defs` even more#22093
grunweg wants to merge 2 commits intomasterfrom
MR-split-ennreal-defs

grunweg commented Feb 19, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Feb 19, 2025 •

edited

Loading

Import changes for modified files

Uh oh!

grunweg commented Feb 19, 2025 •

edited

Loading

Uh oh!

YaelDillies commented Feb 19, 2025

Uh oh!

Vierkantor commented Feb 19, 2025

Uh oh!

Vierkantor commented Feb 19, 2025

Uh oh!

Vierkantor Feb 20, 2025

Uh oh!

Vierkantor commented Feb 20, 2025

Uh oh!

YaelDillies commented Feb 20, 2025 •

edited

Loading

Uh oh!

grunweg commented Feb 20, 2025

Uh oh!

grunweg commented Feb 20, 2025

Uh oh!

grunweg commented Mar 5, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

grunweg commented Feb 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 1c31980474

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Feb 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies commented Feb 19, 2025

Uh oh!

Vierkantor commented Feb 19, 2025

Uh oh!

Vierkantor commented Feb 19, 2025

Uh oh!

Vierkantor Feb 20, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor commented Feb 20, 2025

Uh oh!

YaelDillies commented Feb 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg commented Feb 20, 2025

Uh oh!

grunweg commented Feb 20, 2025

Uh oh!

grunweg commented Mar 5, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

grunweg commented Feb 19, 2025 •

edited

Loading

github-actions bot commented Feb 19, 2025 •

edited

Loading

grunweg commented Feb 19, 2025 •

edited

Loading

YaelDillies commented Feb 20, 2025 •

edited

Loading