-
Notifications
You must be signed in to change notification settings - Fork 297
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/function): helper lemmas and general cleanup #9438
Conversation
Can you summarize what the generalizations to the instances are in the PR description? |
src/analysis/convex/basic.lean
Outdated
@@ -423,6 +423,21 @@ begin | |||
exact h hx hy ha hb hab | |||
end | |||
|
|||
lemma convex_iff_forall_pos_ne : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there any point keeping convex_iff_forall_pos
around? Either you need the strong forward direction, which is just rw convex
, or you need the strong backwards direction, which is rw <-convex_iff_forall_pos_ne
. I think having an intermediate strength version is unecessary.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it's fine to keep? We can nuke it later if we want to.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Thanks π bors d+ (Please merge after updating the PR description following Eric's remark.) |
βοΈ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
) This adds * `convex_iff_pairwise_on_pos` * `convex_on_iff_forall_pos`, `concave_on_iff_forall_pos`, * `convex_on_iff_forall_pos_ne`, `concave_on_iff_forall_pos_ne` * `convex_on.convex_strict_epigraph`, `concave_on.convex_strict_hypograph` generalizes some instance assumptions: * `convex_on.translate_` didn't need `module π Ξ²` but `has_scalar π Ξ²`. * some proofs in `analysis.convex.exposed` were vestigially using `β`. and golfs proofs.
Build failed (retrying...): |
) This adds * `convex_iff_pairwise_on_pos` * `convex_on_iff_forall_pos`, `concave_on_iff_forall_pos`, * `convex_on_iff_forall_pos_ne`, `concave_on_iff_forall_pos_ne` * `convex_on.convex_strict_epigraph`, `concave_on.convex_strict_hypograph` generalizes some instance assumptions: * `convex_on.translate_` didn't need `module π Ξ²` but `has_scalar π Ξ²`. * some proofs in `analysis.convex.exposed` were vestigially using `β`. and golfs proofs.
Build failed (retrying...): |
) This adds * `convex_iff_pairwise_on_pos` * `convex_on_iff_forall_pos`, `concave_on_iff_forall_pos`, * `convex_on_iff_forall_pos_ne`, `concave_on_iff_forall_pos_ne` * `convex_on.convex_strict_epigraph`, `concave_on.convex_strict_hypograph` generalizes some instance assumptions: * `convex_on.translate_` didn't need `module π Ξ²` but `has_scalar π Ξ²`. * some proofs in `analysis.convex.exposed` were vestigially using `β`. and golfs proofs.
Build failed (retrying...): |
bors r- |
βοΈ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Canceled. |
bors merge |
) This adds * `convex_iff_pairwise_on_pos` * `convex_on_iff_forall_pos`, `concave_on_iff_forall_pos`, * `convex_on_iff_forall_pos_ne`, `concave_on_iff_forall_pos_ne` * `convex_on.convex_strict_epigraph`, `concave_on.convex_strict_hypograph` generalizes some instance assumptions: * `convex_on.translate_` didn't need `module π Ξ²` but `has_scalar π Ξ²`. * some proofs in `analysis.convex.exposed` were vestigially using `β`. and golfs proofs.
Build failed (retrying...): |
) This adds * `convex_iff_pairwise_on_pos` * `convex_on_iff_forall_pos`, `concave_on_iff_forall_pos`, * `convex_on_iff_forall_pos_ne`, `concave_on_iff_forall_pos_ne` * `convex_on.convex_strict_epigraph`, `concave_on.convex_strict_hypograph` generalizes some instance assumptions: * `convex_on.translate_` didn't need `module π Ξ²` but `has_scalar π Ξ²`. * some proofs in `analysis.convex.exposed` were vestigially using `β`. and golfs proofs.
Pull request successfully merged into master. Build succeeded: |
This adds
convex_iff_pairwise_on_pos
convex_on_iff_forall_pos
,concave_on_iff_forall_pos
,convex_on_iff_forall_pos_ne
,concave_on_iff_forall_pos_ne
convex_on.convex_strict_epigraph
,concave_on.convex_strict_hypograph
generalizes some instance assumptions:
convex_on.translate_
didn't needmodule π Ξ²
buthas_scalar π Ξ²
.analysis.convex.exposed
were vestigially usingβ
.and golfs proofs.
This is preparatory work for #9437.