src/HOL/Library/Landau_Symbols.thy
 author haftmann Wed Jul 18 20:51:21 2018 +0200 (11 months ago) changeset 68658 16cc1161ad7f parent 68406 6beb45f6cf67 child 68696 8a071eeddb2a permissions -rw-r--r--
tuned equation
     1 (*

     2   File:   Landau_Symbols_Definition.thy

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

     4

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

     6 *)

     7 section {* Definition of Landau symbols *}

     8

     9 theory Landau_Symbols

    10 imports

    11   Complex_Main

    12 begin

    13

    14 lemma eventually_subst':

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

    16   by (rule eventually_subst, erule eventually_rev_mp) simp

    17

    18

    19 subsection {* Definition of Landau symbols *}

    20

    21 text {*

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

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

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

    25   to work with.

    26 *}

    27

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

    29     ("(1O[_]'(_'))")

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

    31

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

    33     ("(1o[_]'(_'))")

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

    35

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

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

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

    39

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

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

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

    43

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

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

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

    47

    48 abbreviation bigo_at_top ("(2O'(_'))") where

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

    50

    51 abbreviation smallo_at_top ("(2o'(_'))") where

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

    53

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

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

    56

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

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

    59

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

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

    62

    63

    64 text {* The following is a set of properties that all Landau symbols satisfy. *}

    65

    66 named_theorems landau_divide_simps

    67

    68 locale landau_symbol =

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

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

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

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

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

    74   assumes in_filtermap_iff:

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

    76   assumes filtercomap:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    95 begin

    96

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

    98

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

   100   using filter_mono'[of F1 F2] by blast

   101

   102 lemma cong_ex:

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

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

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

   106

   107 lemma cong_ex_bigtheta:

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

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

   110

   111 lemma bigtheta_trans1:

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

   113   by (subst cong_bigtheta[symmetric])

   114

   115 lemma bigtheta_trans2:

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

   117   by (subst in_cong_bigtheta)

   118

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

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

   121

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

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

   124

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

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

   127

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

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

   130

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

   132

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

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

   135

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

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

   138

   139 (* Simplifier loops without the NO_MATCH *)

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

   141   by (rule const)

   142

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

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

   145

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

   147   by (rule const_in_iff)

   148

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

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

   151

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

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

   154

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

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

   157

   158 lemma inverse_cancel:

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

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

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

   162 proof

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

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

   165 qed (intro inverse assms)

   166

   167 lemma divide_right:

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

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

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

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

   172

   173 lemma divide_right_iff:

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

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

   176 proof

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

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

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

   180 qed (simp add: divide_right assms)

   181

   182 lemma divide_left:

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

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

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

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

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

   188

   189 lemma divide_left_iff:

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

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

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

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

   194 proof

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

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

   197     by eventually_elim (simp add: divide_inverse)

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

   199     by eventually_elim (simp add: divide_inverse)

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

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

   202 qed (simp add: divide_left assms)

   203

   204 lemma divide:

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

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

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

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

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

   210

   211 lemma divide_eq1:

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

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

   214 proof-

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

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

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

   218 qed

   219

   220 lemma divide_eq2:

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

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

   223 proof-

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

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

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

   227 qed

   228

   229 lemma inverse_eq1:

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

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

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

   233

   234 lemma inverse_eq2:

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

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

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

   238

   239 lemma inverse_flip:

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

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

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

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

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

   245

   246 lemma lift_trans:

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

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

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

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

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

   252

   253 lemma lift_trans':

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

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

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

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

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

   259

   260 lemma lift_trans_bigtheta:

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

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

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

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

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

   266

   267 lemma lift_trans_bigtheta':

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

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

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

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

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

   273

   274 lemma (in landau_symbol) mult_in_1:

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

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

   277   using mult[OF assms] by simp

   278

   279 lemma (in landau_symbol) of_real_cancel:

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

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

   282

   283 lemma (in landau_symbol) of_real_iff:

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

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

   286

   287 lemmas [landau_divide_simps] =

   288   inverse_cancel divide_left_iff divide_eq1 divide_eq2 inverse_eq1 inverse_eq2

   289

   290 end

   291

   292

   293 text {*

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

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

   296   The following locale captures this fact.

   297 *}

   298

   299 locale landau_pair =

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

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

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

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

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

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

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

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

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

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

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

   311

   312 interpretation landau_o:

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

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

   315

   316 interpretation landau_omega:

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

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

   319

   320

   321 context landau_pair

   322 begin

   323

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

   325

   326 lemma bigI:

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

   328   unfolding L_def by blast

   329

   330 lemma bigE:

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

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

   333   using assms unfolding L_def by blast

   334

   335 lemma smallI:

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

   337   unfolding l_def by blast

   338

   339 lemma smallD:

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

   341   unfolding l_def by blast

   342

   343 lemma bigE_nonneg_real:

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

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

   346 proof-

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

   348     by (auto simp: Lr_def)

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

   350     by eventually_elim simp

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

   352 qed

   353

   354 lemma smallD_nonneg_real:

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

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

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

   358

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

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

   361

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

   363   using small_imp_big by blast

   364

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

   366

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

   368   using R by auto

   369

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

   371   using R by auto

   372

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

   374   using R by (auto simp: mult_left_mono)

   375

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

   377   using R by (auto simp: mult_right_mono)

   378

   379 lemma big_trans:

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

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

   382 proof-

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

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

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

   386   proof eventually_elim

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

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

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

   390       by (intro R_mult_left_mono) simp_all

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

   392   qed

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

   394 qed

   395

   396 lemma big_small_trans:

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

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

   399 proof (rule smallI)

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

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

   402   note d(2)

   403   moreover from c d assms(2)

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

   405     by (intro smallD) simp_all

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

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

   408 qed

   409

   410 lemma small_big_trans:

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

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

   413 proof (rule smallI)

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

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

   416   note d(2)

   417   moreover from c d assms(1)

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

   419     by (intro smallD) simp_all

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

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

   422 qed

   423

   424 lemma small_trans:

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

   426   by (rule big_small_trans[OF small_imp_big])

   427

   428 lemma small_big_trans':

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

   430   by (rule small_imp_big[OF small_big_trans])

   431

   432 lemma big_small_trans':

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

   434   by (rule small_imp_big[OF big_small_trans])

   435

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

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

   438

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

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

   441

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

   443   by (rule bigI[of 1]) simp_all

   444

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

   446 proof (rule iffI[OF _ smallI])

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

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

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

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

   451 next

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

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

   454     by eventually_elim simp_all

   455 qed

   456

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

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

   459

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

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

   462

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

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

   465

   466

   467 lemma plus_aux:

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

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

   470 proof (rule R_E)

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

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

   473   {

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

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

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

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

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

   479   } note B = this

   480

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

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

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

   484     using B apply (simp add: algebra_simps)

   485     done

   486 next

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

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

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

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

   491       using landau_o.smallD[OF assms zero_less_one]

   492     proof eventually_elim

   493       case (elim x)

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

   495       also note elim

   496       finally show ?case by simp

   497     qed

   498   qed simp_all

   499 qed

   500

   501 end

   502

   503

   504

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

   506 proof

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

   508   then guess c by (elim landau_o.bigE)

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

   510 next

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

   512   then guess c by (elim landau_omega.bigE)

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

   514 qed

   515

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

   517 proof

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

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

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

   521 next

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

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

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

   525 qed

   526

   527

   528 context landau_pair

   529 begin

   530

   531 lemma big_mono:

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

   533   by (rule bigI[OF zero_less_one]) simp

   534

   535 lemma big_mult:

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

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

   538 proof-

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

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

   541

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

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

   544     using c1(2) c2(2)

   545   proof eventually_elim

   546     case (elim x)

   547     show ?case

   548     proof (cases rule: R_E)

   549       case le

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

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

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

   553     next

   554       case ge

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

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

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

   558     qed

   559   qed

   560   ultimately show ?thesis by (rule bigI)

   561 qed

   562

   563 lemma small_big_mult:

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

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

   566 proof (rule smallI)

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

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

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

   570     by (auto intro!: smallD)

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

   572   proof eventually_elim

   573     case (elim x)

   574     show ?case

   575     proof (cases rule: R_E)

   576       case le

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

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

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

   580     next

   581       case ge

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

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

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

   585     qed

   586   qed

   587 qed

   588

   589 lemma big_small_mult:

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

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

   592

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

   594   by (rule small_big_mult, assumption, rule small_imp_big)

   595

   596 lemmas mult = big_mult small_big_mult big_small_mult small_mult

   597

   598

   599 sublocale big: landau_symbol L L' Lr

   600 proof

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

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

   603   {

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

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

   606   } note A = this

   607   {

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

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

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

   611   }

   612   {

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

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

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

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

   617   }

   618   {

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

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

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

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

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

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

   625   }

   626   {

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

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

   629   }

   630   {

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

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

   633

   634       thm eventually_subst A

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

   636   }

   637   {

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

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

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

   641   }

   642   {

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

   644   }

   645   {

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

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

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

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

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

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

   652   }

   653   {

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

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

   656   }

   657   {

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

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

   660   }

   661   {

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

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

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

   665   }

   666   {

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

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

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

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

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

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

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

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

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

   676   }

   677   {

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

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

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

   681       unfolding L_def L'_def by auto

   682   }

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

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

   685

   686 sublocale small: landau_symbol l l' lr

   687 proof

   688   {

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

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

   691   } note A = this

   692   {

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

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

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

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

   697   }

   698   {

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

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

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

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

   703   }

   704   {

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

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

   707   }

   708   {

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

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

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

   712     proof (rule smallI)

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

   714       from B smallD[OF A c]

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

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

   717     qed

   718   }

   719   {

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

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

   722   }

   723   {

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

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

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

   727   }

   728   {

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

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

   731   }

   732   {

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

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

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

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

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

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

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

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

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

   742       (insert A, auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo

   743        intro: landau_o.big_small_trans landau_o.small_big_trans)

   744   }

   745   {

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

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

   748   }

   749   {

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

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

   752   }

   753   {

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

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

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

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

   758   }

   759   {

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

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

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

   763       unfolding l_def l'_def by auto

   764   }

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

   766

   767

   768 text {* These rules allow chaining of Landau symbol propositions in Isar with "also".*}

   769

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

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

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

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

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

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

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

   777

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

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

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

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

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

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

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

   785

   786 lemmas mult_1_trans =

   787   big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1'''

   788   big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult'''

   789

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

   791 proof

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

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

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

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

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

   797 qed (rule big.cong_bigtheta)

   798

   799 lemma big_prod:

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

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

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

   803

   804 lemma big_prod_in_1:

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

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

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

   808

   809 end

   810

   811

   812 context landau_symbol

   813 begin

   814

   815 lemma plus_absorb1:

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

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

   818 proof (intro equalityI)

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

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

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

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

   823 qed

   824

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

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

   827

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

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

   830

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

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

   833

   834 lemmas absorb = plus_absorb1 plus_absorb2 diff_absorb1 diff_absorb2

   835

   836 end

   837

   838

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

   840   unfolding bigtheta_def bigomega_def by blast

   841

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

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

   844   unfolding bigtheta_def bigo_def bigomega_def by blast+

   845

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

   847   unfolding bigtheta_def by simp

   848

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

   850   unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)

   851

   852 lemmas landau_flip =

   853   bigomega_iff_bigo[symmetric] smallomega_iff_smallo[symmetric]

   854   bigomega_iff_bigo smallomega_iff_smallo bigtheta_sym

   855

   856

   857 interpretation landau_theta: landau_symbol bigtheta bigtheta bigtheta

   858 proof

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

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

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

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

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

   864 next

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

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

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

   868     apply (subst (1 2) bigtheta_def)

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

   870     apply (rule refl)

   871     done

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

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

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

   875 next

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

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

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

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

   880 next

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

   882   assume "F1 \<le> F2"

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

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

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

   886                 landau_o.big.cmult landau_omega.big.cmult

   887                 landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff

   888                 landau_o.big.in_cong landau_omega.big.in_cong

   889                 landau_o.big.mult landau_omega.big.mult

   890                 landau_o.big.inverse landau_omega.big.inverse

   891                 landau_o.big.compose landau_omega.big.compose

   892                 landau_o.big.bot' landau_omega.big.bot'

   893                 landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff

   894                 landau_o.big.sup landau_omega.big.sup

   895                 landau_o.big.filtercomap landau_omega.big.filtercomap

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

   897

   898 lemmas landau_symbols =

   899   landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms

   900   landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms

   901   landau_theta.landau_symbol_axioms

   902

   903 lemma bigoI [intro]:

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

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

   906 proof (rule landau_o.bigI)

   907   show "max 1 c > 0" by simp

   908   note assms

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

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

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

   912 qed

   913

   914 lemma smallomegaD [dest]:

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

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

   917 proof (cases "c > 0")

   918   case False

   919   show ?thesis

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

   921        (insert False, auto intro!: mult_nonpos_nonneg)

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

   923

   924

   925 lemma bigthetaI':

   926   assumes "c1 > 0" "c2 > 0"

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

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

   929 apply (rule bigthetaI)

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

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

   932 done

   933

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

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

   936

   937 lemma (in landau_symbol) ev_eq_trans1:

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

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

   940

   941 lemma (in landau_symbol) ev_eq_trans2:

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

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

   944

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

   946 declare landau_o.bigE landau_omega.bigE [elim]

   947 declare landau_o.smallD

   948

   949 lemma (in landau_symbol) bigtheta_trans1':

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

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

   952

   953 lemma (in landau_symbol) bigtheta_trans2':

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

   955   by (rule bigtheta_trans2, subst bigtheta_sym)

   956

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

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

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

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

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

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

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

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

   965   by (unfold bigomega_iff_bigo smallomega_iff_smallo)

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

   967                 landau_o.big_trans landau_o.small_trans)+

   968

   969 lemmas landau_trans_lift [trans] =

   970   landau_symbols[THEN landau_symbol.lift_trans]

   971   landau_symbols[THEN landau_symbol.lift_trans']

   972   landau_symbols[THEN landau_symbol.lift_trans_bigtheta]

   973   landau_symbols[THEN landau_symbol.lift_trans_bigtheta']

   974

   975 lemmas landau_mult_1_trans [trans] =

   976   landau_o.mult_1_trans landau_omega.mult_1_trans

   977

   978 lemmas landau_trans [trans] =

   979   landau_symbols[THEN landau_symbol.bigtheta_trans1]

   980   landau_symbols[THEN landau_symbol.bigtheta_trans2]

   981   landau_symbols[THEN landau_symbol.bigtheta_trans1']

   982   landau_symbols[THEN landau_symbol.bigtheta_trans2']

   983   landau_symbols[THEN landau_symbol.ev_eq_trans1]

   984   landau_symbols[THEN landau_symbol.ev_eq_trans2]

   985

   986   landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans

   987   landau_omega.big_trans landau_omega.small_trans

   988     landau_omega.small_big_trans landau_omega.big_small_trans

   989

   990   bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans

   991   bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans

   992

   993 lemma bigtheta_inverse [simp]:

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

   995 proof-

   996   {

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

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

   999     note c = this

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

  1001     moreover from c(2,4)

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

  1003     proof eventually_elim

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

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

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

  1007         by (force simp: field_simps norm_inverse norm_divide)

  1008     qed

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

  1010   }

  1011   thus ?thesis unfolding bigtheta_def

  1012     by (force simp: bigomega_iff_bigo bigtheta_sym)

  1013 qed

  1014

  1015 lemma bigtheta_divide:

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

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

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

  1019

  1020 lemma eventually_nonzero_bigtheta:

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

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

  1023 proof-

  1024   {

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

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

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

  1028   }

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

  1030 qed

  1031

  1032

  1033 subsection {* Landau symbols and limits *}

  1034

  1035 lemma bigoI_tendsto_norm:

  1036   fixes f g

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

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

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

  1040 proof (rule bigoI)

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

  1042     using tendstoD by force

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

  1044     unfolding dist_real_def using assms(2)

  1045   proof eventually_elim

  1046     case (elim x)

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

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

  1049       by (simp add: norm_mult abs_mult)

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

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

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

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

  1054       by (rule mult_left_mono) simp_all

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

  1056   qed

  1057 qed

  1058

  1059 lemma bigoI_tendsto:

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

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

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

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

  1064

  1065 lemma bigomegaI_tendsto_norm:

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

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

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

  1069 proof (cases "F = bot")

  1070   case False

  1071   show ?thesis

  1072   proof (rule landau_omega.bigI)

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

  1074     with c_not_0 have "c > 0" by simp

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

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

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

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

  1079     proof (eventually_elim)

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

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

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

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

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

  1085         by (simp add: field_simps norm_mult norm_divide)

  1086     qed

  1087   qed

  1088 qed simp

  1089

  1090 lemma bigomegaI_tendsto:

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

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

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

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

  1095

  1096 lemma smallomegaI_filterlim_at_top_norm:

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

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

  1099 proof (rule landau_omega.smallI)

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

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

  1102     by (subst (asm) filterlim_at_top) simp

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

  1104   proof eventually_elim

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

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

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

  1108   qed

  1109 qed

  1110

  1111 lemma smallomegaI_filterlim_at_infinity:

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

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

  1114 proof (rule smallomegaI_filterlim_at_top_norm)

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

  1116     by (rule filterlim_at_infinity_imp_norm_at_top)

  1117 qed

  1118

  1119 lemma smallomegaD_filterlim_at_top_norm:

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

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

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

  1123 proof (subst filterlim_at_top_gt, clarify)

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

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

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

  1127     by eventually_elim (simp add: field_simps norm_divide)

  1128 qed

  1129

  1130 lemma smallomegaD_filterlim_at_infinity:

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

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

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

  1134   using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm)

  1135

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

  1137   by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)

  1138

  1139 lemma smalloI_tendsto:

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

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

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

  1143 proof (rule landau_o.smallI)

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

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

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

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

  1148     by eventually_elim (simp add: field_simps norm_divide)

  1149 qed

  1150

  1151 lemma smalloD_tendsto:

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

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

  1154 unfolding tendsto_iff

  1155 proof clarify

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

  1157   hence "e/2 > 0" by simp

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

  1159   proof eventually_elim

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

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

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

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

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

  1165   qed

  1166 qed

  1167

  1168 lemma bigthetaI_tendsto_norm:

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

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

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

  1172 proof (rule bigthetaI)

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

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

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

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

  1177

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

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

  1180 qed

  1181

  1182 lemma bigthetaI_tendsto:

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

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

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

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

  1187

  1188 lemma tendsto_add_smallo:

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

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

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

  1192 proof (subst filterlim_cong[OF refl refl])

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

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

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

  1196     by eventually_elim (auto simp: field_simps)

  1197 next

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

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

  1200 qed

  1201

  1202 lemma tendsto_diff_smallo:

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

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

  1205

  1206 lemma tendsto_add_smallo_iff:

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

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

  1209 proof

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

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

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

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

  1214 qed (rule tendsto_add_smallo[OF _ assms])

  1215

  1216 lemma tendsto_diff_smallo_iff:

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

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

  1219

  1220 lemma tendsto_divide_smallo:

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

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

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

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

  1225 proof (subst tendsto_cong)

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

  1227

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

  1229   by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const

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

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

  1232

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

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

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

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

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

  1238   proof eventually_elim

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

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

  1241     show "?f x = ?f' x"

  1242     proof (cases "f1 x = 0")

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

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

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

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

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

  1248       finally show ?thesis .

  1249     qed (insert A, simp)

  1250   qed

  1251 qed

  1252

  1253

  1254 lemma bigo_powr:

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

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

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

  1258 proof-

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

  1260   note c = this

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

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

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

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

  1265 qed

  1266

  1267 lemma smallo_powr:

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

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

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

  1271 proof (rule landau_o.smallI)

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

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

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

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

  1276   proof eventually_elim

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

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

  1279       by (intro powr_mono2) simp_all

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

  1281       by (simp add: field_simps powr_mult powr_powr)

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

  1283   qed

  1284 qed

  1285

  1286 lemma smallo_powr_nonneg:

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

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

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

  1290 proof -

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

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

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

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

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

  1296   finally show ?thesis .

  1297 qed

  1298

  1299 lemma bigtheta_powr:

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

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

  1302 apply (cases "p < 0")

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

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

  1305 done

  1306

  1307 lemma bigo_powr_nonneg:

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

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

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

  1311 proof -

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

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

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

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

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

  1317   finally show ?thesis .

  1318 qed

  1319

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

  1321   by (intro landau_o.smallI) simp_all

  1322

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

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

  1325

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

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

  1328

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

  1330   by (simp add: smallomega_iff_smallo)

  1331

  1332

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

  1334 proof

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

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

  1337 next

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

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

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

  1341 qed

  1342

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

  1344 proof

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

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

  1347 next

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

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

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

  1351 qed

  1352

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

  1354   by (simp add: smallomega_iff_smallo)

  1355

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

  1357   by (simp add: bigomega_iff_bigo)

  1358

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

  1360   unfolding bigtheta_def by simp

  1361

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

  1363   unfolding bigtheta_def by simp

  1364

  1365

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

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

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

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

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

  1371

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

  1373

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

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

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

  1377

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

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

  1380      (auto simp: bigomega_def eventually_False mult_le_0_iff

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

  1382

  1383 lemma smallo_real_nat_transfer:

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

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

  1386

  1387 lemma bigo_real_nat_transfer:

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

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

  1390

  1391 lemma smallomega_real_nat_transfer:

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

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

  1394

  1395 lemma bigomega_real_nat_transfer:

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

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

  1398

  1399 lemma bigtheta_real_nat_transfer:

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

  1401   unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast

  1402

  1403 lemmas landau_real_nat_transfer [intro] =

  1404   bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer

  1405   smallomega_real_nat_transfer bigtheta_real_nat_transfer

  1406

  1407

  1408 lemma landau_symbol_if_at_top_eq [simp]:

  1409   assumes "landau_symbol L L' Lr"

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

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

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

  1413 done

  1414

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

  1416

  1417

  1418

  1419 lemma sum_in_smallo:

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

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

  1422 proof-

  1423   {

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

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

  1426     proof (rule landau_o.smallI)

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

  1428       hence "c/2 > 0" by simp

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

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

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

  1432     qed

  1433   }

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

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

  1436 qed

  1437

  1438 lemma big_sum_in_smallo:

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

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

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

  1442

  1443 lemma sum_in_bigo:

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

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

  1446 proof-

  1447   {

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

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

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

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

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

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

  1454   }

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

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

  1457 qed

  1458

  1459 lemma big_sum_in_bigo:

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

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

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

  1463

  1464 context landau_symbol

  1465 begin

  1466

  1467 lemma mult_cancel_left:

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

  1469   notes   [trans] = bigtheta_trans1 bigtheta_trans2

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

  1471 proof

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

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

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

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

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

  1477     by (intro divide_right) simp_all

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

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

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

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

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

  1483 next

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

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

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

  1487     by (intro landau_theta.mult_right assms)

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

  1489 qed

  1490

  1491 lemma mult_cancel_right:

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

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

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

  1495

  1496 lemma divide_cancel_right:

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

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

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

  1500

  1501 lemma divide_cancel_left:

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

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

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

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

  1506

  1507 end

  1508

  1509

  1510 lemma powr_smallo_iff:

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

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

  1513 proof-

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

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

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

  1517   proof

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

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

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

  1521     thus False by (simp add: eventually_False assms)

  1522   qed

  1523   show ?thesis

  1524   proof (cases p q rule: linorder_cases)

  1525     assume "p < q"

  1526     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A

  1527       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)

  1528     with p < q show ?thesis by auto

  1529   next

  1530     assume "p = q"

  1531     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)

  1532     with B p = q show ?thesis by auto

  1533   next

  1534     assume "p > q"

  1535     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A

  1536       by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)

  1537     with B p > q show ?thesis by auto

  1538   qed

  1539 qed

  1540

  1541 lemma powr_bigo_iff:

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

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

  1544 proof-

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

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

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

  1548   proof

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

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

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

  1552     thus False by (simp add: eventually_False assms)

  1553   qed

  1554   show ?thesis

  1555   proof (cases p q rule: linorder_cases)

  1556     assume "p < q"

  1557     hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A

  1558       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)

  1559     with p < q show ?thesis by (auto intro: landau_o.small_imp_big)

  1560   next

  1561     assume "p = q"

  1562     hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)

  1563     with B p = q show ?thesis by auto

  1564   next

  1565     assume "p > q"

  1566     hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A

  1567       by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)

  1568     with B p > q show ?thesis by (auto intro: landau_o.small_imp_big)

  1569   qed

  1570 qed

  1571

  1572 lemma powr_bigtheta_iff:

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

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

  1575   using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff)

  1576

  1577

  1578 subsection \<open>Flatness of real functions\<close>

  1579

  1580 text \<open>

  1581   Given two real-valued functions $f$ and $g$, we say that $f$ is flatter than $g$ if

  1582   any power of $f(x)$ is asymptotically dominated by any positive power of $g(x)$. This is

  1583   a useful notion since, given two products of powers of functions sorted by flatness, we can

  1584   compare them asymptotically by simply comparing the exponent lists lexicographically.

  1585

  1586   A simple sufficient criterion for flatness it that $\ln f(x) \in o(\ln g(x))$, which we show

  1587   now.

  1588 \<close>

  1589 lemma ln_smallo_imp_flat:

  1590   fixes f g :: "real \<Rightarrow> real"

  1591   assumes lim_f: "filterlim f at_top at_top"

  1592   assumes lim_g: "filterlim g at_top at_top"

  1593   assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"

  1594   assumes q: "q > 0"

  1595   shows   "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)"

  1596 proof (rule smalloI_tendsto)

  1597   from lim_f have "eventually (\<lambda>x. f x > 0) at_top"

  1598     by (simp add: filterlim_at_top_dense)

  1599   hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp

  1600

  1601   from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top"

  1602     by (simp add: filterlim_at_top_dense)

  1603   hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp

  1604   thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top"

  1605     by eventually_elim simp

  1606

  1607   have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) =

  1608                           p * ln (f x) - q * ln (g x)) at_top"

  1609     using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps)

  1610   have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top"

  1611     by (insert q)

  1612        (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult

  1613               tendsto_const tendsto_diff smalloD_tendsto[OF ln_o_ln] lim_g

  1614               filterlim_compose[OF ln_at_top] | simp)+

  1615   hence "filterlim (\<lambda>x. p * ln (f x) - q * ln (g x)) at_bot at_top"

  1616     by (subst (asm) filterlim_cong[OF refl refl eq])

  1617   hence *: "((\<lambda>x. exp (p * ln (f x) - q * ln (g x))) \<longlongrightarrow> 0) at_top"

  1618     by (rule filterlim_compose[OF exp_at_bot])

  1619   have eq: "eventually (\<lambda>x. exp (p * ln (f x) - q * ln (g x)) = f x powr p / g x powr q) at_top"

  1620     using f_nz g_nz by eventually_elim (simp add: powr_def exp_diff)

  1621   show "((\<lambda>x. f x powr p / g x powr q) \<longlongrightarrow> 0) at_top"

  1622     using * by (subst (asm) filterlim_cong[OF refl refl eq])

  1623 qed

  1624

  1625 lemma ln_smallo_imp_flat':

  1626   fixes f g :: "real \<Rightarrow> real"

  1627   assumes lim_f: "filterlim f at_top at_top"

  1628   assumes lim_g: "filterlim g at_top at_top"

  1629   assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"

  1630   assumes q: "q < 0"

  1631   shows   "(\<lambda>x. g x powr q) \<in> o(\<lambda>x. f x powr p)"

  1632 proof -

  1633   from lim_f lim_g have "eventually (\<lambda>x. f x > 0) at_top" "eventually (\<lambda>x. g x > 0) at_top"

  1634     by (simp_all add: filterlim_at_top_dense)

  1635   hence "eventually (\<lambda>x. f x \<noteq> 0) at_top" "eventually (\<lambda>x. g x \<noteq> 0) at_top"

  1636     by (auto elim: eventually_mono)

  1637   moreover from assms have "(\<lambda>x. f x powr -p) \<in> o(\<lambda>x. g x powr -q)"

  1638     by (intro ln_smallo_imp_flat assms) simp_all

  1639   ultimately show ?thesis unfolding powr_minus

  1640     by (simp add: landau_o.small.inverse_cancel)

  1641 qed

  1642

  1643

  1644 subsection \<open>Asymptotic Equivalence\<close>

  1645

  1646 (* TODO Move *)

  1647 lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"

  1648   by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)

  1649

  1650 named_theorems asymp_equiv_intros

  1651 named_theorems asymp_equiv_simps

  1652

  1653 definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"

  1654   ("_ \<sim>[_] _" [51, 10, 51] 50)

  1655   where "f \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"

  1656

  1657 abbreviation (input) asymp_equiv_at_top where

  1658   "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"

  1659

  1660 bundle asymp_equiv_notation

  1661 begin

  1662 notation asymp_equiv_at_top (infix "\<sim>" 50)

  1663 end

  1664

  1665 lemma asymp_equivI: "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F \<Longrightarrow> f \<sim>[F] g"

  1666   by (simp add: asymp_equiv_def)

  1667

  1668 lemma asymp_equivD: "f \<sim>[F] g \<Longrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"

  1669   by (simp add: asymp_equiv_def)

  1670

  1671 lemma asymp_equiv_filtermap_iff:

  1672   "f \<sim>[filtermap h F] g \<longleftrightarrow> (\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"

  1673   by (simp add: asymp_equiv_def filterlim_filtermap)

  1674

  1675 lemma asymp_equiv_refl [simp, asymp_equiv_intros]: "f \<sim>[F] f"

  1676 proof (intro asymp_equivI)

  1677   have "eventually (\<lambda>x. 1 = (if f x = 0 \<and> f x = 0 then 1 else f x / f x)) F"

  1678     by (intro always_eventually) simp

  1679   moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp

  1680   ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"

  1681     by (rule Lim_transform_eventually)

  1682 qed

  1683

  1684 lemma asymp_equiv_symI:

  1685   assumes "f \<sim>[F] g"

  1686   shows   "g \<sim>[F] f"

  1687   using tendsto_inverse[OF asymp_equivD[OF assms]]

  1688   by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong)

  1689

  1690 lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f"

  1691   by (blast intro: asymp_equiv_symI)

  1692

  1693 lemma asymp_equivI':

  1694   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"

  1695   shows   "f \<sim>[F] g"

  1696 proof (cases "F = bot")

  1697   case False

  1698   have "eventually (\<lambda>x. f x \<noteq> 0) F"

  1699   proof (rule ccontr)

  1700     assume "\<not>eventually (\<lambda>x. f x \<noteq> 0) F"

  1701     hence "frequently (\<lambda>x. f x = 0) F" by (simp add: frequently_def)

  1702     hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1)

  1703     from limit_frequently_eq[OF False this assms] show False by simp_all

  1704   qed

  1705   hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"

  1706     by eventually_elim simp

  1707   from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def

  1708     by (rule Lim_transform_eventually)

  1709 qed (simp_all add: asymp_equiv_def)

  1710

  1711

  1712 lemma asymp_equiv_cong:

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

  1714   shows   "f1 \<sim>[F] g1 \<longleftrightarrow> f2 \<sim>[F] g2"

  1715   unfolding asymp_equiv_def

  1716 proof (rule tendsto_cong, goal_cases)

  1717   case 1

  1718   from assms show ?case by eventually_elim simp

  1719 qed

  1720

  1721 lemma asymp_equiv_eventually_zeros:

  1722   fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"

  1723   assumes "f \<sim>[F] g"

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

  1725 proof -

  1726   let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  1727   have "eventually (\<lambda>x. x \<noteq> 0) (nhds (1::'b))"

  1728     by (rule t1_space_nhds) auto

  1729   hence "eventually (\<lambda>x. x \<noteq> 0) (filtermap ?h F)"

  1730     using assms unfolding asymp_equiv_def filterlim_def

  1731     by (rule filter_leD [rotated])

  1732   hence "eventually (\<lambda>x. ?h x \<noteq> 0) F" by (simp add: eventually_filtermap)

  1733   thus ?thesis by eventually_elim (auto split: if_splits)

  1734 qed

  1735

  1736 lemma asymp_equiv_transfer:

  1737   assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"

  1738   shows   "f2 \<sim>[F] g2"

  1739   using assms(1) asymp_equiv_cong[OF assms(2,3)] by simp

  1740

  1741 lemma asymp_equiv_transfer_trans [trans]:

  1742   assumes "(\<lambda>x. f x (h1 x)) \<sim>[F] (\<lambda>x. g x (h1 x))"

  1743   assumes "eventually (\<lambda>x. h1 x = h2 x) F"

  1744   shows   "(\<lambda>x. f x (h2 x)) \<sim>[F] (\<lambda>x. g x (h2 x))"

  1745   by (rule asymp_equiv_transfer[OF assms(1)]) (insert assms(2), auto elim!: eventually_mono)

  1746

  1747 lemma asymp_equiv_trans [trans]:

  1748   fixes f g h

  1749   assumes "f \<sim>[F] g" "g \<sim>[F] h"

  1750   shows   "f \<sim>[F] h"

  1751 proof -

  1752   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  1753   from assms[THEN asymp_equiv_eventually_zeros]

  1754     have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp

  1755   moreover from tendsto_mult[OF assms[THEN asymp_equivD]]

  1756     have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp

  1757   ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)

  1758 qed

  1759

  1760 lemma asymp_equiv_trans_lift1 [trans]:

  1761   assumes "a \<sim>[F] f b" "b \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"

  1762   shows   "a \<sim>[F] f c"

  1763   using assms by (blast intro: asymp_equiv_trans)

  1764

  1765 lemma asymp_equiv_trans_lift2 [trans]:

  1766   assumes "f a \<sim>[F] b" "a \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"

  1767   shows   "f c \<sim>[F] b"

  1768   using asymp_equiv_symI[OF assms(3)[OF assms(2)]] assms(1)

  1769   by (blast intro: asymp_equiv_trans)

  1770

  1771 lemma asymp_equivD_const:

  1772   assumes "f \<sim>[F] (\<lambda>_. c)"

  1773   shows   "(f \<longlongrightarrow> c) F"

  1774 proof (cases "c = 0")

  1775   case False

  1776   with tendsto_mult_right[OF asymp_equivD[OF assms], of c] show ?thesis by simp

  1777 next

  1778   case True

  1779   with asymp_equiv_eventually_zeros[OF assms] show ?thesis

  1780     by (simp add: Lim_eventually)

  1781 qed

  1782

  1783 lemma asymp_equiv_refl_ev:

  1784   assumes "eventually (\<lambda>x. f x = g x) F"

  1785   shows   "f \<sim>[F] g"

  1786   by (intro asymp_equivI Lim_eventually)

  1787      (insert assms, auto elim!: eventually_mono)

  1788

  1789 lemma asymp_equiv_sandwich:

  1790   fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"

  1791   assumes "eventually (\<lambda>x. f x \<ge> 0) F"

  1792   assumes "eventually (\<lambda>x. f x \<le> g x) F"

  1793   assumes "eventually (\<lambda>x. g x \<le> h x) F"

  1794   assumes "f \<sim>[F] h"

  1795   shows   "g \<sim>[F] f" "g \<sim>[F] h"

  1796 proof -

  1797   show "g \<sim>[F] f"

  1798   proof (rule asymp_equivI, rule tendsto_sandwich)

  1799     from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]

  1800       show "eventually (\<lambda>n. (if h n = 0 \<and> f n = 0 then 1 else h n / f n) \<ge>

  1801                               (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"

  1802         by eventually_elim (auto intro!: divide_right_mono)

  1803     from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]

  1804       show "eventually (\<lambda>n. 1 \<le>

  1805                               (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"

  1806         by eventually_elim (auto intro!: divide_right_mono)

  1807   qed (insert asymp_equiv_symI[OF assms(4)], simp_all add: asymp_equiv_def)

  1808   also note \<open>f \<sim>[F] h\<close>

  1809   finally show "g \<sim>[F] h" .

  1810 qed

  1811

  1812 lemma asymp_equiv_imp_eventually_same_sign:

  1813   fixes f g :: "real \<Rightarrow> real"

  1814   assumes "f \<sim>[F] g"

  1815   shows   "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"

  1816 proof -

  1817   from assms have "((\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> sgn 1) F"

  1818     unfolding asymp_equiv_def by (rule tendsto_sgn) simp_all

  1819   from order_tendstoD(1)[OF this, of "1/2"]

  1820     have "eventually (\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x) > 1/2) F"

  1821     by simp

  1822   thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"

  1823   proof eventually_elim

  1824     case (elim x)

  1825     thus ?case

  1826       by (cases "f x" "0 :: real" rule: linorder_cases;

  1827           cases "g x" "0 :: real" rule: linorder_cases) simp_all

  1828   qed

  1829 qed

  1830

  1831 lemma

  1832   fixes f g :: "_ \<Rightarrow> real"

  1833   assumes "f \<sim>[F] g"

  1834   shows   asymp_equiv_eventually_same_sign: "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" (is ?th1)

  1835     and   asymp_equiv_eventually_neg_iff:   "eventually (\<lambda>x. f x < 0 \<longleftrightarrow> g x < 0) F" (is ?th2)

  1836     and   asymp_equiv_eventually_pos_iff:   "eventually (\<lambda>x. f x > 0 \<longleftrightarrow> g x > 0) F" (is ?th3)

  1837 proof -

  1838   from assms have "filterlim (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) (nhds 1) F"

  1839     by (rule asymp_equivD)

  1840   from order_tendstoD(1)[OF this zero_less_one]

  1841     show ?th1 ?th2 ?th3

  1842     by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+

  1843 qed

  1844

  1845 lemma asymp_equiv_tendsto_transfer:

  1846   assumes "f \<sim>[F] g" and "(f \<longlongrightarrow> c) F"

  1847   shows   "(g \<longlongrightarrow> c) F"

  1848 proof -

  1849   let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"

  1850   have "eventually (\<lambda>x. ?h x = g x) F"

  1851     using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp

  1852   moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)

  1853   hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"

  1854     by (rule asymp_equivD)

  1855   from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp

  1856   ultimately show ?thesis by (rule Lim_transform_eventually)

  1857 qed

  1858

  1859 lemma tendsto_asymp_equiv_cong:

  1860   assumes "f \<sim>[F] g"

  1861   shows   "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"

  1862 proof -

  1863   {

  1864     fix f g :: "'a \<Rightarrow> 'b"

  1865     assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"

  1866     have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"

  1867       using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp

  1868     moreover have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F"

  1869       by (intro tendsto_intros asymp_equivD *)

  1870     ultimately have "(f \<longlongrightarrow> c * 1) F"

  1871       by (rule Lim_transform_eventually)

  1872   }

  1873   from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym)

  1874 qed

  1875

  1876

  1877 lemma smallo_imp_eventually_sgn:

  1878   fixes f g :: "real \<Rightarrow> real"

  1879   assumes "g \<in> o(f)"

  1880   shows   "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top"

  1881 proof -

  1882   have "0 < (1/2 :: real)" by simp

  1883   from landau_o.smallD[OF assms, OF this]

  1884     have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp

  1885   thus ?thesis

  1886   proof eventually_elim

  1887     case (elim x)

  1888     thus ?case

  1889       by (cases "f x" "0::real" rule: linorder_cases;

  1890           cases "f x + g x" "0::real" rule: linorder_cases) simp_all

  1891   qed

  1892 qed

  1893

  1894 context

  1895 begin

  1896

  1897 private lemma asymp_equiv_add_rightI:

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

  1899   shows   "(\<lambda>x. f x + h x) \<sim>[F] g"

  1900 proof -

  1901   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

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

  1903     have ev: "eventually (\<lambda>x. g x = 0 \<longrightarrow> h x = 0) F" by eventually_elim auto

  1904   have "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1) F"

  1905     unfolding asymp_equiv_def using ev

  1906     by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps)

  1907   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1 + 0) F" by simp

  1908   also have \<dots> by (intro tendsto_intros asymp_equivD assms smalloD_tendsto)

  1909   finally show "(\<lambda>x. f x + h x) \<sim>[F] g" .

  1910 qed

  1911

  1912 lemma asymp_equiv_add_right [asymp_equiv_simps]:

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

  1914   shows   "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"

  1915 proof

  1916   assume "(\<lambda>x. f x + h x) \<sim>[F] g"

  1917   from asymp_equiv_add_rightI[OF this, of "\<lambda>x. -h x"] assms show "f \<sim>[F] g"

  1918     by simp

  1919 qed (simp_all add: asymp_equiv_add_rightI assms)

  1920

  1921 end

  1922

  1923 lemma asymp_equiv_add_left [asymp_equiv_simps]:

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

  1925   shows   "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"

  1926   using asymp_equiv_add_right[OF assms] by (simp add: add.commute)

  1927

  1928 lemma asymp_equiv_add_right' [asymp_equiv_simps]:

  1929   assumes "h \<in> o[F](g)"

  1930   shows   "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f"

  1931   using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym)

  1932

  1933 lemma asymp_equiv_add_left' [asymp_equiv_simps]:

  1934   assumes "h \<in> o[F](g)"

  1935   shows   "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f"

  1936   using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym)

  1937

  1938 lemma smallo_imp_asymp_equiv:

  1939   assumes "(\<lambda>x. f x - g x) \<in> o[F](g)"

  1940   shows   "f \<sim>[F] g"

  1941 proof -

  1942   from assms have "(\<lambda>x. f x - g x + g x) \<sim>[F] g"

  1943     by (subst asymp_equiv_add_left) simp_all

  1944   thus ?thesis by simp

  1945 qed

  1946

  1947 lemma asymp_equiv_uminus [asymp_equiv_intros]:

  1948   "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. -f x) \<sim>[F] (\<lambda>x. -g x)"

  1949   by (simp add: asymp_equiv_def cong: if_cong)

  1950

  1951 lemma asymp_equiv_uminus_iff [asymp_equiv_simps]:

  1952   "(\<lambda>x. -f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] (\<lambda>x. -g x)"

  1953   by (simp add: asymp_equiv_def cong: if_cong)

  1954

  1955 lemma asymp_equiv_mult [asymp_equiv_intros]:

  1956   fixes f1 f2 g1 g2 :: "'a \<Rightarrow> 'b :: real_normed_field"

  1957   assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"

  1958   shows   "(\<lambda>x. f1 x * f2 x) \<sim>[F] (\<lambda>x. g1 x * g2 x)"

  1959 proof -

  1960   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  1961   let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x

  1962                    else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)"

  1963   let ?S' = "\<lambda>x. ?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) x - ?T f1 g1 x * ?T f2 g2 x"

  1964   {

  1965     fix f g :: "'a \<Rightarrow> 'b" assume "f \<sim>[F] g"

  1966     have "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F"

  1967       by (rule tendsto_eq_intros refl asymp_equivD[OF \<open>f \<sim>[F] g\<close>])+ simp_all

  1968   } note A = this

  1969

  1970   from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"

  1971     by (intro tendsto_mult asymp_equivD)

  1972   moreover {

  1973     have "eventually (\<lambda>x. ?S x = ?S' x) F"

  1974       using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto

  1975     moreover have "(?S \<longlongrightarrow> 0) F"

  1976       by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])

  1977          (auto intro: le_infI1 le_infI2)

  1978     ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)

  1979   }

  1980   ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"

  1981     by (rule Lim_transform)

  1982   thus ?thesis by (simp add: asymp_equiv_def)

  1983 qed

  1984

  1985 lemma asymp_equiv_power [asymp_equiv_intros]:

  1986   "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)"

  1987   by (induction n) (simp_all add: asymp_equiv_mult)

  1988

  1989 lemma asymp_equiv_inverse [asymp_equiv_intros]:

  1990   assumes "f \<sim>[F] g"

  1991   shows   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"

  1992 proof -

  1993   from tendsto_inverse[OF asymp_equivD[OF assms]]

  1994     have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) \<longlongrightarrow> 1) F"

  1995     by (simp add: if_distrib cong: if_cong)

  1996   also have "(\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) =

  1997                (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else inverse (f x) / inverse (g x))"

  1998     by (intro ext) (simp add: field_simps)

  1999   finally show ?thesis by (simp add: asymp_equiv_def)

  2000 qed

  2001

  2002 lemma asymp_equiv_inverse_iff [asymp_equiv_simps]:

  2003   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<sim>[F] g"

  2004 proof

  2005   assume "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"

  2006   hence "(\<lambda>x. inverse (inverse (f x))) \<sim>[F] (\<lambda>x. inverse (inverse (g x)))" (is ?P)

  2007     by (rule asymp_equiv_inverse)

  2008   also have "?P \<longleftrightarrow> f \<sim>[F] g" by (intro asymp_equiv_cong) simp_all

  2009   finally show "f \<sim>[F] g" .

  2010 qed (simp_all add: asymp_equiv_inverse)

  2011

  2012 lemma asymp_equiv_divide [asymp_equiv_intros]:

  2013   assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"

  2014   shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"

  2015   using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)

  2016

  2017 lemma asymp_equiv_compose [asymp_equiv_intros]:

  2018   assumes "f \<sim>[G] g" "filterlim h G F"

  2019   shows   "f \<circ> h \<sim>[F] g \<circ> h"

  2020 proof -

  2021   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  2022   have "f \<circ> h \<sim>[F] g \<circ> h \<longleftrightarrow> ((?T f g \<circ> h) \<longlongrightarrow> 1) F"

  2023     by (simp add: asymp_equiv_def o_def)

  2024   also have "\<dots> \<longleftrightarrow> (?T f g \<longlongrightarrow> 1) (filtermap h F)"

  2025     by (rule tendsto_compose_filtermap)

  2026   also have "\<dots>"

  2027     by (rule tendsto_mono[of _ G]) (insert assms, simp_all add: asymp_equiv_def filterlim_def)

  2028   finally show ?thesis .

  2029 qed

  2030

  2031 lemma asymp_equiv_compose':

  2032   assumes "f \<sim>[G] g" "filterlim h G F"

  2033   shows   "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"

  2034   using asymp_equiv_compose[OF assms] by (simp add: o_def)

  2035

  2036 lemma asymp_equiv_powr_real [asymp_equiv_intros]:

  2037   fixes f g :: "'a \<Rightarrow> real"

  2038   assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"

  2039   shows   "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"

  2040 proof -

  2041   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  2042   have "eventually (\<lambda>x. ?T f g x powr y = ?T (\<lambda>x. f x powr y) (\<lambda>x. g x powr y) x) F"

  2043     using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)

  2044     by eventually_elim (auto simp: powr_divide)

  2045   moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"

  2046     by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all

  2047   hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp

  2048   ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)

  2049 qed

  2050

  2051 lemma asymp_equiv_norm [asymp_equiv_intros]:

  2052   fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"

  2053   assumes "f \<sim>[F] g"

  2054   shows   "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))"

  2055   using tendsto_norm[OF asymp_equivD[OF assms]]

  2056   by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong)

  2057

  2058 lemma asymp_equiv_abs_real [asymp_equiv_intros]:

  2059   fixes f g :: "'a \<Rightarrow> real"

  2060   assumes "f \<sim>[F] g"

  2061   shows   "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)"

  2062   using tendsto_rabs[OF asymp_equivD[OF assms]]

  2063   by (simp add: if_distrib asymp_equiv_def cong: if_cong)

  2064

  2065 lemma asymp_equiv_imp_eventually_le:

  2066   assumes "f \<sim>[F] g" "c > 1"

  2067   shows   "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"

  2068 proof -

  2069   from order_tendstoD(2)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]

  2070        asymp_equiv_eventually_zeros[OF assms(1)]

  2071     show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)

  2072 qed

  2073

  2074 lemma asymp_equiv_imp_eventually_ge:

  2075   assumes "f \<sim>[F] g" "c < 1"

  2076   shows   "eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F"

  2077 proof -

  2078   from order_tendstoD(1)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]

  2079        asymp_equiv_eventually_zeros[OF assms(1)]

  2080     show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)

  2081 qed

  2082

  2083 lemma asymp_equiv_imp_bigo:

  2084   assumes "f \<sim>[F] g"

  2085   shows   "f \<in> O[F](g)"

  2086 proof (rule bigoI)

  2087   have "(3/2::real) > 1" by simp

  2088   from asymp_equiv_imp_eventually_le[OF assms this]

  2089     show "eventually (\<lambda>x. norm (f x) \<le> 3/2 * norm (g x)) F"

  2090     by eventually_elim simp

  2091 qed

  2092

  2093 lemma asymp_equiv_imp_bigomega:

  2094   "f \<sim>[F] g \<Longrightarrow> f \<in> \<Omega>[F](g)"

  2095   using asymp_equiv_imp_bigo[of g F f] by (simp add: asymp_equiv_sym bigomega_iff_bigo)

  2096

  2097 lemma asymp_equiv_imp_bigtheta:

  2098   "f \<sim>[F] g \<Longrightarrow> f \<in> \<Theta>[F](g)"

  2099   by (intro bigthetaI asymp_equiv_imp_bigo asymp_equiv_imp_bigomega)

  2100

  2101 lemma asymp_equiv_at_infinity_transfer:

  2102   assumes "f \<sim>[F] g" "filterlim f at_infinity F"

  2103   shows   "filterlim g at_infinity F"

  2104 proof -

  2105   from assms(1) have "g \<in> \<Theta>[F](f)" by (rule asymp_equiv_imp_bigtheta[OF asymp_equiv_symI])

  2106   also from assms have "f \<in> \<omega>[F](\<lambda>_. 1)" by (simp add: smallomega_1_conv_filterlim)

  2107   finally show ?thesis by (simp add: smallomega_1_conv_filterlim)

  2108 qed

  2109

  2110 lemma asymp_equiv_at_top_transfer:

  2111   fixes f g :: "_ \<Rightarrow> real"

  2112   assumes "f \<sim>[F] g" "filterlim f at_top F"

  2113   shows   "filterlim g at_top F"

  2114 proof (rule filterlim_at_infinity_imp_filterlim_at_top)

  2115   show "filterlim g at_infinity F"

  2116     by (rule asymp_equiv_at_infinity_transfer[OF assms(1) filterlim_mono[OF assms(2)]])

  2117        (auto simp: at_top_le_at_infinity)

  2118   from assms(2) have "eventually (\<lambda>x. f x > 0) F"

  2119     using filterlim_at_top_dense by blast

  2120   with asymp_equiv_eventually_pos_iff[OF assms(1)] show "eventually (\<lambda>x. g x > 0) F"

  2121     by eventually_elim blast

  2122 qed

  2123

  2124 lemma asymp_equiv_at_bot_transfer:

  2125   fixes f g :: "_ \<Rightarrow> real"

  2126   assumes "f \<sim>[F] g" "filterlim f at_bot F"

  2127   shows   "filterlim g at_bot F"

  2128   unfolding filterlim_uminus_at_bot

  2129   by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"])

  2130      (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus)

  2131

  2132 lemma asymp_equivI'_const:

  2133   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0"

  2134   shows   "f \<sim>[F] (\<lambda>x. c * g x)"

  2135   using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2)

  2136   by (intro asymp_equivI') (simp add: field_simps)

  2137

  2138 lemma asymp_equivI'_inverse_const:

  2139   assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> inverse c) F" "c \<noteq> 0"

  2140   shows   "(\<lambda>x. c * f x) \<sim>[F] g"

  2141   using tendsto_mult[OF assms(1) tendsto_const[of "c"]] assms(2)

  2142   by (intro asymp_equivI') (simp add: field_simps)

  2143

  2144 lemma filterlim_at_bot_imp_at_infinity: "filterlim f at_bot F \<Longrightarrow> filterlim f at_infinity F"

  2145   for f :: "_ \<Rightarrow> real" using at_bot_le_at_infinity filterlim_mono by blast

  2146

  2147 lemma asymp_equiv_imp_diff_smallo:

  2148   assumes "f \<sim>[F] g"

  2149   shows   "(\<lambda>x. f x - g x) \<in> o[F](g)"

  2150 proof (rule landau_o.smallI)

  2151   fix c :: real assume "c > 0"

  2152   hence c: "min c 1 > 0" by simp

  2153   let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"

  2154   from assms have "((\<lambda>x. ?h x - 1) \<longlongrightarrow> 1 - 1) F"

  2155     by (intro tendsto_diff asymp_equivD tendsto_const)

  2156   from tendstoD[OF this c] show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"

  2157   proof eventually_elim

  2158     case (elim x)

  2159     from elim have "norm (f x - g x) \<le> norm (f x / g x - 1) * norm (g x)"

  2160       by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps)

  2161     also have "norm (f x / g x - 1) * norm (g x) \<le> c * norm (g x)" using elim

  2162       by (auto split: if_splits simp: mult_right_mono)

  2163     finally show ?case .

  2164   qed

  2165 qed

  2166

  2167 lemma asymp_equiv_altdef:

  2168   "f \<sim>[F] g \<longleftrightarrow> (\<lambda>x. f x - g x) \<in> o[F](g)"

  2169   by (rule iffI[OF asymp_equiv_imp_diff_smallo smallo_imp_asymp_equiv])

  2170

  2171 lemma asymp_equiv_0_left_iff [simp]: "(\<lambda>_. 0) \<sim>[F] f \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

  2172   and asymp_equiv_0_right_iff [simp]: "f \<sim>[F] (\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"

  2173   by (simp_all add: asymp_equiv_altdef landau_o.small_refl_iff)

  2174

  2175 lemma asymp_equiv_sandwich_real:

  2176   fixes f g l u :: "'a \<Rightarrow> real"

  2177   assumes "l \<sim>[F] g" "u \<sim>[F] g" "eventually (\<lambda>x. f x \<in> {l x..u x}) F"

  2178   shows   "f \<sim>[F] g"

  2179   unfolding asymp_equiv_altdef

  2180 proof (rule landau_o.smallI)

  2181   fix c :: real assume c: "c > 0"

  2182   have "eventually (\<lambda>x. norm (f x - g x) \<le> max (norm (l x - g x)) (norm (u x - g x))) F"

  2183     using assms(3) by eventually_elim auto

  2184   moreover have "eventually (\<lambda>x. norm (l x - g x) \<le> c * norm (g x)) F"

  2185                 "eventually (\<lambda>x. norm (u x - g x) \<le> c * norm (g x)) F"

  2186     using assms(1,2) by (auto simp: asymp_equiv_altdef dest: landau_o.smallD[OF _ c])

  2187   hence "eventually (\<lambda>x. max (norm (l x - g x)) (norm (u x - g x)) \<le> c * norm (g x)) F"

  2188     by eventually_elim simp

  2189   ultimately show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"

  2190     by eventually_elim (rule order.trans)

  2191 qed

  2192

  2193 lemma asymp_equiv_sandwich_real':

  2194   fixes f g l u :: "'a \<Rightarrow> real"

  2195   assumes "f \<sim>[F] l" "f \<sim>[F] u" "eventually (\<lambda>x. g x \<in> {l x..u x}) F"

  2196   shows   "f \<sim>[F] g"

  2197   using asymp_equiv_sandwich_real[of l F f u g] assms by (simp add: asymp_equiv_sym)

  2198

  2199 lemma asymp_equiv_sandwich_real'':

  2200   fixes f g l u :: "'a \<Rightarrow> real"

  2201   assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"

  2202           "eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"

  2203   shows   "f \<sim>[F] g"

  2204   by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]

  2205              asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];

  2206       blast intro: asymp_equiv_trans assms(1,2,3))+

  2207

  2208 end