src/HOL/Library/Landau_Symbols.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (4 months ago) changeset 69946 494934c30f38 parent 69597 ff784d5a5bfb child 70365 4df0628e8545 permissions -rw-r--r--
improved code equations taken over from AFP
     1 (*

     2   File:   Landau_Symbols_Definition.thy

     3   Author: Manuel Eberl <eberlm@in.tum.de>

     4

     5   Landau symbols for reasoning about the asymptotic growth of functions.

     6 *)

     7 section \<open>Definition of Landau symbols\<close>

     8

     9 theory Landau_Symbols

    10 imports

    11   Complex_Main

    12 begin

    13

    14 lemma eventually_subst':

    15   "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> eventually (\<lambda>x. P x (f x)) F = eventually (\<lambda>x. P x (g x)) F"

    16   by (rule eventually_subst, erule eventually_rev_mp) simp

    17

    18

    19 subsection \<open>Definition of Landau symbols\<close>

    20

    21 text \<open>

    22   Our Landau symbols are sign-oblivious, i.e. any function always has the same growth

    23   as its absolute. This has the advantage of making some cancelling rules for sums nicer, but

    24   introduces some problems in other places. Nevertheless, we found this definition more convenient

    25   to work with.

    26 \<close>

    27

    28 definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"

    29     (\<open>(1O[_]'(_'))\<close>)

    30   where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"

    31

    32 definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"

    33     (\<open>(1o[_]'(_'))\<close>)

    34   where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"

    35

    36 definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"

    37     (\<open>(1\<Omega>[_]'(_'))\<close>)

    38   where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"

    39

    40 definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"

    41     (\<open>(1\<omega>[_]'(_'))\<close>)

    42   where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"

    43

    44 definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"

    45     (\<open>(1\<Theta>[_]'(_'))\<close>)

    46   where "bigtheta F g = bigo F g \<inter> bigomega F g"

    47

    48 abbreviation bigo_at_top (\<open>(2O'(_'))\<close>) where

    49   "O(g) \<equiv> bigo at_top g"

    50

    51 abbreviation smallo_at_top (\<open>(2o'(_'))\<close>) where

    52   "o(g) \<equiv> smallo at_top g"

    53

    54 abbreviation bigomega_at_top (\<open>(2\<Omega>'(_'))\<close>) where

    55   "\<Omega>(g) \<equiv> bigomega at_top g"

    56

    57 abbreviation smallomega_at_top (\<open>(2\<omega>'(_'))\<close>) where

    58   "\<omega>(g) \<equiv> smallomega at_top g"

    59

    60 abbreviation bigtheta_at_top (\<open>(2\<Theta>'(_'))\<close>) where

    61   "\<Theta>(g) \<equiv> bigtheta at_top g"

    62

    63

    64 text \<open>The following is a set of properties that all Landau symbols satisfy.\<close>

    65

    66 named_theorems landau_divide_simps

    67

    68 locale landau_symbol =

    69   fixes L  :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"

    70   and   L'  :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"

    71   and   Lr  :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"

    72   assumes bot': "L bot f = UNIV"

    73   assumes filter_mono': "F1 \<le> F2 \<Longrightarrow> L F2 f \<subseteq> L F1 f"

    74   assumes in_filtermap_iff:

    75     "f' \<in> L (filtermap h' F') g' \<longleftrightarrow> (\<lambda>x. f' (h' x)) \<in> L' F' (\<lambda>x. g' (h' x))"

    76   assumes filtercomap:

    77     "f' \<in> L F'' g' \<Longrightarrow> (\<lambda>x. f' (h' x)) \<in> L' (filtercomap h' F'') (\<lambda>x. g' (h' x))"

    78   assumes sup: "f \<in> L F1 g \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L (sup F1 F2) g"

    79   assumes in_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"

    80   assumes cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> L F (f) = L F (g)"

    81   assumes cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> L F (f) = L F (g)"

    82   assumes in_cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"

    83   assumes cmult [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. c * f x) = L F (f)"

    84   assumes cmult_in_iff [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"

    85   assumes mult_left [simp]: "f \<in> L F (g) \<Longrightarrow> (\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)"

    86   assumes inverse: "eventually (\<lambda>x. f x \<noteq> 0) F \<Longrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F \<Longrightarrow>

    87                         f \<in> L F (g) \<Longrightarrow> (\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))"

    88   assumes subsetI: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"

    89   assumes plus_subset1: "f \<in> o[F](g) \<Longrightarrow> L F (g) \<subseteq> L F (\<lambda>x. f x + g x)"

    90   assumes trans: "f \<in> L F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"

    91   assumes compose: "f \<in> L F (g) \<Longrightarrow> filterlim h' F G \<Longrightarrow> (\<lambda>x. f (h' x)) \<in> L' G (\<lambda>x. g (h' x))"

    92   assumes norm_iff [simp]: "(\<lambda>x. norm (f x)) \<in> Lr F (\<lambda>x. norm (g x)) \<longleftrightarrow> f \<in> L F (g)"

    93   assumes abs [simp]: "Lr Fr (\<lambda>x. \<bar>fr x\<bar>) = Lr Fr fr"

    94   assumes abs_in_iff [simp]: "(\<lambda>x. \<bar>fr x\<bar>) \<in> Lr Fr gr \<longleftrightarrow> fr \<in> Lr Fr gr"

    95 begin

    96

    97 lemma bot [simp]: "f \<in> L bot g" by (simp add: bot')

    98

    99 lemma filter_mono: "F1 \<le> F2 \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L F1 g"

   100   using filter_mono'[of F1 F2] by blast

   101

   102 lemma cong_ex:

   103   "eventually (\<lambda>x. f1 x = f2 x) F \<Longrightarrow> eventually (\<lambda>x. g1 x = g2 x) F \<Longrightarrow>

   104      f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)"

   105   by (subst cong, assumption, subst in_cong, assumption, rule refl)

   106

   107 lemma cong_ex_bigtheta:

   108   "f1 \<in> \<Theta>[F](f2) \<Longrightarrow> g1 \<in> \<Theta>[F](g2) \<Longrightarrow> f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)"

   109   by (subst cong_bigtheta, assumption, subst in_cong_bigtheta, assumption, rule refl)

   110

   111 lemma bigtheta_trans1:

   112   "f \<in> L F (g) \<Longrightarrow> g \<in> \<Theta>[F](h) \<Longrightarrow> f \<in> L F (h)"

   113   by (subst cong_bigtheta[symmetric])

   114

   115 lemma bigtheta_trans2:

   116   "f \<in> \<Theta>[F](g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"

   117   by (subst in_cong_bigtheta)

   118

   119 lemma cmult' [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x * c) = L F (f)"

   120   by (subst mult.commute) (rule cmult)

   121

   122 lemma cmult_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x * c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"

   123   by (subst mult.commute) (rule cmult_in_iff)

   124

   125 lemma cdiv [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x / c) = L F (f)"

   126   using cmult'[of "inverse c" F f] by (simp add: field_simps)

   127

   128 lemma cdiv_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"

   129   using cmult_in_iff'[of "inverse c" f] by (simp add: field_simps)

   130

   131 lemma uminus [simp]: "L F (\<lambda>x. -g x) = L F (g)" using cmult[of "-1"] by simp

   132

   133 lemma uminus_in_iff [simp]: "(\<lambda>x. -f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"

   134   using cmult_in_iff[of "-1"] by simp

   135

   136 lemma const: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"

   137   by (subst (2) cmult[symmetric]) simp_all

   138

   139 (* Simplifier loops without the NO_MATCH *)

   140 lemma const' [simp]: "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"

   141   by (rule const)

   142

   143 lemma const_in_iff: "c \<noteq> 0 \<Longrightarrow> (\<lambda>_. c) \<in> L F (f) \<longleftrightarrow> (\<lambda>_. 1) \<in> L F (f)"

   144   using cmult_in_iff'[of c "\<lambda>_. 1"] by simp

   145

   146 lemma const_in_iff' [simp]: "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> (\<lambda>_. c) \<in> L F (f) \<longleftrightarrow> (\<lambda>_. 1) \<in> L F (f)"

   147   by (rule const_in_iff)

   148

   149 lemma plus_subset2: "g \<in> o[F](f) \<Longrightarrow> L F (f) \<subseteq> L F (\<lambda>x. f x + g x)"

   150   by (subst add.commute) (rule plus_subset1)

   151

   152 lemma mult_right [simp]: "f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (\<lambda>x. g x * h x)"

   153   using mult_left by (simp add: mult.commute)

   154

   155 lemma mult: "f1 \<in> L F (g1) \<Longrightarrow> f2 \<in> L F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"

   156   by (rule trans, erule mult_left, erule mult_right)

   157

   158 lemma inverse_cancel:

   159   assumes "eventually (\<lambda>x. f x \<noteq> 0) F"

   160   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"

   161   shows   "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> g \<in> L F (f)"

   162 proof

   163   assume "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x))"

   164   from inverse[OF _ _ this] assms show "g \<in> L F (f)" by simp

   165 qed (intro inverse assms)

   166

   167 lemma divide_right:

   168   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"

   169   assumes "f \<in> L F (g)"

   170   shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"

   171   by (subst (1 2) divide_inverse) (intro mult_right inverse assms)

   172

   173 lemma divide_right_iff:

   174   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"

   175   shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> f \<in> L F (g)"

   176 proof

   177   assume "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"

   178   from mult_right[OF this, of h] assms show "f \<in> L F (g)"

   179     by (subst (asm) cong_ex[of _ f F _ g]) (auto elim!: eventually_mono)

   180 qed (simp add: divide_right assms)

   181

   182 lemma divide_left:

   183   assumes "eventually (\<lambda>x. f x \<noteq> 0) F"

   184   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"

   185   assumes "g \<in> L F(f)"

   186   shows   "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"

   187   by (subst (1 2) divide_inverse) (intro mult_left inverse assms)

   188

   189 lemma divide_left_iff:

   190   assumes "eventually (\<lambda>x. f x \<noteq> 0) F"

   191   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"

   192   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"

   193   shows   "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x) \<longleftrightarrow> g \<in> L F (f)"

   194 proof

   195   assume A: "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"

   196   from assms have B: "eventually (\<lambda>x. h x / f x / h x = inverse (f x)) F"

   197     by eventually_elim (simp add: divide_inverse)

   198   from assms have C: "eventually (\<lambda>x. h x / g x / h x = inverse (g x)) F"

   199     by eventually_elim (simp add: divide_inverse)

   200   from divide_right[OF assms(3) A] assms show "g \<in> L F (f)"

   201     by (subst (asm) cong_ex[OF B C]) (simp add: inverse_cancel)

   202 qed (simp add: divide_left assms)

   203

   204 lemma divide:

   205   assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"

   206   assumes "eventually (\<lambda>x. g2 x \<noteq> 0) F"

   207   assumes "f1 \<in> L F (f2)" "g2 \<in> L F (g1)"

   208   shows   "(\<lambda>x. f1 x / g1 x) \<in> L F (\<lambda>x. f2 x / g2 x)"

   209   by (subst (1 2) divide_inverse) (intro mult inverse assms)

   210

   211 lemma divide_eq1:

   212   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"

   213   shows   "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"

   214 proof-

   215   have "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x / h x) \<in> L F (\<lambda>x. g x / h x)"

   216     using assms by (intro in_cong) (auto elim: eventually_mono)

   217   thus ?thesis by (simp only: divide_right_iff assms)

   218 qed

   219

   220 lemma divide_eq2:

   221   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"

   222   shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x) \<longleftrightarrow> f \<in> L F (\<lambda>x. g x * h x)"

   223 proof-

   224   have "L F (\<lambda>x. g x) = L F (\<lambda>x. g x * h x / h x)"

   225     using assms by (intro cong) (auto elim: eventually_mono)

   226   thus ?thesis by (simp only: divide_right_iff assms)

   227 qed

   228

   229 lemma inverse_eq1:

   230   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"

   231   shows   "f \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> (\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"

   232   using divide_eq1[of g F f "\<lambda>_. 1"] by (simp add: divide_inverse assms)

   233

   234 lemma inverse_eq2:

   235   assumes "eventually (\<lambda>x. f x \<noteq> 0) F"

   236   shows   "(\<lambda>x. inverse (f x)) \<in> L F (g) \<longleftrightarrow> (\<lambda>x. 1) \<in> L F (\<lambda>x. f x * g x)"

   237   using divide_eq2[of f F "\<lambda>_. 1" g] by (simp add: divide_inverse assms mult_ac)

   238

   239 lemma inverse_flip:

   240   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"

   241   assumes "eventually (\<lambda>x. h x \<noteq> 0) F"

   242   assumes "(\<lambda>x. inverse (g x)) \<in> L F (h)"

   243   shows   "(\<lambda>x. inverse (h x)) \<in> L F (g)"

   244 using assms by (simp add: divide_eq1 divide_eq2 inverse_eq_divide mult.commute)

   245

   246 lemma lift_trans:

   247   assumes "f \<in> L F (g)"

   248   assumes "(\<lambda>x. t x (g x)) \<in> L F (h)"

   249   assumes "\<And>f g. f \<in> L F (g) \<Longrightarrow> (\<lambda>x. t x (f x)) \<in> L F (\<lambda>x. t x (g x))"

   250   shows   "(\<lambda>x. t x (f x)) \<in> L F (h)"

   251   by (rule trans[OF assms(3)[OF assms(1)] assms(2)])

   252

   253 lemma lift_trans':

   254   assumes "f \<in> L F (\<lambda>x. t x (g x))"

   255   assumes "g \<in> L F (h)"

   256   assumes "\<And>g h. g \<in> L F (h) \<Longrightarrow> (\<lambda>x. t x (g x)) \<in> L F (\<lambda>x. t x (h x))"

   257   shows   "f \<in> L F (\<lambda>x. t x (h x))"

   258   by (rule trans[OF assms(1) assms(3)[OF assms(2)]])

   259

   260 lemma lift_trans_bigtheta:

   261   assumes "f \<in> L F (g)"

   262   assumes "(\<lambda>x. t x (g x)) \<in> \<Theta>[F](h)"

   263   assumes "\<And>f g. f \<in> L F (g) \<Longrightarrow> (\<lambda>x. t x (f x)) \<in> L F (\<lambda>x. t x (g x))"

   264   shows   "(\<lambda>x. t x (f x)) \<in> L F (h)"

   265   using cong_bigtheta[OF assms(2)] assms(3)[OF assms(1)] by simp

   266

   267 lemma lift_trans_bigtheta':

   268   assumes "f \<in> L F (\<lambda>x. t x (g x))"

   269   assumes "g \<in> \<Theta>[F](h)"

   270   assumes "\<And>g h. g \<in> \<Theta>[F](h) \<Longrightarrow> (\<lambda>x. t x (g x)) \<in> \<Theta>[F](\<lambda>x. t x (h x))"

   271   shows   "f \<in> L F (\<lambda>x. t x (h x))"

   272   using cong_bigtheta[OF assms(3)[OF assms(2)]] assms(1)  by simp

   273

   274 lemma (in landau_symbol) mult_in_1:

   275   assumes "f \<in> L F (\<lambda>_. 1)" "g \<in> L F (\<lambda>_. 1)"

   276   shows   "(\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"

   277   using mult[OF assms] by simp

   278

   279 lemma (in landau_symbol) of_real_cancel:

   280   "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<Longrightarrow> f \<in> Lr F g"

   281   by (subst (asm) norm_iff [symmetric], subst (asm) (1 2) norm_of_real) simp_all

   282

   283 lemma (in landau_symbol) of_real_iff:

   284   "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<longleftrightarrow> f \<in> Lr F g"

   285   by (subst norm_iff [symmetric], subst (1 2) norm_of_real) simp_all

   286

   287 lemmas [landau_divide_simps] =

   288   inverse_cancel divide_left_iff divide_eq1 divide_eq2 inverse_eq1 inverse_eq2

   289

   290 end

   291

   292

   293 text \<open>

   294   The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with

   295   $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem.

   296   The following locale captures this fact.

   297 \<close>

   298

   299 locale landau_pair =

   300   fixes L l :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"

   301   fixes L' l' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"

   302   fixes Lr lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"

   303   and   R :: "real \<Rightarrow> real \<Rightarrow> bool"

   304   assumes L_def: "L F g = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"

   305   and     l_def: "l F g = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"

   306   and     L'_def: "L' F' g' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"

   307   and     l'_def: "l' F' g' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"

   308   and     Lr_def: "Lr F'' g'' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"

   309   and     lr_def: "lr F'' g'' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"

   310   and     R:     "R = (\<le>) \<or> R = (\<ge>)"

   311

   312 interpretation landau_o:

   313     landau_pair bigo smallo bigo smallo bigo smallo "(\<le>)"

   314   by unfold_locales (auto simp: bigo_def smallo_def intro!: ext)

   315

   316 interpretation landau_omega:

   317     landau_pair bigomega smallomega bigomega smallomega bigomega smallomega "(\<ge>)"

   318   by unfold_locales (auto simp: bigomega_def smallomega_def intro!: ext)

   319

   320

   321 context landau_pair

   322 begin

   323

   324 lemmas R_E = disjE [OF R, case_names le ge]

   325

   326 lemma bigI:

   327   "c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F \<Longrightarrow> f \<in> L F (g)"

   328   unfolding L_def by blast

   329

   330 lemma bigE:

   331   assumes "f \<in> L F (g)"

   332   obtains c where "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"

   333   using assms unfolding L_def by blast

   334

   335 lemma smallI:

   336   "(\<And>c. c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F) \<Longrightarrow> f \<in> l F (g)"

   337   unfolding l_def by blast

   338

   339 lemma smallD:

   340   "f \<in> l F (g) \<Longrightarrow> c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"

   341   unfolding l_def by blast

   342

   343 lemma bigE_nonneg_real:

   344   assumes "f \<in> Lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F"

   345   obtains c where "c > 0" "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"

   346 proof-

   347   from assms(1) obtain c where c: "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"

   348     by (auto simp: Lr_def)

   349   from c(2) assms(2) have "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"

   350     by eventually_elim simp

   351   from c(1) and this show ?thesis by (rule that)

   352 qed

   353

   354 lemma smallD_nonneg_real:

   355   assumes "f \<in> lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F" "c > 0"

   356   shows   "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"

   357   using assms by (auto simp: lr_def dest!: spec[of _ c] elim: eventually_elim2)

   358

   359 lemma small_imp_big: "f \<in> l F (g) \<Longrightarrow> f \<in> L F (g)"

   360   by (rule bigI[OF _ smallD, of 1]) simp_all

   361

   362 lemma small_subset_big: "l F (g) \<subseteq> L F (g)"

   363   using small_imp_big by blast

   364

   365 lemma R_refl [simp]: "R x x" using R by auto

   366

   367 lemma R_linear: "\<not>R x y \<Longrightarrow> R y x"

   368   using R by auto

   369

   370 lemma R_trans [trans]: "R a b \<Longrightarrow> R b c \<Longrightarrow> R a c"

   371   using R by auto

   372

   373 lemma R_mult_left_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (c*a) (c*b)"

   374   using R by (auto simp: mult_left_mono)

   375

   376 lemma R_mult_right_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (a*c) (b*c)"

   377   using R by (auto simp: mult_right_mono)

   378

   379 lemma big_trans:

   380   assumes "f \<in> L F (g)" "g \<in> L F (h)"

   381   shows   "f \<in> L F (h)"

   382 proof-

   383   from assms(1) guess c by (elim bigE) note c = this

   384   from assms(2) guess d by (elim bigE) note d = this

   385   from c(2) d(2) have "eventually (\<lambda>x. R (norm (f x)) (c * d * (norm (h x)))) F"

   386   proof eventually_elim

   387     fix x assume "R (norm (f x)) (c * (norm (g x)))"

   388     also assume "R (norm (g x)) (d * (norm (h x)))"

   389     with c(1) have "R (c * (norm (g x))) (c * (d * (norm (h x))))"

   390       by (intro R_mult_left_mono) simp_all

   391     finally show "R (norm (f x)) (c * d * (norm (h x)))" by (simp add: algebra_simps)

   392   qed

   393   with c(1) d(1) show ?thesis by (intro bigI[of "c*d"]) simp_all

   394 qed

   395

   396 lemma big_small_trans:

   397   assumes "f \<in> L F (g)" "g \<in> l F (h)"

   398   shows   "f \<in> l F (h)"

   399 proof (rule smallI)

   400   fix c :: real assume c: "c > 0"

   401   from assms(1) guess d by (elim bigE) note d = this

   402   note d(2)

   403   moreover from c d assms(2)

   404     have "eventually (\<lambda>x. R (norm (g x)) (c * inverse d * norm (h x))) F"

   405     by (intro smallD) simp_all

   406   ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * (norm (h x)))) F"

   407     by eventually_elim (erule R_trans, insert R d(1), auto simp: field_simps)

   408 qed

   409

   410 lemma small_big_trans:

   411   assumes "f \<in> l F (g)" "g \<in> L F (h)"

   412   shows   "f \<in> l F (h)"

   413 proof (rule smallI)

   414   fix c :: real assume c: "c > 0"

   415   from assms(2) guess d by (elim bigE) note d = this

   416   note d(2)

   417   moreover from c d assms(1)

   418     have "eventually (\<lambda>x. R (norm (f x)) (c * inverse d * norm (g x))) F"

   419     by (intro smallD) simp_all

   420   ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * norm (h x))) F"

   421     by eventually_elim (rotate_tac 2, erule R_trans, insert R c d(1), auto simp: field_simps)

   422 qed

   423

   424 lemma small_trans:

   425   "f \<in> l F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> l F (h)"

   426   by (rule big_small_trans[OF small_imp_big])

   427

   428 lemma small_big_trans':

   429   "f \<in> l F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"

   430   by (rule small_imp_big[OF small_big_trans])

   431

   432 lemma big_small_trans':

   433   "f \<in> L F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> L F (h)"

   434   by (rule small_imp_big[OF big_small_trans])

   435

   436 lemma big_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"

   437   by (intro subsetI) (drule (1) big_trans)

   438

   439 lemma small_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> l F (f) \<subseteq> l F (g)"

   440   by (intro subsetI) (drule (1) small_big_trans)

   441

   442 lemma big_refl [simp]: "f \<in> L F (f)"

   443   by (rule bigI[of 1]) simp_all

   444

   445 lemma small_refl_iff: "f \<in> l F (f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

   446 proof (rule iffI[OF _ smallI])

   447   assume f: "f \<in> l F f"

   448   have "(1/2::real) > 0" "(2::real) > 0" by simp_all

   449   from smallD[OF f this(1)] smallD[OF f this(2)]

   450     show "eventually (\<lambda>x. f x = 0) F" by eventually_elim (insert R, auto)

   451 next

   452   fix c :: real assume "c > 0" "eventually (\<lambda>x. f x = 0) F"

   453   from this(2) show "eventually (\<lambda>x. R (norm (f x)) (c * norm (f x))) F"

   454     by eventually_elim simp_all

   455 qed

   456

   457 lemma big_small_asymmetric: "f \<in> L F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"

   458   by (drule (1) big_small_trans) (simp add: small_refl_iff)

   459

   460 lemma small_big_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> L F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"

   461   by (drule (1) small_big_trans) (simp add: small_refl_iff)

   462

   463 lemma small_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"

   464   by (drule (1) small_trans) (simp add: small_refl_iff)

   465

   466

   467 lemma plus_aux:

   468   assumes "f \<in> o[F](g)"

   469   shows "g \<in> L F (\<lambda>x. f x + g x)"

   470 proof (rule R_E)

   471   assume [simp]: "R = (\<le>)"

   472   have A: "1/2 > (0::real)" by simp

   473   {

   474     fix x assume "norm (f x) \<le> 1/2 * norm (g x)"

   475     hence "1/2 * (norm (g x)) \<le> (norm (g x)) - (norm (f x))" by simp

   476     also have "norm (g x) - norm (f x) \<le> norm (f x + g x)"

   477       by (subst add.commute) (rule norm_diff_ineq)

   478     finally have "1/2 * (norm (g x)) \<le> norm (f x + g x)" by simp

   479   } note B = this

   480

   481   show "g \<in> L F (\<lambda>x. f x + g x)"

   482     apply (rule bigI[of "2"], simp)

   483     using landau_o.smallD[OF assms A] apply eventually_elim

   484     using B apply (simp add: algebra_simps)

   485     done

   486 next

   487   assume [simp]: "R = (\<lambda>x y. x \<ge> y)"

   488   show "g \<in> L F (\<lambda>x. f x + g x)"

   489   proof (rule bigI[of "1/2"])

   490     show "eventually (\<lambda>x. R (norm (g x)) (1/2 * norm (f x + g x))) F"

   491       using landau_o.smallD[OF assms zero_less_one]

   492     proof eventually_elim

   493       case (elim x)

   494       have "norm (f x + g x) \<le> norm (f x) + norm (g x)" by (rule norm_triangle_ineq)

   495       also note elim

   496       finally show ?case by simp

   497     qed

   498   qed simp_all

   499 qed

   500

   501 end

   502

   503

   504

   505 lemma bigomega_iff_bigo: "g \<in> \<Omega>[F](f) \<longleftrightarrow> f \<in> O[F](g)"

   506 proof

   507   assume "f \<in> O[F](g)"

   508   then guess c by (elim landau_o.bigE)

   509   thus "g \<in> \<Omega>[F](f)" by (intro landau_omega.bigI[of "inverse c"]) (simp_all add: field_simps)

   510 next

   511   assume "g \<in> \<Omega>[F](f)"

   512   then guess c by (elim landau_omega.bigE)

   513   thus "f \<in> O[F](g)" by (intro landau_o.bigI[of "inverse c"]) (simp_all add: field_simps)

   514 qed

   515

   516 lemma smallomega_iff_smallo: "g \<in> \<omega>[F](f) \<longleftrightarrow> f \<in> o[F](g)"

   517 proof

   518   assume "f \<in> o[F](g)"

   519   from landau_o.smallD[OF this, of "inverse c" for c]

   520     show "g \<in> \<omega>[F](f)" by (intro landau_omega.smallI) (simp_all add: field_simps)

   521 next

   522   assume "g \<in> \<omega>[F](f)"

   523   from landau_omega.smallD[OF this, of "inverse c" for c]

   524     show "f \<in> o[F](g)" by (intro landau_o.smallI) (simp_all add: field_simps)

   525 qed

   526

   527

   528 context landau_pair

   529 begin

   530

   531 lemma big_mono:

   532   "eventually (\<lambda>x. R (norm (f x)) (norm (g x))) F \<Longrightarrow> f \<in> L F (g)"

   533   by (rule bigI[OF zero_less_one]) simp

   534

   535 lemma big_mult:

   536   assumes "f1 \<in> L F (g1)" "f2 \<in> L F (g2)"

   537   shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"

   538 proof-

   539   from assms(1) guess c1 by (elim bigE) note c1 = this

   540   from assms(2) guess c2 by (elim bigE) note c2 = this

   541

   542   from c1(1) and c2(1) have "c1 * c2 > 0" by simp

   543   moreover have "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * c2 * norm (g1 x * g2 x))) F"

   544     using c1(2) c2(2)

   545   proof eventually_elim

   546     case (elim x)

   547     show ?case

   548     proof (cases rule: R_E)

   549       case le

   550       have "norm (f1 x) * norm (f2 x) \<le> (c1 * norm (g1 x)) * (c2 * norm (g2 x))"

   551         using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto

   552       with le show ?thesis by (simp add: le norm_mult mult_ac)

   553     next

   554       case ge

   555       have "(c1 * norm (g1 x)) * (c2 * norm (g2 x)) \<le> norm (f1 x) * norm (f2 x)"

   556         using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto

   557       with ge show ?thesis by (simp_all add: norm_mult mult_ac)

   558     qed

   559   qed

   560   ultimately show ?thesis by (rule bigI)

   561 qed

   562

   563 lemma small_big_mult:

   564   assumes "f1 \<in> l F (g1)" "f2 \<in> L F (g2)"

   565   shows   "(\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"

   566 proof (rule smallI)

   567   fix c1 :: real assume c1: "c1 > 0"

   568   from assms(2) guess c2 by (elim bigE) note c2 = this

   569   with c1 assms(1) have "eventually (\<lambda>x. R (norm (f1 x)) (c1 * inverse c2 * norm (g1 x))) F"

   570     by (auto intro!: smallD)

   571   thus "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * norm (g1 x * g2 x))) F" using c2(2)

   572   proof eventually_elim

   573     case (elim x)

   574     show ?case

   575     proof (cases rule: R_E)

   576       case le

   577       have "norm (f1 x) * norm (f2 x) \<le> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"

   578         using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto

   579       with le c2(1) show ?thesis by (simp add: le norm_mult field_simps)

   580     next

   581       case ge

   582       have "norm (f1 x) * norm (f2 x) \<ge> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"

   583         using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto

   584       with ge c2(1) show ?thesis by (simp add: ge norm_mult field_simps)

   585     qed

   586   qed

   587 qed

   588

   589 lemma big_small_mult:

   590   "f1 \<in> L F (g1) \<Longrightarrow> f2 \<in> l F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"

   591   by (subst (1 2) mult.commute) (rule small_big_mult)

   592

   593 lemma small_mult: "f1 \<in> l F (g1) \<Longrightarrow> f2 \<in> l F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"

   594   by (rule small_big_mult, assumption, rule small_imp_big)

   595

   596 lemmas mult = big_mult small_big_mult big_small_mult small_mult

   597

   598

   599 sublocale big: landau_symbol L L' Lr

   600 proof

   601   have L: "L = bigo \<or> L = bigomega"

   602     by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)

   603   {

   604     fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"

   605     hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)

   606   } note A = this

   607   {

   608     fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"

   609     from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]

   610       show "L F (\<lambda>x. c * f x) = L F f" by (intro equalityI big_subsetI) (simp_all add: field_simps)

   611   }

   612   {

   613     fix c :: 'b and F and f g :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"

   614     from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]

   615       have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)

   616     thus "((\<lambda>x. c * f x) \<in> L F g) = (f \<in> L F g)" by (intro iffI) (erule (1) big_trans)+

   617   }

   618   {

   619     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> L F (g)"

   620     assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"

   621     from A guess c by (elim bigE) note c = this

   622     from c(2) B have "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"

   623       by eventually_elim (rule R_E, insert c(1), simp_all add: field_simps norm_inverse norm_divide)

   624     with c(1) show "(\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))" by (rule bigI)

   625   }

   626   {

   627     fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"

   628     with plus_aux show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" by (blast intro!: big_subsetI)

   629   }

   630   {

   631     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"

   632     show "L F (f) = L F (g)" unfolding L_def

   633       by (subst eventually_subst'[OF A]) (rule refl)

   634   }

   635   {

   636     fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"

   637     show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" unfolding L_def mem_Collect_eq

   638       by (subst (1) eventually_subst'[OF A]) (rule refl)

   639   }

   640   {

   641     fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" thus "L F f \<subseteq> L F g" by (rule big_subsetI)

   642   }

   643   {

   644     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"

   645     with A L show "L F (f) = L F (g)" unfolding bigtheta_def

   646       by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo)

   647     fix h:: "'a \<Rightarrow> 'b"

   648     show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" by (rule disjE[OF L])

   649       (insert A, auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans)

   650   }

   651   {

   652     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g"

   653     thus "(\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" by (intro big_mult) simp

   654   }

   655   {

   656     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" "g \<in> L F h"

   657     thus "f \<in> L F (h)" by (rule big_trans)

   658   }

   659   {

   660     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G

   661     assume "f \<in> L F g" and "filterlim h F G"

   662     thus "(\<lambda>x. f (h x)) \<in> L' G (\<lambda>x. g (h x))" by (auto simp: L_def L'_def filterlim_iff)

   663   }

   664   {

   665     fix f g :: "'a \<Rightarrow> 'b" and F G :: "'a filter"

   666     assume "f \<in> L F g" "f \<in> L G g"

   667     from this [THEN bigE] guess c1 c2 . note c12 = this

   668     define c where "c = (if R c1 c2 then c2 else c1)"

   669     from c12 have c: "R c1 c" "R c2 c" "c > 0" by (auto simp: c_def dest: R_linear)

   670     with c12(2,4) have "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"

   671                      "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) G"

   672       by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+

   673     with c show "f \<in> L (sup F G) g" by (auto simp: L_def eventually_sup)

   674   }

   675   {

   676     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"

   677     assume "(f \<in> L F g)"

   678     thus "((\<lambda>x. f (h x)) \<in> L' (filtercomap h F) (\<lambda>x. g (h x)))"

   679       unfolding L_def L'_def by auto

   680   }

   681 qed (auto simp: L_def Lr_def eventually_filtermap L'_def

   682           intro: filter_leD exI[of _ "1::real"])

   683

   684 sublocale small: landau_symbol l l' lr

   685 proof

   686   {

   687     fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"

   688     hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)

   689   } note A = this

   690   {

   691     fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"

   692     from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]

   693       show "l F (\<lambda>x. c * f x) = l F f"

   694         by (intro equalityI small_subsetI) (simp_all add: field_simps)

   695   }

   696   {

   697     fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"

   698     from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]

   699       have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)

   700     thus "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" by (intro iffI) (erule (1) big_small_trans)+

   701   }

   702   {

   703     fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"

   704     with plus_aux show "l F g \<subseteq> l F (\<lambda>x. f x + g x)" by (blast intro!: small_subsetI)

   705   }

   706   {

   707     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> l F (g)"

   708     assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"

   709     show "(\<lambda>x. inverse (g x)) \<in> l F (\<lambda>x. inverse (f x))"

   710     proof (rule smallI)

   711       fix c :: real assume c: "c > 0"

   712       from B smallD[OF A c]

   713         show "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"

   714         by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide)

   715     qed

   716   }

   717   {

   718     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"

   719     show "l F (f) = l F (g)" unfolding l_def by (subst eventually_subst'[OF A]) (rule refl)

   720   }

   721   {

   722     fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"

   723     show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" unfolding l_def mem_Collect_eq

   724       by (subst (1) eventually_subst'[OF A]) (rule refl)

   725   }

   726   {

   727     fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g"

   728     thus "l F f \<subseteq> l F g" by (intro small_subsetI small_imp_big)

   729   }

   730   {

   731     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"

   732     have L: "L = bigo \<or> L = bigomega"

   733       by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)

   734     with A show "l F (f) = l F (g)" unfolding bigtheta_def

   735       by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo)

   736     have l: "l = smallo \<or> l = smallomega"

   737       by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff)

   738     fix h:: "'a \<Rightarrow> 'b"

   739     show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" by (rule disjE[OF l])

   740       (insert A, auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo

   741        intro: landau_o.big_small_trans landau_o.small_big_trans)

   742   }

   743   {

   744     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g"

   745     thus "(\<lambda>x. h x * f x) \<in> l F (\<lambda>x. h x * g x)" by (intro big_small_mult) simp

   746   }

   747   {

   748     fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" "g \<in> l F h"

   749     thus "f \<in> l F (h)" by (rule small_trans)

   750   }

   751   {

   752     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G

   753     assume "f \<in> l F g" and "filterlim h F G"

   754     thus "(\<lambda>x. f (h x)) \<in> l' G (\<lambda>x. g (h x))"

   755       by (auto simp: l_def l'_def filterlim_iff)

   756   }

   757   {

   758     fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"

   759     assume "(f \<in> l F g)"

   760     thus "((\<lambda>x. f (h x)) \<in> l' (filtercomap h F) (\<lambda>x. g (h x)))"

   761       unfolding l_def l'_def by auto

   762   }

   763 qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)

   764

   765

   766 text \<open>These rules allow chaining of Landau symbol propositions in Isar with "also".\<close>

   767

   768 lemma big_mult_1:    "f \<in> L F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"

   769   and big_mult_1':   "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"

   770   and small_mult_1:  "f \<in> l F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"

   771   and small_mult_1': "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> l F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"

   772   and small_mult_1'':  "f \<in> L F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> l F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"

   773   and small_mult_1''': "(\<lambda>_. 1) \<in> l F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"

   774   by (drule (1) big.mult big_small_mult small_big_mult, simp)+

   775

   776 lemma big_1_mult:    "f \<in> L F (g) \<Longrightarrow> h \<in> L F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"

   777   and big_1_mult':   "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"

   778   and small_1_mult:  "f \<in> l F (g) \<Longrightarrow> h \<in> L F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"

   779   and small_1_mult': "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> l F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"

   780   and small_1_mult'':  "f \<in> L F (g) \<Longrightarrow> h \<in> l F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"

   781   and small_1_mult''': "h \<in> l F (\<lambda>_. 1) \<Longrightarrow> f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"

   782   by (drule (1) big.mult big_small_mult small_big_mult, simp)+

   783

   784 lemmas mult_1_trans =

   785   big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1'''

   786   big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult'''

   787

   788 lemma big_equal_iff_bigtheta: "L F (f) = L F (g) \<longleftrightarrow> f \<in> \<Theta>[F](g)"

   789 proof

   790   have L: "L = bigo \<or> L = bigomega"

   791     by (rule R_E) (auto simp: fun_eq_iff L_def bigo_def bigomega_def)

   792   fix f g :: "'a \<Rightarrow> 'b" assume "L F (f) = L F (g)"

   793   with big_refl[of f F] big_refl[of g F] have "f \<in> L F (g)" "g \<in> L F (f)" by simp_all

   794   thus "f \<in> \<Theta>[F](g)" using L unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)

   795 qed (rule big.cong_bigtheta)

   796

   797 lemma big_prod:

   798   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (g x)"

   799   shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>y. \<Prod>x\<in>A. g x y)"

   800   using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult)

   801

   802 lemma big_prod_in_1:

   803   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (\<lambda>_. 1)"

   804   shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>_. 1)"

   805   using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult_in_1)

   806

   807 end

   808

   809

   810 context landau_symbol

   811 begin

   812

   813 lemma plus_absorb1:

   814   assumes "f \<in> o[F](g)"

   815   shows   "L F (\<lambda>x. f x + g x) = L F (g)"

   816 proof (intro equalityI)

   817   from plus_subset1 and assms show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" .

   818   from landau_o.small.plus_subset1[OF assms] and assms have "(\<lambda>x. -f x) \<in> o[F](\<lambda>x. f x + g x)"

   819     by (auto simp: landau_o.small.uminus_in_iff)

   820   from plus_subset1[OF this] show "L F (\<lambda>x. f x + g x) \<subseteq> L F (g)" by simp

   821 qed

   822

   823 lemma plus_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x + g x) = L F (f)"

   824   using plus_absorb1[of g F f] by (simp add: add.commute)

   825

   826 lemma diff_absorb1: "f \<in> o[F](g) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (g)"

   827   by (simp only: diff_conv_add_uminus plus_absorb1 landau_o.small.uminus uminus)

   828

   829 lemma diff_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (f)"

   830   by (simp only: diff_conv_add_uminus plus_absorb2 landau_o.small.uminus_in_iff)

   831

   832 lemmas absorb = plus_absorb1 plus_absorb2 diff_absorb1 diff_absorb2

   833

   834 end

   835

   836

   837 lemma bigthetaI [intro]: "f \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> \<Theta>[F](g)"

   838   unfolding bigtheta_def bigomega_def by blast

   839

   840 lemma bigthetaD1 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> O[F](g)"

   841   and bigthetaD2 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g)"

   842   unfolding bigtheta_def bigo_def bigomega_def by blast+

   843

   844 lemma bigtheta_refl [simp]: "f \<in> \<Theta>[F](f)"

   845   unfolding bigtheta_def by simp

   846

   847 lemma bigtheta_sym: "f \<in> \<Theta>[F](g) \<longleftrightarrow> g \<in> \<Theta>[F](f)"

   848   unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)

   849

   850 lemmas landau_flip =

   851   bigomega_iff_bigo[symmetric] smallomega_iff_smallo[symmetric]

   852   bigomega_iff_bigo smallomega_iff_smallo bigtheta_sym

   853

   854

   855 interpretation landau_theta: landau_symbol bigtheta bigtheta bigtheta

   856 proof

   857   fix f g :: "'a \<Rightarrow> 'b" and F

   858   assume "f \<in> o[F](g)"

   859   hence "O[F](g) \<subseteq> O[F](\<lambda>x. f x + g x)" "\<Omega>[F](g) \<subseteq> \<Omega>[F](\<lambda>x. f x + g x)"

   860     by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+

   861   thus "\<Theta>[F](g) \<subseteq> \<Theta>[F](\<lambda>x. f x + g x)" unfolding bigtheta_def by blast

   862 next

   863   fix f g :: "'a \<Rightarrow> 'b" and F

   864   assume "f \<in> \<Theta>[F](g)"

   865   thus A: "\<Theta>[F](f) = \<Theta>[F](g)"

   866     apply (subst (1 2) bigtheta_def)

   867     apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+

   868     apply (rule refl)

   869     done

   870   thus "\<Theta>[F](f) \<subseteq> \<Theta>[F](g)" by simp

   871   fix h :: "'a \<Rightarrow> 'b"

   872   show "f \<in> \<Theta>[F](h) \<longleftrightarrow> g \<in> \<Theta>[F](h)" by (subst (1 2) bigtheta_sym) (simp add: A)

   873 next

   874   fix f g h :: "'a \<Rightarrow> 'b" and F

   875   assume "f \<in> \<Theta>[F](g)" "g \<in> \<Theta>[F](h)"

   876   thus "f \<in> \<Theta>[F](h)" unfolding bigtheta_def

   877     by (blast intro: landau_o.big.trans landau_omega.big.trans)

   878 next

   879   fix f :: "'a \<Rightarrow> 'b" and F1 F2 :: "'a filter"

   880   assume "F1 \<le> F2"

   881   thus "\<Theta>[F2](f) \<subseteq> \<Theta>[F1](f)"

   882     by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono)

   883 qed (auto simp: bigtheta_def landau_o.big.norm_iff

   884                 landau_o.big.cmult landau_omega.big.cmult

   885                 landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff

   886                 landau_o.big.in_cong landau_omega.big.in_cong

   887                 landau_o.big.mult landau_omega.big.mult

   888                 landau_o.big.inverse landau_omega.big.inverse

   889                 landau_o.big.compose landau_omega.big.compose

   890                 landau_o.big.bot' landau_omega.big.bot'

   891                 landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff

   892                 landau_o.big.sup landau_omega.big.sup

   893                 landau_o.big.filtercomap landau_omega.big.filtercomap

   894           dest: landau_o.big.cong landau_omega.big.cong)

   895

   896 lemmas landau_symbols =

   897   landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms

   898   landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms

   899   landau_theta.landau_symbol_axioms

   900

   901 lemma bigoI [intro]:

   902   assumes "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"

   903   shows   "f \<in> O[F](g)"

   904 proof (rule landau_o.bigI)

   905   show "max 1 c > 0" by simp

   906   note assms

   907   moreover have "\<And>x. c * (norm (g x)) \<le> max 1 c * (norm (g x))" by (simp add: mult_right_mono)

   908   ultimately show "eventually (\<lambda>x. (norm (f x)) \<le> max 1 c * (norm (g x))) F"

   909     by (auto elim!: eventually_mono dest: order.trans)

   910 qed

   911

   912 lemma smallomegaD [dest]:

   913   assumes "f \<in> \<omega>[F](g)"

   914   shows   "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"

   915 proof (cases "c > 0")

   916   case False

   917   show ?thesis

   918     by (intro always_eventually allI, rule order.trans[of _ 0])

   919        (insert False, auto intro!: mult_nonpos_nonneg)

   920 qed (blast dest: landau_omega.smallD[OF assms, of c])

   921

   922

   923 lemma bigthetaI':

   924   assumes "c1 > 0" "c2 > 0"

   925   assumes "eventually (\<lambda>x. c1 * (norm (g x)) \<le> (norm (f x)) \<and> (norm (f x)) \<le> c2 * (norm (g x))) F"

   926   shows   "f \<in> \<Theta>[F](g)"

   927 apply (rule bigthetaI)

   928 apply (rule landau_o.bigI[OF assms(2)]) using assms(3) apply (eventually_elim, simp)

   929 apply (rule landau_omega.bigI[OF assms(1)]) using assms(3) apply (eventually_elim, simp)

   930 done

   931

   932 lemma bigthetaI_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> \<Theta>[F](g)"

   933   by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono)

   934

   935 lemma (in landau_symbol) ev_eq_trans1:

   936   "f \<in> L F (\<lambda>x. g x (h x)) \<Longrightarrow> eventually (\<lambda>x. h x = h' x) F \<Longrightarrow> f \<in> L F (\<lambda>x. g x (h' x))"

   937   by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono)

   938

   939 lemma (in landau_symbol) ev_eq_trans2:

   940   "eventually (\<lambda>x. f x = f' x) F \<Longrightarrow> (\<lambda>x. g x (f' x)) \<in> L F (h) \<Longrightarrow> (\<lambda>x. g x (f x)) \<in> L F (h)"

   941   by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono)

   942

   943 declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro]

   944 declare landau_o.bigE landau_omega.bigE [elim]

   945 declare landau_o.smallD

   946

   947 lemma (in landau_symbol) bigtheta_trans1':

   948   "f \<in> L F (g) \<Longrightarrow> h \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h)"

   949   by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym)

   950

   951 lemma (in landau_symbol) bigtheta_trans2':

   952   "g \<in> \<Theta>[F](f) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"

   953   by (rule bigtheta_trans2, subst bigtheta_sym)

   954

   955 lemma bigo_bigomega_trans:      "f \<in> O[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> O[F](h)"

   956   and bigo_smallomega_trans:    "f \<in> O[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"

   957   and smallo_bigomega_trans:    "f \<in> o[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"

   958   and smallo_smallomega_trans:  "f \<in> o[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"

   959   and bigomega_bigo_trans:      "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](h)"

   960   and bigomega_smallo_trans:    "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"

   961   and smallomega_bigo_trans:    "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"

   962   and smallomega_smallo_trans:  "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"

   963   by (unfold bigomega_iff_bigo smallomega_iff_smallo)

   964      (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans

   965                 landau_o.big_trans landau_o.small_trans)+

   966

   967 lemmas landau_trans_lift [trans] =

   968   landau_symbols[THEN landau_symbol.lift_trans]

   969   landau_symbols[THEN landau_symbol.lift_trans']

   970   landau_symbols[THEN landau_symbol.lift_trans_bigtheta]

   971   landau_symbols[THEN landau_symbol.lift_trans_bigtheta']

   972

   973 lemmas landau_mult_1_trans [trans] =

   974   landau_o.mult_1_trans landau_omega.mult_1_trans

   975

   976 lemmas landau_trans [trans] =

   977   landau_symbols[THEN landau_symbol.bigtheta_trans1]

   978   landau_symbols[THEN landau_symbol.bigtheta_trans2]

   979   landau_symbols[THEN landau_symbol.bigtheta_trans1']

   980   landau_symbols[THEN landau_symbol.bigtheta_trans2']

   981   landau_symbols[THEN landau_symbol.ev_eq_trans1]

   982   landau_symbols[THEN landau_symbol.ev_eq_trans2]

   983

   984   landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans

   985   landau_omega.big_trans landau_omega.small_trans

   986     landau_omega.small_big_trans landau_omega.big_small_trans

   987

   988   bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans

   989   bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans

   990

   991 lemma bigtheta_inverse [simp]:

   992   shows "(\<lambda>x. inverse (f x)) \<in> \<Theta>[F](\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<in> \<Theta>[F](g)"

   993 proof-

   994   {

   995     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"

   996     then guess c1 c2 :: real unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)

   997     note c = this

   998     from c(3) have "inverse c2 > 0" by simp

   999     moreover from c(2,4)

  1000       have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))) F"

  1001     proof eventually_elim

  1002       fix x assume A: "(norm (f x)) \<le> c1 * (norm (g x))" "c2 * (norm (g x)) \<le> (norm (f x))"

  1003       from A c(1,3) have "f x = 0 \<longleftrightarrow> g x = 0" by (auto simp: field_simps mult_le_0_iff)

  1004       with A c(1,3) show "norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))"

  1005         by (force simp: field_simps norm_inverse norm_divide)

  1006     qed

  1007     ultimately have "(\<lambda>x. inverse (f x)) \<in> O[F](\<lambda>x. inverse (g x))" by (rule landau_o.bigI)

  1008   }

  1009   thus ?thesis unfolding bigtheta_def

  1010     by (force simp: bigomega_iff_bigo bigtheta_sym)

  1011 qed

  1012

  1013 lemma bigtheta_divide:

  1014   assumes "f1 \<in> \<Theta>(f2)" "g1 \<in> \<Theta>(g2)"

  1015   shows   "(\<lambda>x. f1 x / g1 x) \<in> \<Theta>(\<lambda>x. f2 x / g2 x)"

  1016   by (subst (1 2) divide_inverse, intro landau_theta.mult) (simp_all add: bigtheta_inverse assms)

  1017

  1018 lemma eventually_nonzero_bigtheta:

  1019   assumes "f \<in> \<Theta>[F](g)"

  1020   shows   "eventually (\<lambda>x. f x \<noteq> 0) F \<longleftrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F"

  1021 proof-

  1022   {

  1023     fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)" and B: "eventually (\<lambda>x. f x \<noteq> 0) F"

  1024     from A guess c1 c2 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)

  1025     from B this(2,4) have "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim auto

  1026   }

  1027   with assms show ?thesis by (force simp: bigtheta_sym)

  1028 qed

  1029

  1030

  1031 subsection \<open>Landau symbols and limits\<close>

  1032

  1033 lemma bigoI_tendsto_norm:

  1034   fixes f g

  1035   assumes "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"

  1036   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"

  1037   shows   "f \<in> O[F](g)"

  1038 proof (rule bigoI)

  1039   from assms have "eventually (\<lambda>x. dist (norm (f x / g x)) c < 1) F"

  1040     using tendstoD by force

  1041   thus "eventually (\<lambda>x. (norm (f x)) \<le> (norm c + 1) * (norm (g x))) F"

  1042     unfolding dist_real_def using assms(2)

  1043   proof eventually_elim

  1044     case (elim x)

  1045     have "(norm (f x)) - norm c * (norm (g x)) \<le> norm ((norm (f x)) - c * (norm (g x)))"

  1046       unfolding norm_mult [symmetric] using norm_triangle_ineq2[of "norm (f x)" "c * norm (g x)"]

  1047       by (simp add: norm_mult abs_mult)

  1048     also from elim have "\<dots> = norm (norm (g x)) * norm (norm (f x / g x) - c)"

  1049       unfolding norm_mult [symmetric] by (simp add: algebra_simps norm_divide)

  1050     also from elim have "norm (norm (f x / g x) - c) \<le> 1" by simp

  1051     hence "norm (norm (g x)) * norm (norm (f x / g x) - c) \<le> norm (norm (g x)) * 1"

  1052       by (rule mult_left_mono) simp_all

  1053     finally show ?case by (simp add: algebra_simps)

  1054   qed

  1055 qed

  1056

  1057 lemma bigoI_tendsto:

  1058   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"

  1059   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"

  1060   shows   "f \<in> O[F](g)"

  1061   using assms by (rule bigoI_tendsto_norm[OF tendsto_norm])

  1062

  1063 lemma bigomegaI_tendsto_norm:

  1064   assumes c_not_0:  "(c::real) \<noteq> 0"

  1065   assumes lim:      "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"

  1066   shows   "f \<in> \<Omega>[F](g)"

  1067 proof (cases "F = bot")

  1068   case False

  1069   show ?thesis

  1070   proof (rule landau_omega.bigI)

  1071     from lim  have "c \<ge> 0" by (rule tendsto_lowerbound) (insert False, simp_all)

  1072     with c_not_0 have "c > 0" by simp

  1073     with c_not_0 show "c/2 > 0" by simp

  1074     from lim have ev: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<epsilon>) F"

  1075       by (subst (asm) tendsto_iff) (simp add: dist_real_def)

  1076     from ev[OF \<open>c/2 > 0\<close>] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"

  1077     proof (eventually_elim)

  1078       fix x assume B: "norm (norm (f x / g x) - c) < c / 2"

  1079       from B have g: "g x \<noteq> 0" by auto

  1080       from B have "-c/2 < -norm (norm (f x / g x) - c)" by simp

  1081       also have "... \<le> norm (f x / g x) - c" by simp

  1082       finally show "(norm (f x)) \<ge> c/2 * (norm (g x))" using g

  1083         by (simp add: field_simps norm_mult norm_divide)

  1084     qed

  1085   qed

  1086 qed simp

  1087

  1088 lemma bigomegaI_tendsto:

  1089   assumes c_not_0:  "(c::real) \<noteq> 0"

  1090   assumes lim:      "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"

  1091   shows   "f \<in> \<Omega>[F](g)"

  1092   by (rule bigomegaI_tendsto_norm[OF _ tendsto_norm, of c]) (insert assms, simp_all)

  1093

  1094 lemma smallomegaI_filterlim_at_top_norm:

  1095   assumes lim: "filterlim (\<lambda>x. norm (f x / g x)) at_top F"

  1096   shows   "f \<in> \<omega>[F](g)"

  1097 proof (rule landau_omega.smallI)

  1098   fix c :: real assume c_pos: "c > 0"

  1099   from lim have ev: "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F"

  1100     by (subst (asm) filterlim_at_top) simp

  1101   thus "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"

  1102   proof eventually_elim

  1103     fix x assume A: "norm (f x / g x) \<ge> c"

  1104     from A c_pos have "g x \<noteq> 0" by auto

  1105     with A show "(norm (f x)) \<ge> c * (norm (g x))" by (simp add: field_simps norm_divide)

  1106   qed

  1107 qed

  1108

  1109 lemma smallomegaI_filterlim_at_infinity:

  1110   assumes lim: "filterlim (\<lambda>x. f x / g x) at_infinity F"

  1111   shows   "f \<in> \<omega>[F](g)"

  1112 proof (rule smallomegaI_filterlim_at_top_norm)

  1113   from lim show "filterlim (\<lambda>x. norm (f x / g x)) at_top F"

  1114     by (rule filterlim_at_infinity_imp_norm_at_top)

  1115 qed

  1116

  1117 lemma smallomegaD_filterlim_at_top_norm:

  1118   assumes "f \<in> \<omega>[F](g)"

  1119   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"

  1120   shows   "LIM x F. norm (f x / g x) :> at_top"

  1121 proof (subst filterlim_at_top_gt, clarify)

  1122   fix c :: real assume c: "c > 0"

  1123   from landau_omega.smallD[OF assms(1) this] assms(2)

  1124     show "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F"

  1125     by eventually_elim (simp add: field_simps norm_divide)

  1126 qed

  1127

  1128 lemma smallomegaD_filterlim_at_infinity:

  1129   assumes "f \<in> \<omega>[F](g)"

  1130   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"

  1131   shows   "LIM x F. f x / g x :> at_infinity"

  1132   using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm)

  1133

  1134 lemma smallomega_1_conv_filterlim: "f \<in> \<omega>[F](\<lambda>_. 1) \<longleftrightarrow> filterlim f at_infinity F"

  1135   by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)

  1136

  1137 lemma smalloI_tendsto:

  1138   assumes lim: "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"

  1139   assumes "eventually (\<lambda>x. g x \<noteq> 0) F"

  1140   shows   "f \<in> o[F](g)"

  1141 proof (rule landau_o.smallI)

  1142   fix c :: real assume c_pos: "c > 0"

  1143   from c_pos and lim have ev: "eventually (\<lambda>x. norm (f x / g x) < c) F"

  1144     by (subst (asm) tendsto_iff) (simp add: dist_real_def)

  1145   with assms(2) show "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"

  1146     by eventually_elim (simp add: field_simps norm_divide)

  1147 qed

  1148

  1149 lemma smalloD_tendsto:

  1150   assumes "f \<in> o[F](g)"

  1151   shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"

  1152 unfolding tendsto_iff

  1153 proof clarify

  1154   fix e :: real assume e: "e > 0"

  1155   hence "e/2 > 0" by simp

  1156   from landau_o.smallD[OF assms this] show "eventually (\<lambda>x. dist (f x / g x) 0 < e) F"

  1157   proof eventually_elim

  1158     fix x assume "(norm (f x)) \<le> e/2 * (norm (g x))"

  1159     with e have "dist (f x / g x) 0 \<le> e/2"

  1160       by (cases "g x = 0") (simp_all add: dist_real_def norm_divide field_simps)

  1161     also from e have "... < e" by simp

  1162     finally show "dist (f x / g x) 0 < e" by simp

  1163   qed

  1164 qed

  1165

  1166 lemma bigthetaI_tendsto_norm:

  1167   assumes c_not_0: "(c::real) \<noteq> 0"

  1168   assumes lim:     "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"

  1169   shows   "f \<in> \<Theta>[F](g)"

  1170 proof (rule bigthetaI)

  1171   from c_not_0 have "\<bar>c\<bar> > 0" by simp

  1172   with lim have "eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<bar>c\<bar>) F"

  1173     by (subst (asm) tendsto_iff) (simp add: dist_real_def)

  1174   hence g: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim (auto simp add: field_simps)

  1175

  1176   from lim g show "f \<in> O[F](g)" by (rule bigoI_tendsto_norm)

  1177   from c_not_0 and lim show "f \<in> \<Omega>[F](g)" by (rule bigomegaI_tendsto_norm)

  1178 qed

  1179

  1180 lemma bigthetaI_tendsto:

  1181   assumes c_not_0: "(c::real) \<noteq> 0"

  1182   assumes lim:     "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"

  1183   shows   "f \<in> \<Theta>[F](g)"

  1184   using assms by (intro bigthetaI_tendsto_norm[OF _ tendsto_norm, of "c"]) simp_all

  1185

  1186 lemma tendsto_add_smallo:

  1187   assumes "(f1 \<longlongrightarrow> a) F"

  1188   assumes "f2 \<in> o[F](f1)"

  1189   shows   "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"

  1190 proof (subst filterlim_cong[OF refl refl])

  1191   from landau_o.smallD[OF assms(2) zero_less_one]

  1192     have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)) F" by simp

  1193   thus "eventually (\<lambda>x. f1 x + f2 x = f1 x * (1 + f2 x / f1 x)) F"

  1194     by eventually_elim (auto simp: field_simps)

  1195 next

  1196   from assms(1) show "((\<lambda>x. f1 x * (1 + f2 x / f1 x)) \<longlongrightarrow> a) F"

  1197     by (force intro: tendsto_eq_intros smalloD_tendsto[OF assms(2)])

  1198 qed

  1199

  1200 lemma tendsto_diff_smallo:

  1201   shows "(f1 \<longlongrightarrow> a) F \<Longrightarrow> f2 \<in> o[F](f1) \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"

  1202   using tendsto_add_smallo[of f1 a F "\<lambda>x. -f2 x"] by simp

  1203

  1204 lemma tendsto_add_smallo_iff:

  1205   assumes "f2 \<in> o[F](f1)"

  1206   shows   "(f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"

  1207 proof

  1208   assume "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"

  1209   hence "((\<lambda>x. f1 x + f2 x - f2 x) \<longlongrightarrow> a) F"

  1210     by (rule tendsto_diff_smallo) (simp add: landau_o.small.plus_absorb2 assms)

  1211   thus "(f1 \<longlongrightarrow> a) F" by simp

  1212 qed (rule tendsto_add_smallo[OF _ assms])

  1213

  1214 lemma tendsto_diff_smallo_iff:

  1215   shows "f2 \<in> o[F](f1) \<Longrightarrow> (f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"

  1216   using tendsto_add_smallo_iff[of "\<lambda>x. -f2 x" F f1 a] by simp

  1217

  1218 lemma tendsto_divide_smallo:

  1219   assumes "((\<lambda>x. f1 x / g1 x) \<longlongrightarrow> a) F"

  1220   assumes "f2 \<in> o[F](f1)" "g2 \<in> o[F](g1)"

  1221   assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"

  1222   shows   "((\<lambda>x. (f1 x + f2 x) / (g1 x + g2 x)) \<longlongrightarrow> a) F" (is "(?f \<longlongrightarrow> _) _")

  1223 proof (subst tendsto_cong)

  1224   let ?f' = "\<lambda>x. (f1 x / g1 x) * (1 + f2 x / f1 x) / (1 + g2 x / g1 x)"

  1225

  1226   have "(?f' \<longlongrightarrow> a * (1 + 0) / (1 + 0)) F"

  1227   by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const

  1228         smalloD_tendsto[OF assms(2)] smalloD_tendsto[OF assms(3)])+ simp_all

  1229   thus "(?f' \<longlongrightarrow> a) F" by simp

  1230

  1231   have "(1/2::real) > 0" by simp

  1232   from landau_o.smallD[OF assms(2) this] landau_o.smallD[OF assms(3) this]

  1233     have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)/2) F"

  1234          "eventually (\<lambda>x. norm (g2 x) \<le> norm (g1 x)/2) F" by simp_all

  1235   with assms(4) show "eventually (\<lambda>x. ?f x = ?f' x) F"

  1236   proof eventually_elim

  1237     fix x assume A: "norm (f2 x) \<le> norm (f1 x)/2" and

  1238                  B: "norm (g2 x) \<le> norm (g1 x)/2" and C: "g1 x \<noteq> 0"

  1239     show "?f x = ?f' x"

  1240     proof (cases "f1 x = 0")

  1241       assume D: "f1 x \<noteq> 0"

  1242       from D have "f1 x + f2 x = f1 x * (1 + f2 x/f1 x)" by (simp add: field_simps)

  1243       moreover from C have "g1 x + g2 x = g1 x * (1 + g2 x/g1 x)" by (simp add: field_simps)

  1244       ultimately have "?f x = (f1 x * (1 + f2 x/f1 x)) / (g1 x * (1 + g2 x/g1 x))" by (simp only:)

  1245       also have "... = ?f' x" by simp

  1246       finally show ?thesis .

  1247     qed (insert A, simp)

  1248   qed

  1249 qed

  1250

  1251

  1252 lemma bigo_powr:

  1253   fixes f :: "'a \<Rightarrow> real"

  1254   assumes "f \<in> O[F](g)" "p \<ge> 0"

  1255   shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)"

  1256 proof-

  1257   from assms(1) guess c by (elim landau_o.bigE landau_omega.bigE IntE)

  1258   note c = this

  1259   from c(2) assms(2) have "eventually (\<lambda>x. (norm (f x)) powr p \<le> (c * (norm (g x))) powr p) F"

  1260     by (auto elim!: eventually_mono intro!: powr_mono2)

  1261   thus "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" using c(1)

  1262     by (intro bigoI[of _ "c powr p"]) (simp_all add: powr_mult)

  1263 qed

  1264

  1265 lemma smallo_powr:

  1266   fixes f :: "'a \<Rightarrow> real"

  1267   assumes "f \<in> o[F](g)" "p > 0"

  1268   shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)"

  1269 proof (rule landau_o.smallI)

  1270   fix c :: real assume c: "c > 0"

  1271   hence "c powr (1/p) > 0" by simp

  1272   from landau_o.smallD[OF assms(1) this]

  1273   show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F"

  1274   proof eventually_elim

  1275     fix x assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))"

  1276     with assms(2) have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p"

  1277       by (intro powr_mono2) simp_all

  1278     also from assms(2) c have "... = c * (norm (g x)) powr p"

  1279       by (simp add: field_simps powr_mult powr_powr)

  1280     finally show "norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)" by simp

  1281   qed

  1282 qed

  1283

  1284 lemma smallo_powr_nonneg:

  1285   fixes f :: "'a \<Rightarrow> real"

  1286   assumes "f \<in> o[F](g)" "p > 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"

  1287   shows   "(\<lambda>x. f x powr p) \<in> o[F](\<lambda>x. g x powr p)"

  1288 proof -

  1289   from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)"

  1290     by (intro bigthetaI_cong) (auto elim!: eventually_mono)

  1291   also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro smallo_powr) fact+

  1292   also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"

  1293     by (intro bigthetaI_cong) (auto elim!: eventually_mono)

  1294   finally show ?thesis .

  1295 qed

  1296

  1297 lemma bigtheta_powr:

  1298   fixes f :: "'a \<Rightarrow> real"

  1299   shows "f \<in> \<Theta>[F](g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>g x\<bar> powr p)"

  1300 apply (cases "p < 0")

  1301 apply (subst bigtheta_inverse[symmetric], subst (1 2) powr_minus[symmetric])

  1302 unfolding bigtheta_def apply (auto simp: bigomega_iff_bigo intro!: bigo_powr)

  1303 done

  1304

  1305 lemma bigo_powr_nonneg:

  1306   fixes f :: "'a \<Rightarrow> real"

  1307   assumes "f \<in> O[F](g)" "p \<ge> 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"

  1308   shows   "(\<lambda>x. f x powr p) \<in> O[F](\<lambda>x. g x powr p)"

  1309 proof -

  1310   from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)"

  1311     by (intro bigthetaI_cong) (auto elim!: eventually_mono)

  1312   also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro bigo_powr) fact+

  1313   also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"

  1314     by (intro bigthetaI_cong) (auto elim!: eventually_mono)

  1315   finally show ?thesis .

  1316 qed

  1317

  1318 lemma zero_in_smallo [simp]: "(\<lambda>_. 0) \<in> o[F](f)"

  1319   by (intro landau_o.smallI) simp_all

  1320

  1321 lemma zero_in_bigo [simp]: "(\<lambda>_. 0) \<in> O[F](f)"

  1322   by (intro landau_o.bigI[of 1]) simp_all

  1323

  1324 lemma in_bigomega_zero [simp]: "f \<in> \<Omega>[F](\<lambda>x. 0)"

  1325   by (rule landau_omega.bigI[of 1]) simp_all

  1326

  1327 lemma in_smallomega_zero [simp]: "f \<in> \<omega>[F](\<lambda>x. 0)"

  1328   by (simp add: smallomega_iff_smallo)

  1329

  1330

  1331 lemma in_smallo_zero_iff [simp]: "f \<in> o[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

  1332 proof

  1333   assume "f \<in> o[F](\<lambda>_. 0)"

  1334   from landau_o.smallD[OF this, of 1] show "eventually (\<lambda>x. f x = 0) F" by simp

  1335 next

  1336   assume "eventually (\<lambda>x. f x = 0) F"

  1337   hence "\<forall>c>0. eventually (\<lambda>x. (norm (f x)) \<le> c * \<bar>0\<bar>) F" by simp

  1338   thus "f \<in> o[F](\<lambda>_. 0)" unfolding smallo_def by simp

  1339 qed

  1340

  1341 lemma in_bigo_zero_iff [simp]: "f \<in> O[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

  1342 proof

  1343   assume "f \<in> O[F](\<lambda>_. 0)"

  1344   thus "eventually (\<lambda>x. f x = 0) F" by (elim landau_o.bigE) simp

  1345 next

  1346   assume "eventually (\<lambda>x. f x = 0) F"

  1347   hence "eventually (\<lambda>x. (norm (f x)) \<le> 1 * \<bar>0\<bar>) F" by simp

  1348   thus "f \<in> O[F](\<lambda>_. 0)" by (intro landau_o.bigI[of 1]) simp_all

  1349 qed

  1350

  1351 lemma zero_in_smallomega_iff [simp]: "(\<lambda>_. 0) \<in> \<omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

  1352   by (simp add: smallomega_iff_smallo)

  1353

  1354 lemma zero_in_bigomega_iff [simp]: "(\<lambda>_. 0) \<in> \<Omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

  1355   by (simp add: bigomega_iff_bigo)

  1356

  1357 lemma zero_in_bigtheta_iff [simp]: "(\<lambda>_. 0) \<in> \<Theta>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

  1358   unfolding bigtheta_def by simp

  1359

  1360 lemma in_bigtheta_zero_iff [simp]: "f \<in> \<Theta>[F](\<lambda>x. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

  1361   unfolding bigtheta_def by simp

  1362

  1363

  1364 lemma cmult_in_bigo_iff    [simp]:  "(\<lambda>x. c * f x) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"

  1365   and cmult_in_bigo_iff'   [simp]:  "(\<lambda>x. f x * c) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"

  1366   and cmult_in_smallo_iff  [simp]:  "(\<lambda>x. c * f x) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"

  1367   and cmult_in_smallo_iff' [simp]: "(\<lambda>x. f x * c) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"

  1368   by (cases "c = 0", simp, simp)+

  1369

  1370 lemma bigo_const [simp]: "(\<lambda>_. c) \<in> O[F](\<lambda>_. 1)" by (rule bigoI[of _ "norm c"]) simp

  1371

  1372 lemma bigo_const_iff [simp]: "(\<lambda>_. c1) \<in> O[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 = 0 \<or> c2 \<noteq> 0"

  1373   by (cases "c1 = 0"; cases "c2 = 0")

  1374      (auto simp: bigo_def eventually_False intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])

  1375

  1376 lemma bigomega_const_iff [simp]: "(\<lambda>_. c1) \<in> \<Omega>[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 \<noteq> 0 \<or> c2 = 0"

  1377   by (cases "c1 = 0"; cases "c2 = 0")

  1378      (auto simp: bigomega_def eventually_False mult_le_0_iff

  1379            intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])

  1380

  1381 lemma smallo_real_nat_transfer:

  1382   "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))"

  1383   by (rule landau_o.small.compose[OF _ filterlim_real_sequentially])

  1384

  1385 lemma bigo_real_nat_transfer:

  1386   "(f :: real \<Rightarrow> real) \<in> O(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> O(\<lambda>x. g (real x))"

  1387   by (rule landau_o.big.compose[OF _ filterlim_real_sequentially])

  1388

  1389 lemma smallomega_real_nat_transfer:

  1390   "(f :: real \<Rightarrow> real) \<in> \<omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<omega>(\<lambda>x. g (real x))"

  1391   by (rule landau_omega.small.compose[OF _ filterlim_real_sequentially])

  1392

  1393 lemma bigomega_real_nat_transfer:

  1394   "(f :: real \<Rightarrow> real) \<in> \<Omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Omega>(\<lambda>x. g (real x))"

  1395   by (rule landau_omega.big.compose[OF _ filterlim_real_sequentially])

  1396

  1397 lemma bigtheta_real_nat_transfer:

  1398   "(f :: real \<Rightarrow> real) \<in> \<Theta>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Theta>(\<lambda>x. g (real x))"

  1399   unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast

  1400

  1401 lemmas landau_real_nat_transfer [intro] =

  1402   bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer

  1403   smallomega_real_nat_transfer bigtheta_real_nat_transfer

  1404

  1405

  1406 lemma landau_symbol_if_at_top_eq [simp]:

  1407   assumes "landau_symbol L L' Lr"

  1408   shows   "L at_top (\<lambda>x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)"

  1409 apply (rule landau_symbol.cong[OF assms])

  1410 using less_add_one[of a] apply (auto intro: eventually_mono  eventually_ge_at_top[of "a + 1"])

  1411 done

  1412

  1413 lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq]

  1414

  1415

  1416

  1417 lemma sum_in_smallo:

  1418   assumes "f \<in> o[F](h)" "g \<in> o[F](h)"

  1419   shows   "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)"

  1420 proof-

  1421   {

  1422     fix f g assume fg: "f \<in> o[F](h)" "g \<in> o[F](h)"

  1423     have "(\<lambda>x. f x + g x) \<in> o[F](h)"

  1424     proof (rule landau_o.smallI)

  1425       fix c :: real assume "c > 0"

  1426       hence "c/2 > 0" by simp

  1427       from fg[THEN landau_o.smallD[OF _ this]]

  1428       show "eventually (\<lambda>x. norm (f x + g x) \<le> c * (norm (h x))) F"

  1429         by eventually_elim (auto intro: order.trans[OF norm_triangle_ineq])

  1430     qed

  1431   }

  1432   from this[of f g] this[of f "\<lambda>x. -g x"] assms

  1433     show "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" by simp_all

  1434 qed

  1435

  1436 lemma big_sum_in_smallo:

  1437   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> o[F](g)"

  1438   shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> o[F](g)"

  1439   using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_smallo)

  1440

  1441 lemma sum_in_bigo:

  1442   assumes "f \<in> O[F](h)" "g \<in> O[F](h)"

  1443   shows   "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)"

  1444 proof-

  1445   {

  1446     fix f g assume fg: "f \<in> O[F](h)" "g \<in> O[F](h)"

  1447     from fg(1) guess c1 by (elim landau_o.bigE) note c1 = this

  1448     from fg(2) guess c2 by (elim landau_o.bigE) note c2 = this

  1449     from c1(2) c2(2) have "eventually (\<lambda>x. norm (f x + g x) \<le> (c1 + c2) * (norm (h x))) F"

  1450       by eventually_elim (auto simp: algebra_simps intro: order.trans[OF norm_triangle_ineq])

  1451     hence "(\<lambda>x. f x + g x) \<in> O[F](h)" by (rule bigoI)

  1452   }

  1453   from this[of f g] this[of f "\<lambda>x. -g x"] assms

  1454     show "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" by simp_all

  1455 qed

  1456

  1457 lemma big_sum_in_bigo:

  1458   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> O[F](g)"

  1459   shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"

  1460   using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)

  1461

  1462 context landau_symbol

  1463 begin

  1464

  1465 lemma mult_cancel_left:

  1466   assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"

  1467   notes   [trans] = bigtheta_trans1 bigtheta_trans2

  1468   shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f2 \<in> L F (g2)"

  1469 proof

  1470   assume A: "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"

  1471   from assms have nz: "eventually (\<lambda>x. f1 x \<noteq> 0) F" by (simp add: eventually_nonzero_bigtheta)

  1472   hence "f2 \<in> \<Theta>[F](\<lambda>x. f1 x * f2 x / f1 x)"

  1473     by (intro bigthetaI_cong) (auto elim!: eventually_mono)

  1474   also from A assms nz have "(\<lambda>x. f1 x * f2 x / f1 x) \<in> L F (\<lambda>x. g1 x * g2 x / f1 x)"

  1475     by (intro divide_right) simp_all

  1476   also from assms nz have "(\<lambda>x. g1 x * g2 x / f1 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x / g1 x)"

  1477     by (intro landau_theta.mult landau_theta.divide) (simp_all add: bigtheta_sym)

  1478   also from assms have "(\<lambda>x. g1 x * g2 x / g1 x) \<in> \<Theta>[F](g2)"

  1479     by (intro bigthetaI_cong) (auto elim!: eventually_mono)

  1480   finally show "f2 \<in> L F (g2)" .

  1481 next

  1482   assume "f2 \<in> L F (g2)"

  1483   hence "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. f1 x * g2 x)" by (rule mult_left)

  1484   also have "(\<lambda>x. f1 x * g2 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x)"

  1485     by (intro landau_theta.mult_right assms)

  1486   finally show "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" .

  1487 qed

  1488

  1489 lemma mult_cancel_right:

  1490   assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"

  1491   shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"

  1492   by (subst (1 2) mult.commute) (rule mult_cancel_left[OF assms])

  1493

  1494 lemma divide_cancel_right:

  1495   assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"

  1496   shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"

  1497   by (subst (1 2) divide_inverse, intro mult_cancel_right bigtheta_inverse) (simp_all add: assms)

  1498

  1499 lemma divide_cancel_left:

  1500   assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"

  1501   shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow>

  1502              (\<lambda>x. inverse (f2 x)) \<in> L F (\<lambda>x. inverse (g2 x))"

  1503   by (simp only: divide_inverse mult_cancel_left[OF assms])

  1504

  1505 end

  1506

  1507

  1508 lemma powr_smallo_iff:

  1509   assumes "filterlim g at_top F" "F \<noteq> bot"

  1510   shows   "(\<lambda>x. g x powr p :: real) \<in> o[F](\<lambda>x. g x powr q) \<longleftrightarrow> p < q"

  1511 proof-

  1512   from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)

  1513   hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp

  1514   have B: "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p) \<Longrightarrow> (\<lambda>x. g x powr p) \<notin> o[F](\<lambda>x. g x powr q)"

  1515   proof

  1516     assume "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)"

  1517     from landau_o.big_small_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp

  1518     with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp

  1519     thus False by (simp add: eventually_False assms)

  1520   qed

  1521   show ?thesis

  1522   proof (cases p q rule: linorder_cases)

  1523     assume "p < q"

  1524     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A

  1525       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)

  1526     with \<open>p < q\<close> show ?thesis by auto

  1527   next

  1528     assume "p = q"

  1529     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)

  1530     with B \<open>p = q\<close> show ?thesis by auto

  1531   next

  1532     assume "p > q"

  1533     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A

  1534       by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)

  1535     with B \<open>p > q\<close> show ?thesis by auto

  1536   qed

  1537 qed

  1538

  1539 lemma powr_bigo_iff:

  1540   assumes "filterlim g at_top F" "F \<noteq> bot"

  1541   shows   "(\<lambda>x. g x powr p :: real) \<in> O[F](\<lambda>x. g x powr q) \<longleftrightarrow> p \<le> q"

  1542 proof-

  1543   from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)

  1544   hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp

  1545   have B: "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p) \<Longrightarrow> (\<lambda>x. g x powr p) \<notin> O[F](\<lambda>x. g x powr q)"

  1546   proof

  1547     assume "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" "(\<lambda>x. g x powr p) \<in> O[F](\<lambda>x. g x powr q)"

  1548     from landau_o.small_big_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp

  1549     with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp

  1550     thus False by (simp add: eventually_False assms)

  1551   qed

  1552   show ?thesis

  1553   proof (cases p q rule: linorder_cases)

  1554     assume "p < q"

  1555     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A

  1556       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)

  1557     with \<open>p < q\<close> show ?thesis by (auto intro: landau_o.small_imp_big)

  1558   next

  1559     assume "p = q"

  1560     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)

  1561     with B \<open>p = q\<close> show ?thesis by auto

  1562   next

  1563     assume "p > q"

  1564     hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A

  1565       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)

  1566     with B \<open>p > q\<close> show ?thesis by (auto intro: landau_o.small_imp_big)

  1567   qed

  1568 qed

  1569

  1570 lemma powr_bigtheta_iff:

  1571   assumes "filterlim g at_top F" "F \<noteq> bot"

  1572   shows   "(\<lambda>x. g x powr p :: real) \<in> \<Theta>[F](\<lambda>x. g x powr q) \<longleftrightarrow> p = q"

  1573   using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff)

  1574

  1575

  1576 subsection \<open>Flatness of real functions\<close>

  1577

  1578 text \<open>

  1579   Given two real-valued functions $f$ and $g$, we say that $f$ is flatter than $g$ if

  1580   any power of $f(x)$ is asymptotically dominated by any positive power of $g(x)$. This is

  1581   a useful notion since, given two products of powers of functions sorted by flatness, we can

  1582   compare them asymptotically by simply comparing the exponent lists lexicographically.

  1583

  1584   A simple sufficient criterion for flatness it that $\ln f(x) \in o(\ln g(x))$, which we show

  1585   now.

  1586 \<close>

  1587 lemma ln_smallo_imp_flat:

  1588   fixes f g :: "real \<Rightarrow> real"

  1589   assumes lim_f: "filterlim f at_top at_top"

  1590   assumes lim_g: "filterlim g at_top at_top"

  1591   assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"

  1592   assumes q: "q > 0"

  1593   shows   "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)"

  1594 proof (rule smalloI_tendsto)

  1595   from lim_f have "eventually (\<lambda>x. f x > 0) at_top"

  1596     by (simp add: filterlim_at_top_dense)

  1597   hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp

  1598

  1599   from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top"

  1600     by (simp add: filterlim_at_top_dense)

  1601   hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp

  1602   thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top"

  1603     by eventually_elim simp

  1604

  1605   have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) =

  1606                           p * ln (f x) - q * ln (g x)) at_top"

  1607     using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps)

  1608   have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top"

  1609     by (insert q)

  1610        (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult

  1611               tendsto_const tendsto_diff smalloD_tendsto[OF ln_o_ln] lim_g

  1612               filterlim_compose[OF ln_at_top] | simp)+

  1613   hence "filterlim (\<lambda>x. p * ln (f x) - q * ln (g x)) at_bot at_top"

  1614     by (subst (asm) filterlim_cong[OF refl refl eq])

  1615   hence *: "((\<lambda>x. exp (p * ln (f x) - q * ln (g x))) \<longlongrightarrow> 0) at_top"

  1616     by (rule filterlim_compose[OF exp_at_bot])

  1617   have eq: "eventually (\<lambda>x. exp (p * ln (f x) - q * ln (g x)) = f x powr p / g x powr q) at_top"

  1618     using f_nz g_nz by eventually_elim (simp add: powr_def exp_diff)

  1619   show "((\<lambda>x. f x powr p / g x powr q) \<longlongrightarrow> 0) at_top"

  1620     using * by (subst (asm) filterlim_cong[OF refl refl eq])

  1621 qed

  1622

  1623 lemma ln_smallo_imp_flat':

  1624   fixes f g :: "real \<Rightarrow> real"

  1625   assumes lim_f: "filterlim f at_top at_top"

  1626   assumes lim_g: "filterlim g at_top at_top"

  1627   assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"

  1628   assumes q: "q < 0"

  1629   shows   "(\<lambda>x. g x powr q) \<in> o(\<lambda>x. f x powr p)"

  1630 proof -

  1631   from lim_f lim_g have "eventually (\<lambda>x. f x > 0) at_top" "eventually (\<lambda>x. g x > 0) at_top"

  1632     by (simp_all add: filterlim_at_top_dense)

  1633   hence "eventually (\<lambda>x. f x \<noteq> 0) at_top" "eventually (\<lambda>x. g x \<noteq> 0) at_top"

  1634     by (auto elim: eventually_mono)

  1635   moreover from assms have "(\<lambda>x. f x powr -p) \<in> o(\<lambda>x. g x powr -q)"

  1636     by (intro ln_smallo_imp_flat assms) simp_all

  1637   ultimately show ?thesis unfolding powr_minus

  1638     by (simp add: landau_o.small.inverse_cancel)

  1639 qed

  1640

  1641

  1642 subsection \<open>Asymptotic Equivalence\<close>

  1643

  1644 (* TODO Move *)

  1645 lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"

  1646   by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)

  1647

  1648 named_theorems asymp_equiv_intros

  1649 named_theorems asymp_equiv_simps

  1650

  1651 definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"

  1652   (\<open>_ \<sim>[_] _\<close> [51, 10, 51] 50)

  1653   where "f \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"

  1654

  1655 abbreviation (input) asymp_equiv_at_top where

  1656   "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"

  1657

  1658 bundle asymp_equiv_notation

  1659 begin

  1660 notation asymp_equiv_at_top (infix \<open>\<sim>\<close> 50)

  1661 end

  1662

  1663 lemma asymp_equivI: "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F \<Longrightarrow> f \<sim>[F] g"

  1664   by (simp add: asymp_equiv_def)

  1665

  1666 lemma asymp_equivD: "f \<sim>[F] g \<Longrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"

  1667   by (simp add: asymp_equiv_def)

  1668

  1669 lemma asymp_equiv_filtermap_iff:

  1670   "f \<sim>[filtermap h F] g \<longleftrightarrow> (\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"

  1671   by (simp add: asymp_equiv_def filterlim_filtermap)

  1672

  1673 lemma asymp_equiv_refl [simp, asymp_equiv_intros]: "f \<sim>[F] f"

  1674 proof (intro asymp_equivI)

  1675   have "eventually (\<lambda>x. 1 = (if f x = 0 \<and> f x = 0 then 1 else f x / f x)) F"

  1676     by (intro always_eventually) simp

  1677   moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp

  1678   ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"

  1679     by (rule Lim_transform_eventually)

  1680 qed

  1681

  1682 lemma asymp_equiv_symI:

  1683   assumes "f \<sim>[F] g"

  1684   shows   "g \<sim>[F] f"

  1685   using tendsto_inverse[OF asymp_equivD[OF assms]]

  1686   by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong)

  1687

  1688 lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f"

  1689   by (blast intro: asymp_equiv_symI)

  1690

  1691 lemma asymp_equivI':

  1692   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"

  1693   shows   "f \<sim>[F] g"

  1694 proof (cases "F = bot")

  1695   case False

  1696   have "eventually (\<lambda>x. f x \<noteq> 0) F"

  1697   proof (rule ccontr)

  1698     assume "\<not>eventually (\<lambda>x. f x \<noteq> 0) F"

  1699     hence "frequently (\<lambda>x. f x = 0) F" by (simp add: frequently_def)

  1700     hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1)

  1701     from limit_frequently_eq[OF False this assms] show False by simp_all

  1702   qed

  1703   hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"

  1704     by eventually_elim simp

  1705   from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def

  1706     by (rule Lim_transform_eventually)

  1707 qed (simp_all add: asymp_equiv_def)

  1708

  1709

  1710 lemma asymp_equiv_cong:

  1711   assumes "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"

  1712   shows   "f1 \<sim>[F] g1 \<longleftrightarrow> f2 \<sim>[F] g2"

  1713   unfolding asymp_equiv_def

  1714 proof (rule tendsto_cong, goal_cases)

  1715   case 1

  1716   from assms show ?case by eventually_elim simp

  1717 qed

  1718

  1719 lemma asymp_equiv_eventually_zeros:

  1720   fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"

  1721   assumes "f \<sim>[F] g"

  1722   shows   "eventually (\<lambda>x. f x = 0 \<longleftrightarrow> g x = 0) F"

  1723 proof -

  1724   let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  1725   have "eventually (\<lambda>x. x \<noteq> 0) (nhds (1::'b))"

  1726     by (rule t1_space_nhds) auto

  1727   hence "eventually (\<lambda>x. x \<noteq> 0) (filtermap ?h F)"

  1728     using assms unfolding asymp_equiv_def filterlim_def

  1729     by (rule filter_leD [rotated])

  1730   hence "eventually (\<lambda>x. ?h x \<noteq> 0) F" by (simp add: eventually_filtermap)

  1731   thus ?thesis by eventually_elim (auto split: if_splits)

  1732 qed

  1733

  1734 lemma asymp_equiv_transfer:

  1735   assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"

  1736   shows   "f2 \<sim>[F] g2"

  1737   using assms(1) asymp_equiv_cong[OF assms(2,3)] by simp

  1738

  1739 lemma asymp_equiv_transfer_trans [trans]:

  1740   assumes "(\<lambda>x. f x (h1 x)) \<sim>[F] (\<lambda>x. g x (h1 x))"

  1741   assumes "eventually (\<lambda>x. h1 x = h2 x) F"

  1742   shows   "(\<lambda>x. f x (h2 x)) \<sim>[F] (\<lambda>x. g x (h2 x))"

  1743   by (rule asymp_equiv_transfer[OF assms(1)]) (insert assms(2), auto elim!: eventually_mono)

  1744

  1745 lemma asymp_equiv_trans [trans]:

  1746   fixes f g h

  1747   assumes "f \<sim>[F] g" "g \<sim>[F] h"

  1748   shows   "f \<sim>[F] h"

  1749 proof -

  1750   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  1751   from assms[THEN asymp_equiv_eventually_zeros]

  1752     have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp

  1753   moreover from tendsto_mult[OF assms[THEN asymp_equivD]]

  1754     have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp

  1755   ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)

  1756 qed

  1757

  1758 lemma asymp_equiv_trans_lift1 [trans]:

  1759   assumes "a \<sim>[F] f b" "b \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"

  1760   shows   "a \<sim>[F] f c"

  1761   using assms by (blast intro: asymp_equiv_trans)

  1762

  1763 lemma asymp_equiv_trans_lift2 [trans]:

  1764   assumes "f a \<sim>[F] b" "a \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"

  1765   shows   "f c \<sim>[F] b"

  1766   using asymp_equiv_symI[OF assms(3)[OF assms(2)]] assms(1)

  1767   by (blast intro: asymp_equiv_trans)

  1768

  1769 lemma asymp_equivD_const:

  1770   assumes "f \<sim>[F] (\<lambda>_. c)"

  1771   shows   "(f \<longlongrightarrow> c) F"

  1772 proof (cases "c = 0")

  1773   case False

  1774   with tendsto_mult_right[OF asymp_equivD[OF assms], of c] show ?thesis by simp

  1775 next

  1776   case True

  1777   with asymp_equiv_eventually_zeros[OF assms] show ?thesis

  1778     by (simp add: Lim_eventually)

  1779 qed

  1780

  1781 lemma asymp_equiv_refl_ev:

  1782   assumes "eventually (\<lambda>x. f x = g x) F"

  1783   shows   "f \<sim>[F] g"

  1784   by (intro asymp_equivI Lim_eventually)

  1785      (insert assms, auto elim!: eventually_mono)

  1786

  1787 lemma asymp_equiv_sandwich:

  1788   fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"

  1789   assumes "eventually (\<lambda>x. f x \<ge> 0) F"

  1790   assumes "eventually (\<lambda>x. f x \<le> g x) F"

  1791   assumes "eventually (\<lambda>x. g x \<le> h x) F"

  1792   assumes "f \<sim>[F] h"

  1793   shows   "g \<sim>[F] f" "g \<sim>[F] h"

  1794 proof -

  1795   show "g \<sim>[F] f"

  1796   proof (rule asymp_equivI, rule tendsto_sandwich)

  1797     from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]

  1798       show "eventually (\<lambda>n. (if h n = 0 \<and> f n = 0 then 1 else h n / f n) \<ge>

  1799                               (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"

  1800         by eventually_elim (auto intro!: divide_right_mono)

  1801     from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]

  1802       show "eventually (\<lambda>n. 1 \<le>

  1803                               (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"

  1804         by eventually_elim (auto intro!: divide_right_mono)

  1805   qed (insert asymp_equiv_symI[OF assms(4)], simp_all add: asymp_equiv_def)

  1806   also note \<open>f \<sim>[F] h\<close>

  1807   finally show "g \<sim>[F] h" .

  1808 qed

  1809

  1810 lemma asymp_equiv_imp_eventually_same_sign:

  1811   fixes f g :: "real \<Rightarrow> real"

  1812   assumes "f \<sim>[F] g"

  1813   shows   "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"

  1814 proof -

  1815   from assms have "((\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> sgn 1) F"

  1816     unfolding asymp_equiv_def by (rule tendsto_sgn) simp_all

  1817   from order_tendstoD(1)[OF this, of "1/2"]

  1818     have "eventually (\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x) > 1/2) F"

  1819     by simp

  1820   thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"

  1821   proof eventually_elim

  1822     case (elim x)

  1823     thus ?case

  1824       by (cases "f x" "0 :: real" rule: linorder_cases;

  1825           cases "g x" "0 :: real" rule: linorder_cases) simp_all

  1826   qed

  1827 qed

  1828

  1829 lemma

  1830   fixes f g :: "_ \<Rightarrow> real"

  1831   assumes "f \<sim>[F] g"

  1832   shows   asymp_equiv_eventually_same_sign: "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" (is ?th1)

  1833     and   asymp_equiv_eventually_neg_iff:   "eventually (\<lambda>x. f x < 0 \<longleftrightarrow> g x < 0) F" (is ?th2)

  1834     and   asymp_equiv_eventually_pos_iff:   "eventually (\<lambda>x. f x > 0 \<longleftrightarrow> g x > 0) F" (is ?th3)

  1835 proof -

  1836   from assms have "filterlim (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) (nhds 1) F"

  1837     by (rule asymp_equivD)

  1838   from order_tendstoD(1)[OF this zero_less_one]

  1839     show ?th1 ?th2 ?th3

  1840     by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+

  1841 qed

  1842

  1843 lemma asymp_equiv_tendsto_transfer:

  1844   assumes "f \<sim>[F] g" and "(f \<longlongrightarrow> c) F"

  1845   shows   "(g \<longlongrightarrow> c) F"

  1846 proof -

  1847   let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"

  1848   have "eventually (\<lambda>x. ?h x = g x) F"

  1849     using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp

  1850   moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)

  1851   hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"

  1852     by (rule asymp_equivD)

  1853   from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp

  1854   ultimately show ?thesis by (rule Lim_transform_eventually)

  1855 qed

  1856

  1857 lemma tendsto_asymp_equiv_cong:

  1858   assumes "f \<sim>[F] g"

  1859   shows   "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"

  1860 proof -

  1861   {

  1862     fix f g :: "'a \<Rightarrow> 'b"

  1863     assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"

  1864     have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"

  1865       using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp

  1866     moreover have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F"

  1867       by (intro tendsto_intros asymp_equivD *)

  1868     ultimately have "(f \<longlongrightarrow> c * 1) F"

  1869       by (rule Lim_transform_eventually)

  1870   }

  1871   from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym)

  1872 qed

  1873

  1874

  1875 lemma smallo_imp_eventually_sgn:

  1876   fixes f g :: "real \<Rightarrow> real"

  1877   assumes "g \<in> o(f)"

  1878   shows   "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top"

  1879 proof -

  1880   have "0 < (1/2 :: real)" by simp

  1881   from landau_o.smallD[OF assms, OF this]

  1882     have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp

  1883   thus ?thesis

  1884   proof eventually_elim

  1885     case (elim x)

  1886     thus ?case

  1887       by (cases "f x" "0::real" rule: linorder_cases;

  1888           cases "f x + g x" "0::real" rule: linorder_cases) simp_all

  1889   qed

  1890 qed

  1891

  1892 context

  1893 begin

  1894

  1895 private lemma asymp_equiv_add_rightI:

  1896   assumes "f \<sim>[F] g" "h \<in> o[F](g)"

  1897   shows   "(\<lambda>x. f x + h x) \<sim>[F] g"

  1898 proof -

  1899   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  1900   from landau_o.smallD[OF assms(2) zero_less_one]

  1901     have ev: "eventually (\<lambda>x. g x = 0 \<longrightarrow> h x = 0) F" by eventually_elim auto

  1902   have "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1) F"

  1903     unfolding asymp_equiv_def using ev

  1904     by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps)

  1905   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1 + 0) F" by simp

  1906   also have \<dots> by (intro tendsto_intros asymp_equivD assms smalloD_tendsto)

  1907   finally show "(\<lambda>x. f x + h x) \<sim>[F] g" .

  1908 qed

  1909

  1910 lemma asymp_equiv_add_right [asymp_equiv_simps]:

  1911   assumes "h \<in> o[F](g)"

  1912   shows   "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"

  1913 proof

  1914   assume "(\<lambda>x. f x + h x) \<sim>[F] g"

  1915   from asymp_equiv_add_rightI[OF this, of "\<lambda>x. -h x"] assms show "f \<sim>[F] g"

  1916     by simp

  1917 qed (simp_all add: asymp_equiv_add_rightI assms)

  1918

  1919 end

  1920

  1921 lemma asymp_equiv_add_left [asymp_equiv_simps]:

  1922   assumes "h \<in> o[F](g)"

  1923   shows   "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"

  1924   using asymp_equiv_add_right[OF assms] by (simp add: add.commute)

  1925

  1926 lemma asymp_equiv_add_right' [asymp_equiv_simps]:

  1927   assumes "h \<in> o[F](g)"

  1928   shows   "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f"

  1929   using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym)

  1930

  1931 lemma asymp_equiv_add_left' [asymp_equiv_simps]:

  1932   assumes "h \<in> o[F](g)"

  1933   shows   "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f"

  1934   using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym)

  1935

  1936 lemma smallo_imp_asymp_equiv:

  1937   assumes "(\<lambda>x. f x - g x) \<in> o[F](g)"

  1938   shows   "f \<sim>[F] g"

  1939 proof -

  1940   from assms have "(\<lambda>x. f x - g x + g x) \<sim>[F] g"

  1941     by (subst asymp_equiv_add_left) simp_all

  1942   thus ?thesis by simp

  1943 qed

  1944

  1945 lemma asymp_equiv_uminus [asymp_equiv_intros]:

  1946   "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. -f x) \<sim>[F] (\<lambda>x. -g x)"

  1947   by (simp add: asymp_equiv_def cong: if_cong)

  1948

  1949 lemma asymp_equiv_uminus_iff [asymp_equiv_simps]:

  1950   "(\<lambda>x. -f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] (\<lambda>x. -g x)"

  1951   by (simp add: asymp_equiv_def cong: if_cong)

  1952

  1953 lemma asymp_equiv_mult [asymp_equiv_intros]:

  1954   fixes f1 f2 g1 g2 :: "'a \<Rightarrow> 'b :: real_normed_field"

  1955   assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"

  1956   shows   "(\<lambda>x. f1 x * f2 x) \<sim>[F] (\<lambda>x. g1 x * g2 x)"

  1957 proof -

  1958   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  1959   let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x

  1960                    else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)"

  1961   let ?S' = "\<lambda>x. ?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) x - ?T f1 g1 x * ?T f2 g2 x"

  1962   {

  1963     fix f g :: "'a \<Rightarrow> 'b" assume "f \<sim>[F] g"

  1964     have "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F"

  1965       by (rule tendsto_eq_intros refl asymp_equivD[OF \<open>f \<sim>[F] g\<close>])+ simp_all

  1966   } note A = this

  1967

  1968   from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"

  1969     by (intro tendsto_mult asymp_equivD)

  1970   moreover {

  1971     have "eventually (\<lambda>x. ?S x = ?S' x) F"

  1972       using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto

  1973     moreover have "(?S \<longlongrightarrow> 0) F"

  1974       by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])

  1975          (auto intro: le_infI1 le_infI2)

  1976     ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)

  1977   }

  1978   ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"

  1979     by (rule Lim_transform)

  1980   thus ?thesis by (simp add: asymp_equiv_def)

  1981 qed

  1982

  1983 lemma asymp_equiv_power [asymp_equiv_intros]:

  1984   "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)"

  1985   by (induction n) (simp_all add: asymp_equiv_mult)

  1986

  1987 lemma asymp_equiv_inverse [asymp_equiv_intros]:

  1988   assumes "f \<sim>[F] g"

  1989   shows   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"

  1990 proof -

  1991   from tendsto_inverse[OF asymp_equivD[OF assms]]

  1992     have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) \<longlongrightarrow> 1) F"

  1993     by (simp add: if_distrib cong: if_cong)

  1994   also have "(\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) =

  1995                (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else inverse (f x) / inverse (g x))"

  1996     by (intro ext) (simp add: field_simps)

  1997   finally show ?thesis by (simp add: asymp_equiv_def)

  1998 qed

  1999

  2000 lemma asymp_equiv_inverse_iff [asymp_equiv_simps]:

  2001   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<sim>[F] g"

  2002 proof

  2003   assume "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"

  2004   hence "(\<lambda>x. inverse (inverse (f x))) \<sim>[F] (\<lambda>x. inverse (inverse (g x)))" (is ?P)

  2005     by (rule asymp_equiv_inverse)

  2006   also have "?P \<longleftrightarrow> f \<sim>[F] g" by (intro asymp_equiv_cong) simp_all

  2007   finally show "f \<sim>[F] g" .

  2008 qed (simp_all add: asymp_equiv_inverse)

  2009

  2010 lemma asymp_equiv_divide [asymp_equiv_intros]:

  2011   assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"

  2012   shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"

  2013   using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)

  2014

  2015 lemma asymp_equiv_compose [asymp_equiv_intros]:

  2016   assumes "f \<sim>[G] g" "filterlim h G F"

  2017   shows   "f \<circ> h \<sim>[F] g \<circ> h"

  2018 proof -

  2019   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  2020   have "f \<circ> h \<sim>[F] g \<circ> h \<longleftrightarrow> ((?T f g \<circ> h) \<longlongrightarrow> 1) F"

  2021     by (simp add: asymp_equiv_def o_def)

  2022   also have "\<dots> \<longleftrightarrow> (?T f g \<longlongrightarrow> 1) (filtermap h F)"

  2023     by (rule tendsto_compose_filtermap)

  2024   also have "\<dots>"

  2025     by (rule tendsto_mono[of _ G]) (insert assms, simp_all add: asymp_equiv_def filterlim_def)

  2026   finally show ?thesis .

  2027 qed

  2028

  2029 lemma asymp_equiv_compose':

  2030   assumes "f \<sim>[G] g" "filterlim h G F"

  2031   shows   "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"

  2032   using asymp_equiv_compose[OF assms] by (simp add: o_def)

  2033

  2034 lemma asymp_equiv_powr_real [asymp_equiv_intros]:

  2035   fixes f g :: "'a \<Rightarrow> real"

  2036   assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"

  2037   shows   "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"

  2038 proof -

  2039   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  2040   have "eventually (\<lambda>x. ?T f g x powr y = ?T (\<lambda>x. f x powr y) (\<lambda>x. g x powr y) x) F"

  2041     using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)

  2042     by eventually_elim (auto simp: powr_divide)

  2043   moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"

  2044     by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all

  2045   hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp

  2046   ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)

  2047 qed

  2048

  2049 lemma asymp_equiv_norm [asymp_equiv_intros]:

  2050   fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"

  2051   assumes "f \<sim>[F] g"

  2052   shows   "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))"

  2053   using tendsto_norm[OF asymp_equivD[OF assms]]

  2054   by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong)

  2055

  2056 lemma asymp_equiv_abs_real [asymp_equiv_intros]:

  2057   fixes f g :: "'a \<Rightarrow> real"

  2058   assumes "f \<sim>[F] g"

  2059   shows   "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)"

  2060   using tendsto_rabs[OF asymp_equivD[OF assms]]

  2061   by (simp add: if_distrib asymp_equiv_def cong: if_cong)

  2062

  2063 lemma asymp_equiv_imp_eventually_le:

  2064   assumes "f \<sim>[F] g" "c > 1"

  2065   shows   "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"

  2066 proof -

  2067   from order_tendstoD(2)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]

  2068        asymp_equiv_eventually_zeros[OF assms(1)]

  2069     show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)

  2070 qed

  2071

  2072 lemma asymp_equiv_imp_eventually_ge:

  2073   assumes "f \<sim>[F] g" "c < 1"

  2074   shows   "eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F"

  2075 proof -

  2076   from order_tendstoD(1)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]

  2077        asymp_equiv_eventually_zeros[OF assms(1)]

  2078     show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)

  2079 qed

  2080

  2081 lemma asymp_equiv_imp_bigo:

  2082   assumes "f \<sim>[F] g"

  2083   shows   "f \<in> O[F](g)"

  2084 proof (rule bigoI)

  2085   have "(3/2::real) > 1" by simp

  2086   from asymp_equiv_imp_eventually_le[OF assms this]

  2087     show "eventually (\<lambda>x. norm (f x) \<le> 3/2 * norm (g x)) F"

  2088     by eventually_elim simp

  2089 qed

  2090

  2091 lemma asymp_equiv_imp_bigomega:

  2092   "f \<sim>[F] g \<Longrightarrow> f \<in> \<Omega>[F](g)"

  2093   using asymp_equiv_imp_bigo[of g F f] by (simp add: asymp_equiv_sym bigomega_iff_bigo)

  2094

  2095 lemma asymp_equiv_imp_bigtheta:

  2096   "f \<sim>[F] g \<Longrightarrow> f \<in> \<Theta>[F](g)"

  2097   by (intro bigthetaI asymp_equiv_imp_bigo asymp_equiv_imp_bigomega)

  2098

  2099 lemma asymp_equiv_at_infinity_transfer:

  2100   assumes "f \<sim>[F] g" "filterlim f at_infinity F"

  2101   shows   "filterlim g at_infinity F"

  2102 proof -

  2103   from assms(1) have "g \<in> \<Theta>[F](f)" by (rule asymp_equiv_imp_bigtheta[OF asymp_equiv_symI])

  2104   also from assms have "f \<in> \<omega>[F](\<lambda>_. 1)" by (simp add: smallomega_1_conv_filterlim)

  2105   finally show ?thesis by (simp add: smallomega_1_conv_filterlim)

  2106 qed

  2107

  2108 lemma asymp_equiv_at_top_transfer:

  2109   fixes f g :: "_ \<Rightarrow> real"

  2110   assumes "f \<sim>[F] g" "filterlim f at_top F"

  2111   shows   "filterlim g at_top F"

  2112 proof (rule filterlim_at_infinity_imp_filterlim_at_top)

  2113   show "filterlim g at_infinity F"

  2114     by (rule asymp_equiv_at_infinity_transfer[OF assms(1) filterlim_mono[OF assms(2)]])

  2115        (auto simp: at_top_le_at_infinity)

  2116   from assms(2) have "eventually (\<lambda>x. f x > 0) F"

  2117     using filterlim_at_top_dense by blast

  2118   with asymp_equiv_eventually_pos_iff[OF assms(1)] show "eventually (\<lambda>x. g x > 0) F"

  2119     by eventually_elim blast

  2120 qed

  2121

  2122 lemma asymp_equiv_at_bot_transfer:

  2123   fixes f g :: "_ \<Rightarrow> real"

  2124   assumes "f \<sim>[F] g" "filterlim f at_bot F"

  2125   shows   "filterlim g at_bot F"

  2126   unfolding filterlim_uminus_at_bot

  2127   by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"])

  2128      (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus)

  2129

  2130 lemma asymp_equivI'_const:

  2131   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0"

  2132   shows   "f \<sim>[F] (\<lambda>x. c * g x)"

  2133   using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2)

  2134   by (intro asymp_equivI') (simp add: field_simps)

  2135

  2136 lemma asymp_equivI'_inverse_const:

  2137   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> inverse c) F" "c \<noteq> 0"

  2138   shows   "(\<lambda>x. c * f x) \<sim>[F] g"

  2139   using tendsto_mult[OF assms(1) tendsto_const[of "c"]] assms(2)

  2140   by (intro asymp_equivI') (simp add: field_simps)

  2141

  2142 lemma filterlim_at_bot_imp_at_infinity: "filterlim f at_bot F \<Longrightarrow> filterlim f at_infinity F"

  2143   for f :: "_ \<Rightarrow> real" using at_bot_le_at_infinity filterlim_mono by blast

  2144

  2145 lemma asymp_equiv_imp_diff_smallo:

  2146   assumes "f \<sim>[F] g"

  2147   shows   "(\<lambda>x. f x - g x) \<in> o[F](g)"

  2148 proof (rule landau_o.smallI)

  2149   fix c :: real assume "c > 0"

  2150   hence c: "min c 1 > 0" by simp

  2151   let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  2152   from assms have "((\<lambda>x. ?h x - 1) \<longlongrightarrow> 1 - 1) F"

  2153     by (intro tendsto_diff asymp_equivD tendsto_const)

  2154   from tendstoD[OF this c] show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"

  2155   proof eventually_elim

  2156     case (elim x)

  2157     from elim have "norm (f x - g x) \<le> norm (f x / g x - 1) * norm (g x)"

  2158       by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps)

  2159     also have "norm (f x / g x - 1) * norm (g x) \<le> c * norm (g x)" using elim

  2160       by (auto split: if_splits simp: mult_right_mono)

  2161     finally show ?case .

  2162   qed

  2163 qed

  2164

  2165 lemma asymp_equiv_altdef:

  2166   "f \<sim>[F] g \<longleftrightarrow> (\<lambda>x. f x - g x) \<in> o[F](g)"

  2167   by (rule iffI[OF asymp_equiv_imp_diff_smallo smallo_imp_asymp_equiv])

  2168

  2169 lemma asymp_equiv_0_left_iff [simp]: "(\<lambda>_. 0) \<sim>[F] f \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

  2170   and asymp_equiv_0_right_iff [simp]: "f \<sim>[F] (\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

  2171   by (simp_all add: asymp_equiv_altdef landau_o.small_refl_iff)

  2172

  2173 lemma asymp_equiv_sandwich_real:

  2174   fixes f g l u :: "'a \<Rightarrow> real"

  2175   assumes "l \<sim>[F] g" "u \<sim>[F] g" "eventually (\<lambda>x. f x \<in> {l x..u x}) F"

  2176   shows   "f \<sim>[F] g"

  2177   unfolding asymp_equiv_altdef

  2178 proof (rule landau_o.smallI)

  2179   fix c :: real assume c: "c > 0"

  2180   have "eventually (\<lambda>x. norm (f x - g x) \<le> max (norm (l x - g x)) (norm (u x - g x))) F"

  2181     using assms(3) by eventually_elim auto

  2182   moreover have "eventually (\<lambda>x. norm (l x - g x) \<le> c * norm (g x)) F"

  2183                 "eventually (\<lambda>x. norm (u x - g x) \<le> c * norm (g x)) F"

  2184     using assms(1,2) by (auto simp: asymp_equiv_altdef dest: landau_o.smallD[OF _ c])

  2185   hence "eventually (\<lambda>x. max (norm (l x - g x)) (norm (u x - g x)) \<le> c * norm (g x)) F"

  2186     by eventually_elim simp

  2187   ultimately show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"

  2188     by eventually_elim (rule order.trans)

  2189 qed

  2190

  2191 lemma asymp_equiv_sandwich_real':

  2192   fixes f g l u :: "'a \<Rightarrow> real"

  2193   assumes "f \<sim>[F] l" "f \<sim>[F] u" "eventually (\<lambda>x. g x \<in> {l x..u x}) F"

  2194   shows   "f \<sim>[F] g"

  2195   using asymp_equiv_sandwich_real[of l F f u g] assms by (simp add: asymp_equiv_sym)

  2196

  2197 lemma asymp_equiv_sandwich_real'':

  2198   fixes f g l u :: "'a \<Rightarrow> real"

  2199   assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"

  2200           "eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"

  2201   shows   "f \<sim>[F] g"

  2202   by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]

  2203              asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];

  2204       blast intro: asymp_equiv_trans assms(1,2,3))+

  2205

  2206 end