src/HOL/Library/Landau_Symbols.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 68406 6beb45f6cf67
child 68696 8a071eeddb2a
permissions -rw-r--r--
tuned equation
     1 (*
     2   File:   Landau_Symbols_Definition.thy
     3   Author: Manuel Eberl <eberlm@in.tum.de>
     4 
     5   Landau symbols for reasoning about the asymptotic growth of functions. 
     6 *)
     7 section {* Definition of Landau symbols *}
     8 
     9 theory Landau_Symbols
    10 imports 
    11   Complex_Main
    12 begin
    13 
    14 lemma eventually_subst':
    15   "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> eventually (\<lambda>x. P x (f x)) F = eventually (\<lambda>x. P x (g x)) F"
    16   by (rule eventually_subst, erule eventually_rev_mp) simp
    17 
    18 
    19 subsection {* Definition of Landau symbols *}
    20 
    21 text {*
    22   Our Landau symbols are sign-oblivious, i.e. any function always has the same growth 
    23   as its absolute. This has the advantage of making some cancelling rules for sums nicer, but 
    24   introduces some problems in other places. Nevertheless, we found this definition more convenient
    25   to work with.
    26 *}
    27 
    28 definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    29     ("(1O[_]'(_'))")
    30   where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"  
    31 
    32 definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    33     ("(1o[_]'(_'))")
    34   where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
    35 
    36 definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    37     ("(1\<Omega>[_]'(_'))")
    38   where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"  
    39 
    40 definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    41     ("(1\<omega>[_]'(_'))")
    42   where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
    43 
    44 definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    45     ("(1\<Theta>[_]'(_'))")
    46   where "bigtheta F g = bigo F g \<inter> bigomega F g"
    47 
    48 abbreviation bigo_at_top ("(2O'(_'))") where
    49   "O(g) \<equiv> bigo at_top g"    
    50 
    51 abbreviation smallo_at_top ("(2o'(_'))") where
    52   "o(g) \<equiv> smallo at_top g"
    53 
    54 abbreviation bigomega_at_top ("(2\<Omega>'(_'))") where
    55   "\<Omega>(g) \<equiv> bigomega at_top g"
    56 
    57 abbreviation smallomega_at_top ("(2\<omega>'(_'))") where
    58   "\<omega>(g) \<equiv> smallomega at_top g"
    59 
    60 abbreviation bigtheta_at_top ("(2\<Theta>'(_'))") where
    61   "\<Theta>(g) \<equiv> bigtheta at_top g"
    62     
    63 
    64 text {* The following is a set of properties that all Landau symbols satisfy. *}
    65 
    66 named_theorems landau_divide_simps
    67 
    68 locale landau_symbol =
    69   fixes L  :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
    70   and   L'  :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"
    71   and   Lr  :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"
    72   assumes bot': "L bot f = UNIV"
    73   assumes filter_mono': "F1 \<le> F2 \<Longrightarrow> L F2 f \<subseteq> L F1 f"
    74   assumes in_filtermap_iff: 
    75     "f' \<in> L (filtermap h' F') g' \<longleftrightarrow> (\<lambda>x. f' (h' x)) \<in> L' F' (\<lambda>x. g' (h' x))"
    76   assumes filtercomap: 
    77     "f' \<in> L F'' g' \<Longrightarrow> (\<lambda>x. f' (h' x)) \<in> L' (filtercomap h' F'') (\<lambda>x. g' (h' x))"
    78   assumes sup: "f \<in> L F1 g \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L (sup F1 F2) g"
    79   assumes in_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"
    80   assumes cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> L F (f) = L F (g)"
    81   assumes cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> L F (f) = L F (g)"
    82   assumes in_cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"
    83   assumes cmult [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. c * f x) = L F (f)"
    84   assumes cmult_in_iff [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
    85   assumes mult_left [simp]: "f \<in> L F (g) \<Longrightarrow> (\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)"
    86   assumes inverse: "eventually (\<lambda>x. f x \<noteq> 0) F \<Longrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F \<Longrightarrow> 
    87                         f \<in> L F (g) \<Longrightarrow> (\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))"
    88   assumes subsetI: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"
    89   assumes plus_subset1: "f \<in> o[F](g) \<Longrightarrow> L F (g) \<subseteq> L F (\<lambda>x. f x + g x)"
    90   assumes trans: "f \<in> L F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
    91   assumes compose: "f \<in> L F (g) \<Longrightarrow> filterlim h' F G \<Longrightarrow> (\<lambda>x. f (h' x)) \<in> L' G (\<lambda>x. g (h' x))"
    92   assumes norm_iff [simp]: "(\<lambda>x. norm (f x)) \<in> Lr F (\<lambda>x. norm (g x)) \<longleftrightarrow> f \<in> L F (g)"
    93   assumes abs [simp]: "Lr Fr (\<lambda>x. \<bar>fr x\<bar>) = Lr Fr fr"
    94   assumes abs_in_iff [simp]: "(\<lambda>x. \<bar>fr x\<bar>) \<in> Lr Fr gr \<longleftrightarrow> fr \<in> Lr Fr gr"
    95 begin
    96 
    97 lemma bot [simp]: "f \<in> L bot g" by (simp add: bot')
    98   
    99 lemma filter_mono: "F1 \<le> F2 \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L F1 g"
   100   using filter_mono'[of F1 F2] by blast
   101 
   102 lemma cong_ex: 
   103   "eventually (\<lambda>x. f1 x = f2 x) F \<Longrightarrow> eventually (\<lambda>x. g1 x = g2 x) F \<Longrightarrow>
   104      f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" 
   105   by (subst cong, assumption, subst in_cong, assumption, rule refl)
   106 
   107 lemma cong_ex_bigtheta: 
   108   "f1 \<in> \<Theta>[F](f2) \<Longrightarrow> g1 \<in> \<Theta>[F](g2) \<Longrightarrow> f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" 
   109   by (subst cong_bigtheta, assumption, subst in_cong_bigtheta, assumption, rule refl)
   110 
   111 lemma bigtheta_trans1: 
   112   "f \<in> L F (g) \<Longrightarrow> g \<in> \<Theta>[F](h) \<Longrightarrow> f \<in> L F (h)"
   113   by (subst cong_bigtheta[symmetric])
   114 
   115 lemma bigtheta_trans2: 
   116   "f \<in> \<Theta>[F](g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
   117   by (subst in_cong_bigtheta)
   118    
   119 lemma cmult' [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x * c) = L F (f)"
   120   by (subst mult.commute) (rule cmult)
   121 
   122 lemma cmult_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x * c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
   123   by (subst mult.commute) (rule cmult_in_iff)
   124 
   125 lemma cdiv [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x / c) = L F (f)"
   126   using cmult'[of "inverse c" F f] by (simp add: field_simps)
   127 
   128 lemma cdiv_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
   129   using cmult_in_iff'[of "inverse c" f] by (simp add: field_simps)
   130   
   131 lemma uminus [simp]: "L F (\<lambda>x. -g x) = L F (g)" using cmult[of "-1"] by simp
   132 
   133 lemma uminus_in_iff [simp]: "(\<lambda>x. -f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
   134   using cmult_in_iff[of "-1"] by simp
   135 
   136 lemma const: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"
   137   by (subst (2) cmult[symmetric]) simp_all
   138 
   139 (* Simplifier loops without the NO_MATCH *)
   140 lemma const' [simp]: "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"
   141   by (rule const)
   142 
   143 lemma const_in_iff: "c \<noteq> 0 \<Longrightarrow> (\<lambda>_. c) \<in> L F (f) \<longleftrightarrow> (\<lambda>_. 1) \<in> L F (f)"
   144   using cmult_in_iff'[of c "\<lambda>_. 1"] by simp
   145 
   146 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)"
   147   by (rule const_in_iff)
   148 
   149 lemma plus_subset2: "g \<in> o[F](f) \<Longrightarrow> L F (f) \<subseteq> L F (\<lambda>x. f x + g x)"
   150   by (subst add.commute) (rule plus_subset1)
   151 
   152 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)"
   153   using mult_left by (simp add: mult.commute)
   154 
   155 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)"
   156   by (rule trans, erule mult_left, erule mult_right)
   157 
   158 lemma inverse_cancel:
   159   assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
   160   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
   161   shows   "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> g \<in> L F (f)"
   162 proof
   163   assume "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x))"
   164   from inverse[OF _ _ this] assms show "g \<in> L F (f)" by simp
   165 qed (intro inverse assms)
   166 
   167 lemma divide_right:
   168   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   169   assumes "f \<in> L F (g)"
   170   shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"
   171   by (subst (1 2) divide_inverse) (intro mult_right inverse assms)
   172 
   173 lemma divide_right_iff:
   174   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   175   shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> f \<in> L F (g)"
   176 proof
   177   assume "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"
   178   from mult_right[OF this, of h] assms show "f \<in> L F (g)"
   179     by (subst (asm) cong_ex[of _ f F _ g]) (auto elim!: eventually_mono)
   180 qed (simp add: divide_right assms)
   181 
   182 lemma divide_left:
   183   assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
   184   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
   185   assumes "g \<in> L F(f)"
   186   shows   "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"
   187   by (subst (1 2) divide_inverse) (intro mult_left inverse assms)
   188 
   189 lemma divide_left_iff:
   190   assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
   191   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
   192   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   193   shows   "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x) \<longleftrightarrow> g \<in> L F (f)"
   194 proof
   195   assume A: "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"
   196   from assms have B: "eventually (\<lambda>x. h x / f x / h x = inverse (f x)) F"
   197     by eventually_elim (simp add: divide_inverse)
   198   from assms have C: "eventually (\<lambda>x. h x / g x / h x = inverse (g x)) F"
   199     by eventually_elim (simp add: divide_inverse)
   200   from divide_right[OF assms(3) A] assms show "g \<in> L F (f)"
   201     by (subst (asm) cong_ex[OF B C]) (simp add: inverse_cancel)
   202 qed (simp add: divide_left assms)
   203 
   204 lemma divide:
   205   assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
   206   assumes "eventually (\<lambda>x. g2 x \<noteq> 0) F"
   207   assumes "f1 \<in> L F (f2)" "g2 \<in> L F (g1)"
   208   shows   "(\<lambda>x. f1 x / g1 x) \<in> L F (\<lambda>x. f2 x / g2 x)"
   209   by (subst (1 2) divide_inverse) (intro mult inverse assms)
   210   
   211 lemma divide_eq1:
   212   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   213   shows   "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
   214 proof-
   215   have "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x / h x) \<in> L F (\<lambda>x. g x / h x)"
   216     using assms by (intro in_cong) (auto elim: eventually_mono)
   217   thus ?thesis by (simp only: divide_right_iff assms)
   218 qed
   219 
   220 lemma divide_eq2:
   221   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   222   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)"
   223 proof-
   224   have "L F (\<lambda>x. g x) = L F (\<lambda>x. g x * h x / h x)"
   225     using assms by (intro cong) (auto elim: eventually_mono)
   226   thus ?thesis by (simp only: divide_right_iff assms)
   227 qed
   228 
   229 lemma inverse_eq1:
   230   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
   231   shows   "f \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> (\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"
   232   using divide_eq1[of g F f "\<lambda>_. 1"] by (simp add: divide_inverse assms)
   233 
   234 lemma inverse_eq2:
   235   assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
   236   shows   "(\<lambda>x. inverse (f x)) \<in> L F (g) \<longleftrightarrow> (\<lambda>x. 1) \<in> L F (\<lambda>x. f x * g x)"
   237   using divide_eq2[of f F "\<lambda>_. 1" g] by (simp add: divide_inverse assms mult_ac)
   238 
   239 lemma inverse_flip:
   240   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
   241   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
   242   assumes "(\<lambda>x. inverse (g x)) \<in> L F (h)"
   243   shows   "(\<lambda>x. inverse (h x)) \<in> L F (g)"
   244 using assms by (simp add: divide_eq1 divide_eq2 inverse_eq_divide mult.commute)
   245 
   246 lemma lift_trans:
   247   assumes "f \<in> L F (g)"
   248   assumes "(\<lambda>x. t x (g x)) \<in> L F (h)"
   249   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))"
   250   shows   "(\<lambda>x. t x (f x)) \<in> L F (h)"
   251   by (rule trans[OF assms(3)[OF assms(1)] assms(2)])
   252 
   253 lemma lift_trans':
   254   assumes "f \<in> L F (\<lambda>x. t x (g x))"
   255   assumes "g \<in> L F (h)"
   256   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))"
   257   shows   "f \<in> L F (\<lambda>x. t x (h x))"
   258   by (rule trans[OF assms(1) assms(3)[OF assms(2)]])
   259 
   260 lemma lift_trans_bigtheta:
   261   assumes "f \<in> L F (g)"
   262   assumes "(\<lambda>x. t x (g x)) \<in> \<Theta>[F](h)"
   263   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))"
   264   shows   "(\<lambda>x. t x (f x)) \<in> L F (h)"
   265   using cong_bigtheta[OF assms(2)] assms(3)[OF assms(1)] by simp
   266 
   267 lemma lift_trans_bigtheta':
   268   assumes "f \<in> L F (\<lambda>x. t x (g x))"
   269   assumes "g \<in> \<Theta>[F](h)"
   270   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))"
   271   shows   "f \<in> L F (\<lambda>x. t x (h x))"
   272   using cong_bigtheta[OF assms(3)[OF assms(2)]] assms(1)  by simp
   273 
   274 lemma (in landau_symbol) mult_in_1:
   275   assumes "f \<in> L F (\<lambda>_. 1)" "g \<in> L F (\<lambda>_. 1)"
   276   shows   "(\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"
   277   using mult[OF assms] by simp
   278 
   279 lemma (in landau_symbol) of_real_cancel:
   280   "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<Longrightarrow> f \<in> Lr F g"
   281   by (subst (asm) norm_iff [symmetric], subst (asm) (1 2) norm_of_real) simp_all
   282 
   283 lemma (in landau_symbol) of_real_iff:
   284   "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<longleftrightarrow> f \<in> Lr F g"
   285   by (subst norm_iff [symmetric], subst (1 2) norm_of_real) simp_all
   286 
   287 lemmas [landau_divide_simps] = 
   288   inverse_cancel divide_left_iff divide_eq1 divide_eq2 inverse_eq1 inverse_eq2
   289 
   290 end
   291 
   292 
   293 text {* 
   294   The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with 
   295   $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem.
   296   The following locale captures this fact.
   297 *}
   298 
   299 locale landau_pair = 
   300   fixes L l :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
   301   fixes L' l' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"
   302   fixes Lr lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"
   303   and   R :: "real \<Rightarrow> real \<Rightarrow> bool"
   304   assumes L_def: "L F g = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"
   305   and     l_def: "l F g = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"
   306   and     L'_def: "L' F' g' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"
   307   and     l'_def: "l' F' g' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"
   308   and     Lr_def: "Lr F'' g'' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"
   309   and     lr_def: "lr F'' g'' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"
   310   and     R:     "R = (\<le>) \<or> R = (\<ge>)"
   311 
   312 interpretation landau_o: 
   313     landau_pair bigo smallo bigo smallo bigo smallo "(\<le>)"
   314   by unfold_locales (auto simp: bigo_def smallo_def intro!: ext)
   315 
   316 interpretation landau_omega: 
   317     landau_pair bigomega smallomega bigomega smallomega bigomega smallomega "(\<ge>)"
   318   by unfold_locales (auto simp: bigomega_def smallomega_def intro!: ext)
   319 
   320 
   321 context landau_pair
   322 begin
   323 
   324 lemmas R_E = disjE [OF R, case_names le ge]
   325 
   326 lemma bigI:
   327   "c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F \<Longrightarrow> f \<in> L F (g)"
   328   unfolding L_def by blast
   329 
   330 lemma bigE:
   331   assumes "f \<in> L F (g)"
   332   obtains c where "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"
   333   using assms unfolding L_def by blast
   334 
   335 lemma smallI:
   336   "(\<And>c. c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F) \<Longrightarrow> f \<in> l F (g)"
   337   unfolding l_def by blast
   338 
   339 lemma smallD:
   340   "f \<in> l F (g) \<Longrightarrow> c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"
   341   unfolding l_def by blast
   342     
   343 lemma bigE_nonneg_real:
   344   assumes "f \<in> Lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F"
   345   obtains c where "c > 0" "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
   346 proof-
   347   from assms(1) obtain c where c: "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
   348     by (auto simp: Lr_def)
   349   from c(2) assms(2) have "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
   350     by eventually_elim simp
   351   from c(1) and this show ?thesis by (rule that)
   352 qed
   353 
   354 lemma smallD_nonneg_real:
   355   assumes "f \<in> lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F" "c > 0"
   356   shows   "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
   357   using assms by (auto simp: lr_def dest!: spec[of _ c] elim: eventually_elim2)
   358 
   359 lemma small_imp_big: "f \<in> l F (g) \<Longrightarrow> f \<in> L F (g)"
   360   by (rule bigI[OF _ smallD, of 1]) simp_all
   361   
   362 lemma small_subset_big: "l F (g) \<subseteq> L F (g)"
   363   using small_imp_big by blast
   364 
   365 lemma R_refl [simp]: "R x x" using R by auto
   366 
   367 lemma R_linear: "\<not>R x y \<Longrightarrow> R y x"
   368   using R by auto
   369 
   370 lemma R_trans [trans]: "R a b \<Longrightarrow> R b c \<Longrightarrow> R a c"
   371   using R by auto
   372 
   373 lemma R_mult_left_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (c*a) (c*b)"
   374   using R by (auto simp: mult_left_mono)
   375 
   376 lemma R_mult_right_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (a*c) (b*c)"
   377   using R by (auto simp: mult_right_mono)
   378 
   379 lemma big_trans:
   380   assumes "f \<in> L F (g)" "g \<in> L F (h)"
   381   shows   "f \<in> L F (h)"
   382 proof-
   383   from assms(1) guess c by (elim bigE) note c = this
   384   from assms(2) guess d by (elim bigE) note d = this
   385   from c(2) d(2) have "eventually (\<lambda>x. R (norm (f x)) (c * d * (norm (h x)))) F"
   386   proof eventually_elim
   387     fix x assume "R (norm (f x)) (c * (norm (g x)))"
   388     also assume "R (norm (g x)) (d * (norm (h x)))"
   389     with c(1) have "R (c * (norm (g x))) (c * (d * (norm (h x))))"
   390       by (intro R_mult_left_mono) simp_all
   391     finally show "R (norm (f x)) (c * d * (norm (h x)))" by (simp add: algebra_simps)
   392   qed
   393   with c(1) d(1) show ?thesis by (intro bigI[of "c*d"]) simp_all
   394 qed
   395 
   396 lemma big_small_trans:
   397   assumes "f \<in> L F (g)" "g \<in> l F (h)"
   398   shows   "f \<in> l F (h)"
   399 proof (rule smallI)
   400   fix c :: real assume c: "c > 0"
   401   from assms(1) guess d by (elim bigE) note d = this
   402   note d(2)
   403   moreover from c d assms(2) 
   404     have "eventually (\<lambda>x. R (norm (g x)) (c * inverse d * norm (h x))) F" 
   405     by (intro smallD) simp_all
   406   ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * (norm (h x)))) F"
   407     by eventually_elim (erule R_trans, insert R d(1), auto simp: field_simps)
   408 qed
   409 
   410 lemma small_big_trans:
   411   assumes "f \<in> l F (g)" "g \<in> L F (h)"
   412   shows   "f \<in> l F (h)"
   413 proof (rule smallI)
   414   fix c :: real assume c: "c > 0"
   415   from assms(2) guess d by (elim bigE) note d = this
   416   note d(2)
   417   moreover from c d assms(1) 
   418     have "eventually (\<lambda>x. R (norm (f x)) (c * inverse d * norm (g x))) F"
   419     by (intro smallD) simp_all
   420   ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * norm (h x))) F"
   421     by eventually_elim (rotate_tac 2, erule R_trans, insert R c d(1), auto simp: field_simps)
   422 qed
   423 
   424 lemma small_trans:
   425   "f \<in> l F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> l F (h)"
   426   by (rule big_small_trans[OF small_imp_big])
   427 
   428 lemma small_big_trans':
   429   "f \<in> l F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
   430   by (rule small_imp_big[OF small_big_trans])
   431 
   432 lemma big_small_trans':
   433   "f \<in> L F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> L F (h)"
   434   by (rule small_imp_big[OF big_small_trans])
   435 
   436 lemma big_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"
   437   by (intro subsetI) (drule (1) big_trans)
   438 
   439 lemma small_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> l F (f) \<subseteq> l F (g)"
   440   by (intro subsetI) (drule (1) small_big_trans)
   441 
   442 lemma big_refl [simp]: "f \<in> L F (f)"
   443   by (rule bigI[of 1]) simp_all
   444 
   445 lemma small_refl_iff: "f \<in> l F (f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
   446 proof (rule iffI[OF _ smallI])
   447   assume f: "f \<in> l F f"
   448   have "(1/2::real) > 0" "(2::real) > 0" by simp_all
   449   from smallD[OF f this(1)] smallD[OF f this(2)]
   450     show "eventually (\<lambda>x. f x = 0) F" by eventually_elim (insert R, auto)
   451 next
   452   fix c :: real assume "c > 0" "eventually (\<lambda>x. f x = 0) F"
   453   from this(2) show "eventually (\<lambda>x. R (norm (f x)) (c * norm (f x))) F"
   454     by eventually_elim simp_all
   455 qed
   456 
   457 lemma big_small_asymmetric: "f \<in> L F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
   458   by (drule (1) big_small_trans) (simp add: small_refl_iff)
   459 
   460 lemma small_big_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> L F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
   461   by (drule (1) small_big_trans) (simp add: small_refl_iff)
   462 
   463 lemma small_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
   464   by (drule (1) small_trans) (simp add: small_refl_iff)
   465 
   466 
   467 lemma plus_aux:
   468   assumes "f \<in> o[F](g)"
   469   shows "g \<in> L F (\<lambda>x. f x + g x)"
   470 proof (rule R_E)
   471   assume [simp]: "R = (\<le>)"
   472   have A: "1/2 > (0::real)" by simp
   473   {
   474     fix x assume "norm (f x) \<le> 1/2 * norm (g x)"
   475     hence "1/2 * (norm (g x)) \<le> (norm (g x)) - (norm (f x))" by simp
   476     also have "norm (g x) - norm (f x) \<le> norm (f x + g x)"
   477       by (subst add.commute) (rule norm_diff_ineq)
   478     finally have "1/2 * (norm (g x)) \<le> norm (f x + g x)" by simp
   479   } note B = this
   480   
   481   show "g \<in> L F (\<lambda>x. f x + g x)"
   482     apply (rule bigI[of "2"], simp)
   483     using landau_o.smallD[OF assms A] apply eventually_elim
   484     using B apply (simp add: algebra_simps) 
   485     done
   486 next
   487   assume [simp]: "R = (\<lambda>x y. x \<ge> y)"
   488   show "g \<in> L F (\<lambda>x. f x + g x)"
   489   proof (rule bigI[of "1/2"])
   490     show "eventually (\<lambda>x. R (norm (g x)) (1/2 * norm (f x + g x))) F"
   491       using landau_o.smallD[OF assms zero_less_one]
   492     proof eventually_elim
   493       case (elim x)
   494       have "norm (f x + g x) \<le> norm (f x) + norm (g x)" by (rule norm_triangle_ineq)
   495       also note elim
   496       finally show ?case by simp
   497     qed
   498   qed simp_all
   499 qed
   500 
   501 end
   502 
   503 
   504 
   505 lemma bigomega_iff_bigo: "g \<in> \<Omega>[F](f) \<longleftrightarrow> f \<in> O[F](g)"
   506 proof
   507   assume "f \<in> O[F](g)"
   508   then guess c by (elim landau_o.bigE)
   509   thus "g \<in> \<Omega>[F](f)" by (intro landau_omega.bigI[of "inverse c"]) (simp_all add: field_simps)
   510 next
   511   assume "g \<in> \<Omega>[F](f)"
   512   then guess c by (elim landau_omega.bigE)
   513   thus "f \<in> O[F](g)" by (intro landau_o.bigI[of "inverse c"]) (simp_all add: field_simps)
   514 qed
   515 
   516 lemma smallomega_iff_smallo: "g \<in> \<omega>[F](f) \<longleftrightarrow> f \<in> o[F](g)"
   517 proof
   518   assume "f \<in> o[F](g)"
   519   from landau_o.smallD[OF this, of "inverse c" for c]
   520     show "g \<in> \<omega>[F](f)" by (intro landau_omega.smallI) (simp_all add: field_simps)
   521 next
   522   assume "g \<in> \<omega>[F](f)"
   523   from landau_omega.smallD[OF this, of "inverse c" for c]
   524     show "f \<in> o[F](g)" by (intro landau_o.smallI) (simp_all add: field_simps)
   525 qed
   526 
   527 
   528 context landau_pair
   529 begin
   530 
   531 lemma big_mono:
   532   "eventually (\<lambda>x. R (norm (f x)) (norm (g x))) F \<Longrightarrow> f \<in> L F (g)"
   533   by (rule bigI[OF zero_less_one]) simp
   534 
   535 lemma big_mult:
   536   assumes "f1 \<in> L F (g1)" "f2 \<in> L F (g2)"
   537   shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
   538 proof-
   539   from assms(1) guess c1 by (elim bigE) note c1 = this
   540   from assms(2) guess c2 by (elim bigE) note c2 = this
   541   
   542   from c1(1) and c2(1) have "c1 * c2 > 0" by simp
   543   moreover have "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * c2 * norm (g1 x * g2 x))) F"
   544     using c1(2) c2(2)
   545   proof eventually_elim
   546     case (elim x)
   547     show ?case
   548     proof (cases rule: R_E)
   549       case le
   550       have "norm (f1 x) * norm (f2 x) \<le> (c1 * norm (g1 x)) * (c2 * norm (g2 x))"
   551         using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
   552       with le show ?thesis by (simp add: le norm_mult mult_ac)
   553     next
   554       case ge
   555       have "(c1 * norm (g1 x)) * (c2 * norm (g2 x)) \<le> norm (f1 x) * norm (f2 x)"
   556         using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
   557       with ge show ?thesis by (simp_all add: norm_mult mult_ac)
   558     qed
   559   qed
   560   ultimately show ?thesis by (rule bigI)
   561 qed
   562 
   563 lemma small_big_mult:
   564   assumes "f1 \<in> l F (g1)" "f2 \<in> L F (g2)"
   565   shows   "(\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"
   566 proof (rule smallI)
   567   fix c1 :: real assume c1: "c1 > 0"
   568   from assms(2) guess c2 by (elim bigE) note c2 = this
   569   with c1 assms(1) have "eventually (\<lambda>x. R (norm (f1 x)) (c1 * inverse c2 * norm (g1 x))) F"
   570     by (auto intro!: smallD)
   571   thus "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * norm (g1 x * g2 x))) F" using c2(2)
   572   proof eventually_elim
   573     case (elim x)
   574     show ?case
   575     proof (cases rule: R_E)
   576       case le
   577       have "norm (f1 x) * norm (f2 x) \<le> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
   578         using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
   579       with le c2(1) show ?thesis by (simp add: le norm_mult field_simps)
   580     next
   581       case ge
   582       have "norm (f1 x) * norm (f2 x) \<ge> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
   583         using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
   584       with ge c2(1) show ?thesis by (simp add: ge norm_mult field_simps)
   585     qed
   586   qed
   587 qed
   588 
   589 lemma big_small_mult: 
   590   "f1 \<in> L F (g1) \<Longrightarrow> f2 \<in> l F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"
   591   by (subst (1 2) mult.commute) (rule small_big_mult)
   592 
   593 lemma small_mult: "f1 \<in> l F (g1) \<Longrightarrow> f2 \<in> l F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"
   594   by (rule small_big_mult, assumption, rule small_imp_big)
   595 
   596 lemmas mult = big_mult small_big_mult big_small_mult small_mult
   597 
   598 
   599 sublocale big: landau_symbol L L' Lr
   600 proof
   601   have L: "L = bigo \<or> L = bigomega"
   602     by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
   603   {
   604     fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
   605     hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
   606   } note A = this
   607   {
   608     fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
   609     from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
   610       show "L F (\<lambda>x. c * f x) = L F f" by (intro equalityI big_subsetI) (simp_all add: field_simps)
   611   }
   612   {
   613     fix c :: 'b and F and f g :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
   614     from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
   615       have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
   616     thus "((\<lambda>x. c * f x) \<in> L F g) = (f \<in> L F g)" by (intro iffI) (erule (1) big_trans)+
   617   }
   618   {
   619     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> L F (g)"
   620     assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
   621     from A guess c by (elim bigE) note c = this
   622     from c(2) B have "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
   623       by eventually_elim (rule R_E, insert c(1), simp_all add: field_simps norm_inverse norm_divide)
   624     with c(1) show "(\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))" by (rule bigI)
   625   }
   626   {
   627     fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
   628     with plus_aux show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" by (blast intro!: big_subsetI) 
   629   }
   630   {
   631     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   632     show "L F (f) = L F (g)" unfolding L_def
   633       
   634       thm eventually_subst A
   635       by (subst eventually_subst'[OF A]) (rule refl)
   636   }
   637   {
   638     fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   639     show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" unfolding L_def mem_Collect_eq
   640       by (subst (1) eventually_subst'[OF A]) (rule refl)
   641   }
   642   {
   643     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)
   644   }
   645   {
   646     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
   647     with A L show "L F (f) = L F (g)" unfolding bigtheta_def
   648       by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo)
   649     fix h:: "'a \<Rightarrow> 'b"
   650     show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" by (rule disjE[OF L]) 
   651       (insert A, auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans)
   652   }
   653   {
   654     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g"
   655     thus "(\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" by (intro big_mult) simp
   656   }
   657   {
   658     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" "g \<in> L F h"
   659     thus "f \<in> L F (h)" by (rule big_trans)
   660   }
   661   {
   662     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
   663     assume "f \<in> L F g" and "filterlim h F G"
   664     thus "(\<lambda>x. f (h x)) \<in> L' G (\<lambda>x. g (h x))" by (auto simp: L_def L'_def filterlim_iff)
   665   }
   666   {
   667     fix f g :: "'a \<Rightarrow> 'b" and F G :: "'a filter"
   668     assume "f \<in> L F g" "f \<in> L G g"
   669     from this [THEN bigE] guess c1 c2 . note c12 = this
   670     define c where "c = (if R c1 c2 then c2 else c1)"
   671     from c12 have c: "R c1 c" "R c2 c" "c > 0" by (auto simp: c_def dest: R_linear)
   672     with c12(2,4) have "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
   673                      "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) G"
   674       by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+
   675     with c show "f \<in> L (sup F G) g" by (auto simp: L_def eventually_sup)
   676   }
   677   {
   678     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
   679     assume "(f \<in> L F g)"
   680     thus "((\<lambda>x. f (h x)) \<in> L' (filtercomap h F) (\<lambda>x. g (h x)))"
   681       unfolding L_def L'_def by auto
   682   }
   683 qed (auto simp: L_def Lr_def eventually_filtermap L'_def
   684           intro: filter_leD exI[of _ "1::real"])
   685 
   686 sublocale small: landau_symbol l l' lr
   687 proof
   688   {
   689     fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   690     hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
   691   } note A = this
   692   {
   693     fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   694     from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
   695       show "l F (\<lambda>x. c * f x) = l F f" 
   696         by (intro equalityI small_subsetI) (simp_all add: field_simps)
   697   }
   698   {
   699     fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   700     from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
   701       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)
   702     thus "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" by (intro iffI) (erule (1) big_small_trans)+
   703   }
   704   {
   705     fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
   706     with plus_aux show "l F g \<subseteq> l F (\<lambda>x. f x + g x)" by (blast intro!: small_subsetI) 
   707   }
   708   {
   709     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> l F (g)"
   710     assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
   711     show "(\<lambda>x. inverse (g x)) \<in> l F (\<lambda>x. inverse (f x))"
   712     proof (rule smallI)
   713       fix c :: real assume c: "c > 0"
   714       from B smallD[OF A c] 
   715         show "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
   716         by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide)
   717     qed
   718   }
   719   {
   720     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   721     show "l F (f) = l F (g)" unfolding l_def by (subst eventually_subst'[OF A]) (rule refl)
   722   }
   723   {
   724     fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   725     show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" unfolding l_def mem_Collect_eq
   726       by (subst (1) eventually_subst'[OF A]) (rule refl)
   727   }
   728   {
   729     fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" 
   730     thus "l F f \<subseteq> l F g" by (intro small_subsetI small_imp_big)
   731   }
   732   {
   733     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
   734     have L: "L = bigo \<or> L = bigomega"
   735       by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
   736     with A show "l F (f) = l F (g)" unfolding bigtheta_def
   737       by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo)
   738     have l: "l = smallo \<or> l = smallomega"
   739       by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff)
   740     fix h:: "'a \<Rightarrow> 'b"
   741     show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" by (rule disjE[OF l]) 
   742       (insert A, auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo 
   743        intro: landau_o.big_small_trans landau_o.small_big_trans)
   744   }
   745   {
   746     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g"
   747     thus "(\<lambda>x. h x * f x) \<in> l F (\<lambda>x. h x * g x)" by (intro big_small_mult) simp
   748   }
   749   {
   750     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" "g \<in> l F h"
   751     thus "f \<in> l F (h)" by (rule small_trans)
   752   }
   753   {
   754     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
   755     assume "f \<in> l F g" and "filterlim h F G"
   756     thus "(\<lambda>x. f (h x)) \<in> l' G (\<lambda>x. g (h x))"
   757       by (auto simp: l_def l'_def filterlim_iff)
   758   }
   759   {
   760     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
   761     assume "(f \<in> l F g)"
   762     thus "((\<lambda>x. f (h x)) \<in> l' (filtercomap h F) (\<lambda>x. g (h x)))"
   763       unfolding l_def l'_def by auto
   764   }
   765 qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)
   766 
   767 
   768 text {* These rules allow chaining of Landau symbol propositions in Isar with "also".*}
   769 
   770 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)"
   771   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)"
   772   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)"
   773   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)"
   774   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)"
   775   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)"
   776   by (drule (1) big.mult big_small_mult small_big_mult, simp)+
   777 
   778 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)"
   779   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)"
   780   and small_1_mult:  "f \<in> l F (g) \<Longrightarrow> h \<in> L F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"
   781   and small_1_mult': "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> l F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"
   782   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)"
   783   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)"
   784   by (drule (1) big.mult big_small_mult small_big_mult, simp)+
   785 
   786 lemmas mult_1_trans = 
   787   big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1'''
   788   big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult'''
   789 
   790 lemma big_equal_iff_bigtheta: "L F (f) = L F (g) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
   791 proof
   792   have L: "L = bigo \<or> L = bigomega"
   793     by (rule R_E) (auto simp: fun_eq_iff L_def bigo_def bigomega_def)
   794   fix f g :: "'a \<Rightarrow> 'b" assume "L F (f) = L F (g)"
   795   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
   796   thus "f \<in> \<Theta>[F](g)" using L unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
   797 qed (rule big.cong_bigtheta)
   798 
   799 lemma big_prod:
   800   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (g x)"
   801   shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>y. \<Prod>x\<in>A. g x y)"
   802   using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult)
   803 
   804 lemma big_prod_in_1:
   805   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (\<lambda>_. 1)"
   806   shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>_. 1)"
   807   using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult_in_1)
   808 
   809 end
   810 
   811 
   812 context landau_symbol
   813 begin
   814   
   815 lemma plus_absorb1:
   816   assumes "f \<in> o[F](g)"
   817   shows   "L F (\<lambda>x. f x + g x) = L F (g)"
   818 proof (intro equalityI)
   819   from plus_subset1 and assms show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" .
   820   from landau_o.small.plus_subset1[OF assms] and assms have "(\<lambda>x. -f x) \<in> o[F](\<lambda>x. f x + g x)"
   821     by (auto simp: landau_o.small.uminus_in_iff)
   822   from plus_subset1[OF this] show "L F (\<lambda>x. f x + g x) \<subseteq> L F (g)" by simp
   823 qed
   824 
   825 lemma plus_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x + g x) = L F (f)"
   826   using plus_absorb1[of g F f] by (simp add: add.commute)
   827 
   828 lemma diff_absorb1: "f \<in> o[F](g) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (g)"
   829   by (simp only: diff_conv_add_uminus plus_absorb1 landau_o.small.uminus uminus)
   830 
   831 lemma diff_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (f)"
   832   by (simp only: diff_conv_add_uminus plus_absorb2 landau_o.small.uminus_in_iff)
   833 
   834 lemmas absorb = plus_absorb1 plus_absorb2 diff_absorb1 diff_absorb2
   835 
   836 end
   837 
   838 
   839 lemma bigthetaI [intro]: "f \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> \<Theta>[F](g)"
   840   unfolding bigtheta_def bigomega_def by blast
   841 
   842 lemma bigthetaD1 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> O[F](g)" 
   843   and bigthetaD2 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g)"
   844   unfolding bigtheta_def bigo_def bigomega_def by blast+
   845 
   846 lemma bigtheta_refl [simp]: "f \<in> \<Theta>[F](f)"
   847   unfolding bigtheta_def by simp
   848 
   849 lemma bigtheta_sym: "f \<in> \<Theta>[F](g) \<longleftrightarrow> g \<in> \<Theta>[F](f)"
   850   unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
   851 
   852 lemmas landau_flip =
   853   bigomega_iff_bigo[symmetric] smallomega_iff_smallo[symmetric]
   854   bigomega_iff_bigo smallomega_iff_smallo bigtheta_sym
   855 
   856 
   857 interpretation landau_theta: landau_symbol bigtheta bigtheta bigtheta
   858 proof
   859   fix f g :: "'a \<Rightarrow> 'b" and F
   860   assume "f \<in> o[F](g)"
   861   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)"
   862     by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+
   863   thus "\<Theta>[F](g) \<subseteq> \<Theta>[F](\<lambda>x. f x + g x)" unfolding bigtheta_def by blast
   864 next
   865   fix f g :: "'a \<Rightarrow> 'b" and F 
   866   assume "f \<in> \<Theta>[F](g)"
   867   thus A: "\<Theta>[F](f) = \<Theta>[F](g)" 
   868     apply (subst (1 2) bigtheta_def)
   869     apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+
   870     apply (rule refl)
   871     done
   872   thus "\<Theta>[F](f) \<subseteq> \<Theta>[F](g)" by simp
   873   fix h :: "'a \<Rightarrow> 'b"
   874   show "f \<in> \<Theta>[F](h) \<longleftrightarrow> g \<in> \<Theta>[F](h)" by (subst (1 2) bigtheta_sym) (simp add: A)
   875 next
   876   fix f g h :: "'a \<Rightarrow> 'b" and F
   877   assume "f \<in> \<Theta>[F](g)" "g \<in> \<Theta>[F](h)"
   878   thus "f \<in> \<Theta>[F](h)" unfolding bigtheta_def
   879     by (blast intro: landau_o.big.trans landau_omega.big.trans)
   880 next
   881   fix f :: "'a \<Rightarrow> 'b" and F1 F2 :: "'a filter"
   882   assume "F1 \<le> F2"
   883   thus "\<Theta>[F2](f) \<subseteq> \<Theta>[F1](f)"
   884     by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono)
   885 qed (auto simp: bigtheta_def landau_o.big.norm_iff 
   886                 landau_o.big.cmult landau_omega.big.cmult 
   887                 landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff 
   888                 landau_o.big.in_cong landau_omega.big.in_cong
   889                 landau_o.big.mult landau_omega.big.mult
   890                 landau_o.big.inverse landau_omega.big.inverse 
   891                 landau_o.big.compose landau_omega.big.compose
   892                 landau_o.big.bot' landau_omega.big.bot'
   893                 landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff
   894                 landau_o.big.sup landau_omega.big.sup
   895                 landau_o.big.filtercomap landau_omega.big.filtercomap
   896           dest: landau_o.big.cong landau_omega.big.cong)
   897 
   898 lemmas landau_symbols = 
   899   landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms
   900   landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms 
   901   landau_theta.landau_symbol_axioms
   902 
   903 lemma bigoI [intro]:
   904   assumes "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
   905   shows   "f \<in> O[F](g)"
   906 proof (rule landau_o.bigI)
   907   show "max 1 c > 0" by simp
   908   note assms
   909   moreover have "\<And>x. c * (norm (g x)) \<le> max 1 c * (norm (g x))" by (simp add: mult_right_mono)
   910   ultimately show "eventually (\<lambda>x. (norm (f x)) \<le> max 1 c * (norm (g x))) F"
   911     by (auto elim!: eventually_mono dest: order.trans)
   912 qed
   913 
   914 lemma smallomegaD [dest]:
   915   assumes "f \<in> \<omega>[F](g)"
   916   shows   "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
   917 proof (cases "c > 0")
   918   case False
   919   show ?thesis 
   920     by (intro always_eventually allI, rule order.trans[of _ 0])
   921        (insert False, auto intro!: mult_nonpos_nonneg)
   922 qed (blast dest: landau_omega.smallD[OF assms, of c])
   923 
   924   
   925 lemma bigthetaI':
   926   assumes "c1 > 0" "c2 > 0"
   927   assumes "eventually (\<lambda>x. c1 * (norm (g x)) \<le> (norm (f x)) \<and> (norm (f x)) \<le> c2 * (norm (g x))) F"
   928   shows   "f \<in> \<Theta>[F](g)"
   929 apply (rule bigthetaI)
   930 apply (rule landau_o.bigI[OF assms(2)]) using assms(3) apply (eventually_elim, simp)
   931 apply (rule landau_omega.bigI[OF assms(1)]) using assms(3) apply (eventually_elim, simp)
   932 done
   933 
   934 lemma bigthetaI_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> \<Theta>[F](g)"
   935   by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono)
   936 
   937 lemma (in landau_symbol) ev_eq_trans1: 
   938   "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))"
   939   by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono)
   940 
   941 lemma (in landau_symbol) ev_eq_trans2: 
   942   "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)"
   943   by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono)
   944 
   945 declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro]
   946 declare landau_o.bigE landau_omega.bigE [elim]
   947 declare landau_o.smallD
   948 
   949 lemma (in landau_symbol) bigtheta_trans1': 
   950   "f \<in> L F (g) \<Longrightarrow> h \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h)"
   951   by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym)
   952 
   953 lemma (in landau_symbol) bigtheta_trans2': 
   954   "g \<in> \<Theta>[F](f) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
   955   by (rule bigtheta_trans2, subst bigtheta_sym)
   956 
   957 lemma bigo_bigomega_trans:      "f \<in> O[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> O[F](h)"
   958   and bigo_smallomega_trans:    "f \<in> O[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
   959   and smallo_bigomega_trans:    "f \<in> o[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
   960   and smallo_smallomega_trans:  "f \<in> o[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
   961   and bigomega_bigo_trans:      "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](h)"
   962   and bigomega_smallo_trans:    "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
   963   and smallomega_bigo_trans:    "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
   964   and smallomega_smallo_trans:  "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
   965   by (unfold bigomega_iff_bigo smallomega_iff_smallo)
   966      (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans 
   967                 landau_o.big_trans landau_o.small_trans)+
   968 
   969 lemmas landau_trans_lift [trans] =
   970   landau_symbols[THEN landau_symbol.lift_trans]
   971   landau_symbols[THEN landau_symbol.lift_trans']
   972   landau_symbols[THEN landau_symbol.lift_trans_bigtheta]
   973   landau_symbols[THEN landau_symbol.lift_trans_bigtheta']
   974 
   975 lemmas landau_mult_1_trans [trans] =
   976   landau_o.mult_1_trans landau_omega.mult_1_trans
   977 
   978 lemmas landau_trans [trans] = 
   979   landau_symbols[THEN landau_symbol.bigtheta_trans1]
   980   landau_symbols[THEN landau_symbol.bigtheta_trans2]
   981   landau_symbols[THEN landau_symbol.bigtheta_trans1']
   982   landau_symbols[THEN landau_symbol.bigtheta_trans2']
   983   landau_symbols[THEN landau_symbol.ev_eq_trans1]
   984   landau_symbols[THEN landau_symbol.ev_eq_trans2]
   985 
   986   landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans
   987   landau_omega.big_trans landau_omega.small_trans 
   988     landau_omega.small_big_trans landau_omega.big_small_trans
   989 
   990   bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans 
   991   bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans
   992 
   993 lemma bigtheta_inverse [simp]: 
   994   shows "(\<lambda>x. inverse (f x)) \<in> \<Theta>[F](\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
   995 proof-
   996   {
   997     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
   998     then guess c1 c2 :: real unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
   999     note c = this
  1000     from c(3) have "inverse c2 > 0" by simp
  1001     moreover from c(2,4)
  1002       have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))) F"
  1003     proof eventually_elim
  1004       fix x assume A: "(norm (f x)) \<le> c1 * (norm (g x))" "c2 * (norm (g x)) \<le> (norm (f x))"
  1005       from A c(1,3) have "f x = 0 \<longleftrightarrow> g x = 0" by (auto simp: field_simps mult_le_0_iff)
  1006       with A c(1,3) show "norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))"
  1007         by (force simp: field_simps norm_inverse norm_divide)
  1008     qed
  1009     ultimately have "(\<lambda>x. inverse (f x)) \<in> O[F](\<lambda>x. inverse (g x))" by (rule landau_o.bigI)
  1010   }
  1011   thus ?thesis unfolding bigtheta_def 
  1012     by (force simp: bigomega_iff_bigo bigtheta_sym)
  1013 qed
  1014 
  1015 lemma bigtheta_divide:
  1016   assumes "f1 \<in> \<Theta>(f2)" "g1 \<in> \<Theta>(g2)"
  1017   shows   "(\<lambda>x. f1 x / g1 x) \<in> \<Theta>(\<lambda>x. f2 x / g2 x)"
  1018   by (subst (1 2) divide_inverse, intro landau_theta.mult) (simp_all add: bigtheta_inverse assms)
  1019 
  1020 lemma eventually_nonzero_bigtheta:
  1021   assumes "f \<in> \<Theta>[F](g)"
  1022   shows   "eventually (\<lambda>x. f x \<noteq> 0) F \<longleftrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F"
  1023 proof-
  1024   {
  1025     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"
  1026     from A guess c1 c2 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
  1027     from B this(2,4) have "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim auto
  1028   }
  1029   with assms show ?thesis by (force simp: bigtheta_sym)
  1030 qed
  1031 
  1032 
  1033 subsection {* Landau symbols and limits *}
  1034 
  1035 lemma bigoI_tendsto_norm:
  1036   fixes f g
  1037   assumes "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
  1038   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  1039   shows   "f \<in> O[F](g)"
  1040 proof (rule bigoI)
  1041   from assms have "eventually (\<lambda>x. dist (norm (f x / g x)) c < 1) F" 
  1042     using tendstoD by force
  1043   thus "eventually (\<lambda>x. (norm (f x)) \<le> (norm c + 1) * (norm (g x))) F"
  1044     unfolding dist_real_def using assms(2)
  1045   proof eventually_elim
  1046     case (elim x)
  1047     have "(norm (f x)) - norm c * (norm (g x)) \<le> norm ((norm (f x)) - c * (norm (g x)))"
  1048       unfolding norm_mult [symmetric] using norm_triangle_ineq2[of "norm (f x)" "c * norm (g x)"]
  1049       by (simp add: norm_mult abs_mult)
  1050     also from elim have "\<dots> = norm (norm (g x)) * norm (norm (f x / g x) - c)"
  1051       unfolding norm_mult [symmetric] by (simp add: algebra_simps norm_divide)
  1052     also from elim have "norm (norm (f x / g x) - c) \<le> 1" by simp
  1053     hence "norm (norm (g x)) * norm (norm (f x / g x) - c) \<le> norm (norm (g x)) * 1" 
  1054       by (rule mult_left_mono) simp_all
  1055     finally show ?case by (simp add: algebra_simps)
  1056   qed
  1057 qed
  1058 
  1059 lemma bigoI_tendsto:
  1060   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
  1061   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  1062   shows   "f \<in> O[F](g)"
  1063   using assms by (rule bigoI_tendsto_norm[OF tendsto_norm])
  1064 
  1065 lemma bigomegaI_tendsto_norm:
  1066   assumes c_not_0:  "(c::real) \<noteq> 0"
  1067   assumes lim:      "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
  1068   shows   "f \<in> \<Omega>[F](g)"
  1069 proof (cases "F = bot")
  1070   case False
  1071   show ?thesis
  1072   proof (rule landau_omega.bigI)
  1073     from lim  have "c \<ge> 0" by (rule tendsto_lowerbound) (insert False, simp_all)
  1074     with c_not_0 have "c > 0" by simp
  1075     with c_not_0 show "c/2 > 0" by simp
  1076     from lim have ev: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<epsilon>) F"
  1077       by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  1078     from ev[OF `c/2 > 0`] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
  1079     proof (eventually_elim)
  1080       fix x assume B: "norm (norm (f x / g x) - c) < c / 2"
  1081       from B have g: "g x \<noteq> 0" by auto
  1082       from B have "-c/2 < -norm (norm (f x / g x) - c)" by simp
  1083       also have "... \<le> norm (f x / g x) - c" by simp
  1084       finally show "(norm (f x)) \<ge> c/2 * (norm (g x))" using g 
  1085         by (simp add: field_simps norm_mult norm_divide)
  1086     qed
  1087   qed
  1088 qed simp
  1089 
  1090 lemma bigomegaI_tendsto:
  1091   assumes c_not_0:  "(c::real) \<noteq> 0"
  1092   assumes lim:      "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
  1093   shows   "f \<in> \<Omega>[F](g)"
  1094   by (rule bigomegaI_tendsto_norm[OF _ tendsto_norm, of c]) (insert assms, simp_all)
  1095 
  1096 lemma smallomegaI_filterlim_at_top_norm:
  1097   assumes lim: "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
  1098   shows   "f \<in> \<omega>[F](g)"
  1099 proof (rule landau_omega.smallI)
  1100   fix c :: real assume c_pos: "c > 0"
  1101   from lim have ev: "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F"
  1102     by (subst (asm) filterlim_at_top) simp
  1103   thus "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
  1104   proof eventually_elim
  1105     fix x assume A: "norm (f x / g x) \<ge> c"
  1106     from A c_pos have "g x \<noteq> 0" by auto
  1107     with A show "(norm (f x)) \<ge> c * (norm (g x))" by (simp add: field_simps norm_divide)
  1108   qed
  1109 qed
  1110 
  1111 lemma smallomegaI_filterlim_at_infinity:
  1112   assumes lim: "filterlim (\<lambda>x. f x / g x) at_infinity F"
  1113   shows   "f \<in> \<omega>[F](g)"
  1114 proof (rule smallomegaI_filterlim_at_top_norm)
  1115   from lim show "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
  1116     by (rule filterlim_at_infinity_imp_norm_at_top)
  1117 qed
  1118   
  1119 lemma smallomegaD_filterlim_at_top_norm:
  1120   assumes "f \<in> \<omega>[F](g)"
  1121   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  1122   shows   "LIM x F. norm (f x / g x) :> at_top"
  1123 proof (subst filterlim_at_top_gt, clarify)
  1124   fix c :: real assume c: "c > 0"
  1125   from landau_omega.smallD[OF assms(1) this] assms(2) 
  1126     show "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F" 
  1127     by eventually_elim (simp add: field_simps norm_divide)
  1128 qed
  1129   
  1130 lemma smallomegaD_filterlim_at_infinity:
  1131   assumes "f \<in> \<omega>[F](g)"
  1132   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  1133   shows   "LIM x F. f x / g x :> at_infinity"
  1134   using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm)
  1135 
  1136 lemma smallomega_1_conv_filterlim: "f \<in> \<omega>[F](\<lambda>_. 1) \<longleftrightarrow> filterlim f at_infinity F"
  1137   by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)
  1138 
  1139 lemma smalloI_tendsto:
  1140   assumes lim: "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
  1141   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  1142   shows   "f \<in> o[F](g)"
  1143 proof (rule landau_o.smallI)
  1144   fix c :: real assume c_pos: "c > 0"
  1145   from c_pos and lim have ev: "eventually (\<lambda>x. norm (f x / g x) < c) F"
  1146     by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  1147   with assms(2) show "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
  1148     by eventually_elim (simp add: field_simps norm_divide)
  1149 qed
  1150 
  1151 lemma smalloD_tendsto:
  1152   assumes "f \<in> o[F](g)"
  1153   shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
  1154 unfolding tendsto_iff
  1155 proof clarify
  1156   fix e :: real assume e: "e > 0"
  1157   hence "e/2 > 0" by simp
  1158   from landau_o.smallD[OF assms this] show "eventually (\<lambda>x. dist (f x / g x) 0 < e) F"
  1159   proof eventually_elim
  1160     fix x assume "(norm (f x)) \<le> e/2 * (norm (g x))"
  1161     with e have "dist (f x / g x) 0 \<le> e/2"
  1162       by (cases "g x = 0") (simp_all add: dist_real_def norm_divide field_simps)
  1163     also from e have "... < e" by simp
  1164     finally show "dist (f x / g x) 0 < e" by simp
  1165   qed
  1166 qed
  1167 
  1168 lemma bigthetaI_tendsto_norm:
  1169   assumes c_not_0: "(c::real) \<noteq> 0"
  1170   assumes lim:     "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
  1171   shows   "f \<in> \<Theta>[F](g)"
  1172 proof (rule bigthetaI)
  1173   from c_not_0 have "\<bar>c\<bar> > 0" by simp
  1174   with lim have "eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<bar>c\<bar>) F"
  1175     by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  1176   hence g: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim (auto simp add: field_simps)
  1177 
  1178   from lim g show "f \<in> O[F](g)" by (rule bigoI_tendsto_norm)
  1179   from c_not_0 and lim show "f \<in> \<Omega>[F](g)" by (rule bigomegaI_tendsto_norm)
  1180 qed
  1181 
  1182 lemma bigthetaI_tendsto:
  1183   assumes c_not_0: "(c::real) \<noteq> 0"
  1184   assumes lim:     "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
  1185   shows   "f \<in> \<Theta>[F](g)"
  1186   using assms by (intro bigthetaI_tendsto_norm[OF _ tendsto_norm, of "c"]) simp_all
  1187 
  1188 lemma tendsto_add_smallo:
  1189   assumes "(f1 \<longlongrightarrow> a) F"
  1190   assumes "f2 \<in> o[F](f1)"
  1191   shows   "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
  1192 proof (subst filterlim_cong[OF refl refl])
  1193   from landau_o.smallD[OF assms(2) zero_less_one] 
  1194     have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)) F" by simp
  1195   thus "eventually (\<lambda>x. f1 x + f2 x = f1 x * (1 + f2 x / f1 x)) F"
  1196     by eventually_elim (auto simp: field_simps)
  1197 next
  1198   from assms(1) show "((\<lambda>x. f1 x * (1 + f2 x / f1 x)) \<longlongrightarrow> a) F"
  1199     by (force intro: tendsto_eq_intros smalloD_tendsto[OF assms(2)])
  1200 qed
  1201 
  1202 lemma tendsto_diff_smallo:
  1203   shows "(f1 \<longlongrightarrow> a) F \<Longrightarrow> f2 \<in> o[F](f1) \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
  1204   using tendsto_add_smallo[of f1 a F "\<lambda>x. -f2 x"] by simp
  1205 
  1206 lemma tendsto_add_smallo_iff:
  1207   assumes "f2 \<in> o[F](f1)"
  1208   shows   "(f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
  1209 proof
  1210   assume "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
  1211   hence "((\<lambda>x. f1 x + f2 x - f2 x) \<longlongrightarrow> a) F"
  1212     by (rule tendsto_diff_smallo) (simp add: landau_o.small.plus_absorb2 assms)
  1213   thus "(f1 \<longlongrightarrow> a) F" by simp
  1214 qed (rule tendsto_add_smallo[OF _ assms])
  1215 
  1216 lemma tendsto_diff_smallo_iff:
  1217   shows "f2 \<in> o[F](f1) \<Longrightarrow> (f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
  1218   using tendsto_add_smallo_iff[of "\<lambda>x. -f2 x" F f1 a] by simp
  1219 
  1220 lemma tendsto_divide_smallo:
  1221   assumes "((\<lambda>x. f1 x / g1 x) \<longlongrightarrow> a) F"
  1222   assumes "f2 \<in> o[F](f1)" "g2 \<in> o[F](g1)"
  1223   assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
  1224   shows   "((\<lambda>x. (f1 x + f2 x) / (g1 x + g2 x)) \<longlongrightarrow> a) F" (is "(?f \<longlongrightarrow> _) _")
  1225 proof (subst tendsto_cong)
  1226   let ?f' = "\<lambda>x. (f1 x / g1 x) * (1 + f2 x / f1 x) / (1 + g2 x / g1 x)"
  1227 
  1228   have "(?f' \<longlongrightarrow> a * (1 + 0) / (1 + 0)) F"
  1229   by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const 
  1230         smalloD_tendsto[OF assms(2)] smalloD_tendsto[OF assms(3)])+ simp_all
  1231   thus "(?f' \<longlongrightarrow> a) F" by simp
  1232 
  1233   have "(1/2::real) > 0" by simp
  1234   from landau_o.smallD[OF assms(2) this] landau_o.smallD[OF assms(3) this]
  1235     have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)/2) F"
  1236          "eventually (\<lambda>x. norm (g2 x) \<le> norm (g1 x)/2) F" by simp_all
  1237   with assms(4) show "eventually (\<lambda>x. ?f x = ?f' x) F"
  1238   proof eventually_elim
  1239     fix x assume A: "norm (f2 x) \<le> norm (f1 x)/2" and 
  1240                  B: "norm (g2 x) \<le> norm (g1 x)/2" and C: "g1 x \<noteq> 0"
  1241     show "?f x = ?f' x"
  1242     proof (cases "f1 x = 0")
  1243       assume D: "f1 x \<noteq> 0"
  1244       from D have "f1 x + f2 x = f1 x * (1 + f2 x/f1 x)" by (simp add: field_simps)
  1245       moreover from C have "g1 x + g2 x = g1 x * (1 + g2 x/g1 x)" by (simp add: field_simps)
  1246       ultimately have "?f x = (f1 x * (1 + f2 x/f1 x)) / (g1 x * (1 + g2 x/g1 x))" by (simp only:)
  1247       also have "... = ?f' x" by simp
  1248       finally show ?thesis .
  1249     qed (insert A, simp)
  1250   qed
  1251 qed
  1252 
  1253 
  1254 lemma bigo_powr:
  1255   fixes f :: "'a \<Rightarrow> real"
  1256   assumes "f \<in> O[F](g)" "p \<ge> 0"
  1257   shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)"
  1258 proof-
  1259   from assms(1) guess c by (elim landau_o.bigE landau_omega.bigE IntE)
  1260   note c = this
  1261   from c(2) assms(2) have "eventually (\<lambda>x. (norm (f x)) powr p \<le> (c * (norm (g x))) powr p) F"
  1262     by (auto elim!: eventually_mono intro!: powr_mono2)
  1263   thus "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" using c(1)
  1264     by (intro bigoI[of _ "c powr p"]) (simp_all add: powr_mult)
  1265 qed
  1266 
  1267 lemma smallo_powr:
  1268   fixes f :: "'a \<Rightarrow> real"
  1269   assumes "f \<in> o[F](g)" "p > 0"
  1270   shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)"
  1271 proof (rule landau_o.smallI)
  1272   fix c :: real assume c: "c > 0"
  1273   hence "c powr (1/p) > 0" by simp
  1274   from landau_o.smallD[OF assms(1) this] 
  1275   show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F"
  1276   proof eventually_elim
  1277     fix x assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))"
  1278     with assms(2) have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p"
  1279       by (intro powr_mono2) simp_all
  1280     also from assms(2) c have "... = c * (norm (g x)) powr p"
  1281       by (simp add: field_simps powr_mult powr_powr)
  1282     finally show "norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)" by simp
  1283   qed
  1284 qed
  1285 
  1286 lemma smallo_powr_nonneg:
  1287   fixes f :: "'a \<Rightarrow> real"
  1288   assumes "f \<in> o[F](g)" "p > 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
  1289   shows   "(\<lambda>x. f x powr p) \<in> o[F](\<lambda>x. g x powr p)"
  1290 proof -
  1291   from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
  1292     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1293   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+
  1294   also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
  1295     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1296   finally show ?thesis .
  1297 qed
  1298 
  1299 lemma bigtheta_powr:
  1300   fixes f :: "'a \<Rightarrow> real"
  1301   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)"
  1302 apply (cases "p < 0")
  1303 apply (subst bigtheta_inverse[symmetric], subst (1 2) powr_minus[symmetric])
  1304 unfolding bigtheta_def apply (auto simp: bigomega_iff_bigo intro!: bigo_powr)
  1305 done
  1306 
  1307 lemma bigo_powr_nonneg:
  1308   fixes f :: "'a \<Rightarrow> real"
  1309   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"
  1310   shows   "(\<lambda>x. f x powr p) \<in> O[F](\<lambda>x. g x powr p)"
  1311 proof -
  1312   from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
  1313     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1314   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+
  1315   also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
  1316     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1317   finally show ?thesis .
  1318 qed
  1319 
  1320 lemma zero_in_smallo [simp]: "(\<lambda>_. 0) \<in> o[F](f)"
  1321   by (intro landau_o.smallI) simp_all
  1322 
  1323 lemma zero_in_bigo [simp]: "(\<lambda>_. 0) \<in> O[F](f)"
  1324   by (intro landau_o.bigI[of 1]) simp_all
  1325 
  1326 lemma in_bigomega_zero [simp]: "f \<in> \<Omega>[F](\<lambda>x. 0)"
  1327   by (rule landau_omega.bigI[of 1]) simp_all
  1328 
  1329 lemma in_smallomega_zero [simp]: "f \<in> \<omega>[F](\<lambda>x. 0)"
  1330   by (simp add: smallomega_iff_smallo)
  1331 
  1332 
  1333 lemma in_smallo_zero_iff [simp]: "f \<in> o[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1334 proof
  1335   assume "f \<in> o[F](\<lambda>_. 0)"
  1336   from landau_o.smallD[OF this, of 1] show "eventually (\<lambda>x. f x = 0) F" by simp
  1337 next
  1338   assume "eventually (\<lambda>x. f x = 0) F"
  1339   hence "\<forall>c>0. eventually (\<lambda>x. (norm (f x)) \<le> c * \<bar>0\<bar>) F" by simp
  1340   thus "f \<in> o[F](\<lambda>_. 0)" unfolding smallo_def by simp
  1341 qed
  1342 
  1343 lemma in_bigo_zero_iff [simp]: "f \<in> O[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1344 proof
  1345   assume "f \<in> O[F](\<lambda>_. 0)"
  1346   thus "eventually (\<lambda>x. f x = 0) F" by (elim landau_o.bigE) simp
  1347 next
  1348   assume "eventually (\<lambda>x. f x = 0) F"
  1349   hence "eventually (\<lambda>x. (norm (f x)) \<le> 1 * \<bar>0\<bar>) F" by simp
  1350   thus "f \<in> O[F](\<lambda>_. 0)" by (intro landau_o.bigI[of 1]) simp_all
  1351 qed
  1352 
  1353 lemma zero_in_smallomega_iff [simp]: "(\<lambda>_. 0) \<in> \<omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1354   by (simp add: smallomega_iff_smallo)
  1355 
  1356 lemma zero_in_bigomega_iff [simp]: "(\<lambda>_. 0) \<in> \<Omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1357   by (simp add: bigomega_iff_bigo)
  1358 
  1359 lemma zero_in_bigtheta_iff [simp]: "(\<lambda>_. 0) \<in> \<Theta>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1360   unfolding bigtheta_def by simp
  1361 
  1362 lemma in_bigtheta_zero_iff [simp]: "f \<in> \<Theta>[F](\<lambda>x. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1363   unfolding bigtheta_def by simp
  1364 
  1365 
  1366 lemma cmult_in_bigo_iff    [simp]:  "(\<lambda>x. c * f x) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
  1367   and cmult_in_bigo_iff'   [simp]:  "(\<lambda>x. f x * c) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
  1368   and cmult_in_smallo_iff  [simp]:  "(\<lambda>x. c * f x) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
  1369   and cmult_in_smallo_iff' [simp]: "(\<lambda>x. f x * c) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
  1370   by (cases "c = 0", simp, simp)+
  1371 
  1372 lemma bigo_const [simp]: "(\<lambda>_. c) \<in> O[F](\<lambda>_. 1)" by (rule bigoI[of _ "norm c"]) simp
  1373 
  1374 lemma bigo_const_iff [simp]: "(\<lambda>_. c1) \<in> O[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 = 0 \<or> c2 \<noteq> 0"
  1375   by (cases "c1 = 0"; cases "c2 = 0")
  1376      (auto simp: bigo_def eventually_False intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
  1377 
  1378 lemma bigomega_const_iff [simp]: "(\<lambda>_. c1) \<in> \<Omega>[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 \<noteq> 0 \<or> c2 = 0"
  1379   by (cases "c1 = 0"; cases "c2 = 0")
  1380      (auto simp: bigomega_def eventually_False mult_le_0_iff 
  1381            intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
  1382 
  1383 lemma smallo_real_nat_transfer:
  1384   "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))"
  1385   by (rule landau_o.small.compose[OF _ filterlim_real_sequentially])
  1386 
  1387 lemma bigo_real_nat_transfer:
  1388   "(f :: real \<Rightarrow> real) \<in> O(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> O(\<lambda>x. g (real x))"
  1389   by (rule landau_o.big.compose[OF _ filterlim_real_sequentially])
  1390 
  1391 lemma smallomega_real_nat_transfer:
  1392   "(f :: real \<Rightarrow> real) \<in> \<omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<omega>(\<lambda>x. g (real x))"
  1393   by (rule landau_omega.small.compose[OF _ filterlim_real_sequentially])
  1394 
  1395 lemma bigomega_real_nat_transfer:
  1396   "(f :: real \<Rightarrow> real) \<in> \<Omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Omega>(\<lambda>x. g (real x))"
  1397   by (rule landau_omega.big.compose[OF _ filterlim_real_sequentially])
  1398 
  1399 lemma bigtheta_real_nat_transfer:
  1400   "(f :: real \<Rightarrow> real) \<in> \<Theta>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Theta>(\<lambda>x. g (real x))"
  1401   unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast
  1402 
  1403 lemmas landau_real_nat_transfer [intro] = 
  1404   bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer 
  1405   smallomega_real_nat_transfer bigtheta_real_nat_transfer
  1406 
  1407 
  1408 lemma landau_symbol_if_at_top_eq [simp]:
  1409   assumes "landau_symbol L L' Lr"
  1410   shows   "L at_top (\<lambda>x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)"
  1411 apply (rule landau_symbol.cong[OF assms])
  1412 using less_add_one[of a] apply (auto intro: eventually_mono  eventually_ge_at_top[of "a + 1"])
  1413 done
  1414 
  1415 lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq]
  1416 
  1417 
  1418 
  1419 lemma sum_in_smallo:
  1420   assumes "f \<in> o[F](h)" "g \<in> o[F](h)"
  1421   shows   "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)"
  1422 proof-
  1423   {
  1424     fix f g assume fg: "f \<in> o[F](h)" "g \<in> o[F](h)"
  1425     have "(\<lambda>x. f x + g x) \<in> o[F](h)"
  1426     proof (rule landau_o.smallI)
  1427       fix c :: real assume "c > 0"
  1428       hence "c/2 > 0" by simp
  1429       from fg[THEN landau_o.smallD[OF _ this]]
  1430       show "eventually (\<lambda>x. norm (f x + g x) \<le> c * (norm (h x))) F"
  1431         by eventually_elim (auto intro: order.trans[OF norm_triangle_ineq])
  1432     qed
  1433   }
  1434   from this[of f g] this[of f "\<lambda>x. -g x"] assms
  1435     show "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" by simp_all
  1436 qed
  1437 
  1438 lemma big_sum_in_smallo:
  1439   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> o[F](g)"
  1440   shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> o[F](g)"
  1441   using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_smallo)
  1442 
  1443 lemma sum_in_bigo:
  1444   assumes "f \<in> O[F](h)" "g \<in> O[F](h)"
  1445   shows   "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)"
  1446 proof-
  1447   {
  1448     fix f g assume fg: "f \<in> O[F](h)" "g \<in> O[F](h)"
  1449     from fg(1) guess c1 by (elim landau_o.bigE) note c1 = this
  1450     from fg(2) guess c2 by (elim landau_o.bigE) note c2 = this
  1451     from c1(2) c2(2) have "eventually (\<lambda>x. norm (f x + g x) \<le> (c1 + c2) * (norm (h x))) F"
  1452       by eventually_elim (auto simp: algebra_simps intro: order.trans[OF norm_triangle_ineq])
  1453     hence "(\<lambda>x. f x + g x) \<in> O[F](h)" by (rule bigoI)
  1454   }
  1455   from this[of f g] this[of f "\<lambda>x. -g x"] assms
  1456     show "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" by simp_all
  1457 qed
  1458 
  1459 lemma big_sum_in_bigo:
  1460   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> O[F](g)"
  1461   shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"
  1462   using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)
  1463 
  1464 context landau_symbol
  1465 begin
  1466 
  1467 lemma mult_cancel_left:
  1468   assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
  1469   notes   [trans] = bigtheta_trans1 bigtheta_trans2
  1470   shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f2 \<in> L F (g2)"
  1471 proof
  1472   assume A: "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
  1473   from assms have nz: "eventually (\<lambda>x. f1 x \<noteq> 0) F" by (simp add: eventually_nonzero_bigtheta)
  1474   hence "f2 \<in> \<Theta>[F](\<lambda>x. f1 x * f2 x / f1 x)"
  1475     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1476   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)" 
  1477     by (intro divide_right) simp_all
  1478   also from assms nz have "(\<lambda>x. g1 x * g2 x / f1 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x / g1 x)"
  1479     by (intro landau_theta.mult landau_theta.divide) (simp_all add: bigtheta_sym)
  1480   also from assms have "(\<lambda>x. g1 x * g2 x / g1 x) \<in> \<Theta>[F](g2)"
  1481     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1482   finally show "f2 \<in> L F (g2)" .
  1483 next
  1484   assume "f2 \<in> L F (g2)"
  1485   hence "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. f1 x * g2 x)" by (rule mult_left)
  1486   also have "(\<lambda>x. f1 x * g2 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x)"
  1487     by (intro landau_theta.mult_right assms)
  1488   finally show "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" .
  1489 qed
  1490 
  1491 lemma mult_cancel_right:
  1492   assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
  1493   shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
  1494   by (subst (1 2) mult.commute) (rule mult_cancel_left[OF assms])
  1495 
  1496 lemma divide_cancel_right:
  1497   assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
  1498   shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
  1499   by (subst (1 2) divide_inverse, intro mult_cancel_right bigtheta_inverse) (simp_all add: assms)
  1500 
  1501 lemma divide_cancel_left:
  1502   assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
  1503   shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> 
  1504              (\<lambda>x. inverse (f2 x)) \<in> L F (\<lambda>x. inverse (g2 x))"
  1505   by (simp only: divide_inverse mult_cancel_left[OF assms])
  1506 
  1507 end
  1508 
  1509 
  1510 lemma powr_smallo_iff:
  1511   assumes "filterlim g at_top F" "F \<noteq> bot"
  1512   shows   "(\<lambda>x. g x powr p :: real) \<in> o[F](\<lambda>x. g x powr q) \<longleftrightarrow> p < q"
  1513 proof-
  1514   from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
  1515   hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
  1516   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)"
  1517   proof
  1518     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)"
  1519     from landau_o.big_small_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
  1520     with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
  1521     thus False by (simp add: eventually_False assms)
  1522   qed
  1523   show ?thesis
  1524   proof (cases p q rule: linorder_cases)
  1525     assume "p < q"
  1526     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
  1527       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
  1528     with `p < q` show ?thesis by auto
  1529   next
  1530     assume "p = q"
  1531     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
  1532     with B `p = q` show ?thesis by auto
  1533   next
  1534     assume "p > q"
  1535     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
  1536       by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)
  1537     with B `p > q` show ?thesis by auto
  1538   qed
  1539 qed
  1540 
  1541 lemma powr_bigo_iff:
  1542   assumes "filterlim g at_top F" "F \<noteq> bot"
  1543   shows   "(\<lambda>x. g x powr p :: real) \<in> O[F](\<lambda>x. g x powr q) \<longleftrightarrow> p \<le> q"
  1544 proof-
  1545   from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
  1546   hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
  1547   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)"
  1548   proof
  1549     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)"
  1550     from landau_o.small_big_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
  1551     with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
  1552     thus False by (simp add: eventually_False assms)
  1553   qed
  1554   show ?thesis
  1555   proof (cases p q rule: linorder_cases)
  1556     assume "p < q"
  1557     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
  1558       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
  1559     with `p < q` show ?thesis by (auto intro: landau_o.small_imp_big)
  1560   next
  1561     assume "p = q"
  1562     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
  1563     with B `p = q` show ?thesis by auto
  1564   next
  1565     assume "p > q"
  1566     hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
  1567       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
  1568     with B `p > q` show ?thesis by (auto intro: landau_o.small_imp_big)
  1569   qed
  1570 qed
  1571 
  1572 lemma powr_bigtheta_iff: 
  1573   assumes "filterlim g at_top F" "F \<noteq> bot"
  1574   shows   "(\<lambda>x. g x powr p :: real) \<in> \<Theta>[F](\<lambda>x. g x powr q) \<longleftrightarrow> p = q"
  1575   using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff)
  1576 
  1577 
  1578 subsection \<open>Flatness of real functions\<close>
  1579 
  1580 text \<open>
  1581   Given two real-valued functions $f$ and $g$, we say that $f$ is flatter than $g$ if
  1582   any power of $f(x)$ is asymptotically dominated by any positive power of $g(x)$. This is
  1583   a useful notion since, given two products of powers of functions sorted by flatness, we can
  1584   compare them asymptotically by simply comparing the exponent lists lexicographically.
  1585 
  1586   A simple sufficient criterion for flatness it that $\ln f(x) \in o(\ln g(x))$, which we show
  1587   now.
  1588 \<close>
  1589 lemma ln_smallo_imp_flat:
  1590   fixes f g :: "real \<Rightarrow> real"
  1591   assumes lim_f: "filterlim f at_top at_top"
  1592   assumes lim_g: "filterlim g at_top at_top"
  1593   assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
  1594   assumes q: "q > 0"
  1595   shows   "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)"
  1596 proof (rule smalloI_tendsto)
  1597   from lim_f have "eventually (\<lambda>x. f x > 0) at_top" 
  1598     by (simp add: filterlim_at_top_dense)
  1599   hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp
  1600   
  1601   from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top"
  1602     by (simp add: filterlim_at_top_dense)
  1603   hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp
  1604   thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top"
  1605     by eventually_elim simp
  1606   
  1607   have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) = 
  1608                           p * ln (f x) - q * ln (g x)) at_top"
  1609     using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps)
  1610   have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top"
  1611     by (insert q)
  1612        (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult
  1613               tendsto_const tendsto_diff smalloD_tendsto[OF ln_o_ln] lim_g
  1614               filterlim_compose[OF ln_at_top] | simp)+
  1615   hence "filterlim (\<lambda>x. p * ln (f x) - q * ln (g x)) at_bot at_top"
  1616     by (subst (asm) filterlim_cong[OF refl refl eq])
  1617   hence *: "((\<lambda>x. exp (p * ln (f x) - q * ln (g x))) \<longlongrightarrow> 0) at_top"
  1618     by (rule filterlim_compose[OF exp_at_bot])
  1619   have eq: "eventually (\<lambda>x. exp (p * ln (f x) - q * ln (g x)) = f x powr p / g x powr q) at_top"
  1620     using f_nz g_nz by eventually_elim (simp add: powr_def exp_diff)
  1621   show "((\<lambda>x. f x powr p / g x powr q) \<longlongrightarrow> 0) at_top"
  1622     using * by (subst (asm) filterlim_cong[OF refl refl eq])
  1623 qed
  1624 
  1625 lemma ln_smallo_imp_flat':
  1626   fixes f g :: "real \<Rightarrow> real"
  1627   assumes lim_f: "filterlim f at_top at_top"
  1628   assumes lim_g: "filterlim g at_top at_top"
  1629   assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
  1630   assumes q: "q < 0"
  1631   shows   "(\<lambda>x. g x powr q) \<in> o(\<lambda>x. f x powr p)"
  1632 proof -
  1633   from lim_f lim_g have "eventually (\<lambda>x. f x > 0) at_top" "eventually (\<lambda>x. g x > 0) at_top"
  1634     by (simp_all add: filterlim_at_top_dense)
  1635   hence "eventually (\<lambda>x. f x \<noteq> 0) at_top" "eventually (\<lambda>x. g x \<noteq> 0) at_top"
  1636     by (auto elim: eventually_mono)
  1637   moreover from assms have "(\<lambda>x. f x powr -p) \<in> o(\<lambda>x. g x powr -q)"
  1638     by (intro ln_smallo_imp_flat assms) simp_all
  1639   ultimately show ?thesis unfolding powr_minus
  1640     by (simp add: landau_o.small.inverse_cancel)
  1641 qed
  1642 
  1643 
  1644 subsection \<open>Asymptotic Equivalence\<close>
  1645 
  1646 (* TODO Move *)
  1647 lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
  1648   by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
  1649 
  1650 named_theorems asymp_equiv_intros
  1651 named_theorems asymp_equiv_simps
  1652 
  1653 definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  1654   ("_ \<sim>[_] _" [51, 10, 51] 50)
  1655   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"
  1656 
  1657 abbreviation (input) asymp_equiv_at_top where
  1658   "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"
  1659 
  1660 bundle asymp_equiv_notation
  1661 begin
  1662 notation asymp_equiv_at_top (infix "\<sim>" 50) 
  1663 end
  1664 
  1665 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"
  1666   by (simp add: asymp_equiv_def)
  1667 
  1668 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"
  1669   by (simp add: asymp_equiv_def)
  1670 
  1671 lemma asymp_equiv_filtermap_iff:
  1672   "f \<sim>[filtermap h F] g \<longleftrightarrow> (\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
  1673   by (simp add: asymp_equiv_def filterlim_filtermap)
  1674 
  1675 lemma asymp_equiv_refl [simp, asymp_equiv_intros]: "f \<sim>[F] f"
  1676 proof (intro asymp_equivI)
  1677   have "eventually (\<lambda>x. 1 = (if f x = 0 \<and> f x = 0 then 1 else f x / f x)) F"
  1678     by (intro always_eventually) simp
  1679   moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
  1680   ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
  1681     by (rule Lim_transform_eventually)
  1682 qed
  1683 
  1684 lemma asymp_equiv_symI: 
  1685   assumes "f \<sim>[F] g"
  1686   shows   "g \<sim>[F] f"
  1687   using tendsto_inverse[OF asymp_equivD[OF assms]]
  1688   by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong)
  1689 
  1690 lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f"
  1691   by (blast intro: asymp_equiv_symI)
  1692 
  1693 lemma asymp_equivI': 
  1694   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
  1695   shows   "f \<sim>[F] g"
  1696 proof (cases "F = bot")
  1697   case False
  1698   have "eventually (\<lambda>x. f x \<noteq> 0) F"
  1699   proof (rule ccontr)
  1700     assume "\<not>eventually (\<lambda>x. f x \<noteq> 0) F"
  1701     hence "frequently (\<lambda>x. f x = 0) F" by (simp add: frequently_def)
  1702     hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1)
  1703     from limit_frequently_eq[OF False this assms] show False by simp_all
  1704   qed
  1705   hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"
  1706     by eventually_elim simp
  1707   from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def 
  1708     by (rule Lim_transform_eventually)
  1709 qed (simp_all add: asymp_equiv_def)
  1710 
  1711 
  1712 lemma asymp_equiv_cong:
  1713   assumes "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
  1714   shows   "f1 \<sim>[F] g1 \<longleftrightarrow> f2 \<sim>[F] g2"
  1715   unfolding asymp_equiv_def
  1716 proof (rule tendsto_cong, goal_cases)
  1717   case 1
  1718   from assms show ?case by eventually_elim simp
  1719 qed
  1720 
  1721 lemma asymp_equiv_eventually_zeros:
  1722   fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
  1723   assumes "f \<sim>[F] g"
  1724   shows   "eventually (\<lambda>x. f x = 0 \<longleftrightarrow> g x = 0) F"
  1725 proof -
  1726   let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  1727   have "eventually (\<lambda>x. x \<noteq> 0) (nhds (1::'b))"
  1728     by (rule t1_space_nhds) auto
  1729   hence "eventually (\<lambda>x. x \<noteq> 0) (filtermap ?h F)"
  1730     using assms unfolding asymp_equiv_def filterlim_def
  1731     by (rule filter_leD [rotated])
  1732   hence "eventually (\<lambda>x. ?h x \<noteq> 0) F" by (simp add: eventually_filtermap)
  1733   thus ?thesis by eventually_elim (auto split: if_splits)
  1734 qed
  1735 
  1736 lemma asymp_equiv_transfer:
  1737   assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
  1738   shows   "f2 \<sim>[F] g2"
  1739   using assms(1) asymp_equiv_cong[OF assms(2,3)] by simp
  1740 
  1741 lemma asymp_equiv_transfer_trans [trans]:
  1742   assumes "(\<lambda>x. f x (h1 x)) \<sim>[F] (\<lambda>x. g x (h1 x))"
  1743   assumes "eventually (\<lambda>x. h1 x = h2 x) F"
  1744   shows   "(\<lambda>x. f x (h2 x)) \<sim>[F] (\<lambda>x. g x (h2 x))"
  1745   by (rule asymp_equiv_transfer[OF assms(1)]) (insert assms(2), auto elim!: eventually_mono)
  1746 
  1747 lemma asymp_equiv_trans [trans]:
  1748   fixes f g h
  1749   assumes "f \<sim>[F] g" "g \<sim>[F] h"
  1750   shows   "f \<sim>[F] h"
  1751 proof -
  1752   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  1753   from assms[THEN asymp_equiv_eventually_zeros]
  1754     have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
  1755   moreover from tendsto_mult[OF assms[THEN asymp_equivD]] 
  1756     have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
  1757   ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
  1758 qed
  1759 
  1760 lemma asymp_equiv_trans_lift1 [trans]:
  1761   assumes "a \<sim>[F] f b" "b \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
  1762   shows   "a \<sim>[F] f c"
  1763   using assms by (blast intro: asymp_equiv_trans)
  1764 
  1765 lemma asymp_equiv_trans_lift2 [trans]:
  1766   assumes "f a \<sim>[F] b" "a \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
  1767   shows   "f c \<sim>[F] b"
  1768   using asymp_equiv_symI[OF assms(3)[OF assms(2)]] assms(1)
  1769   by (blast intro: asymp_equiv_trans)
  1770 
  1771 lemma asymp_equivD_const:
  1772   assumes "f \<sim>[F] (\<lambda>_. c)"
  1773   shows   "(f \<longlongrightarrow> c) F"
  1774 proof (cases "c = 0")
  1775   case False
  1776   with tendsto_mult_right[OF asymp_equivD[OF assms], of c] show ?thesis by simp
  1777 next
  1778   case True
  1779   with asymp_equiv_eventually_zeros[OF assms] show ?thesis
  1780     by (simp add: Lim_eventually)
  1781 qed
  1782 
  1783 lemma asymp_equiv_refl_ev:
  1784   assumes "eventually (\<lambda>x. f x = g x) F"
  1785   shows   "f \<sim>[F] g"
  1786   by (intro asymp_equivI Lim_eventually)
  1787      (insert assms, auto elim!: eventually_mono)
  1788 
  1789 lemma asymp_equiv_sandwich:
  1790   fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"
  1791   assumes "eventually (\<lambda>x. f x \<ge> 0) F"
  1792   assumes "eventually (\<lambda>x. f x \<le> g x) F"
  1793   assumes "eventually (\<lambda>x. g x \<le> h x) F"
  1794   assumes "f \<sim>[F] h"
  1795   shows   "g \<sim>[F] f" "g \<sim>[F] h"
  1796 proof -
  1797   show "g \<sim>[F] f"
  1798   proof (rule asymp_equivI, rule tendsto_sandwich)
  1799     from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
  1800       show "eventually (\<lambda>n. (if h n = 0 \<and> f n = 0 then 1 else h n / f n) \<ge>
  1801                               (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
  1802         by eventually_elim (auto intro!: divide_right_mono)
  1803     from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
  1804       show "eventually (\<lambda>n. 1 \<le>
  1805                               (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
  1806         by eventually_elim (auto intro!: divide_right_mono)
  1807   qed (insert asymp_equiv_symI[OF assms(4)], simp_all add: asymp_equiv_def)
  1808   also note \<open>f \<sim>[F] h\<close>
  1809   finally show "g \<sim>[F] h" .
  1810 qed
  1811 
  1812 lemma asymp_equiv_imp_eventually_same_sign:
  1813   fixes f g :: "real \<Rightarrow> real"
  1814   assumes "f \<sim>[F] g"
  1815   shows   "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
  1816 proof -
  1817   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"
  1818     unfolding asymp_equiv_def by (rule tendsto_sgn) simp_all
  1819   from order_tendstoD(1)[OF this, of "1/2"]
  1820     have "eventually (\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x) > 1/2) F"
  1821     by simp
  1822   thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
  1823   proof eventually_elim
  1824     case (elim x)
  1825     thus ?case
  1826       by (cases "f x" "0 :: real" rule: linorder_cases; 
  1827           cases "g x" "0 :: real" rule: linorder_cases) simp_all
  1828   qed
  1829 qed
  1830 
  1831 lemma
  1832   fixes f g :: "_ \<Rightarrow> real"
  1833   assumes "f \<sim>[F] g"
  1834   shows   asymp_equiv_eventually_same_sign: "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" (is ?th1)
  1835     and   asymp_equiv_eventually_neg_iff:   "eventually (\<lambda>x. f x < 0 \<longleftrightarrow> g x < 0) F" (is ?th2)
  1836     and   asymp_equiv_eventually_pos_iff:   "eventually (\<lambda>x. f x > 0 \<longleftrightarrow> g x > 0) F" (is ?th3)
  1837 proof -
  1838   from assms have "filterlim (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) (nhds 1) F"
  1839     by (rule asymp_equivD)
  1840   from order_tendstoD(1)[OF this zero_less_one]
  1841     show ?th1 ?th2 ?th3
  1842     by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+
  1843 qed
  1844 
  1845 lemma asymp_equiv_tendsto_transfer:
  1846   assumes "f \<sim>[F] g" and "(f \<longlongrightarrow> c) F"
  1847   shows   "(g \<longlongrightarrow> c) F"
  1848 proof -
  1849   let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"
  1850   have "eventually (\<lambda>x. ?h x = g x) F"
  1851     using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
  1852   moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
  1853   hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"
  1854     by (rule asymp_equivD)
  1855   from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp
  1856   ultimately show ?thesis by (rule Lim_transform_eventually)
  1857 qed
  1858 
  1859 lemma tendsto_asymp_equiv_cong:
  1860   assumes "f \<sim>[F] g"
  1861   shows   "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"
  1862 proof -
  1863   {
  1864     fix f g :: "'a \<Rightarrow> 'b"
  1865     assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"
  1866     have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"
  1867       using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp
  1868     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"
  1869       by (intro tendsto_intros asymp_equivD *)
  1870     ultimately have "(f \<longlongrightarrow> c * 1) F"
  1871       by (rule Lim_transform_eventually)
  1872   }
  1873   from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym)
  1874 qed
  1875 
  1876 
  1877 lemma smallo_imp_eventually_sgn:
  1878   fixes f g :: "real \<Rightarrow> real"
  1879   assumes "g \<in> o(f)"
  1880   shows   "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top"
  1881 proof -
  1882   have "0 < (1/2 :: real)" by simp
  1883   from landau_o.smallD[OF assms, OF this] 
  1884     have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp
  1885   thus ?thesis
  1886   proof eventually_elim
  1887     case (elim x)
  1888     thus ?case
  1889       by (cases "f x" "0::real" rule: linorder_cases; 
  1890           cases "f x + g x" "0::real" rule: linorder_cases) simp_all
  1891   qed
  1892 qed
  1893 
  1894 context
  1895 begin
  1896 
  1897 private lemma asymp_equiv_add_rightI:
  1898   assumes "f \<sim>[F] g" "h \<in> o[F](g)"
  1899   shows   "(\<lambda>x. f x + h x) \<sim>[F] g"
  1900 proof -
  1901   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  1902   from landau_o.smallD[OF assms(2) zero_less_one]
  1903     have ev: "eventually (\<lambda>x. g x = 0 \<longrightarrow> h x = 0) F" by eventually_elim auto
  1904   have "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1) F"
  1905     unfolding asymp_equiv_def using ev
  1906     by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps)
  1907   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1 + 0) F" by simp
  1908   also have \<dots> by (intro tendsto_intros asymp_equivD assms smalloD_tendsto)
  1909   finally show "(\<lambda>x. f x + h x) \<sim>[F] g" .
  1910 qed
  1911 
  1912 lemma asymp_equiv_add_right [asymp_equiv_simps]:
  1913   assumes "h \<in> o[F](g)"
  1914   shows   "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
  1915 proof
  1916   assume "(\<lambda>x. f x + h x) \<sim>[F] g"
  1917   from asymp_equiv_add_rightI[OF this, of "\<lambda>x. -h x"] assms show "f \<sim>[F] g"
  1918     by simp
  1919 qed (simp_all add: asymp_equiv_add_rightI assms)
  1920 
  1921 end
  1922 
  1923 lemma asymp_equiv_add_left [asymp_equiv_simps]: 
  1924   assumes "h \<in> o[F](g)"
  1925   shows   "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
  1926   using asymp_equiv_add_right[OF assms] by (simp add: add.commute)
  1927 
  1928 lemma asymp_equiv_add_right' [asymp_equiv_simps]:
  1929   assumes "h \<in> o[F](g)"
  1930   shows   "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f"
  1931   using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym)
  1932   
  1933 lemma asymp_equiv_add_left' [asymp_equiv_simps]:
  1934   assumes "h \<in> o[F](g)"
  1935   shows   "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f"
  1936   using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym)
  1937 
  1938 lemma smallo_imp_asymp_equiv:
  1939   assumes "(\<lambda>x. f x - g x) \<in> o[F](g)"
  1940   shows   "f \<sim>[F] g"
  1941 proof -
  1942   from assms have "(\<lambda>x. f x - g x + g x) \<sim>[F] g"
  1943     by (subst asymp_equiv_add_left) simp_all
  1944   thus ?thesis by simp
  1945 qed
  1946 
  1947 lemma asymp_equiv_uminus [asymp_equiv_intros]:
  1948   "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. -f x) \<sim>[F] (\<lambda>x. -g x)"
  1949   by (simp add: asymp_equiv_def cong: if_cong)
  1950 
  1951 lemma asymp_equiv_uminus_iff [asymp_equiv_simps]:
  1952   "(\<lambda>x. -f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] (\<lambda>x. -g x)"
  1953   by (simp add: asymp_equiv_def cong: if_cong)
  1954 
  1955 lemma asymp_equiv_mult [asymp_equiv_intros]:
  1956   fixes f1 f2 g1 g2 :: "'a \<Rightarrow> 'b :: real_normed_field"
  1957   assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
  1958   shows   "(\<lambda>x. f1 x * f2 x) \<sim>[F] (\<lambda>x. g1 x * g2 x)"
  1959 proof -
  1960   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  1961   let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x
  1962                    else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)"
  1963   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"
  1964   {
  1965     fix f g :: "'a \<Rightarrow> 'b" assume "f \<sim>[F] g"
  1966     have "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F"
  1967       by (rule tendsto_eq_intros refl asymp_equivD[OF \<open>f \<sim>[F] g\<close>])+ simp_all
  1968   } note A = this    
  1969 
  1970   from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"
  1971     by (intro tendsto_mult asymp_equivD)
  1972   moreover {
  1973     have "eventually (\<lambda>x. ?S x = ?S' x) F"
  1974       using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
  1975     moreover have "(?S \<longlongrightarrow> 0) F"
  1976       by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])
  1977          (auto intro: le_infI1 le_infI2)
  1978     ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)
  1979   }
  1980   ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"
  1981     by (rule Lim_transform)
  1982   thus ?thesis by (simp add: asymp_equiv_def)
  1983 qed
  1984 
  1985 lemma asymp_equiv_power [asymp_equiv_intros]:
  1986   "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)"
  1987   by (induction n) (simp_all add: asymp_equiv_mult)
  1988 
  1989 lemma asymp_equiv_inverse [asymp_equiv_intros]:
  1990   assumes "f \<sim>[F] g"
  1991   shows   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
  1992 proof -
  1993   from tendsto_inverse[OF asymp_equivD[OF assms]]
  1994     have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) \<longlongrightarrow> 1) F"
  1995     by (simp add: if_distrib cong: if_cong)
  1996   also have "(\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) =
  1997                (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else inverse (f x) / inverse (g x))"
  1998     by (intro ext) (simp add: field_simps)
  1999   finally show ?thesis by (simp add: asymp_equiv_def)
  2000 qed
  2001 
  2002 lemma asymp_equiv_inverse_iff [asymp_equiv_simps]:
  2003   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<sim>[F] g"
  2004 proof
  2005   assume "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
  2006   hence "(\<lambda>x. inverse (inverse (f x))) \<sim>[F] (\<lambda>x. inverse (inverse (g x)))" (is ?P)
  2007     by (rule asymp_equiv_inverse)
  2008   also have "?P \<longleftrightarrow> f \<sim>[F] g" by (intro asymp_equiv_cong) simp_all
  2009   finally show "f \<sim>[F] g" .
  2010 qed (simp_all add: asymp_equiv_inverse)
  2011 
  2012 lemma asymp_equiv_divide [asymp_equiv_intros]:
  2013   assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
  2014   shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
  2015   using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
  2016 
  2017 lemma asymp_equiv_compose [asymp_equiv_intros]:
  2018   assumes "f \<sim>[G] g" "filterlim h G F"
  2019   shows   "f \<circ> h \<sim>[F] g \<circ> h"
  2020 proof -
  2021   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  2022   have "f \<circ> h \<sim>[F] g \<circ> h \<longleftrightarrow> ((?T f g \<circ> h) \<longlongrightarrow> 1) F"
  2023     by (simp add: asymp_equiv_def o_def)
  2024   also have "\<dots> \<longleftrightarrow> (?T f g \<longlongrightarrow> 1) (filtermap h F)"
  2025     by (rule tendsto_compose_filtermap)
  2026   also have "\<dots>"
  2027     by (rule tendsto_mono[of _ G]) (insert assms, simp_all add: asymp_equiv_def filterlim_def)
  2028   finally show ?thesis .
  2029 qed
  2030 
  2031 lemma asymp_equiv_compose':
  2032   assumes "f \<sim>[G] g" "filterlim h G F"
  2033   shows   "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
  2034   using asymp_equiv_compose[OF assms] by (simp add: o_def)
  2035   
  2036 lemma asymp_equiv_powr_real [asymp_equiv_intros]:
  2037   fixes f g :: "'a \<Rightarrow> real"
  2038   assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
  2039   shows   "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"
  2040 proof -
  2041   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  2042   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"
  2043     using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)
  2044     by eventually_elim (auto simp: powr_divide)
  2045   moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
  2046     by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
  2047   hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
  2048   ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
  2049 qed
  2050 
  2051 lemma asymp_equiv_norm [asymp_equiv_intros]:
  2052   fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
  2053   assumes "f \<sim>[F] g"
  2054   shows   "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))"
  2055   using tendsto_norm[OF asymp_equivD[OF assms]] 
  2056   by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong)
  2057 
  2058 lemma asymp_equiv_abs_real [asymp_equiv_intros]:
  2059   fixes f g :: "'a \<Rightarrow> real"
  2060   assumes "f \<sim>[F] g"
  2061   shows   "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)"
  2062   using tendsto_rabs[OF asymp_equivD[OF assms]] 
  2063   by (simp add: if_distrib asymp_equiv_def cong: if_cong)
  2064 
  2065 lemma asymp_equiv_imp_eventually_le:
  2066   assumes "f \<sim>[F] g" "c > 1"
  2067   shows   "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"
  2068 proof -
  2069   from order_tendstoD(2)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
  2070        asymp_equiv_eventually_zeros[OF assms(1)]
  2071     show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
  2072 qed
  2073 
  2074 lemma asymp_equiv_imp_eventually_ge:
  2075   assumes "f \<sim>[F] g" "c < 1"
  2076   shows   "eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F"
  2077 proof -
  2078   from order_tendstoD(1)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
  2079        asymp_equiv_eventually_zeros[OF assms(1)]
  2080     show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
  2081 qed
  2082 
  2083 lemma asymp_equiv_imp_bigo:
  2084   assumes "f \<sim>[F] g"
  2085   shows   "f \<in> O[F](g)"
  2086 proof (rule bigoI)
  2087   have "(3/2::real) > 1" by simp
  2088   from asymp_equiv_imp_eventually_le[OF assms this]
  2089     show "eventually (\<lambda>x. norm (f x) \<le> 3/2 * norm (g x)) F"
  2090     by eventually_elim simp
  2091 qed
  2092 
  2093 lemma asymp_equiv_imp_bigomega:
  2094   "f \<sim>[F] g \<Longrightarrow> f \<in> \<Omega>[F](g)"
  2095   using asymp_equiv_imp_bigo[of g F f] by (simp add: asymp_equiv_sym bigomega_iff_bigo)
  2096 
  2097 lemma asymp_equiv_imp_bigtheta:
  2098   "f \<sim>[F] g \<Longrightarrow> f \<in> \<Theta>[F](g)"
  2099   by (intro bigthetaI asymp_equiv_imp_bigo asymp_equiv_imp_bigomega)
  2100 
  2101 lemma asymp_equiv_at_infinity_transfer:
  2102   assumes "f \<sim>[F] g" "filterlim f at_infinity F"
  2103   shows   "filterlim g at_infinity F"
  2104 proof -
  2105   from assms(1) have "g \<in> \<Theta>[F](f)" by (rule asymp_equiv_imp_bigtheta[OF asymp_equiv_symI])
  2106   also from assms have "f \<in> \<omega>[F](\<lambda>_. 1)" by (simp add: smallomega_1_conv_filterlim)
  2107   finally show ?thesis by (simp add: smallomega_1_conv_filterlim)
  2108 qed
  2109 
  2110 lemma asymp_equiv_at_top_transfer:
  2111   fixes f g :: "_ \<Rightarrow> real"
  2112   assumes "f \<sim>[F] g" "filterlim f at_top F"
  2113   shows   "filterlim g at_top F"
  2114 proof (rule filterlim_at_infinity_imp_filterlim_at_top)
  2115   show "filterlim g at_infinity F"
  2116     by (rule asymp_equiv_at_infinity_transfer[OF assms(1) filterlim_mono[OF assms(2)]])
  2117        (auto simp: at_top_le_at_infinity)
  2118   from assms(2) have "eventually (\<lambda>x. f x > 0) F"
  2119     using filterlim_at_top_dense by blast
  2120   with asymp_equiv_eventually_pos_iff[OF assms(1)] show "eventually (\<lambda>x. g x > 0) F"
  2121     by eventually_elim blast
  2122 qed
  2123 
  2124 lemma asymp_equiv_at_bot_transfer:
  2125   fixes f g :: "_ \<Rightarrow> real"
  2126   assumes "f \<sim>[F] g" "filterlim f at_bot F"
  2127   shows   "filterlim g at_bot F"
  2128   unfolding filterlim_uminus_at_bot
  2129   by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"])
  2130      (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus)  
  2131 
  2132 lemma asymp_equivI'_const:
  2133   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0"
  2134   shows   "f \<sim>[F] (\<lambda>x. c * g x)"
  2135   using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2)
  2136   by (intro asymp_equivI') (simp add: field_simps)
  2137 
  2138 lemma asymp_equivI'_inverse_const:
  2139   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> inverse c) F" "c \<noteq> 0"
  2140   shows   "(\<lambda>x. c * f x) \<sim>[F] g"
  2141   using tendsto_mult[OF assms(1) tendsto_const[of "c"]] assms(2)
  2142   by (intro asymp_equivI') (simp add: field_simps)
  2143 
  2144 lemma filterlim_at_bot_imp_at_infinity: "filterlim f at_bot F \<Longrightarrow> filterlim f at_infinity F"
  2145   for f :: "_ \<Rightarrow> real" using at_bot_le_at_infinity filterlim_mono by blast
  2146 
  2147 lemma asymp_equiv_imp_diff_smallo:
  2148   assumes "f \<sim>[F] g"
  2149   shows   "(\<lambda>x. f x - g x) \<in> o[F](g)"
  2150 proof (rule landau_o.smallI)
  2151   fix c :: real assume "c > 0"
  2152   hence c: "min c 1 > 0" by simp
  2153   let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  2154   from assms have "((\<lambda>x. ?h x - 1) \<longlongrightarrow> 1 - 1) F"
  2155     by (intro tendsto_diff asymp_equivD tendsto_const)
  2156   from tendstoD[OF this c] show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
  2157   proof eventually_elim
  2158     case (elim x)
  2159     from elim have "norm (f x - g x) \<le> norm (f x / g x - 1) * norm (g x)"
  2160       by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps)
  2161     also have "norm (f x / g x - 1) * norm (g x) \<le> c * norm (g x)" using elim
  2162       by (auto split: if_splits simp: mult_right_mono)
  2163     finally show ?case .
  2164   qed
  2165 qed
  2166 
  2167 lemma asymp_equiv_altdef:
  2168   "f \<sim>[F] g \<longleftrightarrow> (\<lambda>x. f x - g x) \<in> o[F](g)"
  2169   by (rule iffI[OF asymp_equiv_imp_diff_smallo smallo_imp_asymp_equiv])
  2170 
  2171 lemma asymp_equiv_0_left_iff [simp]: "(\<lambda>_. 0) \<sim>[F] f \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  2172   and asymp_equiv_0_right_iff [simp]: "f \<sim>[F] (\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  2173   by (simp_all add: asymp_equiv_altdef landau_o.small_refl_iff)
  2174 
  2175 lemma asymp_equiv_sandwich_real:
  2176   fixes f g l u :: "'a \<Rightarrow> real"
  2177   assumes "l \<sim>[F] g" "u \<sim>[F] g" "eventually (\<lambda>x. f x \<in> {l x..u x}) F"
  2178   shows   "f \<sim>[F] g"
  2179   unfolding asymp_equiv_altdef
  2180 proof (rule landau_o.smallI)
  2181   fix c :: real assume c: "c > 0"
  2182   have "eventually (\<lambda>x. norm (f x - g x) \<le> max (norm (l x - g x)) (norm (u x - g x))) F"
  2183     using assms(3) by eventually_elim auto
  2184   moreover have "eventually (\<lambda>x. norm (l x - g x) \<le> c * norm (g x)) F"
  2185                 "eventually (\<lambda>x. norm (u x - g x) \<le> c * norm (g x)) F"
  2186     using assms(1,2) by (auto simp: asymp_equiv_altdef dest: landau_o.smallD[OF _ c])
  2187   hence "eventually (\<lambda>x. max (norm (l x - g x)) (norm (u x - g x)) \<le> c * norm (g x)) F"
  2188     by eventually_elim simp
  2189   ultimately show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
  2190     by eventually_elim (rule order.trans)
  2191 qed
  2192 
  2193 lemma asymp_equiv_sandwich_real':
  2194   fixes f g l u :: "'a \<Rightarrow> real"
  2195   assumes "f \<sim>[F] l" "f \<sim>[F] u" "eventually (\<lambda>x. g x \<in> {l x..u x}) F"
  2196   shows   "f \<sim>[F] g"
  2197   using asymp_equiv_sandwich_real[of l F f u g] assms by (simp add: asymp_equiv_sym)
  2198 
  2199 lemma asymp_equiv_sandwich_real'':
  2200   fixes f g l u :: "'a \<Rightarrow> real"
  2201   assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"
  2202           "eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"
  2203   shows   "f \<sim>[F] g"
  2204   by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]
  2205              asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];
  2206       blast intro: asymp_equiv_trans assms(1,2,3))+
  2207 
  2208 end