Stream: math-comp users

Topic: monotonicity of (n/(n+1))^(n+1)


view this post on Zulip Christian Doczkal (Sep 07 2021 at 08:48):

In one of my proofs I make use of the fact that the sequence (n/(n+1))(n+1) (n/(n+1))^{(n+1)} is monotonically increasing for n1 n \geq 1 . The only "proof" I found so far is to generalize to a function over the real numbers, and then show that the derivative, WolframAlpha gives

ddn((nn+1)n+1)=(nn+1)n(nlog(nn+1)+1))n+1\frac d {dn} \left( \left( \frac n {n+1} \right)^{n+1} \right) = \frac {\left( \frac n {n + 1} \right)^n (n \log \left(\frac n {n + 1} \right) + 1))}{n + 1}

is strictly positive. Thus, is suffices to show nlog(nn+1)+1>0 n \log \left(\frac n {n + 1} \right) + 1 > 0 for n1 n \geq 1 . The value at 1 is positive (~0.3) and the limit for n n \to \infty is 0, so it should suffice to prove that its derivative

ddn(nlog(nn+1)+1)=nn+1+log(nn+1)\frac d {dn} \left( n \log \left(\frac n {n + 1} \right) + 1 \right) = \frac n {n+1} + \log \left( \frac n {n +1} \right)

is strictly negative. This follows by (again) exploiting that the limit is still 0, the value at 1 negative, and the derivative strictly positive.

Now I wonder how hard it would be to formalize this argument using mathcomp (or mathcomp analysis), assuming the argument is actually sound.

view this post on Zulip Pierre Roux (Sep 07 2021 at 09:41):

I don't know but here is a tentative proof without having to resort on analysis (just need rational numbers):
for all n >= 1:

(n+1)2n(n+2)>1\frac{(n+1)^2}{n(n+2)} > 1

hence

n+1n(n+2)>1n+1\frac{n+1}{n(n+2)} > \frac{1}{n+1}

hence

1+n+1n(n+2)>1+1n+11+\frac{n+1}{n(n+2)} > 1+\frac{1}{n+1}

hence

((n+1)2n(n+2))n+1=(1+1n(n+2))n+1>1+1n+1=n+2n+1\left(\frac{(n+1)^2}{n(n+2)}\right)^{n+1}= \left(1 + \frac{1}{n(n+2)}\right)^{n+1} > 1 + \frac{1}{n+1} = \frac{n+2}{n+1}

because

(1+1n(n+2))n+11n+1+(n+11)1n1n(n+2)\left(1+\frac{1}{n(n+2)}\right)^{n+1} \geq 1^{n+1} + \left(\begin{matrix}n+1\\1\end{matrix}\right)1^n\frac{1}{n(n+2)}

thus

((n+1)2n(n+2))n+1n+1n+2>1\left(\frac{(n+1)^2}{n(n+2)}\right)^{n+1}\frac{n+1}{n+2} > 1

hence

(nn+1)n+1(((n+1)2n(n+2))n+1n+1n+21)>0\left(\frac{n}{n+1}\right)^{n+1}\left(\left(\frac{(n+1)^2}{n(n+2)}\right)^{n+1}\frac{n+1}{n+2} - 1\right) > 0

hence finally

(n+1n+2)n+2(nn+1)n+1>0\left(\frac{n+1}{n+2}\right)^{n+2} - \left(\frac{n}{n+1}\right)^{n+1} > 0

view this post on Zulip Cyril Cohen (Sep 07 2021 at 10:00):

I was going to suggest a similar proof but concluding with (n+1n+2)n+2(nn+1)n+1>1\frac{\left(\frac{n+1}{n+2}\right)^{n+2}}{\left(\frac{n}{n+1}\right)^{n+1}} > 1

view this post on Zulip Cyril Cohen (Sep 07 2021 at 10:11):

That being said, the analytic proof is arguably more elegant, and I think it would be not so hard to reproduce with mathcomp analysis.

view this post on Zulip Christian Doczkal (Sep 07 2021 at 10:55):

Thanks @Pierre Roux and @Cyril Cohen. A colleague tried to get to the form that Cyril suggested, but without success, and I didn't see it either. But then, neither of us is used to these kinds of arguments.

view this post on Zulip Meven Lennon-Bertrand (Sep 07 2021 at 12:39):

I’m late, but here’s yet another proof (using the quotient rather than difference between the successive terms). First we have

(nn+1)n+1(n+1n+2)n+2=(11(n+1)2)n+1(n+2)=exp((n+1)ln(11(n+1)2))(n+2)\frac{\left(\frac{n}{n+1}\right)^{n+1}}{\left(\frac{n+1}{n+2}\right)^{n+2}} = \left(1 - \frac{1}{\left(n+1\right)^2}\right)^{n+1}\left(n+2\right) = \exp\left(\left(n+1\right)\ln\left(1 - \frac{1}{(n+1)^2}\right)\right)\left(n+2\right)

Now ln(1x)<x\ln(1-x) < -x (because ln\ln is convex, thus under its tangent at x=1x=1) and therefore

exp((n+1)ln(11(n+1)2))(n+2)<exp(1n+1)(n+2)\exp\left(\left(n+1\right)\ln\left(1 - \frac{1}{(n+1)^2}\right)\right)\left(n+2\right) < \exp\left(-\frac{1}{n+1}\right)(n+2)

Now that thing’s value at 00 is 2e1<12e^{-1} < 1 and the quotient of two successive terms is e1(11n+2)<1e^{-1}\left(1-\frac{1}{n+2}\right) < 1 and so it is always less than 11, so the original sequence is monotonically increasing.
This still requires some analysis, but probably less than your original argument (the inequality on the logarithm an rough approximate of ee).

view this post on Zulip Laurent Théry (Sep 07 2021 at 22:53):

you mean decreasing. Maybe you can have a look here

view this post on Zulip Christian Doczkal (Sep 08 2021 at 07:33):

No, I meant increasing, as nn+1<1<1+1n \frac n {n+1} < 1 < 1 + \frac 1 n , these are different functions. But there is some similarity, one converges to e e from above and the other to e1 e^{-1} from below.

view this post on Zulip Reynald Affeldt (Sep 08 2021 at 07:40):

(note that there is a proof that the one that converges to $e$ is increasing in a PR to analysis, if you manage to connect both...)

view this post on Zulip Christian Doczkal (Sep 08 2021 at 07:44):

Umm, what's the PR? According to WolframAlpha the one that converges to e e is decreasing. The increasing one, that I mentioned initially, converges to 1/e 1/e .

view this post on Zulip Reynald Affeldt (Sep 08 2021 at 07:46):

https://github.com/math-comp/analysis/pull/207

view this post on Zulip Reynald Affeldt (Sep 08 2021 at 07:51):

that's not exactly the same thing, my bad

view this post on Zulip Christian Doczkal (Sep 08 2021 at 07:52):

Maybe you want to add my sequence to this file? :smirk:

view this post on Zulip Reynald Affeldt (Sep 08 2021 at 07:54):

that would be a good occasion to revise this PR...

view this post on Zulip Christian Doczkal (Sep 08 2021 at 07:55):

As an aside, is it really that much harder to prove 2<e<3 2 < e < 3 than the 2<e4 2 < e \leq 4 which you prove in that PR? (Forgive my ignorance on these matters)

view this post on Zulip Reynald Affeldt (Sep 08 2021 at 07:59):

It is just that 4 was enough for convergence

view this post on Zulip Michael Soegtrop (Sep 08 2021 at 08:18):

@Vincent Semeria : looking at @Christian Doczkal 's question above on proving 2<e<32<e<3 it came to my mind what you once explained to me about the new structure of the standard library reals. If I got you right there is now a common constructive core definition of the reals with several derived branches, one of which are the standard library reals. But there is also a simple computational branch, and there is a lemma which allows to transport any lemma proved in one of the derived branches to any of the other derived branches. So couldn't one simply compute 2<e<32<e<3 in the computational branch (< is decidable there) and use the transport lemma to move this result to the standard library reals? How would this actually look in Coq? I guess this depends a lot on the definition of ee.

What I don't understand is how the math-comp reals are connected to this. Does math-comp reuse the standard library definition or does it has its own?

view this post on Zulip Reynald Affeldt (Sep 08 2021 at 09:10):

mathcomp-analysis does not use the reals of the standard Coq library

view this post on Zulip Vincent Semeria (Sep 08 2021 at 09:36):

@Michael Soegtrop @Christian Doczkal Yes 2 < e < 3 can be proved by computation. The only manual input required is the precision, here 0.1 suffices (because 2 can be approximated to 2.1 and e to 2.6). In other words, a proof of 2 < e is exists 0.1; reflexivity. The constructive interface of real numbers is in the standard library coq/theories/Reals/Abstract/ConstructiveReals.v. All its implementations are isomorphic, for example the computational implementation in CoRN. math-comp/analysis could implement it also, then prove 2 < e by computation in CoRN and deduce 2 < e in math-comp by isomorphism.

view this post on Zulip Laurent Théry (Sep 08 2021 at 10:44):

@Christian Doczkal my bad you are just considering the inverse of the usual definition of ee so in your case it is increasing.

(n/(n+1))n+1=1/((n+1)/n)n+1)=1/(1+1/n)n+1 (n/(n+1))^{n+1} = 1 / ((n + 1) / n)^{n+1}) = 1 / (1 + 1/n)^{n+1}

so can you still use the proofs given here

view this post on Zulip Christian Doczkal (Sep 08 2021 at 11:43):

@Laurent Théry , yes, fair enough.


Last updated: Feb 08 2023 at 07:02 UTC