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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(analysis/seminorm): define the Minkowski functional #9097

Closed
wants to merge 29 commits into from
Closed

[Merged by Bors] - feat(analysis/seminorm): define the Minkowski functional #9097

wants to merge 29 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Sep 8, 2021 •
edited by alexjbest
Loading

This defines the gauge of a set, aka the Minkowski functional, in a vector space over a real normed field.

Co-authored-by: bhavikmehta8@gmail.com

Open in Gitpod

@YaelDillies YaelDillies added the WIP Work in progress label Sep 8, 2021
@github-actions github-actions 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 Sep 8, 2021
@YaelDillies YaelDillies mentioned this pull request Sep 8, 2021
Closed
8 tasks
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Sep 9, 2021
@YaelDillies YaelDillies changed the title feat(analysis/seminorm): define the Minkowksi functional feat(analysis/seminorm): define the Minkowski functional Sep 9, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 19, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 21, 2021
@jcommelin
Copy link
Member

CI is failing.

@jcommelin jcommelin 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 Sep 30, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 13, 2021
@github-actions github-actions bot removed merge-conflict Please `git merge origin/master` then a bot will remove this label. blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Oct 13, 2021
@jcommelin jcommelin removed the needs-documentation This PR is missing required documentation label Oct 27, 2021
ocfnash
ocfnash reviewed Oct 27, 2021
View reviewed changes
src/analysis/seminorm.lean Outdated Show resolved Hide resolved
jcommelin
jcommelin reviewed Nov 1, 2021
View reviewed changes
src/analysis/seminorm.lean Outdated Show resolved Hide resolved
src/analysis/seminorm.lean Outdated Show resolved Hide resolved
src/analysis/seminorm.lean Outdated Show resolved Hide resolved
src/analysis/seminorm.lean Outdated Show resolved Hide resolved
@YaelDillies
Copy link
Collaborator Author

This file earned a nice docstring! It also tripled in size, so if you want me to move to a new file, I'm fine with that.

@YaelDillies 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 Nov 1, 2021
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@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 Nov 2, 2021
bors bot pushed a commit that referenced this pull request Nov 2, 2021
@YaelDillies
feat(analysis/seminorm): define the Minkowski functional (#9097)
c36edd2 
This defines the gauge of a set, aka the Minkowski functional, in a vector space over a real normed field.
@bors
Copy link

bors bot commented Nov 2, 2021

Build failed:

@jcommelin
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Nov 2, 2021

✌️ 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.

@github-actions github-actions bot added the delegated The PR author may merge after reviewing final suggestions. label Nov 2, 2021
@YaelDillies
Merge remote-tracking branch 'origin/master' into gauge
3b0025b
@YaelDillies
remove Yury-sniped lemma :)
fb24b81 
Love it when your lemma is being PRed simultaneously from another branch.
@YaelDillies
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Nov 3, 2021
@YaelDillies
feat(analysis/seminorm): define the Minkowski functional (#9097)
4f033b7 
This defines the gauge of a set, aka the Minkowski functional, in a vector space over a real normed field.

Co-authored-by: <bhavikmehta8@gmail.com>
@bors
Copy link

bors bot commented Nov 3, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/seminorm): define the Minkowski functional [Merged by Bors] - feat(analysis/seminorm): define the Minkowski functional Nov 3, 2021
@bors bors bot closed this Nov 3, 2021
@bors bors bot deleted the gauge branch November 3, 2021 16:45
ericrbg pushed a commit that referenced this pull request Nov 9, 2021
@YaelDillies @ericrbg
feat(analysis/seminorm): define the Minkowski functional (#9097)
817d24d 
This defines the gauge of a set, aka the Minkowski functional, in a vector space over a real normed field.

Co-authored-by: <bhavikmehta8@gmail.com>
@YaelDillies YaelDillies mentioned this pull request Mar 12, 2022
Closed
bors bot pushed a commit that referenced this pull request Mar 12, 2022
@YaelDillies
split(analysis/locally_convex/basic): Split off analysis.seminorm (#…
b21c1c9 
…12624)

Move `balanced`, `absorbs`, `absorbent` to a new file.

For `analysis.seminorm`, I'm crediting
* Jean for #4827
* myself for
  * #9097
  * #11487
* Moritz for
  * #11329
  * #11414
  * #11477

For `analysis.locally_convex.basic`, I'm crediting
* Jean for #4827
* Bhavik for
  * #7358
  * #9097
* myself for
  * #9097
  * #10999
  * #11487
laurentbartholdi pushed a commit that referenced this pull request Mar 17, 2022
@YaelDillies @laurentbartholdi
split(analysis/locally_convex/basic): Split off analysis.seminorm (#…
4401087 
…12624)

Move `balanced`, `absorbs`, `absorbent` to a new file.

For `analysis.seminorm`, I'm crediting
* Jean for #4827
* myself for
  * #9097
  * #11487
* Moritz for
  * #11329
  * #11414
  * #11477

For `analysis.locally_convex.basic`, I'm crediting
* Jean for #4827
* Bhavik for
  * #7358
  * #9097
* myself for
  * #9097
  * #10999
  * #11487
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@RemyDegenne RemyDegenne RemyDegenne left review comments

@jcommelin jcommelin jcommelin left review comments

@ocfnash ocfnash ocfnash left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@YaelDillies @jcommelin @urkud @RemyDegenne @ocfnash