src/HOL/Library/BigO.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 61969 e01015e49041
child 62947 3374f3ffb2ec
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (*  Title:      HOL/Library/BigO.thy
     2     Authors:    Jeremy Avigad and Kevin Donnelly
     3 *)
     4 
     5 section \<open>Big O notation\<close>
     6 
     7 theory BigO
     8 imports Complex_Main Function_Algebras Set_Algebras
     9 begin
    10 
    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
    15 @{cite "Avigad-Donnelly"}.
    16 
    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}
    27 
    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>
    34 
    35 subsection \<open>Definitions\<close>
    36 
    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>}"
    39 
    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
    57 
    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)
    60 
    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)
    70   apply (simp add: ac_simps)
    71   apply (rule mult_left_mono, assumption)
    72   apply (rule order_less_imp_le, assumption)
    73   done
    74 
    75 lemma bigo_refl [intro]: "f \<in> O(f)"
    76   apply(auto simp add: bigo_def)
    77   apply(rule_tac x = 1 in exI)
    78   apply simp
    79   done
    80 
    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
    86 
    87 lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}"
    88   by (auto simp add: bigo_def)
    89 
    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)
    97   apply (rule add_mono)
    98   apply force
    99   apply force
   100   done
   101 
   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
   108 
   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)
   123   apply (simp add: ring_distribs)
   124   apply (rule mult_left_mono)
   125   apply (simp add: abs_triangle_ineq)
   126   apply (simp add: order_less_le)
   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)
   137   apply (simp add: ring_distribs)
   138   apply (rule mult_left_mono)
   139   apply (rule abs_triangle_ineq)
   140   apply (simp add: order_less_le)
   141   done
   142 
   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
   149 
   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")
   164   apply (simp add: ring_distribs)
   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
   168   apply (rule add_mono)
   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)
   180   apply (rule add_nonneg_nonneg)
   181   apply assumption+
   182   done
   183 
   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
   191 
   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
   196 
   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
   204 
   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
   211 
   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
   218 
   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
   226 
   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
   251 
   252 lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o O(g)"
   253   by (unfold bigo_def, auto)
   254 
   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
   274 
   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
   290 
   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
   301 
   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
   307 
   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
   314 
   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"
   327     apply (simp add: func_times)
   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"
   335     apply (simp add: func_times)
   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
   341 
   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
   349 
   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
   358 
   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
   366 
   367 lemma bigo_minus [intro]: "f \<in> O(g) \<Longrightarrow> - f \<in> O(g)"
   368   by (auto simp add: bigo_def fun_Compl_def)
   369 
   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
   376 
   377 lemma bigo_minus3: "O(- f) = O(f)"
   378   by (auto simp add: bigo_def fun_Compl_def)
   379 
   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
   397 
   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)"
   410       by (simp add: set_plus_rearranges)
   411     finally show ?thesis .
   412   qed
   413 qed
   414 
   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
   420 
   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
   425 
   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
   433   apply (simp add: ac_simps)
   434   done
   435 
   436 lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"
   437   apply (rule iffI)
   438   apply (erule bigo_add_commute_imp)+
   439   done
   440 
   441 lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"
   442   by (auto simp add: bigo_def ac_simps)
   443 
   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
   448 
   449 lemma bigo_const3:
   450   fixes c :: "'a::linordered_field"
   451   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)"
   452   apply (simp add: bigo_def)
   453   apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
   454   apply (simp add: abs_mult [symmetric])
   455   done
   456 
   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
   464 
   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
   473 
   474 lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
   475   apply (simp add: bigo_def)
   476   apply (rule_tac x = "\<bar>c\<bar>" in exI)
   477   apply (auto simp add: abs_mult [symmetric])
   478   done
   479 
   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
   484 
   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)"
   488   apply (simp add: bigo_def)
   489   apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
   490   apply (simp add: abs_mult mult.assoc [symmetric])
   491   done
   492 
   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
   500 
   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
   508 
   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)
   515   apply (simp add: func_times)
   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
   522 
   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
   533   apply(simp add: ac_simps)
   534   done
   535 
   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)"
   542     by (simp add: func_times)
   543   also have "(\<lambda>x. c) *o O(g) \<subseteq> O(g)"
   544     by (auto del: subsetI)
   545   finally show ?thesis .
   546 qed
   547 
   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
   550 
   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)
   555   apply (simp add: fun_diff_def)
   556   done
   557 
   558 
   559 subsection \<open>Setsum\<close>
   560 
   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
   584 
   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
   594 
   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
   599 
   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
   615 
   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
   628 
   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
   643 
   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
   658 
   659 
   660 subsection \<open>Misc useful stuff\<close>
   661 
   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
   667 
   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
   673 
   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)
   684   apply (simp add: func_times)
   685   done
   686 
   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)"
   688   apply (simp add: bigo_alt_def)
   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
   699 
   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
   709   apply (simp add: fun_diff_def)
   710   done
   711 
   712 
   713 subsection \<open>Less than or equal to\<close>
   714 
   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)"
   717 
   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
   726 
   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
   735 
   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
   742 
   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
   750 
   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
   760 
   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
   774   apply (simp add: algebra_simps)
   775   apply (subst diff_conv_add_uminus)+
   776   apply (rule add_right_mono)
   777   apply (erule spec)
   778   apply (rule order_trans)
   779   prefer 2
   780   apply (rule abs_ge_zero)
   781   apply (simp add: algebra_simps)
   782   done
   783 
   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
   797   apply (simp add: algebra_simps)
   798   apply (subst diff_conv_add_uminus)+
   799   apply (rule add_left_mono)
   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)
   805   apply (simp add: algebra_simps)
   806   done
   807 
   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
   814   apply (simp add: fun_diff_def)
   815   apply (drule bigo_useful_add)
   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
   821 
   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
   833 
   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)
   837   apply (erule bigo_useful_add)
   838   apply assumption
   839   apply (force split: split_max)
   840   apply (auto split: split_max simp add: func_plus)
   841   done
   842 
   843 lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g \<longlonglongrightarrow> 0 \<Longrightarrow> f \<longlonglongrightarrow> (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
   865 
   866 lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h \<longlonglongrightarrow> 0 \<Longrightarrow> f \<longlonglongrightarrow> a \<Longrightarrow> g \<longlonglongrightarrow> (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
   874 
   875 end