[Merged by Bors] - feat: use a constructor for NNReal by sgouezel · Pull Request #37609 · leanprover-community/mathlib4

sgouezel · 2026-04-03T17:50:48Z

Currently, many elements of NNReal are constructed as pair (x, hx), i.e., as elements of the subtype of nonnegative real numbers. The two types are defeq, but not reducibly, so this creates many defeq abuses. This PR introduces a constructor NNReal.mk and uses it instead of the bare constructor, to avoid these defeq abuses.

github-actions · 2026-04-03T17:51:53Z

PR summary cd8272a9d5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Measurable.nnreal_mk
+ instance {M : Type*} [SMul ℝ M] : SMul ℝ≥0 M
+ inv_mk
+ mk
+-+--+ nnnorm_nnratCast

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) = (8.00, 0.00)

Current number	Change	Type
6893	-8	backward.isDefEq.respectTransparency

Current commit 5954d3878f
Reference commit cd8272a9d5

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

sgouezel · 2026-04-04T10:16:24Z

!radar

leanprover-radar · 2026-04-04T10:16:43Z

Benchmark results for 23488c7 against cd8272a are in. There are no significant changes. @sgouezel

🟥 build//instructions: +7.9G (+0.00%)

Medium changes (2🟥)

🟥 build/module/Mathlib.Analysis.Analytic.Composition//instructions: +19.2G (+16.57%)
🟥 build/module/Mathlib.Geometry.Manifold.Riemannian.Basic//instructions: +4.0G (+5.71%)

riccardobrasca · 2026-04-04T18:24:40Z

!radar

leanprover-radar · 2026-04-04T18:25:00Z

Benchmark results for 21b9539 against cd8272a are in. Significant changes detected! @riccardobrasca

🟥 build//instructions: +109.5G (+0.06%)

Medium changes (8🟥)

🟥 build/module/Mathlib.Analysis.Analytic.Composition//instructions: +19.0G (+16.40%)
🟥 build/module/Mathlib.Geometry.Euclidean.Volume.Measure//instructions: +2.0G (+6.31%)
🟥 build/module/Mathlib.Geometry.Manifold.Riemannian.Basic//instructions: +4.0G (+5.77%)
🟥 build/module/Mathlib.InformationTheory.KullbackLeibler.Basic//instructions: +5.0G (+20.43%) (reduced significance based on absolute threshold)
🟥 build/module/Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue//instructions: +12.4G (+24.95%)
🟥 build/module/Mathlib.MeasureTheory.Measure.FiniteMeasure//instructions: +13.8G (+28.19%)
🟥 build/module/Mathlib.MeasureTheory.Measure.Haar.Unique//instructions: +11.2G (+16.63%)
🟥 build/module/Mathlib.Probability.Distributions.SetBernoulli//instructions: +1.8G (+12.90%)

Small changes (8🟥)

🟥 build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique//instructions: +1.4G (+1.98%)
🟥 build/module/Mathlib.Analysis.Convex.SpecificFunctions.Pow//instructions: +1.3G (+12.52%)
🟥 build/module/Mathlib.MeasureTheory.Covering.Differentiation//instructions: +4.4G (+9.66%)
🟥 build/module/Mathlib.MeasureTheory.Group.MeasurableEquiv//instructions: +971.8M (+3.86%)
🟥 build/module/Mathlib.MeasureTheory.Group.ModularCharacter//instructions: +992.8M (+6.67%)
🟥 build/module/Mathlib.MeasureTheory.Measure.Hausdorff//instructions: +2.1G (+3.11%)
🟥 build/module/Mathlib.MeasureTheory.Measure.ProbabilityMeasure//instructions: +4.1G (+11.23%)
🟥 build/module/Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan//instructions: +794.2M (+3.66%)

sgouezel · 2026-04-04T19:10:10Z

The bad radar comes from the fact that I add an instance

instance {M : Type*} [SMul ℝ M] : SMul ℝ≥0 M :=
  ⟨fun c m ↦ (c : ℝ) • m⟩

while before we only had it for a MulAction, expressed in terms of toRealHom.toMonoidHom (so, with bad defeq behavior at instance transparency). This change is useful to remove several backward.isDefEq.respectTransparency , so I think it's a good change even if it has a small performance impact.

riccardobrasca · 2026-04-04T19:39:08Z

I agree it is worth. Let's just see how is now.

!redar

riccardobrasca · 2026-04-04T19:51:52Z

!radar

leanprover-radar · 2026-04-04T19:52:08Z

Benchmark results for 5954d38 against cd8272a are in. Significant changes detected! @riccardobrasca

🟥 build//instructions: +95.6G (+0.05%)

Medium changes (8🟥)

🟥 build/module/Mathlib.Analysis.Analytic.Composition//instructions: +19.1G (+16.49%)
🟥 build/module/Mathlib.Geometry.Euclidean.Volume.Measure//instructions: +2.0G (+6.43%)
🟥 build/module/Mathlib.Geometry.Manifold.Riemannian.Basic//instructions: +4.0G (+5.75%)
🟥 build/module/Mathlib.InformationTheory.KullbackLeibler.Basic//instructions: +5.0G (+20.44%) (reduced significance based on absolute threshold)
🟥 build/module/Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue//instructions: +12.1G (+24.51%)
🟥 build/module/Mathlib.MeasureTheory.Measure.FiniteMeasure//instructions: +13.7G (+27.97%)
🟥 build/module/Mathlib.MeasureTheory.Measure.Haar.Unique//instructions: +11.2G (+16.58%)
🟥 build/module/Mathlib.Probability.Distributions.SetBernoulli//instructions: +1.8G (+12.86%)

Small changes (8🟥)

🟥 build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique//instructions: +1.4G (+1.93%)
🟥 build/module/Mathlib.Analysis.Convex.SpecificFunctions.Pow//instructions: +1.3G (+12.43%)
🟥 build/module/Mathlib.MeasureTheory.Covering.Differentiation//instructions: +4.5G (+9.70%)
🟥 build/module/Mathlib.MeasureTheory.Group.MeasurableEquiv//instructions: +911.2M (+3.62%)
🟥 build/module/Mathlib.MeasureTheory.Group.ModularCharacter//instructions: +1.1G (+7.38%)
🟥 build/module/Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic//instructions: +893.0M (+3.34%)
🟥 build/module/Mathlib.MeasureTheory.Measure.Hausdorff//instructions: +2.1G (+3.09%)
🟥 build/module/Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan//instructions: +828.4M (+3.81%)

riccardobrasca · 2026-04-04T20:13:48Z

I think we can live with this slow down. Thanks!

bors merge

Currently, many elements of NNReal are constructed as pair (x, hx), i.e., as elements of the subtype of nonnegative real numbers. The two types are defeq, but not reducibly, so this creates many defeq abuses. This PR introduces a constructor `NNReal.mk` and uses it instead of the bare constructor, to avoid these defeq abuses. Co-authored-by: sgouezel <[email protected]>

mathlib-bors · 2026-04-04T20:42:20Z

Pull request successfully merged into master.

Build succeeded:

JovanGerb · 2026-04-04T21:27:29Z

I see a lot of simp; rfl. Are we missing some simp lemma?

Currently, many elements of NNReal are constructed as pair (x, hx), i.e., as elements of the subtype of nonnegative real numbers. The two types are defeq, but not reducibly, so this creates many defeq abuses. This PR introduces a constructor `NNReal.mk` and uses it instead of the bare constructor, to avoid these defeq abuses. Co-authored-by: sgouezel <[email protected]>

start

e610a3b

github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Apr 3, 2026

sgouezel added 16 commits April 3, 2026 20:19

fix

fd3b7aa

fix

6cc8938

fix

3671007

fix

f18f0e1

fix

7c6ff88

fix

2fa1d31

fix

c8601af

fix

929da6e

better

e345950

fix

852b34b

fix

a52d7be

fix

4700e96

fix

5e6de3c

fix

15f6f33

fix

402c371

cleanup

23488c7

riccardobrasca reviewed Apr 4, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean Outdated

sgouezel added 2 commits April 4, 2026 17:57

one more fix

0ae01d6

fix

21b9539

riccardobrasca reviewed Apr 4, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean Outdated

better

5954d38

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Apr 4, 2026

mathlib-bors bot changed the title ~~feat: use a constructor for NNReal~~ [Merged by Bors] - feat: use a constructor for NNReal Apr 4, 2026

mathlib-bors bot closed this Apr 4, 2026

sgouezel mentioned this pull request Apr 7, 2026

chore: improve performance in NNReal by only inheriting SMul from Real for MulAction #37728

Closed

sgouezel deleted the SG_betterNNRealMk branch April 10, 2026 08:37

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary cd8272a9d5

Import changes for modified files

Declarations diff

Uh oh!

sgouezel commented Apr 4, 2026

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

Uh oh!

riccardobrasca commented Apr 4, 2026

Uh oh!

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

Uh oh!

Uh oh!

sgouezel commented Apr 4, 2026

Uh oh!

riccardobrasca commented Apr 4, 2026

Uh oh!

riccardobrasca commented Apr 4, 2026

Uh oh!

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

Uh oh!

Uh oh!

riccardobrasca commented Apr 4, 2026

Uh oh!

mathlib-bors bot commented Apr 4, 2026

Uh oh!

JovanGerb commented Apr 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

sgouezel commented Apr 3, 2026 •

edited

Loading

github-actions bot commented Apr 3, 2026 •

edited

Loading

leanprover-radar commented Apr 4, 2026 •

edited

Loading

leanprover-radar commented Apr 4, 2026 •

edited

Loading

leanprover-radar commented Apr 4, 2026 •

edited

Loading