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