equal
deleted
inserted
replaced
|
1 (* Title: HOL/Complex/ex/BigO_Complex.thy |
|
2 ID: $Id$ |
|
3 Authors: Jeremy Avigad and Kevin Donnelly |
|
4 *) |
|
5 |
|
6 header {* Big O notation -- continued *} |
|
7 |
|
8 theory BigO_Complex |
|
9 imports BigO Complex |
|
10 begin |
|
11 |
|
12 text {* |
|
13 Additional lemmas that require the \texttt{HOL-Complex} logic image. |
|
14 *} |
|
15 |
|
16 lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)" |
|
17 apply (simp add: LIMSEQ_def bigo_alt_def) |
|
18 apply clarify |
|
19 apply (drule_tac x = "r / c" in spec) |
|
20 apply (drule mp) |
|
21 apply (erule divide_pos_pos) |
|
22 apply assumption |
|
23 apply clarify |
|
24 apply (rule_tac x = no in exI) |
|
25 apply (rule allI) |
|
26 apply (drule_tac x = n in spec)+ |
|
27 apply (rule impI) |
|
28 apply (drule mp) |
|
29 apply assumption |
|
30 apply (rule order_le_less_trans) |
|
31 apply assumption |
|
32 apply (rule order_less_le_trans) |
|
33 apply (subgoal_tac "c * abs(g n) < c * (r / c)") |
|
34 apply assumption |
|
35 apply (erule mult_strict_left_mono) |
|
36 apply assumption |
|
37 apply simp |
|
38 done |
|
39 |
|
40 lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a |
|
41 ==> g ----> (a::real)" |
|
42 apply (drule set_plus_imp_minus) |
|
43 apply (drule bigo_LIMSEQ1) |
|
44 apply assumption |
|
45 apply (simp only: fun_diff_def) |
|
46 apply (erule LIMSEQ_diff_approach_zero2) |
|
47 apply assumption |
|
48 done |
|
49 |
|
50 end |