[Merged by Bors] - feat: add classes ContinuousENorm and ENormed(Add)(Comm)Monoid#21670
Closed
[Merged by Bors] - feat: add classes ContinuousENorm and ENormed(Add)(Comm)Monoid#21670
ContinuousENorm and ENormed(Add)(Comm)Monoid#21670Conversation
PR summary 318e19735f
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.Normed.Group.Basic | 1037 | 1054 | +17 (+1.64%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Analysis.Normed.Affine.Simplex |
5 |
4 filesMathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Normed.MulAction |
8 |
4 filesMathlib.Analysis.Polynomial.CauchyBound Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Topology.MetricSpace.CauSeqFilter |
16 |
11 filesMathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.Constructions Mathlib.Analysis.Normed.Group.Subgroup 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 |
17 |
Declarations diff
+ Continuous.enorm
+ ContinuousAt.enorm
+ ContinuousENorm
+ ContinuousOn.enorm
+ ContinuousWithinAt.enorm
+ ENormedAddCommMonoid
+ ENormedAddMonoid
+ ENormedCommMonoid
+ ENormedMonoid
+ Inseparable.enorm_eq_enorm'
+ NormedCommGroup.toENormedCommMonoid
+ NormedGroup.toENormedMonoid
+ SeminormedGroup.toContinuousENorm
+ continuous_enorm
- Continuous.enorm'
- ContinuousAt.enorm'
- ContinuousOn.enorm'
- ContinuousWithinAt.enorm'
- continuous_enorm'
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
ContinuousENorm and ENormed(Add)(Comm)Monoid, take 2
grunweg
commented
Feb 10, 2025
This was referenced Feb 11, 2025
ContinuousENorm and ENormed(Add)(Comm)Monoid, take 2ContinuousENorm and ENormed(Add)(Comm)Monoid
grunweg
commented
Feb 13, 2025
YaelDillies
reviewed
Feb 18, 2025
Contributor
YaelDillies
left a comment
There was a problem hiding this comment.
All you need is ENNReal.isOpenEmbedding_coe, right? Does reducing imports to Topology.Instances.ENNReal.Defs until it proves not much more than ENNReal.isOpenEmbedding_coe bring the import increase to a reasonable amount?
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Contributor
Author
|
This is ready for another look (and formally depends on #22562 now). I will look into merging |
grunweg
added a commit
that referenced
this pull request
Mar 5, 2025
Splitting it out in #21554 was motivated by avoiding imports of ENNReal. This motivation has become moot now: - with #22562, just the basic properties of ENNReal do not add that many further imports - after #21670, Normed/Group/Basic.lean will import ENNReal anyway. Adding to this, the split into Basic and Continuity was never really clear in terms of imports: Basic.lean should be split further, but this does not seem like a good splitting boundary. While at it, replace one 'open' that has been likely mis-ported by 'open scoped'.
grunweg
added a commit
that referenced
this pull request
Mar 5, 2025
Splitting it out in #21554 was motivated by avoiding imports of ENNReal. This motivation has become moot now: - with #22562, just the basic properties of ENNReal do not add that many further imports - after #21670, Normed/Group/Basic.lean will import ENNReal anyway. Adding to this, the split into Basic and Continuity was never really clear in terms of imports: Basic.lean should be split further, but this does not seem like a good splitting boundary. While at it, replace one 'open' that has been likely mis-ported by 'open scoped'.
Collaborator
|
This PR/issue depends on: |
YaelDillies
approved these changes
Mar 5, 2025
Contributor
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks! 🚀
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
Contributor
Author
|
Thanks for the quick review! |
sgouezel
reviewed
Mar 5, 2025
Contributor
Author
|
This is ready for review again. |
Member
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 7, 2025
…21670) and prove that these contain (commutative) `(Add)NormedGroup`s. This allows generalising results from normed spaces/normed groups to `ENNReal` also. A future PR will generalise lemmas in mathlib to use these new classes. This PR only changes a few lemmas, to prove that these definitions are set up right. From the Carleson project. Co-authored-by: grunweg <rothgami@math.hu-berlin.de> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
ContinuousENorm and ENormed(Add)(Comm)MonoidContinuousENorm and ENormed(Add)(Comm)Monoid
3 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
10 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
and prove that these contain (commutative)
(Add)NormedGroups. This allows generalising results from normed spaces/normed groups toENNRealalso.A future PR will generalise lemmas in mathlib to use these new classes. This PR only changes a few lemmas, to prove that these definitions are set up right.
From the Carleson project.
There is a zulip thread for discussing the large import.
Re-done version of #21422.
simpprio #22215 (to fix an unrelated simpNF linter timeout downstream, exposed by this PR)