[Merged by Bors] - feat(analysis/{normed/group}/seminorm): Hom classes for seminorms #16227

YaelDillies · 2022-08-24T10:01:38Z

Introduce add_group_seminorm_class, group_seminorm_class, seminorm_class, the hom classes of add_group_seminorm, group_seminorm, seminorm.

depends on: [Merged by Bors] - split(analysis/normed/group/seminorm): Split off analysis.seminorm #16152

mathlib-dependent-issues-bot · 2022-08-24T21:36:35Z

This PR/issue depends on:

~~[Merged by Bors] - split(analysis/normed/group/seminorm): Split off analysis.seminorm #16152~~
By Dependent Issues (🤖). Happy coding!

Vierkantor

I think this looks good overall but someone who knows about seminorms should definitely check that nothing weird is happening.

src/analysis/normed/group/seminorm.lean

src/analysis/seminorm.lean

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Vierkantor

Thanks!

bors r+

src/analysis/normed/group/seminorm.lean

Vierkantor · 2022-09-02T09:31:14Z

Sorry, I thought this was already reviewed by someone else.

bors r-

bors d=@eric-wieser

bors · 2022-09-02T09:31:16Z

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

bors · 2022-09-02T09:31:18Z

Canceled.

Vierkantor · 2022-09-02T09:31:52Z

(Please feel free to re-assign to someone else, I just picked the first suggestion by GitHub)

YaelDillies · 2022-09-02T09:38:12Z

I think Eric is still on holidays.

Vierkantor · 2022-09-02T11:16:40Z

(Please feel free to re-assign to someone else, I just picked the first suggestion by GitHub)

:)

mariainesdff · 2022-09-07T11:10:44Z

src/algebra/order/absolute_value.lean

-  map_mul := λ f, f.map_mul' }
+  map_zero := λ f, (f.eq_zero' _).2 rfl }
+
+instance mul_hom_class : mul_hom_class (absolute_value R S) R S :=


As @Vierkantor comments for add_group_seminorm_class.to_zero_hom_class, wouldn't it be good to make coe explicit in this and the following instances?

Agreed, copying the data carrying fields is helpful.

mariainesdff · 2022-09-07T17:52:31Z

Besides my comment above, it looks good to me.

j-loreaux

Despite having very few comments, I have tried to look at this carefully, and it looks good to me.

j-loreaux · 2022-09-08T02:27:56Z

src/algebra/order/hom/basic.lean

+/-- `subadditive_hom_class F α β` states that `F` is a type of subadditive morphisms. -/
+class subadditive_hom_class (F : Type*) (α β : out_param $ Type*) [has_add α] [has_add β] [has_le β]
+  extends fun_like F α (λ _, β) :=
+(map_add_le_add (f : F) : ∀ a b, f (a + b) ≤ f a + f b)


This is just bikeshedding, but I think it's reasonable to shorten this to map_add_le.

Suggested change

(map_add_le_add (f : F) : ∀ a b, f (a + b) ≤ f a + f b)

(map_add_le (f : F) : ∀ a b, f (a + b) ≤ f a + f b)

I kept them long to avoid ambiguity with map_mul_le_add (and the eventual map_add_le_max and such).

Feel free to shorten them if we see that no ambiguity arises over time.

bors merge

j-loreaux · 2022-09-08T02:28:14Z

src/algebra/order/hom/basic.lean

+@[to_additive subadditive_hom_class]
+class submultiplicative_hom_class (F : Type*) (α β : out_param $ Type*) [has_mul α] [has_mul β]
+  [has_le β] extends fun_like F α (λ _, β) :=
+(map_mul_le_mul (f : F) : ∀ a b, f (a * b) ≤ f a * f b)


Same here

Suggested change

(map_mul_le_mul (f : F) : ∀ a b, f (a * b) ≤ f a * f b)

(map_mul_le (f : F) : ∀ a b, f (a * b) ≤ f a * f b)

jcommelin · 2022-09-09T12:03:21Z

Thanks, LGTM

bors d+

bors · 2022-09-09T12:03:23Z

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

…6227) Introduce `add_group_seminorm_class`, `group_seminorm_class`, `seminorm_class`, the hom classes of `add_group_seminorm`, `group_seminorm`, `seminorm`.

bors · 2022-09-09T14:44:20Z

Pull request successfully merged into master.

Build succeeded:

…6227) Introduce `add_group_seminorm_class`, `group_seminorm_class`, `seminorm_class`, the hom classes of `add_group_seminorm`, `group_seminorm`, `seminorm`.

YaelDillies added 5 commits August 19, 2022 12:49

initial commit

630b562

kill nonneg'

58edc47

typos

814520a

fix analysis.seminorm

0b40898

seminorm classes

8bc92fc

YaelDillies added awaiting-review The author would like community review of the PR t-analysis Analysis (normed *, calculus) labels Aug 24, 2022

YaelDillies requested a review from mariainesdff August 24, 2022 10:01

YaelDillies mentioned this pull request Aug 24, 2022

[Merged by Bors] - feat(algebra/order/hom/basic): positivity extension for nonnegative homs #16228

Closed

1 task

mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 24, 2022

nolint

9c5fd52

YaelDillies mentioned this pull request Aug 24, 2022

[Merged by Bors] - feat(analysis/normed/group/seminorm): Group norms #16237

Closed

1 task

mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 24, 2022

Merge branch 'master' into seminorm_class

ded1da7

YaelDillies requested a review from Vierkantor August 24, 2022 21:50

Vierkantor self-assigned this Aug 30, 2022

Vierkantor reviewed Aug 30, 2022

View reviewed changes

src/analysis/normed/group/seminorm.lean Show resolved Hide resolved

src/analysis/normed/group/seminorm.lean Show resolved Hide resolved

src/analysis/seminorm.lean Show resolved Hide resolved

Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Aug 30, 2022

Vierkantor requested a review from eric-wieser August 30, 2022 10:36

copy coe over

347e229

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 30, 2022

YaelDillies added 3 commits August 31, 2022 15:55

Merge remote-tracking branch 'origin/master' into seminorm_class

a295508

algebra order hom classes

5df80ed

fix analysis.seminorm

c4e5397

YaelDillies mentioned this pull request Sep 1, 2022

chore(*): remove is_absolute_value #16340

Closed

1 task

fix analysis.convex.gauge

5e9be75

Vierkantor approved these changes Sep 2, 2022

View reviewed changes

src/analysis/normed/group/seminorm.lean Show resolved Hide resolved

leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 2, 2022

Vierkantor added delegated The PR author may merge after reviewing final suggestions. and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Sep 2, 2022

Vierkantor removed their assignment Sep 2, 2022

YaelDillies requested review from j-loreaux and ericrbg September 2, 2022 11:58

ericrbg added the awaiting-review The author would like community review of the PR label Sep 4, 2022

mariainesdff mentioned this pull request Sep 7, 2022

[Merged by Bors] - feat(analysis/normed/ring/seminorm): add ring_seminorm, ring_norm #14115

Closed

mariainesdff reviewed Sep 7, 2022

View reviewed changes

j-loreaux approved these changes Sep 8, 2022

View reviewed changes

github-actions bot removed the awaiting-review The author would like community review of the PR label Sep 9, 2022

bors bot changed the title ~~feat(analysis/{normed/group}/seminorm): Hom classes for seminorms~~ [Merged by Bors] - feat(analysis/{normed/group}/seminorm): Hom classes for seminorms Sep 9, 2022

bors bot closed this Sep 9, 2022

bors bot deleted the seminorm_class branch September 9, 2022 14:44

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(analysis/{normed/group}/seminorm): Hom classes for seminorms #16227

[Merged by Bors] - feat(analysis/{normed/group}/seminorm): Hom classes for seminorms #16227

YaelDillies commented Aug 24, 2022 •

edited by github-actions bot

mathlib-dependent-issues-bot commented Aug 24, 2022

Vierkantor left a comment

Vierkantor left a comment

Vierkantor commented Sep 2, 2022

bors bot commented Sep 2, 2022

bors bot commented Sep 2, 2022

Vierkantor commented Sep 2, 2022

YaelDillies commented Sep 2, 2022

Vierkantor commented Sep 2, 2022

mariainesdff Sep 7, 2022 •

edited

j-loreaux Sep 8, 2022

mariainesdff commented Sep 7, 2022

j-loreaux left a comment

j-loreaux Sep 8, 2022

YaelDillies Sep 9, 2022

YaelDillies Sep 9, 2022

j-loreaux Sep 8, 2022

jcommelin commented Sep 9, 2022

bors bot commented Sep 9, 2022

bors bot commented Sep 9, 2022

	(map_add_le_add (f : F) : ∀ a b, f (a + b) ≤ f a + f b)
	(map_add_le (f : F) : ∀ a b, f (a + b) ≤ f a + f b)

	(map_mul_le_mul (f : F) : ∀ a b, f (a * b) ≤ f a * f b)
	(map_mul_le (f : F) : ∀ a b, f (a * b) ≤ f a * f b)

[Merged by Bors] - feat(analysis/{normed/group}/seminorm): Hom classes for seminorms #16227

[Merged by Bors] - feat(analysis/{normed/group}/seminorm): Hom classes for seminorms #16227

Conversation

YaelDillies commented Aug 24, 2022 • edited by github-actions bot

mathlib-dependent-issues-bot commented Aug 24, 2022

Vierkantor left a comment

Choose a reason for hiding this comment

Vierkantor left a comment

Choose a reason for hiding this comment

Vierkantor commented Sep 2, 2022

bors bot commented Sep 2, 2022

bors bot commented Sep 2, 2022

Vierkantor commented Sep 2, 2022

YaelDillies commented Sep 2, 2022

Vierkantor commented Sep 2, 2022

mariainesdff Sep 7, 2022 • edited

Choose a reason for hiding this comment

j-loreaux Sep 8, 2022

Choose a reason for hiding this comment

mariainesdff commented Sep 7, 2022

j-loreaux left a comment

Choose a reason for hiding this comment

j-loreaux Sep 8, 2022

Choose a reason for hiding this comment

YaelDillies Sep 9, 2022

Choose a reason for hiding this comment

YaelDillies Sep 9, 2022

Choose a reason for hiding this comment

j-loreaux Sep 8, 2022

Choose a reason for hiding this comment

jcommelin commented Sep 9, 2022

bors bot commented Sep 9, 2022

bors bot commented Sep 9, 2022

YaelDillies commented Aug 24, 2022 •

edited by github-actions bot

mariainesdff Sep 7, 2022 •

edited