coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Exponential function

From: Allyx FONTAINE <fontaine AT labri.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Exponential function
Date: Mon, 10 Sep 2012 10:01:55 +0200

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

[Coq-Club] Exponential function, Allyx FONTAINE, 09/10/2012
- <Possible follow-up(s)>
- [Coq-Club] Exponential function, Allyx FONTAINE, 09/10/2012
  - Re: [Coq-Club] Exponential function, AUGER Cédric, 09/10/2012
    - Re: [Coq-Club] Exponential function, Allyx FONTAINE, 09/10/2012
      - Re: [Coq-Club] Exponential function, gallais @ ensl.org, 09/10/2012
        
        Re: [Coq-Club] Exponential function, Allyx FONTAINE, 09/10/2012
      - Re: [Coq-Club] Exponential function, AUGER Cédric, 09/10/2012