[Merged by Bors] - feat(Data/Real/IsNonarchimedean): add lemmas by mariainesdff · Pull Request #16767 · leanprover-community/mathlib4

mariainesdff · 2024-09-13T14:25:17Z

Used in #15373.

github-actions · 2024-09-13T14:26:00Z

PR summary 94efc3eb2a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Order.Hom.Normed`	947
`Mathlib.Algebra.Order.Hom.Ultra`	949
`Mathlib.Data.Real.IsNonarchimedean`	1212

Declarations diff

+ AddGroupSeminormClass.isUltrametricDist
+ GroupNormClass.toNormedCommGroup
+ GroupNormClass.toNormedCommGroup_norm_eq
+ GroupNormClass.toNormedGroup
+ GroupNormClass.toNormedGroup_norm_eq
+ GroupSeminormClass.toSeminormedCommGroup
+ GroupSeminormClass.toSeminormedCommGroup_norm_eq
+ GroupSeminormClass.toSeminormedGroup
+ GroupSeminormClass.toSeminormedGroup_norm_eq
+ add_eq_max_of_ne
+ add_le
+ add_pow_le
+ exists_norm_finset_prod_le
+ exists_norm_finset_prod_le_of_nonempty
+ exists_norm_multiset_prod_le
+ finset_image_add
+ finset_image_add_of_nonempty
+ multiset_image_add
+ multiset_image_add_of_nonempty
+ nmul_le
+ nsmul_le

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.

Mathlib/Data/Real/IsNonarchimedean.lean

j-loreaux

This looks fine to me.

jcommelin · 2024-10-02T12:54:21Z

Thanks 🎉

bors merge

Used in #15373.

mathlib-bors · 2024-10-02T14:31:55Z

Build failed (retrying...):

Build

Used in #15373.

mathlib-bors · 2024-10-02T14:57:35Z

Build failed:

Build

faenuccio

I left some minor comments.

Mathlib/Data/Real/IsNonarchimedean.lean

faenuccio · 2024-10-07T14:53:26Z

Thanks! @jcommelin I think this is ready to go again, I think you can bors-ify it again.

loefflerd · 2024-10-08T07:03:58Z

I'm afraid that there has been some duplication going on here: many of the lemmas in this PR are essentially identical to lemmas that have been independently added by @pechersky in #14768, see Mathlib.Analysis.Normed.Group.Ultra.

Yakov's spellings are slightly different, because the assumptions are given as [Seminormed{Add}Group X] [IsUltrametricDist X] rather than [IsNonarchimedean (norm : X \to \RR)]. I think we should try to standardize on one spelling rather than doing everything twice.

loefflerd · 2024-10-08T07:15:47Z

Muddying the waters further, we also seem to have NonarchimedeanHomClass and various variants of it. @mariainesdff, since you seem to be the author of those classes and also of this PR, can you comment on how they relate to each other?

mariainesdff · 2024-10-08T09:57:19Z

I'm afraid that there has been some duplication going on here: many of the lemmas in this PR are essentially identical to lemmas that have been independently added by @pechersky in #14768, see Mathlib.Analysis.Normed.Group.Ultra.

Yakov's spellings are slightly different, because the assumptions are given as [Seminormed{Add}Group X] [IsUltrametricDist X] rather than [IsNonarchimedean (norm : X \to \RR)]. I think we should try to standardize on one spelling rather than doing everything twice.

IsUltrametricDist is not enough for my purposes since it assumes that you have some canonical distance function (which in lemmas like IsUltrametricDist.norm_add_le_max would be the one induced by a bundled SeminormedAddGroup structure on your type).

However, I want to be able to make the statement that a (semi)norm is nonarchimedean, since I will be using this in situations in which I need to consider more than one (semi)norm on the same additive group or ring.

It is likely that some of the proofs in Mathlib.Analysis.Normed.Group.Ultra can be refactored to use the proofs from this file, but please consider this being postponed to another PR, so that I can continue PRing the construction of C_p.

…rchimedean

loefflerd · 2024-10-19T15:39:45Z

I've pushed some changes as follows.

I removed 3 of the 4 variations of the lemma constructing ultrametric normed groups from an unbundled norm-like function; everything seems to work fine with just the one, most general version.
I added new lemmas in Analysis/Normed/Group/Ultra for the results about finset / multiset products, copying Maria's proofs pretty much verbatim, and replaced the proofs in Maria's file with references to those results.

I'm going to retract my comment about the normed ring lemma, because it's probably not worth building the infrastructure of conversions between bundled / unbundled ring norms just for this one (very specific) lemma.

There's still room for some cleanup in Analysis/Normed/Group/Ultra, to impose a bit more uniformity between related lemmas (and fill in the missing cases e.g. noncommutative List products); but I know Maria has a lot of stuff queued up behind this, so it's not fair to keep her waiting. I vote we go ahead and merge this PR now.

Maria: are you happy with this plan? If so, please remove the "awaiting author" tag, and I'll put it back on the maintainer-merge queue.

mariainesdff · 2024-10-21T06:09:38Z

Maria: are you happy with this plan? If so, please remove the "awaiting author" tag, and I'll put it back on the maintainer-merge queue.

Sounds good; thank you for your commits. I have removed the tag.

loefflerd · 2024-10-21T06:13:48Z

maintainer merge

github-actions · 2024-10-21T06:14:10Z

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

riccardobrasca · 2024-10-21T06:17:59Z

@pechersky is this good for you?

pechersky · 2024-10-21T10:55:03Z

Agreed entirely with David Loeffler. LGTM.

riccardobrasca · 2024-10-21T11:00:21Z

Thanks!

bors merge

Used in #15373. Co-authored-by: Yakov Pechersky <ffxen158@gmail.com> Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com> Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

mathlib-bors · 2024-10-21T11:01:07Z

Build failed:

Build

riccardobrasca · 2024-10-21T11:03:10Z

Can you please merge master and fix the error?

bors d+

mathlib-bors · 2024-10-21T11:03:14Z

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

…anprover-community/mathlib4 into mariainesdff/isNonarchimedean

riccardobrasca · 2024-10-21T14:36:19Z

Thanks!

bors merge

Used in #15373. Co-authored-by: Yakov Pechersky <ffxen158@gmail.com> Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com> Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

mathlib-bors · 2024-10-21T14:51:58Z

Pull request successfully merged into master.

Build succeeded:

feat(Data/Real/IsNonarchimedean): add lemmas

266d0b3

mariainesdff added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-analysis Analysis (normed *, calculus) labels Sep 13, 2024

add imports

05fb717

mariainesdff mentioned this pull request Sep 13, 2024

[Merged by Bors] - feat(Analysis.Normed.Ring.Seminorm): add SmoothingSeminorm #15373

Closed

6 tasks

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

Ruben-VandeVelde reviewed Sep 13, 2024

View reviewed changes

Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 13, 2024

suggested changes

e2afbeb

mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 16, 2024

j-loreaux approved these changes Sep 25, 2024

View reviewed changes

github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 2, 2024

mathlib-bors bot pushed a commit that referenced this pull request Oct 2, 2024

feat(Data/Real/IsNonarchimedean): add lemmas (#16767)

54d43fd

Used in #15373.

mathlib-bors bot pushed a commit that referenced this pull request Oct 2, 2024

feat(Data/Real/IsNonarchimedean): add lemmas (#16767)

9fdaf88

Used in #15373.

faenuccio reviewed Oct 4, 2024

View reviewed changes

mariainesdff added 2 commits October 4, 2024 13:58

Merge branch 'master' into mariainesdff/isNonarchimedean

8e6dbd2

add import

f75961f

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 Oct 4, 2024

Merge branch 'master' into mariainesdff/isNonarchimedean

9cb404e

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 7, 2024

suggested changes

7048a63

add new lemmas to Ultra.lean

212fd18

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 Oct 18, 2024

Merge remote-tracking branch 'origin/master' into mariainesdff/isNona…

8b73ed9

…rchimedean

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 19, 2024

loefflerd added 3 commits October 19, 2024 17:11

remove duplicate lemmas

120d70c

use normed-group theorems in IsNonarchimedean

c921e51

remove already existing lemma

9ce6902

mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 21, 2024

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 21, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 21, 2024

github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 21, 2024

mariainesdff added 2 commits October 21, 2024 16:20

Merge branch 'master' into mariainesdff/isNonarchimedean

4905229

Merge branch 'mariainesdff/isNonarchimedean' of https://github.com/le…

94efc3e

…anprover-community/mathlib4 into mariainesdff/isNonarchimedean

mathlib-bors bot changed the title ~~feat(Data/Real/IsNonarchimedean): add lemmas~~ [Merged by Bors] - feat(Data/Real/IsNonarchimedean): add lemmas Oct 21, 2024

mathlib-bors bot closed this Oct 21, 2024

mathlib-bors bot deleted the mariainesdff/isNonarchimedean branch October 21, 2024 14:52

Conversation

mariainesdff commented Sep 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 94efc3eb2a

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

jcommelin commented Oct 2, 2024

Uh oh!

mathlib-bors bot commented Oct 2, 2024

Uh oh!

mathlib-bors bot commented Oct 2, 2024

Uh oh!

faenuccio left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

faenuccio commented Oct 7, 2024

Uh oh!

loefflerd commented Oct 8, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

loefflerd commented Oct 8, 2024

Uh oh!

mariainesdff commented Oct 8, 2024

Uh oh!

loefflerd commented Oct 19, 2024

Uh oh!

mariainesdff commented Oct 21, 2024

Uh oh!

loefflerd commented Oct 21, 2024

Uh oh!

github-actions bot commented Oct 21, 2024

Uh oh!

riccardobrasca commented Oct 21, 2024

Uh oh!

pechersky commented Oct 21, 2024

Uh oh!

riccardobrasca commented Oct 21, 2024

Uh oh!

mathlib-bors bot commented Oct 21, 2024

Uh oh!

riccardobrasca commented Oct 21, 2024

Uh oh!

mathlib-bors bot commented Oct 21, 2024

Uh oh!

riccardobrasca commented Oct 21, 2024

Uh oh!

mathlib-bors bot commented Oct 21, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

10 participants

mariainesdff commented Sep 13, 2024 •

edited

Loading

github-actions bot commented Sep 13, 2024 •

edited

Loading

loefflerd commented Oct 8, 2024 •

edited

Loading