The Coq mailing list

[Allyx FONTAINE <fontaine AT labri.fr>]

Thank you very much for your help Cédric and Guillaume.
Best regards,
Allyx


Le 10/09/2012 15:23, gallais @ ensl.org a écrit :
> 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)'.