The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Alyx,

With this proof in mind, the formalization is quite simple.
Here is a proof (relying solely on the stdlib).

Cheers,

--
guillaume


On 10 September 2012 13:13, Allyx FONTAINE 
<fontaine AT labri.fr>
 wrote:
>
>
> Le 10/09/2012 11:28, AUGER Cédric a écrit :
>
>> 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.
>
> Thanks for your remark, indeed I forgot to precise that m is a natural
> number greater or equal than x. This ensures that 0 <= (1 - x/m).
>
> The proof I found shows that f(y)=exp(-y) - (1-y) is greater or equal than 0
> (by studying the derivate of f). And then, substituting y with x/m and
> putting at the pow of m gives the result.
>
> I have also never used reals in Coq, and I don't know if such a proof is
> easily feasible.
>
> Allyx
>
>
>
>> So, if you meant your inequality only for negative 'x', I first suggest
>> you to prove that '(1+x/m)^m ≤ exp(x)'.
>
>

Attachment: exp_lb.v
Description: Binary data