--- a/src/HOL/Library/BigO.thy Tue Feb 03 16:40:10 2009 +0100
+++ b/src/HOL/Library/BigO.thy Tue Feb 03 16:50:40 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/BigO.thy
- ID: $Id$
Authors: Jeremy Avigad and Kevin Donnelly
*)
header {* Big O notation *}
theory BigO
-imports Plain "~~/src/HOL/Presburger" SetsAndFunctions
+imports Complex_Main SetsAndFunctions
begin
text {*
@@ -871,4 +870,38 @@
apply (auto split: split_max simp add: func_plus)
done
+lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
+ apply (simp add: LIMSEQ_def bigo_alt_def)
+ apply clarify
+ apply (drule_tac x = "r / c" in spec)
+ apply (drule mp)
+ apply (erule divide_pos_pos)
+ apply assumption
+ apply clarify
+ apply (rule_tac x = no in exI)
+ apply (rule allI)
+ apply (drule_tac x = n in spec)+
+ apply (rule impI)
+ apply (drule mp)
+ apply assumption
+ apply (rule order_le_less_trans)
+ apply assumption
+ apply (rule order_less_le_trans)
+ apply (subgoal_tac "c * abs(g n) < c * (r / c)")
+ apply assumption
+ apply (erule mult_strict_left_mono)
+ apply assumption
+ apply simp
+done
+
+lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a
+ ==> g ----> (a::real)"
+ apply (drule set_plus_imp_minus)
+ apply (drule bigo_LIMSEQ1)
+ apply assumption
+ apply (simp only: fun_diff_def)
+ apply (erule LIMSEQ_diff_approach_zero2)
+ apply assumption
+done
+
end