src/HOL/MacLaurin.thy
changeset 60017 b785d6d06430
parent 59730 b7c394c7a619
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/MacLaurin.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -389,6 +389,12 @@
     1.4                         (exp t / (fact n)) * x ^ n"
     1.5  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
     1.6  
     1.7 +lemma exp_lower_taylor_quadratic:
     1.8 +  fixes x::real
     1.9 +  shows "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
    1.10 +  using Maclaurin_exp_le [of x 3]
    1.11 +  by (auto simp: numeral_3_eq_3 power2_eq_square power_Suc)
    1.12 +
    1.13  
    1.14  subsection{*Version for Sine Function*}
    1.15