Moved Landau_Symbols from the AFP to HOL-Library
authorManuel Eberl <eberlm@in.tum.de>
Fri May 18 17:51:58 2018 +0200 (13 months ago)
changeset 68246b48bab511939
parent 68245 37974ddde928
child 68248 ef1e0cb80fde
Moved Landau_Symbols from the AFP to HOL-Library
CONTRIBUTORS
NEWS
src/HOL/Library/Landau_Symbols.thy
src/HOL/Library/Library.thy
     1.1 --- a/CONTRIBUTORS	Tue May 22 11:05:47 2018 +0200
     1.2 +++ b/CONTRIBUTORS	Fri May 18 17:51:58 2018 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* May 2018: Manuel Eberl
     1.8 +  Landau symbols and asymptotic equivalence (moved from the AFP)
     1.9 +
    1.10  * May 2018: Jose Divasón (Universidad de la Rioja),
    1.11    Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
    1.12    Fabian Immler (TUM)
     2.1 --- a/NEWS	Tue May 22 11:05:47 2018 +0200
     2.2 +++ b/NEWS	Fri May 18 17:51:58 2018 +0200
     2.3 @@ -201,6 +201,8 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Landau_Symbols from the AFP was moved to HOL-Library
     2.8 +
     2.9  * Clarified relationship of characters, strings and code generation:
    2.10  
    2.11    * Type "char" is now a proper datatype of 8-bit values.
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Landau_Symbols.thy	Fri May 18 17:51:58 2018 +0200
     3.3 @@ -0,0 +1,2208 @@
     3.4 +(*
     3.5 +  File:   Landau_Symbols_Definition.thy
     3.6 +  Author: Manuel Eberl <eberlm@in.tum.de>
     3.7 +
     3.8 +  Landau symbols for reasoning about the asymptotic growth of functions. 
     3.9 +*)
    3.10 +section {* Definition of Landau symbols *}
    3.11 +
    3.12 +theory Landau_Symbols
    3.13 +imports 
    3.14 +  Complex_Main
    3.15 +begin
    3.16 +
    3.17 +lemma eventually_subst':
    3.18 +  "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"
    3.19 +  by (rule eventually_subst, erule eventually_rev_mp) simp
    3.20 +
    3.21 +
    3.22 +subsection {* Definition of Landau symbols *}
    3.23 +
    3.24 +text {*
    3.25 +  Our Landau symbols are sign-oblivious, i.e. any function always has the same growth 
    3.26 +  as its absolute. This has the advantage of making some cancelling rules for sums nicer, but 
    3.27 +  introduces some problems in other places. Nevertheless, we found this definition more convenient
    3.28 +  to work with.
    3.29 +*}
    3.30 +
    3.31 +definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    3.32 +    ("(1O[_]'(_'))")
    3.33 +  where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"  
    3.34 +
    3.35 +definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    3.36 +    ("(1o[_]'(_'))")
    3.37 +  where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
    3.38 +
    3.39 +definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    3.40 +    ("(1\<Omega>[_]'(_'))")
    3.41 +  where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"  
    3.42 +
    3.43 +definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    3.44 +    ("(1\<omega>[_]'(_'))")
    3.45 +  where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
    3.46 +
    3.47 +definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    3.48 +    ("(1\<Theta>[_]'(_'))")
    3.49 +  where "bigtheta F g = bigo F g \<inter> bigomega F g"
    3.50 +
    3.51 +abbreviation bigo_at_top ("(2O'(_'))") where
    3.52 +  "O(g) \<equiv> bigo at_top g"    
    3.53 +
    3.54 +abbreviation smallo_at_top ("(2o'(_'))") where
    3.55 +  "o(g) \<equiv> smallo at_top g"
    3.56 +
    3.57 +abbreviation bigomega_at_top ("(2\<Omega>'(_'))") where
    3.58 +  "\<Omega>(g) \<equiv> bigomega at_top g"
    3.59 +
    3.60 +abbreviation smallomega_at_top ("(2\<omega>'(_'))") where
    3.61 +  "\<omega>(g) \<equiv> smallomega at_top g"
    3.62 +
    3.63 +abbreviation bigtheta_at_top ("(2\<Theta>'(_'))") where
    3.64 +  "\<Theta>(g) \<equiv> bigtheta at_top g"
    3.65 +    
    3.66 +
    3.67 +text {* The following is a set of properties that all Landau symbols satisfy. *}
    3.68 +
    3.69 +named_theorems landau_divide_simps
    3.70 +
    3.71 +locale landau_symbol =
    3.72 +  fixes L  :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
    3.73 +  and   L'  :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"
    3.74 +  and   Lr  :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"
    3.75 +  assumes bot': "L bot f = UNIV"
    3.76 +  assumes filter_mono': "F1 \<le> F2 \<Longrightarrow> L F2 f \<subseteq> L F1 f"
    3.77 +  assumes in_filtermap_iff: 
    3.78 +    "f' \<in> L (filtermap h' F') g' \<longleftrightarrow> (\<lambda>x. f' (h' x)) \<in> L' F' (\<lambda>x. g' (h' x))"
    3.79 +  assumes filtercomap: 
    3.80 +    "f' \<in> L F'' g' \<Longrightarrow> (\<lambda>x. f' (h' x)) \<in> L' (filtercomap h' F'') (\<lambda>x. g' (h' x))"
    3.81 +  assumes sup: "f \<in> L F1 g \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L (sup F1 F2) g"
    3.82 +  assumes in_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"
    3.83 +  assumes cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> L F (f) = L F (g)"
    3.84 +  assumes cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> L F (f) = L F (g)"
    3.85 +  assumes in_cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"
    3.86 +  assumes cmult [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. c * f x) = L F (f)"
    3.87 +  assumes cmult_in_iff [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
    3.88 +  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)"
    3.89 +  assumes inverse: "eventually (\<lambda>x. f x \<noteq> 0) F \<Longrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F \<Longrightarrow> 
    3.90 +                        f \<in> L F (g) \<Longrightarrow> (\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))"
    3.91 +  assumes subsetI: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"
    3.92 +  assumes plus_subset1: "f \<in> o[F](g) \<Longrightarrow> L F (g) \<subseteq> L F (\<lambda>x. f x + g x)"
    3.93 +  assumes trans: "f \<in> L F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
    3.94 +  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))"
    3.95 +  assumes norm_iff [simp]: "(\<lambda>x. norm (f x)) \<in> Lr F (\<lambda>x. norm (g x)) \<longleftrightarrow> f \<in> L F (g)"
    3.96 +  assumes abs [simp]: "Lr Fr (\<lambda>x. \<bar>fr x\<bar>) = Lr Fr fr"
    3.97 +  assumes abs_in_iff [simp]: "(\<lambda>x. \<bar>fr x\<bar>) \<in> Lr Fr gr \<longleftrightarrow> fr \<in> Lr Fr gr"
    3.98 +begin
    3.99 +
   3.100 +lemma bot [simp]: "f \<in> L bot g" by (simp add: bot')
   3.101 +  
   3.102 +lemma filter_mono: "F1 \<le> F2 \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L F1 g"
   3.103 +  using filter_mono'[of F1 F2] by blast
   3.104 +
   3.105 +lemma cong_ex: 
   3.106 +  "eventually (\<lambda>x. f1 x = f2 x) F \<Longrightarrow> eventually (\<lambda>x. g1 x = g2 x) F \<Longrightarrow>
   3.107 +     f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" 
   3.108 +  by (subst cong, assumption, subst in_cong, assumption, rule refl)
   3.109 +
   3.110 +lemma cong_ex_bigtheta: 
   3.111 +  "f1 \<in> \<Theta>[F](f2) \<Longrightarrow> g1 \<in> \<Theta>[F](g2) \<Longrightarrow> f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" 
   3.112 +  by (subst cong_bigtheta, assumption, subst in_cong_bigtheta, assumption, rule refl)
   3.113 +
   3.114 +lemma bigtheta_trans1: 
   3.115 +  "f \<in> L F (g) \<Longrightarrow> g \<in> \<Theta>[F](h) \<Longrightarrow> f \<in> L F (h)"
   3.116 +  by (subst cong_bigtheta[symmetric])
   3.117 +
   3.118 +lemma bigtheta_trans2: 
   3.119 +  "f \<in> \<Theta>[F](g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
   3.120 +  by (subst in_cong_bigtheta)
   3.121 +   
   3.122 +lemma cmult' [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x * c) = L F (f)"
   3.123 +  by (subst mult.commute) (rule cmult)
   3.124 +
   3.125 +lemma cmult_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x * c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
   3.126 +  by (subst mult.commute) (rule cmult_in_iff)
   3.127 +
   3.128 +lemma cdiv [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x / c) = L F (f)"
   3.129 +  using cmult'[of "inverse c" F f] by (simp add: field_simps)
   3.130 +
   3.131 +lemma cdiv_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
   3.132 +  using cmult_in_iff'[of "inverse c" f] by (simp add: field_simps)
   3.133 +  
   3.134 +lemma uminus [simp]: "L F (\<lambda>x. -g x) = L F (g)" using cmult[of "-1"] by simp
   3.135 +
   3.136 +lemma uminus_in_iff [simp]: "(\<lambda>x. -f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
   3.137 +  using cmult_in_iff[of "-1"] by simp
   3.138 +
   3.139 +lemma const: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"
   3.140 +  by (subst (2) cmult[symmetric]) simp_all
   3.141 +
   3.142 +(* Simplifier loops without the NO_MATCH *)
   3.143 +lemma const' [simp]: "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"
   3.144 +  by (rule const)
   3.145 +
   3.146 +lemma const_in_iff: "c \<noteq> 0 \<Longrightarrow> (\<lambda>_. c) \<in> L F (f) \<longleftrightarrow> (\<lambda>_. 1) \<in> L F (f)"
   3.147 +  using cmult_in_iff'[of c "\<lambda>_. 1"] by simp
   3.148 +
   3.149 +lemma const_in_iff' [simp]: "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> (\<lambda>_. c) \<in> L F (f) \<longleftrightarrow> (\<lambda>_. 1) \<in> L F (f)"
   3.150 +  by (rule const_in_iff)
   3.151 +
   3.152 +lemma plus_subset2: "g \<in> o[F](f) \<Longrightarrow> L F (f) \<subseteq> L F (\<lambda>x. f x + g x)"
   3.153 +  by (subst add.commute) (rule plus_subset1)
   3.154 +
   3.155 +lemma mult_right [simp]: "f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (\<lambda>x. g x * h x)"
   3.156 +  using mult_left by (simp add: mult.commute)
   3.157 +
   3.158 +lemma 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)"
   3.159 +  by (rule trans, erule mult_left, erule mult_right)
   3.160 +
   3.161 +lemma inverse_cancel:
   3.162 +  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
   3.163 +  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
   3.164 +  shows   "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> g \<in> L F (f)"
   3.165 +proof
   3.166 +  assume "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x))"
   3.167 +  from inverse[OF _ _ this] assms show "g \<in> L F (f)" by simp
   3.168 +qed (intro inverse assms)
   3.169 +
   3.170 +lemma divide_right:
   3.171 +  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   3.172 +  assumes "f \<in> L F (g)"
   3.173 +  shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"
   3.174 +  by (subst (1 2) divide_inverse) (intro mult_right inverse assms)
   3.175 +
   3.176 +lemma divide_right_iff:
   3.177 +  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   3.178 +  shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> f \<in> L F (g)"
   3.179 +proof
   3.180 +  assume "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"
   3.181 +  from mult_right[OF this, of h] assms show "f \<in> L F (g)"
   3.182 +    by (subst (asm) cong_ex[of _ f F _ g]) (auto elim!: eventually_mono)
   3.183 +qed (simp add: divide_right assms)
   3.184 +
   3.185 +lemma divide_left:
   3.186 +  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
   3.187 +  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
   3.188 +  assumes "g \<in> L F(f)"
   3.189 +  shows   "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"
   3.190 +  by (subst (1 2) divide_inverse) (intro mult_left inverse assms)
   3.191 +
   3.192 +lemma divide_left_iff:
   3.193 +  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
   3.194 +  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
   3.195 +  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   3.196 +  shows   "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x) \<longleftrightarrow> g \<in> L F (f)"
   3.197 +proof
   3.198 +  assume A: "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"
   3.199 +  from assms have B: "eventually (\<lambda>x. h x / f x / h x = inverse (f x)) F"
   3.200 +    by eventually_elim (simp add: divide_inverse)
   3.201 +  from assms have C: "eventually (\<lambda>x. h x / g x / h x = inverse (g x)) F"
   3.202 +    by eventually_elim (simp add: divide_inverse)
   3.203 +  from divide_right[OF assms(3) A] assms show "g \<in> L F (f)"
   3.204 +    by (subst (asm) cong_ex[OF B C]) (simp add: inverse_cancel)
   3.205 +qed (simp add: divide_left assms)
   3.206 +
   3.207 +lemma divide:
   3.208 +  assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
   3.209 +  assumes "eventually (\<lambda>x. g2 x \<noteq> 0) F"
   3.210 +  assumes "f1 \<in> L F (f2)" "g2 \<in> L F (g1)"
   3.211 +  shows   "(\<lambda>x. f1 x / g1 x) \<in> L F (\<lambda>x. f2 x / g2 x)"
   3.212 +  by (subst (1 2) divide_inverse) (intro mult inverse assms)
   3.213 +  
   3.214 +lemma divide_eq1:
   3.215 +  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   3.216 +  shows   "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
   3.217 +proof-
   3.218 +  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)"
   3.219 +    using assms by (intro in_cong) (auto elim: eventually_mono)
   3.220 +  thus ?thesis by (simp only: divide_right_iff assms)
   3.221 +qed
   3.222 +
   3.223 +lemma divide_eq2:
   3.224 +  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   3.225 +  shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x) \<longleftrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
   3.226 +proof-
   3.227 +  have "L F (\<lambda>x. g x) = L F (\<lambda>x. g x * h x / h x)"
   3.228 +    using assms by (intro cong) (auto elim: eventually_mono)
   3.229 +  thus ?thesis by (simp only: divide_right_iff assms)
   3.230 +qed
   3.231 +
   3.232 +lemma inverse_eq1:
   3.233 +  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
   3.234 +  shows   "f \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> (\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"
   3.235 +  using divide_eq1[of g F f "\<lambda>_. 1"] by (simp add: divide_inverse assms)
   3.236 +
   3.237 +lemma inverse_eq2:
   3.238 +  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
   3.239 +  shows   "(\<lambda>x. inverse (f x)) \<in> L F (g) \<longleftrightarrow> (\<lambda>x. 1) \<in> L F (\<lambda>x. f x * g x)"
   3.240 +  using divide_eq2[of f F "\<lambda>_. 1" g] by (simp add: divide_inverse assms mult_ac)
   3.241 +
   3.242 +lemma inverse_flip:
   3.243 +  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
   3.244 +  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   3.245 +  assumes "(\<lambda>x. inverse (g x)) \<in> L F (h)"
   3.246 +  shows   "(\<lambda>x. inverse (h x)) \<in> L F (g)"
   3.247 +using assms by (simp add: divide_eq1 divide_eq2 inverse_eq_divide mult.commute)
   3.248 +
   3.249 +lemma lift_trans:
   3.250 +  assumes "f \<in> L F (g)"
   3.251 +  assumes "(\<lambda>x. t x (g x)) \<in> L F (h)"
   3.252 +  assumes "\<And>f g. f \<in> L F (g) \<Longrightarrow> (\<lambda>x. t x (f x)) \<in> L F (\<lambda>x. t x (g x))"
   3.253 +  shows   "(\<lambda>x. t x (f x)) \<in> L F (h)"
   3.254 +  by (rule trans[OF assms(3)[OF assms(1)] assms(2)])
   3.255 +
   3.256 +lemma lift_trans':
   3.257 +  assumes "f \<in> L F (\<lambda>x. t x (g x))"
   3.258 +  assumes "g \<in> L F (h)"
   3.259 +  assumes "\<And>g h. g \<in> L F (h) \<Longrightarrow> (\<lambda>x. t x (g x)) \<in> L F (\<lambda>x. t x (h x))"
   3.260 +  shows   "f \<in> L F (\<lambda>x. t x (h x))"
   3.261 +  by (rule trans[OF assms(1) assms(3)[OF assms(2)]])
   3.262 +
   3.263 +lemma lift_trans_bigtheta:
   3.264 +  assumes "f \<in> L F (g)"
   3.265 +  assumes "(\<lambda>x. t x (g x)) \<in> \<Theta>[F](h)"
   3.266 +  assumes "\<And>f g. f \<in> L F (g) \<Longrightarrow> (\<lambda>x. t x (f x)) \<in> L F (\<lambda>x. t x (g x))"
   3.267 +  shows   "(\<lambda>x. t x (f x)) \<in> L F (h)"
   3.268 +  using cong_bigtheta[OF assms(2)] assms(3)[OF assms(1)] by simp
   3.269 +
   3.270 +lemma lift_trans_bigtheta':
   3.271 +  assumes "f \<in> L F (\<lambda>x. t x (g x))"
   3.272 +  assumes "g \<in> \<Theta>[F](h)"
   3.273 +  assumes "\<And>g h. g \<in> \<Theta>[F](h) \<Longrightarrow> (\<lambda>x. t x (g x)) \<in> \<Theta>[F](\<lambda>x. t x (h x))"
   3.274 +  shows   "f \<in> L F (\<lambda>x. t x (h x))"
   3.275 +  using cong_bigtheta[OF assms(3)[OF assms(2)]] assms(1)  by simp
   3.276 +
   3.277 +lemma (in landau_symbol) mult_in_1:
   3.278 +  assumes "f \<in> L F (\<lambda>_. 1)" "g \<in> L F (\<lambda>_. 1)"
   3.279 +  shows   "(\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"
   3.280 +  using mult[OF assms] by simp
   3.281 +
   3.282 +lemma (in landau_symbol) of_real_cancel:
   3.283 +  "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<Longrightarrow> f \<in> Lr F g"
   3.284 +  by (subst (asm) norm_iff [symmetric], subst (asm) (1 2) norm_of_real) simp_all
   3.285 +
   3.286 +lemma (in landau_symbol) of_real_iff:
   3.287 +  "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<longleftrightarrow> f \<in> Lr F g"
   3.288 +  by (subst norm_iff [symmetric], subst (1 2) norm_of_real) simp_all
   3.289 +
   3.290 +lemmas [landau_divide_simps] = 
   3.291 +  inverse_cancel divide_left_iff divide_eq1 divide_eq2 inverse_eq1 inverse_eq2
   3.292 +
   3.293 +end
   3.294 +
   3.295 +
   3.296 +text {* 
   3.297 +  The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with 
   3.298 +  $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem.
   3.299 +  The following locale captures this fact.
   3.300 +*}
   3.301 +
   3.302 +locale landau_pair = 
   3.303 +  fixes L l :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
   3.304 +  fixes L' l' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"
   3.305 +  fixes Lr lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"
   3.306 +  and   R :: "real \<Rightarrow> real \<Rightarrow> bool"
   3.307 +  assumes L_def: "L F g = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"
   3.308 +  and     l_def: "l F g = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"
   3.309 +  and     L'_def: "L' F' g' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"
   3.310 +  and     l'_def: "l' F' g' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"
   3.311 +  and     Lr_def: "Lr F'' g'' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"
   3.312 +  and     lr_def: "lr F'' g'' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"
   3.313 +  and     R:     "R = (\<le>) \<or> R = (\<ge>)"
   3.314 +
   3.315 +interpretation landau_o: 
   3.316 +    landau_pair bigo smallo bigo smallo bigo smallo "(\<le>)"
   3.317 +  by unfold_locales (auto simp: bigo_def smallo_def intro!: ext)
   3.318 +
   3.319 +interpretation landau_omega: 
   3.320 +    landau_pair bigomega smallomega bigomega smallomega bigomega smallomega "(\<ge>)"
   3.321 +  by unfold_locales (auto simp: bigomega_def smallomega_def intro!: ext)
   3.322 +
   3.323 +
   3.324 +context landau_pair
   3.325 +begin
   3.326 +
   3.327 +lemmas R_E = disjE [OF R, case_names le ge]
   3.328 +
   3.329 +lemma bigI:
   3.330 +  "c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F \<Longrightarrow> f \<in> L F (g)"
   3.331 +  unfolding L_def by blast
   3.332 +
   3.333 +lemma bigE:
   3.334 +  assumes "f \<in> L F (g)"
   3.335 +  obtains c where "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"
   3.336 +  using assms unfolding L_def by blast
   3.337 +
   3.338 +lemma smallI:
   3.339 +  "(\<And>c. c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F) \<Longrightarrow> f \<in> l F (g)"
   3.340 +  unfolding l_def by blast
   3.341 +
   3.342 +lemma smallD:
   3.343 +  "f \<in> l F (g) \<Longrightarrow> c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"
   3.344 +  unfolding l_def by blast
   3.345 +    
   3.346 +lemma bigE_nonneg_real:
   3.347 +  assumes "f \<in> Lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F"
   3.348 +  obtains c where "c > 0" "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
   3.349 +proof-
   3.350 +  from assms(1) obtain c where c: "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
   3.351 +    by (auto simp: Lr_def)
   3.352 +  from c(2) assms(2) have "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
   3.353 +    by eventually_elim simp
   3.354 +  from c(1) and this show ?thesis by (rule that)
   3.355 +qed
   3.356 +
   3.357 +lemma smallD_nonneg_real:
   3.358 +  assumes "f \<in> lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F" "c > 0"
   3.359 +  shows   "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
   3.360 +  using assms by (auto simp: lr_def dest!: spec[of _ c] elim: eventually_elim2)
   3.361 +
   3.362 +lemma small_imp_big: "f \<in> l F (g) \<Longrightarrow> f \<in> L F (g)"
   3.363 +  by (rule bigI[OF _ smallD, of 1]) simp_all
   3.364 +  
   3.365 +lemma small_subset_big: "l F (g) \<subseteq> L F (g)"
   3.366 +  using small_imp_big by blast
   3.367 +
   3.368 +lemma R_refl [simp]: "R x x" using R by auto
   3.369 +
   3.370 +lemma R_linear: "\<not>R x y \<Longrightarrow> R y x"
   3.371 +  using R by auto
   3.372 +
   3.373 +lemma R_trans [trans]: "R a b \<Longrightarrow> R b c \<Longrightarrow> R a c"
   3.374 +  using R by auto
   3.375 +
   3.376 +lemma R_mult_left_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (c*a) (c*b)"
   3.377 +  using R by (auto simp: mult_left_mono)
   3.378 +
   3.379 +lemma R_mult_right_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (a*c) (b*c)"
   3.380 +  using R by (auto simp: mult_right_mono)
   3.381 +
   3.382 +lemma big_trans:
   3.383 +  assumes "f \<in> L F (g)" "g \<in> L F (h)"
   3.384 +  shows   "f \<in> L F (h)"
   3.385 +proof-
   3.386 +  from assms(1) guess c by (elim bigE) note c = this
   3.387 +  from assms(2) guess d by (elim bigE) note d = this
   3.388 +  from c(2) d(2) have "eventually (\<lambda>x. R (norm (f x)) (c * d * (norm (h x)))) F"
   3.389 +  proof eventually_elim
   3.390 +    fix x assume "R (norm (f x)) (c * (norm (g x)))"
   3.391 +    also assume "R (norm (g x)) (d * (norm (h x)))"
   3.392 +    with c(1) have "R (c * (norm (g x))) (c * (d * (norm (h x))))"
   3.393 +      by (intro R_mult_left_mono) simp_all
   3.394 +    finally show "R (norm (f x)) (c * d * (norm (h x)))" by (simp add: algebra_simps)
   3.395 +  qed
   3.396 +  with c(1) d(1) show ?thesis by (intro bigI[of "c*d"]) simp_all
   3.397 +qed
   3.398 +
   3.399 +lemma big_small_trans:
   3.400 +  assumes "f \<in> L F (g)" "g \<in> l F (h)"
   3.401 +  shows   "f \<in> l F (h)"
   3.402 +proof (rule smallI)
   3.403 +  fix c :: real assume c: "c > 0"
   3.404 +  from assms(1) guess d by (elim bigE) note d = this
   3.405 +  note d(2)
   3.406 +  moreover from c d assms(2) 
   3.407 +    have "eventually (\<lambda>x. R (norm (g x)) (c * inverse d * norm (h x))) F" 
   3.408 +    by (intro smallD) simp_all
   3.409 +  ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * (norm (h x)))) F"
   3.410 +    by eventually_elim (erule R_trans, insert R d(1), auto simp: field_simps)
   3.411 +qed
   3.412 +
   3.413 +lemma small_big_trans:
   3.414 +  assumes "f \<in> l F (g)" "g \<in> L F (h)"
   3.415 +  shows   "f \<in> l F (h)"
   3.416 +proof (rule smallI)
   3.417 +  fix c :: real assume c: "c > 0"
   3.418 +  from assms(2) guess d by (elim bigE) note d = this
   3.419 +  note d(2)
   3.420 +  moreover from c d assms(1) 
   3.421 +    have "eventually (\<lambda>x. R (norm (f x)) (c * inverse d * norm (g x))) F"
   3.422 +    by (intro smallD) simp_all
   3.423 +  ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * norm (h x))) F"
   3.424 +    by eventually_elim (rotate_tac 2, erule R_trans, insert R c d(1), auto simp: field_simps)
   3.425 +qed
   3.426 +
   3.427 +lemma small_trans:
   3.428 +  "f \<in> l F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> l F (h)"
   3.429 +  by (rule big_small_trans[OF small_imp_big])
   3.430 +
   3.431 +lemma small_big_trans':
   3.432 +  "f \<in> l F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
   3.433 +  by (rule small_imp_big[OF small_big_trans])
   3.434 +
   3.435 +lemma big_small_trans':
   3.436 +  "f \<in> L F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> L F (h)"
   3.437 +  by (rule small_imp_big[OF big_small_trans])
   3.438 +
   3.439 +lemma big_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"
   3.440 +  by (intro subsetI) (drule (1) big_trans)
   3.441 +
   3.442 +lemma small_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> l F (f) \<subseteq> l F (g)"
   3.443 +  by (intro subsetI) (drule (1) small_big_trans)
   3.444 +
   3.445 +lemma big_refl [simp]: "f \<in> L F (f)"
   3.446 +  by (rule bigI[of 1]) simp_all
   3.447 +
   3.448 +lemma small_refl_iff: "f \<in> l F (f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
   3.449 +proof (rule iffI[OF _ smallI])
   3.450 +  assume f: "f \<in> l F f"
   3.451 +  have "(1/2::real) > 0" "(2::real) > 0" by simp_all
   3.452 +  from smallD[OF f this(1)] smallD[OF f this(2)]
   3.453 +    show "eventually (\<lambda>x. f x = 0) F" by eventually_elim (insert R, auto)
   3.454 +next
   3.455 +  fix c :: real assume "c > 0" "eventually (\<lambda>x. f x = 0) F"
   3.456 +  from this(2) show "eventually (\<lambda>x. R (norm (f x)) (c * norm (f x))) F"
   3.457 +    by eventually_elim simp_all
   3.458 +qed
   3.459 +
   3.460 +lemma big_small_asymmetric: "f \<in> L F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
   3.461 +  by (drule (1) big_small_trans) (simp add: small_refl_iff)
   3.462 +
   3.463 +lemma small_big_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> L F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
   3.464 +  by (drule (1) small_big_trans) (simp add: small_refl_iff)
   3.465 +
   3.466 +lemma small_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
   3.467 +  by (drule (1) small_trans) (simp add: small_refl_iff)
   3.468 +
   3.469 +
   3.470 +lemma plus_aux:
   3.471 +  assumes "f \<in> o[F](g)"
   3.472 +  shows "g \<in> L F (\<lambda>x. f x + g x)"
   3.473 +proof (rule R_E)
   3.474 +  assume [simp]: "R = (\<le>)"
   3.475 +  have A: "1/2 > (0::real)" by simp
   3.476 +  {
   3.477 +    fix x assume "norm (f x) \<le> 1/2 * norm (g x)"
   3.478 +    hence "1/2 * (norm (g x)) \<le> (norm (g x)) - (norm (f x))" by simp
   3.479 +    also have "norm (g x) - norm (f x) \<le> norm (f x + g x)"
   3.480 +      by (subst add.commute) (rule norm_diff_ineq)
   3.481 +    finally have "1/2 * (norm (g x)) \<le> norm (f x + g x)" by simp
   3.482 +  } note B = this
   3.483 +  
   3.484 +  show "g \<in> L F (\<lambda>x. f x + g x)"
   3.485 +    apply (rule bigI[of "2"], simp)
   3.486 +    using landau_o.smallD[OF assms A] apply eventually_elim
   3.487 +    using B apply (simp add: algebra_simps) 
   3.488 +    done
   3.489 +next
   3.490 +  assume [simp]: "R = (\<lambda>x y. x \<ge> y)"
   3.491 +  show "g \<in> L F (\<lambda>x. f x + g x)"
   3.492 +  proof (rule bigI[of "1/2"])
   3.493 +    show "eventually (\<lambda>x. R (norm (g x)) (1/2 * norm (f x + g x))) F"
   3.494 +      using landau_o.smallD[OF assms zero_less_one]
   3.495 +    proof eventually_elim
   3.496 +      case (elim x)
   3.497 +      have "norm (f x + g x) \<le> norm (f x) + norm (g x)" by (rule norm_triangle_ineq)
   3.498 +      also note elim
   3.499 +      finally show ?case by simp
   3.500 +    qed
   3.501 +  qed simp_all
   3.502 +qed
   3.503 +
   3.504 +end
   3.505 +
   3.506 +
   3.507 +
   3.508 +lemma bigomega_iff_bigo: "g \<in> \<Omega>[F](f) \<longleftrightarrow> f \<in> O[F](g)"
   3.509 +proof
   3.510 +  assume "f \<in> O[F](g)"
   3.511 +  then guess c by (elim landau_o.bigE)
   3.512 +  thus "g \<in> \<Omega>[F](f)" by (intro landau_omega.bigI[of "inverse c"]) (simp_all add: field_simps)
   3.513 +next
   3.514 +  assume "g \<in> \<Omega>[F](f)"
   3.515 +  then guess c by (elim landau_omega.bigE)
   3.516 +  thus "f \<in> O[F](g)" by (intro landau_o.bigI[of "inverse c"]) (simp_all add: field_simps)
   3.517 +qed
   3.518 +
   3.519 +lemma smallomega_iff_smallo: "g \<in> \<omega>[F](f) \<longleftrightarrow> f \<in> o[F](g)"
   3.520 +proof
   3.521 +  assume "f \<in> o[F](g)"
   3.522 +  from landau_o.smallD[OF this, of "inverse c" for c]
   3.523 +    show "g \<in> \<omega>[F](f)" by (intro landau_omega.smallI) (simp_all add: field_simps)
   3.524 +next
   3.525 +  assume "g \<in> \<omega>[F](f)"
   3.526 +  from landau_omega.smallD[OF this, of "inverse c" for c]
   3.527 +    show "f \<in> o[F](g)" by (intro landau_o.smallI) (simp_all add: field_simps)
   3.528 +qed
   3.529 +
   3.530 +
   3.531 +context landau_pair
   3.532 +begin
   3.533 +
   3.534 +lemma big_mono:
   3.535 +  "eventually (\<lambda>x. R (norm (f x)) (norm (g x))) F \<Longrightarrow> f \<in> L F (g)"
   3.536 +  by (rule bigI[OF zero_less_one]) simp
   3.537 +
   3.538 +lemma big_mult:
   3.539 +  assumes "f1 \<in> L F (g1)" "f2 \<in> L F (g2)"
   3.540 +  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
   3.541 +proof-
   3.542 +  from assms(1) guess c1 by (elim bigE) note c1 = this
   3.543 +  from assms(2) guess c2 by (elim bigE) note c2 = this
   3.544 +  
   3.545 +  from c1(1) and c2(1) have "c1 * c2 > 0" by simp
   3.546 +  moreover have "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * c2 * norm (g1 x * g2 x))) F"
   3.547 +    using c1(2) c2(2)
   3.548 +  proof eventually_elim
   3.549 +    case (elim x)
   3.550 +    show ?case
   3.551 +    proof (cases rule: R_E)
   3.552 +      case le
   3.553 +      have "norm (f1 x) * norm (f2 x) \<le> (c1 * norm (g1 x)) * (c2 * norm (g2 x))"
   3.554 +        using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
   3.555 +      with le show ?thesis by (simp add: le norm_mult mult_ac)
   3.556 +    next
   3.557 +      case ge
   3.558 +      have "(c1 * norm (g1 x)) * (c2 * norm (g2 x)) \<le> norm (f1 x) * norm (f2 x)"
   3.559 +        using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
   3.560 +      with ge show ?thesis by (simp_all add: norm_mult mult_ac)
   3.561 +    qed
   3.562 +  qed
   3.563 +  ultimately show ?thesis by (rule bigI)
   3.564 +qed
   3.565 +
   3.566 +lemma small_big_mult:
   3.567 +  assumes "f1 \<in> l F (g1)" "f2 \<in> L F (g2)"
   3.568 +  shows   "(\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"
   3.569 +proof (rule smallI)
   3.570 +  fix c1 :: real assume c1: "c1 > 0"
   3.571 +  from assms(2) guess c2 by (elim bigE) note c2 = this
   3.572 +  with c1 assms(1) have "eventually (\<lambda>x. R (norm (f1 x)) (c1 * inverse c2 * norm (g1 x))) F"
   3.573 +    by (auto intro!: smallD)
   3.574 +  thus "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * norm (g1 x * g2 x))) F" using c2(2)
   3.575 +  proof eventually_elim
   3.576 +    case (elim x)
   3.577 +    show ?case
   3.578 +    proof (cases rule: R_E)
   3.579 +      case le
   3.580 +      have "norm (f1 x) * norm (f2 x) \<le> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
   3.581 +        using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
   3.582 +      with le c2(1) show ?thesis by (simp add: le norm_mult field_simps)
   3.583 +    next
   3.584 +      case ge
   3.585 +      have "norm (f1 x) * norm (f2 x) \<ge> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
   3.586 +        using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
   3.587 +      with ge c2(1) show ?thesis by (simp add: ge norm_mult field_simps)
   3.588 +    qed
   3.589 +  qed
   3.590 +qed
   3.591 +
   3.592 +lemma big_small_mult: 
   3.593 +  "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)"
   3.594 +  by (subst (1 2) mult.commute) (rule small_big_mult)
   3.595 +
   3.596 +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)"
   3.597 +  by (rule small_big_mult, assumption, rule small_imp_big)
   3.598 +
   3.599 +lemmas mult = big_mult small_big_mult big_small_mult small_mult
   3.600 +
   3.601 +
   3.602 +sublocale big: landau_symbol L L' Lr
   3.603 +proof
   3.604 +  have L: "L = bigo \<or> L = bigomega"
   3.605 +    by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
   3.606 +  {
   3.607 +    fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
   3.608 +    hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
   3.609 +  } note A = this
   3.610 +  {
   3.611 +    fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
   3.612 +    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
   3.613 +      show "L F (\<lambda>x. c * f x) = L F f" by (intro equalityI big_subsetI) (simp_all add: field_simps)
   3.614 +  }
   3.615 +  {
   3.616 +    fix c :: 'b and F and f g :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
   3.617 +    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
   3.618 +      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)
   3.619 +    thus "((\<lambda>x. c * f x) \<in> L F g) = (f \<in> L F g)" by (intro iffI) (erule (1) big_trans)+
   3.620 +  }
   3.621 +  {
   3.622 +    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> L F (g)"
   3.623 +    assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
   3.624 +    from A guess c by (elim bigE) note c = this
   3.625 +    from c(2) B have "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
   3.626 +      by eventually_elim (rule R_E, insert c(1), simp_all add: field_simps norm_inverse norm_divide)
   3.627 +    with c(1) show "(\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))" by (rule bigI)
   3.628 +  }
   3.629 +  {
   3.630 +    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
   3.631 +    with plus_aux show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" by (blast intro!: big_subsetI) 
   3.632 +  }
   3.633 +  {
   3.634 +    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   3.635 +    show "L F (f) = L F (g)" unfolding L_def
   3.636 +      
   3.637 +      thm eventually_subst A
   3.638 +      by (subst eventually_subst'[OF A]) (rule refl)
   3.639 +  }
   3.640 +  {
   3.641 +    fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   3.642 +    show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" unfolding L_def mem_Collect_eq
   3.643 +      by (subst (1) eventually_subst'[OF A]) (rule refl)
   3.644 +  }
   3.645 +  {
   3.646 +    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)
   3.647 +  }
   3.648 +  {
   3.649 +    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
   3.650 +    with A L show "L F (f) = L F (g)" unfolding bigtheta_def
   3.651 +      by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo)
   3.652 +    fix h:: "'a \<Rightarrow> 'b"
   3.653 +    show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" by (rule disjE[OF L]) 
   3.654 +      (insert A, auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans)
   3.655 +  }
   3.656 +  {
   3.657 +    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g"
   3.658 +    thus "(\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" by (intro big_mult) simp
   3.659 +  }
   3.660 +  {
   3.661 +    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" "g \<in> L F h"
   3.662 +    thus "f \<in> L F (h)" by (rule big_trans)
   3.663 +  }
   3.664 +  {
   3.665 +    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
   3.666 +    assume "f \<in> L F g" and "filterlim h F G"
   3.667 +    thus "(\<lambda>x. f (h x)) \<in> L' G (\<lambda>x. g (h x))" by (auto simp: L_def L'_def filterlim_iff)
   3.668 +  }
   3.669 +  {
   3.670 +    fix f g :: "'a \<Rightarrow> 'b" and F G :: "'a filter"
   3.671 +    assume "f \<in> L F g" "f \<in> L G g"
   3.672 +    from this [THEN bigE] guess c1 c2 . note c12 = this
   3.673 +    define c where "c = (if R c1 c2 then c2 else c1)"
   3.674 +    from c12 have c: "R c1 c" "R c2 c" "c > 0" by (auto simp: c_def dest: R_linear)
   3.675 +    with c12(2,4) have "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
   3.676 +                     "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) G"
   3.677 +      by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+
   3.678 +    with c show "f \<in> L (sup F G) g" by (auto simp: L_def eventually_sup)
   3.679 +  }
   3.680 +  {
   3.681 +    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
   3.682 +    assume "(f \<in> L F g)"
   3.683 +    thus "((\<lambda>x. f (h x)) \<in> L' (filtercomap h F) (\<lambda>x. g (h x)))"
   3.684 +      unfolding L_def L'_def by auto
   3.685 +  }
   3.686 +qed (auto simp: L_def Lr_def eventually_filtermap L'_def
   3.687 +          intro: filter_leD exI[of _ "1::real"])
   3.688 +
   3.689 +sublocale small: landau_symbol l l' lr
   3.690 +proof
   3.691 +  {
   3.692 +    fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   3.693 +    hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
   3.694 +  } note A = this
   3.695 +  {
   3.696 +    fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   3.697 +    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
   3.698 +      show "l F (\<lambda>x. c * f x) = l F f" 
   3.699 +        by (intro equalityI small_subsetI) (simp_all add: field_simps)
   3.700 +  }
   3.701 +  {
   3.702 +    fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   3.703 +    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
   3.704 +      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)
   3.705 +    thus "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" by (intro iffI) (erule (1) big_small_trans)+
   3.706 +  }
   3.707 +  {
   3.708 +    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
   3.709 +    with plus_aux show "l F g \<subseteq> l F (\<lambda>x. f x + g x)" by (blast intro!: small_subsetI) 
   3.710 +  }
   3.711 +  {
   3.712 +    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> l F (g)"
   3.713 +    assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
   3.714 +    show "(\<lambda>x. inverse (g x)) \<in> l F (\<lambda>x. inverse (f x))"
   3.715 +    proof (rule smallI)
   3.716 +      fix c :: real assume c: "c > 0"
   3.717 +      from B smallD[OF A c] 
   3.718 +        show "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
   3.719 +        by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide)
   3.720 +    qed
   3.721 +  }
   3.722 +  {
   3.723 +    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   3.724 +    show "l F (f) = l F (g)" unfolding l_def by (subst eventually_subst'[OF A]) (rule refl)
   3.725 +  }
   3.726 +  {
   3.727 +    fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   3.728 +    show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" unfolding l_def mem_Collect_eq
   3.729 +      by (subst (1) eventually_subst'[OF A]) (rule refl)
   3.730 +  }
   3.731 +  {
   3.732 +    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" 
   3.733 +    thus "l F f \<subseteq> l F g" by (intro small_subsetI small_imp_big)
   3.734 +  }
   3.735 +  {
   3.736 +    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
   3.737 +    have L: "L = bigo \<or> L = bigomega"
   3.738 +      by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
   3.739 +    with A show "l F (f) = l F (g)" unfolding bigtheta_def
   3.740 +      by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo)
   3.741 +    have l: "l = smallo \<or> l = smallomega"
   3.742 +      by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff)
   3.743 +    fix h:: "'a \<Rightarrow> 'b"
   3.744 +    show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" by (rule disjE[OF l]) 
   3.745 +      (insert A, auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo 
   3.746 +       intro: landau_o.big_small_trans landau_o.small_big_trans)
   3.747 +  }
   3.748 +  {
   3.749 +    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g"
   3.750 +    thus "(\<lambda>x. h x * f x) \<in> l F (\<lambda>x. h x * g x)" by (intro big_small_mult) simp
   3.751 +  }
   3.752 +  {
   3.753 +    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" "g \<in> l F h"
   3.754 +    thus "f \<in> l F (h)" by (rule small_trans)
   3.755 +  }
   3.756 +  {
   3.757 +    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
   3.758 +    assume "f \<in> l F g" and "filterlim h F G"
   3.759 +    thus "(\<lambda>x. f (h x)) \<in> l' G (\<lambda>x. g (h x))"
   3.760 +      by (auto simp: l_def l'_def filterlim_iff)
   3.761 +  }
   3.762 +  {
   3.763 +    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
   3.764 +    assume "(f \<in> l F g)"
   3.765 +    thus "((\<lambda>x. f (h x)) \<in> l' (filtercomap h F) (\<lambda>x. g (h x)))"
   3.766 +      unfolding l_def l'_def by auto
   3.767 +  }
   3.768 +qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)
   3.769 +
   3.770 +
   3.771 +text {* These rules allow chaining of Landau symbol propositions in Isar with "also".*}
   3.772 +
   3.773 +lemma big_mult_1:    "f \<in> L F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
   3.774 +  and big_mult_1':   "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
   3.775 +  and small_mult_1:  "f \<in> l F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
   3.776 +  and small_mult_1': "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> l F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
   3.777 +  and small_mult_1'':  "f \<in> L F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> l F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
   3.778 +  and small_mult_1''': "(\<lambda>_. 1) \<in> l F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
   3.779 +  by (drule (1) big.mult big_small_mult small_big_mult, simp)+
   3.780 +
   3.781 +lemma big_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)"
   3.782 +  and big_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)"
   3.783 +  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)"
   3.784 +  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)"
   3.785 +  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)"
   3.786 +  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)"
   3.787 +  by (drule (1) big.mult big_small_mult small_big_mult, simp)+
   3.788 +
   3.789 +lemmas mult_1_trans = 
   3.790 +  big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1'''
   3.791 +  big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult'''
   3.792 +
   3.793 +lemma big_equal_iff_bigtheta: "L F (f) = L F (g) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
   3.794 +proof
   3.795 +  have L: "L = bigo \<or> L = bigomega"
   3.796 +    by (rule R_E) (auto simp: fun_eq_iff L_def bigo_def bigomega_def)
   3.797 +  fix f g :: "'a \<Rightarrow> 'b" assume "L F (f) = L F (g)"
   3.798 +  with big_refl[of f F] big_refl[of g F] have "f \<in> L F (g)" "g \<in> L F (f)" by simp_all
   3.799 +  thus "f \<in> \<Theta>[F](g)" using L unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
   3.800 +qed (rule big.cong_bigtheta)
   3.801 +
   3.802 +lemma big_prod:
   3.803 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (g x)"
   3.804 +  shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>y. \<Prod>x\<in>A. g x y)"
   3.805 +  using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult)
   3.806 +
   3.807 +lemma big_prod_in_1:
   3.808 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (\<lambda>_. 1)"
   3.809 +  shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>_. 1)"
   3.810 +  using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult_in_1)
   3.811 +
   3.812 +end
   3.813 +
   3.814 +
   3.815 +context landau_symbol
   3.816 +begin
   3.817 +  
   3.818 +lemma plus_absorb1:
   3.819 +  assumes "f \<in> o[F](g)"
   3.820 +  shows   "L F (\<lambda>x. f x + g x) = L F (g)"
   3.821 +proof (intro equalityI)
   3.822 +  from plus_subset1 and assms show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" .
   3.823 +  from landau_o.small.plus_subset1[OF assms] and assms have "(\<lambda>x. -f x) \<in> o[F](\<lambda>x. f x + g x)"
   3.824 +    by (auto simp: landau_o.small.uminus_in_iff)
   3.825 +  from plus_subset1[OF this] show "L F (\<lambda>x. f x + g x) \<subseteq> L F (g)" by simp
   3.826 +qed
   3.827 +
   3.828 +lemma plus_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x + g x) = L F (f)"
   3.829 +  using plus_absorb1[of g F f] by (simp add: add.commute)
   3.830 +
   3.831 +lemma diff_absorb1: "f \<in> o[F](g) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (g)"
   3.832 +  by (simp only: diff_conv_add_uminus plus_absorb1 landau_o.small.uminus uminus)
   3.833 +
   3.834 +lemma diff_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (f)"
   3.835 +  by (simp only: diff_conv_add_uminus plus_absorb2 landau_o.small.uminus_in_iff)
   3.836 +
   3.837 +lemmas absorb = plus_absorb1 plus_absorb2 diff_absorb1 diff_absorb2
   3.838 +
   3.839 +end
   3.840 +
   3.841 +
   3.842 +lemma bigthetaI [intro]: "f \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> \<Theta>[F](g)"
   3.843 +  unfolding bigtheta_def bigomega_def by blast
   3.844 +
   3.845 +lemma bigthetaD1 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> O[F](g)" 
   3.846 +  and bigthetaD2 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g)"
   3.847 +  unfolding bigtheta_def bigo_def bigomega_def by blast+
   3.848 +
   3.849 +lemma bigtheta_refl [simp]: "f \<in> \<Theta>[F](f)"
   3.850 +  unfolding bigtheta_def by simp
   3.851 +
   3.852 +lemma bigtheta_sym: "f \<in> \<Theta>[F](g) \<longleftrightarrow> g \<in> \<Theta>[F](f)"
   3.853 +  unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
   3.854 +
   3.855 +lemmas landau_flip =
   3.856 +  bigomega_iff_bigo[symmetric] smallomega_iff_smallo[symmetric]
   3.857 +  bigomega_iff_bigo smallomega_iff_smallo bigtheta_sym
   3.858 +
   3.859 +
   3.860 +interpretation landau_theta: landau_symbol bigtheta bigtheta bigtheta
   3.861 +proof
   3.862 +  fix f g :: "'a \<Rightarrow> 'b" and F
   3.863 +  assume "f \<in> o[F](g)"
   3.864 +  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)"
   3.865 +    by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+
   3.866 +  thus "\<Theta>[F](g) \<subseteq> \<Theta>[F](\<lambda>x. f x + g x)" unfolding bigtheta_def by blast
   3.867 +next
   3.868 +  fix f g :: "'a \<Rightarrow> 'b" and F 
   3.869 +  assume "f \<in> \<Theta>[F](g)"
   3.870 +  thus A: "\<Theta>[F](f) = \<Theta>[F](g)" 
   3.871 +    apply (subst (1 2) bigtheta_def)
   3.872 +    apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+
   3.873 +    apply (rule refl)
   3.874 +    done
   3.875 +  thus "\<Theta>[F](f) \<subseteq> \<Theta>[F](g)" by simp
   3.876 +  fix h :: "'a \<Rightarrow> 'b"
   3.877 +  show "f \<in> \<Theta>[F](h) \<longleftrightarrow> g \<in> \<Theta>[F](h)" by (subst (1 2) bigtheta_sym) (simp add: A)
   3.878 +next
   3.879 +  fix f g h :: "'a \<Rightarrow> 'b" and F
   3.880 +  assume "f \<in> \<Theta>[F](g)" "g \<in> \<Theta>[F](h)"
   3.881 +  thus "f \<in> \<Theta>[F](h)" unfolding bigtheta_def
   3.882 +    by (blast intro: landau_o.big.trans landau_omega.big.trans)
   3.883 +next
   3.884 +  fix f :: "'a \<Rightarrow> 'b" and F1 F2 :: "'a filter"
   3.885 +  assume "F1 \<le> F2"
   3.886 +  thus "\<Theta>[F2](f) \<subseteq> \<Theta>[F1](f)"
   3.887 +    by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono)
   3.888 +qed (auto simp: bigtheta_def landau_o.big.norm_iff 
   3.889 +                landau_o.big.cmult landau_omega.big.cmult 
   3.890 +                landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff 
   3.891 +                landau_o.big.in_cong landau_omega.big.in_cong
   3.892 +                landau_o.big.mult landau_omega.big.mult
   3.893 +                landau_o.big.inverse landau_omega.big.inverse 
   3.894 +                landau_o.big.compose landau_omega.big.compose
   3.895 +                landau_o.big.bot' landau_omega.big.bot'
   3.896 +                landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff
   3.897 +                landau_o.big.sup landau_omega.big.sup
   3.898 +                landau_o.big.filtercomap landau_omega.big.filtercomap
   3.899 +          dest: landau_o.big.cong landau_omega.big.cong)
   3.900 +
   3.901 +lemmas landau_symbols = 
   3.902 +  landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms
   3.903 +  landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms 
   3.904 +  landau_theta.landau_symbol_axioms
   3.905 +
   3.906 +lemma bigoI [intro]:
   3.907 +  assumes "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
   3.908 +  shows   "f \<in> O[F](g)"
   3.909 +proof (rule landau_o.bigI)
   3.910 +  show "max 1 c > 0" by simp
   3.911 +  note assms
   3.912 +  moreover have "\<And>x. c * (norm (g x)) \<le> max 1 c * (norm (g x))" by (simp add: mult_right_mono)
   3.913 +  ultimately show "eventually (\<lambda>x. (norm (f x)) \<le> max 1 c * (norm (g x))) F"
   3.914 +    by (auto elim!: eventually_mono dest: order.trans)
   3.915 +qed
   3.916 +
   3.917 +lemma smallomegaD [dest]:
   3.918 +  assumes "f \<in> \<omega>[F](g)"
   3.919 +  shows   "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
   3.920 +proof (cases "c > 0")
   3.921 +  case False
   3.922 +  show ?thesis 
   3.923 +    by (intro always_eventually allI, rule order.trans[of _ 0])
   3.924 +       (insert False, auto intro!: mult_nonpos_nonneg)
   3.925 +qed (blast dest: landau_omega.smallD[OF assms, of c])
   3.926 +
   3.927 +  
   3.928 +lemma bigthetaI':
   3.929 +  assumes "c1 > 0" "c2 > 0"
   3.930 +  assumes "eventually (\<lambda>x. c1 * (norm (g x)) \<le> (norm (f x)) \<and> (norm (f x)) \<le> c2 * (norm (g x))) F"
   3.931 +  shows   "f \<in> \<Theta>[F](g)"
   3.932 +apply (rule bigthetaI)
   3.933 +apply (rule landau_o.bigI[OF assms(2)]) using assms(3) apply (eventually_elim, simp)
   3.934 +apply (rule landau_omega.bigI[OF assms(1)]) using assms(3) apply (eventually_elim, simp)
   3.935 +done
   3.936 +
   3.937 +lemma bigthetaI_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> \<Theta>[F](g)"
   3.938 +  by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono)
   3.939 +
   3.940 +lemma (in landau_symbol) ev_eq_trans1: 
   3.941 +  "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))"
   3.942 +  by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono)
   3.943 +
   3.944 +lemma (in landau_symbol) ev_eq_trans2: 
   3.945 +  "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)"
   3.946 +  by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono)
   3.947 +
   3.948 +declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro]
   3.949 +declare landau_o.bigE landau_omega.bigE [elim]
   3.950 +declare landau_o.smallD
   3.951 +
   3.952 +lemma (in landau_symbol) bigtheta_trans1': 
   3.953 +  "f \<in> L F (g) \<Longrightarrow> h \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h)"
   3.954 +  by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym)
   3.955 +
   3.956 +lemma (in landau_symbol) bigtheta_trans2': 
   3.957 +  "g \<in> \<Theta>[F](f) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
   3.958 +  by (rule bigtheta_trans2, subst bigtheta_sym)
   3.959 +
   3.960 +lemma bigo_bigomega_trans:      "f \<in> O[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> O[F](h)"
   3.961 +  and bigo_smallomega_trans:    "f \<in> O[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
   3.962 +  and smallo_bigomega_trans:    "f \<in> o[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
   3.963 +  and smallo_smallomega_trans:  "f \<in> o[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
   3.964 +  and bigomega_bigo_trans:      "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](h)"
   3.965 +  and bigomega_smallo_trans:    "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
   3.966 +  and smallomega_bigo_trans:    "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
   3.967 +  and smallomega_smallo_trans:  "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
   3.968 +  by (unfold bigomega_iff_bigo smallomega_iff_smallo)
   3.969 +     (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans 
   3.970 +                landau_o.big_trans landau_o.small_trans)+
   3.971 +
   3.972 +lemmas landau_trans_lift [trans] =
   3.973 +  landau_symbols[THEN landau_symbol.lift_trans]
   3.974 +  landau_symbols[THEN landau_symbol.lift_trans']
   3.975 +  landau_symbols[THEN landau_symbol.lift_trans_bigtheta]
   3.976 +  landau_symbols[THEN landau_symbol.lift_trans_bigtheta']
   3.977 +
   3.978 +lemmas landau_mult_1_trans [trans] =
   3.979 +  landau_o.mult_1_trans landau_omega.mult_1_trans
   3.980 +
   3.981 +lemmas landau_trans [trans] = 
   3.982 +  landau_symbols[THEN landau_symbol.bigtheta_trans1]
   3.983 +  landau_symbols[THEN landau_symbol.bigtheta_trans2]
   3.984 +  landau_symbols[THEN landau_symbol.bigtheta_trans1']
   3.985 +  landau_symbols[THEN landau_symbol.bigtheta_trans2']
   3.986 +  landau_symbols[THEN landau_symbol.ev_eq_trans1]
   3.987 +  landau_symbols[THEN landau_symbol.ev_eq_trans2]
   3.988 +
   3.989 +  landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans
   3.990 +  landau_omega.big_trans landau_omega.small_trans 
   3.991 +    landau_omega.small_big_trans landau_omega.big_small_trans
   3.992 +
   3.993 +  bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans 
   3.994 +  bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans
   3.995 +
   3.996 +lemma bigtheta_inverse [simp]: 
   3.997 +  shows "(\<lambda>x. inverse (f x)) \<in> \<Theta>[F](\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
   3.998 +proof-
   3.999 +  {
  3.1000 +    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
  3.1001 +    then guess c1 c2 :: real unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
  3.1002 +    note c = this
  3.1003 +    from c(3) have "inverse c2 > 0" by simp
  3.1004 +    moreover from c(2,4)
  3.1005 +      have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))) F"
  3.1006 +    proof eventually_elim
  3.1007 +      fix x assume A: "(norm (f x)) \<le> c1 * (norm (g x))" "c2 * (norm (g x)) \<le> (norm (f x))"
  3.1008 +      from A c(1,3) have "f x = 0 \<longleftrightarrow> g x = 0" by (auto simp: field_simps mult_le_0_iff)
  3.1009 +      with A c(1,3) show "norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))"
  3.1010 +        by (force simp: field_simps norm_inverse norm_divide)
  3.1011 +    qed
  3.1012 +    ultimately have "(\<lambda>x. inverse (f x)) \<in> O[F](\<lambda>x. inverse (g x))" by (rule landau_o.bigI)
  3.1013 +  }
  3.1014 +  thus ?thesis unfolding bigtheta_def 
  3.1015 +    by (force simp: bigomega_iff_bigo bigtheta_sym)
  3.1016 +qed
  3.1017 +
  3.1018 +lemma bigtheta_divide:
  3.1019 +  assumes "f1 \<in> \<Theta>(f2)" "g1 \<in> \<Theta>(g2)"
  3.1020 +  shows   "(\<lambda>x. f1 x / g1 x) \<in> \<Theta>(\<lambda>x. f2 x / g2 x)"
  3.1021 +  by (subst (1 2) divide_inverse, intro landau_theta.mult) (simp_all add: bigtheta_inverse assms)
  3.1022 +
  3.1023 +lemma eventually_nonzero_bigtheta:
  3.1024 +  assumes "f \<in> \<Theta>[F](g)"
  3.1025 +  shows   "eventually (\<lambda>x. f x \<noteq> 0) F \<longleftrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F"
  3.1026 +proof-
  3.1027 +  {
  3.1028 +    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"
  3.1029 +    from A guess c1 c2 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
  3.1030 +    from B this(2,4) have "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim auto
  3.1031 +  }
  3.1032 +  with assms show ?thesis by (force simp: bigtheta_sym)
  3.1033 +qed
  3.1034 +
  3.1035 +
  3.1036 +subsection {* Landau symbols and limits *}
  3.1037 +
  3.1038 +lemma bigoI_tendsto_norm:
  3.1039 +  fixes f g
  3.1040 +  assumes "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
  3.1041 +  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  3.1042 +  shows   "f \<in> O[F](g)"
  3.1043 +proof (rule bigoI)
  3.1044 +  from assms have "eventually (\<lambda>x. dist (norm (f x / g x)) c < 1) F" 
  3.1045 +    using tendstoD by force
  3.1046 +  thus "eventually (\<lambda>x. (norm (f x)) \<le> (norm c + 1) * (norm (g x))) F"
  3.1047 +    unfolding dist_real_def using assms(2)
  3.1048 +  proof eventually_elim
  3.1049 +    case (elim x)
  3.1050 +    have "(norm (f x)) - norm c * (norm (g x)) \<le> norm ((norm (f x)) - c * (norm (g x)))"
  3.1051 +      unfolding norm_mult [symmetric] using norm_triangle_ineq2[of "norm (f x)" "c * norm (g x)"]
  3.1052 +      by (simp add: norm_mult abs_mult)
  3.1053 +    also from elim have "\<dots> = norm (norm (g x)) * norm (norm (f x / g x) - c)"
  3.1054 +      unfolding norm_mult [symmetric] by (simp add: algebra_simps norm_divide)
  3.1055 +    also from elim have "norm (norm (f x / g x) - c) \<le> 1" by simp
  3.1056 +    hence "norm (norm (g x)) * norm (norm (f x / g x) - c) \<le> norm (norm (g x)) * 1" 
  3.1057 +      by (rule mult_left_mono) simp_all
  3.1058 +    finally show ?case by (simp add: algebra_simps)
  3.1059 +  qed
  3.1060 +qed
  3.1061 +
  3.1062 +lemma bigoI_tendsto:
  3.1063 +  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
  3.1064 +  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  3.1065 +  shows   "f \<in> O[F](g)"
  3.1066 +  using assms by (rule bigoI_tendsto_norm[OF tendsto_norm])
  3.1067 +
  3.1068 +lemma bigomegaI_tendsto_norm:
  3.1069 +  assumes c_not_0:  "(c::real) \<noteq> 0"
  3.1070 +  assumes lim:      "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
  3.1071 +  shows   "f \<in> \<Omega>[F](g)"
  3.1072 +proof (cases "F = bot")
  3.1073 +  case False
  3.1074 +  show ?thesis
  3.1075 +  proof (rule landau_omega.bigI)
  3.1076 +    from lim  have "c \<ge> 0" by (rule tendsto_lowerbound) (insert False, simp_all)
  3.1077 +    with c_not_0 have "c > 0" by simp
  3.1078 +    with c_not_0 show "c/2 > 0" by simp
  3.1079 +    from lim have ev: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<epsilon>) F"
  3.1080 +      by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  3.1081 +    from ev[OF `c/2 > 0`] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
  3.1082 +    proof (eventually_elim)
  3.1083 +      fix x assume B: "norm (norm (f x / g x) - c) < c / 2"
  3.1084 +      from B have g: "g x \<noteq> 0" by auto
  3.1085 +      from B have "-c/2 < -norm (norm (f x / g x) - c)" by simp
  3.1086 +      also have "... \<le> norm (f x / g x) - c" by simp
  3.1087 +      finally show "(norm (f x)) \<ge> c/2 * (norm (g x))" using g 
  3.1088 +        by (simp add: field_simps norm_mult norm_divide)
  3.1089 +    qed
  3.1090 +  qed
  3.1091 +qed simp
  3.1092 +
  3.1093 +lemma bigomegaI_tendsto:
  3.1094 +  assumes c_not_0:  "(c::real) \<noteq> 0"
  3.1095 +  assumes lim:      "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
  3.1096 +  shows   "f \<in> \<Omega>[F](g)"
  3.1097 +  by (rule bigomegaI_tendsto_norm[OF _ tendsto_norm, of c]) (insert assms, simp_all)
  3.1098 +
  3.1099 +lemma smallomegaI_filterlim_at_top_norm:
  3.1100 +  assumes lim: "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
  3.1101 +  shows   "f \<in> \<omega>[F](g)"
  3.1102 +proof (rule landau_omega.smallI)
  3.1103 +  fix c :: real assume c_pos: "c > 0"
  3.1104 +  from lim have ev: "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F"
  3.1105 +    by (subst (asm) filterlim_at_top) simp
  3.1106 +  thus "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
  3.1107 +  proof eventually_elim
  3.1108 +    fix x assume A: "norm (f x / g x) \<ge> c"
  3.1109 +    from A c_pos have "g x \<noteq> 0" by auto
  3.1110 +    with A show "(norm (f x)) \<ge> c * (norm (g x))" by (simp add: field_simps norm_divide)
  3.1111 +  qed
  3.1112 +qed
  3.1113 +
  3.1114 +lemma smallomegaI_filterlim_at_infinity:
  3.1115 +  assumes lim: "filterlim (\<lambda>x. f x / g x) at_infinity F"
  3.1116 +  shows   "f \<in> \<omega>[F](g)"
  3.1117 +proof (rule smallomegaI_filterlim_at_top_norm)
  3.1118 +  from lim show "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
  3.1119 +    by (rule filterlim_at_infinity_imp_norm_at_top)
  3.1120 +qed
  3.1121 +  
  3.1122 +lemma smallomegaD_filterlim_at_top_norm:
  3.1123 +  assumes "f \<in> \<omega>[F](g)"
  3.1124 +  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  3.1125 +  shows   "LIM x F. norm (f x / g x) :> at_top"
  3.1126 +proof (subst filterlim_at_top_gt, clarify)
  3.1127 +  fix c :: real assume c: "c > 0"
  3.1128 +  from landau_omega.smallD[OF assms(1) this] assms(2) 
  3.1129 +    show "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F" 
  3.1130 +    by eventually_elim (simp add: field_simps norm_divide)
  3.1131 +qed
  3.1132 +  
  3.1133 +lemma smallomegaD_filterlim_at_infinity:
  3.1134 +  assumes "f \<in> \<omega>[F](g)"
  3.1135 +  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  3.1136 +  shows   "LIM x F. f x / g x :> at_infinity"
  3.1137 +  using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm)
  3.1138 +
  3.1139 +lemma smallomega_1_conv_filterlim: "f \<in> \<omega>[F](\<lambda>_. 1) \<longleftrightarrow> filterlim f at_infinity F"
  3.1140 +  by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)
  3.1141 +
  3.1142 +lemma smalloI_tendsto:
  3.1143 +  assumes lim: "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
  3.1144 +  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  3.1145 +  shows   "f \<in> o[F](g)"
  3.1146 +proof (rule landau_o.smallI)
  3.1147 +  fix c :: real assume c_pos: "c > 0"
  3.1148 +  from c_pos and lim have ev: "eventually (\<lambda>x. norm (f x / g x) < c) F"
  3.1149 +    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  3.1150 +  with assms(2) show "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
  3.1151 +    by eventually_elim (simp add: field_simps norm_divide)
  3.1152 +qed
  3.1153 +
  3.1154 +lemma smalloD_tendsto:
  3.1155 +  assumes "f \<in> o[F](g)"
  3.1156 +  shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
  3.1157 +unfolding tendsto_iff
  3.1158 +proof clarify
  3.1159 +  fix e :: real assume e: "e > 0"
  3.1160 +  hence "e/2 > 0" by simp
  3.1161 +  from landau_o.smallD[OF assms this] show "eventually (\<lambda>x. dist (f x / g x) 0 < e) F"
  3.1162 +  proof eventually_elim
  3.1163 +    fix x assume "(norm (f x)) \<le> e/2 * (norm (g x))"
  3.1164 +    with e have "dist (f x / g x) 0 \<le> e/2"
  3.1165 +      by (cases "g x = 0") (simp_all add: dist_real_def norm_divide field_simps)
  3.1166 +    also from e have "... < e" by simp
  3.1167 +    finally show "dist (f x / g x) 0 < e" by simp
  3.1168 +  qed
  3.1169 +qed
  3.1170 +
  3.1171 +lemma bigthetaI_tendsto_norm:
  3.1172 +  assumes c_not_0: "(c::real) \<noteq> 0"
  3.1173 +  assumes lim:     "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
  3.1174 +  shows   "f \<in> \<Theta>[F](g)"
  3.1175 +proof (rule bigthetaI)
  3.1176 +  from c_not_0 have "\<bar>c\<bar> > 0" by simp
  3.1177 +  with lim have "eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<bar>c\<bar>) F"
  3.1178 +    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  3.1179 +  hence g: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim (auto simp add: field_simps)
  3.1180 +
  3.1181 +  from lim g show "f \<in> O[F](g)" by (rule bigoI_tendsto_norm)
  3.1182 +  from c_not_0 and lim show "f \<in> \<Omega>[F](g)" by (rule bigomegaI_tendsto_norm)
  3.1183 +qed
  3.1184 +
  3.1185 +lemma bigthetaI_tendsto:
  3.1186 +  assumes c_not_0: "(c::real) \<noteq> 0"
  3.1187 +  assumes lim:     "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
  3.1188 +  shows   "f \<in> \<Theta>[F](g)"
  3.1189 +  using assms by (intro bigthetaI_tendsto_norm[OF _ tendsto_norm, of "c"]) simp_all
  3.1190 +
  3.1191 +lemma tendsto_add_smallo:
  3.1192 +  assumes "(f1 \<longlongrightarrow> a) F"
  3.1193 +  assumes "f2 \<in> o[F](f1)"
  3.1194 +  shows   "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
  3.1195 +proof (subst filterlim_cong[OF refl refl])
  3.1196 +  from landau_o.smallD[OF assms(2) zero_less_one] 
  3.1197 +    have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)) F" by simp
  3.1198 +  thus "eventually (\<lambda>x. f1 x + f2 x = f1 x * (1 + f2 x / f1 x)) F"
  3.1199 +    by eventually_elim (auto simp: field_simps)
  3.1200 +next
  3.1201 +  from assms(1) show "((\<lambda>x. f1 x * (1 + f2 x / f1 x)) \<longlongrightarrow> a) F"
  3.1202 +    by (force intro: tendsto_eq_intros smalloD_tendsto[OF assms(2)])
  3.1203 +qed
  3.1204 +
  3.1205 +lemma tendsto_diff_smallo:
  3.1206 +  shows "(f1 \<longlongrightarrow> a) F \<Longrightarrow> f2 \<in> o[F](f1) \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
  3.1207 +  using tendsto_add_smallo[of f1 a F "\<lambda>x. -f2 x"] by simp
  3.1208 +
  3.1209 +lemma tendsto_add_smallo_iff:
  3.1210 +  assumes "f2 \<in> o[F](f1)"
  3.1211 +  shows   "(f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
  3.1212 +proof
  3.1213 +  assume "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
  3.1214 +  hence "((\<lambda>x. f1 x + f2 x - f2 x) \<longlongrightarrow> a) F"
  3.1215 +    by (rule tendsto_diff_smallo) (simp add: landau_o.small.plus_absorb2 assms)
  3.1216 +  thus "(f1 \<longlongrightarrow> a) F" by simp
  3.1217 +qed (rule tendsto_add_smallo[OF _ assms])
  3.1218 +
  3.1219 +lemma tendsto_diff_smallo_iff:
  3.1220 +  shows "f2 \<in> o[F](f1) \<Longrightarrow> (f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
  3.1221 +  using tendsto_add_smallo_iff[of "\<lambda>x. -f2 x" F f1 a] by simp
  3.1222 +
  3.1223 +lemma tendsto_divide_smallo:
  3.1224 +  assumes "((\<lambda>x. f1 x / g1 x) \<longlongrightarrow> a) F"
  3.1225 +  assumes "f2 \<in> o[F](f1)" "g2 \<in> o[F](g1)"
  3.1226 +  assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
  3.1227 +  shows   "((\<lambda>x. (f1 x + f2 x) / (g1 x + g2 x)) \<longlongrightarrow> a) F" (is "(?f \<longlongrightarrow> _) _")
  3.1228 +proof (subst tendsto_cong)
  3.1229 +  let ?f' = "\<lambda>x. (f1 x / g1 x) * (1 + f2 x / f1 x) / (1 + g2 x / g1 x)"
  3.1230 +
  3.1231 +  have "(?f' \<longlongrightarrow> a * (1 + 0) / (1 + 0)) F"
  3.1232 +  by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const 
  3.1233 +        smalloD_tendsto[OF assms(2)] smalloD_tendsto[OF assms(3)])+ simp_all
  3.1234 +  thus "(?f' \<longlongrightarrow> a) F" by simp
  3.1235 +
  3.1236 +  have "(1/2::real) > 0" by simp
  3.1237 +  from landau_o.smallD[OF assms(2) this] landau_o.smallD[OF assms(3) this]
  3.1238 +    have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)/2) F"
  3.1239 +         "eventually (\<lambda>x. norm (g2 x) \<le> norm (g1 x)/2) F" by simp_all
  3.1240 +  with assms(4) show "eventually (\<lambda>x. ?f x = ?f' x) F"
  3.1241 +  proof eventually_elim
  3.1242 +    fix x assume A: "norm (f2 x) \<le> norm (f1 x)/2" and 
  3.1243 +                 B: "norm (g2 x) \<le> norm (g1 x)/2" and C: "g1 x \<noteq> 0"
  3.1244 +    show "?f x = ?f' x"
  3.1245 +    proof (cases "f1 x = 0")
  3.1246 +      assume D: "f1 x \<noteq> 0"
  3.1247 +      from D have "f1 x + f2 x = f1 x * (1 + f2 x/f1 x)" by (simp add: field_simps)
  3.1248 +      moreover from C have "g1 x + g2 x = g1 x * (1 + g2 x/g1 x)" by (simp add: field_simps)
  3.1249 +      ultimately have "?f x = (f1 x * (1 + f2 x/f1 x)) / (g1 x * (1 + g2 x/g1 x))" by (simp only:)
  3.1250 +      also have "... = ?f' x" by simp
  3.1251 +      finally show ?thesis .
  3.1252 +    qed (insert A, simp)
  3.1253 +  qed
  3.1254 +qed
  3.1255 +
  3.1256 +
  3.1257 +lemma bigo_powr:
  3.1258 +  fixes f :: "'a \<Rightarrow> real"
  3.1259 +  assumes "f \<in> O[F](g)" "p \<ge> 0"
  3.1260 +  shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)"
  3.1261 +proof-
  3.1262 +  from assms(1) guess c by (elim landau_o.bigE landau_omega.bigE IntE)
  3.1263 +  note c = this
  3.1264 +  from c(2) assms(2) have "eventually (\<lambda>x. (norm (f x)) powr p \<le> (c * (norm (g x))) powr p) F"
  3.1265 +    by (auto elim!: eventually_mono intro!: powr_mono2)
  3.1266 +  thus "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" using c(1)
  3.1267 +    by (intro bigoI[of _ "c powr p"]) (simp_all add: powr_mult)
  3.1268 +qed
  3.1269 +
  3.1270 +lemma smallo_powr:
  3.1271 +  fixes f :: "'a \<Rightarrow> real"
  3.1272 +  assumes "f \<in> o[F](g)" "p > 0"
  3.1273 +  shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)"
  3.1274 +proof (rule landau_o.smallI)
  3.1275 +  fix c :: real assume c: "c > 0"
  3.1276 +  hence "c powr (1/p) > 0" by simp
  3.1277 +  from landau_o.smallD[OF assms(1) this] 
  3.1278 +  show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F"
  3.1279 +  proof eventually_elim
  3.1280 +    fix x assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))"
  3.1281 +    with assms(2) have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p"
  3.1282 +      by (intro powr_mono2) simp_all
  3.1283 +    also from assms(2) c have "... = c * (norm (g x)) powr p"
  3.1284 +      by (simp add: field_simps powr_mult powr_powr)
  3.1285 +    finally show "norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)" by simp
  3.1286 +  qed
  3.1287 +qed
  3.1288 +
  3.1289 +lemma smallo_powr_nonneg:
  3.1290 +  fixes f :: "'a \<Rightarrow> real"
  3.1291 +  assumes "f \<in> o[F](g)" "p > 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
  3.1292 +  shows   "(\<lambda>x. f x powr p) \<in> o[F](\<lambda>x. g x powr p)"
  3.1293 +proof -
  3.1294 +  from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
  3.1295 +    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  3.1296 +  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+
  3.1297 +  also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
  3.1298 +    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  3.1299 +  finally show ?thesis .
  3.1300 +qed
  3.1301 +
  3.1302 +lemma bigtheta_powr:
  3.1303 +  fixes f :: "'a \<Rightarrow> real"
  3.1304 +  shows "f \<in> \<Theta>[F](g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>g x\<bar> powr p)"
  3.1305 +apply (cases "p < 0")
  3.1306 +apply (subst bigtheta_inverse[symmetric], subst (1 2) powr_minus[symmetric])
  3.1307 +unfolding bigtheta_def apply (auto simp: bigomega_iff_bigo intro!: bigo_powr)
  3.1308 +done
  3.1309 +
  3.1310 +lemma bigo_powr_nonneg:
  3.1311 +  fixes f :: "'a \<Rightarrow> real"
  3.1312 +  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"
  3.1313 +  shows   "(\<lambda>x. f x powr p) \<in> O[F](\<lambda>x. g x powr p)"
  3.1314 +proof -
  3.1315 +  from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
  3.1316 +    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  3.1317 +  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+
  3.1318 +  also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
  3.1319 +    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  3.1320 +  finally show ?thesis .
  3.1321 +qed
  3.1322 +
  3.1323 +lemma zero_in_smallo [simp]: "(\<lambda>_. 0) \<in> o[F](f)"
  3.1324 +  by (intro landau_o.smallI) simp_all
  3.1325 +
  3.1326 +lemma zero_in_bigo [simp]: "(\<lambda>_. 0) \<in> O[F](f)"
  3.1327 +  by (intro landau_o.bigI[of 1]) simp_all
  3.1328 +
  3.1329 +lemma in_bigomega_zero [simp]: "f \<in> \<Omega>[F](\<lambda>x. 0)"
  3.1330 +  by (rule landau_omega.bigI[of 1]) simp_all
  3.1331 +
  3.1332 +lemma in_smallomega_zero [simp]: "f \<in> \<omega>[F](\<lambda>x. 0)"
  3.1333 +  by (simp add: smallomega_iff_smallo)
  3.1334 +
  3.1335 +
  3.1336 +lemma in_smallo_zero_iff [simp]: "f \<in> o[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  3.1337 +proof
  3.1338 +  assume "f \<in> o[F](\<lambda>_. 0)"
  3.1339 +  from landau_o.smallD[OF this, of 1] show "eventually (\<lambda>x. f x = 0) F" by simp
  3.1340 +next
  3.1341 +  assume "eventually (\<lambda>x. f x = 0) F"
  3.1342 +  hence "\<forall>c>0. eventually (\<lambda>x. (norm (f x)) \<le> c * \<bar>0\<bar>) F" by simp
  3.1343 +  thus "f \<in> o[F](\<lambda>_. 0)" unfolding smallo_def by simp
  3.1344 +qed
  3.1345 +
  3.1346 +lemma in_bigo_zero_iff [simp]: "f \<in> O[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  3.1347 +proof
  3.1348 +  assume "f \<in> O[F](\<lambda>_. 0)"
  3.1349 +  thus "eventually (\<lambda>x. f x = 0) F" by (elim landau_o.bigE) simp
  3.1350 +next
  3.1351 +  assume "eventually (\<lambda>x. f x = 0) F"
  3.1352 +  hence "eventually (\<lambda>x. (norm (f x)) \<le> 1 * \<bar>0\<bar>) F" by simp
  3.1353 +  thus "f \<in> O[F](\<lambda>_. 0)" by (intro landau_o.bigI[of 1]) simp_all
  3.1354 +qed
  3.1355 +
  3.1356 +lemma zero_in_smallomega_iff [simp]: "(\<lambda>_. 0) \<in> \<omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  3.1357 +  by (simp add: smallomega_iff_smallo)
  3.1358 +
  3.1359 +lemma zero_in_bigomega_iff [simp]: "(\<lambda>_. 0) \<in> \<Omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  3.1360 +  by (simp add: bigomega_iff_bigo)
  3.1361 +
  3.1362 +lemma zero_in_bigtheta_iff [simp]: "(\<lambda>_. 0) \<in> \<Theta>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  3.1363 +  unfolding bigtheta_def by simp
  3.1364 +
  3.1365 +lemma in_bigtheta_zero_iff [simp]: "f \<in> \<Theta>[F](\<lambda>x. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  3.1366 +  unfolding bigtheta_def by simp
  3.1367 +
  3.1368 +
  3.1369 +lemma cmult_in_bigo_iff    [simp]:  "(\<lambda>x. c * f x) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
  3.1370 +  and cmult_in_bigo_iff'   [simp]:  "(\<lambda>x. f x * c) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
  3.1371 +  and cmult_in_smallo_iff  [simp]:  "(\<lambda>x. c * f x) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
  3.1372 +  and cmult_in_smallo_iff' [simp]: "(\<lambda>x. f x * c) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
  3.1373 +  by (cases "c = 0", simp, simp)+
  3.1374 +
  3.1375 +lemma bigo_const [simp]: "(\<lambda>_. c) \<in> O[F](\<lambda>_. 1)" by (rule bigoI[of _ "norm c"]) simp
  3.1376 +
  3.1377 +lemma bigo_const_iff [simp]: "(\<lambda>_. c1) \<in> O[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 = 0 \<or> c2 \<noteq> 0"
  3.1378 +  by (cases "c1 = 0"; cases "c2 = 0")
  3.1379 +     (auto simp: bigo_def eventually_False intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
  3.1380 +
  3.1381 +lemma bigomega_const_iff [simp]: "(\<lambda>_. c1) \<in> \<Omega>[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 \<noteq> 0 \<or> c2 = 0"
  3.1382 +  by (cases "c1 = 0"; cases "c2 = 0")
  3.1383 +     (auto simp: bigomega_def eventually_False mult_le_0_iff 
  3.1384 +           intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
  3.1385 +
  3.1386 +lemma smallo_real_nat_transfer:
  3.1387 +  "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))"
  3.1388 +  by (rule landau_o.small.compose[OF _ filterlim_real_sequentially])
  3.1389 +
  3.1390 +lemma bigo_real_nat_transfer:
  3.1391 +  "(f :: real \<Rightarrow> real) \<in> O(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> O(\<lambda>x. g (real x))"
  3.1392 +  by (rule landau_o.big.compose[OF _ filterlim_real_sequentially])
  3.1393 +
  3.1394 +lemma smallomega_real_nat_transfer:
  3.1395 +  "(f :: real \<Rightarrow> real) \<in> \<omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<omega>(\<lambda>x. g (real x))"
  3.1396 +  by (rule landau_omega.small.compose[OF _ filterlim_real_sequentially])
  3.1397 +
  3.1398 +lemma bigomega_real_nat_transfer:
  3.1399 +  "(f :: real \<Rightarrow> real) \<in> \<Omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Omega>(\<lambda>x. g (real x))"
  3.1400 +  by (rule landau_omega.big.compose[OF _ filterlim_real_sequentially])
  3.1401 +
  3.1402 +lemma bigtheta_real_nat_transfer:
  3.1403 +  "(f :: real \<Rightarrow> real) \<in> \<Theta>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Theta>(\<lambda>x. g (real x))"
  3.1404 +  unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast
  3.1405 +
  3.1406 +lemmas landau_real_nat_transfer [intro] = 
  3.1407 +  bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer 
  3.1408 +  smallomega_real_nat_transfer bigtheta_real_nat_transfer
  3.1409 +
  3.1410 +
  3.1411 +lemma landau_symbol_if_at_top_eq [simp]:
  3.1412 +  assumes "landau_symbol L L' Lr"
  3.1413 +  shows   "L at_top (\<lambda>x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)"
  3.1414 +apply (rule landau_symbol.cong[OF assms])
  3.1415 +using less_add_one[of a] apply (auto intro: eventually_mono  eventually_ge_at_top[of "a + 1"])
  3.1416 +done
  3.1417 +
  3.1418 +lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq]
  3.1419 +
  3.1420 +
  3.1421 +
  3.1422 +lemma sum_in_smallo:
  3.1423 +  assumes "f \<in> o[F](h)" "g \<in> o[F](h)"
  3.1424 +  shows   "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)"
  3.1425 +proof-
  3.1426 +  {
  3.1427 +    fix f g assume fg: "f \<in> o[F](h)" "g \<in> o[F](h)"
  3.1428 +    have "(\<lambda>x. f x + g x) \<in> o[F](h)"
  3.1429 +    proof (rule landau_o.smallI)
  3.1430 +      fix c :: real assume "c > 0"
  3.1431 +      hence "c/2 > 0" by simp
  3.1432 +      from fg[THEN landau_o.smallD[OF _ this]]
  3.1433 +      show "eventually (\<lambda>x. norm (f x + g x) \<le> c * (norm (h x))) F"
  3.1434 +        by eventually_elim (auto intro: order.trans[OF norm_triangle_ineq])
  3.1435 +    qed
  3.1436 +  }
  3.1437 +  from this[of f g] this[of f "\<lambda>x. -g x"] assms
  3.1438 +    show "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" by simp_all
  3.1439 +qed
  3.1440 +
  3.1441 +lemma big_sum_in_smallo:
  3.1442 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> o[F](g)"
  3.1443 +  shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> o[F](g)"
  3.1444 +  using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_smallo)
  3.1445 +
  3.1446 +lemma sum_in_bigo:
  3.1447 +  assumes "f \<in> O[F](h)" "g \<in> O[F](h)"
  3.1448 +  shows   "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)"
  3.1449 +proof-
  3.1450 +  {
  3.1451 +    fix f g assume fg: "f \<in> O[F](h)" "g \<in> O[F](h)"
  3.1452 +    from fg(1) guess c1 by (elim landau_o.bigE) note c1 = this
  3.1453 +    from fg(2) guess c2 by (elim landau_o.bigE) note c2 = this
  3.1454 +    from c1(2) c2(2) have "eventually (\<lambda>x. norm (f x + g x) \<le> (c1 + c2) * (norm (h x))) F"
  3.1455 +      by eventually_elim (auto simp: algebra_simps intro: order.trans[OF norm_triangle_ineq])
  3.1456 +    hence "(\<lambda>x. f x + g x) \<in> O[F](h)" by (rule bigoI)
  3.1457 +  }
  3.1458 +  from this[of f g] this[of f "\<lambda>x. -g x"] assms
  3.1459 +    show "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" by simp_all
  3.1460 +qed
  3.1461 +
  3.1462 +lemma big_sum_in_bigo:
  3.1463 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> O[F](g)"
  3.1464 +  shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"
  3.1465 +  using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)
  3.1466 +
  3.1467 +context landau_symbol
  3.1468 +begin
  3.1469 +
  3.1470 +lemma mult_cancel_left:
  3.1471 +  assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
  3.1472 +  notes   [trans] = bigtheta_trans1 bigtheta_trans2
  3.1473 +  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f2 \<in> L F (g2)"
  3.1474 +proof
  3.1475 +  assume A: "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
  3.1476 +  from assms have nz: "eventually (\<lambda>x. f1 x \<noteq> 0) F" by (simp add: eventually_nonzero_bigtheta)
  3.1477 +  hence "f2 \<in> \<Theta>[F](\<lambda>x. f1 x * f2 x / f1 x)"
  3.1478 +    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  3.1479 +  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)" 
  3.1480 +    by (intro divide_right) simp_all
  3.1481 +  also from assms nz have "(\<lambda>x. g1 x * g2 x / f1 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x / g1 x)"
  3.1482 +    by (intro landau_theta.mult landau_theta.divide) (simp_all add: bigtheta_sym)
  3.1483 +  also from assms have "(\<lambda>x. g1 x * g2 x / g1 x) \<in> \<Theta>[F](g2)"
  3.1484 +    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  3.1485 +  finally show "f2 \<in> L F (g2)" .
  3.1486 +next
  3.1487 +  assume "f2 \<in> L F (g2)"
  3.1488 +  hence "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. f1 x * g2 x)" by (rule mult_left)
  3.1489 +  also have "(\<lambda>x. f1 x * g2 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x)"
  3.1490 +    by (intro landau_theta.mult_right assms)
  3.1491 +  finally show "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" .
  3.1492 +qed
  3.1493 +
  3.1494 +lemma mult_cancel_right:
  3.1495 +  assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
  3.1496 +  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
  3.1497 +  by (subst (1 2) mult.commute) (rule mult_cancel_left[OF assms])
  3.1498 +
  3.1499 +lemma divide_cancel_right:
  3.1500 +  assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
  3.1501 +  shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
  3.1502 +  by (subst (1 2) divide_inverse, intro mult_cancel_right bigtheta_inverse) (simp_all add: assms)
  3.1503 +
  3.1504 +lemma divide_cancel_left:
  3.1505 +  assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
  3.1506 +  shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> 
  3.1507 +             (\<lambda>x. inverse (f2 x)) \<in> L F (\<lambda>x. inverse (g2 x))"
  3.1508 +  by (simp only: divide_inverse mult_cancel_left[OF assms])
  3.1509 +
  3.1510 +end
  3.1511 +
  3.1512 +
  3.1513 +lemma powr_smallo_iff:
  3.1514 +  assumes "filterlim g at_top F" "F \<noteq> bot"
  3.1515 +  shows   "(\<lambda>x. g x powr p :: real) \<in> o[F](\<lambda>x. g x powr q) \<longleftrightarrow> p < q"
  3.1516 +proof-
  3.1517 +  from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
  3.1518 +  hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
  3.1519 +  have B: "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p) \<Longrightarrow> (\<lambda>x. g x powr p) \<notin> o[F](\<lambda>x. g x powr q)"
  3.1520 +  proof
  3.1521 +    assume "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)"
  3.1522 +    from landau_o.big_small_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
  3.1523 +    with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
  3.1524 +    thus False by (simp add: eventually_False assms)
  3.1525 +  qed
  3.1526 +  show ?thesis
  3.1527 +  proof (cases p q rule: linorder_cases)
  3.1528 +    assume "p < q"
  3.1529 +    hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
  3.1530 +      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
  3.1531 +    with `p < q` show ?thesis by auto
  3.1532 +  next
  3.1533 +    assume "p = q"
  3.1534 +    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
  3.1535 +    with B `p = q` show ?thesis by auto
  3.1536 +  next
  3.1537 +    assume "p > q"
  3.1538 +    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
  3.1539 +      by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp: powr_diff [symmetric] )
  3.1540 +    with B `p > q` show ?thesis by auto
  3.1541 +  qed
  3.1542 +qed
  3.1543 +
  3.1544 +lemma powr_bigo_iff:
  3.1545 +  assumes "filterlim g at_top F" "F \<noteq> bot"
  3.1546 +  shows   "(\<lambda>x. g x powr p :: real) \<in> O[F](\<lambda>x. g x powr q) \<longleftrightarrow> p \<le> q"
  3.1547 +proof-
  3.1548 +  from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
  3.1549 +  hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
  3.1550 +  have B: "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p) \<Longrightarrow> (\<lambda>x. g x powr p) \<notin> O[F](\<lambda>x. g x powr q)"
  3.1551 +  proof
  3.1552 +    assume "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" "(\<lambda>x. g x powr p) \<in> O[F](\<lambda>x. g x powr q)"
  3.1553 +    from landau_o.small_big_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
  3.1554 +    with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
  3.1555 +    thus False by (simp add: eventually_False assms)
  3.1556 +  qed
  3.1557 +  show ?thesis
  3.1558 +  proof (cases p q rule: linorder_cases)
  3.1559 +    assume "p < q"
  3.1560 +    hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
  3.1561 +      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
  3.1562 +    with `p < q` show ?thesis by (auto intro: landau_o.small_imp_big)
  3.1563 +  next
  3.1564 +    assume "p = q"
  3.1565 +    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
  3.1566 +    with B `p = q` show ?thesis by auto
  3.1567 +  next
  3.1568 +    assume "p > q"
  3.1569 +    hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
  3.1570 +      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
  3.1571 +    with B `p > q` show ?thesis by (auto intro: landau_o.small_imp_big)
  3.1572 +  qed
  3.1573 +qed
  3.1574 +
  3.1575 +lemma powr_bigtheta_iff: 
  3.1576 +  assumes "filterlim g at_top F" "F \<noteq> bot"
  3.1577 +  shows   "(\<lambda>x. g x powr p :: real) \<in> \<Theta>[F](\<lambda>x. g x powr q) \<longleftrightarrow> p = q"
  3.1578 +  using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff)
  3.1579 +
  3.1580 +
  3.1581 +subsection \<open>Flatness of real functions\<close>
  3.1582 +
  3.1583 +text \<open>
  3.1584 +  Given two real-valued functions $f$ and $g$, we say that $f$ is flatter than $g$ if
  3.1585 +  any power of $f(x)$ is asymptotically dominated by any positive power of $g(x)$. This is
  3.1586 +  a useful notion since, given two products of powers of functions sorted by flatness, we can
  3.1587 +  compare them asymptotically by simply comparing the exponent lists lexicographically.
  3.1588 +
  3.1589 +  A simple sufficient criterion for flatness it that $\ln f(x) \in o(\ln g(x))$, which we show
  3.1590 +  now.
  3.1591 +\<close>
  3.1592 +lemma ln_smallo_imp_flat:
  3.1593 +  fixes f g :: "real \<Rightarrow> real"
  3.1594 +  assumes lim_f: "filterlim f at_top at_top"
  3.1595 +  assumes lim_g: "filterlim g at_top at_top"
  3.1596 +  assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
  3.1597 +  assumes q: "q > 0"
  3.1598 +  shows   "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)"
  3.1599 +proof (rule smalloI_tendsto)
  3.1600 +  from lim_f have "eventually (\<lambda>x. f x > 0) at_top" 
  3.1601 +    by (simp add: filterlim_at_top_dense)
  3.1602 +  hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp
  3.1603 +  
  3.1604 +  from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top"
  3.1605 +    by (simp add: filterlim_at_top_dense)
  3.1606 +  hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp
  3.1607 +  thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top"
  3.1608 +    by eventually_elim simp
  3.1609 +  
  3.1610 +  have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) = 
  3.1611 +                          p * ln (f x) - q * ln (g x)) at_top"
  3.1612 +    using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps)
  3.1613 +  have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top"
  3.1614 +    by (insert q)
  3.1615 +       (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult
  3.1616 +              tendsto_const tendsto_diff smalloD_tendsto[OF ln_o_ln] lim_g
  3.1617 +              filterlim_compose[OF ln_at_top] | simp)+
  3.1618 +  hence "filterlim (\<lambda>x. p * ln (f x) - q * ln (g x)) at_bot at_top"
  3.1619 +    by (subst (asm) filterlim_cong[OF refl refl eq])
  3.1620 +  hence *: "((\<lambda>x. exp (p * ln (f x) - q * ln (g x))) \<longlongrightarrow> 0) at_top"
  3.1621 +    by (rule filterlim_compose[OF exp_at_bot])
  3.1622 +  have eq: "eventually (\<lambda>x. exp (p * ln (f x) - q * ln (g x)) = f x powr p / g x powr q) at_top"
  3.1623 +    using f_nz g_nz by eventually_elim (simp add: powr_def exp_diff)
  3.1624 +  show "((\<lambda>x. f x powr p / g x powr q) \<longlongrightarrow> 0) at_top"
  3.1625 +    using * by (subst (asm) filterlim_cong[OF refl refl eq])
  3.1626 +qed
  3.1627 +
  3.1628 +lemma ln_smallo_imp_flat':
  3.1629 +  fixes f g :: "real \<Rightarrow> real"
  3.1630 +  assumes lim_f: "filterlim f at_top at_top"
  3.1631 +  assumes lim_g: "filterlim g at_top at_top"
  3.1632 +  assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
  3.1633 +  assumes q: "q < 0"
  3.1634 +  shows   "(\<lambda>x. g x powr q) \<in> o(\<lambda>x. f x powr p)"
  3.1635 +proof -
  3.1636 +  from lim_f lim_g have "eventually (\<lambda>x. f x > 0) at_top" "eventually (\<lambda>x. g x > 0) at_top"
  3.1637 +    by (simp_all add: filterlim_at_top_dense)
  3.1638 +  hence "eventually (\<lambda>x. f x \<noteq> 0) at_top" "eventually (\<lambda>x. g x \<noteq> 0) at_top"
  3.1639 +    by (auto elim: eventually_mono)
  3.1640 +  moreover from assms have "(\<lambda>x. f x powr -p) \<in> o(\<lambda>x. g x powr -q)"
  3.1641 +    by (intro ln_smallo_imp_flat assms) simp_all
  3.1642 +  ultimately show ?thesis unfolding powr_minus
  3.1643 +    by (simp add: landau_o.small.inverse_cancel)
  3.1644 +qed
  3.1645 +
  3.1646 +
  3.1647 +subsection \<open>Asymptotic Equivalence\<close>
  3.1648 +
  3.1649 +(* TODO Move *)
  3.1650 +lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
  3.1651 +  by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
  3.1652 +
  3.1653 +named_theorems asymp_equiv_intros
  3.1654 +named_theorems asymp_equiv_simps
  3.1655 +
  3.1656 +definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  3.1657 +  ("_ \<sim>[_] _" [51, 10, 51] 50)
  3.1658 +  where "f \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
  3.1659 +
  3.1660 +abbreviation (input) asymp_equiv_at_top where
  3.1661 +  "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"
  3.1662 +
  3.1663 +bundle asymp_equiv_notation
  3.1664 +begin
  3.1665 +notation asymp_equiv_at_top (infix "\<sim>" 50) 
  3.1666 +end
  3.1667 +
  3.1668 +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"
  3.1669 +  by (simp add: asymp_equiv_def)
  3.1670 +
  3.1671 +lemma asymp_equivD: "f \<sim>[F] g \<Longrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
  3.1672 +  by (simp add: asymp_equiv_def)
  3.1673 +
  3.1674 +lemma asymp_equiv_filtermap_iff:
  3.1675 +  "f \<sim>[filtermap h F] g \<longleftrightarrow> (\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
  3.1676 +  by (simp add: asymp_equiv_def filterlim_filtermap)
  3.1677 +
  3.1678 +lemma asymp_equiv_refl [simp, asymp_equiv_intros]: "f \<sim>[F] f"
  3.1679 +proof (intro asymp_equivI)
  3.1680 +  have "eventually (\<lambda>x. 1 = (if f x = 0 \<and> f x = 0 then 1 else f x / f x)) F"
  3.1681 +    by (intro always_eventually) simp
  3.1682 +  moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
  3.1683 +  ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
  3.1684 +    by (rule Lim_transform_eventually)
  3.1685 +qed
  3.1686 +
  3.1687 +lemma asymp_equiv_symI: 
  3.1688 +  assumes "f \<sim>[F] g"
  3.1689 +  shows   "g \<sim>[F] f"
  3.1690 +  using tendsto_inverse[OF asymp_equivD[OF assms]]
  3.1691 +  by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong)
  3.1692 +
  3.1693 +lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f"
  3.1694 +  by (blast intro: asymp_equiv_symI)
  3.1695 +
  3.1696 +lemma asymp_equivI': 
  3.1697 +  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
  3.1698 +  shows   "f \<sim>[F] g"
  3.1699 +proof (cases "F = bot")
  3.1700 +  case False
  3.1701 +  have "eventually (\<lambda>x. f x \<noteq> 0) F"
  3.1702 +  proof (rule ccontr)
  3.1703 +    assume "\<not>eventually (\<lambda>x. f x \<noteq> 0) F"
  3.1704 +    hence "frequently (\<lambda>x. f x = 0) F" by (simp add: frequently_def)
  3.1705 +    hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1)
  3.1706 +    from limit_frequently_eq[OF False this assms] show False by simp_all
  3.1707 +  qed
  3.1708 +  hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"
  3.1709 +    by eventually_elim simp
  3.1710 +  from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def 
  3.1711 +    by (rule Lim_transform_eventually)
  3.1712 +qed (simp_all add: asymp_equiv_def)
  3.1713 +
  3.1714 +
  3.1715 +lemma asymp_equiv_cong:
  3.1716 +  assumes "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
  3.1717 +  shows   "f1 \<sim>[F] g1 \<longleftrightarrow> f2 \<sim>[F] g2"
  3.1718 +  unfolding asymp_equiv_def
  3.1719 +proof (rule tendsto_cong, goal_cases)
  3.1720 +  case 1
  3.1721 +  from assms show ?case by eventually_elim simp
  3.1722 +qed
  3.1723 +
  3.1724 +lemma asymp_equiv_eventually_zeros:
  3.1725 +  fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
  3.1726 +  assumes "f \<sim>[F] g"
  3.1727 +  shows   "eventually (\<lambda>x. f x = 0 \<longleftrightarrow> g x = 0) F"
  3.1728 +proof -
  3.1729 +  let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  3.1730 +  have "eventually (\<lambda>x. x \<noteq> 0) (nhds (1::'b))"
  3.1731 +    by (rule t1_space_nhds) auto
  3.1732 +  hence "eventually (\<lambda>x. x \<noteq> 0) (filtermap ?h F)"
  3.1733 +    using assms unfolding asymp_equiv_def filterlim_def
  3.1734 +    by (rule filter_leD [rotated])
  3.1735 +  hence "eventually (\<lambda>x. ?h x \<noteq> 0) F" by (simp add: eventually_filtermap)
  3.1736 +  thus ?thesis by eventually_elim (auto split: if_splits)
  3.1737 +qed
  3.1738 +
  3.1739 +lemma asymp_equiv_transfer:
  3.1740 +  assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
  3.1741 +  shows   "f2 \<sim>[F] g2"
  3.1742 +  using assms(1) asymp_equiv_cong[OF assms(2,3)] by simp
  3.1743 +
  3.1744 +lemma asymp_equiv_transfer_trans [trans]:
  3.1745 +  assumes "(\<lambda>x. f x (h1 x)) \<sim>[F] (\<lambda>x. g x (h1 x))"
  3.1746 +  assumes "eventually (\<lambda>x. h1 x = h2 x) F"
  3.1747 +  shows   "(\<lambda>x. f x (h2 x)) \<sim>[F] (\<lambda>x. g x (h2 x))"
  3.1748 +  by (rule asymp_equiv_transfer[OF assms(1)]) (insert assms(2), auto elim!: eventually_mono)
  3.1749 +
  3.1750 +lemma asymp_equiv_trans [trans]:
  3.1751 +  fixes f g h
  3.1752 +  assumes "f \<sim>[F] g" "g \<sim>[F] h"
  3.1753 +  shows   "f \<sim>[F] h"
  3.1754 +proof -
  3.1755 +  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  3.1756 +  from assms[THEN asymp_equiv_eventually_zeros]
  3.1757 +    have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
  3.1758 +  moreover from tendsto_mult[OF assms[THEN asymp_equivD]] 
  3.1759 +    have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
  3.1760 +  ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
  3.1761 +qed
  3.1762 +
  3.1763 +lemma asymp_equiv_trans_lift1 [trans]:
  3.1764 +  assumes "a \<sim>[F] f b" "b \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
  3.1765 +  shows   "a \<sim>[F] f c"
  3.1766 +  using assms by (blast intro: asymp_equiv_trans)
  3.1767 +
  3.1768 +lemma asymp_equiv_trans_lift2 [trans]:
  3.1769 +  assumes "f a \<sim>[F] b" "a \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
  3.1770 +  shows   "f c \<sim>[F] b"
  3.1771 +  using asymp_equiv_symI[OF assms(3)[OF assms(2)]] assms(1)
  3.1772 +  by (blast intro: asymp_equiv_trans)
  3.1773 +
  3.1774 +lemma asymp_equivD_const:
  3.1775 +  assumes "f \<sim>[F] (\<lambda>_. c)"
  3.1776 +  shows   "(f \<longlongrightarrow> c) F"
  3.1777 +proof (cases "c = 0")
  3.1778 +  case False
  3.1779 +  with tendsto_mult_right[OF asymp_equivD[OF assms], of c] show ?thesis by simp
  3.1780 +next
  3.1781 +  case True
  3.1782 +  with asymp_equiv_eventually_zeros[OF assms] show ?thesis
  3.1783 +    by (simp add: Lim_eventually)
  3.1784 +qed
  3.1785 +
  3.1786 +lemma asymp_equiv_refl_ev:
  3.1787 +  assumes "eventually (\<lambda>x. f x = g x) F"
  3.1788 +  shows   "f \<sim>[F] g"
  3.1789 +  by (intro asymp_equivI Lim_eventually)
  3.1790 +     (insert assms, auto elim!: eventually_mono)
  3.1791 +
  3.1792 +lemma asymp_equiv_sandwich:
  3.1793 +  fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"
  3.1794 +  assumes "eventually (\<lambda>x. f x \<ge> 0) F"
  3.1795 +  assumes "eventually (\<lambda>x. f x \<le> g x) F"
  3.1796 +  assumes "eventually (\<lambda>x. g x \<le> h x) F"
  3.1797 +  assumes "f \<sim>[F] h"
  3.1798 +  shows   "g \<sim>[F] f" "g \<sim>[F] h"
  3.1799 +proof -
  3.1800 +  show "g \<sim>[F] f"
  3.1801 +  proof (rule asymp_equivI, rule tendsto_sandwich)
  3.1802 +    from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
  3.1803 +      show "eventually (\<lambda>n. (if h n = 0 \<and> f n = 0 then 1 else h n / f n) \<ge>
  3.1804 +                              (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
  3.1805 +        by eventually_elim (auto intro!: divide_right_mono)
  3.1806 +    from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
  3.1807 +      show "eventually (\<lambda>n. 1 \<le>
  3.1808 +                              (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
  3.1809 +        by eventually_elim (auto intro!: divide_right_mono)
  3.1810 +  qed (insert asymp_equiv_symI[OF assms(4)], simp_all add: asymp_equiv_def)
  3.1811 +  also note \<open>f \<sim>[F] h\<close>
  3.1812 +  finally show "g \<sim>[F] h" .
  3.1813 +qed
  3.1814 +
  3.1815 +lemma asymp_equiv_imp_eventually_same_sign:
  3.1816 +  fixes f g :: "real \<Rightarrow> real"
  3.1817 +  assumes "f \<sim>[F] g"
  3.1818 +  shows   "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
  3.1819 +proof -
  3.1820 +  from assms have "((\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> sgn 1) F"
  3.1821 +    unfolding asymp_equiv_def by (rule tendsto_sgn) simp_all
  3.1822 +  from order_tendstoD(1)[OF this, of "1/2"]
  3.1823 +    have "eventually (\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x) > 1/2) F"
  3.1824 +    by simp
  3.1825 +  thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
  3.1826 +  proof eventually_elim
  3.1827 +    case (elim x)
  3.1828 +    thus ?case
  3.1829 +      by (cases "f x" "0 :: real" rule: linorder_cases; 
  3.1830 +          cases "g x" "0 :: real" rule: linorder_cases) simp_all
  3.1831 +  qed
  3.1832 +qed
  3.1833 +
  3.1834 +lemma
  3.1835 +  fixes f g :: "_ \<Rightarrow> real"
  3.1836 +  assumes "f \<sim>[F] g"
  3.1837 +  shows   asymp_equiv_eventually_same_sign: "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" (is ?th1)
  3.1838 +    and   asymp_equiv_eventually_neg_iff:   "eventually (\<lambda>x. f x < 0 \<longleftrightarrow> g x < 0) F" (is ?th2)
  3.1839 +    and   asymp_equiv_eventually_pos_iff:   "eventually (\<lambda>x. f x > 0 \<longleftrightarrow> g x > 0) F" (is ?th3)
  3.1840 +proof -
  3.1841 +  from assms have "filterlim (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) (nhds 1) F"
  3.1842 +    by (rule asymp_equivD)
  3.1843 +  from order_tendstoD(1)[OF this zero_less_one]
  3.1844 +    show ?th1 ?th2 ?th3
  3.1845 +    by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+
  3.1846 +qed
  3.1847 +
  3.1848 +lemma asymp_equiv_tendsto_transfer:
  3.1849 +  assumes "f \<sim>[F] g" and "(f \<longlongrightarrow> c) F"
  3.1850 +  shows   "(g \<longlongrightarrow> c) F"
  3.1851 +proof -
  3.1852 +  let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"
  3.1853 +  have "eventually (\<lambda>x. ?h x = g x) F"
  3.1854 +    using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
  3.1855 +  moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
  3.1856 +  hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"
  3.1857 +    by (rule asymp_equivD)
  3.1858 +  from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp
  3.1859 +  ultimately show ?thesis by (rule Lim_transform_eventually)
  3.1860 +qed
  3.1861 +
  3.1862 +lemma tendsto_asymp_equiv_cong:
  3.1863 +  assumes "f \<sim>[F] g"
  3.1864 +  shows   "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"
  3.1865 +proof -
  3.1866 +  {
  3.1867 +    fix f g :: "'a \<Rightarrow> 'b"
  3.1868 +    assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"
  3.1869 +    have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"
  3.1870 +      using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp
  3.1871 +    moreover have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F"
  3.1872 +      by (intro tendsto_intros asymp_equivD *)
  3.1873 +    ultimately have "(f \<longlongrightarrow> c * 1) F"
  3.1874 +      by (rule Lim_transform_eventually)
  3.1875 +  }
  3.1876 +  from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym)
  3.1877 +qed
  3.1878 +
  3.1879 +
  3.1880 +lemma smallo_imp_eventually_sgn:
  3.1881 +  fixes f g :: "real \<Rightarrow> real"
  3.1882 +  assumes "g \<in> o(f)"
  3.1883 +  shows   "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top"
  3.1884 +proof -
  3.1885 +  have "0 < (1/2 :: real)" by simp
  3.1886 +  from landau_o.smallD[OF assms, OF this] 
  3.1887 +    have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp
  3.1888 +  thus ?thesis
  3.1889 +  proof eventually_elim
  3.1890 +    case (elim x)
  3.1891 +    thus ?case
  3.1892 +      by (cases "f x" "0::real" rule: linorder_cases; 
  3.1893 +          cases "f x + g x" "0::real" rule: linorder_cases) simp_all
  3.1894 +  qed
  3.1895 +qed
  3.1896 +
  3.1897 +context
  3.1898 +begin
  3.1899 +
  3.1900 +private lemma asymp_equiv_add_rightI:
  3.1901 +  assumes "f \<sim>[F] g" "h \<in> o[F](g)"
  3.1902 +  shows   "(\<lambda>x. f x + h x) \<sim>[F] g"
  3.1903 +proof -
  3.1904 +  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  3.1905 +  from landau_o.smallD[OF assms(2) zero_less_one]
  3.1906 +    have ev: "eventually (\<lambda>x. g x = 0 \<longrightarrow> h x = 0) F" by eventually_elim auto
  3.1907 +  have "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1) F"
  3.1908 +    unfolding asymp_equiv_def using ev
  3.1909 +    by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps)
  3.1910 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1 + 0) F" by simp
  3.1911 +  also have \<dots> by (intro tendsto_intros asymp_equivD assms smalloD_tendsto)
  3.1912 +  finally show "(\<lambda>x. f x + h x) \<sim>[F] g" .
  3.1913 +qed
  3.1914 +
  3.1915 +lemma asymp_equiv_add_right [asymp_equiv_simps]:
  3.1916 +  assumes "h \<in> o[F](g)"
  3.1917 +  shows   "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
  3.1918 +proof
  3.1919 +  assume "(\<lambda>x. f x + h x) \<sim>[F] g"
  3.1920 +  from asymp_equiv_add_rightI[OF this, of "\<lambda>x. -h x"] assms show "f \<sim>[F] g"
  3.1921 +    by simp
  3.1922 +qed (simp_all add: asymp_equiv_add_rightI assms)
  3.1923 +
  3.1924 +end
  3.1925 +
  3.1926 +lemma asymp_equiv_add_left [asymp_equiv_simps]: 
  3.1927 +  assumes "h \<in> o[F](g)"
  3.1928 +  shows   "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
  3.1929 +  using asymp_equiv_add_right[OF assms] by (simp add: add.commute)
  3.1930 +
  3.1931 +lemma asymp_equiv_add_right' [asymp_equiv_simps]:
  3.1932 +  assumes "h \<in> o[F](g)"
  3.1933 +  shows   "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f"
  3.1934 +  using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym)
  3.1935 +  
  3.1936 +lemma asymp_equiv_add_left' [asymp_equiv_simps]:
  3.1937 +  assumes "h \<in> o[F](g)"
  3.1938 +  shows   "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f"
  3.1939 +  using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym)
  3.1940 +
  3.1941 +lemma smallo_imp_asymp_equiv:
  3.1942 +  assumes "(\<lambda>x. f x - g x) \<in> o[F](g)"
  3.1943 +  shows   "f \<sim>[F] g"
  3.1944 +proof -
  3.1945 +  from assms have "(\<lambda>x. f x - g x + g x) \<sim>[F] g"
  3.1946 +    by (subst asymp_equiv_add_left) simp_all
  3.1947 +  thus ?thesis by simp
  3.1948 +qed
  3.1949 +
  3.1950 +lemma asymp_equiv_uminus [asymp_equiv_intros]:
  3.1951 +  "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. -f x) \<sim>[F] (\<lambda>x. -g x)"
  3.1952 +  by (simp add: asymp_equiv_def cong: if_cong)
  3.1953 +
  3.1954 +lemma asymp_equiv_uminus_iff [asymp_equiv_simps]:
  3.1955 +  "(\<lambda>x. -f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] (\<lambda>x. -g x)"
  3.1956 +  by (simp add: asymp_equiv_def cong: if_cong)
  3.1957 +
  3.1958 +lemma asymp_equiv_mult [asymp_equiv_intros]:
  3.1959 +  fixes f1 f2 g1 g2 :: "'a \<Rightarrow> 'b :: real_normed_field"
  3.1960 +  assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
  3.1961 +  shows   "(\<lambda>x. f1 x * f2 x) \<sim>[F] (\<lambda>x. g1 x * g2 x)"
  3.1962 +proof -
  3.1963 +  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  3.1964 +  let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x
  3.1965 +                   else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)"
  3.1966 +  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"
  3.1967 +  {
  3.1968 +    fix f g :: "'a \<Rightarrow> 'b" assume "f \<sim>[F] g"
  3.1969 +    have "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F"
  3.1970 +      by (rule tendsto_eq_intros refl asymp_equivD[OF \<open>f \<sim>[F] g\<close>])+ simp_all
  3.1971 +  } note A = this    
  3.1972 +
  3.1973 +  from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"
  3.1974 +    by (intro tendsto_mult asymp_equivD)
  3.1975 +  moreover {
  3.1976 +    have "eventually (\<lambda>x. ?S x = ?S' x) F"
  3.1977 +      using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
  3.1978 +    moreover have "(?S \<longlongrightarrow> 0) F"
  3.1979 +      by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])
  3.1980 +         (auto intro: le_infI1 le_infI2)
  3.1981 +    ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)
  3.1982 +  }
  3.1983 +  ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"
  3.1984 +    by (rule Lim_transform)
  3.1985 +  thus ?thesis by (simp add: asymp_equiv_def)
  3.1986 +qed
  3.1987 +
  3.1988 +lemma asymp_equiv_power [asymp_equiv_intros]:
  3.1989 +  "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)"
  3.1990 +  by (induction n) (simp_all add: asymp_equiv_mult)
  3.1991 +
  3.1992 +lemma asymp_equiv_inverse [asymp_equiv_intros]:
  3.1993 +  assumes "f \<sim>[F] g"
  3.1994 +  shows   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
  3.1995 +proof -
  3.1996 +  from tendsto_inverse[OF asymp_equivD[OF assms]]
  3.1997 +    have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) \<longlongrightarrow> 1) F"
  3.1998 +    by (simp add: if_distrib cong: if_cong)
  3.1999 +  also have "(\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) =
  3.2000 +               (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else inverse (f x) / inverse (g x))"
  3.2001 +    by (intro ext) (simp add: field_simps)
  3.2002 +  finally show ?thesis by (simp add: asymp_equiv_def)
  3.2003 +qed
  3.2004 +
  3.2005 +lemma asymp_equiv_inverse_iff [asymp_equiv_simps]:
  3.2006 +  "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<sim>[F] g"
  3.2007 +proof
  3.2008 +  assume "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
  3.2009 +  hence "(\<lambda>x. inverse (inverse (f x))) \<sim>[F] (\<lambda>x. inverse (inverse (g x)))" (is ?P)
  3.2010 +    by (rule asymp_equiv_inverse)
  3.2011 +  also have "?P \<longleftrightarrow> f \<sim>[F] g" by (intro asymp_equiv_cong) simp_all
  3.2012 +  finally show "f \<sim>[F] g" .
  3.2013 +qed (simp_all add: asymp_equiv_inverse)
  3.2014 +
  3.2015 +lemma asymp_equiv_divide [asymp_equiv_intros]:
  3.2016 +  assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
  3.2017 +  shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
  3.2018 +  using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
  3.2019 +
  3.2020 +lemma asymp_equiv_compose [asymp_equiv_intros]:
  3.2021 +  assumes "f \<sim>[G] g" "filterlim h G F"
  3.2022 +  shows   "f \<circ> h \<sim>[F] g \<circ> h"
  3.2023 +proof -
  3.2024 +  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  3.2025 +  have "f \<circ> h \<sim>[F] g \<circ> h \<longleftrightarrow> ((?T f g \<circ> h) \<longlongrightarrow> 1) F"
  3.2026 +    by (simp add: asymp_equiv_def o_def)
  3.2027 +  also have "\<dots> \<longleftrightarrow> (?T f g \<longlongrightarrow> 1) (filtermap h F)"
  3.2028 +    by (rule tendsto_compose_filtermap)
  3.2029 +  also have "\<dots>"
  3.2030 +    by (rule tendsto_mono[of _ G]) (insert assms, simp_all add: asymp_equiv_def filterlim_def)
  3.2031 +  finally show ?thesis .
  3.2032 +qed
  3.2033 +
  3.2034 +lemma asymp_equiv_compose':
  3.2035 +  assumes "f \<sim>[G] g" "filterlim h G F"
  3.2036 +  shows   "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
  3.2037 +  using asymp_equiv_compose[OF assms] by (simp add: o_def)
  3.2038 +  
  3.2039 +lemma asymp_equiv_powr_real [asymp_equiv_intros]:
  3.2040 +  fixes f g :: "'a \<Rightarrow> real"
  3.2041 +  assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
  3.2042 +  shows   "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"
  3.2043 +proof -
  3.2044 +  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  3.2045 +  have "eventually (\<lambda>x. ?T f g x powr y = ?T (\<lambda>x. f x powr y) (\<lambda>x. g x powr y) x) F"
  3.2046 +    using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)
  3.2047 +    by eventually_elim (auto simp: powr_divide)
  3.2048 +  moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
  3.2049 +    by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
  3.2050 +  hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
  3.2051 +  ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
  3.2052 +qed
  3.2053 +
  3.2054 +lemma asymp_equiv_norm [asymp_equiv_intros]:
  3.2055 +  fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
  3.2056 +  assumes "f \<sim>[F] g"
  3.2057 +  shows   "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))"
  3.2058 +  using tendsto_norm[OF asymp_equivD[OF assms]] 
  3.2059 +  by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong)
  3.2060 +
  3.2061 +lemma asymp_equiv_abs_real [asymp_equiv_intros]:
  3.2062 +  fixes f g :: "'a \<Rightarrow> real"
  3.2063 +  assumes "f \<sim>[F] g"
  3.2064 +  shows   "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)"
  3.2065 +  using tendsto_rabs[OF asymp_equivD[OF assms]] 
  3.2066 +  by (simp add: if_distrib asymp_equiv_def cong: if_cong)
  3.2067 +
  3.2068 +lemma asymp_equiv_imp_eventually_le:
  3.2069 +  assumes "f \<sim>[F] g" "c > 1"
  3.2070 +  shows   "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"
  3.2071 +proof -
  3.2072 +  from order_tendstoD(2)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
  3.2073 +       asymp_equiv_eventually_zeros[OF assms(1)]
  3.2074 +    show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
  3.2075 +qed
  3.2076 +
  3.2077 +lemma asymp_equiv_imp_eventually_ge:
  3.2078 +  assumes "f \<sim>[F] g" "c < 1"
  3.2079 +  shows   "eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F"
  3.2080 +proof -
  3.2081 +  from order_tendstoD(1)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
  3.2082 +       asymp_equiv_eventually_zeros[OF assms(1)]
  3.2083 +    show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
  3.2084 +qed
  3.2085 +
  3.2086 +lemma asymp_equiv_imp_bigo:
  3.2087 +  assumes "f \<sim>[F] g"
  3.2088 +  shows   "f \<in> O[F](g)"
  3.2089 +proof (rule bigoI)
  3.2090 +  have "(3/2::real) > 1" by simp
  3.2091 +  from asymp_equiv_imp_eventually_le[OF assms this]
  3.2092 +    show "eventually (\<lambda>x. norm (f x) \<le> 3/2 * norm (g x)) F"
  3.2093 +    by eventually_elim simp
  3.2094 +qed
  3.2095 +
  3.2096 +lemma asymp_equiv_imp_bigomega:
  3.2097 +  "f \<sim>[F] g \<Longrightarrow> f \<in> \<Omega>[F](g)"
  3.2098 +  using asymp_equiv_imp_bigo[of g F f] by (simp add: asymp_equiv_sym bigomega_iff_bigo)
  3.2099 +
  3.2100 +lemma asymp_equiv_imp_bigtheta:
  3.2101 +  "f \<sim>[F] g \<Longrightarrow> f \<in> \<Theta>[F](g)"
  3.2102 +  by (intro bigthetaI asymp_equiv_imp_bigo asymp_equiv_imp_bigomega)
  3.2103 +
  3.2104 +lemma asymp_equiv_at_infinity_transfer:
  3.2105 +  assumes "f \<sim>[F] g" "filterlim f at_infinity F"
  3.2106 +  shows   "filterlim g at_infinity F"
  3.2107 +proof -
  3.2108 +  from assms(1) have "g \<in> \<Theta>[F](f)" by (rule asymp_equiv_imp_bigtheta[OF asymp_equiv_symI])
  3.2109 +  also from assms have "f \<in> \<omega>[F](\<lambda>_. 1)" by (simp add: smallomega_1_conv_filterlim)
  3.2110 +  finally show ?thesis by (simp add: smallomega_1_conv_filterlim)
  3.2111 +qed
  3.2112 +
  3.2113 +lemma asymp_equiv_at_top_transfer:
  3.2114 +  fixes f g :: "_ \<Rightarrow> real"
  3.2115 +  assumes "f \<sim>[F] g" "filterlim f at_top F"
  3.2116 +  shows   "filterlim g at_top F"
  3.2117 +proof (rule filterlim_at_infinity_imp_filterlim_at_top)
  3.2118 +  show "filterlim g at_infinity F"
  3.2119 +    by (rule asymp_equiv_at_infinity_transfer[OF assms(1) filterlim_mono[OF assms(2)]])
  3.2120 +       (auto simp: at_top_le_at_infinity)
  3.2121 +  from assms(2) have "eventually (\<lambda>x. f x > 0) F"
  3.2122 +    using filterlim_at_top_dense by blast
  3.2123 +  with asymp_equiv_eventually_pos_iff[OF assms(1)] show "eventually (\<lambda>x. g x > 0) F"
  3.2124 +    by eventually_elim blast
  3.2125 +qed
  3.2126 +
  3.2127 +lemma asymp_equiv_at_bot_transfer:
  3.2128 +  fixes f g :: "_ \<Rightarrow> real"
  3.2129 +  assumes "f \<sim>[F] g" "filterlim f at_bot F"
  3.2130 +  shows   "filterlim g at_bot F"
  3.2131 +  unfolding filterlim_uminus_at_bot
  3.2132 +  by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"])
  3.2133 +     (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus)  
  3.2134 +
  3.2135 +lemma asymp_equivI'_const:
  3.2136 +  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0"
  3.2137 +  shows   "f \<sim>[F] (\<lambda>x. c * g x)"
  3.2138 +  using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2)
  3.2139 +  by (intro asymp_equivI') (simp add: field_simps)
  3.2140 +
  3.2141 +lemma asymp_equivI'_inverse_const:
  3.2142 +  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> inverse c) F" "c \<noteq> 0"
  3.2143 +  shows   "(\<lambda>x. c * f x) \<sim>[F] g"
  3.2144 +  using tendsto_mult[OF assms(1) tendsto_const[of "c"]] assms(2)
  3.2145 +  by (intro asymp_equivI') (simp add: field_simps)
  3.2146 +
  3.2147 +lemma filterlim_at_bot_imp_at_infinity: "filterlim f at_bot F \<Longrightarrow> filterlim f at_infinity F"
  3.2148 +  for f :: "_ \<Rightarrow> real" using at_bot_le_at_infinity filterlim_mono by blast
  3.2149 +
  3.2150 +lemma asymp_equiv_imp_diff_smallo:
  3.2151 +  assumes "f \<sim>[F] g"
  3.2152 +  shows   "(\<lambda>x. f x - g x) \<in> o[F](g)"
  3.2153 +proof (rule landau_o.smallI)
  3.2154 +  fix c :: real assume "c > 0"
  3.2155 +  hence c: "min c 1 > 0" by simp
  3.2156 +  let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  3.2157 +  from assms have "((\<lambda>x. ?h x - 1) \<longlongrightarrow> 1 - 1) F"
  3.2158 +    by (intro tendsto_diff asymp_equivD tendsto_const)
  3.2159 +  from tendstoD[OF this c] show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
  3.2160 +  proof eventually_elim
  3.2161 +    case (elim x)
  3.2162 +    from elim have "norm (f x - g x) \<le> norm (f x / g x - 1) * norm (g x)"
  3.2163 +      by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps)
  3.2164 +    also have "norm (f x / g x - 1) * norm (g x) \<le> c * norm (g x)" using elim
  3.2165 +      by (auto split: if_splits simp: mult_right_mono)
  3.2166 +    finally show ?case .
  3.2167 +  qed
  3.2168 +qed
  3.2169 +
  3.2170 +lemma asymp_equiv_altdef:
  3.2171 +  "f \<sim>[F] g \<longleftrightarrow> (\<lambda>x. f x - g x) \<in> o[F](g)"
  3.2172 +  by (rule iffI[OF asymp_equiv_imp_diff_smallo smallo_imp_asymp_equiv])
  3.2173 +
  3.2174 +lemma asymp_equiv_0_left_iff [simp]: "(\<lambda>_. 0) \<sim>[F] f \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  3.2175 +  and asymp_equiv_0_right_iff [simp]: "f \<sim>[F] (\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  3.2176 +  by (simp_all add: asymp_equiv_altdef landau_o.small_refl_iff)
  3.2177 +
  3.2178 +lemma asymp_equiv_sandwich_real:
  3.2179 +  fixes f g l u :: "'a \<Rightarrow> real"
  3.2180 +  assumes "l \<sim>[F] g" "u \<sim>[F] g" "eventually (\<lambda>x. f x \<in> {l x..u x}) F"
  3.2181 +  shows   "f \<sim>[F] g"
  3.2182 +  unfolding asymp_equiv_altdef
  3.2183 +proof (rule landau_o.smallI)
  3.2184 +  fix c :: real assume c: "c > 0"
  3.2185 +  have "eventually (\<lambda>x. norm (f x - g x) \<le> max (norm (l x - g x)) (norm (u x - g x))) F"
  3.2186 +    using assms(3) by eventually_elim auto
  3.2187 +  moreover have "eventually (\<lambda>x. norm (l x - g x) \<le> c * norm (g x)) F"
  3.2188 +                "eventually (\<lambda>x. norm (u x - g x) \<le> c * norm (g x)) F"
  3.2189 +    using assms(1,2) by (auto simp: asymp_equiv_altdef dest: landau_o.smallD[OF _ c])
  3.2190 +  hence "eventually (\<lambda>x. max (norm (l x - g x)) (norm (u x - g x)) \<le> c * norm (g x)) F"
  3.2191 +    by eventually_elim simp
  3.2192 +  ultimately show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
  3.2193 +    by eventually_elim (rule order.trans)
  3.2194 +qed
  3.2195 +
  3.2196 +lemma asymp_equiv_sandwich_real':
  3.2197 +  fixes f g l u :: "'a \<Rightarrow> real"
  3.2198 +  assumes "f \<sim>[F] l" "f \<sim>[F] u" "eventually (\<lambda>x. g x \<in> {l x..u x}) F"
  3.2199 +  shows   "f \<sim>[F] g"
  3.2200 +  using asymp_equiv_sandwich_real[of l F f u g] assms by (simp add: asymp_equiv_sym)
  3.2201 +
  3.2202 +lemma asymp_equiv_sandwich_real'':
  3.2203 +  fixes f g l u :: "'a \<Rightarrow> real"
  3.2204 +  assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"
  3.2205 +          "eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"
  3.2206 +  shows   "f \<sim>[F] g"
  3.2207 +  by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]
  3.2208 +             asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];
  3.2209 +      blast intro: asymp_equiv_trans assms(1,2,3))+
  3.2210 +
  3.2211 +end
     4.1 --- a/src/HOL/Library/Library.thy	Tue May 22 11:05:47 2018 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Fri May 18 17:51:58 2018 +0200
     4.3 @@ -38,6 +38,7 @@
     4.4    Indicator_Function
     4.5    Infinite_Set
     4.6    IArray
     4.7 +  Landau_Symbols
     4.8    Lattice_Algebras
     4.9    Lattice_Syntax
    4.10    Lattice_Constructions