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/specific_functions): elementary convexity proofs #19026
Conversation
Maybe add some comments to the lemmas where you give an elementary proof instead of the second derivative test, explaining that we use an elementary proof for import reasons? |
have hxy' : 0 < y - x := by linarith, | ||
have hxz' : 0 < z - x := by linarith, |
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 assume you're deliberately avoiding
have hxy' : 0 < y - x := by linarith, | |
have hxz' : 0 < z - x := by linarith, | |
have hxy' : 0 < y - x := sub_pos_of_lt hxy, | |
have hxz' : 0 < z - x := sub_pos_of_lt (hxy.trans hyz), |
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 prefer the automation, someday I will write a linear_combination_for_inequalities
which is fast but avoids calling the lemmas by name ...
bors merge |
…#19026) Give elementary proofs for the convexity of `pow`, `zpow`, `exp`, `log` and `rpow`, avoiding the second derivative test. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Shortcut.20to.20integration)
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Split `analysis/convex/specific_function` into a part which doesn't require differentiation (as of #19026) and a part which does. This removes the dependence of `measure_theory/integral/bochner` on differentiation, and decreases by 11 the length of the longest path in mathlib. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Shortcut.20to.20integration)
Split `analysis/convex/specific_function` into a part which doesn't require differentiation (as of #19026) and a part which does. This removes the dependence of `measure_theory/integral/bochner` on differentiation, and decreases by 11 the length of the longest path in mathlib. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Shortcut.20to.20integration) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Fiddly, not done yet ... help welcome. Cross-reference: leanprover-community/mathlib#19026. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Fiddly, not done yet ... help welcome. Cross-reference: leanprover-community/mathlib#19026. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Give elementary proofs for the convexity of
pow
,zpow
,exp
,log
andrpow
, avoiding the second derivative test.See Zulip