[Merged by Bors] - feat(archive/imo): formalize IMO 2013 problem Q5 #5787
Conversation
archive/imo/imo2013_q5.lean
Outdated
| exact le_of_all_pow_lt_succ x y hx hy' h | ||
| end | ||
|
|
||
| lemma power_bound (n: ℕ) (ε:ℚ) (ha: 0 < ε) : 1 + (n:ℚ) * ε ≤ (1 + ε)^n := |
There was a problem hiding this comment.
This seems like a more generally useful lemma that belongs in mathlib proper. Not in the specific form with ℚ and ℕ, but in various forms with the exponent being from any one of ℕ, ℤ or ℝ (in the first two cases you can probably prove something for powers of numbers in some kind of ordered semiring / ordered field) and whatever the weakest inequalities on the arguments are for the result to be true.
There was a problem hiding this comment.
I agree that this could be generally useful. I've pushed a commit that generalizes ℚ to linear_ordered_comm_ring, and I've added a TODO about moving it into mathlib proper. I don't know about generalizing the exponent -- that sounds like it might make things a bit more complicated.
There was a problem hiding this comment.
I know this result as Bernoulli's inequality, and I see that there is one version two versions in mathlib already:
https://leanprover-community.github.io/mathlib_docs/algebra/group_power/lemmas.html#one_add_mul_le_pow
https://leanprover-community.github.io/mathlib_docs/algebra/group_power/lemmas.html#one_add_mul_le_pow'
There was a problem hiding this comment.
Ah, and actually one_add_sub_mul_le_pow is even closer to what I need. Thanks!
dwrensha
added
the
awaiting-review
|
@bryangingechen Thanks for the review. I've cleaned up the formatting and split out some lemmas. |
|
@dwrensha I did some more golfing / formatting. If you're happy with my changes, feel free to merge. Thanks! |
|
✌️ dwrensha can now approve this pull request. To approve and merge a pull request, simply reply with |
bryangingechen
added
awaiting-author
|
bors r+ |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
(reopening #5786 from a non-fork branch)
This ended up getting rather long. I'm willing to work some more on golfing it down, especially if an expert can provide some hints.