src/HOL/Library/BigO.thy
 author paulson Wed Apr 22 12:43:06 2015 +0100 (2015-04-22) changeset 60142 3275dddf356f parent 60141 833adf7db7d8 child 60500 903bb1495239 permissions -rw-r--r--
fixes for limits
     1 (*  Title:      HOL/Library/BigO.thy

     2     Authors:    Jeremy Avigad and Kevin Donnelly

     3 *)

     4

     5 section {* Big O notation *}

     6

     7 theory BigO

     8 imports Complex_Main Function_Algebras Set_Algebras

     9 begin

    10

    11 text {*

    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 @{text O} operator on sets. (Most uses of this seem

    20   to be inessential.)

    21 \item We no longer use @{text "+"} as output syntax for @{text "+o"}

    22 \item Lemmas involving @{text "sumr"} have been replaced by more general lemmas

    23   involving @{text "setsum"}.

    24 \item The library has been expanded, with e.g.~support for expressions of

    25   the form @{text "f < g + O(h)"}.

    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 @{text "subsetI"} as an intro rule,

    31 rather than as an @{text "intro!"} rule, for example, using

    32 \isa{\isakeyword{declare}}~@{text "subsetI [del, intro]"}.

    33 *}

    34

    35 subsection {* Definitions *}

    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. abs (h x) \<le> c * abs (f x)}"

    39

    40 lemma bigo_pos_const:

    41   "(\<exists>c::'a::linordered_idom. \<forall>x. abs (h x) \<le> c * abs (f x)) \<longleftrightarrow>

    42     (\<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x)))"

    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 = "abs c" in exI)

    49   apply auto

    50   apply (subgoal_tac "c * abs (f x) \<le> abs c * abs (f x)")

    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. abs (h x) \<le> c * abs (f x))}"

    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 * abs (f xa) \<le> ca * (c * abs (g xa))")

    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 abs (g n) \<le> (abs (f n)) 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 * abs (f xa + g xa) \<le> (c + c) * abs (f xa)")

   118   apply (erule_tac x = xa in allE)

   119   apply (erule order_trans)

   120   apply (simp)

   121   apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")

   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 (abs (f n)) < abs (g n) 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 * abs (f xa + g xa) \<le> (c + c) * abs (g xa)")

   132   apply (erule_tac x = xa in allE)

   133   apply (erule order_trans)

   134   apply simp

   135   apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")

   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 "abs (a xa + b xa) \<le> abs (a xa) + abs (b xa)")

   166   apply (subgoal_tac "abs (a xa) + abs (b xa) \<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 = "abs c" 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   apply (drule_tac x = x in spec)+

   204   apply force

   205   done

   206

   207 lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)"

   208   apply (unfold bigo_def)

   209   apply auto

   210   apply (rule_tac x = 1 in exI)

   211   apply auto

   212   done

   213

   214 lemma bigo_abs2: "f =o O(\<lambda>x. abs (f x))"

   215   apply (unfold bigo_def)

   216   apply auto

   217   apply (rule_tac x = 1 in exI)

   218   apply auto

   219   done

   220

   221 lemma bigo_abs3: "O(f) = O(\<lambda>x. abs (f x))"

   222   apply (rule equalityI)

   223   apply (rule bigo_elt_subset)

   224   apply (rule bigo_abs2)

   225   apply (rule bigo_elt_subset)

   226   apply (rule bigo_abs)

   227   done

   228

   229 lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)"

   230   apply (drule set_plus_imp_minus)

   231   apply (rule set_minus_imp_plus)

   232   apply (subst fun_diff_def)

   233 proof -

   234   assume a: "f - g \<in> O(h)"

   235   have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs (abs (f x) - abs (g x)))"

   236     by (rule bigo_abs2)

   237   also have "\<dots> \<subseteq> O(\<lambda>x. abs (f x - g x))"

   238     apply (rule bigo_elt_subset)

   239     apply (rule bigo_bounded)

   240     apply force

   241     apply (rule allI)

   242     apply (rule abs_triangle_ineq3)

   243     done

   244   also have "\<dots> \<subseteq> O(f - g)"

   245     apply (rule bigo_elt_subset)

   246     apply (subst fun_diff_def)

   247     apply (rule bigo_abs)

   248     done

   249   also from a have "\<dots> \<subseteq> O(h)"

   250     by (rule bigo_elt_subset)

   251   finally show "(\<lambda>x. abs (f x) - abs (g x)) \<in> O(h)".

   252 qed

   253

   254 lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs (f x)) =o O(g)"

   255   by (unfold bigo_def, auto)

   256

   257 lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)"

   258 proof -

   259   assume "f \<in> g +o O(h)"

   260   also have "\<dots> \<subseteq> O(g) + O(h)"

   261     by (auto del: subsetI)

   262   also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"

   263     apply (subst bigo_abs3 [symmetric])+

   264     apply (rule refl)

   265     done

   266   also have "\<dots> = O((\<lambda>x. abs (g x)) + (\<lambda>x. abs (h x)))"

   267     by (rule bigo_plus_eq [symmetric]) auto

   268   finally have "f \<in> \<dots>" .

   269   then have "O(f) \<subseteq> \<dots>"

   270     by (elim bigo_elt_subset)

   271   also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"

   272     by (rule bigo_plus_eq, auto)

   273   finally show ?thesis

   274     by (simp add: bigo_abs3 [symmetric])

   275 qed

   276

   277 lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)"

   278   apply (rule subsetI)

   279   apply (subst bigo_def)

   280   apply (auto simp add: bigo_alt_def set_times_def func_times)

   281   apply (rule_tac x = "c * ca" in exI)

   282   apply (rule allI)

   283   apply (erule_tac x = x in allE)+

   284   apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs (f x)) * (ca * abs (g x))")

   285   apply (erule ssubst)

   286   apply (subst abs_mult)

   287   apply (rule mult_mono)

   288   apply assumption+

   289   apply auto

   290   apply (simp add: ac_simps abs_mult)

   291   done

   292

   293 lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)"

   294   apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)

   295   apply (rule_tac x = c in exI)

   296   apply auto

   297   apply (drule_tac x = x in spec)

   298   apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")

   299   apply (force simp add: ac_simps)

   300   apply (rule mult_left_mono, assumption)

   301   apply (rule abs_ge_zero)

   302   done

   303

   304 lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)"

   305   apply (rule subsetD)

   306   apply (rule bigo_mult)

   307   apply (erule set_times_intro, assumption)

   308   done

   309

   310 lemma bigo_mult4 [intro]: "f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)"

   311   apply (drule set_plus_imp_minus)

   312   apply (rule set_minus_imp_plus)

   313   apply (drule bigo_mult3 [where g = g and j = g])

   314   apply (auto simp add: algebra_simps)

   315   done

   316

   317 lemma bigo_mult5:

   318   fixes f :: "'a \<Rightarrow> 'b::linordered_field"

   319   assumes "\<forall>x. f x \<noteq> 0"

   320   shows "O(f * g) \<subseteq> f *o O(g)"

   321 proof

   322   fix h

   323   assume "h \<in> O(f * g)"

   324   then have "(\<lambda>x. 1 / (f x)) * h \<in> (\<lambda>x. 1 / f x) *o O(f * g)"

   325     by auto

   326   also have "\<dots> \<subseteq> O((\<lambda>x. 1 / f x) * (f * g))"

   327     by (rule bigo_mult2)

   328   also have "(\<lambda>x. 1 / f x) * (f * g) = g"

   329     apply (simp add: func_times)

   330     apply (rule ext)

   331     apply (simp add: assms nonzero_divide_eq_eq ac_simps)

   332     done

   333   finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .

   334   then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)"

   335     by auto

   336   also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h"

   337     apply (simp add: func_times)

   338     apply (rule ext)

   339     apply (simp add: assms nonzero_divide_eq_eq ac_simps)

   340     done

   341   finally show "h \<in> f *o O(g)" .

   342 qed

   343

   344 lemma bigo_mult6:

   345   fixes f :: "'a \<Rightarrow> 'b::linordered_field"

   346   shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = f *o O(g)"

   347   apply (rule equalityI)

   348   apply (erule bigo_mult5)

   349   apply (rule bigo_mult2)

   350   done

   351

   352 lemma bigo_mult7:

   353   fixes f :: "'a \<Rightarrow> 'b::linordered_field"

   354   shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<subseteq> O(f) * O(g)"

   355   apply (subst bigo_mult6)

   356   apply assumption

   357   apply (rule set_times_mono3)

   358   apply (rule bigo_refl)

   359   done

   360

   361 lemma bigo_mult8:

   362   fixes f :: "'a \<Rightarrow> 'b::linordered_field"

   363   shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f) * O(g)"

   364   apply (rule equalityI)

   365   apply (erule bigo_mult7)

   366   apply (rule bigo_mult)

   367   done

   368

   369 lemma bigo_minus [intro]: "f \<in> O(g) \<Longrightarrow> - f \<in> O(g)"

   370   by (auto simp add: bigo_def fun_Compl_def)

   371

   372 lemma bigo_minus2: "f \<in> g +o O(h) \<Longrightarrow> - f \<in> -g +o O(h)"

   373   apply (rule set_minus_imp_plus)

   374   apply (drule set_plus_imp_minus)

   375   apply (drule bigo_minus)

   376   apply simp

   377   done

   378

   379 lemma bigo_minus3: "O(- f) = O(f)"

   380   by (auto simp add: bigo_def fun_Compl_def)

   381

   382 lemma bigo_plus_absorb_lemma1: "f \<in> O(g) \<Longrightarrow> f +o O(g) \<subseteq> O(g)"

   383 proof -

   384   assume a: "f \<in> O(g)"

   385   show "f +o O(g) \<subseteq> O(g)"

   386   proof -

   387     have "f \<in> O(f)" by auto

   388     then have "f +o O(g) \<subseteq> O(f) + O(g)"

   389       by (auto del: subsetI)

   390     also have "\<dots> \<subseteq> O(g) + O(g)"

   391     proof -

   392       from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)

   393       then show ?thesis by (auto del: subsetI)

   394     qed

   395     also have "\<dots> \<subseteq> O(g)" by simp

   396     finally show ?thesis .

   397   qed

   398 qed

   399

   400 lemma bigo_plus_absorb_lemma2: "f \<in> O(g) \<Longrightarrow> O(g) \<subseteq> f +o O(g)"

   401 proof -

   402   assume a: "f \<in> O(g)"

   403   show "O(g) \<subseteq> f +o O(g)"

   404   proof -

   405     from a have "- f \<in> O(g)"

   406       by auto

   407     then have "- f +o O(g) \<subseteq> O(g)"

   408       by (elim bigo_plus_absorb_lemma1)

   409     then have "f +o (- f +o O(g)) \<subseteq> f +o O(g)"

   410       by auto

   411     also have "f +o (- f +o O(g)) = O(g)"

   412       by (simp add: set_plus_rearranges)

   413     finally show ?thesis .

   414   qed

   415 qed

   416

   417 lemma bigo_plus_absorb [simp]: "f \<in> O(g) \<Longrightarrow> f +o O(g) = O(g)"

   418   apply (rule equalityI)

   419   apply (erule bigo_plus_absorb_lemma1)

   420   apply (erule bigo_plus_absorb_lemma2)

   421   done

   422

   423 lemma bigo_plus_absorb2 [intro]: "f \<in> O(g) \<Longrightarrow> A \<subseteq> O(g) \<Longrightarrow> f +o A \<subseteq> O(g)"

   424   apply (subgoal_tac "f +o A \<subseteq> f +o O(g)")

   425   apply force+

   426   done

   427

   428 lemma bigo_add_commute_imp: "f \<in> g +o O(h) \<Longrightarrow> g \<in> f +o O(h)"

   429   apply (subst set_minus_plus [symmetric])

   430   apply (subgoal_tac "g - f = - (f - g)")

   431   apply (erule ssubst)

   432   apply (rule bigo_minus)

   433   apply (subst set_minus_plus)

   434   apply assumption

   435   apply (simp add: ac_simps)

   436   done

   437

   438 lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"

   439   apply (rule iffI)

   440   apply (erule bigo_add_commute_imp)+

   441   done

   442

   443 lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"

   444   by (auto simp add: bigo_def ac_simps)

   445

   446 lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)"

   447   apply (rule bigo_elt_subset)

   448   apply (rule bigo_const1)

   449   done

   450

   451 lemma bigo_const3:

   452   fixes c :: "'a::linordered_field"

   453   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)"

   454   apply (simp add: bigo_def)

   455   apply (rule_tac x = "abs (inverse c)" in exI)

   456   apply (simp add: abs_mult [symmetric])

   457   done

   458

   459 lemma bigo_const4:

   460   fixes c :: "'a::linordered_field"

   461   shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)"

   462   apply (rule bigo_elt_subset)

   463   apply (rule bigo_const3)

   464   apply assumption

   465   done

   466

   467 lemma bigo_const [simp]:

   468   fixes c :: "'a::linordered_field"

   469   shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c) = O(\<lambda>x. 1)"

   470   apply (rule equalityI)

   471   apply (rule bigo_const2)

   472   apply (rule bigo_const4)

   473   apply assumption

   474   done

   475

   476 lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"

   477   apply (simp add: bigo_def)

   478   apply (rule_tac x = "abs c" in exI)

   479   apply (auto simp add: abs_mult [symmetric])

   480   done

   481

   482 lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"

   483   apply (rule bigo_elt_subset)

   484   apply (rule bigo_const_mult1)

   485   done

   486

   487 lemma bigo_const_mult3:

   488   fixes c :: "'a::linordered_field"

   489   shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"

   490   apply (simp add: bigo_def)

   491   apply (rule_tac x = "abs (inverse c)" in exI)

   492   apply (simp add: abs_mult mult.assoc [symmetric])

   493   done

   494

   495 lemma bigo_const_mult4:

   496   fixes c :: "'a::linordered_field"

   497   shows "c \<noteq> 0 \<Longrightarrow> O(f) \<subseteq> O(\<lambda>x. c * f x)"

   498   apply (rule bigo_elt_subset)

   499   apply (rule bigo_const_mult3)

   500   apply assumption

   501   done

   502

   503 lemma bigo_const_mult [simp]:

   504   fixes c :: "'a::linordered_field"

   505   shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c * f x) = O(f)"

   506   apply (rule equalityI)

   507   apply (rule bigo_const_mult2)

   508   apply (erule bigo_const_mult4)

   509   done

   510

   511 lemma bigo_const_mult5 [simp]:

   512   fixes c :: "'a::linordered_field"

   513   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) *o O(f) = O(f)"

   514   apply (auto del: subsetI)

   515   apply (rule order_trans)

   516   apply (rule bigo_mult2)

   517   apply (simp add: func_times)

   518   apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)

   519   apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)

   520   apply (simp add: mult.assoc [symmetric] abs_mult)

   521   apply (rule_tac x = "abs (inverse c) * ca" in exI)

   522   apply auto

   523   done

   524

   525 lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"

   526   apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)

   527   apply (rule_tac x = "ca * abs c" in exI)

   528   apply (rule allI)

   529   apply (subgoal_tac "ca * abs c * abs (f x) = abs c * (ca * abs (f x))")

   530   apply (erule ssubst)

   531   apply (subst abs_mult)

   532   apply (rule mult_left_mono)

   533   apply (erule spec)

   534   apply simp

   535   apply(simp add: ac_simps)

   536   done

   537

   538 lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"

   539 proof -

   540   assume "f =o O(g)"

   541   then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)"

   542     by auto

   543   also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)"

   544     by (simp add: func_times)

   545   also have "(\<lambda>x. c) *o O(g) \<subseteq> O(g)"

   546     by (auto del: subsetI)

   547   finally show ?thesis .

   548 qed

   549

   550 lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f (k x)) =o O(\<lambda>x. g (k x))"

   551   unfolding bigo_def by auto

   552

   553 lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow>

   554     (\<lambda>x. f (k x)) =o (\<lambda>x. g (k x)) +o O(\<lambda>x. h(k x))"

   555   apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)

   556   apply (drule bigo_compose1)

   557   apply (simp add: fun_diff_def)

   558   done

   559

   560

   561 subsection {* Setsum *}

   562

   563 lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>

   564     \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow>

   565       (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"

   566   apply (auto simp add: bigo_def)

   567   apply (rule_tac x = "abs c" in exI)

   568   apply (subst abs_of_nonneg) back back

   569   apply (rule setsum_nonneg)

   570   apply force

   571   apply (subst setsum_right_distrib)

   572   apply (rule allI)

   573   apply (rule order_trans)

   574   apply (rule setsum_abs)

   575   apply (rule setsum_mono)

   576   apply (rule order_trans)

   577   apply (drule spec)+

   578   apply (drule bspec)+

   579   apply assumption+

   580   apply (drule bspec)

   581   apply assumption+

   582   apply (rule mult_right_mono)

   583   apply (rule abs_ge_self)

   584   apply force

   585   done

   586

   587 lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow>

   588     \<exists>c. \<forall>x y. abs (f x y) \<le> c * h x y \<Longrightarrow>

   589       (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"

   590   apply (rule bigo_setsum_main)

   591   apply force

   592   apply clarsimp

   593   apply (rule_tac x = c in exI)

   594   apply force

   595   done

   596

   597 lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow>

   598     \<exists>c. \<forall>y. abs (f y) \<le> c * (h y) \<Longrightarrow>

   599       (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"

   600   by (rule bigo_setsum1) auto

   601

   602 lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>

   603     (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"

   604   apply (rule bigo_setsum1)

   605   apply (rule allI)+

   606   apply (rule abs_ge_zero)

   607   apply (unfold bigo_def)

   608   apply auto

   609   apply (rule_tac x = c in exI)

   610   apply (rule allI)+

   611   apply (subst abs_mult)+

   612   apply (subst mult.left_commute)

   613   apply (rule mult_left_mono)

   614   apply (erule spec)

   615   apply (rule abs_ge_zero)

   616   done

   617

   618 lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>

   619     (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o

   620       (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o

   621         O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"

   622   apply (rule set_minus_imp_plus)

   623   apply (subst fun_diff_def)

   624   apply (subst setsum_subtractf [symmetric])

   625   apply (subst right_diff_distrib [symmetric])

   626   apply (rule bigo_setsum3)

   627   apply (subst fun_diff_def [symmetric])

   628   apply (erule set_plus_imp_minus)

   629   done

   630

   631 lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>

   632     \<forall>x. 0 \<le> h x \<Longrightarrow>

   633       (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o

   634         O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"

   635   apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) =

   636       (\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))")

   637   apply (erule ssubst)

   638   apply (erule bigo_setsum3)

   639   apply (rule ext)

   640   apply (rule setsum.cong)

   641   apply (rule refl)

   642   apply (subst abs_of_nonneg)

   643   apply auto

   644   done

   645

   646 lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>

   647     \<forall>x. 0 \<le> h x \<Longrightarrow>

   648       (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o

   649         (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o

   650           O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"

   651   apply (rule set_minus_imp_plus)

   652   apply (subst fun_diff_def)

   653   apply (subst setsum_subtractf [symmetric])

   654   apply (subst right_diff_distrib [symmetric])

   655   apply (rule bigo_setsum5)

   656   apply (subst fun_diff_def [symmetric])

   657   apply (drule set_plus_imp_minus)

   658   apply auto

   659   done

   660

   661

   662 subsection {* Misc useful stuff *}

   663

   664 lemma bigo_useful_intro: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"

   665   apply (subst bigo_plus_idemp [symmetric])

   666   apply (rule set_plus_mono2)

   667   apply assumption+

   668   done

   669

   670 lemma bigo_useful_add: "f =o O(h) \<Longrightarrow> g =o O(h) \<Longrightarrow> f + g =o O(h)"

   671   apply (subst bigo_plus_idemp [symmetric])

   672   apply (rule set_plus_intro)

   673   apply assumption+

   674   done

   675

   676 lemma bigo_useful_const_mult:

   677   fixes c :: "'a::linordered_field"

   678   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)"

   679   apply (rule subsetD)

   680   apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) \<subseteq> O(h)")

   681   apply assumption

   682   apply (rule bigo_const_mult6)

   683   apply (subgoal_tac "f = (\<lambda>x. 1 / c) * ((\<lambda>x. c) * f)")

   684   apply (erule ssubst)

   685   apply (erule set_times_intro2)

   686   apply (simp add: func_times)

   687   done

   688

   689 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)"

   690   apply (simp add: bigo_alt_def)

   691   apply auto

   692   apply (rule_tac x = c in exI)

   693   apply auto

   694   apply (case_tac "x = 0")

   695   apply simp

   696   apply (subgoal_tac "x = Suc (x - 1)")

   697   apply (erule ssubst) back

   698   apply (erule spec)

   699   apply simp

   700   done

   701

   702 lemma bigo_fix2:

   703     "(\<lambda>x. f ((x::nat) + 1)) =o (\<lambda>x. g(x + 1)) +o O(\<lambda>x. h(x + 1)) \<Longrightarrow>

   704        f 0 = g 0 \<Longrightarrow> f =o g +o O(h)"

   705   apply (rule set_minus_imp_plus)

   706   apply (rule bigo_fix)

   707   apply (subst fun_diff_def)

   708   apply (subst fun_diff_def [symmetric])

   709   apply (rule set_plus_imp_minus)

   710   apply simp

   711   apply (simp add: fun_diff_def)

   712   done

   713

   714

   715 subsection {* Less than or equal to *}

   716

   717 definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl "<o" 70)

   718   where "f <o g = (\<lambda>x. max (f x - g x) 0)"

   719

   720 lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> abs (f x) \<Longrightarrow> g =o O(h)"

   721   apply (unfold bigo_def)

   722   apply clarsimp

   723   apply (rule_tac x = c in exI)

   724   apply (rule allI)

   725   apply (rule order_trans)

   726   apply (erule spec)+

   727   done

   728

   729 lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> f x \<Longrightarrow> g =o O(h)"

   730   apply (erule bigo_lesseq1)

   731   apply (rule allI)

   732   apply (drule_tac x = x in spec)

   733   apply (rule order_trans)

   734   apply assumption

   735   apply (rule abs_ge_self)

   736   done

   737

   738 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)"

   739   apply (erule bigo_lesseq2)

   740   apply (rule allI)

   741   apply (subst abs_of_nonneg)

   742   apply (erule spec)+

   743   done

   744

   745 lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>

   746     \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> abs (f x) \<Longrightarrow> g =o O(h)"

   747   apply (erule bigo_lesseq1)

   748   apply (rule allI)

   749   apply (subst abs_of_nonneg)

   750   apply (erule spec)+

   751   done

   752

   753 lemma bigo_lesso1: "\<forall>x. f x \<le> g x \<Longrightarrow> f <o g =o O(h)"

   754   apply (unfold lesso_def)

   755   apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")

   756   apply (erule ssubst)

   757   apply (rule bigo_zero)

   758   apply (unfold func_zero)

   759   apply (rule ext)

   760   apply (simp split: split_max)

   761   done

   762

   763 lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>

   764     \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. k x \<le> f x \<Longrightarrow> k <o g =o O(h)"

   765   apply (unfold lesso_def)

   766   apply (rule bigo_lesseq4)

   767   apply (erule set_plus_imp_minus)

   768   apply (rule allI)

   769   apply (rule max.cobounded2)

   770   apply (rule allI)

   771   apply (subst fun_diff_def)

   772   apply (case_tac "0 \<le> k x - g x")

   773   apply simp

   774   apply (subst abs_of_nonneg)

   775   apply (drule_tac x = x in spec) back

   776   apply (simp add: algebra_simps)

   777   apply (subst diff_conv_add_uminus)+

   778   apply (rule add_right_mono)

   779   apply (erule spec)

   780   apply (rule order_trans)

   781   prefer 2

   782   apply (rule abs_ge_zero)

   783   apply (simp add: algebra_simps)

   784   done

   785

   786 lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>

   787     \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. g x \<le> k x \<Longrightarrow> f <o k =o O(h)"

   788   apply (unfold lesso_def)

   789   apply (rule bigo_lesseq4)

   790   apply (erule set_plus_imp_minus)

   791   apply (rule allI)

   792   apply (rule max.cobounded2)

   793   apply (rule allI)

   794   apply (subst fun_diff_def)

   795   apply (case_tac "0 \<le> f x - k x")

   796   apply simp

   797   apply (subst abs_of_nonneg)

   798   apply (drule_tac x = x in spec) back

   799   apply (simp add: algebra_simps)

   800   apply (subst diff_conv_add_uminus)+

   801   apply (rule add_left_mono)

   802   apply (rule le_imp_neg_le)

   803   apply (erule spec)

   804   apply (rule order_trans)

   805   prefer 2

   806   apply (rule abs_ge_zero)

   807   apply (simp add: algebra_simps)

   808   done

   809

   810 lemma bigo_lesso4:

   811   fixes k :: "'a \<Rightarrow> 'b::linordered_field"

   812   shows "f <o g =o O(k) \<Longrightarrow> g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)"

   813   apply (unfold lesso_def)

   814   apply (drule set_plus_imp_minus)

   815   apply (drule bigo_abs5) back

   816   apply (simp add: fun_diff_def)

   817   apply (drule bigo_useful_add)

   818   apply assumption

   819   apply (erule bigo_lesseq2) back

   820   apply (rule allI)

   821   apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)

   822   done

   823

   824 lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * abs (h x)"

   825   apply (simp only: lesso_def bigo_alt_def)

   826   apply clarsimp

   827   apply (rule_tac x = c in exI)

   828   apply (rule allI)

   829   apply (drule_tac x = x in spec)

   830   apply (subgoal_tac "abs (max (f x - g x) 0) = max (f x - g x) 0")

   831   apply (clarsimp simp add: algebra_simps)

   832   apply (rule abs_of_nonneg)

   833   apply (rule max.cobounded2)

   834   done

   835

   836 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)"

   837   apply (unfold lesso_def)

   838   apply (rule bigo_lesseq3)

   839   apply (erule bigo_useful_add)

   840   apply assumption

   841   apply (force split: split_max)

   842   apply (auto split: split_max simp add: func_plus)

   843   done

   844

   845 lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g ----> 0 \<Longrightarrow> f ----> (0::real)"

   846   apply (simp add: LIMSEQ_iff bigo_alt_def)

   847   apply clarify

   848   apply (drule_tac x = "r / c" in spec)

   849   apply (drule mp)

   850   apply simp

   851   apply clarify

   852   apply (rule_tac x = no in exI)

   853   apply (rule allI)

   854   apply (drule_tac x = n in spec)+

   855   apply (rule impI)

   856   apply (drule mp)

   857   apply assumption

   858   apply (rule order_le_less_trans)

   859   apply assumption

   860   apply (rule order_less_le_trans)

   861   apply (subgoal_tac "c * abs (g n) < c * (r / c)")

   862   apply assumption

   863   apply (erule mult_strict_left_mono)

   864   apply assumption

   865   apply simp

   866   done

   867

   868 lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h ----> 0 \<Longrightarrow> f ----> a \<Longrightarrow> g ----> (a::real)"

   869   apply (drule set_plus_imp_minus)

   870   apply (drule bigo_LIMSEQ1)

   871   apply assumption

   872   apply (simp only: fun_diff_def)

   873   apply (erule Lim_transform2)

   874   apply assumption

   875   done

   876

   877 end
`