Stream: math-comp users

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

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)}$ is monotonically increasing for $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

$$\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 $n \log \left(\frac n {n + 1} \right) + 1 > 0$ for $n \geq 1$. The value at 1 is positive (~0.3) and the limit for $n \to \infty$ is 0, so it should suffice to prove that its derivative

$$\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.

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:

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

hence

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

hence

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

hence

$$\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

$$\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

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

hence

$$\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

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

Cyril Cohen (Sep 07 2021 at 10:00):

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

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.

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.

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

$$\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(1-x) < -x$ (because $\ln$ is convex, thus under its tangent at $x=1$) and therefore

$$\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 $0$ is $2e^{-1} < 1$ and the quotient of two successive terms is $e^{-1}\left(1-\frac{1}{n+2}\right) < 1$ and so it is always less than $1$, 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 $e$).

Laurent Théry (Sep 07 2021 at 22:53):

you mean decreasing. Maybe you can have a look here

Christian Doczkal (Sep 08 2021 at 07:33):

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

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...)

Christian Doczkal (Sep 08 2021 at 07:44):

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

Reynald Affeldt (Sep 08 2021 at 07:46):

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

Reynald Affeldt (Sep 08 2021 at 07:51):

that's not exactly the same thing, my bad

Christian Doczkal (Sep 08 2021 at 07:52):

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

Reynald Affeldt (Sep 08 2021 at 07:54):

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

Christian Doczkal (Sep 08 2021 at 07:55):

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

Reynald Affeldt (Sep 08 2021 at 07:59):

It is just that 4 was enough for convergence

Michael Soegtrop (Sep 08 2021 at 08:18):

@Vincent Semeria : looking at @Christian Doczkal 's question above on proving $2<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<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 $e$.

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?

Reynald Affeldt (Sep 08 2021 at 09:10):

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

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.

Laurent Théry (Sep 08 2021 at 10:44):

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

$$(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

Christian Doczkal (Sep 08 2021 at 11:43):

@Laurent Théry , yes, fair enough.

Last updated: Feb 08 2023 at 07:02 UTC