Skip to content

refactor: unbundle algebra from ENormed*#28803

Open
astrainfinita wants to merge 10 commits intoleanprover-community:masterfrom
astrainfinita:FR_enormed_mixin
Open

refactor: unbundle algebra from ENormed*#28803
astrainfinita wants to merge 10 commits intoleanprover-community:masterfrom
astrainfinita:FR_enormed_mixin

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented Aug 23, 2025 •
edited by bryangingechen
Loading

Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for TopologicalSpace.
This PR continues the work from #23961.

  • Change ESeminormed(Add)Monoid and ENormed(Add)Monoid so they no longer carry algebraic data.
  • Deprecate ESeminormed(Add)CommMonoid and ENormed(Add)CommMonoid in favor of ESeminormed(Add)Monoid and ENormed(Add)Monoid with a commutative algebraic typeclass.
Old New
[ESeminormed(Add)(Comm)Monoid E] [(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]
[ENormed(Add)(Comm)Monoid] [(Add)(Comm)Monoid E] [ENormed(Add)Monoid]

See Zulip discussion

@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Aug 23, 2025

Comments from Original PR #23961

This section contains 7 comment(s) from the original PR, excluding bot comments.

@astrainfinita (2025-04-11 20:55 UTC):
!bench

@grunweg (2025-04-12 08:21 UTC):
Actually, let me go one step further: the diff is straightforward - but I'd like another pair of eyes on

  • whether the TC changes are a good idea in general (I don't understand any subtleties well enough to be sure this is fine),
  • whether the TC metric in the benchmark results is a reason to worry, or we should just ignore it. (Looking at handful of comparisons which were labelled as "not significant", those seem to lie well within the noise levels.)
    maintainer merge?

@grunweg (2025-04-29 16:43 UTC):
Just as a heads-up: #24356 may cause another merge conflict in the same file.

@grunweg (2025-05-06 17:41 UTC):
And #24640 also has slight potential for conflicts (I haven't checked). That is hopefully the last PR modifiying this particular file.

@jcommelin (2025-06-07 07:03 UTC):

Actually, let me go one step further: the diff is straightforward - but I'd like another pair of eyes on

* whether the TC changes are a good idea in general (I don't understand any subtleties well enough to be sure this is fine),

* whether the TC metric in the benchmark results is a reason to worry, or we should just ignore it. (Looking at handful of comparisons which were labelled as "not significant", those seem to lie well within the noise levels.)
  maintainer merge?

This looks like a good change to me.

@FR-vdash-bot could you please respond to the open questions?

@grunweg (2025-08-23 09:33 UTC):
@astrainfinita Would you like to revive this PR? Otherwise, do you mind if I do?

@astrainfinita (2025-08-23 11:08 UTC):
Sorry, I had been away from lean for a few months before. I will revive it.

@astrainfinita astrainfinita mentioned this pull request Aug 23, 2025
Closed
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 23, 2025 •
edited
Loading

PR summary c3c8322bc4

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance : ENormedAddMonoid ℝ≥0∞
- NormedCommGroup.toENormedCommMonoid
- instance : ENormedAddCommMonoid ℝ≥0∞

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.

Increase in tech debt: (relative, absolute) = (2.00, 0.02)
Current number Change Type
86 2 disabled deprecation lints

Current commit 893698ed8b
Reference commit c3c8322bc4

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

@astrainfinita astrainfinita added t-analysis Analysis (normed *, calculus) t-algebra Algebra (groups, rings, fields, etc) slow-typeclass-synthesis bench-after-CI labels Aug 23, 2025
@grunweg grunweg added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 23, 2025
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Aug 23, 2025

Let me know once this PR passes CI, then I'll be happy to review it.

@grunweg grunweg self-assigned this Aug 23, 2025
@ghost
Copy link
Copy Markdown

ghost commented Aug 23, 2025

!bench

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 23, 2025
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 23, 2025

Here are the benchmark results for commit abfecc2.
There were significant changes against commit 3b09799:

  Benchmark                                                               Metric         Change
  =============================================================================================
+ ~Mathlib.Algebra.Module.ZLattice.Basic                                  instructions    -7.5%
+ ~Mathlib.Analysis.CStarAlgebra.CStarMatrix                              instructions   -13.1%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital   instructions    -5.8%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                               instructions    -4.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries                       instructions    -7.4%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic                              instructions    -5.5%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul                                   instructions    -3.5%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv                         instructions    -3.8%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                             instructions    -8.6%
+ ~Mathlib.Analysis.Normed.Lp.lpSpace                                     instructions   -19.6%
+ ~Mathlib.Analysis.Normed.Operator.LinearIsometry                        instructions    -7.1%
+ ~Mathlib.Analysis.NormedSpace.BallAction                                instructions   -11.4%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                         instructions    -7.7%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                         instructions    -7.0%
+ ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm         instructions   -14.4%
+ ~Mathlib.Analysis.Seminorm                                              instructions   -11.8%
+ ~Mathlib.Geometry.Manifold.MFDeriv.NormedSpace                          instructions    -6.2%
+ ~Mathlib.Geometry.Manifold.Riemannian.Basic                             instructions   -19.8%
+ ~Mathlib.Geometry.Manifold.VectorBundle.Hom                             instructions    -9.6%
+ ~Mathlib.Geometry.Manifold.VectorBundle.Riemannian                      instructions   -10.6%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement                           instructions   -16.4%
+ ~Mathlib.MeasureTheory.Function.Holder                                  instructions   -13.1%
+ ~Mathlib.MeasureTheory.Function.LpSpace.Basic                           instructions   -10.4%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                       instructions   -17.7%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain                          instructions   -16.7%
- ~Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic                  instructions    24.8%
+ ~Mathlib.NumberTheory.NumberField.Ideal.Basic                           instructions   -52.8%
+ ~Mathlib.NumberTheory.NumberField.Units.DirichletTheorem                instructions   -13.7%
+ ~Mathlib.Topology.Algebra.Module.FiniteDimension                        instructions   -10.6%
+ ~Mathlib.Topology.VectorBundle.Hom                                      instructions    -8.9%
+ ~Mathlib.Topology.VectorBundle.Riemannian                               instructions    -7.0%

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 23, 2025

File Instructions %
build -1245.679⬝10⁹ (-0.81%)
lint -153.398⬝10⁹ (-2.24%)
Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic +25.123⬝10⁹ (+24.82%)
2 files, Instructions +5.0⬝10⁹
File Instructions %
Mathlib.Geometry.Manifold.MFDeriv.Basic +5.640⬝10⁹ (+4.68%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Basic +5.222⬝10⁹ (+5.34%)
4 files, Instructions +2.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.FDeriv.Prod +2.730⬝10⁹ (+2.09%)
Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus +2.686⬝10⁹ (+3.94%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation +2.293⬝10⁹ (+4.04%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Affine +2.109⬝10⁹ (+3.47%)
13 files, Instructions +1.0⬝10⁹
File Instructions %
Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle +1.752⬝10⁹ (+3.11%)
Mathlib.Analysis.Calculus.ParametricIntegral +1.669⬝10⁹ (+3.12%)
Mathlib.Analysis.Convex.Continuous +1.499⬝10⁹ (+3.92%)
Mathlib.Analysis.BoxIntegral.Basic +1.415⬝10⁹ (+1.81%)
Mathlib.MeasureTheory.Integral.Bochner.Basic +1.315⬝10⁹ (+1.18%)
Mathlib.MeasureTheory.Function.UniformIntegrable +1.292⬝10⁹ (+2.09%)
Mathlib.Geometry.Euclidean.Angle.Sphere +1.275⬝10⁹ (+3.66%)
Mathlib.MeasureTheory.Function.LocallyIntegrable +1.188⬝10⁹ (+2.65%)
Mathlib.Analysis.Calculus.FDeriv.Add +1.166⬝10⁹ (+0.92%)
Mathlib.Analysis.Convex.Integral +1.111⬝10⁹ (+3.99%)
Mathlib.MeasureTheory.Integral.CircleAverage +1.73⬝10⁹ (+3.67%)
Mathlib.MeasureTheory.Integral.PeakFunction +1.66⬝10⁹ (+1.89%)
Mathlib.Analysis.Calculus.FDeriv.Star +1.24⬝10⁹ (+4.89%)
98 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.Analysis.LocallyConvex.Barrelled -1.9⬝10⁹ (-7.49%)
Mathlib.Probability.Independence.Basic -1.10⬝10⁹ (-2.24%)
Mathlib.Topology.Algebra.Module.Cardinality -1.28⬝10⁹ (-6.75%)
Mathlib.Analysis.SpecialFunctions.Pow.Complex -1.29⬝10⁹ (-4.18%)
Mathlib.Analysis.Normed.Module.Complemented -1.35⬝10⁹ (-3.26%)
Mathlib.Dynamics.Ergodic.Action.OfMinimal -1.37⬝10⁹ (-3.56%)
Mathlib.MeasureTheory.Measure.FiniteMeasure -1.39⬝10⁹ (-1.89%)
Mathlib.Analysis.Convex.Birkhoff -1.59⬝10⁹ (-2.71%)
Mathlib.MeasureTheory.Measure.Haar.OfBasis -1.67⬝10⁹ (-1.72%)
Mathlib.Analysis.Normed.Affine.ContinuousAffineMap -1.79⬝10⁹ (-2.19%)
Mathlib.Analysis.Analytic.Linear -1.81⬝10⁹ (-2.59%)
Mathlib.Topology.Algebra.Module.UniformConvergence -1.90⬝10⁹ (-7.77%)
Mathlib.NumberTheory.Padics.AddChar -1.94⬝10⁹ (-4.31%)
Mathlib.Topology.CWComplex.Classical.Basic -1.101⬝10⁹ (-2.09%)
Mathlib.Analysis.Convex.GaugeRescale -1.102⬝10⁹ (-4.90%)
Mathlib.Analysis.Normed.Group.Quotient -1.107⬝10⁹ (-3.30%)
Mathlib.NumberTheory.EulerProduct.Basic -1.109⬝10⁹ (-6.77%)
Mathlib.NumberTheory.DirichletCharacter.GaussSum -1.122⬝10⁹ (-5.93%)
Mathlib.Analysis.Calculus.FDeriv.Defs -1.126⬝10⁹ (-7.75%)
Mathlib.Analysis.Normed.Group.Uniform -1.131⬝10⁹ (-3.63%)
Mathlib.Analysis.Normed.Unbundled.FiniteExtension -1.139⬝10⁹ (-3.70%)
Mathlib.Analysis.NormedSpace.ConformalLinearMap -1.154⬝10⁹ (-7.87%)
Mathlib.Topology.ContinuousMap.Compact -1.156⬝10⁹ (-2.72%)
Mathlib.Analysis.CStarAlgebra.Module.Constructions -1.161⬝10⁹ (-1.85%)
Mathlib.LinearAlgebra.Matrix.Spectrum -1.165⬝10⁹ (-3.35%)
Mathlib.MeasureTheory.Group.Integral -1.167⬝10⁹ (-6.00%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent -1.170⬝10⁹ (-2.70%)
Mathlib.MeasureTheory.Integral.CircleIntegral -1.186⬝10⁹ (-1.86%)
Mathlib.Geometry.Manifold.ContMDiffMFDeriv -1.187⬝10⁹ (-1.99%)
Mathlib.NumberTheory.Cyclotomic.Gal -1.195⬝10⁹ (-7.51%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Series -1.202⬝10⁹ (-5.68%)
Mathlib.Analysis.MeanInequalities -1.203⬝10⁹ (-1.77%)
Mathlib.MeasureTheory.Function.AEEqFun.DomAct -1.216⬝10⁹ (-8.20%)
Mathlib.Topology.ContinuousMap.Ideals -1.217⬝10⁹ (-2.09%)
Mathlib.Topology.ContinuousMap.Bounded.Star -1.218⬝10⁹ (-9.45%)
Mathlib.NumberTheory.Cyclotomic.Discriminant -1.223⬝10⁹ (-3.32%)
Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk -1.225⬝10⁹ (-1.10%)
Mathlib.Analysis.Calculus.LocalExtr.LineDeriv -1.248⬝10⁹ (-8.23%)
Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable -1.249⬝10⁹ (-3.54%)
Mathlib.Analysis.PSeries -1.258⬝10⁹ (-2.41%)
Mathlib.Analysis.CStarAlgebra.Hom -1.261⬝10⁹ (-5.26%)
Mathlib.Topology.PartitionOfUnity -1.263⬝10⁹ (-4.40%)
Mathlib.NumberTheory.LSeries.Nonvanishing -1.270⬝10⁹ (-4.17%)
Mathlib.Analysis.CStarAlgebra.Basic -1.287⬝10⁹ (-4.56%)
Mathlib.MeasureTheory.Measure.Haar.Quotient -1.310⬝10⁹ (-2.77%)
Mathlib.Analysis.InnerProductSpace.Positive -1.315⬝10⁹ (-2.52%)
Mathlib.Analysis.Calculus.IteratedDeriv.Defs -1.339⬝10⁹ (-3.23%)
Mathlib.Analysis.Calculus.Deriv.Comp -1.357⬝10⁹ (-1.64%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation -1.366⬝10⁹ (-1.28%)
Mathlib.Analysis.Normed.Group.Pointwise -1.381⬝10⁹ (-5.87%)
Mathlib.Analysis.InnerProductSpace.StarOrder -1.382⬝10⁹ (-4.28%)
Mathlib.Analysis.InnerProductSpace.Symmetric -1.382⬝10⁹ (-4.14%)
Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions -1.386⬝10⁹ (-1.23%)
Mathlib.MeasureTheory.Measure.CharacteristicFunction -1.396⬝10⁹ (-2.77%)
Mathlib.Analysis.InnerProductSpace.LinearPMap -1.397⬝10⁹ (-3.35%)
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic -1.402⬝10⁹ (-2.88%)
Mathlib.Analysis.Complex.UnitDisc.Basic -1.425⬝10⁹ (-7.10%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd -1.439⬝10⁹ (-2.90%)
Mathlib.RingTheory.LittleWedderburn -1.441⬝10⁹ (-3.94%)
Mathlib.Analysis.InnerProductSpace.Subspace -1.445⬝10⁹ (-5.24%)
Mathlib.NumberTheory.Padics.PadicIntegers -1.446⬝10⁹ (-3.91%)
Mathlib.Combinatorics.SimpleGraph.Regularity.Bound -1.450⬝10⁹ (-4.20%)
Mathlib.Topology.Algebra.Valued.LocallyCompact -1.458⬝10⁹ (-2.43%)
Mathlib.Analysis.Normed.Operator.Banach -1.467⬝10⁹ (-1.26%)
Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual -1.486⬝10⁹ (-3.57%)
Mathlib.Topology.ContinuousMap.Bounded.Basic -1.487⬝10⁹ (-3.35%)
Mathlib.Analysis.Normed.Affine.Isometry -1.502⬝10⁹ (-1.74%)
Mathlib.Analysis.Normed.Algebra.Exponential -1.508⬝10⁹ (-2.66%)
Mathlib.RingTheory.Perfection -1.509⬝10⁹ (-3.17%)
Mathlib.Analysis.Analytic.OfScalars -1.514⬝10⁹ (-3.06%)
Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable -1.516⬝10⁹ (-2.08%)
Mathlib.Analysis.LocallyConvex.AbsConvexOpen -1.517⬝10⁹ (-9.86%)
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic -1.518⬝10⁹ (-3.35%)
Mathlib.NumberTheory.NumberField.Discriminant.Basic -1.519⬝10⁹ (-1.20%)
Mathlib.NumberTheory.ZetaValues -1.534⬝10⁹ (-3.58%)
Mathlib.Analysis.Calculus.Deriv.Pow -1.564⬝10⁹ (-4.65%)
Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar -1.565⬝10⁹ (-4.21%)
Mathlib.Analysis.Normed.Group.Basic -1.573⬝10⁹ (-2.16%)
Mathlib.NumberTheory.ModularForms.Basic -1.590⬝10⁹ (-3.98%)
Mathlib.Analysis.SpecialFunctions.Complex.LogBounds -1.594⬝10⁹ (-1.46%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Prod -1.602⬝10⁹ (-2.97%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic -1.611⬝10⁹ (-0.87%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi -1.623⬝10⁹ (-7.25%)
Mathlib.Analysis.Calculus.SmoothSeries -1.656⬝10⁹ (-3.58%)
Mathlib.MeasureTheory.Measure.Haar.DistribChar -1.692⬝10⁹ (-8.36%)
Mathlib.NumberTheory.Padics.MahlerBasis -1.697⬝10⁹ (-3.86%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital -1.763⬝10⁹ (-1.40%)
Mathlib.Analysis.Normed.Algebra.UnitizationL1 -1.774⬝10⁹ (-7.74%)
Mathlib.Analysis.InnerProductSpace.OfNorm -1.786⬝10⁹ (-3.20%)
Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real -1.800⬝10⁹ (-2.86%)
Mathlib.Analysis.LocallyConvex.ContinuousOfBounded -1.831⬝10⁹ (-9.11%)
Mathlib.Analysis.Calculus.ContDiff.RestrictScalars -1.862⬝10⁹ (-7.36%)
Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic -1.888⬝10⁹ (-3.42%)
Mathlib.Analysis.Analytic.Basic -1.902⬝10⁹ (-0.94%)
Mathlib.Analysis.LocallyConvex.Polar -1.903⬝10⁹ (-6.60%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 -1.919⬝10⁹ (-2.75%)
Mathlib.Probability.Moments.CovarianceBilin -1.928⬝10⁹ (-2.57%)
Mathlib.Analysis.Complex.CauchyIntegral -1.934⬝10⁹ (-3.71%)
67 files, Instructions -3.0⬝10⁹
File Instructions %
Mathlib.Analysis.CStarAlgebra.PositiveLinearMap -2.6⬝10⁹ (-5.32%)
Mathlib.NumberTheory.ClassNumber.Finite -2.27⬝10⁹ (-3.90%)
Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation -2.31⬝10⁹ (-1.41%)
Mathlib.Analysis.Normed.Module.FiniteDimension -2.67⬝10⁹ (-2.29%)
Mathlib.Analysis.NormedSpace.HahnBanach.Extension -2.119⬝10⁹ (-5.24%)
Mathlib.Analysis.LocallyConvex.AbsConvex -2.123⬝10⁹ (-9.02%)
Mathlib.Analysis.NormedSpace.Pointwise -2.138⬝10⁹ (-4.42%)
Mathlib.Analysis.Analytic.IsolatedZeros -2.140⬝10⁹ (-3.00%)
Mathlib.Analysis.Calculus.Deriv.Basic -2.147⬝10⁹ (-2.31%)
Mathlib.Analysis.InnerProductSpace.Orthonormal -2.151⬝10⁹ (-6.18%)
Mathlib.Analysis.LocallyConvex.BalancedCoreHull -2.159⬝10⁹ (-9.67%)
Mathlib.Topology.ContinuousMap.ZeroAtInfty -2.163⬝10⁹ (-4.57%)
Mathlib.Analysis.SpecialFunctions.Exponential -2.180⬝10⁹ (-3.92%)
Mathlib.Geometry.Manifold.GroupLieAlgebra -2.208⬝10⁹ (-5.45%)
Mathlib.RingTheory.ZMod.UnitsCyclic -2.218⬝10⁹ (-6.82%)
Mathlib.Geometry.Manifold.Instances.Sphere -2.236⬝10⁹ (-1.96%)
Mathlib.Analysis.Convex.Cone.Dual -2.243⬝10⁹ (-5.45%)
Mathlib.NumberTheory.Modular -2.244⬝10⁹ (-3.17%)
Mathlib.Analysis.LocallyConvex.WeakSpace -2.262⬝10⁹ (-7.05%)
Mathlib.NumberTheory.LSeries.AbstractFuncEq -2.264⬝10⁹ (-4.53%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody -2.280⬝10⁹ (-2.33%)
Mathlib.Analysis.NormedSpace.Extend -2.292⬝10⁹ (-8.83%)
Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear -2.295⬝10⁹ (-5.82%)
Mathlib.Analysis.RCLike.Basic -2.296⬝10⁹ (-1.96%)
Mathlib.Analysis.InnerProductSpace.Dual -2.297⬝10⁹ (-4.40%)
Mathlib.Analysis.CStarAlgebra.Unitization -2.323⬝10⁹ (-4.15%)
Mathlib.Analysis.SpecificLimits.Normed -2.330⬝10⁹ (-2.96%)
Mathlib.Analysis.CStarAlgebra.Spectrum -2.366⬝10⁹ (-5.10%)
Mathlib.Geometry.Manifold.VectorBundle.SmoothSection -2.377⬝10⁹ (-4.81%)
Mathlib.MeasureTheory.Integral.Bochner.Set -2.407⬝10⁹ (-2.70%)
Mathlib.Analysis.RCLike.Inner -2.421⬝10⁹ (-7.07%)
Mathlib.Analysis.Normed.Module.Dual -2.426⬝10⁹ (-3.64%)
Mathlib.NumberTheory.JacobiSum.Basic -2.427⬝10⁹ (-6.45%)
Mathlib.Analysis.NormedSpace.MStructure -2.429⬝10⁹ (-9.36%)
Mathlib.Analysis.Normed.Operator.Compact -2.436⬝10⁹ (-7.64%)
Mathlib.MeasureTheory.Measure.Haar.Unique -2.448⬝10⁹ (-2.78%)
Mathlib.NumberTheory.Cyclotomic.Rat -2.453⬝10⁹ (-1.93%)
Mathlib.Analysis.Convex.Body -2.467⬝10⁹ (-8.11%)
Mathlib.Analysis.FunctionalSpaces.SobolevInequality -2.470⬝10⁹ (-2.01%)
Mathlib.Analysis.Matrix -2.477⬝10⁹ (-4.35%)
Mathlib.Analysis.LocallyConvex.WeakDual -2.482⬝10⁹ (-8.64%)
Mathlib.NumberTheory.NumberField.Units.Basic -2.510⬝10⁹ (-4.73%)
Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral -2.516⬝10⁹ (-5.62%)
Mathlib.Analysis.Normed.Operator.ContinuousLinearMap -2.531⬝10⁹ (-10.78%)
Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm -2.561⬝10⁹ (-5.08%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique -2.563⬝10⁹ (-2.00%)
Mathlib.Analysis.NormedSpace.HahnBanach.Separation -2.576⬝10⁹ (-4.64%)
Mathlib.Analysis.Normed.Ring.Basic -2.581⬝10⁹ (-3.20%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic -2.601⬝10⁹ (-1.71%)
Mathlib.Analysis.Calculus.LineDeriv.Basic -2.624⬝10⁹ (-4.80%)
Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional -2.628⬝10⁹ (-4.04%)
Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform -2.652⬝10⁹ (-3.62%)
Mathlib.NumberTheory.LegendreSymbol.AddCharacter -2.659⬝10⁹ (-10.59%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable -2.662⬝10⁹ (-6.09%)
Mathlib.Analysis.Normed.Lp.ProdLp -2.688⬝10⁹ (-4.85%)
Mathlib.Analysis.Analytic.CPolynomialDef -2.738⬝10⁹ (-2.78%)
Mathlib.Topology.ContinuousMap.ContinuousMapZero -2.784⬝10⁹ (-4.96%)
Mathlib.Analysis.InnerProductSpace.LinearMap -2.796⬝10⁹ (-4.31%)
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits -2.818⬝10⁹ (-17.41%)
Mathlib.NumberTheory.MulChar.Lemmas -2.826⬝10⁹ (-16.75%)
Mathlib.NumberTheory.Cyclotomic.Three -2.829⬝10⁹ (-7.12%)
Mathlib.Topology.ContinuousMap.Bounded.Normed -2.884⬝10⁹ (-4.71%)
Mathlib.Analysis.Calculus.FDeriv.Symmetric -2.958⬝10⁹ (-2.50%)
Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap -2.959⬝10⁹ (-8.69%)
Mathlib.NumberTheory.Cyclotomic.Basic -2.990⬝10⁹ (-2.99%)
Mathlib.Analysis.Normed.Group.Hom -2.997⬝10⁹ (-7.33%)
Mathlib.NumberTheory.GaussSum -2.998⬝10⁹ (-8.58%)
23 files, Instructions -4.0⬝10⁹
File Instructions %
Mathlib.Algebra.Module.ZLattice.Covolume -3.63⬝10⁹ (-4.35%)
Mathlib.Analysis.Complex.Basic -3.185⬝10⁹ (-5.46%)
Mathlib.Analysis.Normed.Module.Basic -3.200⬝10⁹ (-6.51%)
Mathlib.Analysis.InnerProductSpace.Basic -3.234⬝10⁹ (-3.42%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity -3.250⬝10⁹ (-2.11%)
Mathlib.Analysis.Calculus.LineDeriv.Measurable -3.361⬝10⁹ (-16.52%)
Mathlib.MeasureTheory.Measure.Haar.Disintegration -3.385⬝10⁹ (-7.22%)
Mathlib.RingTheory.Invariant.Profinite -3.386⬝10⁹ (-2.02%)
Mathlib.Analysis.Normed.Algebra.Spectrum -3.410⬝10⁹ (-3.00%)
Mathlib.Analysis.InnerProductSpace.l2Space -3.416⬝10⁹ (-4.18%)
Mathlib.Analysis.Analytic.ConvergenceRadius -3.430⬝10⁹ (-3.25%)
Mathlib.Analysis.Asymptotics.Lemmas -3.538⬝10⁹ (-6.07%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric -3.699⬝10⁹ (-2.22%)
Mathlib.Analysis.LocallyConvex.WeakOperatorTopology -3.739⬝10⁹ (-9.15%)
Mathlib.Analysis.Normed.Algebra.Unitization -3.786⬝10⁹ (-6.28%)
Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter -3.788⬝10⁹ (-11.66%)
Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots -3.805⬝10⁹ (-6.13%)
Mathlib.Analysis.Analytic.IteratedFDeriv -3.806⬝10⁹ (-5.90%)
Mathlib.Analysis.Calculus.VectorField -3.813⬝10⁹ (-4.72%)
Mathlib.Analysis.Distribution.SchwartzSpace -3.816⬝10⁹ (-1.72%)
Mathlib.Analysis.InnerProductSpace.Defs -3.863⬝10⁹ (-7.74%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict -3.882⬝10⁹ (-4.80%)
Mathlib.Analysis.CStarAlgebra.Module.Defs -3.954⬝10⁹ (-6.62%)
14 files, Instructions -5.0⬝10⁹
File Instructions %
Mathlib.Analysis.Convex.EGauge -4.9⬝10⁹ (-10.31%)
Mathlib.LinearAlgebra.Matrix.PosDef -4.69⬝10⁹ (-5.60%)
Mathlib.Analysis.Fourier.FourierTransform -4.203⬝10⁹ (-5.74%)
Mathlib.Topology.ContinuousMap.CompactlySupported -4.220⬝10⁹ (-4.64%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 -4.349⬝10⁹ (-5.19%)
Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality -4.370⬝10⁹ (-13.68%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order -4.464⬝10⁹ (-2.66%)
Mathlib.Analysis.Fourier.ZMod -4.485⬝10⁹ (-14.60%)
Mathlib.Topology.Algebra.Module.Alternating.Topology -4.616⬝10⁹ (-12.20%)
Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction -4.674⬝10⁹ (-10.07%)
Mathlib.Analysis.Calculus.ContDiff.Defs -4.775⬝10⁹ (-2.38%)
Mathlib.Analysis.Analytic.Inverse -4.852⬝10⁹ (-3.63%)
Mathlib.Analysis.LocallyConvex.Bounded -4.939⬝10⁹ (-11.81%)
Mathlib.Analysis.Calculus.FDeriv.Pow -4.943⬝10⁹ (-6.63%)
14 files, Instructions -6.0⬝10⁹
File Instructions %
Mathlib.Analysis.Normed.Unbundled.SpectralNorm -5.15⬝10⁹ (-3.35%)
Mathlib.RingTheory.Polynomial.Cyclotomic.Basic -5.110⬝10⁹ (-11.17%)
Mathlib.Analysis.LocallyConvex.Basic -5.113⬝10⁹ (-15.08%)
Mathlib.Topology.Algebra.Module.Multilinear.Topology -5.222⬝10⁹ (-11.39%)
Mathlib.Analysis.Convex.Side -5.250⬝10⁹ (-6.46%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone -5.335⬝10⁹ (-5.86%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Mul -5.373⬝10⁹ (-8.36%)
Mathlib.Analysis.Convex.Gauge -5.381⬝10⁹ (-8.64%)
Mathlib.Analysis.Normed.Operator.BoundedLinearMaps -5.533⬝10⁹ (-7.45%)
Mathlib.Analysis.CStarAlgebra.Matrix -5.558⬝10⁹ (-5.62%)
Mathlib.Analysis.CStarAlgebra.ApproximateUnit -5.625⬝10⁹ (-3.07%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic -5.684⬝10⁹ (-5.23%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic -5.689⬝10⁹ (-3.07%)
Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar -5.973⬝10⁹ (-23.12%)
10 files, Instructions -7.0⬝10⁹
File Instructions %
Mathlib.Analysis.Analytic.Constructions -6.44⬝10⁹ (-3.05%)
Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno -6.92⬝10⁹ (-3.52%)
Mathlib.Topology.ContinuousMap.StoneWeierstrass -6.332⬝10⁹ (-3.78%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic -6.345⬝10⁹ (-8.63%)
Mathlib.Analysis.Analytic.ChangeOrigin -6.364⬝10⁹ (-6.60%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances -6.412⬝10⁹ (-4.08%)
Mathlib.Analysis.Convolution -6.494⬝10⁹ (-1.97%)
Mathlib.Analysis.InnerProductSpace.PiL2 -6.601⬝10⁹ (-3.78%)
Mathlib.Analysis.Calculus.ContDiff.Bounds -6.673⬝10⁹ (-4.81%)
Mathlib.Analysis.Analytic.Composition -6.921⬝10⁹ (-4.76%)
7 files, Instructions -8.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.Deriv.Mul -7.17⬝10⁹ (-4.11%)
Mathlib.Analysis.Normed.Lp.PiLp -7.24⬝10⁹ (-8.14%)
Mathlib.Analysis.Calculus.ContDiff.Operations -7.390⬝10⁹ (-3.97%)
Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic -7.417⬝10⁹ (-25.67%)
Mathlib.Analysis.LocallyConvex.WithSeminorms -7.547⬝10⁹ (-8.16%)
Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt -7.810⬝10⁹ (-9.95%)
Mathlib.Analysis.Calculus.Implicit -7.926⬝10⁹ (-6.99%)
4 files, Instructions -9.0⬝10⁹
File Instructions %
Mathlib.NumberTheory.FLT.Three -8.16⬝10⁹ (-6.98%)
Mathlib.Geometry.Manifold.Instances.Icc -8.531⬝10⁹ (-27.82%)
Mathlib.Analysis.NormedSpace.Alternating.Basic -8.629⬝10⁹ (-8.35%)
Mathlib.Analysis.CStarAlgebra.Multiplier -8.875⬝10⁹ (-6.77%)
6 files, Instructions -10.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.FormalMultilinearSeries -9.196⬝10⁹ (-11.27%)
Mathlib.Analysis.Asymptotics.TVS -9.575⬝10⁹ (-10.16%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear -9.794⬝10⁹ (-5.99%)
Mathlib.FieldTheory.Galois.Profinite -9.855⬝10⁹ (-8.75%)
Mathlib.Topology.Algebra.Module.StrongTopology -9.906⬝10⁹ (-12.13%)
Mathlib.Geometry.Manifold.ContMDiff.NormedSpace -9.948⬝10⁹ (-6.80%)
3 files, Instructions -11.0⬝10⁹
File Instructions %
Mathlib.Algebra.Module.ZLattice.Basic -10.361⬝10⁹ (-7.54%)
Mathlib.NumberTheory.NumberField.Units.DirichletTheorem -10.417⬝10⁹ (-13.67%)
Mathlib.Analysis.NormedSpace.BallAction -10.699⬝10⁹ (-11.44%)
8 files, Instructions -12.0⬝10⁹
File Instructions %
Mathlib.Geometry.Manifold.MFDeriv.NormedSpace -11.67⬝10⁹ (-6.23%)
Mathlib.Topology.Algebra.Module.FiniteDimension -11.82⬝10⁹ (-10.57%)
Mathlib.MeasureTheory.Function.Holder -11.97⬝10⁹ (-13.06%)
Mathlib.MeasureTheory.Function.LpSpace.Basic -11.132⬝10⁹ (-10.39%)
Mathlib.Analysis.Calculus.ContDiff.Basic -11.240⬝10⁹ (-4.01%)
Mathlib.Topology.VectorBundle.Hom -11.546⬝10⁹ (-8.87%)
Mathlib.Analysis.Normed.Operator.LinearIsometry -11.659⬝10⁹ (-7.11%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital -11.677⬝10⁹ (-5.76%)
4 files, Instructions -13.0⬝10⁹
File Instructions %
Mathlib.NumberTheory.NumberField.Ideal.Basic -12.153⬝10⁹ (-52.80%)
Mathlib.Topology.VectorBundle.Riemannian -12.166⬝10⁹ (-6.95%)
Mathlib.Analysis.Fourier.FourierTransformDeriv -12.563⬝10⁹ (-3.82%)
Mathlib.Analysis.Calculus.FDeriv.Analytic -12.835⬝10⁹ (-5.54%)
File Instructions %
Mathlib.LinearAlgebra.Matrix.SchurComplement -13.321⬝10⁹ (-16.35%)
2 files, Instructions -15.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.FDeriv.Mul -14.523⬝10⁹ (-3.54%)
Mathlib.Geometry.Manifold.VectorBundle.Riemannian -14.671⬝10⁹ (-10.63%)
2 files, Instructions -16.0⬝10⁹
File Instructions %
Mathlib.Analysis.NormedSpace.Multilinear.Curry -15.575⬝10⁹ (-7.04%)
Mathlib.Geometry.Manifold.VectorBundle.Hom -15.849⬝10⁹ (-9.56%)
2 files, Instructions -18.0⬝10⁹
File Instructions %
Mathlib.Analysis.CStarAlgebra.CStarMatrix -17.133⬝10⁹ (-13.08%)
Mathlib.Analysis.Seminorm -17.289⬝10⁹ (-11.77%)
3 files, Instructions -19.0⬝10⁹
File Instructions %
Mathlib.Analysis.NormedSpace.Multilinear.Basic -18.652⬝10⁹ (-7.72%)
Mathlib.Geometry.Manifold.Riemannian.Basic -18.764⬝10⁹ (-19.82%)
Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries -18.896⬝10⁹ (-7.42%)
2 files, Instructions -20.0⬝10⁹
File Instructions %
Mathlib.MeasureTheory.Group.FundamentalDomain -19.804⬝10⁹ (-16.74%)
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp -19.837⬝10⁹ (-17.70%)
File Instructions %
Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm -21.367⬝10⁹ (-14.37%)
Mathlib.Analysis.InnerProductSpace.Adjoint -22.900⬝10⁹ (-8.57%)
Mathlib.Analysis.Normed.Lp.lpSpace -40.826⬝10⁹ (-19.62%)
CI run Lakeprof report

@ghost
Copy link
Copy Markdown

ghost commented Aug 23, 2025

!bench

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Aug 23, 2025 •
edited
Loading

The last commit is even a slight typeclass generalisation. Nice find; let me PR that separately (edit: #28813).

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 23, 2025

Here are the benchmark results for commit 584bd7f.
There were significant changes against commit 3b09799:

  Benchmark                                                               Metric         Change
  =============================================================================================
+ ~Mathlib.Algebra.Module.ZLattice.Basic                                  instructions    -7.6%
+ ~Mathlib.Analysis.CStarAlgebra.CStarMatrix                              instructions   -13.1%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital   instructions    -5.8%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                               instructions    -4.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries                       instructions    -7.4%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic                              instructions    -5.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul                                   instructions    -3.5%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv                         instructions    -3.8%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                             instructions    -8.6%
+ ~Mathlib.Analysis.Normed.Lp.lpSpace                                     instructions   -19.6%
+ ~Mathlib.Analysis.Normed.Operator.LinearIsometry                        instructions    -7.1%
+ ~Mathlib.Analysis.NormedSpace.BallAction                                instructions   -11.5%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                         instructions    -7.7%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                         instructions    -6.9%
+ ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm         instructions   -14.4%
+ ~Mathlib.Analysis.Seminorm                                              instructions   -11.8%
+ ~Mathlib.Geometry.Manifold.MFDeriv.NormedSpace                          instructions    -6.2%
+ ~Mathlib.Geometry.Manifold.Riemannian.Basic                             instructions   -19.8%
+ ~Mathlib.Geometry.Manifold.VectorBundle.Hom                             instructions    -9.5%
+ ~Mathlib.Geometry.Manifold.VectorBundle.Riemannian                      instructions   -10.6%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement                           instructions   -16.5%
+ ~Mathlib.MeasureTheory.Function.Holder                                  instructions   -13.0%
+ ~Mathlib.MeasureTheory.Function.LpSpace.Basic                           instructions   -10.5%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                       instructions   -17.7%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain                          instructions   -16.7%
+ ~Mathlib.NumberTheory.NumberField.Ideal.Basic                           instructions   -53.2%
+ ~Mathlib.NumberTheory.NumberField.Units.DirichletTheorem                instructions   -13.6%
+ ~Mathlib.Topology.Algebra.Module.FiniteDimension                        instructions   -10.5%
+ ~Mathlib.Topology.VectorBundle.Hom                                      instructions    -8.8%
+ ~Mathlib.Topology.VectorBundle.Riemannian                               instructions    -6.9%

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 23, 2025

File Instructions %
build -1252.163⬝10⁹ (-0.81%)
lint -153.689⬝10⁹ (-2.24%)
Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic +6.116⬝10⁹ (+6.04%)
2 files, Instructions +5.0⬝10⁹
File Instructions %
Mathlib.Geometry.Manifold.MFDeriv.Basic +5.740⬝10⁹ (+4.76%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Basic +5.224⬝10⁹ (+5.34%)
3 files, Instructions +2.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.FDeriv.Prod +2.728⬝10⁹ (+2.09%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation +2.293⬝10⁹ (+4.04%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Affine +2.114⬝10⁹ (+3.48%)
14 files, Instructions +1.0⬝10⁹
File Instructions %
Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus +1.958⬝10⁹ (+2.87%)
Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle +1.758⬝10⁹ (+3.12%)
Mathlib.Analysis.Calculus.ParametricIntegral +1.559⬝10⁹ (+2.91%)
Mathlib.MeasureTheory.Function.LocallyIntegrable +1.475⬝10⁹ (+3.29%)
Mathlib.Analysis.Convex.Continuous +1.405⬝10⁹ (+3.67%)
Mathlib.MeasureTheory.Integral.Bochner.Basic +1.322⬝10⁹ (+1.19%)
Mathlib.MeasureTheory.Function.UniformIntegrable +1.279⬝10⁹ (+2.07%)
Mathlib.Geometry.Euclidean.Angle.Sphere +1.271⬝10⁹ (+3.65%)
Mathlib.Analysis.BoxIntegral.Basic +1.232⬝10⁹ (+1.57%)
Mathlib.Analysis.Calculus.FDeriv.Add +1.215⬝10⁹ (+0.96%)
Mathlib.MeasureTheory.Integral.SetToL1 +1.157⬝10⁹ (+0.49%)
Mathlib.Analysis.Calculus.FDeriv.Star +1.115⬝10⁹ (+5.33%)
Mathlib.Analysis.Convex.Integral +1.115⬝10⁹ (+4.01%)
Mathlib.MeasureTheory.Integral.CircleAverage +1.76⬝10⁹ (+3.68%)
99 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.Gradient.Basic -1.0⬝10⁹ (-1.77%)
Mathlib.Analysis.LocallyConvex.Barrelled -1.14⬝10⁹ (-7.53%)
Mathlib.MeasureTheory.Integral.CircleIntegral -1.21⬝10⁹ (-1.60%)
Mathlib.Analysis.Complex.Conformal -1.24⬝10⁹ (-2.31%)
Mathlib.Analysis.SpecialFunctions.Pow.Complex -1.26⬝10⁹ (-4.17%)
Mathlib.Topology.Algebra.Module.Cardinality -1.26⬝10⁹ (-6.74%)
Mathlib.Analysis.Normed.Module.Complemented -1.31⬝10⁹ (-3.25%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Prod -1.54⬝10⁹ (-1.96%)
Mathlib.Topology.Algebra.Module.UniformConvergence -1.92⬝10⁹ (-7.79%)
Mathlib.NumberTheory.Padics.AddChar -1.96⬝10⁹ (-4.31%)
Mathlib.Topology.CWComplex.Classical.Basic -1.97⬝10⁹ (-2.09%)
Mathlib.Analysis.Convex.GaugeRescale -1.103⬝10⁹ (-4.90%)
Mathlib.Analysis.Normed.Group.Quotient -1.111⬝10⁹ (-3.31%)
Mathlib.NumberTheory.EulerProduct.Basic -1.111⬝10⁹ (-6.78%)
Mathlib.Analysis.Analytic.CPolynomial -1.114⬝10⁹ (-2.27%)
Mathlib.NumberTheory.DirichletCharacter.GaussSum -1.121⬝10⁹ (-5.92%)
Mathlib.Analysis.Calculus.FDeriv.Defs -1.128⬝10⁹ (-7.77%)
Mathlib.Dynamics.Ergodic.Action.OfMinimal -1.128⬝10⁹ (-3.88%)
Mathlib.Analysis.Normed.Group.Uniform -1.138⬝10⁹ (-3.65%)
Mathlib.Analysis.LocallyConvex.AbsConvexOpen -1.149⬝10⁹ (-7.46%)
Mathlib.Analysis.NormedSpace.ConformalLinearMap -1.152⬝10⁹ (-7.86%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent -1.159⬝10⁹ (-2.68%)
Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable -1.163⬝10⁹ (-3.29%)
Mathlib.MeasureTheory.Measure.Haar.OfBasis -1.167⬝10⁹ (-1.88%)
Mathlib.MeasureTheory.Group.Integral -1.167⬝10⁹ (-6.00%)
Mathlib.LinearAlgebra.Matrix.Spectrum -1.172⬝10⁹ (-3.37%)
Mathlib.Geometry.Manifold.ContMDiffMFDeriv -1.190⬝10⁹ (-1.99%)
Mathlib.NumberTheory.Cyclotomic.Gal -1.193⬝10⁹ (-7.50%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Series -1.200⬝10⁹ (-5.68%)
Mathlib.NumberTheory.Cyclotomic.Discriminant -1.208⬝10⁹ (-3.28%)
Mathlib.Analysis.MeanInequalities -1.213⬝10⁹ (-1.79%)
Mathlib.MeasureTheory.Function.AEEqFun.DomAct -1.215⬝10⁹ (-8.19%)
Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk -1.239⬝10⁹ (-1.11%)
Mathlib.Analysis.Calculus.LocalExtr.LineDeriv -1.248⬝10⁹ (-8.23%)
Mathlib.Topology.ContinuousMap.Compact -1.256⬝10⁹ (-2.96%)
Mathlib.Analysis.CStarAlgebra.Module.Constructions -1.257⬝10⁹ (-2.00%)
Mathlib.Analysis.CStarAlgebra.Hom -1.262⬝10⁹ (-5.26%)
Mathlib.Topology.PartitionOfUnity -1.264⬝10⁹ (-4.40%)
Mathlib.Analysis.Calculus.Deriv.Comp -1.271⬝10⁹ (-1.53%)
Mathlib.NumberTheory.LSeries.Nonvanishing -1.272⬝10⁹ (-4.18%)
Mathlib.Analysis.CStarAlgebra.Basic -1.286⬝10⁹ (-4.56%)
Mathlib.Topology.ContinuousMap.Ideals -1.303⬝10⁹ (-2.24%)
Mathlib.MeasureTheory.Measure.Haar.Quotient -1.307⬝10⁹ (-2.77%)
Mathlib.Analysis.Normed.Unbundled.FiniteExtension -1.314⬝10⁹ (-4.26%)
Mathlib.Analysis.InnerProductSpace.Positive -1.324⬝10⁹ (-2.54%)
Mathlib.Analysis.Calculus.IteratedDeriv.Defs -1.341⬝10⁹ (-3.23%)
Mathlib.Analysis.PSeries -1.346⬝10⁹ (-2.58%)
Mathlib.Combinatorics.SimpleGraph.Regularity.Bound -1.359⬝10⁹ (-3.94%)
Mathlib.Analysis.InnerProductSpace.Symmetric -1.363⬝10⁹ (-4.09%)
Mathlib.Analysis.Normed.Group.Pointwise -1.380⬝10⁹ (-5.86%)
Mathlib.Analysis.InnerProductSpace.StarOrder -1.383⬝10⁹ (-4.28%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation -1.386⬝10⁹ (-1.30%)
Mathlib.Analysis.InnerProductSpace.LinearPMap -1.387⬝10⁹ (-3.33%)
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic -1.404⬝10⁹ (-2.89%)
Mathlib.Analysis.Normed.Affine.Isometry -1.406⬝10⁹ (-1.63%)
Mathlib.MeasureTheory.Measure.CharacteristicFunction -1.420⬝10⁹ (-2.81%)
Mathlib.Analysis.Complex.UnitDisc.Basic -1.423⬝10⁹ (-7.09%)
Mathlib.Analysis.Normed.Operator.Banach -1.432⬝10⁹ (-1.23%)
Mathlib.Analysis.Analytic.Linear -1.445⬝10⁹ (-3.46%)
Mathlib.RingTheory.LittleWedderburn -1.448⬝10⁹ (-3.96%)
Mathlib.Topology.Algebra.Valued.LocallyCompact -1.459⬝10⁹ (-2.43%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd -1.465⬝10⁹ (-2.95%)
Mathlib.Topology.ContinuousMap.Bounded.Basic -1.476⬝10⁹ (-3.33%)
Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual -1.486⬝10⁹ (-3.57%)
Mathlib.Analysis.Analytic.OfScalars -1.498⬝10⁹ (-3.03%)
Mathlib.Analysis.Normed.Algebra.Exponential -1.507⬝10⁹ (-2.66%)
Mathlib.NumberTheory.NumberField.Discriminant.Basic -1.514⬝10⁹ (-1.20%)
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic -1.519⬝10⁹ (-3.35%)
Mathlib.NumberTheory.Padics.PadicIntegers -1.538⬝10⁹ (-4.16%)
Mathlib.NumberTheory.ZetaValues -1.551⬝10⁹ (-3.62%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic -1.567⬝10⁹ (-0.84%)
Mathlib.Analysis.Calculus.Deriv.Pow -1.568⬝10⁹ (-4.66%)
Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar -1.570⬝10⁹ (-4.22%)
Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions -1.573⬝10⁹ (-1.39%)
Mathlib.Analysis.Normed.Group.Basic -1.576⬝10⁹ (-2.16%)
Mathlib.NumberTheory.ModularForms.Basic -1.584⬝10⁹ (-3.97%)
Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable -1.596⬝10⁹ (-2.19%)
Mathlib.RingTheory.Perfection -1.599⬝10⁹ (-3.36%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi -1.621⬝10⁹ (-7.24%)
Mathlib.Analysis.Calculus.SmoothSeries -1.662⬝10⁹ (-3.60%)
Mathlib.NumberTheory.Padics.MahlerBasis -1.694⬝10⁹ (-3.85%)
Mathlib.MeasureTheory.Measure.Haar.DistribChar -1.695⬝10⁹ (-8.37%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital -1.747⬝10⁹ (-1.39%)
Mathlib.Analysis.InnerProductSpace.OfNorm -1.761⬝10⁹ (-3.16%)
Mathlib.Analysis.SpecialFunctions.Complex.LogBounds -1.768⬝10⁹ (-1.62%)
Mathlib.Analysis.Normed.Algebra.UnitizationL1 -1.777⬝10⁹ (-7.75%)
Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real -1.816⬝10⁹ (-2.88%)
Mathlib.NumberTheory.Modular -1.856⬝10⁹ (-2.62%)
Mathlib.Analysis.Analytic.Basic -1.858⬝10⁹ (-0.91%)
Mathlib.Analysis.Calculus.ContDiff.RestrictScalars -1.861⬝10⁹ (-7.36%)
Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic -1.910⬝10⁹ (-3.46%)
Mathlib.Probability.Moments.CovarianceBilin -1.912⬝10⁹ (-2.55%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 -1.913⬝10⁹ (-2.74%)
Mathlib.NumberTheory.ClassNumber.Finite -1.923⬝10⁹ (-3.70%)
Mathlib.Analysis.LocallyConvex.ContinuousOfBounded -1.925⬝10⁹ (-9.58%)
Mathlib.Analysis.Complex.CauchyIntegral -1.929⬝10⁹ (-3.70%)
Mathlib.Analysis.NormedSpace.HahnBanach.Extension -1.936⬝10⁹ (-4.79%)
Mathlib.Analysis.Calculus.Deriv.Basic -1.948⬝10⁹ (-2.09%)
Mathlib.Analysis.InnerProductSpace.Orthonormal -1.974⬝10⁹ (-5.67%)
62 files, Instructions -3.0⬝10⁹
File Instructions %
Mathlib.Analysis.CStarAlgebra.PositiveLinearMap -2.24⬝10⁹ (-5.37%)
Mathlib.Analysis.Normed.Module.FiniteDimension -2.46⬝10⁹ (-2.27%)
Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation -2.47⬝10⁹ (-1.42%)
Mathlib.Analysis.LocallyConvex.Polar -2.87⬝10⁹ (-7.24%)
Mathlib.Analysis.InnerProductSpace.Dual -2.116⬝10⁹ (-4.05%)
Mathlib.Topology.ContinuousMap.Bounded.Normed -2.127⬝10⁹ (-3.47%)
Mathlib.Analysis.Analytic.IsolatedZeros -2.132⬝10⁹ (-2.99%)
Mathlib.Analysis.NormedSpace.Pointwise -2.153⬝10⁹ (-4.45%)
Mathlib.Analysis.LocallyConvex.BalancedCoreHull -2.158⬝10⁹ (-9.66%)
Mathlib.Topology.ContinuousMap.ZeroAtInfty -2.159⬝10⁹ (-4.56%)
Mathlib.Analysis.SpecialFunctions.Exponential -2.181⬝10⁹ (-3.92%)
Mathlib.NumberTheory.LSeries.AbstractFuncEq -2.182⬝10⁹ (-4.36%)
Mathlib.Geometry.Manifold.GroupLieAlgebra -2.205⬝10⁹ (-5.44%)
Mathlib.Analysis.Convex.Cone.Dual -2.227⬝10⁹ (-5.42%)
Mathlib.Analysis.LocallyConvex.WeakSpace -2.256⬝10⁹ (-7.03%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody -2.279⬝10⁹ (-2.33%)
Mathlib.Geometry.Manifold.VectorBundle.SmoothSection -2.284⬝10⁹ (-4.62%)
Mathlib.Analysis.NormedSpace.Extend -2.294⬝10⁹ (-8.84%)
Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear -2.297⬝10⁹ (-5.82%)
Mathlib.Analysis.RCLike.Basic -2.301⬝10⁹ (-1.96%)
Mathlib.RingTheory.ZMod.UnitsCyclic -2.305⬝10⁹ (-7.09%)
Mathlib.Analysis.LocallyConvex.AbsConvex -2.307⬝10⁹ (-9.80%)
Mathlib.Analysis.SpecificLimits.Normed -2.322⬝10⁹ (-2.95%)
Mathlib.Analysis.Normed.Module.Dual -2.325⬝10⁹ (-3.49%)
Mathlib.Analysis.CStarAlgebra.Unitization -2.326⬝10⁹ (-4.16%)
Mathlib.Analysis.RCLike.Inner -2.331⬝10⁹ (-6.81%)
Mathlib.Analysis.Normed.Operator.Compact -2.349⬝10⁹ (-7.37%)
Mathlib.Analysis.CStarAlgebra.Spectrum -2.368⬝10⁹ (-5.10%)
Mathlib.MeasureTheory.Integral.Bochner.Set -2.413⬝10⁹ (-2.71%)
Mathlib.Analysis.NormedSpace.MStructure -2.423⬝10⁹ (-9.33%)
Mathlib.NumberTheory.Cyclotomic.Rat -2.423⬝10⁹ (-1.91%)
Mathlib.MeasureTheory.Measure.Haar.Unique -2.426⬝10⁹ (-2.75%)
Mathlib.NumberTheory.JacobiSum.Basic -2.428⬝10⁹ (-6.46%)
Mathlib.Analysis.Convex.Body -2.472⬝10⁹ (-8.13%)
Mathlib.Analysis.LocallyConvex.WeakDual -2.483⬝10⁹ (-8.64%)
Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral -2.519⬝10⁹ (-5.63%)
Mathlib.Analysis.Calculus.LineDeriv.Basic -2.526⬝10⁹ (-4.62%)
Mathlib.Analysis.Normed.Operator.ContinuousLinearMap -2.532⬝10⁹ (-10.78%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique -2.544⬝10⁹ (-1.98%)
Mathlib.Analysis.Analytic.CPolynomialDef -2.566⬝10⁹ (-2.61%)
Mathlib.Analysis.NormedSpace.HahnBanach.Separation -2.573⬝10⁹ (-4.63%)
Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm -2.575⬝10⁹ (-5.11%)
Mathlib.Analysis.Matrix -2.576⬝10⁹ (-4.53%)
Mathlib.Analysis.Normed.Ring.Basic -2.580⬝10⁹ (-3.20%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic -2.591⬝10⁹ (-1.71%)
Mathlib.NumberTheory.NumberField.Units.Basic -2.609⬝10⁹ (-4.92%)
Mathlib.Analysis.FunctionalSpaces.SobolevInequality -2.624⬝10⁹ (-2.13%)
Mathlib.NumberTheory.LegendreSymbol.AddCharacter -2.659⬝10⁹ (-10.59%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable -2.662⬝10⁹ (-6.09%)
Mathlib.Geometry.Manifold.Instances.Sphere -2.674⬝10⁹ (-2.35%)
Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional -2.725⬝10⁹ (-4.19%)
Mathlib.NumberTheory.Cyclotomic.Three -2.735⬝10⁹ (-6.89%)
Mathlib.Analysis.Normed.Lp.ProdLp -2.786⬝10⁹ (-5.02%)
Mathlib.Topology.ContinuousMap.ContinuousMapZero -2.787⬝10⁹ (-4.97%)
Mathlib.Analysis.InnerProductSpace.LinearMap -2.794⬝10⁹ (-4.30%)
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits -2.818⬝10⁹ (-17.41%)
Mathlib.NumberTheory.MulChar.Lemmas -2.828⬝10⁹ (-16.76%)
Mathlib.NumberTheory.GaussSum -2.901⬝10⁹ (-8.30%)
Mathlib.Algebra.Module.ZLattice.Covolume -2.956⬝10⁹ (-4.19%)
Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap -2.960⬝10⁹ (-8.69%)
Mathlib.Analysis.Calculus.FDeriv.Symmetric -2.967⬝10⁹ (-2.51%)
Mathlib.Analysis.Normed.Group.Hom -2.986⬝10⁹ (-7.31%)
24 files, Instructions -4.0⬝10⁹
File Instructions %
Mathlib.NumberTheory.Cyclotomic.Basic -3.26⬝10⁹ (-3.02%)
Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform -3.103⬝10⁹ (-4.24%)
Mathlib.Analysis.Normed.Module.Basic -3.113⬝10⁹ (-6.34%)
Mathlib.Analysis.Complex.Basic -3.158⬝10⁹ (-5.41%)
Mathlib.Analysis.InnerProductSpace.Basic -3.179⬝10⁹ (-3.36%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity -3.273⬝10⁹ (-2.12%)
Mathlib.Analysis.Calculus.LineDeriv.Measurable -3.358⬝10⁹ (-16.51%)
Mathlib.MeasureTheory.Measure.Haar.Disintegration -3.383⬝10⁹ (-7.22%)
Mathlib.Analysis.Normed.Algebra.Spectrum -3.395⬝10⁹ (-2.99%)
Mathlib.Analysis.InnerProductSpace.l2Space -3.429⬝10⁹ (-4.20%)
Mathlib.RingTheory.Invariant.Profinite -3.441⬝10⁹ (-2.05%)
Mathlib.Analysis.Analytic.ConvergenceRadius -3.445⬝10⁹ (-3.26%)
Mathlib.Analysis.Asymptotics.Lemmas -3.534⬝10⁹ (-6.07%)
Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter -3.694⬝10⁹ (-11.37%)
Mathlib.Analysis.Distribution.SchwartzSpace -3.694⬝10⁹ (-1.66%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric -3.702⬝10⁹ (-2.22%)
Mathlib.Analysis.Calculus.VectorField -3.716⬝10⁹ (-4.60%)
Mathlib.Analysis.LocallyConvex.WeakOperatorTopology -3.732⬝10⁹ (-9.13%)
Mathlib.Analysis.Normed.Algebra.Unitization -3.792⬝10⁹ (-6.29%)
Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots -3.801⬝10⁹ (-6.12%)
Mathlib.Analysis.Analytic.IteratedFDeriv -3.809⬝10⁹ (-5.91%)
Mathlib.Analysis.InnerProductSpace.Defs -3.865⬝10⁹ (-7.75%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict -3.888⬝10⁹ (-4.80%)
Mathlib.Analysis.CStarAlgebra.Module.Defs -3.956⬝10⁹ (-6.62%)
17 files, Instructions -5.0⬝10⁹
File Instructions %
Mathlib.Analysis.Convex.EGauge -4.9⬝10⁹ (-10.31%)
Mathlib.Analysis.Fourier.FourierTransform -4.189⬝10⁹ (-5.72%)
Mathlib.Topology.ContinuousMap.CompactlySupported -4.214⬝10⁹ (-4.63%)
Mathlib.LinearAlgebra.Matrix.PosDef -4.248⬝10⁹ (-5.85%)
Mathlib.Analysis.Fourier.ZMod -4.306⬝10⁹ (-14.02%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 -4.346⬝10⁹ (-5.19%)
Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality -4.368⬝10⁹ (-13.67%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order -4.478⬝10⁹ (-2.67%)
Mathlib.Topology.Algebra.Module.Alternating.Topology -4.620⬝10⁹ (-12.21%)
Mathlib.Analysis.LocallyConvex.Bounded -4.659⬝10⁹ (-11.14%)
Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction -4.682⬝10⁹ (-10.09%)
Mathlib.RingTheory.Polynomial.Cyclotomic.Basic -4.740⬝10⁹ (-10.36%)
Mathlib.Analysis.Calculus.ContDiff.Defs -4.756⬝10⁹ (-2.37%)
Mathlib.Analysis.Normed.Unbundled.SpectralNorm -4.771⬝10⁹ (-3.18%)
Mathlib.Analysis.LocallyConvex.Basic -4.931⬝10⁹ (-14.54%)
Mathlib.Analysis.Calculus.FDeriv.Pow -4.941⬝10⁹ (-6.63%)
Mathlib.Analysis.Analytic.Inverse -4.986⬝10⁹ (-3.73%)
11 files, Instructions -6.0⬝10⁹
File Instructions %
Mathlib.Topology.Algebra.Module.Multilinear.Topology -5.232⬝10⁹ (-11.41%)
Mathlib.Analysis.Convex.Side -5.233⬝10⁹ (-6.44%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone -5.362⬝10⁹ (-5.89%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Mul -5.363⬝10⁹ (-8.34%)
Mathlib.Analysis.Convex.Gauge -5.393⬝10⁹ (-8.66%)
Mathlib.Analysis.Normed.Operator.BoundedLinearMaps -5.541⬝10⁹ (-7.46%)
Mathlib.Analysis.CStarAlgebra.Matrix -5.555⬝10⁹ (-5.62%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic -5.668⬝10⁹ (-5.22%)
Mathlib.Analysis.CStarAlgebra.ApproximateUnit -5.722⬝10⁹ (-3.13%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic -5.783⬝10⁹ (-3.12%)
Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar -5.969⬝10⁹ (-23.11%)
12 files, Instructions -7.0⬝10⁹
File Instructions %
Mathlib.Analysis.Analytic.Constructions -6.39⬝10⁹ (-3.05%)
Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno -6.74⬝10⁹ (-3.51%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic -6.83⬝10⁹ (-8.27%)
Mathlib.Topology.ContinuousMap.StoneWeierstrass -6.311⬝10⁹ (-3.77%)
Mathlib.Analysis.Analytic.ChangeOrigin -6.360⬝10⁹ (-6.60%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances -6.370⬝10⁹ (-4.06%)
Mathlib.Analysis.Convolution -6.466⬝10⁹ (-1.97%)
Mathlib.Analysis.InnerProductSpace.PiL2 -6.506⬝10⁹ (-3.73%)
Mathlib.Analysis.Calculus.ContDiff.Bounds -6.657⬝10⁹ (-4.80%)
Mathlib.Analysis.Normed.Lp.PiLp -6.952⬝10⁹ (-8.06%)
Mathlib.Analysis.Analytic.Composition -6.953⬝10⁹ (-4.78%)
Mathlib.Analysis.Calculus.Deriv.Mul -6.973⬝10⁹ (-4.08%)
5 files, Instructions -8.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.ContDiff.Operations -7.397⬝10⁹ (-3.97%)
Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic -7.511⬝10⁹ (-26.00%)
Mathlib.Analysis.LocallyConvex.WithSeminorms -7.558⬝10⁹ (-8.17%)
Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt -7.799⬝10⁹ (-9.94%)
Mathlib.Analysis.Calculus.Implicit -7.927⬝10⁹ (-6.99%)
4 files, Instructions -9.0⬝10⁹
File Instructions %
Mathlib.NumberTheory.FLT.Three -8.23⬝10⁹ (-6.99%)
Mathlib.Geometry.Manifold.Instances.Icc -8.624⬝10⁹ (-28.12%)
Mathlib.Analysis.NormedSpace.Alternating.Basic -8.627⬝10⁹ (-8.35%)
Mathlib.Analysis.CStarAlgebra.Multiplier -8.881⬝10⁹ (-6.77%)
6 files, Instructions -10.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.FormalMultilinearSeries -9.191⬝10⁹ (-11.27%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear -9.332⬝10⁹ (-5.71%)
Mathlib.Analysis.Asymptotics.TVS -9.379⬝10⁹ (-9.95%)
Mathlib.Topology.Algebra.Module.StrongTopology -9.825⬝10⁹ (-12.03%)
Mathlib.FieldTheory.Galois.Profinite -9.829⬝10⁹ (-8.73%)
Mathlib.Geometry.Manifold.ContMDiff.NormedSpace -9.937⬝10⁹ (-6.79%)
3 files, Instructions -11.0⬝10⁹
File Instructions %
Mathlib.NumberTheory.NumberField.Units.DirichletTheorem -10.333⬝10⁹ (-13.56%)
Mathlib.Algebra.Module.ZLattice.Basic -10.379⬝10⁹ (-7.55%)
Mathlib.Analysis.NormedSpace.BallAction -10.717⬝10⁹ (-11.46%)
8 files, Instructions -12.0⬝10⁹
File Instructions %
Mathlib.Topology.Algebra.Module.FiniteDimension -11.48⬝10⁹ (-10.54%)
Mathlib.Geometry.Manifold.MFDeriv.NormedSpace -11.72⬝10⁹ (-6.24%)
Mathlib.MeasureTheory.Function.Holder -11.77⬝10⁹ (-13.04%)
Mathlib.MeasureTheory.Function.LpSpace.Basic -11.208⬝10⁹ (-10.46%)
Mathlib.Analysis.Calculus.ContDiff.Basic -11.307⬝10⁹ (-4.04%)
Mathlib.Topology.VectorBundle.Hom -11.484⬝10⁹ (-8.83%)
Mathlib.Analysis.Normed.Operator.LinearIsometry -11.668⬝10⁹ (-7.11%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital -11.702⬝10⁹ (-5.77%)
4 files, Instructions -13.0⬝10⁹
File Instructions %
Mathlib.Topology.VectorBundle.Riemannian -12.141⬝10⁹ (-6.94%)
Mathlib.NumberTheory.NumberField.Ideal.Basic -12.242⬝10⁹ (-53.18%)
Mathlib.Analysis.Fourier.FourierTransformDeriv -12.494⬝10⁹ (-3.80%)
Mathlib.Analysis.Calculus.FDeriv.Analytic -12.908⬝10⁹ (-5.57%)
File Instructions %
Mathlib.LinearAlgebra.Matrix.SchurComplement -13.412⬝10⁹ (-16.46%)
2 files, Instructions -15.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.FDeriv.Mul -14.496⬝10⁹ (-3.54%)
Mathlib.Geometry.Manifold.VectorBundle.Riemannian -14.663⬝10⁹ (-10.62%)
2 files, Instructions -16.0⬝10⁹
File Instructions %
Mathlib.Analysis.NormedSpace.Multilinear.Curry -15.290⬝10⁹ (-6.91%)
Mathlib.Geometry.Manifold.VectorBundle.Hom -15.748⬝10⁹ (-9.50%)
2 files, Instructions -18.0⬝10⁹
File Instructions %
Mathlib.Analysis.CStarAlgebra.CStarMatrix -17.134⬝10⁹ (-13.08%)
Mathlib.Analysis.Seminorm -17.311⬝10⁹ (-11.78%)
3 files, Instructions -19.0⬝10⁹
File Instructions %
Mathlib.Analysis.NormedSpace.Multilinear.Basic -18.656⬝10⁹ (-7.73%)
Mathlib.Geometry.Manifold.Riemannian.Basic -18.760⬝10⁹ (-19.81%)
Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries -18.844⬝10⁹ (-7.40%)
2 files, Instructions -20.0⬝10⁹
File Instructions %
Mathlib.MeasureTheory.Group.FundamentalDomain -19.805⬝10⁹ (-16.74%)
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp -19.862⬝10⁹ (-17.72%)
File Instructions %
Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm -21.357⬝10⁹ (-14.36%)
Mathlib.Analysis.InnerProductSpace.Adjoint -22.860⬝10⁹ (-8.56%)
Mathlib.Analysis.Normed.Lp.lpSpace -40.764⬝10⁹ (-19.59%)
CI run Lakeprof report

grunweg added a commit to grunweg/mathlib4 that referenced this pull request Aug 23, 2025
@grunweg
chore(IntervalIntegrable/Basic): generalise typeclasses slightly
0220de0 
Discovered in leanprover-community#28803.
@grunweg grunweg mentioned this pull request Aug 23, 2025
Closed
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 24, 2025
grunweg
grunweg reviewed Aug 24, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 24, 2025

🚀 Pull request has been placed on the maintainer queue by grunweg.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 24, 2025
@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Aug 24, 2025

Could you summarize the main changes to the typeclasses in the PR commit? e.g.:

  • Change ESeminormedAddMonoid, 'ENormedAddMonoid`, ... so that ...
  • Deprecate ESeminormedAddCommMonoid, ... in favor of ...

@bryangingechen bryangingechen added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 24, 2025
@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Aug 24, 2025

This looks fine to me and I'll happily merge as is, but is there also a plan for removing these classes completely, sticking to ENorm, and replacing the classes here with Prop-valued classes saying "the ENorm is compatible with the topology (i.e. continuous)" etc?

@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Aug 24, 2025

Let's get this in once you fix up the PR description / commit message. Thanks!
bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 24, 2025

✌️ astrainfinita can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-author A reviewer has asked the author a question or requested changes. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 24, 2025
pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025
@grunweg @pechersky
chore(IntervalIntegrable/Basic): generalise typeclasses slightly (lea…
3656148 
…nprover-community#28813)

Discovered in leanprover-community#28803. Transitively part of the Carleson project, as this is about the enorm classes.

While this PR is basically performance-neutral; transplanting this to leanprover-community#28803 speeds up the file by 20 * 10⁹ instructions.
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Aug 25, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Aug 25, 2025
@astrainfinita
refactor: unbundle algebra from ENormed* (#28803)
3c96d4d 
Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`.
This PR continues the work from #23961.

- Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data.
- Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass.

|Old|New|
|
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 25, 2025

Build failed:

@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Aug 25, 2025

I am not convinced that we should merge this now. I agree that there is a performance improvement, but if we want to go this way we should probably do it for the other classes like NormedAddCommGroup and friends. I expect this will give much bigger performance improvement even, but at the expense of a reduced readability of typeclasses declarations. Until we have a way to shortcut variables declarations (something like [[NormedAddCommGroup E]] which would automatically register the lower typeclasses), I am not convinced that the performance gain outweighs the readability loss. But in any case this is a major design decision with consequences all over mathlib, so this should definitely be discussed thoroughly on Zulip before any PR in this direction is merged and we have a clear plan to go forward.

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Aug 25, 2025

There is a PR (depending on this, which would need a rebase) which does the same change for NormedAddCommGroup.
And didn't we merge quite a few such PRs a few months ago, with some discussion?

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Aug 25, 2025

I'm not too psyched about the readability loss either, but having worked in differential geometry long enough, I guess I got used to this. This is a problem which needs a solution, but I'm not convinced waiting it out is it.

@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Aug 25, 2025

We merged PRs unbundling order and algebra. This gave a crazy performance improvement, but still there was a long discussion and several experiments to see the best way to do it. I'm saying we should do the same here. (And to be fair I'm personally completely in favor of merging, but I do think this should be discussed very seriously beforehand)

@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Aug 25, 2025

The design of ENormed typeclasses is already different from Normed typeclasses, and the impact is much smaller than the changes to Normed typeclasses. I think there will be less controversy about it?

@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Aug 25, 2025

The design of ENormed typeclasses is already different from Normed typeclasses, and the impact is much smaller than the changes to Normed typeclasses. I think there will be less controversy about it?

I believe the point is this: even if in this case there is not too much fallout from the change, it would be undesirable to have some typeclasses unbundled and some bundled without some underlying ground rules, otherwise we end up baking in a bunch of design decisions into the library that few people understand and will be difficult to maintain. As Sébastien said, there is a way forward on this, but we need to decide on a bigger plan first.

For the time being, I've started a Zulip thread.

bors d-

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 25, 2025

🚫 All delegations have been removed from this PR. To re-add a delegation, reply with bors d+ (to delegate the PR author) or bors d=list,of,github,usernames to delegate multiple users.

@ghost ghost removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Aug 25, 2025
@bryangingechen bryangingechen added the awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there label Aug 25, 2025
FormulaRabbit81 pushed a commit to YaelDillies/mathlib4 that referenced this pull request Aug 30, 2025
@grunweg @FormulaRabbit81
chore(IntervalIntegrable/Basic): generalise typeclasses slightly (lea…
16f3923 
…nprover-community#28813)

Discovered in leanprover-community#28803. Transitively part of the Carleson project, as this is about the enorm classes.

While this PR is basically performance-neutral; transplanting this to leanprover-community#28803 speeds up the file by 20 * 10⁹ instructions.
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 2, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Sep 2, 2025

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

@grunweg grunweg mentioned this pull request Apr 14, 2026
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg grunweg left review comments

Assignees

@grunweg grunweg

Labels

awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) slow-typeclass-synthesis t-algebra Algebra (groups, rings, fields, etc) t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

8 participants

@astrainfinita @grunweg @leanprover-bot @mathlib4-dependent-issues-bot @bryangingechen @kbuzzard @sgouezel @mathlib4-merge-conflict-bot
⚡