src/HOL/Library/Landau_Symbols.thy

Moved Landau_Symbols from the AFP to HOL-Library

(*
  File:   Landau_Symbols_Definition.thy
  Author: Manuel Eberl <[e-mail]>

  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