|
1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 section \<open>Comparing growth of functions on natural numbers by a preorder relation\<close> |
|
5 |
|
6 theory Function_Growth |
|
7 imports |
|
8 Main |
|
9 "HOL-Library.Preorder" |
|
10 "HOL-Library.Discrete" |
|
11 begin |
|
12 |
|
13 (* FIXME move *) |
|
14 |
|
15 context linorder |
|
16 begin |
|
17 |
|
18 lemma mono_invE: |
|
19 fixes f :: "'a \<Rightarrow> 'b::order" |
|
20 assumes "mono f" |
|
21 assumes "f x < f y" |
|
22 obtains "x < y" |
|
23 proof |
|
24 show "x < y" |
|
25 proof (rule ccontr) |
|
26 assume "\<not> x < y" |
|
27 then have "y \<le> x" by simp |
|
28 with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE) |
|
29 with \<open>f x < f y\<close> show False by simp |
|
30 qed |
|
31 qed |
|
32 |
|
33 end |
|
34 |
|
35 lemma (in semidom_divide) power_diff: |
|
36 fixes a :: 'a |
|
37 assumes "a \<noteq> 0" |
|
38 assumes "m \<ge> n" |
|
39 shows "a ^ (m - n) = (a ^ m) div (a ^ n)" |
|
40 proof - |
|
41 define q where "q = m - n" |
|
42 with assms have "m = q + n" by (simp add: q_def) |
|
43 with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add) |
|
44 qed |
|
45 |
|
46 |
|
47 subsection \<open>Motivation\<close> |
|
48 |
|
49 text \<open> |
|
50 When comparing growth of functions in computer science, it is common to adhere |
|
51 on Landau Symbols (``O-Notation''). However these come at the cost of notational |
|
52 oddities, particularly writing \<open>f = O(g)\<close> for \<open>f \<in> O(g)\<close> etc. |
|
53 |
|
54 Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood, |
|
55 Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225). |
|
56 We establish a quasi order relation \<open>\<lesssim>\<close> on functions such that |
|
57 \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>. From a didactic point of view, this does not only |
|
58 avoid the notational oddities mentioned above but also emphasizes the key insight |
|
59 of a growth hierarchy of functions: |
|
60 \<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>\<close>. |
|
61 \<close> |
|
62 |
|
63 subsection \<open>Model\<close> |
|
64 |
|
65 text \<open> |
|
66 Our growth functions are of type \<open>\<nat> \<Rightarrow> \<nat>\<close>. This is different |
|
67 to the usual conventions for Landau symbols for which \<open>\<real> \<Rightarrow> \<real>\<close> |
|
68 would be appropriate, but we argue that \<open>\<real> \<Rightarrow> \<real>\<close> is more |
|
69 appropriate for analysis, whereas our setting is discrete. |
|
70 |
|
71 Note that we also restrict the additional coefficients to \<open>\<nat>\<close>, something |
|
72 we discuss at the particular definitions. |
|
73 \<close> |
|
74 |
|
75 subsection \<open>The \<open>\<lesssim>\<close> relation\<close> |
|
76 |
|
77 definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50) |
|
78 where |
|
79 "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)" |
|
80 |
|
81 text \<open> |
|
82 This yields \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>. Note that \<open>c\<close> is restricted to |
|
83 \<open>\<nat>\<close>. This does not pose any problems since if \<open>f \<in> O(g)\<close> holds for |
|
84 a \<open>c \<in> \<real>\<close>, it also holds for \<open>\<lceil>c\<rceil> \<in> \<nat>\<close> by transitivity. |
|
85 \<close> |
|
86 |
|
87 lemma less_eq_funI [intro?]: |
|
88 assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" |
|
89 shows "f \<lesssim> g" |
|
90 unfolding less_eq_fun_def by (rule assms) |
|
91 |
|
92 lemma not_less_eq_funI: |
|
93 assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m" |
|
94 shows "\<not> f \<lesssim> g" |
|
95 using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast |
|
96 |
|
97 lemma less_eq_funE [elim?]: |
|
98 assumes "f \<lesssim> g" |
|
99 obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m" |
|
100 using assms unfolding less_eq_fun_def by blast |
|
101 |
|
102 lemma not_less_eq_funE: |
|
103 assumes "\<not> f \<lesssim> g" and "c > 0" |
|
104 obtains m where "m > n" and "c * g m < f m" |
|
105 using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast |
|
106 |
|
107 |
|
108 subsection \<open>The \<open>\<approx>\<close> relation, the equivalence relation induced by \<open>\<lesssim>\<close>\<close> |
|
109 |
|
110 definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50) |
|
111 where |
|
112 "f \<cong> g \<longleftrightarrow> |
|
113 (\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m)" |
|
114 |
|
115 text \<open> |
|
116 This yields \<open>f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)\<close>. Concerning \<open>c\<^sub>1\<close> and \<open>c\<^sub>2\<close> |
|
117 restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>. |
|
118 \<close> |
|
119 |
|
120 lemma equiv_funI: |
|
121 assumes "\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
|
122 shows "f \<cong> g" |
|
123 unfolding equiv_fun_def by (rule assms) |
|
124 |
|
125 lemma not_equiv_funI: |
|
126 assumes "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow> |
|
127 \<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m" |
|
128 shows "\<not> f \<cong> g" |
|
129 using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast |
|
130 |
|
131 lemma equiv_funE: |
|
132 assumes "f \<cong> g" |
|
133 obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0" |
|
134 and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
|
135 using assms unfolding equiv_fun_def by blast |
|
136 |
|
137 lemma not_equiv_funE: |
|
138 fixes n c\<^sub>1 c\<^sub>2 |
|
139 assumes "\<not> f \<cong> g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0" |
|
140 obtains m where "m > n" |
|
141 and "c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m" |
|
142 using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast |
|
143 |
|
144 |
|
145 subsection \<open>The \<open>\<prec>\<close> relation, the strict part of \<open>\<lesssim>\<close>\<close> |
|
146 |
|
147 definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50) |
|
148 where |
|
149 "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f" |
|
150 |
|
151 lemma less_funI: |
|
152 assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" |
|
153 and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m" |
|
154 shows "f \<prec> g" |
|
155 using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast |
|
156 |
|
157 lemma not_less_funI: |
|
158 assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m" |
|
159 and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" |
|
160 shows "\<not> f \<prec> g" |
|
161 using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast |
|
162 |
|
163 lemma less_funE [elim?]: |
|
164 assumes "f \<prec> g" |
|
165 obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m" |
|
166 and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m" |
|
167 proof - |
|
168 from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def) |
|
169 from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for m |
|
170 by (rule less_eq_funE) blast |
|
171 { fix c n :: nat |
|
172 assume "c > 0" |
|
173 with \<open>\<not> g \<lesssim> f\<close> obtain m where "m > n" "c * f m < g m" |
|
174 by (rule not_less_eq_funE) blast |
|
175 then have **: "\<exists>m>n. c * f m < g m" by blast |
|
176 } note ** = this |
|
177 from * ** show thesis by (rule that) |
|
178 qed |
|
179 |
|
180 lemma not_less_funE: |
|
181 assumes "\<not> f \<prec> g" and "c > 0" |
|
182 obtains m where "m > n" and "c * g m < f m" |
|
183 | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q" |
|
184 using assms unfolding less_fun_def linorder_not_less [symmetric] by blast |
|
185 |
|
186 text \<open> |
|
187 I did not find a proof for \<open>f \<prec> g \<longleftrightarrow> f \<in> o(g)\<close>. Maybe this only |
|
188 holds if \<open>f\<close> and/or \<open>g\<close> are of a certain class of functions. |
|
189 However \<open>f \<in> o(g) \<longrightarrow> f \<prec> g\<close> is provable, and this yields a |
|
190 handy introduction rule. |
|
191 |
|
192 Note that D. Knuth ignores \<open>o\<close> altogether. So what \dots |
|
193 |
|
194 Something still has to be said about the coefficient \<open>c\<close> in |
|
195 the definition of \<open>(\<prec>)\<close>. In the typical definition of \<open>o\<close>, |
|
196 it occurs on the \emph{right} hand side of the \<open>(>)\<close>. The reason |
|
197 is that the situation is dual to the definition of \<open>O\<close>: the definition |
|
198 works since \<open>c\<close> may become arbitrary small. Since this is not possible |
|
199 within @{term \<nat>}, we push the coefficient to the left hand side instead such |
|
200 that it may become arbitrary big instead. |
|
201 \<close> |
|
202 |
|
203 lemma less_fun_strongI: |
|
204 assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m" |
|
205 shows "f \<prec> g" |
|
206 proof (rule less_funI) |
|
207 have "1 > (0::nat)" by simp |
|
208 with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m |
|
209 by blast |
|
210 have "\<forall>m>n. f m \<le> 1 * g m" |
|
211 proof (rule allI, rule impI) |
|
212 fix m |
|
213 assume "m > n" |
|
214 with * have "1 * f m < g m" by simp |
|
215 then show "f m \<le> 1 * g m" by simp |
|
216 qed |
|
217 with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast |
|
218 fix c n :: nat |
|
219 assume "c > 0" |
|
220 with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for m by blast |
|
221 then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp |
|
222 moreover have "Suc (q + n) > n" by simp |
|
223 ultimately show "\<exists>m>n. c * f m < g m" by blast |
|
224 qed |
|
225 |
|
226 |
|
227 subsection \<open>\<open>\<lesssim>\<close> is a preorder\<close> |
|
228 |
|
229 text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close> |
|
230 |
|
231 interpretation fun_order: preorder_equiv less_eq_fun less_fun |
|
232 rewrites "fun_order.equiv = equiv_fun" |
|
233 proof - |
|
234 interpret preorder: preorder_equiv less_eq_fun less_fun |
|
235 proof |
|
236 fix f g h |
|
237 show "f \<lesssim> f" |
|
238 proof |
|
239 have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto |
|
240 then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast |
|
241 qed |
|
242 show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f" |
|
243 by (fact less_fun_def) |
|
244 assume "f \<lesssim> g" and "g \<lesssim> h" |
|
245 show "f \<lesssim> h" |
|
246 proof |
|
247 from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1 |
|
248 where "c\<^sub>1 > 0" and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" |
|
249 by rule blast |
|
250 from \<open>g \<lesssim> h\<close> obtain n\<^sub>2 c\<^sub>2 |
|
251 where "c\<^sub>2 > 0" and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * h m" |
|
252 by rule blast |
|
253 have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" |
|
254 proof (rule allI, rule impI) |
|
255 fix m |
|
256 assume Q: "m > max n\<^sub>1 n\<^sub>2" |
|
257 from P\<^sub>1 Q have *: "f m \<le> c\<^sub>1 * g m" by simp |
|
258 from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * h m" by simp |
|
259 with \<open>c\<^sub>1 > 0\<close> have "c\<^sub>1 * g m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by simp |
|
260 with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans) |
|
261 qed |
|
262 then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule |
|
263 moreover from \<open>c\<^sub>1 > 0\<close> \<open>c\<^sub>2 > 0\<close> have "c\<^sub>1 * c\<^sub>2 > 0" by simp |
|
264 ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast |
|
265 qed |
|
266 qed |
|
267 from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" . |
|
268 show "preorder_equiv.equiv less_eq_fun = equiv_fun" |
|
269 proof (rule ext, rule ext, unfold preorder.equiv_def) |
|
270 fix f g |
|
271 show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g" |
|
272 proof |
|
273 assume "f \<cong> g" |
|
274 then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0" |
|
275 and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
|
276 by (rule equiv_funE) blast |
|
277 have "\<forall>m>n. f m \<le> c\<^sub>1 * g m" |
|
278 proof (rule allI, rule impI) |
|
279 fix m |
|
280 assume "m > n" |
|
281 with * show "f m \<le> c\<^sub>1 * g m" by simp |
|
282 qed |
|
283 with \<open>c\<^sub>1 > 0\<close> have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast |
|
284 then have "f \<lesssim> g" .. |
|
285 have "\<forall>m>n. g m \<le> c\<^sub>2 * f m" |
|
286 proof (rule allI, rule impI) |
|
287 fix m |
|
288 assume "m > n" |
|
289 with * show "g m \<le> c\<^sub>2 * f m" by simp |
|
290 qed |
|
291 with \<open>c\<^sub>2 > 0\<close> have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast |
|
292 then have "g \<lesssim> f" .. |
|
293 from \<open>f \<lesssim> g\<close> and \<open>g \<lesssim> f\<close> show "f \<lesssim> g \<and> g \<lesssim> f" .. |
|
294 next |
|
295 assume "f \<lesssim> g \<and> g \<lesssim> f" |
|
296 then have "f \<lesssim> g" and "g \<lesssim> f" by auto |
|
297 from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0" |
|
298 and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast |
|
299 from \<open>g \<lesssim> f\<close> obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0" |
|
300 and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * f m" by rule blast |
|
301 have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
|
302 proof (rule allI, rule impI) |
|
303 fix m |
|
304 assume Q: "m > max n\<^sub>1 n\<^sub>2" |
|
305 from P\<^sub>1 Q have "f m \<le> c\<^sub>1 * g m" by simp |
|
306 moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp |
|
307 ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" .. |
|
308 qed |
|
309 with \<open>c\<^sub>1 > 0\<close> \<open>c\<^sub>2 > 0\<close> have "\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. |
|
310 \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast |
|
311 then show "f \<cong> g" by (rule equiv_funI) |
|
312 qed |
|
313 qed |
|
314 qed |
|
315 |
|
316 declare fun_order.antisym [intro?] |
|
317 |
|
318 |
|
319 subsection \<open>Simple examples\<close> |
|
320 |
|
321 text \<open> |
|
322 Most of these are left as constructive exercises for the reader. Note that additional |
|
323 preconditions to the functions may be necessary. The list here is by no means to be |
|
324 intended as complete construction set for typical functions, here surely something |
|
325 has to be added yet. |
|
326 \<close> |
|
327 |
|
328 text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close> |
|
329 |
|
330 lemma equiv_fun_mono_const: |
|
331 assumes "mono f" and "\<exists>n. f n > 0" |
|
332 shows "(\<lambda>n. f n + k) \<cong> f" |
|
333 proof (cases "k = 0") |
|
334 case True then show ?thesis by simp |
|
335 next |
|
336 case False |
|
337 show ?thesis |
|
338 proof |
|
339 show "(\<lambda>n. f n + k) \<lesssim> f" |
|
340 proof |
|
341 from \<open>\<exists>n. f n > 0\<close> obtain n where "f n > 0" .. |
|
342 have "\<forall>m>n. f m + k \<le> Suc k * f m" |
|
343 proof (rule allI, rule impI) |
|
344 fix m |
|
345 assume "n < m" |
|
346 with \<open>mono f\<close> have "f n \<le> f m" |
|
347 using less_imp_le_nat monoE by blast |
|
348 with \<open>0 < f n\<close> have "0 < f m" by auto |
|
349 then obtain l where "f m = Suc l" by (cases "f m") simp_all |
|
350 then show "f m + k \<le> Suc k * f m" by simp |
|
351 qed |
|
352 then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m + k \<le> c * f m" by blast |
|
353 qed |
|
354 show "f \<lesssim> (\<lambda>n. f n + k)" |
|
355 proof |
|
356 have "f m \<le> 1 * (f m + k)" for m by simp |
|
357 then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (f m + k)" by blast |
|
358 qed |
|
359 qed |
|
360 qed |
|
361 |
|
362 lemma |
|
363 assumes "strict_mono f" |
|
364 shows "(\<lambda>n. f n + k) \<cong> f" |
|
365 proof (rule equiv_fun_mono_const) |
|
366 from assms show "mono f" by (rule strict_mono_mono) |
|
367 show "\<exists>n. 0 < f n" |
|
368 proof (rule ccontr) |
|
369 assume "\<not> (\<exists>n. 0 < f n)" |
|
370 then have "\<And>n. f n = 0" by simp |
|
371 then have "f 0 = f 1" by simp |
|
372 moreover from \<open>strict_mono f\<close> have "f 0 < f 1" |
|
373 by (simp add: strict_mono_def) |
|
374 ultimately show False by simp |
|
375 qed |
|
376 qed |
|
377 |
|
378 lemma |
|
379 "(\<lambda>n. Suc k * f n) \<cong> f" |
|
380 proof |
|
381 show "(\<lambda>n. Suc k * f n) \<lesssim> f" |
|
382 proof |
|
383 have "Suc k * f m \<le> Suc k * f m" for m by simp |
|
384 then show "\<exists>c>0. \<exists>n. \<forall>m>n. Suc k * f m \<le> c * f m" by blast |
|
385 qed |
|
386 show "f \<lesssim> (\<lambda>n. Suc k * f n)" |
|
387 proof |
|
388 have "f m \<le> 1 * (Suc k * f m)" for m by simp |
|
389 then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (Suc k * f m)" by blast |
|
390 qed |
|
391 qed |
|
392 |
|
393 lemma |
|
394 "f \<lesssim> (\<lambda>n. f n + g n)" |
|
395 by rule auto |
|
396 |
|
397 lemma |
|
398 "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)" |
|
399 by (rule less_fun_strongI) auto |
|
400 |
|
401 lemma |
|
402 "(\<lambda>_. k) \<prec> Discrete.log" |
|
403 proof (rule less_fun_strongI) |
|
404 fix c :: nat |
|
405 have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m" |
|
406 proof (rule allI, rule impI) |
|
407 fix m :: nat |
|
408 assume "2 ^ Suc (c * k) < m" |
|
409 then have "2 ^ Suc (c * k) \<le> m" by simp |
|
410 with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m" |
|
411 by (blast dest: monoD) |
|
412 moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp |
|
413 ultimately show "c * k < Discrete.log m" by auto |
|
414 qed |
|
415 then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" .. |
|
416 qed |
|
417 |
|
418 (*lemma |
|
419 "Discrete.log \<prec> Discrete.sqrt" |
|
420 proof (rule less_fun_strongI)*) |
|
421 text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close> |
|
422 |
|
423 lemma |
|
424 "Discrete.sqrt \<prec> id" |
|
425 proof (rule less_fun_strongI) |
|
426 fix c :: nat |
|
427 assume "0 < c" |
|
428 have "\<forall>m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m" |
|
429 proof (rule allI, rule impI) |
|
430 fix m |
|
431 assume "(Suc c)\<^sup>2 < m" |
|
432 then have "(Suc c)\<^sup>2 \<le> m" by simp |
|
433 with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<le> Discrete.sqrt m" by (rule monoE) |
|
434 then have "Suc c \<le> Discrete.sqrt m" by simp |
|
435 then have "c < Discrete.sqrt m" by simp |
|
436 moreover from \<open>(Suc c)\<^sup>2 < m\<close> have "Discrete.sqrt m > 0" by simp |
|
437 ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp |
|
438 also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric]) |
|
439 finally show "c * Discrete.sqrt m < id m" by simp |
|
440 qed |
|
441 then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" .. |
|
442 qed |
|
443 |
|
444 lemma |
|
445 "id \<prec> (\<lambda>n. n\<^sup>2)" |
|
446 by (rule less_fun_strongI) (auto simp add: power2_eq_square) |
|
447 |
|
448 lemma |
|
449 "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)" |
|
450 by (rule less_fun_strongI) auto |
|
451 |
|
452 (*lemma |
|
453 "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)" |
|
454 proof (rule less_fun_strongI)*) |
|
455 text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close> |
|
456 |
|
457 end |