perf(Analysis/Normed/Group): lower instance priorities by JovanGerb · Pull Request #37962 · leanprover-community/mathlib4

JovanGerb · 2026-04-12T19:54:54Z

This is an attempt to improve performance by lowering the priority of some normed instances.

The idea is that when looking for algebraic instances, searching in the Normed hierarchy is likely to be expensive and not useful.

github-actions · 2026-04-12T19:55:56Z

PR summary 3d8100bbc6

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Complex.Isometry	1981	1982	+1 (+0.05%)

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Complex.Isometry`	1

Declarations diff

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

You can run this locally as follows

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

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

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

Decrease in tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type
6751	-2	backward.isDefEq.respectTransparency

Current commit 3a213a7faf
Reference commit 3d8100bbc6

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

JovanGerb · 2026-04-12T19:56:27Z

!bench

leanprover-radar · 2026-04-12T19:56:46Z

Benchmark results for 588a6c1 against 3d8100b are in. Significant changes detected! @JovanGerb

✅ build//instructions: -948.1G (-0.55%)

Large changes (10✅, 1🟥)

✅ build/module/Mathlib.Analysis.CStarAlgebra.Matrix//instructions: -22.1G (-15.66%)
🟥 build/module/Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas//instructions: +12.8G (+11.67%)
✅ build/module/Mathlib.Analysis.Normed.Lp.lpSpace//instructions: -49.9G (-24.28%)
✅ build/module/Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm//instructions: -19.3G (-18.65%)
✅ build/module/Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar//instructions: -9.3G (-37.50%)
✅ build/module/Mathlib.FieldTheory.Galois.Profinite//instructions: -9.0G (-12.79%)
✅ build/module/Mathlib.Geometry.Manifold.Riemannian.Basic//instructions: -19.2G (-27.19%)
✅ build/module/Mathlib.MeasureTheory.Function.SimpleFuncDenseLp//instructions: -16.8G (-18.95%)
✅ build/module/Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule//instructions: -17.5G (-28.35%)
✅ build/module/Mathlib.NumberTheory.NumberField.Ideal.Basic//instructions: -23.0G (-63.41%)
✅ build/module/Mathlib.NumberTheory.NumberField.Units.Regulator//instructions: -12.5G (-25.06%)

Medium changes (66✅, 14🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (163✅, 69🟥)

Too many entries to display here. View the full report on radar instead.

JovanGerb · 2026-04-13T03:15:47Z

!bench

leanprover-radar · 2026-04-13T03:16:11Z

Benchmark results for 877ba14 against 3d8100b are in. Significant changes detected! @JovanGerb

✅ build//instructions: -876.6G (-0.50%)

Large changes (9✅, 1🟥)

🟥 build/module/Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas//instructions: +13.4G (+12.23%)
✅ build/module/Mathlib.Analysis.Normed.Lp.lpSpace//instructions: -49.3G (-24.01%)
✅ build/module/Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm//instructions: -19.3G (-18.70%)
✅ build/module/Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar//instructions: -9.4G (-37.69%)
✅ build/module/Mathlib.FieldTheory.Galois.Profinite//instructions: -9.4G (-13.36%)
✅ build/module/Mathlib.Geometry.Manifold.Riemannian.Basic//instructions: -19.2G (-27.19%)
✅ build/module/Mathlib.MeasureTheory.Function.SimpleFuncDenseLp//instructions: -16.7G (-18.84%)
✅ build/module/Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule//instructions: -18.0G (-29.13%)
✅ build/module/Mathlib.NumberTheory.NumberField.Ideal.Basic//instructions: -23.1G (-63.50%)
✅ build/module/Mathlib.NumberTheory.NumberField.Units.Regulator//instructions: -12.5G (-25.07%)

Medium changes (65✅, 15🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (154✅, 77🟥)

Too many entries to display here. View the full report on radar instead.

This reverts commit 877ba14.

JovanGerb · 2026-04-13T03:51:58Z

!bench

leanprover-radar · 2026-04-13T03:52:19Z

Benchmark results for 53446cc against 3d8100b are in. Significant changes detected! @JovanGerb

✅ build//instructions: -931.8G (-0.54%)

Large changes (10✅, 2🟥)

✅ build/module/Mathlib.Analysis.CStarAlgebra.Matrix//instructions: -22.0G (-15.54%)
🟥 build/module/Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas//instructions: +12.8G (+11.72%)
✅ build/module/Mathlib.Analysis.Normed.Lp.lpSpace//instructions: -49.9G (-24.29%)
✅ build/module/Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm//instructions: -19.1G (-18.52%)
✅ build/module/Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar//instructions: -9.4G (-37.66%)
✅ build/module/Mathlib.FieldTheory.Galois.Profinite//instructions: -9.1G (-12.83%)
✅ build/module/Mathlib.Geometry.Manifold.Riemannian.Basic//instructions: -19.3G (-27.25%)
✅ build/module/Mathlib.MeasureTheory.Function.SimpleFuncDenseLp//instructions: -16.8G (-18.93%)
✅ build/module/Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule//instructions: -17.4G (-28.26%)
✅ build/module/Mathlib.NumberTheory.NumberField.Ideal.Basic//instructions: -23.0G (-63.45%)
✅ build/module/Mathlib.NumberTheory.NumberField.Units.Regulator//instructions: -12.5G (-25.14%)
🟥 build/module/Mathlib.Probability.ConditionalExpectation//instructions: +17.0G (+137.48%)

Medium changes (66✅, 15🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (161✅, 67🟥)

Too many entries to display here. View the full report on radar instead.

JovanGerb · 2026-04-13T04:10:40Z

!bench

leanprover-radar · 2026-04-13T04:10:58Z

Benchmark results for 268a6a5 against 3d8100b are in. Significant changes detected! @JovanGerb

✅ build//instructions: -940.6G (-0.54%)

Large changes (10✅, 1🟥)

✅ build/module/Mathlib.Analysis.CStarAlgebra.Matrix//instructions: -22.0G (-15.56%)
🟥 build/module/Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas//instructions: +12.9G (+11.75%)
✅ build/module/Mathlib.Analysis.Normed.Lp.lpSpace//instructions: -50.0G (-24.32%)
✅ build/module/Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm//instructions: -19.3G (-18.66%)
✅ build/module/Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar//instructions: -9.3G (-37.27%)
✅ build/module/Mathlib.FieldTheory.Galois.Profinite//instructions: -9.1G (-12.89%)
✅ build/module/Mathlib.Geometry.Manifold.Riemannian.Basic//instructions: -19.2G (-27.18%)
✅ build/module/Mathlib.MeasureTheory.Function.SimpleFuncDenseLp//instructions: -16.8G (-18.98%)
✅ build/module/Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule//instructions: -17.5G (-28.30%)
✅ build/module/Mathlib.NumberTheory.NumberField.Ideal.Basic//instructions: -23.0G (-63.41%)
✅ build/module/Mathlib.NumberTheory.NumberField.Units.Regulator//instructions: -12.4G (-24.91%)

Medium changes (66✅, 15🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (165✅, 67🟥)

Too many entries to display here. View the full report on radar instead.

grunweg

Thanks a lot for doing this; this looks great! I have a few clarification questions (and would maintainer merge otherwise/already merge some parts of it).

Mathlib/Analysis/Calculus/DiffContOnCl.lean

grunweg · 2026-04-13T10:41:28Z

Mathlib/Analysis/Complex/Isometry.lean



 noncomputable section
+suppress_compilation -- needed to avoid a panic!


Can you minimize this? This seems worth reporting!

grunweg · 2026-04-13T10:42:07Z

Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

 end basic

-variable [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
+variable [Fintype m] [NonUnitalCStarAlgebra A]


Is there a reason for this change? (I like it regardless; if it compiles on its own, I'm happy to splice-bot it.)

Yes, a linter suddenly told me that these hypotheses were unused.

Um, once more:
splice-bot

Split PR created

Split off the changes to Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean in #37996.

grunweg · 2026-04-13T10:43:10Z

Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean

-variable [Fintype ι]
-
-lemma toLp_pi (p : ℝ≥0∞) [Fact (1 ≤ p)] (hX : HasGaussianLaw (fun ω ↦ (X · ω)) P) :
+lemma toLp_pi [Finite ι] (p : ℝ≥0∞) [Fact (1 ≤ p)] (hX : HasGaussianLaw (fun ω ↦ (X · ω)) P) :


Thanks for the fix. I gather this is linter with the lower priority, but not now --- do you know why/ is there a deeper problem we should fix?

Similarly to the other change, the linter now recognized that some type class assumption was unused. This is because the synthesis order changed, so a different instance was found. This does not necessarily mean that something is wrong, though it is a bit counter intuitive.

Makes sense, thanks!

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

perf(Analysis/Normed/Group): lower instance priorities

aec0f19

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

JovanGerb added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 12, 2026

JovanGerb added 3 commits April 12, 2026 23:59

fixes

0e0c658

fixes

7121b64

fix

588a6c1

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 13, 2026

also for ring and field

877ba14

JovanGerb added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 13, 2026

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 13, 2026

JovanGerb added 2 commits April 13, 2026 05:50

Revert "also for ring and field"

9dcb80c

This reverts commit 877ba14.

even lower?

53446cc

higher?

268a6a5

grunweg reviewed Apr 13, 2026

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 13, 2026

Update Mathlib/Analysis/Calculus/DiffContOnCl.lean

3a213a7

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-splicebot bot mentioned this pull request Apr 13, 2026

chore(Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean): automated extraction #37996

Open



		noncomputable section
		suppress_compilation -- needed to avoid a panic!

Conversation

JovanGerb commented Apr 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3d8100bbc6

Import changes for modified files

Declarations diff

Uh oh!

JovanGerb commented Apr 12, 2026

Uh oh!

leanprover-radar commented Apr 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JovanGerb commented Apr 13, 2026

Uh oh!

leanprover-radar commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JovanGerb commented Apr 13, 2026

Uh oh!

leanprover-radar commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JovanGerb commented Apr 13, 2026

Uh oh!

leanprover-radar commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mathlib-splicebot bot Apr 13, 2026

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

JovanGerb commented Apr 12, 2026 •

edited

Loading

github-actions bot commented Apr 12, 2026 •

edited

Loading

leanprover-radar commented Apr 12, 2026 •

edited

Loading

leanprover-radar commented Apr 13, 2026 •

edited

Loading

leanprover-radar commented Apr 13, 2026 •

edited

Loading

leanprover-radar commented Apr 13, 2026 •

edited

Loading