equal
deleted
inserted
replaced
76 using assms by (approximation 20) |
76 using assms by (approximation 20) |
77 |
77 |
78 lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x" |
78 lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x" |
79 by (approximation 30 splitting: x=1 taylor: x = 3) |
79 by (approximation 30 splitting: x=1 taylor: x = 3) |
80 |
80 |
81 approximate "10" |
81 lemma "(n::real) \<in> {32 .. 62} \<Longrightarrow> \<lceil>log 2 (2 * (\<lfloor>n\<rfloor> div 2) + 1)\<rceil> = \<lceil>log 2 (\<lfloor>n\<rfloor> + 1)\<rceil>" |
|
82 unfolding eq_iff |
|
83 by (approximation 20) |
|
84 |
|
85 approximate 10 |
82 |
86 |
83 end |
87 end |