chore: change prios of some normed ring to ring instances #24011

kbuzzard · 2025-04-13T21:43:08Z

An attempt to make our priority 100 instance choices more consistent in Analysis/Normed/Ring/Basic.lean.

See Zulip

Co-authored-by: Eric Wieser <[email protected]>

Let's see whether this alone has an affect on the benchmark

…smul

kbuzzard · 2025-04-13T21:43:20Z

!bench

github-actions · 2025-04-13T21:44:10Z

PR summary 95e3c54d89

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ NormMulClass.toNormSMulClass
+ NormMulClass.toNormSMulClass_op
+ NormSMulClass
+ NormSMulClass.toIsBoundedSMul
+ NormedDivisionRing.toNormSMulClass
+ NormedField.to_isNormSMulClass
+ Pi.toNormSMulClass
+ Prod.toNormSMulClass
+ instance (priority := 100) NormedSpace.toNormSMulClass [NormedSpace 𝕜 E] : NormSMulClass 𝕜 E
- NormedField.to_isBoundedSMul
- instance (priority := 100) NormedSpace.isBoundedSMul [NormedSpace 𝕜 E] : IsBoundedSMul 𝕜 E

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

leanprover-bot · 2025-04-13T22:12:54Z

Here are the benchmark results for commit d421df7.
There were no significant changes against commit 9f26568.

github-actions · 2025-04-13T22:13:25Z

File	Instructions	%
`build`	+23.822⬝10⁹	(+0.01%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic`	+3.823⬝10⁹	(+2.22%)

2 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Sums.Products`	+2.575⬝10⁹	(+0.95%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric`	+2.97⬝10⁹	(+1.17%)

4 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.RCLike.Basic`	+1.954⬝10⁹	(+1.64%)
`Mathlib.Analysis.Calculus.FDeriv.Mul`	+1.488⬝10⁹	(+0.35%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order`	+1.148⬝10⁹	(+0.66%)
`Mathlib.Analysis.Normed.Algebra.Spectrum`	+1.139⬝10⁹	(+0.91%)

2 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.NumberTheory.Cyclotomic.Rat`	-1.79⬝10⁹	(-0.97%)
`Mathlib.Topology.ContinuousMap.StoneWeierstrass`	-1.520⬝10⁹	(-0.71%)

CI run

kbuzzard · 2025-04-13T22:17:30Z

Mathlib.CategoryTheory.Sums.Products went up +2.575⬝10⁹ but it doesn't even import the file I changed!

kbuzzard · 2025-04-13T22:18:48Z

!bench

leanprover-bot · 2025-04-13T22:46:53Z

Here are the benchmark results for commit 615938d.
There were no significant changes against commit 9f26568.

github-actions · 2025-04-13T22:47:32Z

File	Instructions	%
`build`	+39.239⬝10⁹	(+0.02%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic`	+3.829⬝10⁹	(+2.22%)

2 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Sums.Products`	+2.903⬝10⁹	(+1.07%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric`	+2.76⬝10⁹	(+1.16%)

4 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.RCLike.Basic`	+1.951⬝10⁹	(+1.63%)
`Mathlib.Analysis.Calculus.FDeriv.Mul`	+1.501⬝10⁹	(+0.35%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order`	+1.209⬝10⁹	(+0.70%)
`Mathlib.Analysis.Normed.Algebra.Spectrum`	+1.126⬝10⁹	(+0.90%)

2 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.NumberTheory.Cyclotomic.Rat`	-1.87⬝10⁹	(-0.98%)
`Mathlib.Topology.ContinuousMap.StoneWeierstrass`	-1.503⬝10⁹	(-0.70%)

CI run

…buzzard-harmonise-normed-ring-prios

kbuzzard · 2025-04-13T22:52:42Z

Now merging David's ideas (via Eric's #24003) to see if there's any difference.

kbuzzard · 2025-04-13T22:52:47Z

!bench

leanprover-bot · 2025-04-13T23:20:39Z

Here are the benchmark results for commit 95e3c54.
There were significant changes against commit 28daac2:

  Benchmark                                             Metric         Change
  ===========================================================================
+ build                                                 parsing         -5.6%
- ~Mathlib.Analysis.Analytic.Basic                      instructions    17.1%
- ~Mathlib.Analysis.Analytic.CPolynomialDef             instructions    18.9%
- ~Mathlib.Analysis.Analytic.ChangeOrigin               instructions     9.9%
- ~Mathlib.Analysis.Analytic.Constructions              instructions    13.1%
- ~Mathlib.Analysis.Analytic.Inverse                    instructions     9.2%
- ~Mathlib.Analysis.Calculus.ContDiff.Basic             instructions    11.4%
- ~Mathlib.Analysis.Calculus.ContDiff.Defs              instructions    15.0%
- ~Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries     instructions    10.6%
- ~Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno        instructions     9.1%
- ~Mathlib.Analysis.Calculus.ContDiff.Operations        instructions    15.4%
- ~Mathlib.Analysis.Calculus.Deriv.Basic                instructions    12.9%
- ~Mathlib.Analysis.Calculus.Deriv.Mul                  instructions    10.2%
- ~Mathlib.Analysis.Calculus.FDeriv.Analytic            instructions     7.0%
- ~Mathlib.Analysis.Calculus.FDeriv.Mul                 instructions     3.4%
- ~Mathlib.Analysis.Convolution                         instructions     5.8%
- ~Mathlib.Analysis.NormedSpace.Multilinear.Basic       instructions     4.1%
- ~Mathlib.Analysis.NormedSpace.Multilinear.Curry       instructions     5.2%
- ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear   instructions     6.8%
- ~Mathlib.CategoryTheory.Sums.Products                 instructions    73.1%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Constructions   instructions   -38.7%

github-actions · 2025-04-13T23:21:11Z

File	Instructions	%
`build`	+1311.139⬝10⁹	(+0.83%)
`lint`	+47.663⬝10⁹	(+0.62%)
`Mathlib.CategoryTheory.Sums.Products`	+113.832⬝10⁹	(+73.09%)
`Mathlib.Analysis.Analytic.Basic`	+46.661⬝10⁹	(+17.13%)
`Mathlib.Analysis.Calculus.ContDiff.Basic`	+33.645⬝10⁹	(+11.41%)

2 files, Instructions +31.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries`	+31.264⬝10⁹	(+10.64%)
`Mathlib.Analysis.Calculus.ContDiff.Defs`	+31.105⬝10⁹	(+14.95%)

File	Instructions	%
`Mathlib.Analysis.Calculus.ContDiff.Operations`	+29.481⬝10⁹	(+15.43%)
`Mathlib.Analysis.Analytic.Constructions`	+24.517⬝10⁹	(+13.07%)

2 files, Instructions +21.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Convolution`	+21.599⬝10⁹	(+5.80%)
`Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno`	+21.252⬝10⁹	(+9.11%)

2 files, Instructions +19.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Calculus.FDeriv.Analytic`	+19.815⬝10⁹	(+6.99%)
`Mathlib.Analysis.Analytic.CPolynomialDef`	+19.801⬝10⁹	(+18.85%)

File	Instructions	%
`Mathlib.Analysis.Calculus.Deriv.Mul`	+17.109⬝10⁹	(+10.17%)
`Mathlib.Analysis.Calculus.FDeriv.Mul`	+14.559⬝10⁹	(+3.43%)
`Mathlib.Analysis.Analytic.Inverse`	+13.552⬝10⁹	(+9.18%)

3 files, Instructions +11.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear`	+11.816⬝10⁹	(+6.76%)
`Mathlib.Analysis.Calculus.Deriv.Basic`	+11.683⬝10⁹	(+12.91%)
`Mathlib.Analysis.NormedSpace.Multilinear.Curry`	+11.386⬝10⁹	(+5.17%)

2 files, Instructions +10.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.NormedSpace.Multilinear.Basic`	+10.979⬝10⁹	(+4.13%)
`Mathlib.Analysis.Analytic.ChangeOrigin`	+10.754⬝10⁹	(+9.94%)

3 files, Instructions +9.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Analytic.Composition`	+9.644⬝10⁹	(+6.25%)
`Mathlib.Analysis.InnerProductSpace.Adjoint`	+9.255⬝10⁹	(+3.73%)
`Mathlib.Analysis.Analytic.CPolynomial`	+9.23⬝10⁹	(+17.18%)

File	Instructions	%
`Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula`	+8.949⬝10⁹	(+3.08%)
`Mathlib.Analysis.Calculus.Deriv.Comp`	+7.178⬝10⁹	(+8.64%)
`Mathlib.Geometry.Manifold.MFDeriv.NormedSpace`	+6.544⬝10⁹	(+2.95%)

4 files, Instructions +5.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Analytic.IteratedFDeriv`	+5.857⬝10⁹	(+8.17%)
`Mathlib.Analysis.Calculus.Deriv.Prod`	+5.793⬝10⁹	(+15.19%)
`Mathlib.Geometry.Manifold.ContMDiff.NormedSpace`	+5.609⬝10⁹	(+3.26%)
`Mathlib.Analysis.Calculus.Implicit`	+5.5⬝10⁹	(+3.88%)

6 files, Instructions +4.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Calculus.Deriv.Add`	+4.795⬝10⁹	(+11.19%)
`Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm`	+4.744⬝10⁹	(+2.61%)
`Mathlib.Analysis.Calculus.FormalMultilinearSeries`	+4.592⬝10⁹	(+5.79%)
`Mathlib.Analysis.Distribution.SchwartzSpace`	+4.481⬝10⁹	(+1.95%)
`Mathlib.MeasureTheory.Function.Holder`	+4.174⬝10⁹	(+4.30%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic`	+4.107⬝10⁹	(+2.39%)

10 files, Instructions +3.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.RCLike.Basic`	+3.913⬝10⁹	(+3.36%)
`Mathlib.Analysis.Calculus.ContDiff.Bounds`	+3.844⬝10⁹	(+2.45%)
`Mathlib.Analysis.Calculus.FDeriv.Symmetric`	+3.713⬝10⁹	(+3.07%)
`Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic`	+3.687⬝10⁹	(+6.55%)
`Mathlib.Analysis.CStarAlgebra.Matrix`	+3.670⬝10⁹	(+2.77%)
`Mathlib.Analysis.CStarAlgebra.Multiplier`	+3.551⬝10⁹	(+2.42%)
`Mathlib.Analysis.Analytic.IsolatedZeros`	+3.540⬝10⁹	(+4.63%)
`Mathlib.Analysis.Normed.Operator.BoundedLinearMaps`	+3.360⬝10⁹	(+4.50%)
`Mathlib.Analysis.NormedSpace.OperatorNorm.Prod`	+3.270⬝10⁹	(+4.55%)
`Mathlib.Analysis.NormedSpace.OperatorNorm.Mul`	+3.123⬝10⁹	(+4.95%)

15 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Mathlib.RingTheory.IntegralClosure.IntegralRestrict`	+2.921⬝10⁹	(+1.15%)
`Mathlib.Analysis.InnerProductSpace.l2Space`	+2.905⬝10⁹	(+3.27%)
`Mathlib.MeasureTheory.Integral.SetIntegral`	+2.884⬝10⁹	(+2.26%)
`Mathlib.NumberTheory.Divisors`	+2.775⬝10⁹	(+3.64%)
`Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions`	+2.760⬝10⁹	(+6.74%)
`Mathlib.Analysis.Analytic.Linear`	+2.756⬝10⁹	(+5.40%)
`Mathlib.RingTheory.Ideal.Norm.RelNorm`	+2.655⬝10⁹	(+1.97%)
`Mathlib.Analysis.Normed.Module.FiniteDimension`	+2.467⬝10⁹	(+2.44%)
`Mathlib.Analysis.Calculus.SmoothSeries`	+2.393⬝10⁹	(+4.87%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric`	+2.183⬝10⁹	(+1.22%)
`Mathlib.LinearAlgebra.Matrix.PosDef`	+2.170⬝10⁹	(+3.34%)
`Mathlib.Analysis.Calculus.FDeriv.Equiv`	+2.133⬝10⁹	(+2.60%)
`Mathlib.Algebra.Homology.HomotopyCategory.Triangulated`	+2.123⬝10⁹	(+1.65%)
`Mathlib.Analysis.Normed.MulAction`	+2.35⬝10⁹	(+12.79%)
`Mathlib.Analysis.SpecialFunctions.Exponential`	+2.13⬝10⁹	(+3.26%)

36 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Calculus.LineDeriv.Basic`	+1.963⬝10⁹	(+3.51%)
`Mathlib.Analysis.Calculus.VectorField`	+1.861⬝10⁹	(+2.11%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order`	+1.781⬝10⁹	(+1.03%)
`Mathlib.MeasureTheory.Integral.IntegralEqImproper`	+1.742⬝10⁹	(+1.99%)
`Mathlib.Algebra.Module.LocalizedModule.Basic`	+1.738⬝10⁹	(+1.13%)
`Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula`	+1.733⬝10⁹	(+1.10%)
`Mathlib.Analysis.Normed.Lp.lpSpace`	+1.562⬝10⁹	(+0.72%)
`Mathlib.Topology.VectorBundle.Hom`	+1.550⬝10⁹	(+1.96%)
`Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2`	+1.510⬝10⁹	(+1.46%)
`Mathlib.Analysis.Normed.Algebra.Spectrum`	+1.469⬝10⁹	(+1.18%)
`Mathlib.Analysis.InnerProductSpace.Projection`	+1.452⬝10⁹	(+0.75%)
`Mathlib.Analysis.Calculus.ParametricIntegral`	+1.441⬝10⁹	(+2.50%)
`Mathlib.Analysis.Calculus.MeanValue`	+1.436⬝10⁹	(+1.48%)
`Mathlib.Analysis.CStarAlgebra.Unitization`	+1.427⬝10⁹	(+2.54%)
`Mathlib.Analysis.Calculus.IteratedDeriv.Defs`	+1.359⬝10⁹	(+2.94%)
`Mathlib.Analysis.Normed.Algebra.Unitization`	+1.358⬝10⁹	(+2.02%)
`Mathlib.Analysis.Calculus.Deriv.Slope`	+1.337⬝10⁹	(+6.21%)
`Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus`	+1.306⬝10⁹	(+1.95%)
`Mathlib.Analysis.Analytic.Uniqueness`	+1.284⬝10⁹	(+3.81%)
`Mathlib.MeasureTheory.Function.LpSpace.Basic`	+1.261⬝10⁹	(+1.19%)
`Mathlib.Analysis.Calculus.FDeriv.Bilinear`	+1.260⬝10⁹	(+3.84%)
`Mathlib.Analysis.InnerProductSpace.Calculus`	+1.228⬝10⁹	(+1.69%)
`Mathlib.Analysis.Analytic.Within`	+1.223⬝10⁹	(+7.92%)
`Mathlib.MeasureTheory.VectorMeasure.WithDensity`	+1.215⬝10⁹	(+6.98%)
`Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable`	+1.174⬝10⁹	(+2.40%)
`Mathlib.Combinatorics.SimpleGraph.Walk`	+1.151⬝10⁹	(+3.04%)
`Mathlib.Data.Nat.Init`	+1.150⬝10⁹	(+3.34%)
`Mathlib.Analysis.NormedSpace.ConformalLinearMap`	+1.139⬝10⁹	(+7.87%)
`Mathlib.Analysis.InnerProductSpace.PiL2`	+1.94⬝10⁹	(+0.50%)
`Mathlib.Analysis.InnerProductSpace.StarOrder`	+1.42⬝10⁹	(+3.05%)
`Mathlib.Analysis.Calculus.ParametricIntervalIntegral`	+1.26⬝10⁹	(+5.87%)
`Mathlib.Data.List.Sort`	+1.25⬝10⁹	(+5.96%)
`Mathlib.Topology.ContinuousMap.Bounded.Normed`	+1.25⬝10⁹	(+1.58%)
`Mathlib.Analysis.Calculus.ContDiff.RCLike`	+1.21⬝10⁹	(+5.02%)
`Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts`	+1.17⬝10⁹	(+3.50%)
`Mathlib.Analysis.Asymptotics.Defs`	+1.3⬝10⁹	(+1.35%)

4 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Normed.Module.Dual`	-1.67⬝10⁹	(-1.22%)
`Mathlib.RingTheory.Kaehler.CotangentComplex`	-1.172⬝10⁹	(-0.43%)
`Mathlib.Analysis.Asymptotics.Lemmas`	-1.181⬝10⁹	(-2.02%)
`Mathlib.Topology.ContinuousMap.StoneWeierstrass`	-1.447⬝10⁹	(-0.67%)

File	Instructions	%
`Mathlib.Analysis.InnerProductSpace.NormPow`	-2.42⬝10⁹	(-5.70%)
`Mathlib.Analysis.Fourier.FourierTransformDeriv`	-3.400⬝10⁹	(-0.93%)
`Mathlib.RingTheory.Etale.Kaehler`	-7.297⬝10⁹	(-2.38%)
`Mathlib.Topology.Algebra.InfiniteSum.Constructions`	-32.557⬝10⁹	(-38.65%)
CI run

loefflerd and others added 16 commits April 1, 2025 22:12

Mahler stuff

bdae772

Merge remote-tracking branch 'origin/master' into DL_norm_smul

e970a73

add prod and pi, use .of_norm_le

ebff4c5

unused argument

b49bcdb

Apply suggestions from code review

6b4a2dd

Co-authored-by: Eric Wieser <[email protected]>

add opposite, downgrade instance to lemma

05f4c7a

add instance from NormedSpace

0bc8fa3

use NormSMulClass instead of IsBoundedSMul

dbb8949

fix build

64e80b0

Apply suggestions from code review

6d96501

Co-authored-by: Eric Wieser <[email protected]>

Remove a redundant instance

42cb3bc

Let's see whether this alone has an affect on the benchmark

fix

d694215

update yamls for deleted instance

32bce8c

oops

1fa93ca

Merge commit '28daac21cdf24d42249214b8e9abe0a5ffcc6bda' into DL_norm_…

0ac28ed

…smul

chore: change prios of some normed ring to ring instances

d421df7

kbuzzard added the WIP Work in progress label Apr 13, 2025

github-actions bot added the t-analysis Analysis (normed *, calculus) label Apr 13, 2025

add newline

615938d

Merge remote-tracking branch 'origin/DL_norm_smul-alternative' into k…

95e3c54

…buzzard-harmonise-normed-ring-prios

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: change prios of some normed ring to ring instances #24011

chore: change prios of some normed ring to ring instances #24011

kbuzzard commented Apr 13, 2025

kbuzzard commented Apr 13, 2025

github-actions bot commented Apr 13, 2025 •

edited

Loading

Declarations diff

leanprover-bot commented Apr 13, 2025

github-actions bot commented Apr 13, 2025

kbuzzard commented Apr 13, 2025

kbuzzard commented Apr 13, 2025

leanprover-bot commented Apr 13, 2025

github-actions bot commented Apr 13, 2025

kbuzzard commented Apr 13, 2025

kbuzzard commented Apr 13, 2025

leanprover-bot commented Apr 13, 2025

github-actions bot commented Apr 13, 2025

chore: change prios of some normed ring to ring instances #24011

Are you sure you want to change the base?

chore: change prios of some normed ring to ring instances #24011

Conversation

kbuzzard commented Apr 13, 2025

kbuzzard commented Apr 13, 2025

github-actions bot commented Apr 13, 2025 • edited Loading

PR summary 95e3c54d89

Import changes for modified files

Declarations diff

leanprover-bot commented Apr 13, 2025

github-actions bot commented Apr 13, 2025

kbuzzard commented Apr 13, 2025

kbuzzard commented Apr 13, 2025

leanprover-bot commented Apr 13, 2025

github-actions bot commented Apr 13, 2025

kbuzzard commented Apr 13, 2025

kbuzzard commented Apr 13, 2025

leanprover-bot commented Apr 13, 2025

github-actions bot commented Apr 13, 2025

github-actions bot commented Apr 13, 2025 •

edited

Loading