src/HOL/Library/BigO.thy
 author wenzelm Mon Dec 28 01:28:28 2015 +0100 (2015-12-28) changeset 61945 1135b8de26c3 parent 61762 d50b993b4fb9 child 61969 e01015e49041 permissions -rw-r--r--
more symbols;
1 (*  Title:      HOL/Library/BigO.thy
2     Authors:    Jeremy Avigad and Kevin Donnelly
3 *)
5 section \<open>Big O notation\<close>
7 theory BigO
8 imports Complex_Main Function_Algebras Set_Algebras
9 begin
11 text \<open>
12 This library is designed to support asymptotic big O'' calculations,
13 i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g + 14 O(h)$.  An earlier version of this library is described in detail in
17 The main changes in this version are as follows:
18 \begin{itemize}
19 \item We have eliminated the \<open>O\<close> operator on sets. (Most uses of this seem
20   to be inessential.)
21 \item We no longer use \<open>+\<close> as output syntax for \<open>+o\<close>
22 \item Lemmas involving \<open>sumr\<close> have been replaced by more general lemmas
23   involving `\<open>setsum\<close>.
24 \item The library has been expanded, with e.g.~support for expressions of
25   the form \<open>f < g + O(h)\<close>.
26 \end{itemize}
28 Note also since the Big O library includes rules that demonstrate set
29 inclusion, to use the automated reasoners effectively with the library
30 one should redeclare the theorem \<open>subsetI\<close> as an intro rule,
31 rather than as an \<open>intro!\<close> rule, for example, using
32 \isa{\isakeyword{declare}}~\<open>subsetI [del, intro]\<close>.
33 \<close>
35 subsection \<open>Definitions\<close>
37 definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(1O'(_'))")
38   where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>}"
40 lemma bigo_pos_const:
41   "(\<exists>c::'a::linordered_idom. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>) \<longleftrightarrow>
42     (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
43   apply auto
44   apply (case_tac "c = 0")
45   apply simp
46   apply (rule_tac x = "1" in exI)
47   apply simp
48   apply (rule_tac x = "\<bar>c\<bar>" in exI)
49   apply auto
50   apply (subgoal_tac "c * \<bar>f x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>")
51   apply (erule_tac x = x in allE)
52   apply force
53   apply (rule mult_right_mono)
54   apply (rule abs_ge_self)
55   apply (rule abs_ge_zero)
56   done
58 lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)}"
59   by (auto simp add: bigo_def bigo_pos_const)
61 lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"
62   apply (auto simp add: bigo_alt_def)
63   apply (rule_tac x = "ca * c" in exI)
64   apply (rule conjI)
65   apply simp
66   apply (rule allI)
67   apply (drule_tac x = "xa" in spec)+
68   apply (subgoal_tac "ca * \<bar>f xa\<bar> \<le> ca * (c * \<bar>g xa\<bar>)")
69   apply (erule order_trans)
71   apply (rule mult_left_mono, assumption)
72   apply (rule order_less_imp_le, assumption)
73   done
75 lemma bigo_refl [intro]: "f \<in> O(f)"
77   apply(rule_tac x = 1 in exI)
78   apply simp
79   done
81 lemma bigo_zero: "0 \<in> O(g)"
82   apply (auto simp add: bigo_def func_zero)
83   apply (rule_tac x = 0 in exI)
84   apply auto
85   done
87 lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}"
88   by (auto simp add: bigo_def)
90 lemma bigo_plus_self_subset [intro]: "O(f) + O(f) \<subseteq> O(f)"
91   apply (auto simp add: bigo_alt_def set_plus_def)
92   apply (rule_tac x = "c + ca" in exI)
93   apply auto
94   apply (simp add: ring_distribs func_plus)
95   apply (rule order_trans)
96   apply (rule abs_triangle_ineq)
98   apply force
99   apply force
100   done
102 lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
103   apply (rule equalityI)
104   apply (rule bigo_plus_self_subset)
105   apply (rule set_zero_plus2)
106   apply (rule bigo_zero)
107   done
109 lemma bigo_plus_subset [intro]: "O(f + g) \<subseteq> O(f) + O(g)"
110   apply (rule subsetI)
111   apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
112   apply (subst bigo_pos_const [symmetric])+
113   apply (rule_tac x = "\<lambda>n. if \<bar>g n\<bar> \<le> \<bar>f n\<bar> then x n else 0" in exI)
114   apply (rule conjI)
115   apply (rule_tac x = "c + c" in exI)
116   apply (clarsimp)
117   apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>f xa\<bar>")
118   apply (erule_tac x = xa in allE)
119   apply (erule order_trans)
120   apply (simp)
121   apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
122   apply (erule order_trans)
124   apply (rule mult_left_mono)
127   apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
128   apply (rule conjI)
129   apply (rule_tac x = "c + c" in exI)
130   apply auto
131   apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>g xa\<bar>")
132   apply (erule_tac x = xa in allE)
133   apply (erule order_trans)
134   apply simp
135   apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
136   apply (erule order_trans)
138   apply (rule mult_left_mono)
139   apply (rule abs_triangle_ineq)
141   done
143 lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
144   apply (subgoal_tac "A + B \<subseteq> O(f) + O(f)")
145   apply (erule order_trans)
146   apply simp
147   apply (auto del: subsetI simp del: bigo_plus_idemp)
148   done
150 lemma bigo_plus_eq: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> O(f + g) = O(f) + O(g)"
151   apply (rule equalityI)
152   apply (rule bigo_plus_subset)
153   apply (simp add: bigo_alt_def set_plus_def func_plus)
154   apply clarify
155   apply (rule_tac x = "max c ca" in exI)
156   apply (rule conjI)
157   apply (subgoal_tac "c \<le> max c ca")
158   apply (erule order_less_le_trans)
159   apply assumption
160   apply (rule max.cobounded1)
161   apply clarify
162   apply (drule_tac x = "xa" in spec)+
163   apply (subgoal_tac "0 \<le> f xa + g xa")
165   apply (subgoal_tac "\<bar>a xa + b xa\<bar> \<le> \<bar>a xa\<bar> + \<bar>b xa\<bar>")
166   apply (subgoal_tac "\<bar>a xa\<bar> + \<bar>b xa\<bar> \<le> max c ca * f xa + max c ca * g xa")
167   apply force
169   apply (subgoal_tac "c * f xa \<le> max c ca * f xa")
170   apply force
171   apply (rule mult_right_mono)
172   apply (rule max.cobounded1)
173   apply assumption
174   apply (subgoal_tac "ca * g xa \<le> max c ca * g xa")
175   apply force
176   apply (rule mult_right_mono)
177   apply (rule max.cobounded2)
178   apply assumption
179   apply (rule abs_triangle_ineq)
181   apply assumption+
182   done
184 lemma bigo_bounded_alt: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> c * g x \<Longrightarrow> f \<in> O(g)"
185   apply (auto simp add: bigo_def)
186   apply (rule_tac x = "\<bar>c\<bar>" in exI)
187   apply auto
188   apply (drule_tac x = x in spec)+
189   apply (simp add: abs_mult [symmetric])
190   done
192 lemma bigo_bounded: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> g x \<Longrightarrow> f \<in> O(g)"
193   apply (erule bigo_bounded_alt [of f 1 g])
194   apply simp
195   done
197 lemma bigo_bounded2: "\<forall>x. lb x \<le> f x \<Longrightarrow> \<forall>x. f x \<le> lb x + g x \<Longrightarrow> f \<in> lb +o O(g)"
198   apply (rule set_minus_imp_plus)
199   apply (rule bigo_bounded)
200   apply (auto simp add: fun_Compl_def func_plus)
201   apply (drule_tac x = x in spec)+
202   apply force
203   done
205 lemma bigo_abs: "(\<lambda>x. \<bar>f x\<bar>) =o O(f)"
206   apply (unfold bigo_def)
207   apply auto
208   apply (rule_tac x = 1 in exI)
209   apply auto
210   done
212 lemma bigo_abs2: "f =o O(\<lambda>x. \<bar>f x\<bar>)"
213   apply (unfold bigo_def)
214   apply auto
215   apply (rule_tac x = 1 in exI)
216   apply auto
217   done
219 lemma bigo_abs3: "O(f) = O(\<lambda>x. \<bar>f x\<bar>)"
220   apply (rule equalityI)
221   apply (rule bigo_elt_subset)
222   apply (rule bigo_abs2)
223   apply (rule bigo_elt_subset)
224   apply (rule bigo_abs)
225   done
227 lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o (\<lambda>x. \<bar>g x\<bar>) +o O(h)"
228   apply (drule set_plus_imp_minus)
229   apply (rule set_minus_imp_plus)
230   apply (subst fun_diff_def)
231 proof -
232   assume a: "f - g \<in> O(h)"
233   have "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) =o O(\<lambda>x. \<bar>\<bar>f x\<bar> - \<bar>g x\<bar>\<bar>)"
234     by (rule bigo_abs2)
235   also have "\<dots> \<subseteq> O(\<lambda>x. \<bar>f x - g x\<bar>)"
236     apply (rule bigo_elt_subset)
237     apply (rule bigo_bounded)
238     apply force
239     apply (rule allI)
240     apply (rule abs_triangle_ineq3)
241     done
242   also have "\<dots> \<subseteq> O(f - g)"
243     apply (rule bigo_elt_subset)
244     apply (subst fun_diff_def)
245     apply (rule bigo_abs)
246     done
247   also from a have "\<dots> \<subseteq> O(h)"
248     by (rule bigo_elt_subset)
249   finally show "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) \<in> O(h)".
250 qed
252 lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o O(g)"
253   by (unfold bigo_def, auto)
255 lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)"
256 proof -
257   assume "f \<in> g +o O(h)"
258   also have "\<dots> \<subseteq> O(g) + O(h)"
259     by (auto del: subsetI)
260   also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
261     apply (subst bigo_abs3 [symmetric])+
262     apply (rule refl)
263     done
264   also have "\<dots> = O((\<lambda>x. \<bar>g x\<bar>) + (\<lambda>x. \<bar>h x\<bar>))"
265     by (rule bigo_plus_eq [symmetric]) auto
266   finally have "f \<in> \<dots>" .
267   then have "O(f) \<subseteq> \<dots>"
268     by (elim bigo_elt_subset)
269   also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
270     by (rule bigo_plus_eq, auto)
271   finally show ?thesis
272     by (simp add: bigo_abs3 [symmetric])
273 qed
275 lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)"
276   apply (rule subsetI)
277   apply (subst bigo_def)
278   apply (auto simp add: bigo_alt_def set_times_def func_times)
279   apply (rule_tac x = "c * ca" in exI)
280   apply (rule allI)
281   apply (erule_tac x = x in allE)+
282   apply (subgoal_tac "c * ca * \<bar>f x * g x\<bar> = (c * \<bar>f x\<bar>) * (ca * \<bar>g x\<bar>)")
283   apply (erule ssubst)
284   apply (subst abs_mult)
285   apply (rule mult_mono)
286   apply assumption+
287   apply auto
288   apply (simp add: ac_simps abs_mult)
289   done
291 lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)"
292   apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
293   apply (rule_tac x = c in exI)
294   apply auto
295   apply (drule_tac x = x in spec)
296   apply (subgoal_tac "\<bar>f x\<bar> * \<bar>b x\<bar> \<le> \<bar>f x\<bar> * (c * \<bar>g x\<bar>)")
297   apply (force simp add: ac_simps)
298   apply (rule mult_left_mono, assumption)
299   apply (rule abs_ge_zero)
300   done
302 lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)"
303   apply (rule subsetD)
304   apply (rule bigo_mult)
305   apply (erule set_times_intro, assumption)
306   done
308 lemma bigo_mult4 [intro]: "f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)"
309   apply (drule set_plus_imp_minus)
310   apply (rule set_minus_imp_plus)
311   apply (drule bigo_mult3 [where g = g and j = g])
312   apply (auto simp add: algebra_simps)
313   done
315 lemma bigo_mult5:
316   fixes f :: "'a \<Rightarrow> 'b::linordered_field"
317   assumes "\<forall>x. f x \<noteq> 0"
318   shows "O(f * g) \<subseteq> f *o O(g)"
319 proof
320   fix h
321   assume "h \<in> O(f * g)"
322   then have "(\<lambda>x. 1 / (f x)) * h \<in> (\<lambda>x. 1 / f x) *o O(f * g)"
323     by auto
324   also have "\<dots> \<subseteq> O((\<lambda>x. 1 / f x) * (f * g))"
325     by (rule bigo_mult2)
326   also have "(\<lambda>x. 1 / f x) * (f * g) = g"
328     apply (rule ext)
329     apply (simp add: assms nonzero_divide_eq_eq ac_simps)
330     done
331   finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .
332   then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)"
333     by auto
334   also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h"
336     apply (rule ext)
337     apply (simp add: assms nonzero_divide_eq_eq ac_simps)
338     done
339   finally show "h \<in> f *o O(g)" .
340 qed
342 lemma bigo_mult6:
343   fixes f :: "'a \<Rightarrow> 'b::linordered_field"
344   shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = f *o O(g)"
345   apply (rule equalityI)
346   apply (erule bigo_mult5)
347   apply (rule bigo_mult2)
348   done
350 lemma bigo_mult7:
351   fixes f :: "'a \<Rightarrow> 'b::linordered_field"
352   shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<subseteq> O(f) * O(g)"
353   apply (subst bigo_mult6)
354   apply assumption
355   apply (rule set_times_mono3)
356   apply (rule bigo_refl)
357   done
359 lemma bigo_mult8:
360   fixes f :: "'a \<Rightarrow> 'b::linordered_field"
361   shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f) * O(g)"
362   apply (rule equalityI)
363   apply (erule bigo_mult7)
364   apply (rule bigo_mult)
365   done
367 lemma bigo_minus [intro]: "f \<in> O(g) \<Longrightarrow> - f \<in> O(g)"
368   by (auto simp add: bigo_def fun_Compl_def)
370 lemma bigo_minus2: "f \<in> g +o O(h) \<Longrightarrow> - f \<in> -g +o O(h)"
371   apply (rule set_minus_imp_plus)
372   apply (drule set_plus_imp_minus)
373   apply (drule bigo_minus)
374   apply simp
375   done
377 lemma bigo_minus3: "O(- f) = O(f)"
378   by (auto simp add: bigo_def fun_Compl_def)
380 lemma bigo_plus_absorb_lemma1: "f \<in> O(g) \<Longrightarrow> f +o O(g) \<subseteq> O(g)"
381 proof -
382   assume a: "f \<in> O(g)"
383   show "f +o O(g) \<subseteq> O(g)"
384   proof -
385     have "f \<in> O(f)" by auto
386     then have "f +o O(g) \<subseteq> O(f) + O(g)"
387       by (auto del: subsetI)
388     also have "\<dots> \<subseteq> O(g) + O(g)"
389     proof -
390       from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)
391       then show ?thesis by (auto del: subsetI)
392     qed
393     also have "\<dots> \<subseteq> O(g)" by simp
394     finally show ?thesis .
395   qed
396 qed
398 lemma bigo_plus_absorb_lemma2: "f \<in> O(g) \<Longrightarrow> O(g) \<subseteq> f +o O(g)"
399 proof -
400   assume a: "f \<in> O(g)"
401   show "O(g) \<subseteq> f +o O(g)"
402   proof -
403     from a have "- f \<in> O(g)"
404       by auto
405     then have "- f +o O(g) \<subseteq> O(g)"
406       by (elim bigo_plus_absorb_lemma1)
407     then have "f +o (- f +o O(g)) \<subseteq> f +o O(g)"
408       by auto
409     also have "f +o (- f +o O(g)) = O(g)"
411     finally show ?thesis .
412   qed
413 qed
415 lemma bigo_plus_absorb [simp]: "f \<in> O(g) \<Longrightarrow> f +o O(g) = O(g)"
416   apply (rule equalityI)
417   apply (erule bigo_plus_absorb_lemma1)
418   apply (erule bigo_plus_absorb_lemma2)
419   done
421 lemma bigo_plus_absorb2 [intro]: "f \<in> O(g) \<Longrightarrow> A \<subseteq> O(g) \<Longrightarrow> f +o A \<subseteq> O(g)"
422   apply (subgoal_tac "f +o A \<subseteq> f +o O(g)")
423   apply force+
424   done
426 lemma bigo_add_commute_imp: "f \<in> g +o O(h) \<Longrightarrow> g \<in> f +o O(h)"
427   apply (subst set_minus_plus [symmetric])
428   apply (subgoal_tac "g - f = - (f - g)")
429   apply (erule ssubst)
430   apply (rule bigo_minus)
431   apply (subst set_minus_plus)
432   apply assumption
434   done
436 lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"
437   apply (rule iffI)
439   done
441 lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"
442   by (auto simp add: bigo_def ac_simps)
444 lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)"
445   apply (rule bigo_elt_subset)
446   apply (rule bigo_const1)
447   done
449 lemma bigo_const3:
450   fixes c :: "'a::linordered_field"
451   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)"
453   apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
454   apply (simp add: abs_mult [symmetric])
455   done
457 lemma bigo_const4:
458   fixes c :: "'a::linordered_field"
459   shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)"
460   apply (rule bigo_elt_subset)
461   apply (rule bigo_const3)
462   apply assumption
463   done
465 lemma bigo_const [simp]:
466   fixes c :: "'a::linordered_field"
467   shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c) = O(\<lambda>x. 1)"
468   apply (rule equalityI)
469   apply (rule bigo_const2)
470   apply (rule bigo_const4)
471   apply assumption
472   done
474 lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
476   apply (rule_tac x = "\<bar>c\<bar>" in exI)
477   apply (auto simp add: abs_mult [symmetric])
478   done
480 lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"
481   apply (rule bigo_elt_subset)
482   apply (rule bigo_const_mult1)
483   done
485 lemma bigo_const_mult3:
486   fixes c :: "'a::linordered_field"
487   shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
489   apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
490   apply (simp add: abs_mult mult.assoc [symmetric])
491   done
493 lemma bigo_const_mult4:
494   fixes c :: "'a::linordered_field"
495   shows "c \<noteq> 0 \<Longrightarrow> O(f) \<subseteq> O(\<lambda>x. c * f x)"
496   apply (rule bigo_elt_subset)
497   apply (rule bigo_const_mult3)
498   apply assumption
499   done
501 lemma bigo_const_mult [simp]:
502   fixes c :: "'a::linordered_field"
503   shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c * f x) = O(f)"
504   apply (rule equalityI)
505   apply (rule bigo_const_mult2)
506   apply (erule bigo_const_mult4)
507   done
509 lemma bigo_const_mult5 [simp]:
510   fixes c :: "'a::linordered_field"
511   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) *o O(f) = O(f)"
512   apply (auto del: subsetI)
513   apply (rule order_trans)
514   apply (rule bigo_mult2)
516   apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
517   apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
518   apply (simp add: mult.assoc [symmetric] abs_mult)
519   apply (rule_tac x = "\<bar>inverse c\<bar> * ca" in exI)
520   apply auto
521   done
523 lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"
524   apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
525   apply (rule_tac x = "ca * \<bar>c\<bar>" in exI)
526   apply (rule allI)
527   apply (subgoal_tac "ca * \<bar>c\<bar> * \<bar>f x\<bar> = \<bar>c\<bar> * (ca * \<bar>f x\<bar>)")
528   apply (erule ssubst)
529   apply (subst abs_mult)
530   apply (rule mult_left_mono)
531   apply (erule spec)
532   apply simp
534   done
536 lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
537 proof -
538   assume "f =o O(g)"
539   then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)"
540     by auto
541   also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)"
543   also have "(\<lambda>x. c) *o O(g) \<subseteq> O(g)"
544     by (auto del: subsetI)
545   finally show ?thesis .
546 qed
548 lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f (k x)) =o O(\<lambda>x. g (k x))"
549   unfolding bigo_def by auto
551 lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow>
552     (\<lambda>x. f (k x)) =o (\<lambda>x. g (k x)) +o O(\<lambda>x. h(k x))"
553   apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)
554   apply (drule bigo_compose1)
556   done
559 subsection \<open>Setsum\<close>
561 lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>
562     \<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> \<le> c * h x y \<Longrightarrow>
563       (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
564   apply (auto simp add: bigo_def)
565   apply (rule_tac x = "\<bar>c\<bar>" in exI)
566   apply (subst abs_of_nonneg) back back
567   apply (rule setsum_nonneg)
568   apply force
569   apply (subst setsum_right_distrib)
570   apply (rule allI)
571   apply (rule order_trans)
572   apply (rule setsum_abs)
573   apply (rule setsum_mono)
574   apply (rule order_trans)
575   apply (drule spec)+
576   apply (drule bspec)+
577   apply assumption+
578   apply (drule bspec)
579   apply assumption+
580   apply (rule mult_right_mono)
581   apply (rule abs_ge_self)
582   apply force
583   done
585 lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow>
586     \<exists>c. \<forall>x y. \<bar>f x y\<bar> \<le> c * h x y \<Longrightarrow>
587       (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
588   apply (rule bigo_setsum_main)
589   apply force
590   apply clarsimp
591   apply (rule_tac x = c in exI)
592   apply force
593   done
595 lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow>
596     \<exists>c. \<forall>y. \<bar>f y\<bar> \<le> c * (h y) \<Longrightarrow>
597       (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"
598   by (rule bigo_setsum1) auto
600 lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
601     (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)"
602   apply (rule bigo_setsum1)
603   apply (rule allI)+
604   apply (rule abs_ge_zero)
605   apply (unfold bigo_def)
606   apply auto
607   apply (rule_tac x = c in exI)
608   apply (rule allI)+
609   apply (subst abs_mult)+
610   apply (subst mult.left_commute)
611   apply (rule mult_left_mono)
612   apply (erule spec)
613   apply (rule abs_ge_zero)
614   done
616 lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
617     (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
618       (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
619         O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)"
620   apply (rule set_minus_imp_plus)
621   apply (subst fun_diff_def)
622   apply (subst setsum_subtractf [symmetric])
623   apply (subst right_diff_distrib [symmetric])
624   apply (rule bigo_setsum3)
625   apply (subst fun_diff_def [symmetric])
626   apply (erule set_plus_imp_minus)
627   done
629 lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>
630     \<forall>x. 0 \<le> h x \<Longrightarrow>
631       (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
632         O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
633   apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) =
634       (\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)")
635   apply (erule ssubst)
636   apply (erule bigo_setsum3)
637   apply (rule ext)
638   apply (rule setsum.cong)
639   apply (rule refl)
640   apply (subst abs_of_nonneg)
641   apply auto
642   done
644 lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>
645     \<forall>x. 0 \<le> h x \<Longrightarrow>
646       (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
647         (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
648           O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
649   apply (rule set_minus_imp_plus)
650   apply (subst fun_diff_def)
651   apply (subst setsum_subtractf [symmetric])
652   apply (subst right_diff_distrib [symmetric])
653   apply (rule bigo_setsum5)
654   apply (subst fun_diff_def [symmetric])
655   apply (drule set_plus_imp_minus)
656   apply auto
657   done
660 subsection \<open>Misc useful stuff\<close>
662 lemma bigo_useful_intro: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
663   apply (subst bigo_plus_idemp [symmetric])
664   apply (rule set_plus_mono2)
665   apply assumption+
666   done
668 lemma bigo_useful_add: "f =o O(h) \<Longrightarrow> g =o O(h) \<Longrightarrow> f + g =o O(h)"
669   apply (subst bigo_plus_idemp [symmetric])
670   apply (rule set_plus_intro)
671   apply assumption+
672   done
674 lemma bigo_useful_const_mult:
675   fixes c :: "'a::linordered_field"
676   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)"
677   apply (rule subsetD)
678   apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) \<subseteq> O(h)")
679   apply assumption
680   apply (rule bigo_const_mult6)
681   apply (subgoal_tac "f = (\<lambda>x. 1 / c) * ((\<lambda>x. c) * f)")
682   apply (erule ssubst)
683   apply (erule set_times_intro2)
685   done
687 lemma bigo_fix: "(\<lambda>x::nat. f (x + 1)) =o O(\<lambda>x. h (x + 1)) \<Longrightarrow> f 0 = 0 \<Longrightarrow> f =o O(h)"
689   apply auto
690   apply (rule_tac x = c in exI)
691   apply auto
692   apply (case_tac "x = 0")
693   apply simp
694   apply (subgoal_tac "x = Suc (x - 1)")
695   apply (erule ssubst) back
696   apply (erule spec)
697   apply simp
698   done
700 lemma bigo_fix2:
701     "(\<lambda>x. f ((x::nat) + 1)) =o (\<lambda>x. g(x + 1)) +o O(\<lambda>x. h(x + 1)) \<Longrightarrow>
702        f 0 = g 0 \<Longrightarrow> f =o g +o O(h)"
703   apply (rule set_minus_imp_plus)
704   apply (rule bigo_fix)
705   apply (subst fun_diff_def)
706   apply (subst fun_diff_def [symmetric])
707   apply (rule set_plus_imp_minus)
708   apply simp
710   done
713 subsection \<open>Less than or equal to\<close>
715 definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl "<o" 70)
716   where "f <o g = (\<lambda>x. max (f x - g x) 0)"
718 lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
719   apply (unfold bigo_def)
720   apply clarsimp
721   apply (rule_tac x = c in exI)
722   apply (rule allI)
723   apply (rule order_trans)
724   apply (erule spec)+
725   done
727 lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> f x \<Longrightarrow> g =o O(h)"
728   apply (erule bigo_lesseq1)
729   apply (rule allI)
730   apply (drule_tac x = x in spec)
731   apply (rule order_trans)
732   apply assumption
733   apply (rule abs_ge_self)
734   done
736 lemma bigo_lesseq3: "f =o O(h) \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> f x \<Longrightarrow> g =o O(h)"
737   apply (erule bigo_lesseq2)
738   apply (rule allI)
739   apply (subst abs_of_nonneg)
740   apply (erule spec)+
741   done
743 lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
744     \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
745   apply (erule bigo_lesseq1)
746   apply (rule allI)
747   apply (subst abs_of_nonneg)
748   apply (erule spec)+
749   done
751 lemma bigo_lesso1: "\<forall>x. f x \<le> g x \<Longrightarrow> f <o g =o O(h)"
752   apply (unfold lesso_def)
753   apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")
754   apply (erule ssubst)
755   apply (rule bigo_zero)
756   apply (unfold func_zero)
757   apply (rule ext)
758   apply (simp split: split_max)
759   done
761 lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>
762     \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. k x \<le> f x \<Longrightarrow> k <o g =o O(h)"
763   apply (unfold lesso_def)
764   apply (rule bigo_lesseq4)
765   apply (erule set_plus_imp_minus)
766   apply (rule allI)
767   apply (rule max.cobounded2)
768   apply (rule allI)
769   apply (subst fun_diff_def)
770   apply (case_tac "0 \<le> k x - g x")
771   apply simp
772   apply (subst abs_of_nonneg)
773   apply (drule_tac x = x in spec) back
777   apply (erule spec)
778   apply (rule order_trans)
779   prefer 2
780   apply (rule abs_ge_zero)
782   done
784 lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
785     \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. g x \<le> k x \<Longrightarrow> f <o k =o O(h)"
786   apply (unfold lesso_def)
787   apply (rule bigo_lesseq4)
788   apply (erule set_plus_imp_minus)
789   apply (rule allI)
790   apply (rule max.cobounded2)
791   apply (rule allI)
792   apply (subst fun_diff_def)
793   apply (case_tac "0 \<le> f x - k x")
794   apply simp
795   apply (subst abs_of_nonneg)
796   apply (drule_tac x = x in spec) back
800   apply (rule le_imp_neg_le)
801   apply (erule spec)
802   apply (rule order_trans)
803   prefer 2
804   apply (rule abs_ge_zero)
806   done
808 lemma bigo_lesso4:
809   fixes k :: "'a \<Rightarrow> 'b::linordered_field"
810   shows "f <o g =o O(k) \<Longrightarrow> g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)"
811   apply (unfold lesso_def)
812   apply (drule set_plus_imp_minus)
813   apply (drule bigo_abs5) back
816   apply assumption
817   apply (erule bigo_lesseq2) back
818   apply (rule allI)
819   apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)
820   done
822 lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * \<bar>h x\<bar>"
823   apply (simp only: lesso_def bigo_alt_def)
824   apply clarsimp
825   apply (rule_tac x = c in exI)
826   apply (rule allI)
827   apply (drule_tac x = x in spec)
828   apply (subgoal_tac "\<bar>max (f x - g x) 0\<bar> = max (f x - g x) 0")
829   apply (clarsimp simp add: algebra_simps)
830   apply (rule abs_of_nonneg)
831   apply (rule max.cobounded2)
832   done
834 lemma lesso_add: "f <o g =o O(h) \<Longrightarrow> k <o l =o O(h) \<Longrightarrow> (f + k) <o (g + l) =o O(h)"
835   apply (unfold lesso_def)
836   apply (rule bigo_lesseq3)
838   apply assumption
839   apply (force split: split_max)
840   apply (auto split: split_max simp add: func_plus)
841   done
843 lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g ----> 0 \<Longrightarrow> f ----> (0::real)"
844   apply (simp add: LIMSEQ_iff bigo_alt_def)
845   apply clarify
846   apply (drule_tac x = "r / c" in spec)
847   apply (drule mp)
848   apply simp
849   apply clarify
850   apply (rule_tac x = no in exI)
851   apply (rule allI)
852   apply (drule_tac x = n in spec)+
853   apply (rule impI)
854   apply (drule mp)
855   apply assumption
856   apply (rule order_le_less_trans)
857   apply assumption
858   apply (rule order_less_le_trans)
859   apply (subgoal_tac "c * \<bar>g n\<bar> < c * (r / c)")
860   apply assumption
861   apply (erule mult_strict_left_mono)
862   apply assumption
863   apply simp
864   done
866 lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h ----> 0 \<Longrightarrow> f ----> a \<Longrightarrow> g ----> (a::real)"
867   apply (drule set_plus_imp_minus)
868   apply (drule bigo_LIMSEQ1)
869   apply assumption
870   apply (simp only: fun_diff_def)
871   apply (erule Lim_transform2)
872   apply assumption
873   done
875 end