feat: add classes `ContinuousENorm` and `ENormed(Add)(Comm)Monoid` by grunweg · Pull Request #21422 · leanprover-community/mathlib4

grunweg · 2025-02-04T13:31:48Z

This will allow generalising results from normed spaces/normed groups to ENNReal also.
From the Carleson project.
A future PR will generalise lemmas in mathlib to use these new classes.

depends on: [Merged by Bors] - perf(RingTheory/Artinian): reorder arguments in IsArtinianRing.isMaximal_of_isPrime #21449 for fixing the simpNF linter time-out

github-actions · 2025-02-04T13:32:44Z

PR summary 11b1b0885c

Import changes exceeding 2%

%	File
+4.56%	`Mathlib.Analysis.Normed.Group.Basic`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Group.Basic	1141	1193	+52 (+4.56%)

Import changes for all files

Files	Import difference
7 files `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter`	2
35 files `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.IsIntegral` `Mathlib.Analysis.Complex.OperatorNorm` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Topology` `Mathlib.Analysis.InnerProductSpace.Defs` `Mathlib.Analysis.LocallyConvex.ContinuousOfBounded` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Normed.Group.Tannery` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.Analysis.NormedSpace.Extend` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Modular` `Mathlib.Topology.ContinuousMap.Bounded.Star` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps`	5
`Mathlib.Analysis.BoxIntegral.Partition.Additive`	6
23 files `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics` `Mathlib.Analysis.NormedSpace.OperatorNorm.Basic` `Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.Analysis.NormedSpace.OperatorNorm.Mul` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Topology.Category.DeltaGenerated` `Mathlib.Topology.Compactness.DeltaGeneratedSpace` `Mathlib.Topology.ContinuousMap.Bounded.Basic` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported`	7
5 files `Mathlib.Analysis.Normed.Algebra.Ultra` `Mathlib.Analysis.Normed.Field.Ultra` `Mathlib.Data.Real.IsNonarchimedean` `Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued`	9
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital` `Mathlib.Topology.ContinuousMap.Polynomial`	13
16 files `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.Analysis.Normed.Group.Ultra` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.LinearAlgebra.Matrix.Gershgorin` `Mathlib.NumberTheory.DirichletCharacter.Bounds` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.Topology.Algebra.Module.FiniteDimension` `Mathlib.Topology.Algebra.Polynomial`	16
`Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.Multilinear.Topology`	20
42 files `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.Analysis.Normed.Field.Lemmas` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.Analysis.Normed.Group.NullSubmodule` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.MulAction` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.NormedSpace.BallAction` `Mathlib.Analysis.NormedSpace.ConformalLinearMap` `Mathlib.Analysis.NormedSpace.ENormedSpace` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.Analysis.NormedSpace.SphereNormEquiv` `Mathlib.Analysis.Seminorm` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.Topology.Germ` `Mathlib.Topology.UniformSpace.Dini`	23
`Mathlib.Analysis.Polynomial.CauchyBound`	34
`Mathlib.Topology.Algebra.InfiniteSum.Field`	43
5 files `Mathlib.Analysis.Asymptotics.Defs` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.Topology.MetricSpace.CauSeqFilter`	45
12 files `Mathlib.Analysis.Normed.Group.Basic` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Analysis.Normed.Group.CocompactMap` `Mathlib.Analysis.Normed.Group.Constructions` `Mathlib.Analysis.Normed.Group.Int` `Mathlib.Analysis.Normed.Group.Rat` `Mathlib.Analysis.Normed.Group.Submodule` `Mathlib.Analysis.Normed.Order.Hom.Basic` `Mathlib.Analysis.Normed.Order.Hom.Ultra` `Mathlib.Analysis.NormedSpace.IndicatorFunction` `Mathlib.Analysis.NormedSpace.MStructure` `Mathlib.InformationTheory.Hamming`	52

Declarations diff

+ ContinuousENorm
+ ENormedAddCommMonoid
+ ENormedAddMonoid
+ ENormedCommMonoid
+ ENormedMonoid
+ instance [SeminormedAddGroup E] : ContinuousENorm E
+ instance [SeminormedGroup E] : ContinuousENorm 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).

grunweg · 2025-02-04T15:26:43Z

The diagnostics output on the simp lemma is not helpful: putting

set_option diagnostics true in
example (I : Ideal (MvPolynomial σ k)) : vanishingIdeal (zeroLocus I) = sorry := by simp

at the end of Mathlib/RingTheory/Nullstellensatz.lean (i.e., the LHS of the lemma that times out in CI) yields

[diag] Diagnostics ▼
  [reduction] unfolded declarations (max: 156, num: 8): ▶
  [reduction] unfolded instances (max: 975, num: 38): ▼
    [] Field.toCommRing ↦ 975     [] CommRing.toRing ↦ 912     [] Ring.toSemiring ↦ 717     [] CommSemiring.toSemiring ↦ 657     [] EuclideanDomain.toCommRing ↦ 550     [] Field.toEuclideanDomain ↦ 550     [] Semiring.toNonUnitalSemiring ↦ 484     [] NonUnitalSemiring.toNonUnitalNonAssocSemiring ↦ 444     [] Semiring.toNonAssocSemiring ↦ 404     [] NonAssocSemiring.toNonUnitalNonAssocSemiring ↦ 400     [] NonUnitalNonAssocSemiring.toAddCommMonoid ↦ 366     [] CommRing.toCommSemiring ↦ 349     [] Field.toSemifield ↦ 342     [] Semifield.toCommSemiring ↦ 342     [] AddCommMonoid.toAddMonoid ↦ 318     [] DivisionRing.toRing ↦ 269     [] AddMonoid.toAddZeroClass ↦ 88     [] AddZeroClass.toZero ↦ 84     [] MulZeroClass.toZero ↦ 84     [] NonUnitalNonAssocSemiring.toMulZeroClass ↦ 84     [] PartialOrder.toPreorder ↦ 84     [] LinearOrder.toPartialOrder ↦ 80     [] Preorder.toLT ↦ 48     [] Finset.instUnion ↦ 40     [] AddMonoid.toAddSemigroup ↦ 36     [] AddMonoidAlgebra.commRing ↦ 35     [] instCommRingMvPolynomial ↦ 35     [] AddMonoidAlgebra.nonUnitalNonAssocSemiring ↦ 34     [] AddMonoidAlgebra.nonUnitalSemiring ↦ 34     [] AddMonoidAlgebra.nonUnitalCommSemiring ↦ 30     [] Lattice.toSemilatticeSup ↦ 30     [] NonUnitalCommSemiring.toNonUnitalSemiring ↦ 30     [] SemilatticeSup.toPartialOrder ↦ 30     [] Finsupp.instAddCommMonoid ↦ 28     [] Finsupp.instAddMonoid ↦ 28     [] AddCommGroup.toAddGroup ↦ 22     [] AddGroup.toSubNegMonoid ↦ 22     [] SubNegMonoid.toAddMonoid ↦ 22 
  [reduction] unfolded reducible declarations (max: 96, num: 11): ▶
  [def_eq] heuristic for solving `f a =?= f b` (max: 60, num: 1): ▶

The instance searches do not traverse anything related to ENorm. (In fact, reverting the ENorm change does not change anything in the output.)

fpvandoorn · 2025-02-04T15:27:51Z

Yes, please also add the multiplicative versions of these classes, so that we can keep using to_additive

grunweg · 2025-02-04T15:34:01Z

Added (and force-pushed, sorry).

fpvandoorn · 2025-02-04T15:39:01Z

Can you add a doc of the form "We don't have ENormedAddCommGroup extend EMetricSpace, since the canonical instance ℝ≥0∞ is not an EMetricSpace. The reason that ℝ≥0∞ isn't an EMetricSpace is because it carries the order-topology, which is distinct from the topology coming from edist."

fpvandoorn · 2025-02-04T15:42:25Z

Upon reflection, the definition of EMetricSpace might just be "wrong" in that it is undesirable to require that the topology comes from edist. You rarely want to think of points with distance ∞ from every other point to be isolated points.

And indeed: the only instances for EMetricSpace come from other EMetricSpaces or from MetricSpace.

But changing that is of course not part of this PR, so the previous description is still useful to have.

fpvandoorn · 2025-02-04T15:43:55Z

Other than that, LGTM, but I'll let someone else merge/delegate it, since I'm a coauthor.

grunweg · 2025-02-04T16:32:03Z

Added a comment.

The simpNF linter still fails, and I'm still at a loss why.

…imal_of_isPrime`

grunweg · 2025-02-05T09:29:13Z

@JovanGerb diagnosed the hang and found a fix 🎉 I hope that with it included, the linting step will finally pass.

mathlib4-dependent-issues-bot · 2025-02-05T13:09:45Z

This PR/issue depends on:

~~[Merged by Bors] - perf(RingTheory/Artinian): reorder arguments in IsArtinianRing.isMaximal_of_isPrime #21449~~
By Dependent Issues (🤖). Happy coding!

grunweg · 2025-02-05T14:31:19Z

@fpvandoorn I copied the instances from your Carleson file; this causes issues (including what looks like a diamond to me); you can see the build failing. I haven't looked into it deeply so far.

Mathlib/Analysis/Normed/Group/Basic.lean

grunweg · 2025-02-05T17:34:31Z

One step further: now line 993 errors. The relevant snippet is (line 993 is the to_additive).

@[to_additive Filter.Tendsto.enorm]
lemma Filter.Tendsto.enorm' (h : Tendsto f l (𝓝 a)) : Tendsto (‖f ·‖ₑ) l (𝓝 ‖a‖ₑ) :=
  .comp continuous_enorm'.continuousAt h

The error message is

application type mismatch
  instContinuousENorm
argument has type
  SeminormedAddGroup E
but function has type
  [inst : SeminormedGroup E] → ContinuousENorm E

I wonder: continuous_enorm(') on line 950 takes no argument E, but ENormed(Add)Monoid does. Is this related to this error?

Mathlib/Analysis/Normed/Group/Basic.lean

fpvandoorn · 2025-02-07T15:32:55Z

Mathlib/Analysis/Normed/Group/Basic.lean

 import Mathlib.Algebra.Group.Subgroup.Ker
 import Mathlib.Analysis.Normed.Group.Seminorm
-import Mathlib.Topology.Instances.ENNReal.Defs
+import Mathlib.Topology.Instances.ENNReal.Lemmas


This import increase is in tension with the aim to reduce the imports of this file, see https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Turn.20.60Complex.2Eabs.60.20into.20.60Norm.60
cc @YaelDillies

I guess you need this to know that one of the coercions is continuous?

I am interested to know why you need this new import, yes

Mathlib/Analysis/Normed/Group/Basic.lean

grunweg · 2025-02-11T10:38:22Z

Closing in favour of #21670 (which passes CI now).

…ansported This would have helped me in #21422.

…me cannot be tr… (#21716) …ansported This would have helped me in #21422. Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

grunweg force-pushed the MR-generalise-enorm-2 branch from bdc326e to 196c3fc Compare February 4, 2025 13:32

fpvandoorn added the carleson part of the ongoing formalization of Carleson's theorem label Feb 4, 2025

fpvandoorn added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 4, 2025

grunweg changed the title ~~feat: add classes ContinuousENorm and ENormedAdd(Comm)Monoid~~ feat: add classes ContinuousENorm and ENormed(Add)(Comm)Monoid Feb 4, 2025

Change

3763173

grunweg force-pushed the MR-generalise-enorm-2 branch from 3c688b6 to 3763173 Compare February 4, 2025 15:33

grunweg added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 4, 2025

Add comment.

9217d4f

perf(RingTheory/Artinian): reorder arguments in `IsArtinianRing.isMax…

217ceb5

…imal_of_isPrime`

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 5, 2025

grunweg mentioned this pull request Feb 5, 2025

[Merged by Bors] - perf(RingTheory/Artinian): reorder arguments in IsArtinianRing.isMaximal_of_isPrime #21449

Closed

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 5, 2025

grunweg added 2 commits February 5, 2025 11:06

WIP: add basic instances

31c81e2

WIP: copy-paste instances from the Carleson file; errors

9c0ecd1

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 5, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 5, 2025

Merge remote-tracking branch 'origin/master' into MR-generalise-enorm-2

f2d8088

fpvandoorn reviewed Feb 5, 2025

View reviewed changes

Mathlib/Analysis/Normed/Group/Basic.lean Outdated Show resolved Hide resolved

Fix this error; remove other instances for now.

11b1b08

grunweg commented Feb 5, 2025

View reviewed changes

Mathlib/Analysis/Normed/Group/Basic.lean Outdated Show resolved Hide resolved

fpvandoorn reviewed Feb 5, 2025

View reviewed changes

Mathlib/Analysis/Normed/Group/Basic.lean Outdated Show resolved Hide resolved

fpvandoorn reviewed Feb 7, 2025

View reviewed changes

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 10, 2025

fpvandoorn reviewed Feb 10, 2025

View reviewed changes

Mathlib/Analysis/Normed/Group/Basic.lean Outdated Show resolved Hide resolved

grunweg added 3 commits February 10, 2025 16:34

Fix to_additive.

4881191

Generalise Continuous.enorm(') and continuous_enorm(').

0a79e74

Fixup

25dc12c

grunweg mentioned this pull request Feb 10, 2025

[Merged by Bors] - feat: add classes ContinuousENorm and ENormed(Add)(Comm)Monoid #21670

Closed

2 tasks

grunweg closed this Feb 11, 2025

grunweg deleted the MR-generalise-enorm-2 branch February 11, 2025 10:38

grunweg added a commit that referenced this pull request Feb 11, 2025

doc(to_additive): more helpful error message when a name cannot be tr…

8007eaf

…ansported This would have helped me in #21422.

grunweg mentioned this pull request Feb 11, 2025

[Merged by Bors] - doc(Tactic/ToAdditive/Frontend): more helpful error message when a name cannot be tr… #21716

Closed

Conversation

grunweg commented Feb 4, 2025 • edited by alreadydone Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 11b1b0885c

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Feb 4, 2025

Uh oh!

fpvandoorn commented Feb 4, 2025

Uh oh!

grunweg commented Feb 4, 2025

Uh oh!

fpvandoorn commented Feb 4, 2025

Uh oh!

fpvandoorn commented Feb 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

fpvandoorn commented Feb 4, 2025

Uh oh!

grunweg commented Feb 4, 2025

Uh oh!

grunweg commented Feb 5, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Feb 5, 2025

Uh oh!

grunweg commented Feb 5, 2025

Uh oh!

Uh oh!

grunweg commented Feb 5, 2025

Uh oh!

Uh oh!

Uh oh!

fpvandoorn Feb 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 7, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

grunweg commented Feb 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

grunweg commented Feb 4, 2025 •

edited by alreadydone

Loading

github-actions bot commented Feb 4, 2025 •

edited

Loading

fpvandoorn commented Feb 4, 2025 •

edited

Loading

fpvandoorn Feb 7, 2025 •

edited

Loading