-
Notifications
You must be signed in to change notification settings - Fork 299
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): log is concave #5508
Conversation
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.
Thanks for this!
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
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.
more of the same :)
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
…ncave' into dupuisf_log_is_concave
✌️ dupuisf can now approve this pull request. To approve and merge a pull request, simply reply with |
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.
Couple more things, also could you mention concave_on_log_Ioi
and friend in the module docstring of convex.specific_functions
?
Apart from this, looks good!
bors d+
{ intros x hx, | ||
rw [function.iterate_succ, function.iterate_one], | ||
change (deriv (deriv log)) x ≤ 0, | ||
rw [deriv_log', deriv_inv (show x ≠ 0, by {rintro rfl, exact lt_irrefl 0 hx})], | ||
exact neg_nonpos.mpr (inv_nonneg.mpr (pow_two_nonneg x)) } |
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 just wrote a quick PR #5521, which will let this be simplified to
{ intros x hx,
simp [function.iterate_succ, function.iterate_one, pow_two_nonneg] }
Let's not hold your PR up for this though.
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.
Nice!
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
…ncave' into dupuisf_log_is_concave
bors r+ |
This PR proves that the real log is concave on `Ioi 0` and `Iio 0`, and adds lemmas about concavity of functions along the way. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
This PR proves that the real log is concave on
Ioi 0
andIio 0
, and adds lemmas about concavity of functions along the way.