changeset 74324 | 308e74afab83 |
parent 70817 | dd675800469d |
child 74543 | ee039c11fb6f |
74323:5c452041fe83 | 74324:308e74afab83 |
---|---|
1 (* |
1 (* |
2 File: Landau_Symbols_Definition.thy |
2 File: Landau_Symbols_Definition.thy |
3 Author: Manuel Eberl <eberlm@in.tum.de> |
3 Author: Manuel Eberl <eberlm@in.tum.de> |
4 |
4 |
5 Landau symbols for reasoning about the asymptotic growth of functions. |
5 Landau symbols for reasoning about the asymptotic growth of functions. |
6 *) |
6 *) |
7 section \<open>Definition of Landau symbols\<close> |
7 section \<open>Definition of Landau symbols\<close> |
8 |
8 |
9 theory Landau_Symbols |
9 theory Landau_Symbols |
10 imports |
10 imports |
11 Complex_Main |
11 Complex_Main |
12 begin |
12 begin |
13 |
13 |
14 lemma eventually_subst': |
14 lemma eventually_subst': |
15 "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> eventually (\<lambda>x. P x (f x)) F = eventually (\<lambda>x. P x (g x)) F" |
15 "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> eventually (\<lambda>x. P x (f x)) F = eventually (\<lambda>x. P x (g x)) F" |
17 |
17 |
18 |
18 |
19 subsection \<open>Definition of Landau symbols\<close> |
19 subsection \<open>Definition of Landau symbols\<close> |
20 |
20 |
21 text \<open> |
21 text \<open> |
22 Our Landau symbols are sign-oblivious, i.e. any function always has the same growth |
22 Our Landau symbols are sign-oblivious, i.e. any function always has the same growth |
23 as its absolute. This has the advantage of making some cancelling rules for sums nicer, but |
23 as its absolute. This has the advantage of making some cancelling rules for sums nicer, but |
24 introduces some problems in other places. Nevertheless, we found this definition more convenient |
24 introduces some problems in other places. Nevertheless, we found this definition more convenient |
25 to work with. |
25 to work with. |
26 \<close> |
26 \<close> |
27 |
27 |
28 definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
28 definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
29 (\<open>(1O[_]'(_'))\<close>) |
29 (\<open>(1O[_]'(_'))\<close>) |
30 where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}" |
30 where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}" |
31 |
31 |
32 definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
32 definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
33 (\<open>(1o[_]'(_'))\<close>) |
33 (\<open>(1o[_]'(_'))\<close>) |
34 where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}" |
34 where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}" |
35 |
35 |
36 definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
36 definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
37 (\<open>(1\<Omega>[_]'(_'))\<close>) |
37 (\<open>(1\<Omega>[_]'(_'))\<close>) |
38 where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}" |
38 where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}" |
39 |
39 |
40 definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
40 definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
41 (\<open>(1\<omega>[_]'(_'))\<close>) |
41 (\<open>(1\<omega>[_]'(_'))\<close>) |
42 where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}" |
42 where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}" |
43 |
43 |
44 definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
44 definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
45 (\<open>(1\<Theta>[_]'(_'))\<close>) |
45 (\<open>(1\<Theta>[_]'(_'))\<close>) |
46 where "bigtheta F g = bigo F g \<inter> bigomega F g" |
46 where "bigtheta F g = bigo F g \<inter> bigomega F g" |
47 |
47 |
48 abbreviation bigo_at_top (\<open>(2O'(_'))\<close>) where |
48 abbreviation bigo_at_top (\<open>(2O'(_'))\<close>) where |
49 "O(g) \<equiv> bigo at_top g" |
49 "O(g) \<equiv> bigo at_top g" |
50 |
50 |
51 abbreviation smallo_at_top (\<open>(2o'(_'))\<close>) where |
51 abbreviation smallo_at_top (\<open>(2o'(_'))\<close>) where |
52 "o(g) \<equiv> smallo at_top g" |
52 "o(g) \<equiv> smallo at_top g" |
53 |
53 |
54 abbreviation bigomega_at_top (\<open>(2\<Omega>'(_'))\<close>) where |
54 abbreviation bigomega_at_top (\<open>(2\<Omega>'(_'))\<close>) where |
57 abbreviation smallomega_at_top (\<open>(2\<omega>'(_'))\<close>) where |
57 abbreviation smallomega_at_top (\<open>(2\<omega>'(_'))\<close>) where |
58 "\<omega>(g) \<equiv> smallomega at_top g" |
58 "\<omega>(g) \<equiv> smallomega at_top g" |
59 |
59 |
60 abbreviation bigtheta_at_top (\<open>(2\<Theta>'(_'))\<close>) where |
60 abbreviation bigtheta_at_top (\<open>(2\<Theta>'(_'))\<close>) where |
61 "\<Theta>(g) \<equiv> bigtheta at_top g" |
61 "\<Theta>(g) \<equiv> bigtheta at_top g" |
62 |
62 |
63 |
63 |
64 text \<open>The following is a set of properties that all Landau symbols satisfy.\<close> |
64 text \<open>The following is a set of properties that all Landau symbols satisfy.\<close> |
65 |
65 |
66 named_theorems landau_divide_simps |
66 named_theorems landau_divide_simps |
67 |
67 |
69 fixes L :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
69 fixes L :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
70 and L' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set" |
70 and L' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set" |
71 and Lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set" |
71 and Lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set" |
72 assumes bot': "L bot f = UNIV" |
72 assumes bot': "L bot f = UNIV" |
73 assumes filter_mono': "F1 \<le> F2 \<Longrightarrow> L F2 f \<subseteq> L F1 f" |
73 assumes filter_mono': "F1 \<le> F2 \<Longrightarrow> L F2 f \<subseteq> L F1 f" |
74 assumes in_filtermap_iff: |
74 assumes in_filtermap_iff: |
75 "f' \<in> L (filtermap h' F') g' \<longleftrightarrow> (\<lambda>x. f' (h' x)) \<in> L' F' (\<lambda>x. g' (h' x))" |
75 "f' \<in> L (filtermap h' F') g' \<longleftrightarrow> (\<lambda>x. f' (h' x)) \<in> L' F' (\<lambda>x. g' (h' x))" |
76 assumes filtercomap: |
76 assumes filtercomap: |
77 "f' \<in> L F'' g' \<Longrightarrow> (\<lambda>x. f' (h' x)) \<in> L' (filtercomap h' F'') (\<lambda>x. g' (h' x))" |
77 "f' \<in> L F'' g' \<Longrightarrow> (\<lambda>x. f' (h' x)) \<in> L' (filtercomap h' F'') (\<lambda>x. g' (h' x))" |
78 assumes sup: "f \<in> L F1 g \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L (sup F1 F2) g" |
78 assumes sup: "f \<in> L F1 g \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L (sup F1 F2) g" |
79 assumes in_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" |
79 assumes in_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" |
80 assumes cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> L F (f) = L F (g)" |
80 assumes cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> L F (f) = L F (g)" |
81 assumes cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> L F (f) = L F (g)" |
81 assumes cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> L F (f) = L F (g)" |
82 assumes in_cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" |
82 assumes in_cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" |
83 assumes cmult [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. c * f x) = L F (f)" |
83 assumes cmult [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. c * f x) = L F (f)" |
84 assumes cmult_in_iff [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)" |
84 assumes cmult_in_iff [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)" |
85 assumes mult_left [simp]: "f \<in> L F (g) \<Longrightarrow> (\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" |
85 assumes mult_left [simp]: "f \<in> L F (g) \<Longrightarrow> (\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" |
86 assumes inverse: "eventually (\<lambda>x. f x \<noteq> 0) F \<Longrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F \<Longrightarrow> |
86 assumes inverse: "eventually (\<lambda>x. f x \<noteq> 0) F \<Longrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F \<Longrightarrow> |
87 f \<in> L F (g) \<Longrightarrow> (\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))" |
87 f \<in> L F (g) \<Longrightarrow> (\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))" |
88 assumes subsetI: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)" |
88 assumes subsetI: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)" |
89 assumes plus_subset1: "f \<in> o[F](g) \<Longrightarrow> L F (g) \<subseteq> L F (\<lambda>x. f x + g x)" |
89 assumes plus_subset1: "f \<in> o[F](g) \<Longrightarrow> L F (g) \<subseteq> L F (\<lambda>x. f x + g x)" |
90 assumes trans: "f \<in> L F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)" |
90 assumes trans: "f \<in> L F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)" |
91 assumes compose: "f \<in> L F (g) \<Longrightarrow> filterlim h' F G \<Longrightarrow> (\<lambda>x. f (h' x)) \<in> L' G (\<lambda>x. g (h' x))" |
91 assumes compose: "f \<in> L F (g) \<Longrightarrow> filterlim h' F G \<Longrightarrow> (\<lambda>x. f (h' x)) \<in> L' G (\<lambda>x. g (h' x))" |
93 assumes abs [simp]: "Lr Fr (\<lambda>x. \<bar>fr x\<bar>) = Lr Fr fr" |
93 assumes abs [simp]: "Lr Fr (\<lambda>x. \<bar>fr x\<bar>) = Lr Fr fr" |
94 assumes abs_in_iff [simp]: "(\<lambda>x. \<bar>fr x\<bar>) \<in> Lr Fr gr \<longleftrightarrow> fr \<in> Lr Fr gr" |
94 assumes abs_in_iff [simp]: "(\<lambda>x. \<bar>fr x\<bar>) \<in> Lr Fr gr \<longleftrightarrow> fr \<in> Lr Fr gr" |
95 begin |
95 begin |
96 |
96 |
97 lemma bot [simp]: "f \<in> L bot g" by (simp add: bot') |
97 lemma bot [simp]: "f \<in> L bot g" by (simp add: bot') |
98 |
98 |
99 lemma filter_mono: "F1 \<le> F2 \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L F1 g" |
99 lemma filter_mono: "F1 \<le> F2 \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L F1 g" |
100 using filter_mono'[of F1 F2] by blast |
100 using filter_mono'[of F1 F2] by blast |
101 |
101 |
102 lemma cong_ex: |
102 lemma cong_ex: |
103 "eventually (\<lambda>x. f1 x = f2 x) F \<Longrightarrow> eventually (\<lambda>x. g1 x = g2 x) F \<Longrightarrow> |
103 "eventually (\<lambda>x. f1 x = f2 x) F \<Longrightarrow> eventually (\<lambda>x. g1 x = g2 x) F \<Longrightarrow> |
104 f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" |
104 f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" |
105 by (subst cong, assumption, subst in_cong, assumption, rule refl) |
105 by (subst cong, assumption, subst in_cong, assumption, rule refl) |
106 |
106 |
107 lemma cong_ex_bigtheta: |
107 lemma cong_ex_bigtheta: |
108 "f1 \<in> \<Theta>[F](f2) \<Longrightarrow> g1 \<in> \<Theta>[F](g2) \<Longrightarrow> f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" |
108 "f1 \<in> \<Theta>[F](f2) \<Longrightarrow> g1 \<in> \<Theta>[F](g2) \<Longrightarrow> f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" |
109 by (subst cong_bigtheta, assumption, subst in_cong_bigtheta, assumption, rule refl) |
109 by (subst cong_bigtheta, assumption, subst in_cong_bigtheta, assumption, rule refl) |
110 |
110 |
111 lemma bigtheta_trans1: |
111 lemma bigtheta_trans1: |
112 "f \<in> L F (g) \<Longrightarrow> g \<in> \<Theta>[F](h) \<Longrightarrow> f \<in> L F (h)" |
112 "f \<in> L F (g) \<Longrightarrow> g \<in> \<Theta>[F](h) \<Longrightarrow> f \<in> L F (h)" |
113 by (subst cong_bigtheta[symmetric]) |
113 by (subst cong_bigtheta[symmetric]) |
114 |
114 |
115 lemma bigtheta_trans2: |
115 lemma bigtheta_trans2: |
116 "f \<in> \<Theta>[F](g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)" |
116 "f \<in> \<Theta>[F](g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)" |
117 by (subst in_cong_bigtheta) |
117 by (subst in_cong_bigtheta) |
118 |
118 |
119 lemma cmult' [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x * c) = L F (f)" |
119 lemma cmult' [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x * c) = L F (f)" |
120 by (subst mult.commute) (rule cmult) |
120 by (subst mult.commute) (rule cmult) |
121 |
121 |
122 lemma cmult_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x * c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)" |
122 lemma cmult_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x * c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)" |
123 by (subst mult.commute) (rule cmult_in_iff) |
123 by (subst mult.commute) (rule cmult_in_iff) |
125 lemma cdiv [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x / c) = L F (f)" |
125 lemma cdiv [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x / c) = L F (f)" |
126 using cmult'[of "inverse c" F f] by (simp add: field_simps) |
126 using cmult'[of "inverse c" F f] by (simp add: field_simps) |
127 |
127 |
128 lemma cdiv_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)" |
128 lemma cdiv_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)" |
129 using cmult_in_iff'[of "inverse c" f] by (simp add: field_simps) |
129 using cmult_in_iff'[of "inverse c" f] by (simp add: field_simps) |
130 |
130 |
131 lemma uminus [simp]: "L F (\<lambda>x. -g x) = L F (g)" using cmult[of "-1"] by simp |
131 lemma uminus [simp]: "L F (\<lambda>x. -g x) = L F (g)" using cmult[of "-1"] by simp |
132 |
132 |
133 lemma uminus_in_iff [simp]: "(\<lambda>x. -f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)" |
133 lemma uminus_in_iff [simp]: "(\<lambda>x. -f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)" |
134 using cmult_in_iff[of "-1"] by simp |
134 using cmult_in_iff[of "-1"] by simp |
135 |
135 |
205 assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F" |
205 assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F" |
206 assumes "eventually (\<lambda>x. g2 x \<noteq> 0) F" |
206 assumes "eventually (\<lambda>x. g2 x \<noteq> 0) F" |
207 assumes "f1 \<in> L F (f2)" "g2 \<in> L F (g1)" |
207 assumes "f1 \<in> L F (f2)" "g2 \<in> L F (g1)" |
208 shows "(\<lambda>x. f1 x / g1 x) \<in> L F (\<lambda>x. f2 x / g2 x)" |
208 shows "(\<lambda>x. f1 x / g1 x) \<in> L F (\<lambda>x. f2 x / g2 x)" |
209 by (subst (1 2) divide_inverse) (intro mult inverse assms) |
209 by (subst (1 2) divide_inverse) (intro mult inverse assms) |
210 |
210 |
211 lemma divide_eq1: |
211 lemma divide_eq1: |
212 assumes "eventually (\<lambda>x. h x \<noteq> 0) F" |
212 assumes "eventually (\<lambda>x. h x \<noteq> 0) F" |
213 shows "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)" |
213 shows "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)" |
214 proof- |
214 proof- |
215 have "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x / h x) \<in> L F (\<lambda>x. g x / h x)" |
215 have "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x / h x) \<in> L F (\<lambda>x. g x / h x)" |
282 |
282 |
283 lemma (in landau_symbol) of_real_iff: |
283 lemma (in landau_symbol) of_real_iff: |
284 "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<longleftrightarrow> f \<in> Lr F g" |
284 "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<longleftrightarrow> f \<in> Lr F g" |
285 by (subst norm_iff [symmetric], subst (1 2) norm_of_real) simp_all |
285 by (subst norm_iff [symmetric], subst (1 2) norm_of_real) simp_all |
286 |
286 |
287 lemmas [landau_divide_simps] = |
287 lemmas [landau_divide_simps] = |
288 inverse_cancel divide_left_iff divide_eq1 divide_eq2 inverse_eq1 inverse_eq2 |
288 inverse_cancel divide_left_iff divide_eq1 divide_eq2 inverse_eq1 inverse_eq2 |
289 |
289 |
290 end |
290 end |
291 |
291 |
292 |
292 |
293 text \<open> |
293 text \<open> |
294 The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with |
294 The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with |
295 $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem. |
295 $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem. |
296 The following locale captures this fact. |
296 The following locale captures this fact. |
297 \<close> |
297 \<close> |
298 |
298 |
299 locale landau_pair = |
299 locale landau_pair = |
300 fixes L l :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
300 fixes L l :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
301 fixes L' l' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set" |
301 fixes L' l' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set" |
302 fixes Lr lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set" |
302 fixes Lr lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set" |
303 and R :: "real \<Rightarrow> real \<Rightarrow> bool" |
303 and R :: "real \<Rightarrow> real \<Rightarrow> bool" |
304 assumes L_def: "L F g = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}" |
304 assumes L_def: "L F g = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}" |
307 and l'_def: "l' F' g' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}" |
307 and l'_def: "l' F' g' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}" |
308 and Lr_def: "Lr F'' g'' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}" |
308 and Lr_def: "Lr F'' g'' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}" |
309 and lr_def: "lr F'' g'' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}" |
309 and lr_def: "lr F'' g'' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}" |
310 and R: "R = (\<le>) \<or> R = (\<ge>)" |
310 and R: "R = (\<le>) \<or> R = (\<ge>)" |
311 |
311 |
312 interpretation landau_o: |
312 interpretation landau_o: |
313 landau_pair bigo smallo bigo smallo bigo smallo "(\<le>)" |
313 landau_pair bigo smallo bigo smallo bigo smallo "(\<le>)" |
314 by unfold_locales (auto simp: bigo_def smallo_def intro!: ext) |
314 by unfold_locales (auto simp: bigo_def smallo_def intro!: ext) |
315 |
315 |
316 interpretation landau_omega: |
316 interpretation landau_omega: |
317 landau_pair bigomega smallomega bigomega smallomega bigomega smallomega "(\<ge>)" |
317 landau_pair bigomega smallomega bigomega smallomega bigomega smallomega "(\<ge>)" |
318 by unfold_locales (auto simp: bigomega_def smallomega_def intro!: ext) |
318 by unfold_locales (auto simp: bigomega_def smallomega_def intro!: ext) |
319 |
319 |
320 |
320 |
321 context landau_pair |
321 context landau_pair |
337 unfolding l_def by blast |
337 unfolding l_def by blast |
338 |
338 |
339 lemma smallD: |
339 lemma smallD: |
340 "f \<in> l F (g) \<Longrightarrow> c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F" |
340 "f \<in> l F (g) \<Longrightarrow> c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F" |
341 unfolding l_def by blast |
341 unfolding l_def by blast |
342 |
342 |
343 lemma bigE_nonneg_real: |
343 lemma bigE_nonneg_real: |
344 assumes "f \<in> Lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F" |
344 assumes "f \<in> Lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F" |
345 obtains c where "c > 0" "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F" |
345 obtains c where "c > 0" "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F" |
346 proof- |
346 proof- |
347 from assms(1) obtain c where c: "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F" |
347 from assms(1) obtain c where c: "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F" |
356 shows "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F" |
356 shows "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F" |
357 using assms by (auto simp: lr_def dest!: spec[of _ c] elim: eventually_elim2) |
357 using assms by (auto simp: lr_def dest!: spec[of _ c] elim: eventually_elim2) |
358 |
358 |
359 lemma small_imp_big: "f \<in> l F (g) \<Longrightarrow> f \<in> L F (g)" |
359 lemma small_imp_big: "f \<in> l F (g) \<Longrightarrow> f \<in> L F (g)" |
360 by (rule bigI[OF _ smallD, of 1]) simp_all |
360 by (rule bigI[OF _ smallD, of 1]) simp_all |
361 |
361 |
362 lemma small_subset_big: "l F (g) \<subseteq> L F (g)" |
362 lemma small_subset_big: "l F (g) \<subseteq> L F (g)" |
363 using small_imp_big by blast |
363 using small_imp_big by blast |
364 |
364 |
365 lemma R_refl [simp]: "R x x" using R by auto |
365 lemma R_refl [simp]: "R x x" using R by auto |
366 |
366 |
378 |
378 |
379 lemma big_trans: |
379 lemma big_trans: |
380 assumes "f \<in> L F (g)" "g \<in> L F (h)" |
380 assumes "f \<in> L F (g)" "g \<in> L F (h)" |
381 shows "f \<in> L F (h)" |
381 shows "f \<in> L F (h)" |
382 proof- |
382 proof- |
383 from assms(1) guess c by (elim bigE) note c = this |
383 from assms obtain c d where *: "0 < c" "0 < d" |
384 from assms(2) guess d by (elim bigE) note d = this |
384 and **: "\<forall>\<^sub>F x in F. R (norm (f x)) (c * norm (g x))" |
385 from c(2) d(2) have "eventually (\<lambda>x. R (norm (f x)) (c * d * (norm (h x)))) F" |
385 "\<forall>\<^sub>F x in F. R (norm (g x)) (d * norm (h x))" |
386 by (elim bigE) |
|
387 from ** have "eventually (\<lambda>x. R (norm (f x)) (c * d * (norm (h x)))) F" |
|
386 proof eventually_elim |
388 proof eventually_elim |
387 fix x assume "R (norm (f x)) (c * (norm (g x)))" |
389 fix x assume "R (norm (f x)) (c * (norm (g x)))" |
388 also assume "R (norm (g x)) (d * (norm (h x)))" |
390 also assume "R (norm (g x)) (d * (norm (h x)))" |
389 with c(1) have "R (c * (norm (g x))) (c * (d * (norm (h x))))" |
391 with \<open>0 < c\<close> have "R (c * (norm (g x))) (c * (d * (norm (h x))))" |
390 by (intro R_mult_left_mono) simp_all |
392 by (intro R_mult_left_mono) simp_all |
391 finally show "R (norm (f x)) (c * d * (norm (h x)))" by (simp add: algebra_simps) |
393 finally show "R (norm (f x)) (c * d * (norm (h x)))" |
392 qed |
394 by (simp add: algebra_simps) |
393 with c(1) d(1) show ?thesis by (intro bigI[of "c*d"]) simp_all |
395 qed |
396 with * show ?thesis by (intro bigI[of "c*d"]) simp_all |
|
394 qed |
397 qed |
395 |
398 |
396 lemma big_small_trans: |
399 lemma big_small_trans: |
397 assumes "f \<in> L F (g)" "g \<in> l F (h)" |
400 assumes "f \<in> L F (g)" "g \<in> l F (h)" |
398 shows "f \<in> l F (h)" |
401 shows "f \<in> l F (h)" |
399 proof (rule smallI) |
402 proof (rule smallI) |
400 fix c :: real assume c: "c > 0" |
403 fix c :: real assume c: "c > 0" |
401 from assms(1) guess d by (elim bigE) note d = this |
404 from assms(1) obtain d where d: "d > 0" and *: "\<forall>\<^sub>F x in F. R (norm (f x)) (d * norm (g x))" |
402 note d(2) |
405 by (elim bigE) |
403 moreover from c d assms(2) |
406 from assms(2) c d have "eventually (\<lambda>x. R (norm (g x)) (c * inverse d * norm (h x))) F" |
404 have "eventually (\<lambda>x. R (norm (g x)) (c * inverse d * norm (h x))) F" |
|
405 by (intro smallD) simp_all |
407 by (intro smallD) simp_all |
406 ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * (norm (h x)))) F" |
408 with * show "eventually (\<lambda>x. R (norm (f x)) (c * (norm (h x)))) F" |
407 by eventually_elim (erule R_trans, insert R d(1), auto simp: field_simps) |
409 proof eventually_elim |
410 case (elim x) |
|
411 show ?case |
|
412 by (use elim(1) in \<open>rule R_trans\<close>) (use elim(2) R d in \<open>auto simp: field_simps\<close>) |
|
413 qed |
|
408 qed |
414 qed |
409 |
415 |
410 lemma small_big_trans: |
416 lemma small_big_trans: |
411 assumes "f \<in> l F (g)" "g \<in> L F (h)" |
417 assumes "f \<in> l F (g)" "g \<in> L F (h)" |
412 shows "f \<in> l F (h)" |
418 shows "f \<in> l F (h)" |
413 proof (rule smallI) |
419 proof (rule smallI) |
414 fix c :: real assume c: "c > 0" |
420 fix c :: real assume c: "c > 0" |
415 from assms(2) guess d by (elim bigE) note d = this |
421 from assms(2) obtain d where d: "d > 0" and *: "\<forall>\<^sub>F x in F. R (norm (g x)) (d * norm (h x))" |
416 note d(2) |
422 by (elim bigE) |
417 moreover from c d assms(1) |
423 from assms(1) c d have "eventually (\<lambda>x. R (norm (f x)) (c * inverse d * norm (g x))) F" |
418 have "eventually (\<lambda>x. R (norm (f x)) (c * inverse d * norm (g x))) F" |
|
419 by (intro smallD) simp_all |
424 by (intro smallD) simp_all |
420 ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * norm (h x))) F" |
425 with * show "eventually (\<lambda>x. R (norm (f x)) (c * norm (h x))) F" |
421 by eventually_elim (rotate_tac 2, erule R_trans, insert R c d(1), auto simp: field_simps) |
426 by eventually_elim (rotate_tac 2, erule R_trans, insert R c d, auto simp: field_simps) |
422 qed |
427 qed |
423 |
428 |
424 lemma small_trans: |
429 lemma small_trans: |
425 "f \<in> l F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> l F (h)" |
430 "f \<in> l F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> l F (h)" |
426 by (rule big_small_trans[OF small_imp_big]) |
431 by (rule big_small_trans[OF small_imp_big]) |
466 |
471 |
467 lemma plus_aux: |
472 lemma plus_aux: |
468 assumes "f \<in> o[F](g)" |
473 assumes "f \<in> o[F](g)" |
469 shows "g \<in> L F (\<lambda>x. f x + g x)" |
474 shows "g \<in> L F (\<lambda>x. f x + g x)" |
470 proof (rule R_E) |
475 proof (rule R_E) |
471 assume [simp]: "R = (\<le>)" |
476 assume R: "R = (\<le>)" |
472 have A: "1/2 > (0::real)" by simp |
477 have A: "1/2 > (0::real)" by simp |
473 { |
478 have B: "1/2 * (norm (g x)) \<le> norm (f x + g x)" |
474 fix x assume "norm (f x) \<le> 1/2 * norm (g x)" |
479 if "norm (f x) \<le> 1/2 * norm (g x)" for x |
475 hence "1/2 * (norm (g x)) \<le> (norm (g x)) - (norm (f x))" by simp |
480 proof - |
481 from that have "1/2 * (norm (g x)) \<le> (norm (g x)) - (norm (f x))" |
|
482 by simp |
|
476 also have "norm (g x) - norm (f x) \<le> norm (f x + g x)" |
483 also have "norm (g x) - norm (f x) \<le> norm (f x + g x)" |
477 by (subst add.commute) (rule norm_diff_ineq) |
484 by (subst add.commute) (rule norm_diff_ineq) |
478 finally have "1/2 * (norm (g x)) \<le> norm (f x + g x)" by simp |
485 finally show ?thesis by simp |
479 } note B = this |
486 qed |
480 |
|
481 show "g \<in> L F (\<lambda>x. f x + g x)" |
487 show "g \<in> L F (\<lambda>x. f x + g x)" |
482 apply (rule bigI[of "2"], simp) |
488 apply (rule bigI[of "2"]) |
483 using landau_o.smallD[OF assms A] apply eventually_elim |
489 apply simp |
484 using B apply (simp add: algebra_simps) |
490 apply (use landau_o.smallD[OF assms A] in eventually_elim) |
491 apply (use B in \<open>simp add: R algebra_simps\<close>) |
|
485 done |
492 done |
486 next |
493 next |
487 assume [simp]: "R = (\<lambda>x y. x \<ge> y)" |
494 assume R: "R = (\<lambda>x y. x \<ge> y)" |
488 show "g \<in> L F (\<lambda>x. f x + g x)" |
495 show "g \<in> L F (\<lambda>x. f x + g x)" |
489 proof (rule bigI[of "1/2"]) |
496 proof (rule bigI[of "1/2"]) |
490 show "eventually (\<lambda>x. R (norm (g x)) (1/2 * norm (f x + g x))) F" |
497 show "eventually (\<lambda>x. R (norm (g x)) (1/2 * norm (f x + g x))) F" |
491 using landau_o.smallD[OF assms zero_less_one] |
498 using landau_o.smallD[OF assms zero_less_one] |
492 proof eventually_elim |
499 proof eventually_elim |
493 case (elim x) |
500 case (elim x) |
494 have "norm (f x + g x) \<le> norm (f x) + norm (g x)" by (rule norm_triangle_ineq) |
501 have "norm (f x + g x) \<le> norm (f x) + norm (g x)" |
502 by (rule norm_triangle_ineq) |
|
495 also note elim |
503 also note elim |
496 finally show ?case by simp |
504 finally show ?case by (simp add: R) |
497 qed |
505 qed |
498 qed simp_all |
506 qed simp_all |
499 qed |
507 qed |
500 |
508 |
501 end |
509 end |
502 |
|
503 |
510 |
504 |
511 |
505 lemma bigomega_iff_bigo: "g \<in> \<Omega>[F](f) \<longleftrightarrow> f \<in> O[F](g)" |
512 lemma bigomega_iff_bigo: "g \<in> \<Omega>[F](f) \<longleftrightarrow> f \<in> O[F](g)" |
506 proof |
513 proof |
507 assume "f \<in> O[F](g)" |
514 assume "f \<in> O[F](g)" |
508 then guess c by (elim landau_o.bigE) |
515 then obtain c where "0 < c" "\<forall>\<^sub>F x in F. norm (f x) \<le> c * norm (g x)" |
509 thus "g \<in> \<Omega>[F](f)" by (intro landau_omega.bigI[of "inverse c"]) (simp_all add: field_simps) |
516 by (rule landau_o.bigE) |
517 then show "g \<in> \<Omega>[F](f)" |
|
518 by (intro landau_omega.bigI[of "inverse c"]) (simp_all add: field_simps) |
|
510 next |
519 next |
511 assume "g \<in> \<Omega>[F](f)" |
520 assume "g \<in> \<Omega>[F](f)" |
512 then guess c by (elim landau_omega.bigE) |
521 then obtain c where "0 < c" "\<forall>\<^sub>F x in F. c * norm (f x) \<le> norm (g x)" |
513 thus "f \<in> O[F](g)" by (intro landau_o.bigI[of "inverse c"]) (simp_all add: field_simps) |
522 by (rule landau_omega.bigE) |
523 then show "f \<in> O[F](g)" |
|
524 by (intro landau_o.bigI[of "inverse c"]) (simp_all add: field_simps) |
|
514 qed |
525 qed |
515 |
526 |
516 lemma smallomega_iff_smallo: "g \<in> \<omega>[F](f) \<longleftrightarrow> f \<in> o[F](g)" |
527 lemma smallomega_iff_smallo: "g \<in> \<omega>[F](f) \<longleftrightarrow> f \<in> o[F](g)" |
517 proof |
528 proof |
518 assume "f \<in> o[F](g)" |
529 assume "f \<in> o[F](g)" |
534 |
545 |
535 lemma big_mult: |
546 lemma big_mult: |
536 assumes "f1 \<in> L F (g1)" "f2 \<in> L F (g2)" |
547 assumes "f1 \<in> L F (g1)" "f2 \<in> L F (g2)" |
537 shows "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" |
548 shows "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" |
538 proof- |
549 proof- |
539 from assms(1) guess c1 by (elim bigE) note c1 = this |
550 from assms obtain c1 c2 where *: "c1 > 0" "c2 > 0" |
540 from assms(2) guess c2 by (elim bigE) note c2 = this |
551 and **: "\<forall>\<^sub>F x in F. R (norm (f1 x)) (c1 * norm (g1 x))" |
541 |
552 "\<forall>\<^sub>F x in F. R (norm (f2 x)) (c2 * norm (g2 x))" |
542 from c1(1) and c2(1) have "c1 * c2 > 0" by simp |
553 by (elim bigE) |
554 from * have "c1 * c2 > 0" by simp |
|
543 moreover have "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * c2 * norm (g1 x * g2 x))) F" |
555 moreover have "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * c2 * norm (g1 x * g2 x))) F" |
544 using c1(2) c2(2) |
556 using ** |
545 proof eventually_elim |
557 proof eventually_elim |
546 case (elim x) |
558 case (elim x) |
547 show ?case |
559 show ?case |
548 proof (cases rule: R_E) |
560 proof (cases rule: R_E) |
549 case le |
561 case le |
550 have "norm (f1 x) * norm (f2 x) \<le> (c1 * norm (g1 x)) * (c2 * norm (g2 x))" |
562 have "norm (f1 x) * norm (f2 x) \<le> (c1 * norm (g1 x)) * (c2 * norm (g2 x))" |
551 using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto |
563 using elim le * by (intro mult_mono mult_nonneg_nonneg) auto |
552 with le show ?thesis by (simp add: le norm_mult mult_ac) |
564 with le show ?thesis by (simp add: le norm_mult mult_ac) |
553 next |
565 next |
554 case ge |
566 case ge |
555 have "(c1 * norm (g1 x)) * (c2 * norm (g2 x)) \<le> norm (f1 x) * norm (f2 x)" |
567 have "(c1 * norm (g1 x)) * (c2 * norm (g2 x)) \<le> norm (f1 x) * norm (f2 x)" |
556 using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto |
568 using elim ge * by (intro mult_mono mult_nonneg_nonneg) auto |
557 with ge show ?thesis by (simp_all add: norm_mult mult_ac) |
569 with ge show ?thesis by (simp_all add: norm_mult mult_ac) |
558 qed |
570 qed |
559 qed |
571 qed |
560 ultimately show ?thesis by (rule bigI) |
572 ultimately show ?thesis by (rule bigI) |
561 qed |
573 qed |
563 lemma small_big_mult: |
575 lemma small_big_mult: |
564 assumes "f1 \<in> l F (g1)" "f2 \<in> L F (g2)" |
576 assumes "f1 \<in> l F (g1)" "f2 \<in> L F (g2)" |
565 shows "(\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)" |
577 shows "(\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)" |
566 proof (rule smallI) |
578 proof (rule smallI) |
567 fix c1 :: real assume c1: "c1 > 0" |
579 fix c1 :: real assume c1: "c1 > 0" |
568 from assms(2) guess c2 by (elim bigE) note c2 = this |
580 from assms(2) obtain c2 where c2: "c2 > 0" |
569 with c1 assms(1) have "eventually (\<lambda>x. R (norm (f1 x)) (c1 * inverse c2 * norm (g1 x))) F" |
581 and *: "\<forall>\<^sub>F x in F. R (norm (f2 x)) (c2 * norm (g2 x))" by (elim bigE) |
582 from assms(1) c1 c2 have "eventually (\<lambda>x. R (norm (f1 x)) (c1 * inverse c2 * norm (g1 x))) F" |
|
570 by (auto intro!: smallD) |
583 by (auto intro!: smallD) |
571 thus "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * norm (g1 x * g2 x))) F" using c2(2) |
584 with * show "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * norm (g1 x * g2 x))) F" |
572 proof eventually_elim |
585 proof eventually_elim |
573 case (elim x) |
586 case (elim x) |
574 show ?case |
587 show ?case |
575 proof (cases rule: R_E) |
588 proof (cases rule: R_E) |
576 case le |
589 case le |
577 have "norm (f1 x) * norm (f2 x) \<le> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))" |
590 have "norm (f1 x) * norm (f2 x) \<le> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))" |
578 using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto |
591 using elim le c1 c2 by (intro mult_mono mult_nonneg_nonneg) auto |
579 with le c2(1) show ?thesis by (simp add: le norm_mult field_simps) |
592 with le c2 show ?thesis by (simp add: le norm_mult field_simps) |
580 next |
593 next |
581 case ge |
594 case ge |
582 have "norm (f1 x) * norm (f2 x) \<ge> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))" |
595 have "norm (f1 x) * norm (f2 x) \<ge> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))" |
583 using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto |
596 using elim ge c1 c2 by (intro mult_mono mult_nonneg_nonneg) auto |
584 with ge c2(1) show ?thesis by (simp add: ge norm_mult field_simps) |
597 with ge c2 show ?thesis by (simp add: ge norm_mult field_simps) |
585 qed |
598 qed |
586 qed |
599 qed |
587 qed |
600 qed |
588 |
601 |
589 lemma big_small_mult: |
602 lemma big_small_mult: |
590 "f1 \<in> L F (g1) \<Longrightarrow> f2 \<in> l F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)" |
603 "f1 \<in> L F (g1) \<Longrightarrow> f2 \<in> l F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)" |
591 by (subst (1 2) mult.commute) (rule small_big_mult) |
604 by (subst (1 2) mult.commute) (rule small_big_mult) |
592 |
605 |
593 lemma small_mult: "f1 \<in> l F (g1) \<Longrightarrow> f2 \<in> l F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)" |
606 lemma small_mult: "f1 \<in> l F (g1) \<Longrightarrow> f2 \<in> l F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)" |
594 by (rule small_big_mult, assumption, rule small_imp_big) |
607 by (rule small_big_mult, assumption, rule small_imp_big) |
598 |
611 |
599 sublocale big: landau_symbol L L' Lr |
612 sublocale big: landau_symbol L L' Lr |
600 proof |
613 proof |
601 have L: "L = bigo \<or> L = bigomega" |
614 have L: "L = bigo \<or> L = bigomega" |
602 by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff) |
615 by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff) |
603 { |
616 have A: "(\<lambda>x. c * f x) \<in> L F f" if "c \<noteq> 0" for c :: 'b and F and f :: "'a \<Rightarrow> 'b" |
604 fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0" |
617 using that by (intro bigI[of "norm c"]) (simp_all add: norm_mult) |
605 hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult) |
618 show "L F (\<lambda>x. c * f x) = L F f" if "c \<noteq> 0" for c :: 'b and F and f :: "'a \<Rightarrow> 'b" |
606 } note A = this |
619 using \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] |
607 { |
620 by (intro equalityI big_subsetI) (simp_all add: field_simps) |
608 fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0" |
621 show "((\<lambda>x. c * f x) \<in> L F g) = (f \<in> L F g)" if "c \<noteq> 0" |
609 from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] |
622 for c :: 'b and F and f g :: "'a \<Rightarrow> 'b" |
610 show "L F (\<lambda>x. c * f x) = L F f" by (intro equalityI big_subsetI) (simp_all add: field_simps) |
623 proof - |
611 } |
|
612 { |
|
613 fix c :: 'b and F and f g :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0" |
|
614 from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] |
624 from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] |
615 have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps) |
625 have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" |
616 thus "((\<lambda>x. c * f x) \<in> L F g) = (f \<in> L F g)" by (intro iffI) (erule (1) big_trans)+ |
626 by (simp_all add: field_simps) |
617 } |
627 then show ?thesis by (intro iffI) (erule (1) big_trans)+ |
618 { |
628 qed |
619 fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> L F (g)" |
629 show "(\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))" |
620 assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F" |
630 if *: "f \<in> L F (g)" and **: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F" |
621 from A guess c by (elim bigE) note c = this |
631 for f g :: "'a \<Rightarrow> 'b" and F |
622 from c(2) B have "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F" |
632 proof - |
623 by eventually_elim (rule R_E, insert c(1), simp_all add: field_simps norm_inverse norm_divide) |
633 from * obtain c where c: "c > 0" and ***: "\<forall>\<^sub>F x in F. R (norm (f x)) (c * norm (g x))" |
624 with c(1) show "(\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))" by (rule bigI) |
634 by (elim bigE) |
625 } |
635 from ** *** have "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F" |
626 { |
636 by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide c) |
627 fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)" |
637 with c show ?thesis by (rule bigI) |
628 with plus_aux show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" by (blast intro!: big_subsetI) |
638 qed |
629 } |
639 show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" if "f \<in> o[F](g)" for f g :: "'a \<Rightarrow> 'b" and F |
630 { |
640 using plus_aux that by (blast intro!: big_subsetI) |
631 fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F" |
641 show "L F (f) = L F (g)" if "eventually (\<lambda>x. f x = g x) F" for f g :: "'a \<Rightarrow> 'b" and F |
632 show "L F (f) = L F (g)" unfolding L_def |
642 unfolding L_def by (subst eventually_subst'[OF that]) (rule refl) |
633 by (subst eventually_subst'[OF A]) (rule refl) |
643 show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" if "eventually (\<lambda>x. f x = g x) F" |
634 } |
644 for f g h :: "'a \<Rightarrow> 'b" and F |
635 { |
645 unfolding L_def mem_Collect_eq |
636 fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F" |
646 by (subst (1) eventually_subst'[OF that]) (rule refl) |
637 show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" unfolding L_def mem_Collect_eq |
647 show "L F f \<subseteq> L F g" if "f \<in> L F g" for f g :: "'a \<Rightarrow> 'b" and F |
638 by (subst (1) eventually_subst'[OF A]) (rule refl) |
648 using that by (rule big_subsetI) |
639 } |
649 show "L F (f) = L F (g)" if "f \<in> \<Theta>[F](g)" for f g :: "'a \<Rightarrow> 'b" and F |
640 { |
650 using L that unfolding bigtheta_def |
641 fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" thus "L F f \<subseteq> L F g" by (rule big_subsetI) |
651 by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo) |
642 } |
652 show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" if "f \<in> \<Theta>[F](g)" for f g h :: "'a \<Rightarrow> 'b" and F |
643 { |
653 by (rule disjE[OF L]) |
644 fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)" |
654 (use that in \<open>auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans\<close>) |
645 with A L show "L F (f) = L F (g)" unfolding bigtheta_def |
655 show "(\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" if "f \<in> L F g" for f g h :: "'a \<Rightarrow> 'b" and F |
646 by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo) |
656 using that by (intro big_mult) simp |
647 fix h:: "'a \<Rightarrow> 'b" |
657 show "f \<in> L F (h)" if "f \<in> L F g" "g \<in> L F h" for f g h :: "'a \<Rightarrow> 'b" and F |
648 show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" by (rule disjE[OF L]) |
658 using that by (rule big_trans) |
649 (insert A, auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans) |
659 show "(\<lambda>x. f (h x)) \<in> L' G (\<lambda>x. g (h x))" |
650 } |
660 if "f \<in> L F g" and "filterlim h F G" |
651 { |
661 for f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G |
652 fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" |
662 using that by (auto simp: L_def L'_def filterlim_iff) |
653 thus "(\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" by (intro big_mult) simp |
663 show "f \<in> L (sup F G) g" if "f \<in> L F g" "f \<in> L G g" |
654 } |
664 for f g :: "'a \<Rightarrow> 'b" and F G :: "'a filter" |
655 { |
665 proof - |
656 fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" "g \<in> L F h" |
666 from that [THEN bigE] obtain c1 c2 |
657 thus "f \<in> L F (h)" by (rule big_trans) |
667 where *: "c1 > 0" "c2 > 0" |
658 } |
668 and **: "\<forall>\<^sub>F x in F. R (norm (f x)) (c1 * norm (g x))" |
659 { |
669 "\<forall>\<^sub>F x in G. R (norm (f x)) (c2 * norm (g x))" . |
660 fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G |
|
661 assume "f \<in> L F g" and "filterlim h F G" |
|
662 thus "(\<lambda>x. f (h x)) \<in> L' G (\<lambda>x. g (h x))" by (auto simp: L_def L'_def filterlim_iff) |
|
663 } |
|
664 { |
|
665 fix f g :: "'a \<Rightarrow> 'b" and F G :: "'a filter" |
|
666 assume "f \<in> L F g" "f \<in> L G g" |
|
667 from this [THEN bigE] guess c1 c2 . note c12 = this |
|
668 define c where "c = (if R c1 c2 then c2 else c1)" |
670 define c where "c = (if R c1 c2 then c2 else c1)" |
669 from c12 have c: "R c1 c" "R c2 c" "c > 0" by (auto simp: c_def dest: R_linear) |
671 from * have c: "R c1 c" "R c2 c" "c > 0" |
670 with c12(2,4) have "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F" |
672 by (auto simp: c_def dest: R_linear) |
671 "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) G" |
673 with ** have "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F" |
674 "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) G" |
|
672 by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+ |
675 by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+ |
673 with c show "f \<in> L (sup F G) g" by (auto simp: L_def eventually_sup) |
676 with c show "f \<in> L (sup F G) g" |
674 } |
677 by (auto simp: L_def eventually_sup) |
675 { |
678 qed |
676 fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter" |
679 show "((\<lambda>x. f (h x)) \<in> L' (filtercomap h F) (\<lambda>x. g (h x)))" if "(f \<in> L F g)" |
677 assume "(f \<in> L F g)" |
680 for f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter" |
678 thus "((\<lambda>x. f (h x)) \<in> L' (filtercomap h F) (\<lambda>x. g (h x)))" |
681 using that unfolding L_def L'_def by auto |
679 unfolding L_def L'_def by auto |
|
680 } |
|
681 qed (auto simp: L_def Lr_def eventually_filtermap L'_def |
682 qed (auto simp: L_def Lr_def eventually_filtermap L'_def |
682 intro: filter_leD exI[of _ "1::real"]) |
683 intro: filter_leD exI[of _ "1::real"]) |
683 |
684 |
684 sublocale small: landau_symbol l l' lr |
685 sublocale small: landau_symbol l l' lr |
685 proof |
686 proof |
686 { |
687 have A: "(\<lambda>x. c * f x) \<in> L F f" if "c \<noteq> 0" for c :: 'b and f :: "'a \<Rightarrow> 'b" and F |
687 fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0" |
688 using that by (intro bigI[of "norm c"]) (simp_all add: norm_mult) |
688 hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult) |
689 show "l F (\<lambda>x. c * f x) = l F f" if "c \<noteq> 0" for c :: 'b and f :: "'a \<Rightarrow> 'b" and F |
689 } note A = this |
690 using that and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] |
690 { |
691 by (intro equalityI small_subsetI) (simp_all add: field_simps) |
691 fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0" |
692 show "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" if "c \<noteq> 0" for c :: 'b and f g :: "'a \<Rightarrow> 'b" and F |
692 from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] |
693 proof - |
693 show "l F (\<lambda>x. c * f x) = l F f" |
694 from that and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] |
694 by (intro equalityI small_subsetI) (simp_all add: field_simps) |
695 have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" |
695 } |
696 by (simp_all add: field_simps) |
696 { |
697 then show ?thesis |
697 fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0" |
698 by (intro iffI) (erule (1) big_small_trans)+ |
698 from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] |
699 qed |
699 have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps) |
700 show "l F g \<subseteq> l F (\<lambda>x. f x + g x)" if "f \<in> o[F](g)" for f g :: "'a \<Rightarrow> 'b" and F |
700 thus "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" by (intro iffI) (erule (1) big_small_trans)+ |
701 using plus_aux that by (blast intro!: small_subsetI) |
701 } |
702 show "(\<lambda>x. inverse (g x)) \<in> l F (\<lambda>x. inverse (f x))" |
702 { |
703 if A: "f \<in> l F (g)" and B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F" |
703 fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)" |
704 for f g :: "'a \<Rightarrow> 'b" and F |
704 with plus_aux show "l F g \<subseteq> l F (\<lambda>x. f x + g x)" by (blast intro!: small_subsetI) |
705 proof (rule smallI) |
705 } |
706 fix c :: real assume c: "c > 0" |
706 { |
707 from B smallD[OF A c] |
707 fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> l F (g)" |
708 show "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F" |
708 assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F" |
709 by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide) |
709 show "(\<lambda>x. inverse (g x)) \<in> l F (\<lambda>x. inverse (f x))" |
710 qed |
710 proof (rule smallI) |
711 show "l F (f) = l F (g)" if "eventually (\<lambda>x. f x = g x) F" for f g :: "'a \<Rightarrow> 'b" and F |
711 fix c :: real assume c: "c > 0" |
712 unfolding l_def by (subst eventually_subst'[OF that]) (rule refl) |
712 from B smallD[OF A c] |
713 show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" if "eventually (\<lambda>x. f x = g x) F" for f g h :: "'a \<Rightarrow> 'b" and F |
713 show "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F" |
714 unfolding l_def mem_Collect_eq by (subst (1) eventually_subst'[OF that]) (rule refl) |
714 by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide) |
715 show "l F f \<subseteq> l F g" if "f \<in> l F g" for f g :: "'a \<Rightarrow> 'b" and F |
715 qed |
716 using that by (intro small_subsetI small_imp_big) |
716 } |
717 show "l F (f) = l F (g)" if "f \<in> \<Theta>[F](g)" for f g :: "'a \<Rightarrow> 'b" and F |
717 { |
718 proof - |
718 fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F" |
|
719 show "l F (f) = l F (g)" unfolding l_def by (subst eventually_subst'[OF A]) (rule refl) |
|
720 } |
|
721 { |
|
722 fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F" |
|
723 show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" unfolding l_def mem_Collect_eq |
|
724 by (subst (1) eventually_subst'[OF A]) (rule refl) |
|
725 } |
|
726 { |
|
727 fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" |
|
728 thus "l F f \<subseteq> l F g" by (intro small_subsetI small_imp_big) |
|
729 } |
|
730 { |
|
731 fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)" |
|
732 have L: "L = bigo \<or> L = bigomega" |
719 have L: "L = bigo \<or> L = bigomega" |
733 by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff) |
720 by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff) |
734 with A show "l F (f) = l F (g)" unfolding bigtheta_def |
721 with that show ?thesis unfolding bigtheta_def |
735 by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo) |
722 by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo) |
723 qed |
|
724 show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" if "f \<in> \<Theta>[F](g)" for f g h :: "'a \<Rightarrow> 'b" and F |
|
725 proof - |
|
736 have l: "l = smallo \<or> l = smallomega" |
726 have l: "l = smallo \<or> l = smallomega" |
737 by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff) |
727 by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff) |
738 fix h:: "'a \<Rightarrow> 'b" |
728 show ?thesis |
739 show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" by (rule disjE[OF l]) |
729 by (rule disjE[OF l]) |
740 (insert A, auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo |
730 (use that in \<open>auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo |
741 intro: landau_o.big_small_trans landau_o.small_big_trans) |
731 intro: landau_o.big_small_trans landau_o.small_big_trans\<close>) |
742 } |
732 qed |
743 { |
733 show "(\<lambda>x. h x * f x) \<in> l F (\<lambda>x. h x * g x)" if "f \<in> l F g" for f g h :: "'a \<Rightarrow> 'b" and F |
744 fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" |
734 using that by (intro big_small_mult) simp |
745 thus "(\<lambda>x. h x * f x) \<in> l F (\<lambda>x. h x * g x)" by (intro big_small_mult) simp |
735 show "f \<in> l F (h)" if "f \<in> l F g" "g \<in> l F h" for f g h :: "'a \<Rightarrow> 'b" and F |
746 } |
736 using that by (rule small_trans) |
747 { |
737 show "(\<lambda>x. f (h x)) \<in> l' G (\<lambda>x. g (h x))" if "f \<in> l F g" and "filterlim h F G" |
748 fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" "g \<in> l F h" |
738 for f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G |
749 thus "f \<in> l F (h)" by (rule small_trans) |
739 using that by (auto simp: l_def l'_def filterlim_iff) |
750 } |
740 show "((\<lambda>x. f (h x)) \<in> l' (filtercomap h F) (\<lambda>x. g (h x)))" if "f \<in> l F g" |
751 { |
741 for f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter" |
752 fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G |
742 using that unfolding l_def l'_def by auto |
753 assume "f \<in> l F g" and "filterlim h F G" |
|
754 thus "(\<lambda>x. f (h x)) \<in> l' G (\<lambda>x. g (h x))" |
|
755 by (auto simp: l_def l'_def filterlim_iff) |
|
756 } |
|
757 { |
|
758 fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter" |
|
759 assume "(f \<in> l F g)" |
|
760 thus "((\<lambda>x. f (h x)) \<in> l' (filtercomap h F) (\<lambda>x. g (h x)))" |
|
761 unfolding l_def l'_def by auto |
|
762 } |
|
763 qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD) |
743 qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD) |
764 |
744 |
765 |
745 |
766 text \<open>These rules allow chaining of Landau symbol propositions in Isar with "also".\<close> |
746 text \<open>These rules allow chaining of Landau symbol propositions in Isar with "also".\<close> |
767 |
747 |
779 and small_1_mult': "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> l F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)" |
759 and small_1_mult': "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> l F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)" |
780 and small_1_mult'': "f \<in> L F (g) \<Longrightarrow> h \<in> l F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)" |
760 and small_1_mult'': "f \<in> L F (g) \<Longrightarrow> h \<in> l F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)" |
781 and small_1_mult''': "h \<in> l F (\<lambda>_. 1) \<Longrightarrow> f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)" |
761 and small_1_mult''': "h \<in> l F (\<lambda>_. 1) \<Longrightarrow> f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)" |
782 by (drule (1) big.mult big_small_mult small_big_mult, simp)+ |
762 by (drule (1) big.mult big_small_mult small_big_mult, simp)+ |
783 |
763 |
784 lemmas mult_1_trans = |
764 lemmas mult_1_trans = |
785 big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1''' |
765 big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1''' |
786 big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult''' |
766 big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult''' |
787 |
767 |
788 lemma big_equal_iff_bigtheta: "L F (f) = L F (g) \<longleftrightarrow> f \<in> \<Theta>[F](g)" |
768 lemma big_equal_iff_bigtheta: "L F (f) = L F (g) \<longleftrightarrow> f \<in> \<Theta>[F](g)" |
789 proof |
769 proof |
807 end |
787 end |
808 |
788 |
809 |
789 |
810 context landau_symbol |
790 context landau_symbol |
811 begin |
791 begin |
812 |
792 |
813 lemma plus_absorb1: |
793 lemma plus_absorb1: |
814 assumes "f \<in> o[F](g)" |
794 assumes "f \<in> o[F](g)" |
815 shows "L F (\<lambda>x. f x + g x) = L F (g)" |
795 shows "L F (\<lambda>x. f x + g x) = L F (g)" |
816 proof (intro equalityI) |
796 proof (intro equalityI) |
817 from plus_subset1 and assms show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" . |
797 from plus_subset1 and assms show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" . |
835 |
815 |
836 |
816 |
837 lemma bigthetaI [intro]: "f \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> \<Theta>[F](g)" |
817 lemma bigthetaI [intro]: "f \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> \<Theta>[F](g)" |
838 unfolding bigtheta_def bigomega_def by blast |
818 unfolding bigtheta_def bigomega_def by blast |
839 |
819 |
840 lemma bigthetaD1 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> O[F](g)" |
820 lemma bigthetaD1 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> O[F](g)" |
841 and bigthetaD2 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g)" |
821 and bigthetaD2 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g)" |
842 unfolding bigtheta_def bigo_def bigomega_def by blast+ |
822 unfolding bigtheta_def bigo_def bigomega_def by blast+ |
843 |
823 |
844 lemma bigtheta_refl [simp]: "f \<in> \<Theta>[F](f)" |
824 lemma bigtheta_refl [simp]: "f \<in> \<Theta>[F](f)" |
845 unfolding bigtheta_def by simp |
825 unfolding bigtheta_def by simp |
858 assume "f \<in> o[F](g)" |
838 assume "f \<in> o[F](g)" |
859 hence "O[F](g) \<subseteq> O[F](\<lambda>x. f x + g x)" "\<Omega>[F](g) \<subseteq> \<Omega>[F](\<lambda>x. f x + g x)" |
839 hence "O[F](g) \<subseteq> O[F](\<lambda>x. f x + g x)" "\<Omega>[F](g) \<subseteq> \<Omega>[F](\<lambda>x. f x + g x)" |
860 by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+ |
840 by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+ |
861 thus "\<Theta>[F](g) \<subseteq> \<Theta>[F](\<lambda>x. f x + g x)" unfolding bigtheta_def by blast |
841 thus "\<Theta>[F](g) \<subseteq> \<Theta>[F](\<lambda>x. f x + g x)" unfolding bigtheta_def by blast |
862 next |
842 next |
863 fix f g :: "'a \<Rightarrow> 'b" and F |
843 fix f g :: "'a \<Rightarrow> 'b" and F |
864 assume "f \<in> \<Theta>[F](g)" |
844 assume "f \<in> \<Theta>[F](g)" |
865 thus A: "\<Theta>[F](f) = \<Theta>[F](g)" |
845 thus A: "\<Theta>[F](f) = \<Theta>[F](g)" |
866 apply (subst (1 2) bigtheta_def) |
846 apply (subst (1 2) bigtheta_def) |
867 apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+ |
847 apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+ |
868 apply (rule refl) |
848 apply (rule refl) |
869 done |
849 done |
870 thus "\<Theta>[F](f) \<subseteq> \<Theta>[F](g)" by simp |
850 thus "\<Theta>[F](f) \<subseteq> \<Theta>[F](g)" by simp |
878 next |
858 next |
879 fix f :: "'a \<Rightarrow> 'b" and F1 F2 :: "'a filter" |
859 fix f :: "'a \<Rightarrow> 'b" and F1 F2 :: "'a filter" |
880 assume "F1 \<le> F2" |
860 assume "F1 \<le> F2" |
881 thus "\<Theta>[F2](f) \<subseteq> \<Theta>[F1](f)" |
861 thus "\<Theta>[F2](f) \<subseteq> \<Theta>[F1](f)" |
882 by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono) |
862 by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono) |
883 qed (auto simp: bigtheta_def landau_o.big.norm_iff |
863 qed (auto simp: bigtheta_def landau_o.big.norm_iff |
884 landau_o.big.cmult landau_omega.big.cmult |
864 landau_o.big.cmult landau_omega.big.cmult |
885 landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff |
865 landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff |
886 landau_o.big.in_cong landau_omega.big.in_cong |
866 landau_o.big.in_cong landau_omega.big.in_cong |
887 landau_o.big.mult landau_omega.big.mult |
867 landau_o.big.mult landau_omega.big.mult |
888 landau_o.big.inverse landau_omega.big.inverse |
868 landau_o.big.inverse landau_omega.big.inverse |
889 landau_o.big.compose landau_omega.big.compose |
869 landau_o.big.compose landau_omega.big.compose |
890 landau_o.big.bot' landau_omega.big.bot' |
870 landau_o.big.bot' landau_omega.big.bot' |
891 landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff |
871 landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff |
892 landau_o.big.sup landau_omega.big.sup |
872 landau_o.big.sup landau_omega.big.sup |
893 landau_o.big.filtercomap landau_omega.big.filtercomap |
873 landau_o.big.filtercomap landau_omega.big.filtercomap |
894 dest: landau_o.big.cong landau_omega.big.cong) |
874 dest: landau_o.big.cong landau_omega.big.cong) |
895 |
875 |
896 lemmas landau_symbols = |
876 lemmas landau_symbols = |
897 landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms |
877 landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms |
898 landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms |
878 landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms |
899 landau_theta.landau_symbol_axioms |
879 landau_theta.landau_symbol_axioms |
900 |
880 |
901 lemma bigoI [intro]: |
881 lemma bigoI [intro]: |
902 assumes "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F" |
882 assumes "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F" |
903 shows "f \<in> O[F](g)" |
883 shows "f \<in> O[F](g)" |
904 proof (rule landau_o.bigI) |
884 proof (rule landau_o.bigI) |
905 show "max 1 c > 0" by simp |
885 show "max 1 c > 0" by simp |
906 note assms |
886 have "c * (norm (g x)) \<le> max 1 c * (norm (g x))" for x |
907 moreover have "\<And>x. c * (norm (g x)) \<le> max 1 c * (norm (g x))" by (simp add: mult_right_mono) |
887 by (simp add: mult_right_mono) |
908 ultimately show "eventually (\<lambda>x. (norm (f x)) \<le> max 1 c * (norm (g x))) F" |
888 with assms show "eventually (\<lambda>x. (norm (f x)) \<le> max 1 c * (norm (g x))) F" |
909 by (auto elim!: eventually_mono dest: order.trans) |
889 by (auto elim!: eventually_mono dest: order.trans) |
910 qed |
890 qed |
911 |
891 |
912 lemma smallomegaD [dest]: |
892 lemma smallomegaD [dest]: |
913 assumes "f \<in> \<omega>[F](g)" |
893 assumes "f \<in> \<omega>[F](g)" |
914 shows "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F" |
894 shows "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F" |
915 proof (cases "c > 0") |
895 proof (cases "c > 0") |
916 case False |
896 case False |
917 show ?thesis |
897 show ?thesis |
918 by (intro always_eventually allI, rule order.trans[of _ 0]) |
898 by (intro always_eventually allI, rule order.trans[of _ 0]) |
919 (insert False, auto intro!: mult_nonpos_nonneg) |
899 (insert False, auto intro!: mult_nonpos_nonneg) |
920 qed (blast dest: landau_omega.smallD[OF assms, of c]) |
900 qed (blast dest: landau_omega.smallD[OF assms, of c]) |
921 |
901 |
922 |
902 |
923 lemma bigthetaI': |
903 lemma bigthetaI': |
924 assumes "c1 > 0" "c2 > 0" |
904 assumes "c1 > 0" "c2 > 0" |
925 assumes "eventually (\<lambda>x. c1 * (norm (g x)) \<le> (norm (f x)) \<and> (norm (f x)) \<le> c2 * (norm (g x))) F" |
905 assumes "eventually (\<lambda>x. c1 * (norm (g x)) \<le> (norm (f x)) \<and> (norm (f x)) \<le> c2 * (norm (g x))) F" |
926 shows "f \<in> \<Theta>[F](g)" |
906 shows "f \<in> \<Theta>[F](g)" |
927 apply (rule bigthetaI) |
907 apply (rule bigthetaI) |
930 done |
910 done |
931 |
911 |
932 lemma bigthetaI_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> \<Theta>[F](g)" |
912 lemma bigthetaI_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> \<Theta>[F](g)" |
933 by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono) |
913 by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono) |
934 |
914 |
935 lemma (in landau_symbol) ev_eq_trans1: |
915 lemma (in landau_symbol) ev_eq_trans1: |
936 "f \<in> L F (\<lambda>x. g x (h x)) \<Longrightarrow> eventually (\<lambda>x. h x = h' x) F \<Longrightarrow> f \<in> L F (\<lambda>x. g x (h' x))" |
916 "f \<in> L F (\<lambda>x. g x (h x)) \<Longrightarrow> eventually (\<lambda>x. h x = h' x) F \<Longrightarrow> f \<in> L F (\<lambda>x. g x (h' x))" |
937 by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono) |
917 by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono) |
938 |
918 |
939 lemma (in landau_symbol) ev_eq_trans2: |
919 lemma (in landau_symbol) ev_eq_trans2: |
940 "eventually (\<lambda>x. f x = f' x) F \<Longrightarrow> (\<lambda>x. g x (f' x)) \<in> L F (h) \<Longrightarrow> (\<lambda>x. g x (f x)) \<in> L F (h)" |
920 "eventually (\<lambda>x. f x = f' x) F \<Longrightarrow> (\<lambda>x. g x (f' x)) \<in> L F (h) \<Longrightarrow> (\<lambda>x. g x (f x)) \<in> L F (h)" |
941 by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono) |
921 by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono) |
942 |
922 |
943 declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro] |
923 declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro] |
944 declare landau_o.bigE landau_omega.bigE [elim] |
924 declare landau_o.bigE landau_omega.bigE [elim] |
945 declare landau_o.smallD |
925 declare landau_o.smallD |
946 |
926 |
947 lemma (in landau_symbol) bigtheta_trans1': |
927 lemma (in landau_symbol) bigtheta_trans1': |
948 "f \<in> L F (g) \<Longrightarrow> h \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h)" |
928 "f \<in> L F (g) \<Longrightarrow> h \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h)" |
949 by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym) |
929 by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym) |
950 |
930 |
951 lemma (in landau_symbol) bigtheta_trans2': |
931 lemma (in landau_symbol) bigtheta_trans2': |
952 "g \<in> \<Theta>[F](f) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)" |
932 "g \<in> \<Theta>[F](f) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)" |
953 by (rule bigtheta_trans2, subst bigtheta_sym) |
933 by (rule bigtheta_trans2, subst bigtheta_sym) |
954 |
934 |
955 lemma bigo_bigomega_trans: "f \<in> O[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> O[F](h)" |
935 lemma bigo_bigomega_trans: "f \<in> O[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> O[F](h)" |
956 and bigo_smallomega_trans: "f \<in> O[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)" |
936 and bigo_smallomega_trans: "f \<in> O[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)" |
959 and bigomega_bigo_trans: "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](h)" |
939 and bigomega_bigo_trans: "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](h)" |
960 and bigomega_smallo_trans: "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)" |
940 and bigomega_smallo_trans: "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)" |
961 and smallomega_bigo_trans: "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)" |
941 and smallomega_bigo_trans: "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)" |
962 and smallomega_smallo_trans: "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)" |
942 and smallomega_smallo_trans: "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)" |
963 by (unfold bigomega_iff_bigo smallomega_iff_smallo) |
943 by (unfold bigomega_iff_bigo smallomega_iff_smallo) |
964 (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans |
944 (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans |
965 landau_o.big_trans landau_o.small_trans)+ |
945 landau_o.big_trans landau_o.small_trans)+ |
966 |
946 |
967 lemmas landau_trans_lift [trans] = |
947 lemmas landau_trans_lift [trans] = |
968 landau_symbols[THEN landau_symbol.lift_trans] |
948 landau_symbols[THEN landau_symbol.lift_trans] |
969 landau_symbols[THEN landau_symbol.lift_trans'] |
949 landau_symbols[THEN landau_symbol.lift_trans'] |
971 landau_symbols[THEN landau_symbol.lift_trans_bigtheta'] |
951 landau_symbols[THEN landau_symbol.lift_trans_bigtheta'] |
972 |
952 |
973 lemmas landau_mult_1_trans [trans] = |
953 lemmas landau_mult_1_trans [trans] = |
974 landau_o.mult_1_trans landau_omega.mult_1_trans |
954 landau_o.mult_1_trans landau_omega.mult_1_trans |
975 |
955 |
976 lemmas landau_trans [trans] = |
956 lemmas landau_trans [trans] = |
977 landau_symbols[THEN landau_symbol.bigtheta_trans1] |
957 landau_symbols[THEN landau_symbol.bigtheta_trans1] |
978 landau_symbols[THEN landau_symbol.bigtheta_trans2] |
958 landau_symbols[THEN landau_symbol.bigtheta_trans2] |
979 landau_symbols[THEN landau_symbol.bigtheta_trans1'] |
959 landau_symbols[THEN landau_symbol.bigtheta_trans1'] |
980 landau_symbols[THEN landau_symbol.bigtheta_trans2'] |
960 landau_symbols[THEN landau_symbol.bigtheta_trans2'] |
981 landau_symbols[THEN landau_symbol.ev_eq_trans1] |
961 landau_symbols[THEN landau_symbol.ev_eq_trans1] |
982 landau_symbols[THEN landau_symbol.ev_eq_trans2] |
962 landau_symbols[THEN landau_symbol.ev_eq_trans2] |
983 |
963 |
984 landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans |
964 landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans |
985 landau_omega.big_trans landau_omega.small_trans |
965 landau_omega.big_trans landau_omega.small_trans |
986 landau_omega.small_big_trans landau_omega.big_small_trans |
966 landau_omega.small_big_trans landau_omega.big_small_trans |
987 |
967 |
988 bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans |
968 bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans |
989 bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans |
969 bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans |
990 |
970 |
991 lemma bigtheta_inverse [simp]: |
971 lemma bigtheta_inverse [simp]: |
992 shows "(\<lambda>x. inverse (f x)) \<in> \<Theta>[F](\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<in> \<Theta>[F](g)" |
972 shows "(\<lambda>x. inverse (f x)) \<in> \<Theta>[F](\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<in> \<Theta>[F](g)" |
993 proof- |
973 proof - |
994 { |
974 have "(\<lambda>x. inverse (f x)) \<in> O[F](\<lambda>x. inverse (g x))" |
995 fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)" |
975 if A: "f \<in> \<Theta>[F](g)" |
996 then guess c1 c2 :: real unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE) |
976 for f g :: "'a \<Rightarrow> 'b" and F |
997 note c = this |
977 proof - |
998 from c(3) have "inverse c2 > 0" by simp |
978 from A obtain c1 c2 :: real where *: "c1 > 0" "c2 > 0" |
999 moreover from c(2,4) |
979 and **: "\<forall>\<^sub>F x in F. norm (f x) \<le> c1 * norm (g x)" |
1000 have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))) F" |
980 "\<forall>\<^sub>F x in F. c2 * norm (g x) \<le> norm (f x)" |
981 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE) |
|
982 from \<open>c2 > 0\<close> have c2: "inverse c2 > 0" by simp |
|
983 from ** have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))) F" |
|
1001 proof eventually_elim |
984 proof eventually_elim |
1002 fix x assume A: "(norm (f x)) \<le> c1 * (norm (g x))" "c2 * (norm (g x)) \<le> (norm (f x))" |
985 fix x assume A: "norm (f x) \<le> c1 * norm (g x)" "c2 * norm (g x) \<le> norm (f x)" |
1003 from A c(1,3) have "f x = 0 \<longleftrightarrow> g x = 0" by (auto simp: field_simps mult_le_0_iff) |
986 from A * have "f x = 0 \<longleftrightarrow> g x = 0" |
1004 with A c(1,3) show "norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))" |
987 by (auto simp: field_simps mult_le_0_iff) |
988 with A * show "norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))" |
|
1005 by (force simp: field_simps norm_inverse norm_divide) |
989 by (force simp: field_simps norm_inverse norm_divide) |
1006 qed |
990 qed |
1007 ultimately have "(\<lambda>x. inverse (f x)) \<in> O[F](\<lambda>x. inverse (g x))" by (rule landau_o.bigI) |
991 with c2 show ?thesis by (rule landau_o.bigI) |
1008 } |
992 qed |
1009 thus ?thesis unfolding bigtheta_def |
993 then show ?thesis |
994 unfolding bigtheta_def |
|
1010 by (force simp: bigomega_iff_bigo bigtheta_sym) |
995 by (force simp: bigomega_iff_bigo bigtheta_sym) |
1011 qed |
996 qed |
1012 |
997 |
1013 lemma bigtheta_divide: |
998 lemma bigtheta_divide: |
1014 assumes "f1 \<in> \<Theta>(f2)" "g1 \<in> \<Theta>(g2)" |
999 assumes "f1 \<in> \<Theta>(f2)" "g1 \<in> \<Theta>(g2)" |
1016 by (subst (1 2) divide_inverse, intro landau_theta.mult) (simp_all add: bigtheta_inverse assms) |
1001 by (subst (1 2) divide_inverse, intro landau_theta.mult) (simp_all add: bigtheta_inverse assms) |
1017 |
1002 |
1018 lemma eventually_nonzero_bigtheta: |
1003 lemma eventually_nonzero_bigtheta: |
1019 assumes "f \<in> \<Theta>[F](g)" |
1004 assumes "f \<in> \<Theta>[F](g)" |
1020 shows "eventually (\<lambda>x. f x \<noteq> 0) F \<longleftrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F" |
1005 shows "eventually (\<lambda>x. f x \<noteq> 0) F \<longleftrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F" |
1021 proof- |
1006 proof - |
1022 { |
1007 have "eventually (\<lambda>x. g x \<noteq> 0) F" |
1023 fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)" and B: "eventually (\<lambda>x. f x \<noteq> 0) F" |
1008 if A: "f \<in> \<Theta>[F](g)" and B: "eventually (\<lambda>x. f x \<noteq> 0) F" |
1024 from A guess c1 c2 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE) |
1009 for f g :: "'a \<Rightarrow> 'b" |
1025 from B this(2,4) have "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim auto |
1010 proof - |
1026 } |
1011 from A obtain c1 c2 where |
1012 "\<forall>\<^sub>F x in F. norm (f x) \<le> c1 * norm (g x)" |
|
1013 "\<forall>\<^sub>F x in F. c2 * norm (g x) \<le> norm (f x)" |
|
1014 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE) |
|
1015 with B show ?thesis by eventually_elim auto |
|
1016 qed |
|
1027 with assms show ?thesis by (force simp: bigtheta_sym) |
1017 with assms show ?thesis by (force simp: bigtheta_sym) |
1028 qed |
1018 qed |
1029 |
1019 |
1030 |
1020 |
1031 subsection \<open>Landau symbols and limits\<close> |
1021 subsection \<open>Landau symbols and limits\<close> |
1034 fixes f g |
1024 fixes f g |
1035 assumes "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F" |
1025 assumes "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F" |
1036 assumes "eventually (\<lambda>x. g x \<noteq> 0) F" |
1026 assumes "eventually (\<lambda>x. g x \<noteq> 0) F" |
1037 shows "f \<in> O[F](g)" |
1027 shows "f \<in> O[F](g)" |
1038 proof (rule bigoI) |
1028 proof (rule bigoI) |
1039 from assms have "eventually (\<lambda>x. dist (norm (f x / g x)) c < 1) F" |
1029 from assms have "eventually (\<lambda>x. dist (norm (f x / g x)) c < 1) F" |
1040 using tendstoD by force |
1030 using tendstoD by force |
1041 thus "eventually (\<lambda>x. (norm (f x)) \<le> (norm c + 1) * (norm (g x))) F" |
1031 thus "eventually (\<lambda>x. (norm (f x)) \<le> (norm c + 1) * (norm (g x))) F" |
1042 unfolding dist_real_def using assms(2) |
1032 unfolding dist_real_def using assms(2) |
1043 proof eventually_elim |
1033 proof eventually_elim |
1044 case (elim x) |
1034 case (elim x) |
1046 unfolding norm_mult [symmetric] using norm_triangle_ineq2[of "norm (f x)" "c * norm (g x)"] |
1036 unfolding norm_mult [symmetric] using norm_triangle_ineq2[of "norm (f x)" "c * norm (g x)"] |
1047 by (simp add: norm_mult abs_mult) |
1037 by (simp add: norm_mult abs_mult) |
1048 also from elim have "\<dots> = norm (norm (g x)) * norm (norm (f x / g x) - c)" |
1038 also from elim have "\<dots> = norm (norm (g x)) * norm (norm (f x / g x) - c)" |
1049 unfolding norm_mult [symmetric] by (simp add: algebra_simps norm_divide) |
1039 unfolding norm_mult [symmetric] by (simp add: algebra_simps norm_divide) |
1050 also from elim have "norm (norm (f x / g x) - c) \<le> 1" by simp |
1040 also from elim have "norm (norm (f x / g x) - c) \<le> 1" by simp |
1051 hence "norm (norm (g x)) * norm (norm (f x / g x) - c) \<le> norm (norm (g x)) * 1" |
1041 hence "norm (norm (g x)) * norm (norm (f x / g x) - c) \<le> norm (norm (g x)) * 1" |
1052 by (rule mult_left_mono) simp_all |
1042 by (rule mult_left_mono) simp_all |
1053 finally show ?case by (simp add: algebra_simps) |
1043 finally show ?case by (simp add: algebra_simps) |
1054 qed |
1044 qed |
1055 qed |
1045 qed |
1056 |
1046 |
1077 proof (eventually_elim) |
1067 proof (eventually_elim) |
1078 fix x assume B: "norm (norm (f x / g x) - c) < c / 2" |
1068 fix x assume B: "norm (norm (f x / g x) - c) < c / 2" |
1079 from B have g: "g x \<noteq> 0" by auto |
1069 from B have g: "g x \<noteq> 0" by auto |
1080 from B have "-c/2 < -norm (norm (f x / g x) - c)" by simp |
1070 from B have "-c/2 < -norm (norm (f x / g x) - c)" by simp |
1081 also have "... \<le> norm (f x / g x) - c" by simp |
1071 also have "... \<le> norm (f x / g x) - c" by simp |
1082 finally show "(norm (f x)) \<ge> c/2 * (norm (g x))" using g |
1072 finally show "(norm (f x)) \<ge> c/2 * (norm (g x))" using g |
1083 by (simp add: field_simps norm_mult norm_divide) |
1073 by (simp add: field_simps norm_mult norm_divide) |
1084 qed |
1074 qed |
1085 qed |
1075 qed |
1086 qed simp |
1076 qed simp |
1087 |
1077 |
1111 shows "f \<in> \<omega>[F](g)" |
1101 shows "f \<in> \<omega>[F](g)" |
1112 proof (rule smallomegaI_filterlim_at_top_norm) |
1102 proof (rule smallomegaI_filterlim_at_top_norm) |
1113 from lim show "filterlim (\<lambda>x. norm (f x / g x)) at_top F" |
1103 from lim show "filterlim (\<lambda>x. norm (f x / g x)) at_top F" |
1114 by (rule filterlim_at_infinity_imp_norm_at_top) |
1104 by (rule filterlim_at_infinity_imp_norm_at_top) |
1115 qed |
1105 qed |
1116 |
1106 |
1117 lemma smallomegaD_filterlim_at_top_norm: |
1107 lemma smallomegaD_filterlim_at_top_norm: |
1118 assumes "f \<in> \<omega>[F](g)" |
1108 assumes "f \<in> \<omega>[F](g)" |
1119 assumes "eventually (\<lambda>x. g x \<noteq> 0) F" |
1109 assumes "eventually (\<lambda>x. g x \<noteq> 0) F" |
1120 shows "LIM x F. norm (f x / g x) :> at_top" |
1110 shows "LIM x F. norm (f x / g x) :> at_top" |
1121 proof (subst filterlim_at_top_gt, clarify) |
1111 proof (subst filterlim_at_top_gt, clarify) |
1122 fix c :: real assume c: "c > 0" |
1112 fix c :: real assume c: "c > 0" |
1123 from landau_omega.smallD[OF assms(1) this] assms(2) |
1113 from landau_omega.smallD[OF assms(1) this] assms(2) |
1124 show "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F" |
1114 show "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F" |
1125 by eventually_elim (simp add: field_simps norm_divide) |
1115 by eventually_elim (simp add: field_simps norm_divide) |
1126 qed |
1116 qed |
1127 |
1117 |
1128 lemma smallomegaD_filterlim_at_infinity: |
1118 lemma smallomegaD_filterlim_at_infinity: |
1129 assumes "f \<in> \<omega>[F](g)" |
1119 assumes "f \<in> \<omega>[F](g)" |
1130 assumes "eventually (\<lambda>x. g x \<noteq> 0) F" |
1120 assumes "eventually (\<lambda>x. g x \<noteq> 0) F" |
1131 shows "LIM x F. f x / g x :> at_infinity" |
1121 shows "LIM x F. f x / g x :> at_infinity" |
1132 using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm) |
1122 using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm) |
1186 lemma tendsto_add_smallo: |
1176 lemma tendsto_add_smallo: |
1187 assumes "(f1 \<longlongrightarrow> a) F" |
1177 assumes "(f1 \<longlongrightarrow> a) F" |
1188 assumes "f2 \<in> o[F](f1)" |
1178 assumes "f2 \<in> o[F](f1)" |
1189 shows "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F" |
1179 shows "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F" |
1190 proof (subst filterlim_cong[OF refl refl]) |
1180 proof (subst filterlim_cong[OF refl refl]) |
1191 from landau_o.smallD[OF assms(2) zero_less_one] |
1181 from landau_o.smallD[OF assms(2) zero_less_one] |
1192 have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)) F" by simp |
1182 have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)) F" by simp |
1193 thus "eventually (\<lambda>x. f1 x + f2 x = f1 x * (1 + f2 x / f1 x)) F" |
1183 thus "eventually (\<lambda>x. f1 x + f2 x = f1 x * (1 + f2 x / f1 x)) F" |
1194 by eventually_elim (auto simp: field_simps) |
1184 by eventually_elim (auto simp: field_simps) |
1195 next |
1185 next |
1196 from assms(1) show "((\<lambda>x. f1 x * (1 + f2 x / f1 x)) \<longlongrightarrow> a) F" |
1186 from assms(1) show "((\<lambda>x. f1 x * (1 + f2 x / f1 x)) \<longlongrightarrow> a) F" |
1222 shows "((\<lambda>x. (f1 x + f2 x) / (g1 x + g2 x)) \<longlongrightarrow> a) F" (is "(?f \<longlongrightarrow> _) _") |
1212 shows "((\<lambda>x. (f1 x + f2 x) / (g1 x + g2 x)) \<longlongrightarrow> a) F" (is "(?f \<longlongrightarrow> _) _") |
1223 proof (subst tendsto_cong) |
1213 proof (subst tendsto_cong) |
1224 let ?f' = "\<lambda>x. (f1 x / g1 x) * (1 + f2 x / f1 x) / (1 + g2 x / g1 x)" |
1214 let ?f' = "\<lambda>x. (f1 x / g1 x) * (1 + f2 x / f1 x) / (1 + g2 x / g1 x)" |
1225 |
1215 |
1226 have "(?f' \<longlongrightarrow> a * (1 + 0) / (1 + 0)) F" |
1216 have "(?f' \<longlongrightarrow> a * (1 + 0) / (1 + 0)) F" |
1227 by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const |
1217 by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const |
1228 smalloD_tendsto[OF assms(2)] smalloD_tendsto[OF assms(3)])+ simp_all |
1218 smalloD_tendsto[OF assms(2)] smalloD_tendsto[OF assms(3)])+ simp_all |
1229 thus "(?f' \<longlongrightarrow> a) F" by simp |
1219 thus "(?f' \<longlongrightarrow> a) F" by simp |
1230 |
1220 |
1231 have "(1/2::real) > 0" by simp |
1221 have "(1/2::real) > 0" by simp |
1232 from landau_o.smallD[OF assms(2) this] landau_o.smallD[OF assms(3) this] |
1222 from landau_o.smallD[OF assms(2) this] landau_o.smallD[OF assms(3) this] |
1233 have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)/2) F" |
1223 have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)/2) F" |
1234 "eventually (\<lambda>x. norm (g2 x) \<le> norm (g1 x)/2) F" by simp_all |
1224 "eventually (\<lambda>x. norm (g2 x) \<le> norm (g1 x)/2) F" by simp_all |
1235 with assms(4) show "eventually (\<lambda>x. ?f x = ?f' x) F" |
1225 with assms(4) show "eventually (\<lambda>x. ?f x = ?f' x) F" |
1236 proof eventually_elim |
1226 proof eventually_elim |
1237 fix x assume A: "norm (f2 x) \<le> norm (f1 x)/2" and |
1227 fix x assume A: "norm (f2 x) \<le> norm (f1 x)/2" and |
1238 B: "norm (g2 x) \<le> norm (g1 x)/2" and C: "g1 x \<noteq> 0" |
1228 B: "norm (g2 x) \<le> norm (g1 x)/2" and C: "g1 x \<noteq> 0" |
1239 show "?f x = ?f' x" |
1229 show "?f x = ?f' x" |
1240 proof (cases "f1 x = 0") |
1230 proof (cases "f1 x = 0") |
1241 assume D: "f1 x \<noteq> 0" |
1231 assume D: "f1 x \<noteq> 0" |
1242 from D have "f1 x + f2 x = f1 x * (1 + f2 x/f1 x)" by (simp add: field_simps) |
1232 from D have "f1 x + f2 x = f1 x * (1 + f2 x/f1 x)" by (simp add: field_simps) |
1252 lemma bigo_powr: |
1242 lemma bigo_powr: |
1253 fixes f :: "'a \<Rightarrow> real" |
1243 fixes f :: "'a \<Rightarrow> real" |
1254 assumes "f \<in> O[F](g)" "p \<ge> 0" |
1244 assumes "f \<in> O[F](g)" "p \<ge> 0" |
1255 shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" |
1245 shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" |
1256 proof- |
1246 proof- |
1257 from assms(1) guess c by (elim landau_o.bigE landau_omega.bigE IntE) |
1247 from assms(1) obtain c where c: "c > 0" and *: "\<forall>\<^sub>F x in F. norm (f x) \<le> c * norm (g x)" |
1258 note c = this |
1248 by (elim landau_o.bigE landau_omega.bigE IntE) |
1259 from c(2) assms(2) have "eventually (\<lambda>x. (norm (f x)) powr p \<le> (c * (norm (g x))) powr p) F" |
1249 from assms(2) * have "eventually (\<lambda>x. (norm (f x)) powr p \<le> (c * norm (g x)) powr p) F" |
1260 by (auto elim!: eventually_mono intro!: powr_mono2) |
1250 by (auto elim!: eventually_mono intro!: powr_mono2) |
1261 thus "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" using c(1) |
1251 with c show "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" |
1262 by (intro bigoI[of _ "c powr p"]) (simp_all add: powr_mult) |
1252 by (intro bigoI[of _ "c powr p"]) (simp_all add: powr_mult) |
1263 qed |
1253 qed |
1264 |
1254 |
1265 lemma smallo_powr: |
1255 lemma smallo_powr: |
1266 fixes f :: "'a \<Rightarrow> real" |
1256 fixes f :: "'a \<Rightarrow> real" |
1267 assumes "f \<in> o[F](g)" "p > 0" |
1257 assumes "f \<in> o[F](g)" "p > 0" |
1268 shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)" |
1258 shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)" |
1269 proof (rule landau_o.smallI) |
1259 proof (rule landau_o.smallI) |
1270 fix c :: real assume c: "c > 0" |
1260 fix c :: real assume c: "c > 0" |
1271 hence "c powr (1/p) > 0" by simp |
1261 hence "c powr (1/p) > 0" by simp |
1272 from landau_o.smallD[OF assms(1) this] |
1262 from landau_o.smallD[OF assms(1) this] |
1273 show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F" |
1263 show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F" |
1274 proof eventually_elim |
1264 proof eventually_elim |
1275 fix x assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))" |
1265 fix x assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))" |
1276 with assms(2) have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p" |
1266 with assms(2) have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p" |
1277 by (intro powr_mono2) simp_all |
1267 by (intro powr_mono2) simp_all |
1284 lemma smallo_powr_nonneg: |
1274 lemma smallo_powr_nonneg: |
1285 fixes f :: "'a \<Rightarrow> real" |
1275 fixes f :: "'a \<Rightarrow> real" |
1286 assumes "f \<in> o[F](g)" "p > 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F" |
1276 assumes "f \<in> o[F](g)" "p > 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F" |
1287 shows "(\<lambda>x. f x powr p) \<in> o[F](\<lambda>x. g x powr p)" |
1277 shows "(\<lambda>x. f x powr p) \<in> o[F](\<lambda>x. g x powr p)" |
1288 proof - |
1278 proof - |
1289 from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" |
1279 from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" |
1290 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1280 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1291 also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro smallo_powr) fact+ |
1281 also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro smallo_powr) fact+ |
1292 also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)" |
1282 also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)" |
1293 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1283 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1294 finally show ?thesis . |
1284 finally show ?thesis . |
1305 lemma bigo_powr_nonneg: |
1295 lemma bigo_powr_nonneg: |
1306 fixes f :: "'a \<Rightarrow> real" |
1296 fixes f :: "'a \<Rightarrow> real" |
1307 assumes "f \<in> O[F](g)" "p \<ge> 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F" |
1297 assumes "f \<in> O[F](g)" "p \<ge> 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F" |
1308 shows "(\<lambda>x. f x powr p) \<in> O[F](\<lambda>x. g x powr p)" |
1298 shows "(\<lambda>x. f x powr p) \<in> O[F](\<lambda>x. g x powr p)" |
1309 proof - |
1299 proof - |
1310 from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" |
1300 from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" |
1311 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1301 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1312 also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro bigo_powr) fact+ |
1302 also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro bigo_powr) fact+ |
1313 also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)" |
1303 also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)" |
1314 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1304 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1315 finally show ?thesis . |
1305 finally show ?thesis . |
1373 by (cases "c1 = 0"; cases "c2 = 0") |
1363 by (cases "c1 = 0"; cases "c2 = 0") |
1374 (auto simp: bigo_def eventually_False intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"]) |
1364 (auto simp: bigo_def eventually_False intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"]) |
1375 |
1365 |
1376 lemma bigomega_const_iff [simp]: "(\<lambda>_. c1) \<in> \<Omega>[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 \<noteq> 0 \<or> c2 = 0" |
1366 lemma bigomega_const_iff [simp]: "(\<lambda>_. c1) \<in> \<Omega>[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 \<noteq> 0 \<or> c2 = 0" |
1377 by (cases "c1 = 0"; cases "c2 = 0") |
1367 by (cases "c1 = 0"; cases "c2 = 0") |
1378 (auto simp: bigomega_def eventually_False mult_le_0_iff |
1368 (auto simp: bigomega_def eventually_False mult_le_0_iff |
1379 intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"]) |
1369 intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"]) |
1380 |
1370 |
1381 lemma smallo_real_nat_transfer: |
1371 lemma smallo_real_nat_transfer: |
1382 "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))" |
1372 "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))" |
1383 by (rule landau_o.small.compose[OF _ filterlim_real_sequentially]) |
1373 by (rule landau_o.small.compose[OF _ filterlim_real_sequentially]) |
1396 |
1386 |
1397 lemma bigtheta_real_nat_transfer: |
1387 lemma bigtheta_real_nat_transfer: |
1398 "(f :: real \<Rightarrow> real) \<in> \<Theta>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Theta>(\<lambda>x. g (real x))" |
1388 "(f :: real \<Rightarrow> real) \<in> \<Theta>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Theta>(\<lambda>x. g (real x))" |
1399 unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast |
1389 unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast |
1400 |
1390 |
1401 lemmas landau_real_nat_transfer [intro] = |
1391 lemmas landau_real_nat_transfer [intro] = |
1402 bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer |
1392 bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer |
1403 smallomega_real_nat_transfer bigtheta_real_nat_transfer |
1393 smallomega_real_nat_transfer bigtheta_real_nat_transfer |
1404 |
1394 |
1405 |
1395 |
1406 lemma landau_symbol_if_at_top_eq [simp]: |
1396 lemma landau_symbol_if_at_top_eq [simp]: |
1407 assumes "landau_symbol L L' Lr" |
1397 assumes "landau_symbol L L' Lr" |
1415 |
1405 |
1416 |
1406 |
1417 lemma sum_in_smallo: |
1407 lemma sum_in_smallo: |
1418 assumes "f \<in> o[F](h)" "g \<in> o[F](h)" |
1408 assumes "f \<in> o[F](h)" "g \<in> o[F](h)" |
1419 shows "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" |
1409 shows "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" |
1420 proof- |
1410 proof - |
1421 { |
1411 have "(\<lambda>x. f x + g x) \<in> o[F](h)" if "f \<in> o[F](h)" "g \<in> o[F](h)" for f g |
1422 fix f g assume fg: "f \<in> o[F](h)" "g \<in> o[F](h)" |
1412 proof (rule landau_o.smallI) |
1423 have "(\<lambda>x. f x + g x) \<in> o[F](h)" |
1413 fix c :: real assume "c > 0" |
1424 proof (rule landau_o.smallI) |
1414 hence "c/2 > 0" by simp |
1425 fix c :: real assume "c > 0" |
1415 from that[THEN landau_o.smallD[OF _ this]] |
1426 hence "c/2 > 0" by simp |
1416 show "eventually (\<lambda>x. norm (f x + g x) \<le> c * (norm (h x))) F" |
1427 from fg[THEN landau_o.smallD[OF _ this]] |
1417 by eventually_elim (auto intro: order.trans[OF norm_triangle_ineq]) |
1428 show "eventually (\<lambda>x. norm (f x + g x) \<le> c * (norm (h x))) F" |
1418 qed |
1429 by eventually_elim (auto intro: order.trans[OF norm_triangle_ineq]) |
|
1430 qed |
|
1431 } |
|
1432 from this[of f g] this[of f "\<lambda>x. -g x"] assms |
1419 from this[of f g] this[of f "\<lambda>x. -g x"] assms |
1433 show "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" by simp_all |
1420 show "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" by simp_all |
1434 qed |
1421 qed |
1435 |
1422 |
1436 lemma big_sum_in_smallo: |
1423 lemma big_sum_in_smallo: |
1439 using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_smallo) |
1426 using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_smallo) |
1440 |
1427 |
1441 lemma sum_in_bigo: |
1428 lemma sum_in_bigo: |
1442 assumes "f \<in> O[F](h)" "g \<in> O[F](h)" |
1429 assumes "f \<in> O[F](h)" "g \<in> O[F](h)" |
1443 shows "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" |
1430 shows "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" |
1444 proof- |
1431 proof - |
1445 { |
1432 have "(\<lambda>x. f x + g x) \<in> O[F](h)" if "f \<in> O[F](h)" "g \<in> O[F](h)" for f g |
1446 fix f g assume fg: "f \<in> O[F](h)" "g \<in> O[F](h)" |
1433 proof - |
1447 from fg(1) guess c1 by (elim landau_o.bigE) note c1 = this |
1434 from that obtain c1 c2 where *: "c1 > 0" "c2 > 0" |
1448 from fg(2) guess c2 by (elim landau_o.bigE) note c2 = this |
1435 and **: "\<forall>\<^sub>F x in F. norm (f x) \<le> c1 * norm (h x)" |
1449 from c1(2) c2(2) have "eventually (\<lambda>x. norm (f x + g x) \<le> (c1 + c2) * (norm (h x))) F" |
1436 "\<forall>\<^sub>F x in F. norm (g x) \<le> c2 * norm (h x)" |
1437 by (elim landau_o.bigE) |
|
1438 from ** have "eventually (\<lambda>x. norm (f x + g x) \<le> (c1 + c2) * (norm (h x))) F" |
|
1450 by eventually_elim (auto simp: algebra_simps intro: order.trans[OF norm_triangle_ineq]) |
1439 by eventually_elim (auto simp: algebra_simps intro: order.trans[OF norm_triangle_ineq]) |
1451 hence "(\<lambda>x. f x + g x) \<in> O[F](h)" by (rule bigoI) |
1440 then show ?thesis by (rule bigoI) |
1452 } |
1441 qed |
1453 from this[of f g] this[of f "\<lambda>x. -g x"] assms |
1442 from assms this[of f g] this[of f "\<lambda>x. - g x"] |
1454 show "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" by simp_all |
1443 show "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" by simp_all |
1455 qed |
1444 qed |
1456 |
1445 |
1457 lemma big_sum_in_bigo: |
1446 lemma big_sum_in_bigo: |
1458 assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> O[F](g)" |
1447 assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> O[F](g)" |
1459 shows "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)" |
1448 shows "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)" |
1469 proof |
1458 proof |
1470 assume A: "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" |
1459 assume A: "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" |
1471 from assms have nz: "eventually (\<lambda>x. f1 x \<noteq> 0) F" by (simp add: eventually_nonzero_bigtheta) |
1460 from assms have nz: "eventually (\<lambda>x. f1 x \<noteq> 0) F" by (simp add: eventually_nonzero_bigtheta) |
1472 hence "f2 \<in> \<Theta>[F](\<lambda>x. f1 x * f2 x / f1 x)" |
1461 hence "f2 \<in> \<Theta>[F](\<lambda>x. f1 x * f2 x / f1 x)" |
1473 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1462 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1474 also from A assms nz have "(\<lambda>x. f1 x * f2 x / f1 x) \<in> L F (\<lambda>x. g1 x * g2 x / f1 x)" |
1463 also from A assms nz have "(\<lambda>x. f1 x * f2 x / f1 x) \<in> L F (\<lambda>x. g1 x * g2 x / f1 x)" |
1475 by (intro divide_right) simp_all |
1464 by (intro divide_right) simp_all |
1476 also from assms nz have "(\<lambda>x. g1 x * g2 x / f1 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x / g1 x)" |
1465 also from assms nz have "(\<lambda>x. g1 x * g2 x / f1 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x / g1 x)" |
1477 by (intro landau_theta.mult landau_theta.divide) (simp_all add: bigtheta_sym) |
1466 by (intro landau_theta.mult landau_theta.divide) (simp_all add: bigtheta_sym) |
1478 also from assms have "(\<lambda>x. g1 x * g2 x / g1 x) \<in> \<Theta>[F](g2)" |
1467 also from assms have "(\<lambda>x. g1 x * g2 x / g1 x) \<in> \<Theta>[F](g2)" |
1479 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1468 by (intro bigthetaI_cong) (auto elim!: eventually_mono) |
1496 shows "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> f1 \<in> L F (g1)" |
1485 shows "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> f1 \<in> L F (g1)" |
1497 by (subst (1 2) divide_inverse, intro mult_cancel_right bigtheta_inverse) (simp_all add: assms) |
1486 by (subst (1 2) divide_inverse, intro mult_cancel_right bigtheta_inverse) (simp_all add: assms) |
1498 |
1487 |
1499 lemma divide_cancel_left: |
1488 lemma divide_cancel_left: |
1500 assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F" |
1489 assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F" |
1501 shows "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> |
1490 shows "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> |
1502 (\<lambda>x. inverse (f2 x)) \<in> L F (\<lambda>x. inverse (g2 x))" |
1491 (\<lambda>x. inverse (f2 x)) \<in> L F (\<lambda>x. inverse (g2 x))" |
1503 by (simp only: divide_inverse mult_cancel_left[OF assms]) |
1492 by (simp only: divide_inverse mult_cancel_left[OF assms]) |
1504 |
1493 |
1505 end |
1494 end |
1506 |
1495 |
1565 by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff) |
1554 by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff) |
1566 with B \<open>p > q\<close> show ?thesis by (auto intro: landau_o.small_imp_big) |
1555 with B \<open>p > q\<close> show ?thesis by (auto intro: landau_o.small_imp_big) |
1567 qed |
1556 qed |
1568 qed |
1557 qed |
1569 |
1558 |
1570 lemma powr_bigtheta_iff: |
1559 lemma powr_bigtheta_iff: |
1571 assumes "filterlim g at_top F" "F \<noteq> bot" |
1560 assumes "filterlim g at_top F" "F \<noteq> bot" |
1572 shows "(\<lambda>x. g x powr p :: real) \<in> \<Theta>[F](\<lambda>x. g x powr q) \<longleftrightarrow> p = q" |
1561 shows "(\<lambda>x. g x powr p :: real) \<in> \<Theta>[F](\<lambda>x. g x powr q) \<longleftrightarrow> p = q" |
1573 using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff) |
1562 using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff) |
1574 |
1563 |
1575 |
1564 |
1590 assumes lim_g: "filterlim g at_top at_top" |
1579 assumes lim_g: "filterlim g at_top at_top" |
1591 assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))" |
1580 assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))" |
1592 assumes q: "q > 0" |
1581 assumes q: "q > 0" |
1593 shows "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)" |
1582 shows "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)" |
1594 proof (rule smalloI_tendsto) |
1583 proof (rule smalloI_tendsto) |
1595 from lim_f have "eventually (\<lambda>x. f x > 0) at_top" |
1584 from lim_f have "eventually (\<lambda>x. f x > 0) at_top" |
1596 by (simp add: filterlim_at_top_dense) |
1585 by (simp add: filterlim_at_top_dense) |
1597 hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp |
1586 hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp |
1598 |
1587 |
1599 from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top" |
1588 from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top" |
1600 by (simp add: filterlim_at_top_dense) |
1589 by (simp add: filterlim_at_top_dense) |
1601 hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp |
1590 hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp |
1602 thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top" |
1591 thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top" |
1603 by eventually_elim simp |
1592 by eventually_elim simp |
1604 |
1593 |
1605 have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) = |
1594 have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) = |
1606 p * ln (f x) - q * ln (g x)) at_top" |
1595 p * ln (f x) - q * ln (g x)) at_top" |
1607 using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps) |
1596 using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps) |
1608 have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top" |
1597 have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top" |
1609 by (insert q) |
1598 by (insert q) |
1610 (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult |
1599 (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult |
1651 abbreviation (input) asymp_equiv_at_top where |
1640 abbreviation (input) asymp_equiv_at_top where |
1652 "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g" |
1641 "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g" |
1653 |
1642 |
1654 bundle asymp_equiv_notation |
1643 bundle asymp_equiv_notation |
1655 begin |
1644 begin |
1656 notation asymp_equiv_at_top (infix \<open>\<sim>\<close> 50) |
1645 notation asymp_equiv_at_top (infix \<open>\<sim>\<close> 50) |
1657 end |
1646 end |
1658 |
1647 |
1659 lemma asymp_equivI: "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F \<Longrightarrow> f \<sim>[F] g" |
1648 lemma asymp_equivI: "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F \<Longrightarrow> f \<sim>[F] g" |
1660 by (simp add: asymp_equiv_def) |
1649 by (simp add: asymp_equiv_def) |
1661 |
1650 |
1673 moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp |
1662 moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp |
1674 ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F" |
1663 ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F" |
1675 by (simp add: tendsto_eventually) |
1664 by (simp add: tendsto_eventually) |
1676 qed |
1665 qed |
1677 |
1666 |
1678 lemma asymp_equiv_symI: |
1667 lemma asymp_equiv_symI: |
1679 assumes "f \<sim>[F] g" |
1668 assumes "f \<sim>[F] g" |
1680 shows "g \<sim>[F] f" |
1669 shows "g \<sim>[F] f" |
1681 using tendsto_inverse[OF asymp_equivD[OF assms]] |
1670 using tendsto_inverse[OF asymp_equivD[OF assms]] |
1682 by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong) |
1671 by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong) |
1683 |
1672 |
1684 lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f" |
1673 lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f" |
1685 by (blast intro: asymp_equiv_symI) |
1674 by (blast intro: asymp_equiv_symI) |
1686 |
1675 |
1687 lemma asymp_equivI': |
1676 lemma asymp_equivI': |
1688 assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F" |
1677 assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F" |
1689 shows "f \<sim>[F] g" |
1678 shows "f \<sim>[F] g" |
1690 proof (cases "F = bot") |
1679 proof (cases "F = bot") |
1691 case False |
1680 case False |
1692 have "eventually (\<lambda>x. f x \<noteq> 0) F" |
1681 have "eventually (\<lambda>x. f x \<noteq> 0) F" |
1696 hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1) |
1685 hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1) |
1697 from limit_frequently_eq[OF False this assms] show False by simp_all |
1686 from limit_frequently_eq[OF False this assms] show False by simp_all |
1698 qed |
1687 qed |
1699 hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F" |
1688 hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F" |
1700 by eventually_elim simp |
1689 by eventually_elim simp |
1701 with assms show "f \<sim>[F] g" unfolding asymp_equiv_def |
1690 with assms show "f \<sim>[F] g" unfolding asymp_equiv_def |
1702 by (rule Lim_transform_eventually) |
1691 by (rule Lim_transform_eventually) |
1703 qed (simp_all add: asymp_equiv_def) |
1692 qed (simp_all add: asymp_equiv_def) |
1704 |
1693 |
1705 |
1694 |
1706 lemma asymp_equiv_cong: |
1695 lemma asymp_equiv_cong: |
1742 fixes f g h |
1731 fixes f g h |
1743 assumes "f \<sim>[F] g" "g \<sim>[F] h" |
1732 assumes "f \<sim>[F] g" "g \<sim>[F] h" |
1744 shows "f \<sim>[F] h" |
1733 shows "f \<sim>[F] h" |
1745 proof - |
1734 proof - |
1746 let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x" |
1735 let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x" |
1747 from tendsto_mult[OF assms[THEN asymp_equivD]] |
1736 from tendsto_mult[OF assms[THEN asymp_equivD]] |
1748 have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp |
1737 have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp |
1749 moreover from assms[THEN asymp_equiv_eventually_zeros] |
1738 moreover from assms[THEN asymp_equiv_eventually_zeros] |
1750 have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp |
1739 have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp |
1751 ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually) |
1740 ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually) |
1752 qed |
1741 qed |
1815 by simp |
1804 by simp |
1816 thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" |
1805 thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" |
1817 proof eventually_elim |
1806 proof eventually_elim |
1818 case (elim x) |
1807 case (elim x) |
1819 thus ?case |
1808 thus ?case |
1820 by (cases "f x" "0 :: real" rule: linorder_cases; |
1809 by (cases "f x" "0 :: real" rule: linorder_cases; |
1821 cases "g x" "0 :: real" rule: linorder_cases) simp_all |
1810 cases "g x" "0 :: real" rule: linorder_cases) simp_all |
1822 qed |
1811 qed |
1823 qed |
1812 qed |
1824 |
1813 |
1825 lemma |
1814 lemma |
1843 let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x" |
1832 let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x" |
1844 from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI) |
1833 from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI) |
1845 hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F" |
1834 hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F" |
1846 by (rule asymp_equivD) |
1835 by (rule asymp_equivD) |
1847 from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp |
1836 from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp |
1848 moreover |
1837 moreover |
1849 have "eventually (\<lambda>x. ?h x = g x) F" |
1838 have "eventually (\<lambda>x. ?h x = g x) F" |
1850 using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp |
1839 using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp |
1851 ultimately show ?thesis |
1840 ultimately show ?thesis |
1852 by (rule Lim_transform_eventually) |
1841 by (rule Lim_transform_eventually) |
1853 qed |
1842 qed |
1854 |
1843 |
1855 lemma tendsto_asymp_equiv_cong: |
1844 lemma tendsto_asymp_equiv_cong: |
1856 assumes "f \<sim>[F] g" |
1845 assumes "f \<sim>[F] g" |
1857 shows "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F" |
1846 shows "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F" |
1858 proof - |
1847 proof - |
1859 { |
1848 have "(f \<longlongrightarrow> c * 1) F" if fg: "f \<sim>[F] g" and "(g \<longlongrightarrow> c) F" for f g :: "'a \<Rightarrow> 'b" |
1860 fix f g :: "'a \<Rightarrow> 'b" |
1849 proof - |
1861 assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F" |
1850 from that have *: "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F" |
1862 have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F" |
1851 by (intro tendsto_intros asymp_equivD) |
1863 by (intro tendsto_intros asymp_equivD *) |
|
1864 moreover |
|
1865 have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F" |
1852 have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F" |
1866 using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp |
1853 using asymp_equiv_eventually_zeros[OF fg] by eventually_elim simp |
1867 ultimately have "(f \<longlongrightarrow> c * 1) F" |
1854 with * show ?thesis by (rule Lim_transform_eventually) |
1868 by (rule Lim_transform_eventually) |
1855 qed |
1869 } |
|
1870 from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym) |
1856 from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym) |
1871 qed |
1857 qed |
1872 |
1858 |
1873 |
1859 |
1874 lemma smallo_imp_eventually_sgn: |
1860 lemma smallo_imp_eventually_sgn: |
1875 fixes f g :: "real \<Rightarrow> real" |
1861 fixes f g :: "real \<Rightarrow> real" |
1876 assumes "g \<in> o(f)" |
1862 assumes "g \<in> o(f)" |
1877 shows "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top" |
1863 shows "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top" |
1878 proof - |
1864 proof - |
1879 have "0 < (1/2 :: real)" by simp |
1865 have "0 < (1/2 :: real)" by simp |
1880 from landau_o.smallD[OF assms, OF this] |
1866 from landau_o.smallD[OF assms, OF this] |
1881 have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp |
1867 have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp |
1882 thus ?thesis |
1868 thus ?thesis |
1883 proof eventually_elim |
1869 proof eventually_elim |
1884 case (elim x) |
1870 case (elim x) |
1885 thus ?case |
1871 thus ?case |
1886 by (cases "f x" "0::real" rule: linorder_cases; |
1872 by (cases "f x" "0::real" rule: linorder_cases; |
1887 cases "f x + g x" "0::real" rule: linorder_cases) simp_all |
1873 cases "f x + g x" "0::real" rule: linorder_cases) simp_all |
1888 qed |
1874 qed |
1889 qed |
1875 qed |
1890 |
1876 |
1891 context |
1877 context |
1915 by simp |
1901 by simp |
1916 qed (simp_all add: asymp_equiv_add_rightI assms) |
1902 qed (simp_all add: asymp_equiv_add_rightI assms) |
1917 |
1903 |
1918 end |
1904 end |
1919 |
1905 |
1920 lemma asymp_equiv_add_left [asymp_equiv_simps]: |
1906 lemma asymp_equiv_add_left [asymp_equiv_simps]: |
1921 assumes "h \<in> o[F](g)" |
1907 assumes "h \<in> o[F](g)" |
1922 shows "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g" |
1908 shows "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g" |
1923 using asymp_equiv_add_right[OF assms] by (simp add: add.commute) |
1909 using asymp_equiv_add_right[OF assms] by (simp add: add.commute) |
1924 |
1910 |
1925 lemma asymp_equiv_add_right' [asymp_equiv_simps]: |
1911 lemma asymp_equiv_add_right' [asymp_equiv_simps]: |
1926 assumes "h \<in> o[F](g)" |
1912 assumes "h \<in> o[F](g)" |
1927 shows "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f" |
1913 shows "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f" |
1928 using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym) |
1914 using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym) |
1929 |
1915 |
1930 lemma asymp_equiv_add_left' [asymp_equiv_simps]: |
1916 lemma asymp_equiv_add_left' [asymp_equiv_simps]: |
1931 assumes "h \<in> o[F](g)" |
1917 assumes "h \<in> o[F](g)" |
1932 shows "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f" |
1918 shows "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f" |
1933 using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym) |
1919 using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym) |
1934 |
1920 |
1956 proof - |
1942 proof - |
1957 let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x" |
1943 let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x" |
1958 let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x |
1944 let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x |
1959 else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)" |
1945 else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)" |
1960 let ?S' = "\<lambda>x. ?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) x - ?T f1 g1 x * ?T f2 g2 x" |
1946 let ?S' = "\<lambda>x. ?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) x - ?T f1 g1 x * ?T f2 g2 x" |
1947 have A: "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F" if "f \<sim>[F] g" for f g :: "'a \<Rightarrow> 'b" |
|
1948 by (rule tendsto_eq_intros refl asymp_equivD[OF that])+ simp_all |
|
1949 |
|
1950 from assms have *: "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F" |
|
1951 by (intro tendsto_mult asymp_equivD) |
|
1961 { |
1952 { |
1962 fix f g :: "'a \<Rightarrow> 'b" assume "f \<sim>[F] g" |
|
1963 have "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F" |
|
1964 by (rule tendsto_eq_intros refl asymp_equivD[OF \<open>f \<sim>[F] g\<close>])+ simp_all |
|
1965 } note A = this |
|
1966 |
|
1967 from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F" |
|
1968 by (intro tendsto_mult asymp_equivD) |
|
1969 moreover { |
|
1970 have "(?S \<longlongrightarrow> 0) F" |
1953 have "(?S \<longlongrightarrow> 0) F" |
1971 by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]]) |
1954 by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]]) |
1972 (auto intro: le_infI1 le_infI2) |
1955 (auto intro: le_infI1 le_infI2) |
1973 moreover have "eventually (\<lambda>x. ?S x = ?S' x) F" |
1956 moreover have "eventually (\<lambda>x. ?S x = ?S' x) F" |
1974 using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto |
1957 using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto |
1975 ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually) |
1958 ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually) |
1976 } |
1959 } |
1977 ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F" |
1960 with * have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F" |
1978 by (rule Lim_transform) |
1961 by (rule Lim_transform) |
1979 thus ?thesis by (simp add: asymp_equiv_def) |
1962 then show ?thesis by (simp add: asymp_equiv_def) |
1980 qed |
1963 qed |
1981 |
1964 |
1982 lemma asymp_equiv_power [asymp_equiv_intros]: |
1965 lemma asymp_equiv_power [asymp_equiv_intros]: |
1983 "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)" |
1966 "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)" |
1984 by (induction n) (simp_all add: asymp_equiv_mult) |
1967 by (induction n) (simp_all add: asymp_equiv_mult) |
2027 |
2010 |
2028 lemma asymp_equiv_compose': |
2011 lemma asymp_equiv_compose': |
2029 assumes "f \<sim>[G] g" "filterlim h G F" |
2012 assumes "f \<sim>[G] g" "filterlim h G F" |
2030 shows "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))" |
2013 shows "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))" |
2031 using asymp_equiv_compose[OF assms] by (simp add: o_def) |
2014 using asymp_equiv_compose[OF assms] by (simp add: o_def) |
2032 |
2015 |
2033 lemma asymp_equiv_powr_real [asymp_equiv_intros]: |
2016 lemma asymp_equiv_powr_real [asymp_equiv_intros]: |
2034 fixes f g :: "'a \<Rightarrow> real" |
2017 fixes f g :: "'a \<Rightarrow> real" |
2035 assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F" |
2018 assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F" |
2036 shows "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)" |
2019 shows "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)" |
2037 proof - |
2020 proof - |
2047 |
2030 |
2048 lemma asymp_equiv_norm [asymp_equiv_intros]: |
2031 lemma asymp_equiv_norm [asymp_equiv_intros]: |
2049 fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field" |
2032 fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field" |
2050 assumes "f \<sim>[F] g" |
2033 assumes "f \<sim>[F] g" |
2051 shows "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))" |
2034 shows "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))" |
2052 using tendsto_norm[OF asymp_equivD[OF assms]] |
2035 using tendsto_norm[OF asymp_equivD[OF assms]] |
2053 by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong) |
2036 by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong) |
2054 |
2037 |
2055 lemma asymp_equiv_abs_real [asymp_equiv_intros]: |
2038 lemma asymp_equiv_abs_real [asymp_equiv_intros]: |
2056 fixes f g :: "'a \<Rightarrow> real" |
2039 fixes f g :: "'a \<Rightarrow> real" |
2057 assumes "f \<sim>[F] g" |
2040 assumes "f \<sim>[F] g" |
2058 shows "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)" |
2041 shows "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)" |
2059 using tendsto_rabs[OF asymp_equivD[OF assms]] |
2042 using tendsto_rabs[OF asymp_equivD[OF assms]] |
2060 by (simp add: if_distrib asymp_equiv_def cong: if_cong) |
2043 by (simp add: if_distrib asymp_equiv_def cong: if_cong) |
2061 |
2044 |
2062 lemma asymp_equiv_imp_eventually_le: |
2045 lemma asymp_equiv_imp_eventually_le: |
2063 assumes "f \<sim>[F] g" "c > 1" |
2046 assumes "f \<sim>[F] g" "c > 1" |
2064 shows "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F" |
2047 shows "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F" |
2122 fixes f g :: "_ \<Rightarrow> real" |
2105 fixes f g :: "_ \<Rightarrow> real" |
2123 assumes "f \<sim>[F] g" "filterlim f at_bot F" |
2106 assumes "f \<sim>[F] g" "filterlim f at_bot F" |
2124 shows "filterlim g at_bot F" |
2107 shows "filterlim g at_bot F" |
2125 unfolding filterlim_uminus_at_bot |
2108 unfolding filterlim_uminus_at_bot |
2126 by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"]) |
2109 by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"]) |
2127 (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus) |
2110 (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus) |
2128 |
2111 |
2129 lemma asymp_equivI'_const: |
2112 lemma asymp_equivI'_const: |
2130 assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0" |
2113 assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0" |
2131 shows "f \<sim>[F] (\<lambda>x. c * g x)" |
2114 shows "f \<sim>[F] (\<lambda>x. c * g x)" |
2132 using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2) |
2115 using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2) |