The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 10 Sep 2012 10:01:55 +0200,
Allyx FONTAINE 
<fontaine AT labri.fr>
 a écrit :

> Hello,
> 
> I would like to prove the following inequality:
> 
> forall x m, ( 1 - x/m)^m <= exp(-x)
> 
> The question is: are there some works (in real standard library or 
> contributions) about this kind of inequality using exponential?
> How should I proceed to prove this one?
> 
> Thanks,
> Best regards,
> 
> Allyx

You lack some hypothesis, I fear.

I assume you want to mean that 'm' is some positive integer (to extend
to m = 0, you have to say that "x → x⁰(=1)" is stronger than the
division by 0),
and that exp(x) is defined by (1+x+x²/2+x³/6+x⁴/24+…+x^i/(i!)+…)

In such a case, if you take 'm' an even number (so, m=2 to fix stuff),
you have to show that
∀ x, (1-x/2)^2 ≤ exp(-x)
Now, it is a well know fact that 'exp(-x)' tends to 0 when 'x' tends to
+infinity, but '(1-x/2)^2' will tend to +infinity when 'x' tends to
+infinity, so there is one point from which your inequality won't hold
anymore.

For 'x' negative, I can easily do a proof (on paper, I have never
proved stuff with reals in Coq) that it is true (whether 'm' is odd or
even). I do not know from a given even 'm', from which point your
inequality becomes wrong (I suspect it to be from 0, as suggested by
the case 'm=0' when 'x' tends to 0 by positive values). When 'm' is
odd, your inequality is correct from a certain point (obviously lesser
than 'm' since from that point, the left part will become negative, and
that the exponential is always positive) to +infinity, but I do not know
if this point is or is not 0.

To sum up, you have to take more precise hypothesis, and at least
convince you on paper that it is true.

So, if you meant your inequality only for negative 'x', I first suggest
you to prove that '(1+x/m)^m ≤ exp(x)'.