The Coq mailing list

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

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

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

The proof I had in mind for -x≥0 was just that

(1+x/m)^m = Σ a_i x^i

where

a_i = 0 for i>m

a_i = m!/(i! × (m-i)! × m^i) for 0 ≤ i ≤ m

whereas exp(x) = Σ b_i x^i

where

b_i = 1/(i!)

as

a_i = b_i for i ∈ {0; 1}, and a_i < b_i for i > 1,
you have that for x>0 (real) and m>0 (natural), (1+x/m)^m < exp(x) and
so, (1-x/m)^m < exp(x) for x<0 (real) and m>0 (natural).

That proof seems easy if the right theorems exist, but works only for
x<0. I do not know if you can modify the proof (for example by grouping
consecutive terms) to show that it holds for ]0; m].

Some other track to follow is that the following assertions are
equivalent (assuming m natural >0):

∀ x≤m. (1-x/m)^m ≤ exp(-x)

∀ y≤1. (1-my/m)^m ≤ exp(-my)

∀ y≤1. (1-y)^m ≤ exp(-my)

∀ y≤1. (1-y)^m ≤ exp(-y)^m

∀ y≤1. (1-y) ≤ exp(-y)

∀ y≥-1. (1+y) ≤ exp(y)

∀ z≥0. z ≤ exp(z-1)

The last two assertions seem easier to prove. So you may whish to prove
them first.