# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1526658718 -7200
# Node ID b48bab5119391a03af2288617d063b809d35d3e2
# Parent  37974ddde92844c3389aab7e2977b350f737568a
Moved Landau_Symbols from the AFP to HOL-Library

diff -r 37974ddde928 -r b48bab511939 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue May 22 11:05:47 2018 +0200
+++ b/CONTRIBUTORS	Fri May 18 17:51:58 2018 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* May 2018: Manuel Eberl
+  Landau symbols and asymptotic equivalence (moved from the AFP)
+
 * May 2018: Jose Divasón (Universidad de la Rioja),
   Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
   Fabian Immler (TUM)
diff -r 37974ddde928 -r b48bab511939 NEWS
--- a/NEWS	Tue May 22 11:05:47 2018 +0200
+++ b/NEWS	Fri May 18 17:51:58 2018 +0200
@@ -201,6 +201,8 @@
 
 *** HOL ***
 
+* Landau_Symbols from the AFP was moved to HOL-Library
+
 * Clarified relationship of characters, strings and code generation:
 
   * Type "char" is now a proper datatype of 8-bit values.
diff -r 37974ddde928 -r b48bab511939 src/HOL/Library/Landau_Symbols.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Landau_Symbols.thy	Fri May 18 17:51:58 2018 +0200
@@ -0,0 +1,2208 @@
+(*
+  File:   Landau_Symbols_Definition.thy
+  Author: Manuel Eberl <eberlm@in.tum.de>
+
+  Landau symbols for reasoning about the asymptotic growth of functions. 
+*)
+section {* Definition of Landau symbols *}
+
+theory Landau_Symbols
+imports 
+  Complex_Main
+begin
+
+lemma eventually_subst':
+  "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"
+  by (rule eventually_subst, erule eventually_rev_mp) simp
+
+
+subsection {* Definition of Landau symbols *}
+
+text {*
+  Our Landau symbols are sign-oblivious, i.e. any function always has the same growth 
+  as its absolute. This has the advantage of making some cancelling rules for sums nicer, but 
+  introduces some problems in other places. Nevertheless, we found this definition more convenient
+  to work with.
+*}
+
+definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
+    ("(1O[_]'(_'))")
+  where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"  
+
+definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
+    ("(1o[_]'(_'))")
+  where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
+
+definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
+    ("(1\<Omega>[_]'(_'))")
+  where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"  
+
+definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
+    ("(1\<omega>[_]'(_'))")
+  where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
+
+definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
+    ("(1\<Theta>[_]'(_'))")
+  where "bigtheta F g = bigo F g \<inter> bigomega F g"
+
+abbreviation bigo_at_top ("(2O'(_'))") where
+  "O(g) \<equiv> bigo at_top g"    
+
+abbreviation smallo_at_top ("(2o'(_'))") where
+  "o(g) \<equiv> smallo at_top g"
+
+abbreviation bigomega_at_top ("(2\<Omega>'(_'))") where
+  "\<Omega>(g) \<equiv> bigomega at_top g"
+
+abbreviation smallomega_at_top ("(2\<omega>'(_'))") where
+  "\<omega>(g) \<equiv> smallomega at_top g"
+
+abbreviation bigtheta_at_top ("(2\<Theta>'(_'))") where
+  "\<Theta>(g) \<equiv> bigtheta at_top g"
+    
+
+text {* The following is a set of properties that all Landau symbols satisfy. *}
+
+named_theorems landau_divide_simps
+
+locale landau_symbol =
+  fixes L  :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
+  and   L'  :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"
+  and   Lr  :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"
+  assumes bot': "L bot f = UNIV"
+  assumes filter_mono': "F1 \<le> F2 \<Longrightarrow> L F2 f \<subseteq> L F1 f"
+  assumes in_filtermap_iff: 
+    "f' \<in> L (filtermap h' F') g' \<longleftrightarrow> (\<lambda>x. f' (h' x)) \<in> L' F' (\<lambda>x. g' (h' x))"
+  assumes filtercomap: 
+    "f' \<in> L F'' g' \<Longrightarrow> (\<lambda>x. f' (h' x)) \<in> L' (filtercomap h' F'') (\<lambda>x. g' (h' x))"
+  assumes sup: "f \<in> L F1 g \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L (sup F1 F2) g"
+  assumes in_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"
+  assumes cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> L F (f) = L F (g)"
+  assumes cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> L F (f) = L F (g)"
+  assumes in_cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"
+  assumes cmult [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. c * f x) = L F (f)"
+  assumes cmult_in_iff [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
+  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)"
+  assumes inverse: "eventually (\<lambda>x. f x \<noteq> 0) F \<Longrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F \<Longrightarrow> 
+                        f \<in> L F (g) \<Longrightarrow> (\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))"
+  assumes subsetI: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"
+  assumes plus_subset1: "f \<in> o[F](g) \<Longrightarrow> L F (g) \<subseteq> L F (\<lambda>x. f x + g x)"
+  assumes trans: "f \<in> L F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
+  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))"
+  assumes norm_iff [simp]: "(\<lambda>x. norm (f x)) \<in> Lr F (\<lambda>x. norm (g x)) \<longleftrightarrow> f \<in> L F (g)"
+  assumes abs [simp]: "Lr Fr (\<lambda>x. \<bar>fr x\<bar>) = Lr Fr fr"
+  assumes abs_in_iff [simp]: "(\<lambda>x. \<bar>fr x\<bar>) \<in> Lr Fr gr \<longleftrightarrow> fr \<in> Lr Fr gr"
+begin
+
+lemma bot [simp]: "f \<in> L bot g" by (simp add: bot')
+  
+lemma filter_mono: "F1 \<le> F2 \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L F1 g"
+  using filter_mono'[of F1 F2] by blast
+
+lemma cong_ex: 
+  "eventually (\<lambda>x. f1 x = f2 x) F \<Longrightarrow> eventually (\<lambda>x. g1 x = g2 x) F \<Longrightarrow>
+     f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" 
+  by (subst cong, assumption, subst in_cong, assumption, rule refl)
+
+lemma cong_ex_bigtheta: 
+  "f1 \<in> \<Theta>[F](f2) \<Longrightarrow> g1 \<in> \<Theta>[F](g2) \<Longrightarrow> f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" 
+  by (subst cong_bigtheta, assumption, subst in_cong_bigtheta, assumption, rule refl)
+
+lemma bigtheta_trans1: 
+  "f \<in> L F (g) \<Longrightarrow> g \<in> \<Theta>[F](h) \<Longrightarrow> f \<in> L F (h)"
+  by (subst cong_bigtheta[symmetric])
+
+lemma bigtheta_trans2: 
+  "f \<in> \<Theta>[F](g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
+  by (subst in_cong_bigtheta)
+   
+lemma cmult' [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x * c) = L F (f)"
+  by (subst mult.commute) (rule cmult)
+
+lemma cmult_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x * c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
+  by (subst mult.commute) (rule cmult_in_iff)
+
+lemma cdiv [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x / c) = L F (f)"
+  using cmult'[of "inverse c" F f] by (simp add: field_simps)
+
+lemma cdiv_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
+  using cmult_in_iff'[of "inverse c" f] by (simp add: field_simps)
+  
+lemma uminus [simp]: "L F (\<lambda>x. -g x) = L F (g)" using cmult[of "-1"] by simp
+
+lemma uminus_in_iff [simp]: "(\<lambda>x. -f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
+  using cmult_in_iff[of "-1"] by simp
+
+lemma const: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"
+  by (subst (2) cmult[symmetric]) simp_all
+
+(* Simplifier loops without the NO_MATCH *)
+lemma const' [simp]: "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"
+  by (rule const)
+
+lemma const_in_iff: "c \<noteq> 0 \<Longrightarrow> (\<lambda>_. c) \<in> L F (f) \<longleftrightarrow> (\<lambda>_. 1) \<in> L F (f)"
+  using cmult_in_iff'[of c "\<lambda>_. 1"] by simp
+
+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)"
+  by (rule const_in_iff)
+
+lemma plus_subset2: "g \<in> o[F](f) \<Longrightarrow> L F (f) \<subseteq> L F (\<lambda>x. f x + g x)"
+  by (subst add.commute) (rule plus_subset1)
+
+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)"
+  using mult_left by (simp add: mult.commute)
+
+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)"
+  by (rule trans, erule mult_left, erule mult_right)
+
+lemma inverse_cancel:
+  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
+  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+  shows   "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> g \<in> L F (f)"
+proof
+  assume "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x))"
+  from inverse[OF _ _ this] assms show "g \<in> L F (f)" by simp
+qed (intro inverse assms)
+
+lemma divide_right:
+  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+  assumes "f \<in> L F (g)"
+  shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"
+  by (subst (1 2) divide_inverse) (intro mult_right inverse assms)
+
+lemma divide_right_iff:
+  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+  shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> f \<in> L F (g)"
+proof
+  assume "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"
+  from mult_right[OF this, of h] assms show "f \<in> L F (g)"
+    by (subst (asm) cong_ex[of _ f F _ g]) (auto elim!: eventually_mono)
+qed (simp add: divide_right assms)
+
+lemma divide_left:
+  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
+  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+  assumes "g \<in> L F(f)"
+  shows   "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"
+  by (subst (1 2) divide_inverse) (intro mult_left inverse assms)
+
+lemma divide_left_iff:
+  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
+  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+  shows   "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x) \<longleftrightarrow> g \<in> L F (f)"
+proof
+  assume A: "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"
+  from assms have B: "eventually (\<lambda>x. h x / f x / h x = inverse (f x)) F"
+    by eventually_elim (simp add: divide_inverse)
+  from assms have C: "eventually (\<lambda>x. h x / g x / h x = inverse (g x)) F"
+    by eventually_elim (simp add: divide_inverse)
+  from divide_right[OF assms(3) A] assms show "g \<in> L F (f)"
+    by (subst (asm) cong_ex[OF B C]) (simp add: inverse_cancel)
+qed (simp add: divide_left assms)
+
+lemma divide:
+  assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
+  assumes "eventually (\<lambda>x. g2 x \<noteq> 0) F"
+  assumes "f1 \<in> L F (f2)" "g2 \<in> L F (g1)"
+  shows   "(\<lambda>x. f1 x / g1 x) \<in> L F (\<lambda>x. f2 x / g2 x)"
+  by (subst (1 2) divide_inverse) (intro mult inverse assms)
+  
+lemma divide_eq1:
+  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+  shows   "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
+proof-
+  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)"
+    using assms by (intro in_cong) (auto elim: eventually_mono)
+  thus ?thesis by (simp only: divide_right_iff assms)
+qed
+
+lemma divide_eq2:
+  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+  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)"
+proof-
+  have "L F (\<lambda>x. g x) = L F (\<lambda>x. g x * h x / h x)"
+    using assms by (intro cong) (auto elim: eventually_mono)
+  thus ?thesis by (simp only: divide_right_iff assms)
+qed
+
+lemma inverse_eq1:
+  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+  shows   "f \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> (\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"
+  using divide_eq1[of g F f "\<lambda>_. 1"] by (simp add: divide_inverse assms)
+
+lemma inverse_eq2:
+  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
+  shows   "(\<lambda>x. inverse (f x)) \<in> L F (g) \<longleftrightarrow> (\<lambda>x. 1) \<in> L F (\<lambda>x. f x * g x)"
+  using divide_eq2[of f F "\<lambda>_. 1" g] by (simp add: divide_inverse assms mult_ac)
+
+lemma inverse_flip:
+  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+  assumes "(\<lambda>x. inverse (g x)) \<in> L F (h)"
+  shows   "(\<lambda>x. inverse (h x)) \<in> L F (g)"
+using assms by (simp add: divide_eq1 divide_eq2 inverse_eq_divide mult.commute)
+
+lemma lift_trans:
+  assumes "f \<in> L F (g)"
+  assumes "(\<lambda>x. t x (g x)) \<in> L F (h)"
+  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))"
+  shows   "(\<lambda>x. t x (f x)) \<in> L F (h)"
+  by (rule trans[OF assms(3)[OF assms(1)] assms(2)])
+
+lemma lift_trans':
+  assumes "f \<in> L F (\<lambda>x. t x (g x))"
+  assumes "g \<in> L F (h)"
+  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))"
+  shows   "f \<in> L F (\<lambda>x. t x (h x))"
+  by (rule trans[OF assms(1) assms(3)[OF assms(2)]])
+
+lemma lift_trans_bigtheta:
+  assumes "f \<in> L F (g)"
+  assumes "(\<lambda>x. t x (g x)) \<in> \<Theta>[F](h)"
+  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))"
+  shows   "(\<lambda>x. t x (f x)) \<in> L F (h)"
+  using cong_bigtheta[OF assms(2)] assms(3)[OF assms(1)] by simp
+
+lemma lift_trans_bigtheta':
+  assumes "f \<in> L F (\<lambda>x. t x (g x))"
+  assumes "g \<in> \<Theta>[F](h)"
+  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))"
+  shows   "f \<in> L F (\<lambda>x. t x (h x))"
+  using cong_bigtheta[OF assms(3)[OF assms(2)]] assms(1)  by simp
+
+lemma (in landau_symbol) mult_in_1:
+  assumes "f \<in> L F (\<lambda>_. 1)" "g \<in> L F (\<lambda>_. 1)"
+  shows   "(\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"
+  using mult[OF assms] by simp
+
+lemma (in landau_symbol) of_real_cancel:
+  "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<Longrightarrow> f \<in> Lr F g"
+  by (subst (asm) norm_iff [symmetric], subst (asm) (1 2) norm_of_real) simp_all
+
+lemma (in landau_symbol) of_real_iff:
+  "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<longleftrightarrow> f \<in> Lr F g"
+  by (subst norm_iff [symmetric], subst (1 2) norm_of_real) simp_all
+
+lemmas [landau_divide_simps] = 
+  inverse_cancel divide_left_iff divide_eq1 divide_eq2 inverse_eq1 inverse_eq2
+
+end
+
+
+text {* 
+  The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with 
+  $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem.
+  The following locale captures this fact.
+*}
+
+locale landau_pair = 
+  fixes L l :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
+  fixes L' l' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"
+  fixes Lr lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"
+  and   R :: "real \<Rightarrow> real \<Rightarrow> bool"
+  assumes L_def: "L F g = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"
+  and     l_def: "l F g = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"
+  and     L'_def: "L' F' g' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"
+  and     l'_def: "l' F' g' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"
+  and     Lr_def: "Lr F'' g'' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"
+  and     lr_def: "lr F'' g'' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"
+  and     R:     "R = (\<le>) \<or> R = (\<ge>)"
+
+interpretation landau_o: 
+    landau_pair bigo smallo bigo smallo bigo smallo "(\<le>)"
+  by unfold_locales (auto simp: bigo_def smallo_def intro!: ext)
+
+interpretation landau_omega: 
+    landau_pair bigomega smallomega bigomega smallomega bigomega smallomega "(\<ge>)"
+  by unfold_locales (auto simp: bigomega_def smallomega_def intro!: ext)
+
+
+context landau_pair
+begin
+
+lemmas R_E = disjE [OF R, case_names le ge]
+
+lemma bigI:
+  "c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F \<Longrightarrow> f \<in> L F (g)"
+  unfolding L_def by blast
+
+lemma bigE:
+  assumes "f \<in> L F (g)"
+  obtains c where "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"
+  using assms unfolding L_def by blast
+
+lemma smallI:
+  "(\<And>c. c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F) \<Longrightarrow> f \<in> l F (g)"
+  unfolding l_def by blast
+
+lemma smallD:
+  "f \<in> l F (g) \<Longrightarrow> c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"
+  unfolding l_def by blast
+    
+lemma bigE_nonneg_real:
+  assumes "f \<in> Lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F"
+  obtains c where "c > 0" "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
+proof-
+  from assms(1) obtain c where c: "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
+    by (auto simp: Lr_def)
+  from c(2) assms(2) have "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
+    by eventually_elim simp
+  from c(1) and this show ?thesis by (rule that)
+qed
+
+lemma smallD_nonneg_real:
+  assumes "f \<in> lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F" "c > 0"
+  shows   "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
+  using assms by (auto simp: lr_def dest!: spec[of _ c] elim: eventually_elim2)
+
+lemma small_imp_big: "f \<in> l F (g) \<Longrightarrow> f \<in> L F (g)"
+  by (rule bigI[OF _ smallD, of 1]) simp_all
+  
+lemma small_subset_big: "l F (g) \<subseteq> L F (g)"
+  using small_imp_big by blast
+
+lemma R_refl [simp]: "R x x" using R by auto
+
+lemma R_linear: "\<not>R x y \<Longrightarrow> R y x"
+  using R by auto
+
+lemma R_trans [trans]: "R a b \<Longrightarrow> R b c \<Longrightarrow> R a c"
+  using R by auto
+
+lemma R_mult_left_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (c*a) (c*b)"
+  using R by (auto simp: mult_left_mono)
+
+lemma R_mult_right_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (a*c) (b*c)"
+  using R by (auto simp: mult_right_mono)
+
+lemma big_trans:
+  assumes "f \<in> L F (g)" "g \<in> L F (h)"
+  shows   "f \<in> L F (h)"
+proof-
+  from assms(1) guess c by (elim bigE) note c = this
+  from assms(2) guess d by (elim bigE) note d = this
+  from c(2) d(2) have "eventually (\<lambda>x. R (norm (f x)) (c * d * (norm (h x)))) F"
+  proof eventually_elim
+    fix x assume "R (norm (f x)) (c * (norm (g x)))"
+    also assume "R (norm (g x)) (d * (norm (h x)))"
+    with c(1) have "R (c * (norm (g x))) (c * (d * (norm (h x))))"
+      by (intro R_mult_left_mono) simp_all
+    finally show "R (norm (f x)) (c * d * (norm (h x)))" by (simp add: algebra_simps)
+  qed
+  with c(1) d(1) show ?thesis by (intro bigI[of "c*d"]) simp_all
+qed
+
+lemma big_small_trans:
+  assumes "f \<in> L F (g)" "g \<in> l F (h)"
+  shows   "f \<in> l F (h)"
+proof (rule smallI)
+  fix c :: real assume c: "c > 0"
+  from assms(1) guess d by (elim bigE) note d = this
+  note d(2)
+  moreover from c d assms(2) 
+    have "eventually (\<lambda>x. R (norm (g x)) (c * inverse d * norm (h x))) F" 
+    by (intro smallD) simp_all
+  ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * (norm (h x)))) F"
+    by eventually_elim (erule R_trans, insert R d(1), auto simp: field_simps)
+qed
+
+lemma small_big_trans:
+  assumes "f \<in> l F (g)" "g \<in> L F (h)"
+  shows   "f \<in> l F (h)"
+proof (rule smallI)
+  fix c :: real assume c: "c > 0"
+  from assms(2) guess d by (elim bigE) note d = this
+  note d(2)
+  moreover from c d assms(1) 
+    have "eventually (\<lambda>x. R (norm (f x)) (c * inverse d * norm (g x))) F"
+    by (intro smallD) simp_all
+  ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * norm (h x))) F"
+    by eventually_elim (rotate_tac 2, erule R_trans, insert R c d(1), auto simp: field_simps)
+qed
+
+lemma small_trans:
+  "f \<in> l F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> l F (h)"
+  by (rule big_small_trans[OF small_imp_big])
+
+lemma small_big_trans':
+  "f \<in> l F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
+  by (rule small_imp_big[OF small_big_trans])
+
+lemma big_small_trans':
+  "f \<in> L F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> L F (h)"
+  by (rule small_imp_big[OF big_small_trans])
+
+lemma big_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"
+  by (intro subsetI) (drule (1) big_trans)
+
+lemma small_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> l F (f) \<subseteq> l F (g)"
+  by (intro subsetI) (drule (1) small_big_trans)
+
+lemma big_refl [simp]: "f \<in> L F (f)"
+  by (rule bigI[of 1]) simp_all
+
+lemma small_refl_iff: "f \<in> l F (f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+proof (rule iffI[OF _ smallI])
+  assume f: "f \<in> l F f"
+  have "(1/2::real) > 0" "(2::real) > 0" by simp_all
+  from smallD[OF f this(1)] smallD[OF f this(2)]
+    show "eventually (\<lambda>x. f x = 0) F" by eventually_elim (insert R, auto)
+next
+  fix c :: real assume "c > 0" "eventually (\<lambda>x. f x = 0) F"
+  from this(2) show "eventually (\<lambda>x. R (norm (f x)) (c * norm (f x))) F"
+    by eventually_elim simp_all
+qed
+
+lemma big_small_asymmetric: "f \<in> L F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
+  by (drule (1) big_small_trans) (simp add: small_refl_iff)
+
+lemma small_big_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> L F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
+  by (drule (1) small_big_trans) (simp add: small_refl_iff)
+
+lemma small_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
+  by (drule (1) small_trans) (simp add: small_refl_iff)
+
+
+lemma plus_aux:
+  assumes "f \<in> o[F](g)"
+  shows "g \<in> L F (\<lambda>x. f x + g x)"
+proof (rule R_E)
+  assume [simp]: "R = (\<le>)"
+  have A: "1/2 > (0::real)" by simp
+  {
+    fix x assume "norm (f x) \<le> 1/2 * norm (g x)"
+    hence "1/2 * (norm (g x)) \<le> (norm (g x)) - (norm (f x))" by simp
+    also have "norm (g x) - norm (f x) \<le> norm (f x + g x)"
+      by (subst add.commute) (rule norm_diff_ineq)
+    finally have "1/2 * (norm (g x)) \<le> norm (f x + g x)" by simp
+  } note B = this
+  
+  show "g \<in> L F (\<lambda>x. f x + g x)"
+    apply (rule bigI[of "2"], simp)
+    using landau_o.smallD[OF assms A] apply eventually_elim
+    using B apply (simp add: algebra_simps) 
+    done
+next
+  assume [simp]: "R = (\<lambda>x y. x \<ge> y)"
+  show "g \<in> L F (\<lambda>x. f x + g x)"
+  proof (rule bigI[of "1/2"])
+    show "eventually (\<lambda>x. R (norm (g x)) (1/2 * norm (f x + g x))) F"
+      using landau_o.smallD[OF assms zero_less_one]
+    proof eventually_elim
+      case (elim x)
+      have "norm (f x + g x) \<le> norm (f x) + norm (g x)" by (rule norm_triangle_ineq)
+      also note elim
+      finally show ?case by simp
+    qed
+  qed simp_all
+qed
+
+end
+
+
+
+lemma bigomega_iff_bigo: "g \<in> \<Omega>[F](f) \<longleftrightarrow> f \<in> O[F](g)"
+proof
+  assume "f \<in> O[F](g)"
+  then guess c by (elim landau_o.bigE)
+  thus "g \<in> \<Omega>[F](f)" by (intro landau_omega.bigI[of "inverse c"]) (simp_all add: field_simps)
+next
+  assume "g \<in> \<Omega>[F](f)"
+  then guess c by (elim landau_omega.bigE)
+  thus "f \<in> O[F](g)" by (intro landau_o.bigI[of "inverse c"]) (simp_all add: field_simps)
+qed
+
+lemma smallomega_iff_smallo: "g \<in> \<omega>[F](f) \<longleftrightarrow> f \<in> o[F](g)"
+proof
+  assume "f \<in> o[F](g)"
+  from landau_o.smallD[OF this, of "inverse c" for c]
+    show "g \<in> \<omega>[F](f)" by (intro landau_omega.smallI) (simp_all add: field_simps)
+next
+  assume "g \<in> \<omega>[F](f)"
+  from landau_omega.smallD[OF this, of "inverse c" for c]
+    show "f \<in> o[F](g)" by (intro landau_o.smallI) (simp_all add: field_simps)
+qed
+
+
+context landau_pair
+begin
+
+lemma big_mono:
+  "eventually (\<lambda>x. R (norm (f x)) (norm (g x))) F \<Longrightarrow> f \<in> L F (g)"
+  by (rule bigI[OF zero_less_one]) simp
+
+lemma big_mult:
+  assumes "f1 \<in> L F (g1)" "f2 \<in> L F (g2)"
+  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
+proof-
+  from assms(1) guess c1 by (elim bigE) note c1 = this
+  from assms(2) guess c2 by (elim bigE) note c2 = this
+  
+  from c1(1) and c2(1) have "c1 * c2 > 0" by simp
+  moreover have "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * c2 * norm (g1 x * g2 x))) F"
+    using c1(2) c2(2)
+  proof eventually_elim
+    case (elim x)
+    show ?case
+    proof (cases rule: R_E)
+      case le
+      have "norm (f1 x) * norm (f2 x) \<le> (c1 * norm (g1 x)) * (c2 * norm (g2 x))"
+        using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
+      with le show ?thesis by (simp add: le norm_mult mult_ac)
+    next
+      case ge
+      have "(c1 * norm (g1 x)) * (c2 * norm (g2 x)) \<le> norm (f1 x) * norm (f2 x)"
+        using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
+      with ge show ?thesis by (simp_all add: norm_mult mult_ac)
+    qed
+  qed
+  ultimately show ?thesis by (rule bigI)
+qed
+
+lemma small_big_mult:
+  assumes "f1 \<in> l F (g1)" "f2 \<in> L F (g2)"
+  shows   "(\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"
+proof (rule smallI)
+  fix c1 :: real assume c1: "c1 > 0"
+  from assms(2) guess c2 by (elim bigE) note c2 = this
+  with c1 assms(1) have "eventually (\<lambda>x. R (norm (f1 x)) (c1 * inverse c2 * norm (g1 x))) F"
+    by (auto intro!: smallD)
+  thus "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * norm (g1 x * g2 x))) F" using c2(2)
+  proof eventually_elim
+    case (elim x)
+    show ?case
+    proof (cases rule: R_E)
+      case le
+      have "norm (f1 x) * norm (f2 x) \<le> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
+        using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
+      with le c2(1) show ?thesis by (simp add: le norm_mult field_simps)
+    next
+      case ge
+      have "norm (f1 x) * norm (f2 x) \<ge> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
+        using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
+      with ge c2(1) show ?thesis by (simp add: ge norm_mult field_simps)
+    qed
+  qed
+qed
+
+lemma big_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)"
+  by (subst (1 2) mult.commute) (rule small_big_mult)
+
+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)"
+  by (rule small_big_mult, assumption, rule small_imp_big)
+
+lemmas mult = big_mult small_big_mult big_small_mult small_mult
+
+
+sublocale big: landau_symbol L L' Lr
+proof
+  have L: "L = bigo \<or> L = bigomega"
+    by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
+  {
+    fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
+    hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
+  } note A = this
+  {
+    fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
+    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
+      show "L F (\<lambda>x. c * f x) = L F f" by (intro equalityI big_subsetI) (simp_all add: field_simps)
+  }
+  {
+    fix c :: 'b and F and f g :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
+    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
+      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)
+    thus "((\<lambda>x. c * f x) \<in> L F g) = (f \<in> L F g)" by (intro iffI) (erule (1) big_trans)+
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> L F (g)"
+    assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
+    from A guess c by (elim bigE) note c = this
+    from c(2) B have "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
+      by eventually_elim (rule R_E, insert c(1), simp_all add: field_simps norm_inverse norm_divide)
+    with c(1) show "(\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))" by (rule bigI)
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
+    with plus_aux show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" by (blast intro!: big_subsetI) 
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
+    show "L F (f) = L F (g)" unfolding L_def
+      
+      thm eventually_subst A
+      by (subst eventually_subst'[OF A]) (rule refl)
+  }
+  {
+    fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
+    show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" unfolding L_def mem_Collect_eq
+      by (subst (1) eventually_subst'[OF A]) (rule refl)
+  }
+  {
+    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)
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
+    with A L show "L F (f) = L F (g)" unfolding bigtheta_def
+      by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo)
+    fix h:: "'a \<Rightarrow> 'b"
+    show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" by (rule disjE[OF L]) 
+      (insert A, auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans)
+  }
+  {
+    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g"
+    thus "(\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" by (intro big_mult) simp
+  }
+  {
+    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" "g \<in> L F h"
+    thus "f \<in> L F (h)" by (rule big_trans)
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
+    assume "f \<in> L F g" and "filterlim h F G"
+    thus "(\<lambda>x. f (h x)) \<in> L' G (\<lambda>x. g (h x))" by (auto simp: L_def L'_def filterlim_iff)
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F G :: "'a filter"
+    assume "f \<in> L F g" "f \<in> L G g"
+    from this [THEN bigE] guess c1 c2 . note c12 = this
+    define c where "c = (if R c1 c2 then c2 else c1)"
+    from c12 have c: "R c1 c" "R c2 c" "c > 0" by (auto simp: c_def dest: R_linear)
+    with c12(2,4) have "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
+                     "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) G"
+      by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+
+    with c show "f \<in> L (sup F G) g" by (auto simp: L_def eventually_sup)
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
+    assume "(f \<in> L F g)"
+    thus "((\<lambda>x. f (h x)) \<in> L' (filtercomap h F) (\<lambda>x. g (h x)))"
+      unfolding L_def L'_def by auto
+  }
+qed (auto simp: L_def Lr_def eventually_filtermap L'_def
+          intro: filter_leD exI[of _ "1::real"])
+
+sublocale small: landau_symbol l l' lr
+proof
+  {
+    fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
+    hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
+  } note A = this
+  {
+    fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
+    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
+      show "l F (\<lambda>x. c * f x) = l F f" 
+        by (intro equalityI small_subsetI) (simp_all add: field_simps)
+  }
+  {
+    fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
+    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
+      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)
+    thus "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" by (intro iffI) (erule (1) big_small_trans)+
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
+    with plus_aux show "l F g \<subseteq> l F (\<lambda>x. f x + g x)" by (blast intro!: small_subsetI) 
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> l F (g)"
+    assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
+    show "(\<lambda>x. inverse (g x)) \<in> l F (\<lambda>x. inverse (f x))"
+    proof (rule smallI)
+      fix c :: real assume c: "c > 0"
+      from B smallD[OF A c] 
+        show "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
+        by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide)
+    qed
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
+    show "l F (f) = l F (g)" unfolding l_def by (subst eventually_subst'[OF A]) (rule refl)
+  }
+  {
+    fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
+    show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" unfolding l_def mem_Collect_eq
+      by (subst (1) eventually_subst'[OF A]) (rule refl)
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" 
+    thus "l F f \<subseteq> l F g" by (intro small_subsetI small_imp_big)
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
+    have L: "L = bigo \<or> L = bigomega"
+      by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
+    with A show "l F (f) = l F (g)" unfolding bigtheta_def
+      by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo)
+    have l: "l = smallo \<or> l = smallomega"
+      by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff)
+    fix h:: "'a \<Rightarrow> 'b"
+    show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" by (rule disjE[OF l]) 
+      (insert A, auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo 
+       intro: landau_o.big_small_trans landau_o.small_big_trans)
+  }
+  {
+    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g"
+    thus "(\<lambda>x. h x * f x) \<in> l F (\<lambda>x. h x * g x)" by (intro big_small_mult) simp
+  }
+  {
+    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" "g \<in> l F h"
+    thus "f \<in> l F (h)" by (rule small_trans)
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
+    assume "f \<in> l F g" and "filterlim h F G"
+    thus "(\<lambda>x. f (h x)) \<in> l' G (\<lambda>x. g (h x))"
+      by (auto simp: l_def l'_def filterlim_iff)
+  }
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
+    assume "(f \<in> l F g)"
+    thus "((\<lambda>x. f (h x)) \<in> l' (filtercomap h F) (\<lambda>x. g (h x)))"
+      unfolding l_def l'_def by auto
+  }
+qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)
+
+
+text {* These rules allow chaining of Landau symbol propositions in Isar with "also".*}
+
+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)"
+  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)"
+  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)"
+  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)"
+  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)"
+  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)"
+  by (drule (1) big.mult big_small_mult small_big_mult, simp)+
+
+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)"
+  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)"
+  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)"
+  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)"
+  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)"
+  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)"
+  by (drule (1) big.mult big_small_mult small_big_mult, simp)+
+
+lemmas mult_1_trans = 
+  big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1'''
+  big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult'''
+
+lemma big_equal_iff_bigtheta: "L F (f) = L F (g) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
+proof
+  have L: "L = bigo \<or> L = bigomega"
+    by (rule R_E) (auto simp: fun_eq_iff L_def bigo_def bigomega_def)
+  fix f g :: "'a \<Rightarrow> 'b" assume "L F (f) = L F (g)"
+  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
+  thus "f \<in> \<Theta>[F](g)" using L unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
+qed (rule big.cong_bigtheta)
+
+lemma big_prod:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (g x)"
+  shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>y. \<Prod>x\<in>A. g x y)"
+  using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult)
+
+lemma big_prod_in_1:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (\<lambda>_. 1)"
+  shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>_. 1)"
+  using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult_in_1)
+
+end
+
+
+context landau_symbol
+begin
+  
+lemma plus_absorb1:
+  assumes "f \<in> o[F](g)"
+  shows   "L F (\<lambda>x. f x + g x) = L F (g)"
+proof (intro equalityI)
+  from plus_subset1 and assms show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" .
+  from landau_o.small.plus_subset1[OF assms] and assms have "(\<lambda>x. -f x) \<in> o[F](\<lambda>x. f x + g x)"
+    by (auto simp: landau_o.small.uminus_in_iff)
+  from plus_subset1[OF this] show "L F (\<lambda>x. f x + g x) \<subseteq> L F (g)" by simp
+qed
+
+lemma plus_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x + g x) = L F (f)"
+  using plus_absorb1[of g F f] by (simp add: add.commute)
+
+lemma diff_absorb1: "f \<in> o[F](g) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (g)"
+  by (simp only: diff_conv_add_uminus plus_absorb1 landau_o.small.uminus uminus)
+
+lemma diff_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (f)"
+  by (simp only: diff_conv_add_uminus plus_absorb2 landau_o.small.uminus_in_iff)
+
+lemmas absorb = plus_absorb1 plus_absorb2 diff_absorb1 diff_absorb2
+
+end
+
+
+lemma bigthetaI [intro]: "f \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> \<Theta>[F](g)"
+  unfolding bigtheta_def bigomega_def by blast
+
+lemma bigthetaD1 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> O[F](g)" 
+  and bigthetaD2 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g)"
+  unfolding bigtheta_def bigo_def bigomega_def by blast+
+
+lemma bigtheta_refl [simp]: "f \<in> \<Theta>[F](f)"
+  unfolding bigtheta_def by simp
+
+lemma bigtheta_sym: "f \<in> \<Theta>[F](g) \<longleftrightarrow> g \<in> \<Theta>[F](f)"
+  unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
+
+lemmas landau_flip =
+  bigomega_iff_bigo[symmetric] smallomega_iff_smallo[symmetric]
+  bigomega_iff_bigo smallomega_iff_smallo bigtheta_sym
+
+
+interpretation landau_theta: landau_symbol bigtheta bigtheta bigtheta
+proof
+  fix f g :: "'a \<Rightarrow> 'b" and F
+  assume "f \<in> o[F](g)"
+  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)"
+    by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+
+  thus "\<Theta>[F](g) \<subseteq> \<Theta>[F](\<lambda>x. f x + g x)" unfolding bigtheta_def by blast
+next
+  fix f g :: "'a \<Rightarrow> 'b" and F 
+  assume "f \<in> \<Theta>[F](g)"
+  thus A: "\<Theta>[F](f) = \<Theta>[F](g)" 
+    apply (subst (1 2) bigtheta_def)
+    apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+
+    apply (rule refl)
+    done
+  thus "\<Theta>[F](f) \<subseteq> \<Theta>[F](g)" by simp
+  fix h :: "'a \<Rightarrow> 'b"
+  show "f \<in> \<Theta>[F](h) \<longleftrightarrow> g \<in> \<Theta>[F](h)" by (subst (1 2) bigtheta_sym) (simp add: A)
+next
+  fix f g h :: "'a \<Rightarrow> 'b" and F
+  assume "f \<in> \<Theta>[F](g)" "g \<in> \<Theta>[F](h)"
+  thus "f \<in> \<Theta>[F](h)" unfolding bigtheta_def
+    by (blast intro: landau_o.big.trans landau_omega.big.trans)
+next
+  fix f :: "'a \<Rightarrow> 'b" and F1 F2 :: "'a filter"
+  assume "F1 \<le> F2"
+  thus "\<Theta>[F2](f) \<subseteq> \<Theta>[F1](f)"
+    by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono)
+qed (auto simp: bigtheta_def landau_o.big.norm_iff 
+                landau_o.big.cmult landau_omega.big.cmult 
+                landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff 
+                landau_o.big.in_cong landau_omega.big.in_cong
+                landau_o.big.mult landau_omega.big.mult
+                landau_o.big.inverse landau_omega.big.inverse 
+                landau_o.big.compose landau_omega.big.compose
+                landau_o.big.bot' landau_omega.big.bot'
+                landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff
+                landau_o.big.sup landau_omega.big.sup
+                landau_o.big.filtercomap landau_omega.big.filtercomap
+          dest: landau_o.big.cong landau_omega.big.cong)
+
+lemmas landau_symbols = 
+  landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms
+  landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms 
+  landau_theta.landau_symbol_axioms
+
+lemma bigoI [intro]:
+  assumes "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
+  shows   "f \<in> O[F](g)"
+proof (rule landau_o.bigI)
+  show "max 1 c > 0" by simp
+  note assms
+  moreover have "\<And>x. c * (norm (g x)) \<le> max 1 c * (norm (g x))" by (simp add: mult_right_mono)
+  ultimately show "eventually (\<lambda>x. (norm (f x)) \<le> max 1 c * (norm (g x))) F"
+    by (auto elim!: eventually_mono dest: order.trans)
+qed
+
+lemma smallomegaD [dest]:
+  assumes "f \<in> \<omega>[F](g)"
+  shows   "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
+proof (cases "c > 0")
+  case False
+  show ?thesis 
+    by (intro always_eventually allI, rule order.trans[of _ 0])
+       (insert False, auto intro!: mult_nonpos_nonneg)
+qed (blast dest: landau_omega.smallD[OF assms, of c])
+
+  
+lemma bigthetaI':
+  assumes "c1 > 0" "c2 > 0"
+  assumes "eventually (\<lambda>x. c1 * (norm (g x)) \<le> (norm (f x)) \<and> (norm (f x)) \<le> c2 * (norm (g x))) F"
+  shows   "f \<in> \<Theta>[F](g)"
+apply (rule bigthetaI)
+apply (rule landau_o.bigI[OF assms(2)]) using assms(3) apply (eventually_elim, simp)
+apply (rule landau_omega.bigI[OF assms(1)]) using assms(3) apply (eventually_elim, simp)
+done
+
+lemma bigthetaI_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> \<Theta>[F](g)"
+  by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono)
+
+lemma (in landau_symbol) ev_eq_trans1: 
+  "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))"
+  by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono)
+
+lemma (in landau_symbol) ev_eq_trans2: 
+  "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)"
+  by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono)
+
+declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro]
+declare landau_o.bigE landau_omega.bigE [elim]
+declare landau_o.smallD
+
+lemma (in landau_symbol) bigtheta_trans1': 
+  "f \<in> L F (g) \<Longrightarrow> h \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h)"
+  by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym)
+
+lemma (in landau_symbol) bigtheta_trans2': 
+  "g \<in> \<Theta>[F](f) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
+  by (rule bigtheta_trans2, subst bigtheta_sym)
+
+lemma bigo_bigomega_trans:      "f \<in> O[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> O[F](h)"
+  and bigo_smallomega_trans:    "f \<in> O[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
+  and smallo_bigomega_trans:    "f \<in> o[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
+  and smallo_smallomega_trans:  "f \<in> o[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
+  and bigomega_bigo_trans:      "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](h)"
+  and bigomega_smallo_trans:    "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
+  and smallomega_bigo_trans:    "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
+  and smallomega_smallo_trans:  "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
+  by (unfold bigomega_iff_bigo smallomega_iff_smallo)
+     (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans 
+                landau_o.big_trans landau_o.small_trans)+
+
+lemmas landau_trans_lift [trans] =
+  landau_symbols[THEN landau_symbol.lift_trans]
+  landau_symbols[THEN landau_symbol.lift_trans']
+  landau_symbols[THEN landau_symbol.lift_trans_bigtheta]
+  landau_symbols[THEN landau_symbol.lift_trans_bigtheta']
+
+lemmas landau_mult_1_trans [trans] =
+  landau_o.mult_1_trans landau_omega.mult_1_trans
+
+lemmas landau_trans [trans] = 
+  landau_symbols[THEN landau_symbol.bigtheta_trans1]
+  landau_symbols[THEN landau_symbol.bigtheta_trans2]
+  landau_symbols[THEN landau_symbol.bigtheta_trans1']
+  landau_symbols[THEN landau_symbol.bigtheta_trans2']
+  landau_symbols[THEN landau_symbol.ev_eq_trans1]
+  landau_symbols[THEN landau_symbol.ev_eq_trans2]
+
+  landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans
+  landau_omega.big_trans landau_omega.small_trans 
+    landau_omega.small_big_trans landau_omega.big_small_trans
+
+  bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans 
+  bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans
+
+lemma bigtheta_inverse [simp]: 
+  shows "(\<lambda>x. inverse (f x)) \<in> \<Theta>[F](\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
+proof-
+  {
+    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
+    then guess c1 c2 :: real unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
+    note c = this
+    from c(3) have "inverse c2 > 0" by simp
+    moreover from c(2,4)
+      have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))) F"
+    proof eventually_elim
+      fix x assume A: "(norm (f x)) \<le> c1 * (norm (g x))" "c2 * (norm (g x)) \<le> (norm (f x))"
+      from A c(1,3) have "f x = 0 \<longleftrightarrow> g x = 0" by (auto simp: field_simps mult_le_0_iff)
+      with A c(1,3) show "norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))"
+        by (force simp: field_simps norm_inverse norm_divide)
+    qed
+    ultimately have "(\<lambda>x. inverse (f x)) \<in> O[F](\<lambda>x. inverse (g x))" by (rule landau_o.bigI)
+  }
+  thus ?thesis unfolding bigtheta_def 
+    by (force simp: bigomega_iff_bigo bigtheta_sym)
+qed
+
+lemma bigtheta_divide:
+  assumes "f1 \<in> \<Theta>(f2)" "g1 \<in> \<Theta>(g2)"
+  shows   "(\<lambda>x. f1 x / g1 x) \<in> \<Theta>(\<lambda>x. f2 x / g2 x)"
+  by (subst (1 2) divide_inverse, intro landau_theta.mult) (simp_all add: bigtheta_inverse assms)
+
+lemma eventually_nonzero_bigtheta:
+  assumes "f \<in> \<Theta>[F](g)"
+  shows   "eventually (\<lambda>x. f x \<noteq> 0) F \<longleftrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F"
+proof-
+  {
+    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"
+    from A guess c1 c2 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
+    from B this(2,4) have "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim auto
+  }
+  with assms show ?thesis by (force simp: bigtheta_sym)
+qed
+
+
+subsection {* Landau symbols and limits *}
+
+lemma bigoI_tendsto_norm:
+  fixes f g
+  assumes "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
+  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+  shows   "f \<in> O[F](g)"
+proof (rule bigoI)
+  from assms have "eventually (\<lambda>x. dist (norm (f x / g x)) c < 1) F" 
+    using tendstoD by force
+  thus "eventually (\<lambda>x. (norm (f x)) \<le> (norm c + 1) * (norm (g x))) F"
+    unfolding dist_real_def using assms(2)
+  proof eventually_elim
+    case (elim x)
+    have "(norm (f x)) - norm c * (norm (g x)) \<le> norm ((norm (f x)) - c * (norm (g x)))"
+      unfolding norm_mult [symmetric] using norm_triangle_ineq2[of "norm (f x)" "c * norm (g x)"]
+      by (simp add: norm_mult abs_mult)
+    also from elim have "\<dots> = norm (norm (g x)) * norm (norm (f x / g x) - c)"
+      unfolding norm_mult [symmetric] by (simp add: algebra_simps norm_divide)
+    also from elim have "norm (norm (f x / g x) - c) \<le> 1" by simp
+    hence "norm (norm (g x)) * norm (norm (f x / g x) - c) \<le> norm (norm (g x)) * 1" 
+      by (rule mult_left_mono) simp_all
+    finally show ?case by (simp add: algebra_simps)
+  qed
+qed
+
+lemma bigoI_tendsto:
+  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
+  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+  shows   "f \<in> O[F](g)"
+  using assms by (rule bigoI_tendsto_norm[OF tendsto_norm])
+
+lemma bigomegaI_tendsto_norm:
+  assumes c_not_0:  "(c::real) \<noteq> 0"
+  assumes lim:      "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
+  shows   "f \<in> \<Omega>[F](g)"
+proof (cases "F = bot")
+  case False
+  show ?thesis
+  proof (rule landau_omega.bigI)
+    from lim  have "c \<ge> 0" by (rule tendsto_lowerbound) (insert False, simp_all)
+    with c_not_0 have "c > 0" by simp
+    with c_not_0 show "c/2 > 0" by simp
+    from lim have ev: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<epsilon>) F"
+      by (subst (asm) tendsto_iff) (simp add: dist_real_def)
+    from ev[OF `c/2 > 0`] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
+    proof (eventually_elim)
+      fix x assume B: "norm (norm (f x / g x) - c) < c / 2"
+      from B have g: "g x \<noteq> 0" by auto
+      from B have "-c/2 < -norm (norm (f x / g x) - c)" by simp
+      also have "... \<le> norm (f x / g x) - c" by simp
+      finally show "(norm (f x)) \<ge> c/2 * (norm (g x))" using g 
+        by (simp add: field_simps norm_mult norm_divide)
+    qed
+  qed
+qed simp
+
+lemma bigomegaI_tendsto:
+  assumes c_not_0:  "(c::real) \<noteq> 0"
+  assumes lim:      "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
+  shows   "f \<in> \<Omega>[F](g)"
+  by (rule bigomegaI_tendsto_norm[OF _ tendsto_norm, of c]) (insert assms, simp_all)
+
+lemma smallomegaI_filterlim_at_top_norm:
+  assumes lim: "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
+  shows   "f \<in> \<omega>[F](g)"
+proof (rule landau_omega.smallI)
+  fix c :: real assume c_pos: "c > 0"
+  from lim have ev: "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F"
+    by (subst (asm) filterlim_at_top) simp
+  thus "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
+  proof eventually_elim
+    fix x assume A: "norm (f x / g x) \<ge> c"
+    from A c_pos have "g x \<noteq> 0" by auto
+    with A show "(norm (f x)) \<ge> c * (norm (g x))" by (simp add: field_simps norm_divide)
+  qed
+qed
+
+lemma smallomegaI_filterlim_at_infinity:
+  assumes lim: "filterlim (\<lambda>x. f x / g x) at_infinity F"
+  shows   "f \<in> \<omega>[F](g)"
+proof (rule smallomegaI_filterlim_at_top_norm)
+  from lim show "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
+    by (rule filterlim_at_infinity_imp_norm_at_top)
+qed
+  
+lemma smallomegaD_filterlim_at_top_norm:
+  assumes "f \<in> \<omega>[F](g)"
+  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+  shows   "LIM x F. norm (f x / g x) :> at_top"
+proof (subst filterlim_at_top_gt, clarify)
+  fix c :: real assume c: "c > 0"
+  from landau_omega.smallD[OF assms(1) this] assms(2) 
+    show "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F" 
+    by eventually_elim (simp add: field_simps norm_divide)
+qed
+  
+lemma smallomegaD_filterlim_at_infinity:
+  assumes "f \<in> \<omega>[F](g)"
+  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+  shows   "LIM x F. f x / g x :> at_infinity"
+  using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm)
+
+lemma smallomega_1_conv_filterlim: "f \<in> \<omega>[F](\<lambda>_. 1) \<longleftrightarrow> filterlim f at_infinity F"
+  by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)
+
+lemma smalloI_tendsto:
+  assumes lim: "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
+  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+  shows   "f \<in> o[F](g)"
+proof (rule landau_o.smallI)
+  fix c :: real assume c_pos: "c > 0"
+  from c_pos and lim have ev: "eventually (\<lambda>x. norm (f x / g x) < c) F"
+    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
+  with assms(2) show "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
+    by eventually_elim (simp add: field_simps norm_divide)
+qed
+
+lemma smalloD_tendsto:
+  assumes "f \<in> o[F](g)"
+  shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
+unfolding tendsto_iff
+proof clarify
+  fix e :: real assume e: "e > 0"
+  hence "e/2 > 0" by simp
+  from landau_o.smallD[OF assms this] show "eventually (\<lambda>x. dist (f x / g x) 0 < e) F"
+  proof eventually_elim
+    fix x assume "(norm (f x)) \<le> e/2 * (norm (g x))"
+    with e have "dist (f x / g x) 0 \<le> e/2"
+      by (cases "g x = 0") (simp_all add: dist_real_def norm_divide field_simps)
+    also from e have "... < e" by simp
+    finally show "dist (f x / g x) 0 < e" by simp
+  qed
+qed
+
+lemma bigthetaI_tendsto_norm:
+  assumes c_not_0: "(c::real) \<noteq> 0"
+  assumes lim:     "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
+  shows   "f \<in> \<Theta>[F](g)"
+proof (rule bigthetaI)
+  from c_not_0 have "\<bar>c\<bar> > 0" by simp
+  with lim have "eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<bar>c\<bar>) F"
+    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
+  hence g: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim (auto simp add: field_simps)
+
+  from lim g show "f \<in> O[F](g)" by (rule bigoI_tendsto_norm)
+  from c_not_0 and lim show "f \<in> \<Omega>[F](g)" by (rule bigomegaI_tendsto_norm)
+qed
+
+lemma bigthetaI_tendsto:
+  assumes c_not_0: "(c::real) \<noteq> 0"
+  assumes lim:     "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
+  shows   "f \<in> \<Theta>[F](g)"
+  using assms by (intro bigthetaI_tendsto_norm[OF _ tendsto_norm, of "c"]) simp_all
+
+lemma tendsto_add_smallo:
+  assumes "(f1 \<longlongrightarrow> a) F"
+  assumes "f2 \<in> o[F](f1)"
+  shows   "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
+proof (subst filterlim_cong[OF refl refl])
+  from landau_o.smallD[OF assms(2) zero_less_one] 
+    have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)) F" by simp
+  thus "eventually (\<lambda>x. f1 x + f2 x = f1 x * (1 + f2 x / f1 x)) F"
+    by eventually_elim (auto simp: field_simps)
+next
+  from assms(1) show "((\<lambda>x. f1 x * (1 + f2 x / f1 x)) \<longlongrightarrow> a) F"
+    by (force intro: tendsto_eq_intros smalloD_tendsto[OF assms(2)])
+qed
+
+lemma tendsto_diff_smallo:
+  shows "(f1 \<longlongrightarrow> a) F \<Longrightarrow> f2 \<in> o[F](f1) \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
+  using tendsto_add_smallo[of f1 a F "\<lambda>x. -f2 x"] by simp
+
+lemma tendsto_add_smallo_iff:
+  assumes "f2 \<in> o[F](f1)"
+  shows   "(f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
+proof
+  assume "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
+  hence "((\<lambda>x. f1 x + f2 x - f2 x) \<longlongrightarrow> a) F"
+    by (rule tendsto_diff_smallo) (simp add: landau_o.small.plus_absorb2 assms)
+  thus "(f1 \<longlongrightarrow> a) F" by simp
+qed (rule tendsto_add_smallo[OF _ assms])
+
+lemma tendsto_diff_smallo_iff:
+  shows "f2 \<in> o[F](f1) \<Longrightarrow> (f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
+  using tendsto_add_smallo_iff[of "\<lambda>x. -f2 x" F f1 a] by simp
+
+lemma tendsto_divide_smallo:
+  assumes "((\<lambda>x. f1 x / g1 x) \<longlongrightarrow> a) F"
+  assumes "f2 \<in> o[F](f1)" "g2 \<in> o[F](g1)"
+  assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
+  shows   "((\<lambda>x. (f1 x + f2 x) / (g1 x + g2 x)) \<longlongrightarrow> a) F" (is "(?f \<longlongrightarrow> _) _")
+proof (subst tendsto_cong)
+  let ?f' = "\<lambda>x. (f1 x / g1 x) * (1 + f2 x / f1 x) / (1 + g2 x / g1 x)"
+
+  have "(?f' \<longlongrightarrow> a * (1 + 0) / (1 + 0)) F"
+  by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const 
+        smalloD_tendsto[OF assms(2)] smalloD_tendsto[OF assms(3)])+ simp_all
+  thus "(?f' \<longlongrightarrow> a) F" by simp
+
+  have "(1/2::real) > 0" by simp
+  from landau_o.smallD[OF assms(2) this] landau_o.smallD[OF assms(3) this]
+    have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)/2) F"
+         "eventually (\<lambda>x. norm (g2 x) \<le> norm (g1 x)/2) F" by simp_all
+  with assms(4) show "eventually (\<lambda>x. ?f x = ?f' x) F"
+  proof eventually_elim
+    fix x assume A: "norm (f2 x) \<le> norm (f1 x)/2" and 
+                 B: "norm (g2 x) \<le> norm (g1 x)/2" and C: "g1 x \<noteq> 0"
+    show "?f x = ?f' x"
+    proof (cases "f1 x = 0")
+      assume D: "f1 x \<noteq> 0"
+      from D have "f1 x + f2 x = f1 x * (1 + f2 x/f1 x)" by (simp add: field_simps)
+      moreover from C have "g1 x + g2 x = g1 x * (1 + g2 x/g1 x)" by (simp add: field_simps)
+      ultimately have "?f x = (f1 x * (1 + f2 x/f1 x)) / (g1 x * (1 + g2 x/g1 x))" by (simp only:)
+      also have "... = ?f' x" by simp
+      finally show ?thesis .
+    qed (insert A, simp)
+  qed
+qed
+
+
+lemma bigo_powr:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes "f \<in> O[F](g)" "p \<ge> 0"
+  shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)"
+proof-
+  from assms(1) guess c by (elim landau_o.bigE landau_omega.bigE IntE)
+  note c = this
+  from c(2) assms(2) have "eventually (\<lambda>x. (norm (f x)) powr p \<le> (c * (norm (g x))) powr p) F"
+    by (auto elim!: eventually_mono intro!: powr_mono2)
+  thus "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" using c(1)
+    by (intro bigoI[of _ "c powr p"]) (simp_all add: powr_mult)
+qed
+
+lemma smallo_powr:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes "f \<in> o[F](g)" "p > 0"
+  shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)"
+proof (rule landau_o.smallI)
+  fix c :: real assume c: "c > 0"
+  hence "c powr (1/p) > 0" by simp
+  from landau_o.smallD[OF assms(1) this] 
+  show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F"
+  proof eventually_elim
+    fix x assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))"
+    with assms(2) have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p"
+      by (intro powr_mono2) simp_all
+    also from assms(2) c have "... = c * (norm (g x)) powr p"
+      by (simp add: field_simps powr_mult powr_powr)
+    finally show "norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)" by simp
+  qed
+qed
+
+lemma smallo_powr_nonneg:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes "f \<in> o[F](g)" "p > 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
+  shows   "(\<lambda>x. f x powr p) \<in> o[F](\<lambda>x. g x powr p)"
+proof -
+  from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
+    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+  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+
+  also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
+    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+  finally show ?thesis .
+qed
+
+lemma bigtheta_powr:
+  fixes f :: "'a \<Rightarrow> real"
+  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)"
+apply (cases "p < 0")
+apply (subst bigtheta_inverse[symmetric], subst (1 2) powr_minus[symmetric])
+unfolding bigtheta_def apply (auto simp: bigomega_iff_bigo intro!: bigo_powr)
+done
+
+lemma bigo_powr_nonneg:
+  fixes f :: "'a \<Rightarrow> real"
+  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"
+  shows   "(\<lambda>x. f x powr p) \<in> O[F](\<lambda>x. g x powr p)"
+proof -
+  from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
+    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+  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+
+  also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
+    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+  finally show ?thesis .
+qed
+
+lemma zero_in_smallo [simp]: "(\<lambda>_. 0) \<in> o[F](f)"
+  by (intro landau_o.smallI) simp_all
+
+lemma zero_in_bigo [simp]: "(\<lambda>_. 0) \<in> O[F](f)"
+  by (intro landau_o.bigI[of 1]) simp_all
+
+lemma in_bigomega_zero [simp]: "f \<in> \<Omega>[F](\<lambda>x. 0)"
+  by (rule landau_omega.bigI[of 1]) simp_all
+
+lemma in_smallomega_zero [simp]: "f \<in> \<omega>[F](\<lambda>x. 0)"
+  by (simp add: smallomega_iff_smallo)
+
+
+lemma in_smallo_zero_iff [simp]: "f \<in> o[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+proof
+  assume "f \<in> o[F](\<lambda>_. 0)"
+  from landau_o.smallD[OF this, of 1] show "eventually (\<lambda>x. f x = 0) F" by simp
+next
+  assume "eventually (\<lambda>x. f x = 0) F"
+  hence "\<forall>c>0. eventually (\<lambda>x. (norm (f x)) \<le> c * \<bar>0\<bar>) F" by simp
+  thus "f \<in> o[F](\<lambda>_. 0)" unfolding smallo_def by simp
+qed
+
+lemma in_bigo_zero_iff [simp]: "f \<in> O[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+proof
+  assume "f \<in> O[F](\<lambda>_. 0)"
+  thus "eventually (\<lambda>x. f x = 0) F" by (elim landau_o.bigE) simp
+next
+  assume "eventually (\<lambda>x. f x = 0) F"
+  hence "eventually (\<lambda>x. (norm (f x)) \<le> 1 * \<bar>0\<bar>) F" by simp
+  thus "f \<in> O[F](\<lambda>_. 0)" by (intro landau_o.bigI[of 1]) simp_all
+qed
+
+lemma zero_in_smallomega_iff [simp]: "(\<lambda>_. 0) \<in> \<omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+  by (simp add: smallomega_iff_smallo)
+
+lemma zero_in_bigomega_iff [simp]: "(\<lambda>_. 0) \<in> \<Omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+  by (simp add: bigomega_iff_bigo)
+
+lemma zero_in_bigtheta_iff [simp]: "(\<lambda>_. 0) \<in> \<Theta>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+  unfolding bigtheta_def by simp
+
+lemma in_bigtheta_zero_iff [simp]: "f \<in> \<Theta>[F](\<lambda>x. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+  unfolding bigtheta_def by simp
+
+
+lemma cmult_in_bigo_iff    [simp]:  "(\<lambda>x. c * f x) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
+  and cmult_in_bigo_iff'   [simp]:  "(\<lambda>x. f x * c) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
+  and cmult_in_smallo_iff  [simp]:  "(\<lambda>x. c * f x) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
+  and cmult_in_smallo_iff' [simp]: "(\<lambda>x. f x * c) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
+  by (cases "c = 0", simp, simp)+
+
+lemma bigo_const [simp]: "(\<lambda>_. c) \<in> O[F](\<lambda>_. 1)" by (rule bigoI[of _ "norm c"]) simp
+
+lemma bigo_const_iff [simp]: "(\<lambda>_. c1) \<in> O[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 = 0 \<or> c2 \<noteq> 0"
+  by (cases "c1 = 0"; cases "c2 = 0")
+     (auto simp: bigo_def eventually_False intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
+
+lemma bigomega_const_iff [simp]: "(\<lambda>_. c1) \<in> \<Omega>[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 \<noteq> 0 \<or> c2 = 0"
+  by (cases "c1 = 0"; cases "c2 = 0")
+     (auto simp: bigomega_def eventually_False mult_le_0_iff 
+           intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
+
+lemma smallo_real_nat_transfer:
+  "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))"
+  by (rule landau_o.small.compose[OF _ filterlim_real_sequentially])
+
+lemma bigo_real_nat_transfer:
+  "(f :: real \<Rightarrow> real) \<in> O(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> O(\<lambda>x. g (real x))"
+  by (rule landau_o.big.compose[OF _ filterlim_real_sequentially])
+
+lemma smallomega_real_nat_transfer:
+  "(f :: real \<Rightarrow> real) \<in> \<omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<omega>(\<lambda>x. g (real x))"
+  by (rule landau_omega.small.compose[OF _ filterlim_real_sequentially])
+
+lemma bigomega_real_nat_transfer:
+  "(f :: real \<Rightarrow> real) \<in> \<Omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Omega>(\<lambda>x. g (real x))"
+  by (rule landau_omega.big.compose[OF _ filterlim_real_sequentially])
+
+lemma bigtheta_real_nat_transfer:
+  "(f :: real \<Rightarrow> real) \<in> \<Theta>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Theta>(\<lambda>x. g (real x))"
+  unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast
+
+lemmas landau_real_nat_transfer [intro] = 
+  bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer 
+  smallomega_real_nat_transfer bigtheta_real_nat_transfer
+
+
+lemma landau_symbol_if_at_top_eq [simp]:
+  assumes "landau_symbol L L' Lr"
+  shows   "L at_top (\<lambda>x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)"
+apply (rule landau_symbol.cong[OF assms])
+using less_add_one[of a] apply (auto intro: eventually_mono  eventually_ge_at_top[of "a + 1"])
+done
+
+lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq]
+
+
+
+lemma sum_in_smallo:
+  assumes "f \<in> o[F](h)" "g \<in> o[F](h)"
+  shows   "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)"
+proof-
+  {
+    fix f g assume fg: "f \<in> o[F](h)" "g \<in> o[F](h)"
+    have "(\<lambda>x. f x + g x) \<in> o[F](h)"
+    proof (rule landau_o.smallI)
+      fix c :: real assume "c > 0"
+      hence "c/2 > 0" by simp
+      from fg[THEN landau_o.smallD[OF _ this]]
+      show "eventually (\<lambda>x. norm (f x + g x) \<le> c * (norm (h x))) F"
+        by eventually_elim (auto intro: order.trans[OF norm_triangle_ineq])
+    qed
+  }
+  from this[of f g] this[of f "\<lambda>x. -g x"] assms
+    show "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" by simp_all
+qed
+
+lemma big_sum_in_smallo:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> o[F](g)"
+  shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> o[F](g)"
+  using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_smallo)
+
+lemma sum_in_bigo:
+  assumes "f \<in> O[F](h)" "g \<in> O[F](h)"
+  shows   "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)"
+proof-
+  {
+    fix f g assume fg: "f \<in> O[F](h)" "g \<in> O[F](h)"
+    from fg(1) guess c1 by (elim landau_o.bigE) note c1 = this
+    from fg(2) guess c2 by (elim landau_o.bigE) note c2 = this
+    from c1(2) c2(2) have "eventually (\<lambda>x. norm (f x + g x) \<le> (c1 + c2) * (norm (h x))) F"
+      by eventually_elim (auto simp: algebra_simps intro: order.trans[OF norm_triangle_ineq])
+    hence "(\<lambda>x. f x + g x) \<in> O[F](h)" by (rule bigoI)
+  }
+  from this[of f g] this[of f "\<lambda>x. -g x"] assms
+    show "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" by simp_all
+qed
+
+lemma big_sum_in_bigo:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> O[F](g)"
+  shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"
+  using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)
+
+context landau_symbol
+begin
+
+lemma mult_cancel_left:
+  assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
+  notes   [trans] = bigtheta_trans1 bigtheta_trans2
+  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f2 \<in> L F (g2)"
+proof
+  assume A: "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
+  from assms have nz: "eventually (\<lambda>x. f1 x \<noteq> 0) F" by (simp add: eventually_nonzero_bigtheta)
+  hence "f2 \<in> \<Theta>[F](\<lambda>x. f1 x * f2 x / f1 x)"
+    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+  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)" 
+    by (intro divide_right) simp_all
+  also from assms nz have "(\<lambda>x. g1 x * g2 x / f1 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x / g1 x)"
+    by (intro landau_theta.mult landau_theta.divide) (simp_all add: bigtheta_sym)
+  also from assms have "(\<lambda>x. g1 x * g2 x / g1 x) \<in> \<Theta>[F](g2)"
+    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+  finally show "f2 \<in> L F (g2)" .
+next
+  assume "f2 \<in> L F (g2)"
+  hence "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. f1 x * g2 x)" by (rule mult_left)
+  also have "(\<lambda>x. f1 x * g2 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x)"
+    by (intro landau_theta.mult_right assms)
+  finally show "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" .
+qed
+
+lemma mult_cancel_right:
+  assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
+  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
+  by (subst (1 2) mult.commute) (rule mult_cancel_left[OF assms])
+
+lemma divide_cancel_right:
+  assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
+  shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
+  by (subst (1 2) divide_inverse, intro mult_cancel_right bigtheta_inverse) (simp_all add: assms)
+
+lemma divide_cancel_left:
+  assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
+  shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> 
+             (\<lambda>x. inverse (f2 x)) \<in> L F (\<lambda>x. inverse (g2 x))"
+  by (simp only: divide_inverse mult_cancel_left[OF assms])
+
+end
+
+
+lemma powr_smallo_iff:
+  assumes "filterlim g at_top F" "F \<noteq> bot"
+  shows   "(\<lambda>x. g x powr p :: real) \<in> o[F](\<lambda>x. g x powr q) \<longleftrightarrow> p < q"
+proof-
+  from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
+  hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
+  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)"
+  proof
+    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)"
+    from landau_o.big_small_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
+    with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
+    thus False by (simp add: eventually_False assms)
+  qed
+  show ?thesis
+  proof (cases p q rule: linorder_cases)
+    assume "p < q"
+    hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
+      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+    with `p < q` show ?thesis by auto
+  next
+    assume "p = q"
+    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
+    with B `p = q` show ?thesis by auto
+  next
+    assume "p > q"
+    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
+      by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp: powr_diff [symmetric] )
+    with B `p > q` show ?thesis by auto
+  qed
+qed
+
+lemma powr_bigo_iff:
+  assumes "filterlim g at_top F" "F \<noteq> bot"
+  shows   "(\<lambda>x. g x powr p :: real) \<in> O[F](\<lambda>x. g x powr q) \<longleftrightarrow> p \<le> q"
+proof-
+  from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
+  hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
+  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)"
+  proof
+    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)"
+    from landau_o.small_big_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
+    with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
+    thus False by (simp add: eventually_False assms)
+  qed
+  show ?thesis
+  proof (cases p q rule: linorder_cases)
+    assume "p < q"
+    hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
+      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+    with `p < q` show ?thesis by (auto intro: landau_o.small_imp_big)
+  next
+    assume "p = q"
+    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
+    with B `p = q` show ?thesis by auto
+  next
+    assume "p > q"
+    hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
+      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+    with B `p > q` show ?thesis by (auto intro: landau_o.small_imp_big)
+  qed
+qed
+
+lemma powr_bigtheta_iff: 
+  assumes "filterlim g at_top F" "F \<noteq> bot"
+  shows   "(\<lambda>x. g x powr p :: real) \<in> \<Theta>[F](\<lambda>x. g x powr q) \<longleftrightarrow> p = q"
+  using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff)
+
+
+subsection \<open>Flatness of real functions\<close>
+
+text \<open>
+  Given two real-valued functions $f$ and $g$, we say that $f$ is flatter than $g$ if
+  any power of $f(x)$ is asymptotically dominated by any positive power of $g(x)$. This is
+  a useful notion since, given two products of powers of functions sorted by flatness, we can
+  compare them asymptotically by simply comparing the exponent lists lexicographically.
+
+  A simple sufficient criterion for flatness it that $\ln f(x) \in o(\ln g(x))$, which we show
+  now.
+\<close>
+lemma ln_smallo_imp_flat:
+  fixes f g :: "real \<Rightarrow> real"
+  assumes lim_f: "filterlim f at_top at_top"
+  assumes lim_g: "filterlim g at_top at_top"
+  assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
+  assumes q: "q > 0"
+  shows   "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)"
+proof (rule smalloI_tendsto)
+  from lim_f have "eventually (\<lambda>x. f x > 0) at_top" 
+    by (simp add: filterlim_at_top_dense)
+  hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp
+  
+  from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top"
+    by (simp add: filterlim_at_top_dense)
+  hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp
+  thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top"
+    by eventually_elim simp
+  
+  have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) = 
+                          p * ln (f x) - q * ln (g x)) at_top"
+    using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps)
+  have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top"
+    by (insert q)
+       (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult
+              tendsto_const tendsto_diff smalloD_tendsto[OF ln_o_ln] lim_g
+              filterlim_compose[OF ln_at_top] | simp)+
+  hence "filterlim (\<lambda>x. p * ln (f x) - q * ln (g x)) at_bot at_top"
+    by (subst (asm) filterlim_cong[OF refl refl eq])
+  hence *: "((\<lambda>x. exp (p * ln (f x) - q * ln (g x))) \<longlongrightarrow> 0) at_top"
+    by (rule filterlim_compose[OF exp_at_bot])
+  have eq: "eventually (\<lambda>x. exp (p * ln (f x) - q * ln (g x)) = f x powr p / g x powr q) at_top"
+    using f_nz g_nz by eventually_elim (simp add: powr_def exp_diff)
+  show "((\<lambda>x. f x powr p / g x powr q) \<longlongrightarrow> 0) at_top"
+    using * by (subst (asm) filterlim_cong[OF refl refl eq])
+qed
+
+lemma ln_smallo_imp_flat':
+  fixes f g :: "real \<Rightarrow> real"
+  assumes lim_f: "filterlim f at_top at_top"
+  assumes lim_g: "filterlim g at_top at_top"
+  assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
+  assumes q: "q < 0"
+  shows   "(\<lambda>x. g x powr q) \<in> o(\<lambda>x. f x powr p)"
+proof -
+  from lim_f lim_g have "eventually (\<lambda>x. f x > 0) at_top" "eventually (\<lambda>x. g x > 0) at_top"
+    by (simp_all add: filterlim_at_top_dense)
+  hence "eventually (\<lambda>x. f x \<noteq> 0) at_top" "eventually (\<lambda>x. g x \<noteq> 0) at_top"
+    by (auto elim: eventually_mono)
+  moreover from assms have "(\<lambda>x. f x powr -p) \<in> o(\<lambda>x. g x powr -q)"
+    by (intro ln_smallo_imp_flat assms) simp_all
+  ultimately show ?thesis unfolding powr_minus
+    by (simp add: landau_o.small.inverse_cancel)
+qed
+
+
+subsection \<open>Asymptotic Equivalence\<close>
+
+(* TODO Move *)
+lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
+  by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
+
+named_theorems asymp_equiv_intros
+named_theorems asymp_equiv_simps
+
+definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  ("_ \<sim>[_] _" [51, 10, 51] 50)
+  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"
+
+abbreviation (input) asymp_equiv_at_top where
+  "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"
+
+bundle asymp_equiv_notation
+begin
+notation asymp_equiv_at_top (infix "\<sim>" 50) 
+end
+
+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"
+  by (simp add: asymp_equiv_def)
+
+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"
+  by (simp add: asymp_equiv_def)
+
+lemma asymp_equiv_filtermap_iff:
+  "f \<sim>[filtermap h F] g \<longleftrightarrow> (\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
+  by (simp add: asymp_equiv_def filterlim_filtermap)
+
+lemma asymp_equiv_refl [simp, asymp_equiv_intros]: "f \<sim>[F] f"
+proof (intro asymp_equivI)
+  have "eventually (\<lambda>x. 1 = (if f x = 0 \<and> f x = 0 then 1 else f x / f x)) F"
+    by (intro always_eventually) simp
+  moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
+  ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
+    by (rule Lim_transform_eventually)
+qed
+
+lemma asymp_equiv_symI: 
+  assumes "f \<sim>[F] g"
+  shows   "g \<sim>[F] f"
+  using tendsto_inverse[OF asymp_equivD[OF assms]]
+  by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong)
+
+lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f"
+  by (blast intro: asymp_equiv_symI)
+
+lemma asymp_equivI': 
+  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
+  shows   "f \<sim>[F] g"
+proof (cases "F = bot")
+  case False
+  have "eventually (\<lambda>x. f x \<noteq> 0) F"
+  proof (rule ccontr)
+    assume "\<not>eventually (\<lambda>x. f x \<noteq> 0) F"
+    hence "frequently (\<lambda>x. f x = 0) F" by (simp add: frequently_def)
+    hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1)
+    from limit_frequently_eq[OF False this assms] show False by simp_all
+  qed
+  hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"
+    by eventually_elim simp
+  from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def 
+    by (rule Lim_transform_eventually)
+qed (simp_all add: asymp_equiv_def)
+
+
+lemma asymp_equiv_cong:
+  assumes "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
+  shows   "f1 \<sim>[F] g1 \<longleftrightarrow> f2 \<sim>[F] g2"
+  unfolding asymp_equiv_def
+proof (rule tendsto_cong, goal_cases)
+  case 1
+  from assms show ?case by eventually_elim simp
+qed
+
+lemma asymp_equiv_eventually_zeros:
+  fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
+  assumes "f \<sim>[F] g"
+  shows   "eventually (\<lambda>x. f x = 0 \<longleftrightarrow> g x = 0) F"
+proof -
+  let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+  have "eventually (\<lambda>x. x \<noteq> 0) (nhds (1::'b))"
+    by (rule t1_space_nhds) auto
+  hence "eventually (\<lambda>x. x \<noteq> 0) (filtermap ?h F)"
+    using assms unfolding asymp_equiv_def filterlim_def
+    by (rule filter_leD [rotated])
+  hence "eventually (\<lambda>x. ?h x \<noteq> 0) F" by (simp add: eventually_filtermap)
+  thus ?thesis by eventually_elim (auto split: if_splits)
+qed
+
+lemma asymp_equiv_transfer:
+  assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
+  shows   "f2 \<sim>[F] g2"
+  using assms(1) asymp_equiv_cong[OF assms(2,3)] by simp
+
+lemma asymp_equiv_transfer_trans [trans]:
+  assumes "(\<lambda>x. f x (h1 x)) \<sim>[F] (\<lambda>x. g x (h1 x))"
+  assumes "eventually (\<lambda>x. h1 x = h2 x) F"
+  shows   "(\<lambda>x. f x (h2 x)) \<sim>[F] (\<lambda>x. g x (h2 x))"
+  by (rule asymp_equiv_transfer[OF assms(1)]) (insert assms(2), auto elim!: eventually_mono)
+
+lemma asymp_equiv_trans [trans]:
+  fixes f g h
+  assumes "f \<sim>[F] g" "g \<sim>[F] h"
+  shows   "f \<sim>[F] h"
+proof -
+  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+  from assms[THEN asymp_equiv_eventually_zeros]
+    have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
+  moreover from tendsto_mult[OF assms[THEN asymp_equivD]] 
+    have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
+  ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
+qed
+
+lemma asymp_equiv_trans_lift1 [trans]:
+  assumes "a \<sim>[F] f b" "b \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
+  shows   "a \<sim>[F] f c"
+  using assms by (blast intro: asymp_equiv_trans)
+
+lemma asymp_equiv_trans_lift2 [trans]:
+  assumes "f a \<sim>[F] b" "a \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
+  shows   "f c \<sim>[F] b"
+  using asymp_equiv_symI[OF assms(3)[OF assms(2)]] assms(1)
+  by (blast intro: asymp_equiv_trans)
+
+lemma asymp_equivD_const:
+  assumes "f \<sim>[F] (\<lambda>_. c)"
+  shows   "(f \<longlongrightarrow> c) F"
+proof (cases "c = 0")
+  case False
+  with tendsto_mult_right[OF asymp_equivD[OF assms], of c] show ?thesis by simp
+next
+  case True
+  with asymp_equiv_eventually_zeros[OF assms] show ?thesis
+    by (simp add: Lim_eventually)
+qed
+
+lemma asymp_equiv_refl_ev:
+  assumes "eventually (\<lambda>x. f x = g x) F"
+  shows   "f \<sim>[F] g"
+  by (intro asymp_equivI Lim_eventually)
+     (insert assms, auto elim!: eventually_mono)
+
+lemma asymp_equiv_sandwich:
+  fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"
+  assumes "eventually (\<lambda>x. f x \<ge> 0) F"
+  assumes "eventually (\<lambda>x. f x \<le> g x) F"
+  assumes "eventually (\<lambda>x. g x \<le> h x) F"
+  assumes "f \<sim>[F] h"
+  shows   "g \<sim>[F] f" "g \<sim>[F] h"
+proof -
+  show "g \<sim>[F] f"
+  proof (rule asymp_equivI, rule tendsto_sandwich)
+    from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
+      show "eventually (\<lambda>n. (if h n = 0 \<and> f n = 0 then 1 else h n / f n) \<ge>
+                              (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
+        by eventually_elim (auto intro!: divide_right_mono)
+    from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
+      show "eventually (\<lambda>n. 1 \<le>
+                              (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
+        by eventually_elim (auto intro!: divide_right_mono)
+  qed (insert asymp_equiv_symI[OF assms(4)], simp_all add: asymp_equiv_def)
+  also note \<open>f \<sim>[F] h\<close>
+  finally show "g \<sim>[F] h" .
+qed
+
+lemma asymp_equiv_imp_eventually_same_sign:
+  fixes f g :: "real \<Rightarrow> real"
+  assumes "f \<sim>[F] g"
+  shows   "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
+proof -
+  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"
+    unfolding asymp_equiv_def by (rule tendsto_sgn) simp_all
+  from order_tendstoD(1)[OF this, of "1/2"]
+    have "eventually (\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x) > 1/2) F"
+    by simp
+  thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
+  proof eventually_elim
+    case (elim x)
+    thus ?case
+      by (cases "f x" "0 :: real" rule: linorder_cases; 
+          cases "g x" "0 :: real" rule: linorder_cases) simp_all
+  qed
+qed
+
+lemma
+  fixes f g :: "_ \<Rightarrow> real"
+  assumes "f \<sim>[F] g"
+  shows   asymp_equiv_eventually_same_sign: "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" (is ?th1)
+    and   asymp_equiv_eventually_neg_iff:   "eventually (\<lambda>x. f x < 0 \<longleftrightarrow> g x < 0) F" (is ?th2)
+    and   asymp_equiv_eventually_pos_iff:   "eventually (\<lambda>x. f x > 0 \<longleftrightarrow> g x > 0) F" (is ?th3)
+proof -
+  from assms have "filterlim (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) (nhds 1) F"
+    by (rule asymp_equivD)
+  from order_tendstoD(1)[OF this zero_less_one]
+    show ?th1 ?th2 ?th3
+    by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+
+qed
+
+lemma asymp_equiv_tendsto_transfer:
+  assumes "f \<sim>[F] g" and "(f \<longlongrightarrow> c) F"
+  shows   "(g \<longlongrightarrow> c) F"
+proof -
+  let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"
+  have "eventually (\<lambda>x. ?h x = g x) F"
+    using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
+  moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
+  hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"
+    by (rule asymp_equivD)
+  from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp
+  ultimately show ?thesis by (rule Lim_transform_eventually)
+qed
+
+lemma tendsto_asymp_equiv_cong:
+  assumes "f \<sim>[F] g"
+  shows   "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"
+proof -
+  {
+    fix f g :: "'a \<Rightarrow> 'b"
+    assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"
+    have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"
+      using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp
+    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"
+      by (intro tendsto_intros asymp_equivD *)
+    ultimately have "(f \<longlongrightarrow> c * 1) F"
+      by (rule Lim_transform_eventually)
+  }
+  from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym)
+qed
+
+
+lemma smallo_imp_eventually_sgn:
+  fixes f g :: "real \<Rightarrow> real"
+  assumes "g \<in> o(f)"
+  shows   "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top"
+proof -
+  have "0 < (1/2 :: real)" by simp
+  from landau_o.smallD[OF assms, OF this] 
+    have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp
+  thus ?thesis
+  proof eventually_elim
+    case (elim x)
+    thus ?case
+      by (cases "f x" "0::real" rule: linorder_cases; 
+          cases "f x + g x" "0::real" rule: linorder_cases) simp_all
+  qed
+qed
+
+context
+begin
+
+private lemma asymp_equiv_add_rightI:
+  assumes "f \<sim>[F] g" "h \<in> o[F](g)"
+  shows   "(\<lambda>x. f x + h x) \<sim>[F] g"
+proof -
+  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+  from landau_o.smallD[OF assms(2) zero_less_one]
+    have ev: "eventually (\<lambda>x. g x = 0 \<longrightarrow> h x = 0) F" by eventually_elim auto
+  have "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1) F"
+    unfolding asymp_equiv_def using ev
+    by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps)
+  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1 + 0) F" by simp
+  also have \<dots> by (intro tendsto_intros asymp_equivD assms smalloD_tendsto)
+  finally show "(\<lambda>x. f x + h x) \<sim>[F] g" .
+qed
+
+lemma asymp_equiv_add_right [asymp_equiv_simps]:
+  assumes "h \<in> o[F](g)"
+  shows   "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
+proof
+  assume "(\<lambda>x. f x + h x) \<sim>[F] g"
+  from asymp_equiv_add_rightI[OF this, of "\<lambda>x. -h x"] assms show "f \<sim>[F] g"
+    by simp
+qed (simp_all add: asymp_equiv_add_rightI assms)
+
+end
+
+lemma asymp_equiv_add_left [asymp_equiv_simps]: 
+  assumes "h \<in> o[F](g)"
+  shows   "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
+  using asymp_equiv_add_right[OF assms] by (simp add: add.commute)
+
+lemma asymp_equiv_add_right' [asymp_equiv_simps]:
+  assumes "h \<in> o[F](g)"
+  shows   "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f"
+  using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym)
+  
+lemma asymp_equiv_add_left' [asymp_equiv_simps]:
+  assumes "h \<in> o[F](g)"
+  shows   "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f"
+  using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym)
+
+lemma smallo_imp_asymp_equiv:
+  assumes "(\<lambda>x. f x - g x) \<in> o[F](g)"
+  shows   "f \<sim>[F] g"
+proof -
+  from assms have "(\<lambda>x. f x - g x + g x) \<sim>[F] g"
+    by (subst asymp_equiv_add_left) simp_all
+  thus ?thesis by simp
+qed
+
+lemma asymp_equiv_uminus [asymp_equiv_intros]:
+  "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. -f x) \<sim>[F] (\<lambda>x. -g x)"
+  by (simp add: asymp_equiv_def cong: if_cong)
+
+lemma asymp_equiv_uminus_iff [asymp_equiv_simps]:
+  "(\<lambda>x. -f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] (\<lambda>x. -g x)"
+  by (simp add: asymp_equiv_def cong: if_cong)
+
+lemma asymp_equiv_mult [asymp_equiv_intros]:
+  fixes f1 f2 g1 g2 :: "'a \<Rightarrow> 'b :: real_normed_field"
+  assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
+  shows   "(\<lambda>x. f1 x * f2 x) \<sim>[F] (\<lambda>x. g1 x * g2 x)"
+proof -
+  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+  let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x
+                   else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)"
+  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"
+  {
+    fix f g :: "'a \<Rightarrow> 'b" assume "f \<sim>[F] g"
+    have "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F"
+      by (rule tendsto_eq_intros refl asymp_equivD[OF \<open>f \<sim>[F] g\<close>])+ simp_all
+  } note A = this    
+
+  from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"
+    by (intro tendsto_mult asymp_equivD)
+  moreover {
+    have "eventually (\<lambda>x. ?S x = ?S' x) F"
+      using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
+    moreover have "(?S \<longlongrightarrow> 0) F"
+      by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])
+         (auto intro: le_infI1 le_infI2)
+    ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)
+  }
+  ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"
+    by (rule Lim_transform)
+  thus ?thesis by (simp add: asymp_equiv_def)
+qed
+
+lemma asymp_equiv_power [asymp_equiv_intros]:
+  "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)"
+  by (induction n) (simp_all add: asymp_equiv_mult)
+
+lemma asymp_equiv_inverse [asymp_equiv_intros]:
+  assumes "f \<sim>[F] g"
+  shows   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
+proof -
+  from tendsto_inverse[OF asymp_equivD[OF assms]]
+    have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) \<longlongrightarrow> 1) F"
+    by (simp add: if_distrib cong: if_cong)
+  also have "(\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) =
+               (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else inverse (f x) / inverse (g x))"
+    by (intro ext) (simp add: field_simps)
+  finally show ?thesis by (simp add: asymp_equiv_def)
+qed
+
+lemma asymp_equiv_inverse_iff [asymp_equiv_simps]:
+  "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<sim>[F] g"
+proof
+  assume "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
+  hence "(\<lambda>x. inverse (inverse (f x))) \<sim>[F] (\<lambda>x. inverse (inverse (g x)))" (is ?P)
+    by (rule asymp_equiv_inverse)
+  also have "?P \<longleftrightarrow> f \<sim>[F] g" by (intro asymp_equiv_cong) simp_all
+  finally show "f \<sim>[F] g" .
+qed (simp_all add: asymp_equiv_inverse)
+
+lemma asymp_equiv_divide [asymp_equiv_intros]:
+  assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
+  shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
+  using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
+
+lemma asymp_equiv_compose [asymp_equiv_intros]:
+  assumes "f \<sim>[G] g" "filterlim h G F"
+  shows   "f \<circ> h \<sim>[F] g \<circ> h"
+proof -
+  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+  have "f \<circ> h \<sim>[F] g \<circ> h \<longleftrightarrow> ((?T f g \<circ> h) \<longlongrightarrow> 1) F"
+    by (simp add: asymp_equiv_def o_def)
+  also have "\<dots> \<longleftrightarrow> (?T f g \<longlongrightarrow> 1) (filtermap h F)"
+    by (rule tendsto_compose_filtermap)
+  also have "\<dots>"
+    by (rule tendsto_mono[of _ G]) (insert assms, simp_all add: asymp_equiv_def filterlim_def)
+  finally show ?thesis .
+qed
+
+lemma asymp_equiv_compose':
+  assumes "f \<sim>[G] g" "filterlim h G F"
+  shows   "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
+  using asymp_equiv_compose[OF assms] by (simp add: o_def)
+  
+lemma asymp_equiv_powr_real [asymp_equiv_intros]:
+  fixes f g :: "'a \<Rightarrow> real"
+  assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
+  shows   "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"
+proof -
+  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+  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"
+    using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)
+    by eventually_elim (auto simp: powr_divide)
+  moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
+    by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
+  hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
+  ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
+qed
+
+lemma asymp_equiv_norm [asymp_equiv_intros]:
+  fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
+  assumes "f \<sim>[F] g"
+  shows   "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))"
+  using tendsto_norm[OF asymp_equivD[OF assms]] 
+  by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong)
+
+lemma asymp_equiv_abs_real [asymp_equiv_intros]:
+  fixes f g :: "'a \<Rightarrow> real"
+  assumes "f \<sim>[F] g"
+  shows   "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)"
+  using tendsto_rabs[OF asymp_equivD[OF assms]] 
+  by (simp add: if_distrib asymp_equiv_def cong: if_cong)
+
+lemma asymp_equiv_imp_eventually_le:
+  assumes "f \<sim>[F] g" "c > 1"
+  shows   "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"
+proof -
+  from order_tendstoD(2)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
+       asymp_equiv_eventually_zeros[OF assms(1)]
+    show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
+qed
+
+lemma asymp_equiv_imp_eventually_ge:
+  assumes "f \<sim>[F] g" "c < 1"
+  shows   "eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F"
+proof -
+  from order_tendstoD(1)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
+       asymp_equiv_eventually_zeros[OF assms(1)]
+    show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
+qed
+
+lemma asymp_equiv_imp_bigo:
+  assumes "f \<sim>[F] g"
+  shows   "f \<in> O[F](g)"
+proof (rule bigoI)
+  have "(3/2::real) > 1" by simp
+  from asymp_equiv_imp_eventually_le[OF assms this]
+    show "eventually (\<lambda>x. norm (f x) \<le> 3/2 * norm (g x)) F"
+    by eventually_elim simp
+qed
+
+lemma asymp_equiv_imp_bigomega:
+  "f \<sim>[F] g \<Longrightarrow> f \<in> \<Omega>[F](g)"
+  using asymp_equiv_imp_bigo[of g F f] by (simp add: asymp_equiv_sym bigomega_iff_bigo)
+
+lemma asymp_equiv_imp_bigtheta:
+  "f \<sim>[F] g \<Longrightarrow> f \<in> \<Theta>[F](g)"
+  by (intro bigthetaI asymp_equiv_imp_bigo asymp_equiv_imp_bigomega)
+
+lemma asymp_equiv_at_infinity_transfer:
+  assumes "f \<sim>[F] g" "filterlim f at_infinity F"
+  shows   "filterlim g at_infinity F"
+proof -
+  from assms(1) have "g \<in> \<Theta>[F](f)" by (rule asymp_equiv_imp_bigtheta[OF asymp_equiv_symI])
+  also from assms have "f \<in> \<omega>[F](\<lambda>_. 1)" by (simp add: smallomega_1_conv_filterlim)
+  finally show ?thesis by (simp add: smallomega_1_conv_filterlim)
+qed
+
+lemma asymp_equiv_at_top_transfer:
+  fixes f g :: "_ \<Rightarrow> real"
+  assumes "f \<sim>[F] g" "filterlim f at_top F"
+  shows   "filterlim g at_top F"
+proof (rule filterlim_at_infinity_imp_filterlim_at_top)
+  show "filterlim g at_infinity F"
+    by (rule asymp_equiv_at_infinity_transfer[OF assms(1) filterlim_mono[OF assms(2)]])
+       (auto simp: at_top_le_at_infinity)
+  from assms(2) have "eventually (\<lambda>x. f x > 0) F"
+    using filterlim_at_top_dense by blast
+  with asymp_equiv_eventually_pos_iff[OF assms(1)] show "eventually (\<lambda>x. g x > 0) F"
+    by eventually_elim blast
+qed
+
+lemma asymp_equiv_at_bot_transfer:
+  fixes f g :: "_ \<Rightarrow> real"
+  assumes "f \<sim>[F] g" "filterlim f at_bot F"
+  shows   "filterlim g at_bot F"
+  unfolding filterlim_uminus_at_bot
+  by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"])
+     (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus)  
+
+lemma asymp_equivI'_const:
+  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0"
+  shows   "f \<sim>[F] (\<lambda>x. c * g x)"
+  using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2)
+  by (intro asymp_equivI') (simp add: field_simps)
+
+lemma asymp_equivI'_inverse_const:
+  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> inverse c) F" "c \<noteq> 0"
+  shows   "(\<lambda>x. c * f x) \<sim>[F] g"
+  using tendsto_mult[OF assms(1) tendsto_const[of "c"]] assms(2)
+  by (intro asymp_equivI') (simp add: field_simps)
+
+lemma filterlim_at_bot_imp_at_infinity: "filterlim f at_bot F \<Longrightarrow> filterlim f at_infinity F"
+  for f :: "_ \<Rightarrow> real" using at_bot_le_at_infinity filterlim_mono by blast
+
+lemma asymp_equiv_imp_diff_smallo:
+  assumes "f \<sim>[F] g"
+  shows   "(\<lambda>x. f x - g x) \<in> o[F](g)"
+proof (rule landau_o.smallI)
+  fix c :: real assume "c > 0"
+  hence c: "min c 1 > 0" by simp
+  let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+  from assms have "((\<lambda>x. ?h x - 1) \<longlongrightarrow> 1 - 1) F"
+    by (intro tendsto_diff asymp_equivD tendsto_const)
+  from tendstoD[OF this c] show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
+  proof eventually_elim
+    case (elim x)
+    from elim have "norm (f x - g x) \<le> norm (f x / g x - 1) * norm (g x)"
+      by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps)
+    also have "norm (f x / g x - 1) * norm (g x) \<le> c * norm (g x)" using elim
+      by (auto split: if_splits simp: mult_right_mono)
+    finally show ?case .
+  qed
+qed
+
+lemma asymp_equiv_altdef:
+  "f \<sim>[F] g \<longleftrightarrow> (\<lambda>x. f x - g x) \<in> o[F](g)"
+  by (rule iffI[OF asymp_equiv_imp_diff_smallo smallo_imp_asymp_equiv])
+
+lemma asymp_equiv_0_left_iff [simp]: "(\<lambda>_. 0) \<sim>[F] f \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+  and asymp_equiv_0_right_iff [simp]: "f \<sim>[F] (\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+  by (simp_all add: asymp_equiv_altdef landau_o.small_refl_iff)
+
+lemma asymp_equiv_sandwich_real:
+  fixes f g l u :: "'a \<Rightarrow> real"
+  assumes "l \<sim>[F] g" "u \<sim>[F] g" "eventually (\<lambda>x. f x \<in> {l x..u x}) F"
+  shows   "f \<sim>[F] g"
+  unfolding asymp_equiv_altdef
+proof (rule landau_o.smallI)
+  fix c :: real assume c: "c > 0"
+  have "eventually (\<lambda>x. norm (f x - g x) \<le> max (norm (l x - g x)) (norm (u x - g x))) F"
+    using assms(3) by eventually_elim auto
+  moreover have "eventually (\<lambda>x. norm (l x - g x) \<le> c * norm (g x)) F"
+                "eventually (\<lambda>x. norm (u x - g x) \<le> c * norm (g x)) F"
+    using assms(1,2) by (auto simp: asymp_equiv_altdef dest: landau_o.smallD[OF _ c])
+  hence "eventually (\<lambda>x. max (norm (l x - g x)) (norm (u x - g x)) \<le> c * norm (g x)) F"
+    by eventually_elim simp
+  ultimately show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
+    by eventually_elim (rule order.trans)
+qed
+
+lemma asymp_equiv_sandwich_real':
+  fixes f g l u :: "'a \<Rightarrow> real"
+  assumes "f \<sim>[F] l" "f \<sim>[F] u" "eventually (\<lambda>x. g x \<in> {l x..u x}) F"
+  shows   "f \<sim>[F] g"
+  using asymp_equiv_sandwich_real[of l F f u g] assms by (simp add: asymp_equiv_sym)
+
+lemma asymp_equiv_sandwich_real'':
+  fixes f g l u :: "'a \<Rightarrow> real"
+  assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"
+          "eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"
+  shows   "f \<sim>[F] g"
+  by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]
+             asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];
+      blast intro: asymp_equiv_trans assms(1,2,3))+
+
+end
diff -r 37974ddde928 -r b48bab511939 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue May 22 11:05:47 2018 +0200
+++ b/src/HOL/Library/Library.thy	Fri May 18 17:51:58 2018 +0200
@@ -38,6 +38,7 @@
   Indicator_Function
   Infinite_Set
   IArray
+  Landau_Symbols
   Lattice_Algebras
   Lattice_Syntax
   Lattice_Constructions