Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(analysis/convex): the gauge as a seminorm over is_R_or_C #14879

Closed
wants to merge 12 commits into from

Conversation

mcdoll
Copy link
Member

@mcdoll mcdoll commented Jun 21, 2022

Constructs the gauge for a set on a vector spaces over is_R_or_C assuming that the set is convex, balanced and absorbing.

The main part of this PR is to show that if a set is balanced then the corresponding gauge has the correct scaling behavior.

Co-authored-by: Yaël Dillies yael.dillies@gmail.com


Open in Gitpod

@mcdoll mcdoll added WIP Work in progress awaiting-CI The author would like to see what CI has to say before doing more work. labels Jun 21, 2022
@mcdoll mcdoll removed the WIP Work in progress label Jun 21, 2022
@mathlib-dependent-issues-bot 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 Jun 21, 2022
@mathlib-dependent-issues-bot 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 Jul 9, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

@mcdoll mcdoll added the awaiting-review The author would like community review of the PR label Jul 9, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 9, 2022
src/analysis/convex/gauge.lean Show resolved Hide resolved
src/data/complex/is_R_or_C.lean Outdated Show resolved Hide resolved
@mcdoll mcdoll added the t-analysis Analysis (normed *, calculus) label Jul 24, 2022
@dupuisf
Copy link
Collaborator

dupuisf commented Aug 9, 2022

Looks good!

bors r+

@github-actions github-actions bot 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 Aug 9, 2022
bors bot pushed a commit that referenced this pull request Aug 9, 2022
Constructs the gauge for a set on a vector spaces over `is_R_or_C` assuming that the set is convex, balanced and absorbing.

The main part of this PR is to show that if a set is balanced then the corresponding gauge has the correct scaling behavior.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>



Co-authored-by: YaelDillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Moritz Doll <doll@uni-bremen.de>
@bors
Copy link

bors bot commented Aug 9, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/convex): the gauge as a seminorm over is_R_or_C [Merged by Bors] - feat(analysis/convex): the gauge as a seminorm over is_R_or_C Aug 9, 2022
@bors bors bot closed this Aug 9, 2022
@bors bors bot deleted the mcdoll/gauge_complex branch August 9, 2022 11:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-analysis Analysis (normed *, calculus)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants