refactor: mixin class for `norm_smul` with strict equality #24003

eric-wieser · 2025-04-13T14:47:22Z

Define a typeclass for normed modules where the norm is exactly multiplicative (not just sub-multiplicative).

This is a subset of #23787, leaving out the change to NormedSpace.

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

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

…smul

github-actions · 2025-04-13T14:48:23Z

PR summary 0ac28ed9f4

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

eric-wieser · 2025-04-13T14:49:05Z

!bench

leanprover-bot · 2025-04-13T15:17:49Z

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

  Benchmark                                             Metric         Change
  ===========================================================================
- ~Mathlib.Analysis.Analytic.Basic                      instructions    17.1%
- ~Mathlib.Analysis.Analytic.CPolynomialDef             instructions    18.8%
- ~Mathlib.Analysis.Analytic.ChangeOrigin               instructions    10.2%
- ~Mathlib.Analysis.Analytic.Constructions              instructions    13.0%
- ~Mathlib.Analysis.Analytic.Inverse                    instructions     8.8%
- ~Mathlib.Analysis.Calculus.ContDiff.Basic             instructions    11.4%
- ~Mathlib.Analysis.Calculus.ContDiff.Defs              instructions    14.9%
- ~Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries     instructions    10.6%
- ~Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno        instructions     9.0%
- ~Mathlib.Analysis.Calculus.ContDiff.Operations        instructions    15.3%
- ~Mathlib.Analysis.Calculus.Deriv.Basic                instructions    12.7%
- ~Mathlib.Analysis.Calculus.Deriv.Mul                  instructions     9.8%
- ~Mathlib.Analysis.Calculus.FDeriv.Analytic            instructions     7.0%
- ~Mathlib.Analysis.Calculus.FDeriv.Mul                 instructions     3.0%
- ~Mathlib.Analysis.Convolution                         instructions     5.8%
- ~Mathlib.Analysis.NormedSpace.Multilinear.Basic       instructions     3.9%
- ~Mathlib.Analysis.NormedSpace.Multilinear.Curry       instructions     5.2%
- ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear   instructions     6.7%

github-actions · 2025-04-13T15:18:20Z

File	Instructions	%
`build`	+512.30⬝10⁹	(+0.32%)
`lint`	+36.240⬝10⁹	(+0.47%)
`Mathlib.Analysis.Analytic.Basic`	+46.497⬝10⁹	(+17.07%)
`Mathlib.Analysis.Calculus.ContDiff.Basic`	+33.499⬝10⁹	(+11.36%)

2 files, Instructions +30.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries`	+30.987⬝10⁹	(+10.55%)
`Mathlib.Analysis.Calculus.ContDiff.Defs`	+30.932⬝10⁹	(+14.87%)

File	Instructions	%
`Mathlib.Analysis.Calculus.ContDiff.Operations`	+29.247⬝10⁹	(+15.31%)
`Mathlib.Analysis.Analytic.Constructions`	+24.303⬝10⁹	(+12.95%)

2 files, Instructions +21.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Convolution`	+21.405⬝10⁹	(+5.75%)
`Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno`	+21.77⬝10⁹	(+9.03%)

2 files, Instructions +19.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Calculus.FDeriv.Analytic`	+19.835⬝10⁹	(+7.00%)
`Mathlib.Analysis.Analytic.CPolynomialDef`	+19.799⬝10⁹	(+18.84%)

File	Instructions	%
`Mathlib.Analysis.Calculus.Deriv.Mul`	+16.532⬝10⁹	(+9.82%)
`Mathlib.Analysis.Analytic.Inverse`	+13.47⬝10⁹	(+8.84%)
`Mathlib.Analysis.Calculus.FDeriv.Mul`	+12.834⬝10⁹	(+3.02%)

3 files, Instructions +11.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear`	+11.717⬝10⁹	(+6.71%)
`Mathlib.Analysis.Calculus.Deriv.Basic`	+11.507⬝10⁹	(+12.72%)
`Mathlib.Analysis.NormedSpace.Multilinear.Curry`	+11.499⬝10⁹	(+5.22%)

2 files, Instructions +10.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Analytic.ChangeOrigin`	+10.983⬝10⁹	(+10.16%)
`Mathlib.Analysis.NormedSpace.Multilinear.Basic`	+10.392⬝10⁹	(+3.91%)

File	Instructions	%
`Mathlib.Analysis.Analytic.Composition`	+9.503⬝10⁹	(+6.16%)

2 files, Instructions +8.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Analytic.CPolynomial`	+8.922⬝10⁹	(+16.98%)
`Mathlib.Analysis.InnerProductSpace.Adjoint`	+8.781⬝10⁹	(+3.54%)

File	Instructions	%
`Mathlib.Analysis.Calculus.Deriv.Comp`	+7.255⬝10⁹	(+8.73%)
`Mathlib.Geometry.Manifold.MFDeriv.NormedSpace`	+6.335⬝10⁹	(+2.86%)

3 files, Instructions +5.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Analytic.IteratedFDeriv`	+5.754⬝10⁹	(+8.03%)
`Mathlib.Analysis.Calculus.Deriv.Prod`	+5.466⬝10⁹	(+14.33%)
`Mathlib.Geometry.Manifold.ContMDiff.NormedSpace`	+5.427⬝10⁹	(+3.16%)

4 files, Instructions +4.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Calculus.Deriv.Add`	+4.670⬝10⁹	(+10.89%)
`Mathlib.Analysis.Calculus.FormalMultilinearSeries`	+4.663⬝10⁹	(+5.88%)
`Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm`	+4.496⬝10⁹	(+2.47%)
`Mathlib.Analysis.Calculus.Implicit`	+4.212⬝10⁹	(+3.26%)

8 files, Instructions +3.0⬝10⁹

File	Instructions	%
`Mathlib.MeasureTheory.Function.Holder`	+3.932⬝10⁹	(+4.05%)
`Mathlib.Analysis.Analytic.IsolatedZeros`	+3.895⬝10⁹	(+5.09%)
`Mathlib.Analysis.Distribution.SchwartzSpace`	+3.761⬝10⁹	(+1.64%)
`Mathlib.Analysis.Calculus.ContDiff.Bounds`	+3.529⬝10⁹	(+2.25%)
`Mathlib.Analysis.CStarAlgebra.Matrix`	+3.202⬝10⁹	(+2.41%)
`Mathlib.Analysis.Calculus.FDeriv.Symmetric`	+3.162⬝10⁹	(+2.61%)
`Mathlib.Analysis.Normed.Operator.BoundedLinearMaps`	+3.155⬝10⁹	(+4.23%)
`Mathlib.Analysis.CStarAlgebra.Multiplier`	+3.88⬝10⁹	(+2.10%)

7 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.NormedSpace.OperatorNorm.Prod`	+2.877⬝10⁹	(+4.01%)
`Mathlib.Analysis.Analytic.Linear`	+2.727⬝10⁹	(+5.34%)
`Mathlib.Analysis.NormedSpace.OperatorNorm.Mul`	+2.634⬝10⁹	(+4.17%)
`Mathlib.Analysis.InnerProductSpace.l2Space`	+2.527⬝10⁹	(+2.84%)
`Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions`	+2.505⬝10⁹	(+6.12%)
`Mathlib.Analysis.Normed.Module.FiniteDimension`	+2.393⬝10⁹	(+2.36%)
`Mathlib.Analysis.Calculus.SmoothSeries`	+2.295⬝10⁹	(+4.67%)

22 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Calculus.FDeriv.Equiv`	+1.993⬝10⁹	(+2.43%)
`Mathlib.MeasureTheory.Integral.SetIntegral`	+1.882⬝10⁹	(+1.47%)
`Mathlib.Analysis.Normed.MulAction`	+1.865⬝10⁹	(+11.72%)
`Mathlib.Analysis.Calculus.LineDeriv.Basic`	+1.830⬝10⁹	(+3.27%)
`Mathlib.Analysis.SpecialFunctions.Exponential`	+1.671⬝10⁹	(+2.71%)
`Mathlib.Analysis.Calculus.VectorField`	+1.648⬝10⁹	(+1.87%)
`Mathlib.MeasureTheory.Integral.IntegralEqImproper`	+1.482⬝10⁹	(+1.69%)
`Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2`	+1.395⬝10⁹	(+1.35%)
`Mathlib.Topology.VectorBundle.Hom`	+1.365⬝10⁹	(+1.72%)
`Mathlib.Analysis.InnerProductSpace.Projection`	+1.361⬝10⁹	(+0.71%)
`Mathlib.Analysis.Calculus.FDeriv.Bilinear`	+1.333⬝10⁹	(+4.06%)
`Mathlib.Analysis.Calculus.ParametricIntegral`	+1.324⬝10⁹	(+2.30%)
`Mathlib.Analysis.CStarAlgebra.Unitization`	+1.292⬝10⁹	(+2.30%)
`Mathlib.Analysis.Calculus.MeanValue`	+1.261⬝10⁹	(+1.30%)
`Mathlib.Analysis.Analytic.Uniqueness`	+1.238⬝10⁹	(+3.67%)
`Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus`	+1.189⬝10⁹	(+1.78%)
`Mathlib.Analysis.Normed.Algebra.Unitization`	+1.147⬝10⁹	(+1.70%)
`Mathlib.Analysis.Analytic.Within`	+1.135⬝10⁹	(+7.35%)
`Mathlib.Analysis.Calculus.Deriv.Slope`	+1.92⬝10⁹	(+5.07%)
`Mathlib.MeasureTheory.VectorMeasure.WithDensity`	+1.49⬝10⁹	(+6.02%)
`Mathlib.Analysis.InnerProductSpace.Calculus`	+1.37⬝10⁹	(+1.43%)
`Mathlib.Analysis.NormedSpace.ConformalLinearMap`	+1.9⬝10⁹	(+6.98%)

7 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension`	-1.3⬝10⁹	(-1.70%)
`Mathlib.Analysis.CStarAlgebra.Module.Defs`	-1.13⬝10⁹	(-1.62%)
`Mathlib.MeasureTheory.Integral.CircleIntegral`	-1.94⬝10⁹	(-1.62%)
`Mathlib.Analysis.Normed.Affine.ContinuousAffineMap`	-1.100⬝10⁹	(-1.99%)
`Mathlib.Analysis.Normed.Affine.AddTorsor`	-1.108⬝10⁹	(-3.91%)
`Mathlib.Analysis.InnerProductSpace.Basic`	-1.264⬝10⁹	(-1.31%)
`Mathlib.Analysis.Asymptotics.Lemmas`	-1.400⬝10⁹	(-2.39%)

File	Instructions	%
`Mathlib.Analysis.InnerProductSpace.NormPow`	-2.122⬝10⁹	(-5.93%)
`Mathlib.Analysis.Fourier.FourierTransformDeriv`	-3.901⬝10⁹	(-1.07%)
CI run

kbuzzard · 2025-04-13T20:17:22Z

I can see that certain things are slower in traces on this branch. For example

import Mathlib

variable (𝕜 F : Type*) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F]

set_option trace.profiler.useHeartbeats true in
set_option trace.profiler true in
set_option trace.Meta.synthInstance true in
#synth ContinuousConstSMul 𝕜 F

takes 1479817 mHeartbeats on master and 1866830 mHeartbeats on this branch (a 25% slowdown). Matt has suggested on the Zulip thread #mathlib4 > Normed modules @ 💬 that there are now two paths to (0 : 𝕜), taking two different routes from NormedCommRing to NonUnitalNonAssocSemiring (explicitly NormedCommRing->NonUnitalNormedCommRing->NonUnitalCommRing->NonUnitalNonAssocCommRing->NonUnitalNonAssocCommSemiring->NonUnitalNonAssocSemiring vs NormedCommRing->SeminormedCommRing->SeminormedRing->Ring->NonAssocRing->NonUnitalNonAssocRing->NonUnitalNonAssocSemiring) but these routes are rfl even with with_reducible_and_instances on. The big difference in the traces comes when trying to check that two instances of IsBoundedSMul 𝕜 F are defeq; this needs a 0 on 𝕜 and we have

                  [] [37879.000000] ✅️ MulZeroClass.toZero =?= MulZeroClass.toZero ▶

on this branch vs

                  [] [39.000000] ✅️ MulZeroClass.toZero =?= MulZeroClass.toZero

on master. Digging further into the slow trace the only times things don't look syntactically identical is right at the end:

                                                  [] [5318.000000] ✅️ Ring.toSemiring =?= Ring.toSemiring ▼
                                                    [] [5051.000000] ✅️ NormedRing.toRing.1 =?= SeminormedRing.toRing.1 ▼
                                                      [whnf] [27.000000] Non-easy whnf: Ring 𝕜 
                                                      [whnf] [992.000000] Non-easy whnf: NormedRing.toRing ▶
                                                      [whnf] [1434.000000] Non-easy whnf: SeminormedRing.toRing ▶
                                                      [] [1448.000000] ✅️ NormedRing.toRing =?= SeminormedRing.toRing ▼
                                                        [whnf] [310.000000] Non-easy whnf: NormedCommRing.toNormedRing ▶
                                                        [whnf] [368.000000] Non-easy whnf: Field.toCommRing ▶
                                                        [whnf] [289.000000] Non-easy whnf: SeminormedCommRing.toSeminormedRing ▶
                                                        [] [23.000000] ✅️ NormedRing.toRing =?= NormedRing.toRing

where Lean has made two ring structures on 𝕜, one through NormedRing and one through SeminormedRing. I kind of feel like this is one of these situations where one line of code might fix everything up but I don't yet know what that line is.

loefflerd · 2025-04-14T07:28:59Z

Thanks Eric for making this PR! I am going to set #23787 to draft, and this PR to non-draft, since it contains the "first stage" of what I planned for that PR. Thanks to everyone who has contributed so far to trying to diagnose the slow-downs!

loefflerd and others added 15 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

eric-wieser mentioned this pull request Apr 13, 2025

refactor: mixin class for norm_smul with strict equality #23787

Draft

kbuzzard mentioned this pull request Apr 13, 2025

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

Closed

loefflerd marked this pull request as ready for review April 14, 2025 07:29

loefflerd changed the title ~~refactor: mixin class for norm_smul with strict equality (alternative)~~ refactor: mixin class for norm_smul with strict equality Apr 14, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor: mixin class for `norm_smul` with strict equality #24003

refactor: mixin class for `norm_smul` with strict equality #24003

eric-wieser commented Apr 13, 2025 •

edited by loefflerd

Loading

github-actions bot commented Apr 13, 2025

Declarations diff

eric-wieser commented Apr 13, 2025

leanprover-bot commented Apr 13, 2025

github-actions bot commented Apr 13, 2025

kbuzzard commented Apr 13, 2025 •

edited

Loading

loefflerd commented Apr 14, 2025

refactor: mixin class for norm_smul with strict equality #24003

Are you sure you want to change the base?

refactor: mixin class for norm_smul with strict equality #24003

Conversation

eric-wieser commented Apr 13, 2025 • edited by loefflerd Loading

github-actions bot commented Apr 13, 2025

PR summary 0ac28ed9f4

Import changes for modified files

Declarations diff

eric-wieser commented Apr 13, 2025

leanprover-bot commented Apr 13, 2025

github-actions bot commented Apr 13, 2025

kbuzzard commented Apr 13, 2025 • edited Loading

loefflerd commented Apr 14, 2025

refactor: mixin class for `norm_smul` with strict equality #24003

refactor: mixin class for `norm_smul` with strict equality #24003

eric-wieser commented Apr 13, 2025 •

edited by loefflerd

Loading

kbuzzard commented Apr 13, 2025 •

edited

Loading