equal
deleted
inserted
replaced
595 declare power_Suc [simp] |
595 declare power_Suc [simp] |
596 |
596 |
597 text\<open>32-bit Approximation to e\<close> |
597 text\<open>32-bit Approximation to e\<close> |
598 lemma e_approx_32: "\<bar>exp(1) - 5837465777 / 2147483648\<bar> \<le> (inverse(2 ^ 32)::real)" |
598 lemma e_approx_32: "\<bar>exp(1) - 5837465777 / 2147483648\<bar> \<le> (inverse(2 ^ 32)::real)" |
599 using Taylor_exp [of 1 14] exp_le |
599 using Taylor_exp [of 1 14] exp_le |
600 apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral) |
600 apply (simp add: setsum_distrib_right in_Reals_norm Re_exp atMost_nat_numeral fact_numeral) |
601 apply (simp only: pos_le_divide_eq [symmetric], linarith) |
601 apply (simp only: pos_le_divide_eq [symmetric], linarith) |
602 done |
602 done |
603 |
603 |
604 lemma e_less_3: "exp 1 < (3::real)" |
604 lemma e_less_3: "exp 1 < (3::real)" |
605 using e_approx_32 |
605 using e_approx_32 |