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/convex/cone): add inner_dual_cone_of_inner_dual_cone_eq_self for nonempty, closed, convex cones #15637

Closed
wants to merge 36 commits into from
Closed

[Merged by Bors] - feat(analysis/convex/cone): add inner_dual_cone_of_inner_dual_cone_eq_self for nonempty, closed, convex cones #15637

wants to merge 36 commits into from

Conversation

apurvnakade
Copy link
Collaborator

@apurvnakade apurvnakade commented Jul 23, 2022 •
edited
Loading

We add the following results about convex cones:

  • instance has_zero
  • inner_dual_cone_zero
  • inner_dual_cone_univ
  • pointed_of_nonempty_of_is_closed
  • hyperplane_separation_of_nonempty_of_is_closed_of_nmem
  • inner_dual_cone_of_inner_dual_cone_eq_self

References:

Open in Gitpod

@apurvnakade apurvnakade added the WIP Work in progress label Jul 23, 2022
@apurvnakade apurvnakade mentioned this pull request Jul 23, 2022
Closed
@urkud urkud added the t-analysis Analysis (normed *, calculus) label Jul 24, 2022
bors bot pushed a commit that referenced this pull request Jul 27, 2022
@apurvnakade
feat(analysis/convex/cone): add inner_dual_cone_eq_Inter_inner_dual_c…
23c3981 
…one_singleton (#15639)

Proof that a dual cone equals the intersection of dual cones of singleton sets.
Part of #15637
@apurvnakade apurvnakade mentioned this pull request Jul 30, 2022
Closed
2 tasks
bottine pushed a commit to bottine/mathlib that referenced this pull request Jul 30, 2022
@apurvnakade @bottine
feat(analysis/convex/cone): add inner_dual_cone_eq_Inter_inner_dual_c…
99b5b5c 
…one_singleton (leanprover-community#15639)

Proof that a dual cone equals the intersection of dual cones of singleton sets.
Part of leanprover-community#15637
robertylewis pushed a commit that referenced this pull request Aug 2, 2022
@apurvnakade @robertylewis
feat(analysis/convex/cone): add inner_dual_cone_eq_Inter_inner_dual_c…
b1f6b86 
…one_singleton (#15639)

Proof that a dual cone equals the intersection of dual cones of singleton sets.
Part of #15637
khwilson pushed a commit that referenced this pull request Aug 2, 2022
@apurvnakade @khwilson
feat(analysis/convex/cone): add inner_dual_cone_eq_Inter_inner_dual_c…
8f8d676 
…one_singleton (#15639)

Proof that a dual cone equals the intersection of dual cones of singleton sets.
Part of #15637
@apurvnakade @eric-wieser
Apply suggestions from code review
4dbccad 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@apurvnakade apurvnakade 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 10, 2022
@apurvnakade
Copy link
Collaborator Author

apurvnakade commented Aug 10, 2022 •
edited
Loading

TODO: I still need to add docstrings to these theorems and merge the previous branches.

@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 Aug 10, 2022
@apurvnakade apurvnakade 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 10, 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 Aug 10, 2022
bors bot pushed a commit that referenced this pull request Aug 10, 2022
@apurvnakade @eric-wieser
feat(analysis/convex/cone): dual of a convex cone is closed (#15766)
fb16dbc 
We prove that the dual of a convex cone is always closed.
Part of #15637



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@ocfnash
Copy link
Collaborator

ocfnash commented Aug 24, 2022

Thanks! Please apply my suggestions and then feel free to merge.

bors d+

@bors
Copy link

bors bot commented Aug 24, 2022

✌️ apurvnakade 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 delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Aug 24, 2022
@ocfnash
Copy link
Collaborator

ocfnash commented Aug 24, 2022

Please also update the PR description: it seems to be out of date.

@apurvnakade @ocfnash
Apply suggestions from code review
c4aa401 
Co-authored-by: Oliver Nash <github@olivernash.org>
@apurvnakade apurvnakade added the awaiting-CI The author would like to see what CI has to say before doing more work. label Aug 24, 2022
@apurvnakade apurvnakade changed the title feat(analysis/convex/cone): dual_of_dual_eq_self feat(analysis/convex/cone): add inner_dual_cone_of_inner_dual_cone_eq_self for nonempty, closed, convex cones Aug 24, 2022
@apurvnakade @eric-wieser
Apply suggestions from code review
dc1f473 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@apurvnakade @ocfnash
Apply suggestions from code review
652cd76 
Co-authored-by: Oliver Nash <github@olivernash.org>
@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 Aug 24, 2022
@apurvnakade
Copy link
Collaborator Author

Bors merge

bors bot pushed a commit that referenced this pull request Aug 25, 2022
@apurvnakade
feat(analysis/convex/cone): add `inner_dual_cone_of_inner_dual_cone_e…
42d6407 
…q_self` for nonempty, closed, convex cones (#15637)

We add the following results about convex cones:
- instance `has_zero`
- `inner_dual_cone_zero`
- `inner_dual_cone_univ`
- `pointed_of_nonempty_of_is_closed`
- `hyperplane_separation_of_nonempty_of_is_closed_of_nmem`
- `inner_dual_cone_of_inner_dual_cone_eq_self`

References: 
- https://ti.inf.ethz.ch/ew/lehre/ApproxSDP09/notes/conelp.pdf
- Stephen P. Boyd and Lieven Vandenberghe. Convex Optimization. Cambridge University Press.
  ISBN 978-0-521-83378-3. available at https://web.stanford.edu/~boyd/cvxbook/bv_cvxbook.pdf
@bors
Copy link

bors bot commented Aug 25, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/convex/cone): add inner_dual_cone_of_inner_dual_cone_eq_self for nonempty, closed, convex cones [Merged by Bors] - feat(analysis/convex/cone): add inner_dual_cone_of_inner_dual_cone_eq_self for nonempty, closed, convex cones Aug 25, 2022
@bors bors bot closed this Aug 25, 2022
@bors bors bot deleted the apurva/dual-of-dual branch August 25, 2022 05:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@ocfnash ocfnash ocfnash left review comments

@mcdoll mcdoll mcdoll approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@apurvnakade @ocfnash @eric-wieser @mcdoll @urkud @mathlib-dependent-issues-bot