leanprover-community
feat(analysis/special_functions/pow): Add Bernoulli's Inequalities
If -1 < x and 0 ≤ r ≤ 1, then (1 + x)^r ≤ 1 + r * x, and if -1 < x and 1 ≤ r, then 1 + r * x ≤ (1 + x)^r.
Can these be phrased for ordered rings? See the similar lemmas in algebra.group_power.basic, such as one_add_mul_le_pow'.
Can these be phrased for ordered rings? See the similar lemmas in
algebra.group_power.basic, such asone_add_mul_le_pow'.
The statement in one_add_mul_le_pow' is for a natural number exponent, but the statement in this PR has a real exponent, so I don't think I can phrase this for ordered rings. I think a weaker statement holds in ordered rings/fields with natural/integer exponents?
The statement in
one_add_mul_le_pow'is for a natural number exponent, but the statement in this PR has a real exponent, so I don't think I can phrase this for ordered rings.
Ah, I see! But in this generality, perhaps we want the fact that a convex function is bounded below by the tangent line at any point. That is effectively what you are proving, right? You may find that the four main proofs (which all use exists_deriv_eq_slope as their main ingredient) are unified by this point of view.
I think proving that a convex/concave function is bounded by its tangent lines would be useful for more than just this, so I will have a look at that. My current proof doesn't explicitly use convexity, but it is probably equivalent.
Do you need these results for something in particular? I don't want to send you on a long digression if this is blocking something else.
But if you are simply trying to make a useful contribution to the library, it would be very nice to have this result. I think you can state it in arbitrary dimension, and you need only convexity plus differentiability at the point under consideration. The argument is that in a given direction v, the function (f (x + tv) - f x) / t is nonincreasing, so if the derivative exists then it's its infimum. Some notes -- see Proposition 3.3.2, Proposition 3.4.1 (iii).
(With this result you won't directly need the mean value theorem exists_deriv_eq_slope to get Bernoulli -- instead its use will be packaged inside the fact that ^ is convex, convex_on_rpow.)
@urkud has worked a lot on convexity, if he has time he will be able to give you more precise advice as to the formulation and approach.
Do you need these results for something in particular? I don't want to send you on a long digression if this is blocking something else.
It's not blocking anything for me personally, I am PRing this as this came up as something that might be useful for @jamesa9283 for proving something (I think it's Lemma 5.3 on Analytic.pdf?).
I will have a look at the document you've linked. Thanks!
It's not blocking anything for me personally, I am PRing this as this came up as something that might be useful for @jamesa9283 for proving something (I think it's Lemma 5.3 on Analytic.pdf?).
I was working on Lemma 5.3 from here: https://www.math.uni-bonn.de/people/scholze/Analytic.pdf and I used it for a case of the second part.
Note that the weighted mean inequality applied to w₁=r, w₂=1-r, p₁=(1+x)^r, p₂=1 gives one version of this inequality, and other versions follow by change of variables.
