src/HOL/Library/Landau_Symbols.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69597 ff784d5a5bfb
child 70365 4df0628e8545
permissions -rw-r--r--
improved code equations taken over from AFP
     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 \<open>Definition of Landau symbols\<close>
     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 \<open>Definition of Landau symbols\<close>
    20 
    21 text \<open>
    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 \<close>
    27 
    28 definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    29     (\<open>(1O[_]'(_'))\<close>)
    30   where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"  
    31 
    32 definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    33     (\<open>(1o[_]'(_'))\<close>)
    34   where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
    35 
    36 definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    37     (\<open>(1\<Omega>[_]'(_'))\<close>)
    38   where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"  
    39 
    40 definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    41     (\<open>(1\<omega>[_]'(_'))\<close>)
    42   where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
    43 
    44 definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
    45     (\<open>(1\<Theta>[_]'(_'))\<close>)
    46   where "bigtheta F g = bigo F g \<inter> bigomega F g"
    47 
    48 abbreviation bigo_at_top (\<open>(2O'(_'))\<close>) where
    49   "O(g) \<equiv> bigo at_top g"    
    50 
    51 abbreviation smallo_at_top (\<open>(2o'(_'))\<close>) where
    52   "o(g) \<equiv> smallo at_top g"
    53 
    54 abbreviation bigomega_at_top (\<open>(2\<Omega>'(_'))\<close>) where
    55   "\<Omega>(g) \<equiv> bigomega at_top g"
    56 
    57 abbreviation smallomega_at_top (\<open>(2\<omega>'(_'))\<close>) where
    58   "\<omega>(g) \<equiv> smallomega at_top g"
    59 
    60 abbreviation bigtheta_at_top (\<open>(2\<Theta>'(_'))\<close>) where
    61   "\<Theta>(g) \<equiv> bigtheta at_top g"
    62     
    63 
    64 text \<open>The following is a set of properties that all Landau symbols satisfy.\<close>
    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 \<open>
   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 \<close>
   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 \<open>c \<noteq> 0\<close> 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 \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
   615       have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
   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       by (subst eventually_subst'[OF A]) (rule refl)
   634   }
   635   {
   636     fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   637     show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" unfolding L_def mem_Collect_eq
   638       by (subst (1) eventually_subst'[OF A]) (rule refl)
   639   }
   640   {
   641     fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" thus "L F f \<subseteq> L F g" by (rule big_subsetI)
   642   }
   643   {
   644     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
   645     with A L show "L F (f) = L F (g)" unfolding bigtheta_def
   646       by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo)
   647     fix h:: "'a \<Rightarrow> 'b"
   648     show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" by (rule disjE[OF L]) 
   649       (insert A, auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans)
   650   }
   651   {
   652     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g"
   653     thus "(\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" by (intro big_mult) simp
   654   }
   655   {
   656     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" "g \<in> L F h"
   657     thus "f \<in> L F (h)" by (rule big_trans)
   658   }
   659   {
   660     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
   661     assume "f \<in> L F g" and "filterlim h F G"
   662     thus "(\<lambda>x. f (h x)) \<in> L' G (\<lambda>x. g (h x))" by (auto simp: L_def L'_def filterlim_iff)
   663   }
   664   {
   665     fix f g :: "'a \<Rightarrow> 'b" and F G :: "'a filter"
   666     assume "f \<in> L F g" "f \<in> L G g"
   667     from this [THEN bigE] guess c1 c2 . note c12 = this
   668     define c where "c = (if R c1 c2 then c2 else c1)"
   669     from c12 have c: "R c1 c" "R c2 c" "c > 0" by (auto simp: c_def dest: R_linear)
   670     with c12(2,4) have "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
   671                      "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) G"
   672       by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+
   673     with c show "f \<in> L (sup F G) g" by (auto simp: L_def eventually_sup)
   674   }
   675   {
   676     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
   677     assume "(f \<in> L F g)"
   678     thus "((\<lambda>x. f (h x)) \<in> L' (filtercomap h F) (\<lambda>x. g (h x)))"
   679       unfolding L_def L'_def by auto
   680   }
   681 qed (auto simp: L_def Lr_def eventually_filtermap L'_def
   682           intro: filter_leD exI[of _ "1::real"])
   683 
   684 sublocale small: landau_symbol l l' lr
   685 proof
   686   {
   687     fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   688     hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
   689   } note A = this
   690   {
   691     fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   692     from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
   693       show "l F (\<lambda>x. c * f x) = l F f" 
   694         by (intro equalityI small_subsetI) (simp_all add: field_simps)
   695   }
   696   {
   697     fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   698     from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
   699       have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
   700     thus "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" by (intro iffI) (erule (1) big_small_trans)+
   701   }
   702   {
   703     fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
   704     with plus_aux show "l F g \<subseteq> l F (\<lambda>x. f x + g x)" by (blast intro!: small_subsetI) 
   705   }
   706   {
   707     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> l F (g)"
   708     assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
   709     show "(\<lambda>x. inverse (g x)) \<in> l F (\<lambda>x. inverse (f x))"
   710     proof (rule smallI)
   711       fix c :: real assume c: "c > 0"
   712       from B smallD[OF A c] 
   713         show "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
   714         by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide)
   715     qed
   716   }
   717   {
   718     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   719     show "l F (f) = l F (g)" unfolding l_def by (subst eventually_subst'[OF A]) (rule refl)
   720   }
   721   {
   722     fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
   723     show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" unfolding l_def mem_Collect_eq
   724       by (subst (1) eventually_subst'[OF A]) (rule refl)
   725   }
   726   {
   727     fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" 
   728     thus "l F f \<subseteq> l F g" by (intro small_subsetI small_imp_big)
   729   }
   730   {
   731     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
   732     have L: "L = bigo \<or> L = bigomega"
   733       by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
   734     with A show "l F (f) = l F (g)" unfolding bigtheta_def
   735       by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo)
   736     have l: "l = smallo \<or> l = smallomega"
   737       by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff)
   738     fix h:: "'a \<Rightarrow> 'b"
   739     show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" by (rule disjE[OF l]) 
   740       (insert A, auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo 
   741        intro: landau_o.big_small_trans landau_o.small_big_trans)
   742   }
   743   {
   744     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g"
   745     thus "(\<lambda>x. h x * f x) \<in> l F (\<lambda>x. h x * g x)" by (intro big_small_mult) simp
   746   }
   747   {
   748     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" "g \<in> l F h"
   749     thus "f \<in> l F (h)" by (rule small_trans)
   750   }
   751   {
   752     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
   753     assume "f \<in> l F g" and "filterlim h F G"
   754     thus "(\<lambda>x. f (h x)) \<in> l' G (\<lambda>x. g (h x))"
   755       by (auto simp: l_def l'_def filterlim_iff)
   756   }
   757   {
   758     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
   759     assume "(f \<in> l F g)"
   760     thus "((\<lambda>x. f (h x)) \<in> l' (filtercomap h F) (\<lambda>x. g (h x)))"
   761       unfolding l_def l'_def by auto
   762   }
   763 qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)
   764 
   765 
   766 text \<open>These rules allow chaining of Landau symbol propositions in Isar with "also".\<close>
   767 
   768 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)"
   769   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)"
   770   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)"
   771   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)"
   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   by (drule (1) big.mult big_small_mult small_big_mult, simp)+
   775 
   776 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)"
   777   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)"
   778   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)"
   779   and small_1_mult': "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> l F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"
   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   by (drule (1) big.mult big_small_mult small_big_mult, simp)+
   783 
   784 lemmas mult_1_trans = 
   785   big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1'''
   786   big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult'''
   787 
   788 lemma big_equal_iff_bigtheta: "L F (f) = L F (g) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
   789 proof
   790   have L: "L = bigo \<or> L = bigomega"
   791     by (rule R_E) (auto simp: fun_eq_iff L_def bigo_def bigomega_def)
   792   fix f g :: "'a \<Rightarrow> 'b" assume "L F (f) = L F (g)"
   793   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
   794   thus "f \<in> \<Theta>[F](g)" using L unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
   795 qed (rule big.cong_bigtheta)
   796 
   797 lemma big_prod:
   798   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (g x)"
   799   shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>y. \<Prod>x\<in>A. g x y)"
   800   using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult)
   801 
   802 lemma big_prod_in_1:
   803   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (\<lambda>_. 1)"
   804   shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>_. 1)"
   805   using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult_in_1)
   806 
   807 end
   808 
   809 
   810 context landau_symbol
   811 begin
   812   
   813 lemma plus_absorb1:
   814   assumes "f \<in> o[F](g)"
   815   shows   "L F (\<lambda>x. f x + g x) = L F (g)"
   816 proof (intro equalityI)
   817   from plus_subset1 and assms show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" .
   818   from landau_o.small.plus_subset1[OF assms] and assms have "(\<lambda>x. -f x) \<in> o[F](\<lambda>x. f x + g x)"
   819     by (auto simp: landau_o.small.uminus_in_iff)
   820   from plus_subset1[OF this] show "L F (\<lambda>x. f x + g x) \<subseteq> L F (g)" by simp
   821 qed
   822 
   823 lemma plus_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x + g x) = L F (f)"
   824   using plus_absorb1[of g F f] by (simp add: add.commute)
   825 
   826 lemma diff_absorb1: "f \<in> o[F](g) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (g)"
   827   by (simp only: diff_conv_add_uminus plus_absorb1 landau_o.small.uminus uminus)
   828 
   829 lemma diff_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (f)"
   830   by (simp only: diff_conv_add_uminus plus_absorb2 landau_o.small.uminus_in_iff)
   831 
   832 lemmas absorb = plus_absorb1 plus_absorb2 diff_absorb1 diff_absorb2
   833 
   834 end
   835 
   836 
   837 lemma bigthetaI [intro]: "f \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> \<Theta>[F](g)"
   838   unfolding bigtheta_def bigomega_def by blast
   839 
   840 lemma bigthetaD1 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> O[F](g)" 
   841   and bigthetaD2 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g)"
   842   unfolding bigtheta_def bigo_def bigomega_def by blast+
   843 
   844 lemma bigtheta_refl [simp]: "f \<in> \<Theta>[F](f)"
   845   unfolding bigtheta_def by simp
   846 
   847 lemma bigtheta_sym: "f \<in> \<Theta>[F](g) \<longleftrightarrow> g \<in> \<Theta>[F](f)"
   848   unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
   849 
   850 lemmas landau_flip =
   851   bigomega_iff_bigo[symmetric] smallomega_iff_smallo[symmetric]
   852   bigomega_iff_bigo smallomega_iff_smallo bigtheta_sym
   853 
   854 
   855 interpretation landau_theta: landau_symbol bigtheta bigtheta bigtheta
   856 proof
   857   fix f g :: "'a \<Rightarrow> 'b" and F
   858   assume "f \<in> o[F](g)"
   859   hence "O[F](g) \<subseteq> O[F](\<lambda>x. f x + g x)" "\<Omega>[F](g) \<subseteq> \<Omega>[F](\<lambda>x. f x + g x)"
   860     by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+
   861   thus "\<Theta>[F](g) \<subseteq> \<Theta>[F](\<lambda>x. f x + g x)" unfolding bigtheta_def by blast
   862 next
   863   fix f g :: "'a \<Rightarrow> 'b" and F 
   864   assume "f \<in> \<Theta>[F](g)"
   865   thus A: "\<Theta>[F](f) = \<Theta>[F](g)" 
   866     apply (subst (1 2) bigtheta_def)
   867     apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+
   868     apply (rule refl)
   869     done
   870   thus "\<Theta>[F](f) \<subseteq> \<Theta>[F](g)" by simp
   871   fix h :: "'a \<Rightarrow> 'b"
   872   show "f \<in> \<Theta>[F](h) \<longleftrightarrow> g \<in> \<Theta>[F](h)" by (subst (1 2) bigtheta_sym) (simp add: A)
   873 next
   874   fix f g h :: "'a \<Rightarrow> 'b" and F
   875   assume "f \<in> \<Theta>[F](g)" "g \<in> \<Theta>[F](h)"
   876   thus "f \<in> \<Theta>[F](h)" unfolding bigtheta_def
   877     by (blast intro: landau_o.big.trans landau_omega.big.trans)
   878 next
   879   fix f :: "'a \<Rightarrow> 'b" and F1 F2 :: "'a filter"
   880   assume "F1 \<le> F2"
   881   thus "\<Theta>[F2](f) \<subseteq> \<Theta>[F1](f)"
   882     by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono)
   883 qed (auto simp: bigtheta_def landau_o.big.norm_iff 
   884                 landau_o.big.cmult landau_omega.big.cmult 
   885                 landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff 
   886                 landau_o.big.in_cong landau_omega.big.in_cong
   887                 landau_o.big.mult landau_omega.big.mult
   888                 landau_o.big.inverse landau_omega.big.inverse 
   889                 landau_o.big.compose landau_omega.big.compose
   890                 landau_o.big.bot' landau_omega.big.bot'
   891                 landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff
   892                 landau_o.big.sup landau_omega.big.sup
   893                 landau_o.big.filtercomap landau_omega.big.filtercomap
   894           dest: landau_o.big.cong landau_omega.big.cong)
   895 
   896 lemmas landau_symbols = 
   897   landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms
   898   landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms 
   899   landau_theta.landau_symbol_axioms
   900 
   901 lemma bigoI [intro]:
   902   assumes "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
   903   shows   "f \<in> O[F](g)"
   904 proof (rule landau_o.bigI)
   905   show "max 1 c > 0" by simp
   906   note assms
   907   moreover have "\<And>x. c * (norm (g x)) \<le> max 1 c * (norm (g x))" by (simp add: mult_right_mono)
   908   ultimately show "eventually (\<lambda>x. (norm (f x)) \<le> max 1 c * (norm (g x))) F"
   909     by (auto elim!: eventually_mono dest: order.trans)
   910 qed
   911 
   912 lemma smallomegaD [dest]:
   913   assumes "f \<in> \<omega>[F](g)"
   914   shows   "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
   915 proof (cases "c > 0")
   916   case False
   917   show ?thesis 
   918     by (intro always_eventually allI, rule order.trans[of _ 0])
   919        (insert False, auto intro!: mult_nonpos_nonneg)
   920 qed (blast dest: landau_omega.smallD[OF assms, of c])
   921 
   922   
   923 lemma bigthetaI':
   924   assumes "c1 > 0" "c2 > 0"
   925   assumes "eventually (\<lambda>x. c1 * (norm (g x)) \<le> (norm (f x)) \<and> (norm (f x)) \<le> c2 * (norm (g x))) F"
   926   shows   "f \<in> \<Theta>[F](g)"
   927 apply (rule bigthetaI)
   928 apply (rule landau_o.bigI[OF assms(2)]) using assms(3) apply (eventually_elim, simp)
   929 apply (rule landau_omega.bigI[OF assms(1)]) using assms(3) apply (eventually_elim, simp)
   930 done
   931 
   932 lemma bigthetaI_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> \<Theta>[F](g)"
   933   by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono)
   934 
   935 lemma (in landau_symbol) ev_eq_trans1: 
   936   "f \<in> L F (\<lambda>x. g x (h x)) \<Longrightarrow> eventually (\<lambda>x. h x = h' x) F \<Longrightarrow> f \<in> L F (\<lambda>x. g x (h' x))"
   937   by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono)
   938 
   939 lemma (in landau_symbol) ev_eq_trans2: 
   940   "eventually (\<lambda>x. f x = f' x) F \<Longrightarrow> (\<lambda>x. g x (f' x)) \<in> L F (h) \<Longrightarrow> (\<lambda>x. g x (f x)) \<in> L F (h)"
   941   by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono)
   942 
   943 declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro]
   944 declare landau_o.bigE landau_omega.bigE [elim]
   945 declare landau_o.smallD
   946 
   947 lemma (in landau_symbol) bigtheta_trans1': 
   948   "f \<in> L F (g) \<Longrightarrow> h \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h)"
   949   by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym)
   950 
   951 lemma (in landau_symbol) bigtheta_trans2': 
   952   "g \<in> \<Theta>[F](f) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
   953   by (rule bigtheta_trans2, subst bigtheta_sym)
   954 
   955 lemma bigo_bigomega_trans:      "f \<in> O[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> O[F](h)"
   956   and bigo_smallomega_trans:    "f \<in> O[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
   957   and smallo_bigomega_trans:    "f \<in> o[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
   958   and smallo_smallomega_trans:  "f \<in> o[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
   959   and bigomega_bigo_trans:      "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](h)"
   960   and bigomega_smallo_trans:    "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
   961   and smallomega_bigo_trans:    "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
   962   and smallomega_smallo_trans:  "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
   963   by (unfold bigomega_iff_bigo smallomega_iff_smallo)
   964      (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans 
   965                 landau_o.big_trans landau_o.small_trans)+
   966 
   967 lemmas landau_trans_lift [trans] =
   968   landau_symbols[THEN landau_symbol.lift_trans]
   969   landau_symbols[THEN landau_symbol.lift_trans']
   970   landau_symbols[THEN landau_symbol.lift_trans_bigtheta]
   971   landau_symbols[THEN landau_symbol.lift_trans_bigtheta']
   972 
   973 lemmas landau_mult_1_trans [trans] =
   974   landau_o.mult_1_trans landau_omega.mult_1_trans
   975 
   976 lemmas landau_trans [trans] = 
   977   landau_symbols[THEN landau_symbol.bigtheta_trans1]
   978   landau_symbols[THEN landau_symbol.bigtheta_trans2]
   979   landau_symbols[THEN landau_symbol.bigtheta_trans1']
   980   landau_symbols[THEN landau_symbol.bigtheta_trans2']
   981   landau_symbols[THEN landau_symbol.ev_eq_trans1]
   982   landau_symbols[THEN landau_symbol.ev_eq_trans2]
   983 
   984   landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans
   985   landau_omega.big_trans landau_omega.small_trans 
   986     landau_omega.small_big_trans landau_omega.big_small_trans
   987 
   988   bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans 
   989   bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans
   990 
   991 lemma bigtheta_inverse [simp]: 
   992   shows "(\<lambda>x. inverse (f x)) \<in> \<Theta>[F](\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
   993 proof-
   994   {
   995     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
   996     then guess c1 c2 :: real unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
   997     note c = this
   998     from c(3) have "inverse c2 > 0" by simp
   999     moreover from c(2,4)
  1000       have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))) F"
  1001     proof eventually_elim
  1002       fix x assume A: "(norm (f x)) \<le> c1 * (norm (g x))" "c2 * (norm (g x)) \<le> (norm (f x))"
  1003       from A c(1,3) have "f x = 0 \<longleftrightarrow> g x = 0" by (auto simp: field_simps mult_le_0_iff)
  1004       with A c(1,3) show "norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))"
  1005         by (force simp: field_simps norm_inverse norm_divide)
  1006     qed
  1007     ultimately have "(\<lambda>x. inverse (f x)) \<in> O[F](\<lambda>x. inverse (g x))" by (rule landau_o.bigI)
  1008   }
  1009   thus ?thesis unfolding bigtheta_def 
  1010     by (force simp: bigomega_iff_bigo bigtheta_sym)
  1011 qed
  1012 
  1013 lemma bigtheta_divide:
  1014   assumes "f1 \<in> \<Theta>(f2)" "g1 \<in> \<Theta>(g2)"
  1015   shows   "(\<lambda>x. f1 x / g1 x) \<in> \<Theta>(\<lambda>x. f2 x / g2 x)"
  1016   by (subst (1 2) divide_inverse, intro landau_theta.mult) (simp_all add: bigtheta_inverse assms)
  1017 
  1018 lemma eventually_nonzero_bigtheta:
  1019   assumes "f \<in> \<Theta>[F](g)"
  1020   shows   "eventually (\<lambda>x. f x \<noteq> 0) F \<longleftrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F"
  1021 proof-
  1022   {
  1023     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)" and B: "eventually (\<lambda>x. f x \<noteq> 0) F"
  1024     from A guess c1 c2 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
  1025     from B this(2,4) have "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim auto
  1026   }
  1027   with assms show ?thesis by (force simp: bigtheta_sym)
  1028 qed
  1029 
  1030 
  1031 subsection \<open>Landau symbols and limits\<close>
  1032 
  1033 lemma bigoI_tendsto_norm:
  1034   fixes f g
  1035   assumes "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
  1036   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  1037   shows   "f \<in> O[F](g)"
  1038 proof (rule bigoI)
  1039   from assms have "eventually (\<lambda>x. dist (norm (f x / g x)) c < 1) F" 
  1040     using tendstoD by force
  1041   thus "eventually (\<lambda>x. (norm (f x)) \<le> (norm c + 1) * (norm (g x))) F"
  1042     unfolding dist_real_def using assms(2)
  1043   proof eventually_elim
  1044     case (elim x)
  1045     have "(norm (f x)) - norm c * (norm (g x)) \<le> norm ((norm (f x)) - c * (norm (g x)))"
  1046       unfolding norm_mult [symmetric] using norm_triangle_ineq2[of "norm (f x)" "c * norm (g x)"]
  1047       by (simp add: norm_mult abs_mult)
  1048     also from elim have "\<dots> = norm (norm (g x)) * norm (norm (f x / g x) - c)"
  1049       unfolding norm_mult [symmetric] by (simp add: algebra_simps norm_divide)
  1050     also from elim have "norm (norm (f x / g x) - c) \<le> 1" by simp
  1051     hence "norm (norm (g x)) * norm (norm (f x / g x) - c) \<le> norm (norm (g x)) * 1" 
  1052       by (rule mult_left_mono) simp_all
  1053     finally show ?case by (simp add: algebra_simps)
  1054   qed
  1055 qed
  1056 
  1057 lemma bigoI_tendsto:
  1058   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
  1059   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  1060   shows   "f \<in> O[F](g)"
  1061   using assms by (rule bigoI_tendsto_norm[OF tendsto_norm])
  1062 
  1063 lemma bigomegaI_tendsto_norm:
  1064   assumes c_not_0:  "(c::real) \<noteq> 0"
  1065   assumes lim:      "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
  1066   shows   "f \<in> \<Omega>[F](g)"
  1067 proof (cases "F = bot")
  1068   case False
  1069   show ?thesis
  1070   proof (rule landau_omega.bigI)
  1071     from lim  have "c \<ge> 0" by (rule tendsto_lowerbound) (insert False, simp_all)
  1072     with c_not_0 have "c > 0" by simp
  1073     with c_not_0 show "c/2 > 0" by simp
  1074     from lim have ev: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<epsilon>) F"
  1075       by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  1076     from ev[OF \<open>c/2 > 0\<close>] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
  1077     proof (eventually_elim)
  1078       fix x assume B: "norm (norm (f x / g x) - c) < c / 2"
  1079       from B have g: "g x \<noteq> 0" by auto
  1080       from B have "-c/2 < -norm (norm (f x / g x) - c)" by simp
  1081       also have "... \<le> norm (f x / g x) - c" by simp
  1082       finally show "(norm (f x)) \<ge> c/2 * (norm (g x))" using g 
  1083         by (simp add: field_simps norm_mult norm_divide)
  1084     qed
  1085   qed
  1086 qed simp
  1087 
  1088 lemma bigomegaI_tendsto:
  1089   assumes c_not_0:  "(c::real) \<noteq> 0"
  1090   assumes lim:      "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
  1091   shows   "f \<in> \<Omega>[F](g)"
  1092   by (rule bigomegaI_tendsto_norm[OF _ tendsto_norm, of c]) (insert assms, simp_all)
  1093 
  1094 lemma smallomegaI_filterlim_at_top_norm:
  1095   assumes lim: "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
  1096   shows   "f \<in> \<omega>[F](g)"
  1097 proof (rule landau_omega.smallI)
  1098   fix c :: real assume c_pos: "c > 0"
  1099   from lim have ev: "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F"
  1100     by (subst (asm) filterlim_at_top) simp
  1101   thus "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
  1102   proof eventually_elim
  1103     fix x assume A: "norm (f x / g x) \<ge> c"
  1104     from A c_pos have "g x \<noteq> 0" by auto
  1105     with A show "(norm (f x)) \<ge> c * (norm (g x))" by (simp add: field_simps norm_divide)
  1106   qed
  1107 qed
  1108 
  1109 lemma smallomegaI_filterlim_at_infinity:
  1110   assumes lim: "filterlim (\<lambda>x. f x / g x) at_infinity F"
  1111   shows   "f \<in> \<omega>[F](g)"
  1112 proof (rule smallomegaI_filterlim_at_top_norm)
  1113   from lim show "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
  1114     by (rule filterlim_at_infinity_imp_norm_at_top)
  1115 qed
  1116   
  1117 lemma smallomegaD_filterlim_at_top_norm:
  1118   assumes "f \<in> \<omega>[F](g)"
  1119   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  1120   shows   "LIM x F. norm (f x / g x) :> at_top"
  1121 proof (subst filterlim_at_top_gt, clarify)
  1122   fix c :: real assume c: "c > 0"
  1123   from landau_omega.smallD[OF assms(1) this] assms(2) 
  1124     show "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F" 
  1125     by eventually_elim (simp add: field_simps norm_divide)
  1126 qed
  1127   
  1128 lemma smallomegaD_filterlim_at_infinity:
  1129   assumes "f \<in> \<omega>[F](g)"
  1130   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  1131   shows   "LIM x F. f x / g x :> at_infinity"
  1132   using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm)
  1133 
  1134 lemma smallomega_1_conv_filterlim: "f \<in> \<omega>[F](\<lambda>_. 1) \<longleftrightarrow> filterlim f at_infinity F"
  1135   by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)
  1136 
  1137 lemma smalloI_tendsto:
  1138   assumes lim: "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
  1139   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
  1140   shows   "f \<in> o[F](g)"
  1141 proof (rule landau_o.smallI)
  1142   fix c :: real assume c_pos: "c > 0"
  1143   from c_pos and lim have ev: "eventually (\<lambda>x. norm (f x / g x) < c) F"
  1144     by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  1145   with assms(2) show "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
  1146     by eventually_elim (simp add: field_simps norm_divide)
  1147 qed
  1148 
  1149 lemma smalloD_tendsto:
  1150   assumes "f \<in> o[F](g)"
  1151   shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
  1152 unfolding tendsto_iff
  1153 proof clarify
  1154   fix e :: real assume e: "e > 0"
  1155   hence "e/2 > 0" by simp
  1156   from landau_o.smallD[OF assms this] show "eventually (\<lambda>x. dist (f x / g x) 0 < e) F"
  1157   proof eventually_elim
  1158     fix x assume "(norm (f x)) \<le> e/2 * (norm (g x))"
  1159     with e have "dist (f x / g x) 0 \<le> e/2"
  1160       by (cases "g x = 0") (simp_all add: dist_real_def norm_divide field_simps)
  1161     also from e have "... < e" by simp
  1162     finally show "dist (f x / g x) 0 < e" by simp
  1163   qed
  1164 qed
  1165 
  1166 lemma bigthetaI_tendsto_norm:
  1167   assumes c_not_0: "(c::real) \<noteq> 0"
  1168   assumes lim:     "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
  1169   shows   "f \<in> \<Theta>[F](g)"
  1170 proof (rule bigthetaI)
  1171   from c_not_0 have "\<bar>c\<bar> > 0" by simp
  1172   with lim have "eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<bar>c\<bar>) F"
  1173     by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  1174   hence g: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim (auto simp add: field_simps)
  1175 
  1176   from lim g show "f \<in> O[F](g)" by (rule bigoI_tendsto_norm)
  1177   from c_not_0 and lim show "f \<in> \<Omega>[F](g)" by (rule bigomegaI_tendsto_norm)
  1178 qed
  1179 
  1180 lemma bigthetaI_tendsto:
  1181   assumes c_not_0: "(c::real) \<noteq> 0"
  1182   assumes lim:     "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
  1183   shows   "f \<in> \<Theta>[F](g)"
  1184   using assms by (intro bigthetaI_tendsto_norm[OF _ tendsto_norm, of "c"]) simp_all
  1185 
  1186 lemma tendsto_add_smallo:
  1187   assumes "(f1 \<longlongrightarrow> a) F"
  1188   assumes "f2 \<in> o[F](f1)"
  1189   shows   "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
  1190 proof (subst filterlim_cong[OF refl refl])
  1191   from landau_o.smallD[OF assms(2) zero_less_one] 
  1192     have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)) F" by simp
  1193   thus "eventually (\<lambda>x. f1 x + f2 x = f1 x * (1 + f2 x / f1 x)) F"
  1194     by eventually_elim (auto simp: field_simps)
  1195 next
  1196   from assms(1) show "((\<lambda>x. f1 x * (1 + f2 x / f1 x)) \<longlongrightarrow> a) F"
  1197     by (force intro: tendsto_eq_intros smalloD_tendsto[OF assms(2)])
  1198 qed
  1199 
  1200 lemma tendsto_diff_smallo:
  1201   shows "(f1 \<longlongrightarrow> a) F \<Longrightarrow> f2 \<in> o[F](f1) \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
  1202   using tendsto_add_smallo[of f1 a F "\<lambda>x. -f2 x"] by simp
  1203 
  1204 lemma tendsto_add_smallo_iff:
  1205   assumes "f2 \<in> o[F](f1)"
  1206   shows   "(f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
  1207 proof
  1208   assume "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
  1209   hence "((\<lambda>x. f1 x + f2 x - f2 x) \<longlongrightarrow> a) F"
  1210     by (rule tendsto_diff_smallo) (simp add: landau_o.small.plus_absorb2 assms)
  1211   thus "(f1 \<longlongrightarrow> a) F" by simp
  1212 qed (rule tendsto_add_smallo[OF _ assms])
  1213 
  1214 lemma tendsto_diff_smallo_iff:
  1215   shows "f2 \<in> o[F](f1) \<Longrightarrow> (f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
  1216   using tendsto_add_smallo_iff[of "\<lambda>x. -f2 x" F f1 a] by simp
  1217 
  1218 lemma tendsto_divide_smallo:
  1219   assumes "((\<lambda>x. f1 x / g1 x) \<longlongrightarrow> a) F"
  1220   assumes "f2 \<in> o[F](f1)" "g2 \<in> o[F](g1)"
  1221   assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
  1222   shows   "((\<lambda>x. (f1 x + f2 x) / (g1 x + g2 x)) \<longlongrightarrow> a) F" (is "(?f \<longlongrightarrow> _) _")
  1223 proof (subst tendsto_cong)
  1224   let ?f' = "\<lambda>x. (f1 x / g1 x) * (1 + f2 x / f1 x) / (1 + g2 x / g1 x)"
  1225 
  1226   have "(?f' \<longlongrightarrow> a * (1 + 0) / (1 + 0)) F"
  1227   by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const 
  1228         smalloD_tendsto[OF assms(2)] smalloD_tendsto[OF assms(3)])+ simp_all
  1229   thus "(?f' \<longlongrightarrow> a) F" by simp
  1230 
  1231   have "(1/2::real) > 0" by simp
  1232   from landau_o.smallD[OF assms(2) this] landau_o.smallD[OF assms(3) this]
  1233     have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)/2) F"
  1234          "eventually (\<lambda>x. norm (g2 x) \<le> norm (g1 x)/2) F" by simp_all
  1235   with assms(4) show "eventually (\<lambda>x. ?f x = ?f' x) F"
  1236   proof eventually_elim
  1237     fix x assume A: "norm (f2 x) \<le> norm (f1 x)/2" and 
  1238                  B: "norm (g2 x) \<le> norm (g1 x)/2" and C: "g1 x \<noteq> 0"
  1239     show "?f x = ?f' x"
  1240     proof (cases "f1 x = 0")
  1241       assume D: "f1 x \<noteq> 0"
  1242       from D have "f1 x + f2 x = f1 x * (1 + f2 x/f1 x)" by (simp add: field_simps)
  1243       moreover from C have "g1 x + g2 x = g1 x * (1 + g2 x/g1 x)" by (simp add: field_simps)
  1244       ultimately have "?f x = (f1 x * (1 + f2 x/f1 x)) / (g1 x * (1 + g2 x/g1 x))" by (simp only:)
  1245       also have "... = ?f' x" by simp
  1246       finally show ?thesis .
  1247     qed (insert A, simp)
  1248   qed
  1249 qed
  1250 
  1251 
  1252 lemma bigo_powr:
  1253   fixes f :: "'a \<Rightarrow> real"
  1254   assumes "f \<in> O[F](g)" "p \<ge> 0"
  1255   shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)"
  1256 proof-
  1257   from assms(1) guess c by (elim landau_o.bigE landau_omega.bigE IntE)
  1258   note c = this
  1259   from c(2) assms(2) have "eventually (\<lambda>x. (norm (f x)) powr p \<le> (c * (norm (g x))) powr p) F"
  1260     by (auto elim!: eventually_mono intro!: powr_mono2)
  1261   thus "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" using c(1)
  1262     by (intro bigoI[of _ "c powr p"]) (simp_all add: powr_mult)
  1263 qed
  1264 
  1265 lemma smallo_powr:
  1266   fixes f :: "'a \<Rightarrow> real"
  1267   assumes "f \<in> o[F](g)" "p > 0"
  1268   shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)"
  1269 proof (rule landau_o.smallI)
  1270   fix c :: real assume c: "c > 0"
  1271   hence "c powr (1/p) > 0" by simp
  1272   from landau_o.smallD[OF assms(1) this] 
  1273   show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F"
  1274   proof eventually_elim
  1275     fix x assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))"
  1276     with assms(2) have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p"
  1277       by (intro powr_mono2) simp_all
  1278     also from assms(2) c have "... = c * (norm (g x)) powr p"
  1279       by (simp add: field_simps powr_mult powr_powr)
  1280     finally show "norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)" by simp
  1281   qed
  1282 qed
  1283 
  1284 lemma smallo_powr_nonneg:
  1285   fixes f :: "'a \<Rightarrow> real"
  1286   assumes "f \<in> o[F](g)" "p > 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
  1287   shows   "(\<lambda>x. f x powr p) \<in> o[F](\<lambda>x. g x powr p)"
  1288 proof -
  1289   from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
  1290     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1291   also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro smallo_powr) fact+
  1292   also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
  1293     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1294   finally show ?thesis .
  1295 qed
  1296 
  1297 lemma bigtheta_powr:
  1298   fixes f :: "'a \<Rightarrow> real"
  1299   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)"
  1300 apply (cases "p < 0")
  1301 apply (subst bigtheta_inverse[symmetric], subst (1 2) powr_minus[symmetric])
  1302 unfolding bigtheta_def apply (auto simp: bigomega_iff_bigo intro!: bigo_powr)
  1303 done
  1304 
  1305 lemma bigo_powr_nonneg:
  1306   fixes f :: "'a \<Rightarrow> real"
  1307   assumes "f \<in> O[F](g)" "p \<ge> 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
  1308   shows   "(\<lambda>x. f x powr p) \<in> O[F](\<lambda>x. g x powr p)"
  1309 proof -
  1310   from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
  1311     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1312   also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro bigo_powr) fact+
  1313   also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
  1314     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1315   finally show ?thesis .
  1316 qed
  1317 
  1318 lemma zero_in_smallo [simp]: "(\<lambda>_. 0) \<in> o[F](f)"
  1319   by (intro landau_o.smallI) simp_all
  1320 
  1321 lemma zero_in_bigo [simp]: "(\<lambda>_. 0) \<in> O[F](f)"
  1322   by (intro landau_o.bigI[of 1]) simp_all
  1323 
  1324 lemma in_bigomega_zero [simp]: "f \<in> \<Omega>[F](\<lambda>x. 0)"
  1325   by (rule landau_omega.bigI[of 1]) simp_all
  1326 
  1327 lemma in_smallomega_zero [simp]: "f \<in> \<omega>[F](\<lambda>x. 0)"
  1328   by (simp add: smallomega_iff_smallo)
  1329 
  1330 
  1331 lemma in_smallo_zero_iff [simp]: "f \<in> o[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1332 proof
  1333   assume "f \<in> o[F](\<lambda>_. 0)"
  1334   from landau_o.smallD[OF this, of 1] show "eventually (\<lambda>x. f x = 0) F" by simp
  1335 next
  1336   assume "eventually (\<lambda>x. f x = 0) F"
  1337   hence "\<forall>c>0. eventually (\<lambda>x. (norm (f x)) \<le> c * \<bar>0\<bar>) F" by simp
  1338   thus "f \<in> o[F](\<lambda>_. 0)" unfolding smallo_def by simp
  1339 qed
  1340 
  1341 lemma in_bigo_zero_iff [simp]: "f \<in> O[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1342 proof
  1343   assume "f \<in> O[F](\<lambda>_. 0)"
  1344   thus "eventually (\<lambda>x. f x = 0) F" by (elim landau_o.bigE) simp
  1345 next
  1346   assume "eventually (\<lambda>x. f x = 0) F"
  1347   hence "eventually (\<lambda>x. (norm (f x)) \<le> 1 * \<bar>0\<bar>) F" by simp
  1348   thus "f \<in> O[F](\<lambda>_. 0)" by (intro landau_o.bigI[of 1]) simp_all
  1349 qed
  1350 
  1351 lemma zero_in_smallomega_iff [simp]: "(\<lambda>_. 0) \<in> \<omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1352   by (simp add: smallomega_iff_smallo)
  1353 
  1354 lemma zero_in_bigomega_iff [simp]: "(\<lambda>_. 0) \<in> \<Omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1355   by (simp add: bigomega_iff_bigo)
  1356 
  1357 lemma zero_in_bigtheta_iff [simp]: "(\<lambda>_. 0) \<in> \<Theta>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1358   unfolding bigtheta_def by simp
  1359 
  1360 lemma in_bigtheta_zero_iff [simp]: "f \<in> \<Theta>[F](\<lambda>x. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  1361   unfolding bigtheta_def by simp
  1362 
  1363 
  1364 lemma cmult_in_bigo_iff    [simp]:  "(\<lambda>x. c * f x) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
  1365   and cmult_in_bigo_iff'   [simp]:  "(\<lambda>x. f x * c) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
  1366   and cmult_in_smallo_iff  [simp]:  "(\<lambda>x. c * f x) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
  1367   and cmult_in_smallo_iff' [simp]: "(\<lambda>x. f x * c) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
  1368   by (cases "c = 0", simp, simp)+
  1369 
  1370 lemma bigo_const [simp]: "(\<lambda>_. c) \<in> O[F](\<lambda>_. 1)" by (rule bigoI[of _ "norm c"]) simp
  1371 
  1372 lemma bigo_const_iff [simp]: "(\<lambda>_. c1) \<in> O[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 = 0 \<or> c2 \<noteq> 0"
  1373   by (cases "c1 = 0"; cases "c2 = 0")
  1374      (auto simp: bigo_def eventually_False intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
  1375 
  1376 lemma bigomega_const_iff [simp]: "(\<lambda>_. c1) \<in> \<Omega>[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 \<noteq> 0 \<or> c2 = 0"
  1377   by (cases "c1 = 0"; cases "c2 = 0")
  1378      (auto simp: bigomega_def eventually_False mult_le_0_iff 
  1379            intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
  1380 
  1381 lemma smallo_real_nat_transfer:
  1382   "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))"
  1383   by (rule landau_o.small.compose[OF _ filterlim_real_sequentially])
  1384 
  1385 lemma bigo_real_nat_transfer:
  1386   "(f :: real \<Rightarrow> real) \<in> O(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> O(\<lambda>x. g (real x))"
  1387   by (rule landau_o.big.compose[OF _ filterlim_real_sequentially])
  1388 
  1389 lemma smallomega_real_nat_transfer:
  1390   "(f :: real \<Rightarrow> real) \<in> \<omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<omega>(\<lambda>x. g (real x))"
  1391   by (rule landau_omega.small.compose[OF _ filterlim_real_sequentially])
  1392 
  1393 lemma bigomega_real_nat_transfer:
  1394   "(f :: real \<Rightarrow> real) \<in> \<Omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Omega>(\<lambda>x. g (real x))"
  1395   by (rule landau_omega.big.compose[OF _ filterlim_real_sequentially])
  1396 
  1397 lemma bigtheta_real_nat_transfer:
  1398   "(f :: real \<Rightarrow> real) \<in> \<Theta>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Theta>(\<lambda>x. g (real x))"
  1399   unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast
  1400 
  1401 lemmas landau_real_nat_transfer [intro] = 
  1402   bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer 
  1403   smallomega_real_nat_transfer bigtheta_real_nat_transfer
  1404 
  1405 
  1406 lemma landau_symbol_if_at_top_eq [simp]:
  1407   assumes "landau_symbol L L' Lr"
  1408   shows   "L at_top (\<lambda>x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)"
  1409 apply (rule landau_symbol.cong[OF assms])
  1410 using less_add_one[of a] apply (auto intro: eventually_mono  eventually_ge_at_top[of "a + 1"])
  1411 done
  1412 
  1413 lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq]
  1414 
  1415 
  1416 
  1417 lemma sum_in_smallo:
  1418   assumes "f \<in> o[F](h)" "g \<in> o[F](h)"
  1419   shows   "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)"
  1420 proof-
  1421   {
  1422     fix f g assume fg: "f \<in> o[F](h)" "g \<in> o[F](h)"
  1423     have "(\<lambda>x. f x + g x) \<in> o[F](h)"
  1424     proof (rule landau_o.smallI)
  1425       fix c :: real assume "c > 0"
  1426       hence "c/2 > 0" by simp
  1427       from fg[THEN landau_o.smallD[OF _ this]]
  1428       show "eventually (\<lambda>x. norm (f x + g x) \<le> c * (norm (h x))) F"
  1429         by eventually_elim (auto intro: order.trans[OF norm_triangle_ineq])
  1430     qed
  1431   }
  1432   from this[of f g] this[of f "\<lambda>x. -g x"] assms
  1433     show "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" by simp_all
  1434 qed
  1435 
  1436 lemma big_sum_in_smallo:
  1437   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> o[F](g)"
  1438   shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> o[F](g)"
  1439   using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_smallo)
  1440 
  1441 lemma sum_in_bigo:
  1442   assumes "f \<in> O[F](h)" "g \<in> O[F](h)"
  1443   shows   "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)"
  1444 proof-
  1445   {
  1446     fix f g assume fg: "f \<in> O[F](h)" "g \<in> O[F](h)"
  1447     from fg(1) guess c1 by (elim landau_o.bigE) note c1 = this
  1448     from fg(2) guess c2 by (elim landau_o.bigE) note c2 = this
  1449     from c1(2) c2(2) have "eventually (\<lambda>x. norm (f x + g x) \<le> (c1 + c2) * (norm (h x))) F"
  1450       by eventually_elim (auto simp: algebra_simps intro: order.trans[OF norm_triangle_ineq])
  1451     hence "(\<lambda>x. f x + g x) \<in> O[F](h)" by (rule bigoI)
  1452   }
  1453   from this[of f g] this[of f "\<lambda>x. -g x"] assms
  1454     show "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" by simp_all
  1455 qed
  1456 
  1457 lemma big_sum_in_bigo:
  1458   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> O[F](g)"
  1459   shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"
  1460   using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)
  1461 
  1462 context landau_symbol
  1463 begin
  1464 
  1465 lemma mult_cancel_left:
  1466   assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
  1467   notes   [trans] = bigtheta_trans1 bigtheta_trans2
  1468   shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f2 \<in> L F (g2)"
  1469 proof
  1470   assume A: "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
  1471   from assms have nz: "eventually (\<lambda>x. f1 x \<noteq> 0) F" by (simp add: eventually_nonzero_bigtheta)
  1472   hence "f2 \<in> \<Theta>[F](\<lambda>x. f1 x * f2 x / f1 x)"
  1473     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1474   also from A assms nz have "(\<lambda>x. f1 x * f2 x / f1 x) \<in> L F (\<lambda>x. g1 x * g2 x / f1 x)" 
  1475     by (intro divide_right) simp_all
  1476   also from assms nz have "(\<lambda>x. g1 x * g2 x / f1 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x / g1 x)"
  1477     by (intro landau_theta.mult landau_theta.divide) (simp_all add: bigtheta_sym)
  1478   also from assms have "(\<lambda>x. g1 x * g2 x / g1 x) \<in> \<Theta>[F](g2)"
  1479     by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  1480   finally show "f2 \<in> L F (g2)" .
  1481 next
  1482   assume "f2 \<in> L F (g2)"
  1483   hence "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. f1 x * g2 x)" by (rule mult_left)
  1484   also have "(\<lambda>x. f1 x * g2 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x)"
  1485     by (intro landau_theta.mult_right assms)
  1486   finally show "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" .
  1487 qed
  1488 
  1489 lemma mult_cancel_right:
  1490   assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
  1491   shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
  1492   by (subst (1 2) mult.commute) (rule mult_cancel_left[OF assms])
  1493 
  1494 lemma divide_cancel_right:
  1495   assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
  1496   shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
  1497   by (subst (1 2) divide_inverse, intro mult_cancel_right bigtheta_inverse) (simp_all add: assms)
  1498 
  1499 lemma divide_cancel_left:
  1500   assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
  1501   shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> 
  1502              (\<lambda>x. inverse (f2 x)) \<in> L F (\<lambda>x. inverse (g2 x))"
  1503   by (simp only: divide_inverse mult_cancel_left[OF assms])
  1504 
  1505 end
  1506 
  1507 
  1508 lemma powr_smallo_iff:
  1509   assumes "filterlim g at_top F" "F \<noteq> bot"
  1510   shows   "(\<lambda>x. g x powr p :: real) \<in> o[F](\<lambda>x. g x powr q) \<longleftrightarrow> p < q"
  1511 proof-
  1512   from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
  1513   hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
  1514   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)"
  1515   proof
  1516     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)"
  1517     from landau_o.big_small_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
  1518     with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
  1519     thus False by (simp add: eventually_False assms)
  1520   qed
  1521   show ?thesis
  1522   proof (cases p q rule: linorder_cases)
  1523     assume "p < q"
  1524     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
  1525       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
  1526     with \<open>p < q\<close> show ?thesis by auto
  1527   next
  1528     assume "p = q"
  1529     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
  1530     with B \<open>p = q\<close> show ?thesis by auto
  1531   next
  1532     assume "p > q"
  1533     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
  1534       by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)
  1535     with B \<open>p > q\<close> show ?thesis by auto
  1536   qed
  1537 qed
  1538 
  1539 lemma powr_bigo_iff:
  1540   assumes "filterlim g at_top F" "F \<noteq> bot"
  1541   shows   "(\<lambda>x. g x powr p :: real) \<in> O[F](\<lambda>x. g x powr q) \<longleftrightarrow> p \<le> q"
  1542 proof-
  1543   from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
  1544   hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
  1545   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)"
  1546   proof
  1547     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)"
  1548     from landau_o.small_big_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
  1549     with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
  1550     thus False by (simp add: eventually_False assms)
  1551   qed
  1552   show ?thesis
  1553   proof (cases p q rule: linorder_cases)
  1554     assume "p < q"
  1555     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
  1556       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
  1557     with \<open>p < q\<close> show ?thesis by (auto intro: landau_o.small_imp_big)
  1558   next
  1559     assume "p = q"
  1560     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
  1561     with B \<open>p = q\<close> show ?thesis by auto
  1562   next
  1563     assume "p > q"
  1564     hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
  1565       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
  1566     with B \<open>p > q\<close> show ?thesis by (auto intro: landau_o.small_imp_big)
  1567   qed
  1568 qed
  1569 
  1570 lemma powr_bigtheta_iff: 
  1571   assumes "filterlim g at_top F" "F \<noteq> bot"
  1572   shows   "(\<lambda>x. g x powr p :: real) \<in> \<Theta>[F](\<lambda>x. g x powr q) \<longleftrightarrow> p = q"
  1573   using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff)
  1574 
  1575 
  1576 subsection \<open>Flatness of real functions\<close>
  1577 
  1578 text \<open>
  1579   Given two real-valued functions $f$ and $g$, we say that $f$ is flatter than $g$ if
  1580   any power of $f(x)$ is asymptotically dominated by any positive power of $g(x)$. This is
  1581   a useful notion since, given two products of powers of functions sorted by flatness, we can
  1582   compare them asymptotically by simply comparing the exponent lists lexicographically.
  1583 
  1584   A simple sufficient criterion for flatness it that $\ln f(x) \in o(\ln g(x))$, which we show
  1585   now.
  1586 \<close>
  1587 lemma ln_smallo_imp_flat:
  1588   fixes f g :: "real \<Rightarrow> real"
  1589   assumes lim_f: "filterlim f at_top at_top"
  1590   assumes lim_g: "filterlim g at_top at_top"
  1591   assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
  1592   assumes q: "q > 0"
  1593   shows   "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)"
  1594 proof (rule smalloI_tendsto)
  1595   from lim_f have "eventually (\<lambda>x. f x > 0) at_top" 
  1596     by (simp add: filterlim_at_top_dense)
  1597   hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp
  1598   
  1599   from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top"
  1600     by (simp add: filterlim_at_top_dense)
  1601   hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp
  1602   thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top"
  1603     by eventually_elim simp
  1604   
  1605   have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) = 
  1606                           p * ln (f x) - q * ln (g x)) at_top"
  1607     using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps)
  1608   have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top"
  1609     by (insert q)
  1610        (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult
  1611               tendsto_const tendsto_diff smalloD_tendsto[OF ln_o_ln] lim_g
  1612               filterlim_compose[OF ln_at_top] | simp)+
  1613   hence "filterlim (\<lambda>x. p * ln (f x) - q * ln (g x)) at_bot at_top"
  1614     by (subst (asm) filterlim_cong[OF refl refl eq])
  1615   hence *: "((\<lambda>x. exp (p * ln (f x) - q * ln (g x))) \<longlongrightarrow> 0) at_top"
  1616     by (rule filterlim_compose[OF exp_at_bot])
  1617   have eq: "eventually (\<lambda>x. exp (p * ln (f x) - q * ln (g x)) = f x powr p / g x powr q) at_top"
  1618     using f_nz g_nz by eventually_elim (simp add: powr_def exp_diff)
  1619   show "((\<lambda>x. f x powr p / g x powr q) \<longlongrightarrow> 0) at_top"
  1620     using * by (subst (asm) filterlim_cong[OF refl refl eq])
  1621 qed
  1622 
  1623 lemma ln_smallo_imp_flat':
  1624   fixes f g :: "real \<Rightarrow> real"
  1625   assumes lim_f: "filterlim f at_top at_top"
  1626   assumes lim_g: "filterlim g at_top at_top"
  1627   assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
  1628   assumes q: "q < 0"
  1629   shows   "(\<lambda>x. g x powr q) \<in> o(\<lambda>x. f x powr p)"
  1630 proof -
  1631   from lim_f lim_g have "eventually (\<lambda>x. f x > 0) at_top" "eventually (\<lambda>x. g x > 0) at_top"
  1632     by (simp_all add: filterlim_at_top_dense)
  1633   hence "eventually (\<lambda>x. f x \<noteq> 0) at_top" "eventually (\<lambda>x. g x \<noteq> 0) at_top"
  1634     by (auto elim: eventually_mono)
  1635   moreover from assms have "(\<lambda>x. f x powr -p) \<in> o(\<lambda>x. g x powr -q)"
  1636     by (intro ln_smallo_imp_flat assms) simp_all
  1637   ultimately show ?thesis unfolding powr_minus
  1638     by (simp add: landau_o.small.inverse_cancel)
  1639 qed
  1640 
  1641 
  1642 subsection \<open>Asymptotic Equivalence\<close>
  1643 
  1644 (* TODO Move *)
  1645 lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
  1646   by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
  1647 
  1648 named_theorems asymp_equiv_intros
  1649 named_theorems asymp_equiv_simps
  1650 
  1651 definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  1652   (\<open>_ \<sim>[_] _\<close> [51, 10, 51] 50)
  1653   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"
  1654 
  1655 abbreviation (input) asymp_equiv_at_top where
  1656   "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"
  1657 
  1658 bundle asymp_equiv_notation
  1659 begin
  1660 notation asymp_equiv_at_top (infix \<open>\<sim>\<close> 50) 
  1661 end
  1662 
  1663 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"
  1664   by (simp add: asymp_equiv_def)
  1665 
  1666 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"
  1667   by (simp add: asymp_equiv_def)
  1668 
  1669 lemma asymp_equiv_filtermap_iff:
  1670   "f \<sim>[filtermap h F] g \<longleftrightarrow> (\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
  1671   by (simp add: asymp_equiv_def filterlim_filtermap)
  1672 
  1673 lemma asymp_equiv_refl [simp, asymp_equiv_intros]: "f \<sim>[F] f"
  1674 proof (intro asymp_equivI)
  1675   have "eventually (\<lambda>x. 1 = (if f x = 0 \<and> f x = 0 then 1 else f x / f x)) F"
  1676     by (intro always_eventually) simp
  1677   moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
  1678   ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
  1679     by (rule Lim_transform_eventually)
  1680 qed
  1681 
  1682 lemma asymp_equiv_symI: 
  1683   assumes "f \<sim>[F] g"
  1684   shows   "g \<sim>[F] f"
  1685   using tendsto_inverse[OF asymp_equivD[OF assms]]
  1686   by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong)
  1687 
  1688 lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f"
  1689   by (blast intro: asymp_equiv_symI)
  1690 
  1691 lemma asymp_equivI': 
  1692   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
  1693   shows   "f \<sim>[F] g"
  1694 proof (cases "F = bot")
  1695   case False
  1696   have "eventually (\<lambda>x. f x \<noteq> 0) F"
  1697   proof (rule ccontr)
  1698     assume "\<not>eventually (\<lambda>x. f x \<noteq> 0) F"
  1699     hence "frequently (\<lambda>x. f x = 0) F" by (simp add: frequently_def)
  1700     hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1)
  1701     from limit_frequently_eq[OF False this assms] show False by simp_all
  1702   qed
  1703   hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"
  1704     by eventually_elim simp
  1705   from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def 
  1706     by (rule Lim_transform_eventually)
  1707 qed (simp_all add: asymp_equiv_def)
  1708 
  1709 
  1710 lemma asymp_equiv_cong:
  1711   assumes "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
  1712   shows   "f1 \<sim>[F] g1 \<longleftrightarrow> f2 \<sim>[F] g2"
  1713   unfolding asymp_equiv_def
  1714 proof (rule tendsto_cong, goal_cases)
  1715   case 1
  1716   from assms show ?case by eventually_elim simp
  1717 qed
  1718 
  1719 lemma asymp_equiv_eventually_zeros:
  1720   fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
  1721   assumes "f \<sim>[F] g"
  1722   shows   "eventually (\<lambda>x. f x = 0 \<longleftrightarrow> g x = 0) F"
  1723 proof -
  1724   let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  1725   have "eventually (\<lambda>x. x \<noteq> 0) (nhds (1::'b))"
  1726     by (rule t1_space_nhds) auto
  1727   hence "eventually (\<lambda>x. x \<noteq> 0) (filtermap ?h F)"
  1728     using assms unfolding asymp_equiv_def filterlim_def
  1729     by (rule filter_leD [rotated])
  1730   hence "eventually (\<lambda>x. ?h x \<noteq> 0) F" by (simp add: eventually_filtermap)
  1731   thus ?thesis by eventually_elim (auto split: if_splits)
  1732 qed
  1733 
  1734 lemma asymp_equiv_transfer:
  1735   assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
  1736   shows   "f2 \<sim>[F] g2"
  1737   using assms(1) asymp_equiv_cong[OF assms(2,3)] by simp
  1738 
  1739 lemma asymp_equiv_transfer_trans [trans]:
  1740   assumes "(\<lambda>x. f x (h1 x)) \<sim>[F] (\<lambda>x. g x (h1 x))"
  1741   assumes "eventually (\<lambda>x. h1 x = h2 x) F"
  1742   shows   "(\<lambda>x. f x (h2 x)) \<sim>[F] (\<lambda>x. g x (h2 x))"
  1743   by (rule asymp_equiv_transfer[OF assms(1)]) (insert assms(2), auto elim!: eventually_mono)
  1744 
  1745 lemma asymp_equiv_trans [trans]:
  1746   fixes f g h
  1747   assumes "f \<sim>[F] g" "g \<sim>[F] h"
  1748   shows   "f \<sim>[F] h"
  1749 proof -
  1750   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  1751   from assms[THEN asymp_equiv_eventually_zeros]
  1752     have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
  1753   moreover from tendsto_mult[OF assms[THEN asymp_equivD]] 
  1754     have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
  1755   ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
  1756 qed
  1757 
  1758 lemma asymp_equiv_trans_lift1 [trans]:
  1759   assumes "a \<sim>[F] f b" "b \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
  1760   shows   "a \<sim>[F] f c"
  1761   using assms by (blast intro: asymp_equiv_trans)
  1762 
  1763 lemma asymp_equiv_trans_lift2 [trans]:
  1764   assumes "f a \<sim>[F] b" "a \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
  1765   shows   "f c \<sim>[F] b"
  1766   using asymp_equiv_symI[OF assms(3)[OF assms(2)]] assms(1)
  1767   by (blast intro: asymp_equiv_trans)
  1768 
  1769 lemma asymp_equivD_const:
  1770   assumes "f \<sim>[F] (\<lambda>_. c)"
  1771   shows   "(f \<longlongrightarrow> c) F"
  1772 proof (cases "c = 0")
  1773   case False
  1774   with tendsto_mult_right[OF asymp_equivD[OF assms], of c] show ?thesis by simp
  1775 next
  1776   case True
  1777   with asymp_equiv_eventually_zeros[OF assms] show ?thesis
  1778     by (simp add: Lim_eventually)
  1779 qed
  1780 
  1781 lemma asymp_equiv_refl_ev:
  1782   assumes "eventually (\<lambda>x. f x = g x) F"
  1783   shows   "f \<sim>[F] g"
  1784   by (intro asymp_equivI Lim_eventually)
  1785      (insert assms, auto elim!: eventually_mono)
  1786 
  1787 lemma asymp_equiv_sandwich:
  1788   fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"
  1789   assumes "eventually (\<lambda>x. f x \<ge> 0) F"
  1790   assumes "eventually (\<lambda>x. f x \<le> g x) F"
  1791   assumes "eventually (\<lambda>x. g x \<le> h x) F"
  1792   assumes "f \<sim>[F] h"
  1793   shows   "g \<sim>[F] f" "g \<sim>[F] h"
  1794 proof -
  1795   show "g \<sim>[F] f"
  1796   proof (rule asymp_equivI, rule tendsto_sandwich)
  1797     from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
  1798       show "eventually (\<lambda>n. (if h n = 0 \<and> f n = 0 then 1 else h n / f n) \<ge>
  1799                               (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
  1800         by eventually_elim (auto intro!: divide_right_mono)
  1801     from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
  1802       show "eventually (\<lambda>n. 1 \<le>
  1803                               (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
  1804         by eventually_elim (auto intro!: divide_right_mono)
  1805   qed (insert asymp_equiv_symI[OF assms(4)], simp_all add: asymp_equiv_def)
  1806   also note \<open>f \<sim>[F] h\<close>
  1807   finally show "g \<sim>[F] h" .
  1808 qed
  1809 
  1810 lemma asymp_equiv_imp_eventually_same_sign:
  1811   fixes f g :: "real \<Rightarrow> real"
  1812   assumes "f \<sim>[F] g"
  1813   shows   "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
  1814 proof -
  1815   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"
  1816     unfolding asymp_equiv_def by (rule tendsto_sgn) simp_all
  1817   from order_tendstoD(1)[OF this, of "1/2"]
  1818     have "eventually (\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x) > 1/2) F"
  1819     by simp
  1820   thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
  1821   proof eventually_elim
  1822     case (elim x)
  1823     thus ?case
  1824       by (cases "f x" "0 :: real" rule: linorder_cases; 
  1825           cases "g x" "0 :: real" rule: linorder_cases) simp_all
  1826   qed
  1827 qed
  1828 
  1829 lemma
  1830   fixes f g :: "_ \<Rightarrow> real"
  1831   assumes "f \<sim>[F] g"
  1832   shows   asymp_equiv_eventually_same_sign: "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" (is ?th1)
  1833     and   asymp_equiv_eventually_neg_iff:   "eventually (\<lambda>x. f x < 0 \<longleftrightarrow> g x < 0) F" (is ?th2)
  1834     and   asymp_equiv_eventually_pos_iff:   "eventually (\<lambda>x. f x > 0 \<longleftrightarrow> g x > 0) F" (is ?th3)
  1835 proof -
  1836   from assms have "filterlim (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) (nhds 1) F"
  1837     by (rule asymp_equivD)
  1838   from order_tendstoD(1)[OF this zero_less_one]
  1839     show ?th1 ?th2 ?th3
  1840     by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+
  1841 qed
  1842 
  1843 lemma asymp_equiv_tendsto_transfer:
  1844   assumes "f \<sim>[F] g" and "(f \<longlongrightarrow> c) F"
  1845   shows   "(g \<longlongrightarrow> c) F"
  1846 proof -
  1847   let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"
  1848   have "eventually (\<lambda>x. ?h x = g x) F"
  1849     using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
  1850   moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
  1851   hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"
  1852     by (rule asymp_equivD)
  1853   from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp
  1854   ultimately show ?thesis by (rule Lim_transform_eventually)
  1855 qed
  1856 
  1857 lemma tendsto_asymp_equiv_cong:
  1858   assumes "f \<sim>[F] g"
  1859   shows   "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"
  1860 proof -
  1861   {
  1862     fix f g :: "'a \<Rightarrow> 'b"
  1863     assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"
  1864     have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"
  1865       using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp
  1866     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"
  1867       by (intro tendsto_intros asymp_equivD *)
  1868     ultimately have "(f \<longlongrightarrow> c * 1) F"
  1869       by (rule Lim_transform_eventually)
  1870   }
  1871   from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym)
  1872 qed
  1873 
  1874 
  1875 lemma smallo_imp_eventually_sgn:
  1876   fixes f g :: "real \<Rightarrow> real"
  1877   assumes "g \<in> o(f)"
  1878   shows   "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top"
  1879 proof -
  1880   have "0 < (1/2 :: real)" by simp
  1881   from landau_o.smallD[OF assms, OF this] 
  1882     have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp
  1883   thus ?thesis
  1884   proof eventually_elim
  1885     case (elim x)
  1886     thus ?case
  1887       by (cases "f x" "0::real" rule: linorder_cases; 
  1888           cases "f x + g x" "0::real" rule: linorder_cases) simp_all
  1889   qed
  1890 qed
  1891 
  1892 context
  1893 begin
  1894 
  1895 private lemma asymp_equiv_add_rightI:
  1896   assumes "f \<sim>[F] g" "h \<in> o[F](g)"
  1897   shows   "(\<lambda>x. f x + h x) \<sim>[F] g"
  1898 proof -
  1899   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  1900   from landau_o.smallD[OF assms(2) zero_less_one]
  1901     have ev: "eventually (\<lambda>x. g x = 0 \<longrightarrow> h x = 0) F" by eventually_elim auto
  1902   have "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1) F"
  1903     unfolding asymp_equiv_def using ev
  1904     by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps)
  1905   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1 + 0) F" by simp
  1906   also have \<dots> by (intro tendsto_intros asymp_equivD assms smalloD_tendsto)
  1907   finally show "(\<lambda>x. f x + h x) \<sim>[F] g" .
  1908 qed
  1909 
  1910 lemma asymp_equiv_add_right [asymp_equiv_simps]:
  1911   assumes "h \<in> o[F](g)"
  1912   shows   "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
  1913 proof
  1914   assume "(\<lambda>x. f x + h x) \<sim>[F] g"
  1915   from asymp_equiv_add_rightI[OF this, of "\<lambda>x. -h x"] assms show "f \<sim>[F] g"
  1916     by simp
  1917 qed (simp_all add: asymp_equiv_add_rightI assms)
  1918 
  1919 end
  1920 
  1921 lemma asymp_equiv_add_left [asymp_equiv_simps]: 
  1922   assumes "h \<in> o[F](g)"
  1923   shows   "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
  1924   using asymp_equiv_add_right[OF assms] by (simp add: add.commute)
  1925 
  1926 lemma asymp_equiv_add_right' [asymp_equiv_simps]:
  1927   assumes "h \<in> o[F](g)"
  1928   shows   "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f"
  1929   using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym)
  1930   
  1931 lemma asymp_equiv_add_left' [asymp_equiv_simps]:
  1932   assumes "h \<in> o[F](g)"
  1933   shows   "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f"
  1934   using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym)
  1935 
  1936 lemma smallo_imp_asymp_equiv:
  1937   assumes "(\<lambda>x. f x - g x) \<in> o[F](g)"
  1938   shows   "f \<sim>[F] g"
  1939 proof -
  1940   from assms have "(\<lambda>x. f x - g x + g x) \<sim>[F] g"
  1941     by (subst asymp_equiv_add_left) simp_all
  1942   thus ?thesis by simp
  1943 qed
  1944 
  1945 lemma asymp_equiv_uminus [asymp_equiv_intros]:
  1946   "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. -f x) \<sim>[F] (\<lambda>x. -g x)"
  1947   by (simp add: asymp_equiv_def cong: if_cong)
  1948 
  1949 lemma asymp_equiv_uminus_iff [asymp_equiv_simps]:
  1950   "(\<lambda>x. -f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] (\<lambda>x. -g x)"
  1951   by (simp add: asymp_equiv_def cong: if_cong)
  1952 
  1953 lemma asymp_equiv_mult [asymp_equiv_intros]:
  1954   fixes f1 f2 g1 g2 :: "'a \<Rightarrow> 'b :: real_normed_field"
  1955   assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
  1956   shows   "(\<lambda>x. f1 x * f2 x) \<sim>[F] (\<lambda>x. g1 x * g2 x)"
  1957 proof -
  1958   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  1959   let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x
  1960                    else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)"
  1961   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"
  1962   {
  1963     fix f g :: "'a \<Rightarrow> 'b" assume "f \<sim>[F] g"
  1964     have "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F"
  1965       by (rule tendsto_eq_intros refl asymp_equivD[OF \<open>f \<sim>[F] g\<close>])+ simp_all
  1966   } note A = this    
  1967 
  1968   from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"
  1969     by (intro tendsto_mult asymp_equivD)
  1970   moreover {
  1971     have "eventually (\<lambda>x. ?S x = ?S' x) F"
  1972       using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
  1973     moreover have "(?S \<longlongrightarrow> 0) F"
  1974       by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])
  1975          (auto intro: le_infI1 le_infI2)
  1976     ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)
  1977   }
  1978   ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"
  1979     by (rule Lim_transform)
  1980   thus ?thesis by (simp add: asymp_equiv_def)
  1981 qed
  1982 
  1983 lemma asymp_equiv_power [asymp_equiv_intros]:
  1984   "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)"
  1985   by (induction n) (simp_all add: asymp_equiv_mult)
  1986 
  1987 lemma asymp_equiv_inverse [asymp_equiv_intros]:
  1988   assumes "f \<sim>[F] g"
  1989   shows   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
  1990 proof -
  1991   from tendsto_inverse[OF asymp_equivD[OF assms]]
  1992     have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) \<longlongrightarrow> 1) F"
  1993     by (simp add: if_distrib cong: if_cong)
  1994   also have "(\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) =
  1995                (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else inverse (f x) / inverse (g x))"
  1996     by (intro ext) (simp add: field_simps)
  1997   finally show ?thesis by (simp add: asymp_equiv_def)
  1998 qed
  1999 
  2000 lemma asymp_equiv_inverse_iff [asymp_equiv_simps]:
  2001   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<sim>[F] g"
  2002 proof
  2003   assume "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
  2004   hence "(\<lambda>x. inverse (inverse (f x))) \<sim>[F] (\<lambda>x. inverse (inverse (g x)))" (is ?P)
  2005     by (rule asymp_equiv_inverse)
  2006   also have "?P \<longleftrightarrow> f \<sim>[F] g" by (intro asymp_equiv_cong) simp_all
  2007   finally show "f \<sim>[F] g" .
  2008 qed (simp_all add: asymp_equiv_inverse)
  2009 
  2010 lemma asymp_equiv_divide [asymp_equiv_intros]:
  2011   assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
  2012   shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
  2013   using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
  2014 
  2015 lemma asymp_equiv_compose [asymp_equiv_intros]:
  2016   assumes "f \<sim>[G] g" "filterlim h G F"
  2017   shows   "f \<circ> h \<sim>[F] g \<circ> h"
  2018 proof -
  2019   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  2020   have "f \<circ> h \<sim>[F] g \<circ> h \<longleftrightarrow> ((?T f g \<circ> h) \<longlongrightarrow> 1) F"
  2021     by (simp add: asymp_equiv_def o_def)
  2022   also have "\<dots> \<longleftrightarrow> (?T f g \<longlongrightarrow> 1) (filtermap h F)"
  2023     by (rule tendsto_compose_filtermap)
  2024   also have "\<dots>"
  2025     by (rule tendsto_mono[of _ G]) (insert assms, simp_all add: asymp_equiv_def filterlim_def)
  2026   finally show ?thesis .
  2027 qed
  2028 
  2029 lemma asymp_equiv_compose':
  2030   assumes "f \<sim>[G] g" "filterlim h G F"
  2031   shows   "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
  2032   using asymp_equiv_compose[OF assms] by (simp add: o_def)
  2033   
  2034 lemma asymp_equiv_powr_real [asymp_equiv_intros]:
  2035   fixes f g :: "'a \<Rightarrow> real"
  2036   assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
  2037   shows   "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"
  2038 proof -
  2039   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  2040   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"
  2041     using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)
  2042     by eventually_elim (auto simp: powr_divide)
  2043   moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
  2044     by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
  2045   hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
  2046   ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
  2047 qed
  2048 
  2049 lemma asymp_equiv_norm [asymp_equiv_intros]:
  2050   fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
  2051   assumes "f \<sim>[F] g"
  2052   shows   "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))"
  2053   using tendsto_norm[OF asymp_equivD[OF assms]] 
  2054   by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong)
  2055 
  2056 lemma asymp_equiv_abs_real [asymp_equiv_intros]:
  2057   fixes f g :: "'a \<Rightarrow> real"
  2058   assumes "f \<sim>[F] g"
  2059   shows   "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)"
  2060   using tendsto_rabs[OF asymp_equivD[OF assms]] 
  2061   by (simp add: if_distrib asymp_equiv_def cong: if_cong)
  2062 
  2063 lemma asymp_equiv_imp_eventually_le:
  2064   assumes "f \<sim>[F] g" "c > 1"
  2065   shows   "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"
  2066 proof -
  2067   from order_tendstoD(2)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
  2068        asymp_equiv_eventually_zeros[OF assms(1)]
  2069     show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
  2070 qed
  2071 
  2072 lemma asymp_equiv_imp_eventually_ge:
  2073   assumes "f \<sim>[F] g" "c < 1"
  2074   shows   "eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F"
  2075 proof -
  2076   from order_tendstoD(1)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
  2077        asymp_equiv_eventually_zeros[OF assms(1)]
  2078     show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
  2079 qed
  2080 
  2081 lemma asymp_equiv_imp_bigo:
  2082   assumes "f \<sim>[F] g"
  2083   shows   "f \<in> O[F](g)"
  2084 proof (rule bigoI)
  2085   have "(3/2::real) > 1" by simp
  2086   from asymp_equiv_imp_eventually_le[OF assms this]
  2087     show "eventually (\<lambda>x. norm (f x) \<le> 3/2 * norm (g x)) F"
  2088     by eventually_elim simp
  2089 qed
  2090 
  2091 lemma asymp_equiv_imp_bigomega:
  2092   "f \<sim>[F] g \<Longrightarrow> f \<in> \<Omega>[F](g)"
  2093   using asymp_equiv_imp_bigo[of g F f] by (simp add: asymp_equiv_sym bigomega_iff_bigo)
  2094 
  2095 lemma asymp_equiv_imp_bigtheta:
  2096   "f \<sim>[F] g \<Longrightarrow> f \<in> \<Theta>[F](g)"
  2097   by (intro bigthetaI asymp_equiv_imp_bigo asymp_equiv_imp_bigomega)
  2098 
  2099 lemma asymp_equiv_at_infinity_transfer:
  2100   assumes "f \<sim>[F] g" "filterlim f at_infinity F"
  2101   shows   "filterlim g at_infinity F"
  2102 proof -
  2103   from assms(1) have "g \<in> \<Theta>[F](f)" by (rule asymp_equiv_imp_bigtheta[OF asymp_equiv_symI])
  2104   also from assms have "f \<in> \<omega>[F](\<lambda>_. 1)" by (simp add: smallomega_1_conv_filterlim)
  2105   finally show ?thesis by (simp add: smallomega_1_conv_filterlim)
  2106 qed
  2107 
  2108 lemma asymp_equiv_at_top_transfer:
  2109   fixes f g :: "_ \<Rightarrow> real"
  2110   assumes "f \<sim>[F] g" "filterlim f at_top F"
  2111   shows   "filterlim g at_top F"
  2112 proof (rule filterlim_at_infinity_imp_filterlim_at_top)
  2113   show "filterlim g at_infinity F"
  2114     by (rule asymp_equiv_at_infinity_transfer[OF assms(1) filterlim_mono[OF assms(2)]])
  2115        (auto simp: at_top_le_at_infinity)
  2116   from assms(2) have "eventually (\<lambda>x. f x > 0) F"
  2117     using filterlim_at_top_dense by blast
  2118   with asymp_equiv_eventually_pos_iff[OF assms(1)] show "eventually (\<lambda>x. g x > 0) F"
  2119     by eventually_elim blast
  2120 qed
  2121 
  2122 lemma asymp_equiv_at_bot_transfer:
  2123   fixes f g :: "_ \<Rightarrow> real"
  2124   assumes "f \<sim>[F] g" "filterlim f at_bot F"
  2125   shows   "filterlim g at_bot F"
  2126   unfolding filterlim_uminus_at_bot
  2127   by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"])
  2128      (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus)  
  2129 
  2130 lemma asymp_equivI'_const:
  2131   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0"
  2132   shows   "f \<sim>[F] (\<lambda>x. c * g x)"
  2133   using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2)
  2134   by (intro asymp_equivI') (simp add: field_simps)
  2135 
  2136 lemma asymp_equivI'_inverse_const:
  2137   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> inverse c) F" "c \<noteq> 0"
  2138   shows   "(\<lambda>x. c * f x) \<sim>[F] g"
  2139   using tendsto_mult[OF assms(1) tendsto_const[of "c"]] assms(2)
  2140   by (intro asymp_equivI') (simp add: field_simps)
  2141 
  2142 lemma filterlim_at_bot_imp_at_infinity: "filterlim f at_bot F \<Longrightarrow> filterlim f at_infinity F"
  2143   for f :: "_ \<Rightarrow> real" using at_bot_le_at_infinity filterlim_mono by blast
  2144 
  2145 lemma asymp_equiv_imp_diff_smallo:
  2146   assumes "f \<sim>[F] g"
  2147   shows   "(\<lambda>x. f x - g x) \<in> o[F](g)"
  2148 proof (rule landau_o.smallI)
  2149   fix c :: real assume "c > 0"
  2150   hence c: "min c 1 > 0" by simp
  2151   let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
  2152   from assms have "((\<lambda>x. ?h x - 1) \<longlongrightarrow> 1 - 1) F"
  2153     by (intro tendsto_diff asymp_equivD tendsto_const)
  2154   from tendstoD[OF this c] show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
  2155   proof eventually_elim
  2156     case (elim x)
  2157     from elim have "norm (f x - g x) \<le> norm (f x / g x - 1) * norm (g x)"
  2158       by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps)
  2159     also have "norm (f x / g x - 1) * norm (g x) \<le> c * norm (g x)" using elim
  2160       by (auto split: if_splits simp: mult_right_mono)
  2161     finally show ?case .
  2162   qed
  2163 qed
  2164 
  2165 lemma asymp_equiv_altdef:
  2166   "f \<sim>[F] g \<longleftrightarrow> (\<lambda>x. f x - g x) \<in> o[F](g)"
  2167   by (rule iffI[OF asymp_equiv_imp_diff_smallo smallo_imp_asymp_equiv])
  2168 
  2169 lemma asymp_equiv_0_left_iff [simp]: "(\<lambda>_. 0) \<sim>[F] f \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  2170   and asymp_equiv_0_right_iff [simp]: "f \<sim>[F] (\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
  2171   by (simp_all add: asymp_equiv_altdef landau_o.small_refl_iff)
  2172 
  2173 lemma asymp_equiv_sandwich_real:
  2174   fixes f g l u :: "'a \<Rightarrow> real"
  2175   assumes "l \<sim>[F] g" "u \<sim>[F] g" "eventually (\<lambda>x. f x \<in> {l x..u x}) F"
  2176   shows   "f \<sim>[F] g"
  2177   unfolding asymp_equiv_altdef
  2178 proof (rule landau_o.smallI)
  2179   fix c :: real assume c: "c > 0"
  2180   have "eventually (\<lambda>x. norm (f x - g x) \<le> max (norm (l x - g x)) (norm (u x - g x))) F"
  2181     using assms(3) by eventually_elim auto
  2182   moreover have "eventually (\<lambda>x. norm (l x - g x) \<le> c * norm (g x)) F"
  2183                 "eventually (\<lambda>x. norm (u x - g x) \<le> c * norm (g x)) F"
  2184     using assms(1,2) by (auto simp: asymp_equiv_altdef dest: landau_o.smallD[OF _ c])
  2185   hence "eventually (\<lambda>x. max (norm (l x - g x)) (norm (u x - g x)) \<le> c * norm (g x)) F"
  2186     by eventually_elim simp
  2187   ultimately show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
  2188     by eventually_elim (rule order.trans)
  2189 qed
  2190 
  2191 lemma asymp_equiv_sandwich_real':
  2192   fixes f g l u :: "'a \<Rightarrow> real"
  2193   assumes "f \<sim>[F] l" "f \<sim>[F] u" "eventually (\<lambda>x. g x \<in> {l x..u x}) F"
  2194   shows   "f \<sim>[F] g"
  2195   using asymp_equiv_sandwich_real[of l F f u g] assms by (simp add: asymp_equiv_sym)
  2196 
  2197 lemma asymp_equiv_sandwich_real'':
  2198   fixes f g l u :: "'a \<Rightarrow> real"
  2199   assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"
  2200           "eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"
  2201   shows   "f \<sim>[F] g"
  2202   by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]
  2203              asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];
  2204       blast intro: asymp_equiv_trans assms(1,2,3))+
  2205 
  2206 end