[Merged by Bors] - feat: e-seminormed monoid by grunweg · Pull Request #27385 · leanprover-community/mathlib4

grunweg · 2025-07-23T10:12:32Z

Most lemmas about these do not require the enorm to be positive definite (i.e., work fine if a nontrivial element has zero enorm), or can be rephrased easily. A handful of lemmas do require this condition.
Add a new class ESeminormed(Add)(Comm)Monoid, which only asks that zero have enorm,
and generalise most lemmas to this class.

The motivating example behind this is eLpNorm, which is an enormed commutative (additive) monoid --- when we drop the definiteness requirement. This will (hopefully) allow unifying many lemma about eLpNorm with their more general enorm variants.

github-actions · 2025-07-23T10:13:43Z

PR summary ed5dc595cc

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ ESeminormedAddCommMonoid
+ ESeminormedAddMonoid
+ ESeminormedCommMonoid
+ ESeminormedMonoid

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

… actual norms

grunweg · 2025-07-24T19:16:58Z

One proof in InjectiveSeminorm.lean needed a fix to not time out: otherwise, the proof would fail with errors like

type mismatch
  MonoidHom.map_pow ?m.905023 ?m.905024 ?m.905025
has type
  ?m.905023 (?m.905024 ^ ?m.905025) = ?m.905023 ?m.905024 ^ ?m.905025 : Prop
but is expected to have type
  mapL (f ^ n) = mapL f ^ n : Prop

Filling in the underscores for f and n makes things work again.
In local testing, adding by apply in front makes it slightly faster with the placeholders filled it (but that's hard to say since wall times are noisy and incremental profiling). Putting by apply with the underscores still fails, but much faster.
Using set_option profiler true in in front of the declaration shows that attribute application is really slow. (22s when failing in term mode, about 4-5s in tactic mode; about 2-3 seconds on my computer when filling in the placeholders.)

I am not sure why this is.

grunweg · 2025-07-24T19:17:15Z

In any case, hopefully everything works now.

sgouezel · 2025-07-27T17:10:53Z

The terminology for addcommgroups is SeminormedAddCommGroup and NormedAddCommGroup. Would it make sense to follow a parallel convention here?

grunweg · 2025-07-29T07:42:45Z

Good question. I'm not sure that convention is helpful, though, because the various enorm classes are not in perfect analogy to normed ones.
The ENorm class (which is the weakest typeclass of all) imposes no assumption on the enorm at all; ContinuousENorm (the next weakest class) only asks for the enorm to be continuous.
If I wanted to follow the new convention, one should also rename

ENorm to (e.g.) ESeminorm --- which is confusing given that no conditions are imposed on the enorm,
ContinuousENorm to e.g. ContinuousESeminorm (which only asks for continuity of the enorm, same issue).

grunweg · 2025-08-11T13:47:16Z

Would you like to take a look, Yael? You reviewed more enorm PRs in the past than Heather did.
(Of course, I won't mind a review from Heather either - nor anybody else for that matter.)

grunweg · 2025-08-12T12:16:24Z

Ready for review again. ~~, assuming CI passes.~~ it does!

YaelDillies

Thanks! 🚀

maintainer merge

github-actions · 2025-08-12T12:56:37Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

mathlib4-merge-conflict-bot · 2025-08-13T14:53:51Z

This pull request has conflicts, please merge master and resolve them.

sgouezel

bors d+

Mathlib/Analysis/Normed/Group/Basic.lean

mathlib-bors · 2025-08-16T07:43:50Z

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

grunweg · 2025-08-16T12:29:31Z

bors merge

Most lemmas about these do not require the enorm to be positive definite (i.e., work fine if a nontrivial element has zero enorm), or can be rephrased easily. A handful of lemmas do require this condition. Add a new class `ESeminormed(Add)(Comm)Monoid`, which only asks that zero have enorm, and generalise most lemmas to this class. The motivating example behind this is `eLpNorm`, which is an enormed commutative (additive) monoid

mathlib-bors · 2025-08-16T13:17:57Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...

Most lemmas about these do not require the enorm to be positive definite (i.e., work fine if a nontrivial element has zero enorm), or can be rephrased easily. A handful of lemmas do require this condition. Add a new class `ESeminormed(Add)(Comm)Monoid`, which only asks that zero have enorm, and generalise most lemmas to this class. The motivating example behind this is `eLpNorm`, which is an enormed commutative (additive) monoid

grunweg added 2 commits July 23, 2025 12:04

Start

466ec2f

Restore two lemmas, for normed groups

65b20be

grunweg added WIP Work in progress carleson part of the ongoing formalization of Carleson's theorem labels Jul 23, 2025

github-actions bot added the t-analysis Analysis (normed *, calculus) label Jul 23, 2025

grunweg added 6 commits July 23, 2025 13:43

Sorry a few

e772613

Generalise a few lemmas to seminorms: the others in this file require…

9e3dceb

… actual norms

A few more

0ca4e02

Fix

374c9de

More classes; restore previous lemmas

c115ed6

Strengthen

df9adbb

grunweg changed the title ~~Start~~ feat: weaken definiteness requirement for ENormed(Add)(Comm)Monoids Jul 24, 2025

grunweg added 7 commits July 24, 2025 18:21

Better inheritance

241235c

chore(LpSeminorm/Basic): fix sorries

b7eccbc

Fixup inheritance

7231c79

wip: generalise IntegrableOn.restrict_toMeasurable to seminorms

d9b17e8

Fix last sorries (up to follow-ups)

605d8c3

Sorry mysterious broken proof

b418eb4

Speed up proof: still slow

5e81eb5

grunweg removed the WIP Work in progress label Jul 24, 2025

leanprover-community-bot-assistant assigned hrmacbeth Aug 8, 2025

grunweg assigned YaelDillies and unassigned hrmacbeth Aug 11, 2025

Merge branch 'master' into enorm-pseudo

81da09d

grunweg added 3 commits August 12, 2025 14:09

Reduce diff

2646a8d

Comment

22243e8

Move

ea37f7e

grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 12, 2025

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

YaelDillies approved these changes Aug 12, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 12, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 13, 2025

Merge branch 'master' into enorm-pseudo

1772d24

grunweg added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 14, 2025

Fix

f38e1bb

grunweg removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 14, 2025

sgouezel reviewed Aug 16, 2025

View reviewed changes

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

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 16, 2025

Typo

ff41799

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

mathlib-bors bot changed the title ~~feat: e-seminormed monoid~~ [Merged by Bors] - feat: e-seminormed monoid Aug 16, 2025

mathlib-bors bot closed this Aug 16, 2025

grunweg deleted the enorm-pseudo branch August 16, 2025 18:06

Conversation

grunweg commented Jul 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary ed5dc595cc

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Jul 24, 2025

Uh oh!

grunweg commented Jul 24, 2025

Uh oh!

sgouezel commented Jul 27, 2025

Uh oh!

grunweg commented Jul 29, 2025

Uh oh!

grunweg commented Aug 11, 2025

Uh oh!

grunweg commented Aug 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Aug 12, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Aug 13, 2025

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Aug 16, 2025

Uh oh!

grunweg commented Aug 16, 2025

Uh oh!

mathlib-bors bot commented Aug 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

grunweg commented Jul 23, 2025 •

edited

Loading

github-actions bot commented Jul 23, 2025 •

edited

Loading

grunweg commented Aug 12, 2025 •

edited

Loading