In one of my proofs I make use of the fact that the sequence is monotonically increasing for . 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
is strictly positive. Thus, is suffices to show for . The value at 1 is positive (~0.3) and the limit for is 0, so it should suffice to prove that its derivative
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.
I don't know but here is a tentative proof without having to resort on analysis (just need rational numbers):
for all n >= 1:
I was going to suggest a similar proof but concluding with
That being said, the analytic proof is arguably more elegant, and I think it would be not so hard to reproduce with mathcomp analysis.
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.
I’m late, but here’s yet another proof (using the quotient rather than difference between the successive terms). First we have
Now (because is convex, thus under its tangent at ) and therefore
Now that thing’s value at is and the quotient of two successive terms is and so it is always less than , 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 ).
you mean decreasing. Maybe you can have a look here
No, I meant increasing, as , these are different functions. But there is some similarity, one converges to from above and the other to from below.
(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...)
Umm, what's the PR? According to WolframAlpha the one that converges to is decreasing. The increasing one, that I mentioned initially, converges to .
that's not exactly the same thing, my bad
Maybe you want to add my sequence to this file? :smirk:
that would be a good occasion to revise this PR...
As an aside, is it really that much harder to prove than the which you prove in that PR? (Forgive my ignorance on these matters)
It is just that 4 was enough for convergence
@Vincent Semeria : looking at @Christian Doczkal 's question above on proving 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 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 .
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?
mathcomp-analysis does not use the reals of the standard Coq library
@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.
@Christian Doczkal my bad you are just considering the inverse of the usual definition of so in your case it is increasing.
so can you still use the proofs given here
@Laurent Théry , yes, fair enough.
Last updated: Feb 08 2023 at 07:02 UTC