src/HOL/Library/Landau_Symbols.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 69597 ff784d5a5bfb
child 70365 4df0628e8545
permissions -rw-r--r--
improved code equations taken over from AFP
eberlm@68246
     1
(*
eberlm@68246
     2
  File:   Landau_Symbols_Definition.thy
eberlm@68246
     3
  Author: Manuel Eberl <eberlm@in.tum.de>
eberlm@68246
     4
eberlm@68246
     5
  Landau symbols for reasoning about the asymptotic growth of functions. 
eberlm@68246
     6
*)
wenzelm@69272
     7
section \<open>Definition of Landau symbols\<close>
eberlm@68246
     8
eberlm@68246
     9
theory Landau_Symbols
eberlm@68246
    10
imports 
eberlm@68246
    11
  Complex_Main
eberlm@68246
    12
begin
eberlm@68246
    13
eberlm@68246
    14
lemma eventually_subst':
eberlm@68246
    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"
eberlm@68246
    16
  by (rule eventually_subst, erule eventually_rev_mp) simp
eberlm@68246
    17
eberlm@68246
    18
wenzelm@69272
    19
subsection \<open>Definition of Landau symbols\<close>
eberlm@68246
    20
wenzelm@69272
    21
text \<open>
eberlm@68246
    22
  Our Landau symbols are sign-oblivious, i.e. any function always has the same growth 
eberlm@68246
    23
  as its absolute. This has the advantage of making some cancelling rules for sums nicer, but 
eberlm@68246
    24
  introduces some problems in other places. Nevertheless, we found this definition more convenient
eberlm@68246
    25
  to work with.
wenzelm@69272
    26
\<close>
eberlm@68246
    27
eberlm@68246
    28
definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
wenzelm@69597
    29
    (\<open>(1O[_]'(_'))\<close>)
eberlm@68246
    30
  where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"  
eberlm@68246
    31
eberlm@68246
    32
definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
wenzelm@69597
    33
    (\<open>(1o[_]'(_'))\<close>)
eberlm@68246
    34
  where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
eberlm@68246
    35
eberlm@68246
    36
definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
wenzelm@69597
    37
    (\<open>(1\<Omega>[_]'(_'))\<close>)
eberlm@68246
    38
  where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"  
eberlm@68246
    39
eberlm@68246
    40
definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
wenzelm@69597
    41
    (\<open>(1\<omega>[_]'(_'))\<close>)
eberlm@68246
    42
  where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
eberlm@68246
    43
eberlm@68246
    44
definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
wenzelm@69597
    45
    (\<open>(1\<Theta>[_]'(_'))\<close>)
eberlm@68246
    46
  where "bigtheta F g = bigo F g \<inter> bigomega F g"
eberlm@68246
    47
wenzelm@69597
    48
abbreviation bigo_at_top (\<open>(2O'(_'))\<close>) where
eberlm@68246
    49
  "O(g) \<equiv> bigo at_top g"    
eberlm@68246
    50
wenzelm@69597
    51
abbreviation smallo_at_top (\<open>(2o'(_'))\<close>) where
eberlm@68246
    52
  "o(g) \<equiv> smallo at_top g"
eberlm@68246
    53
wenzelm@69597
    54
abbreviation bigomega_at_top (\<open>(2\<Omega>'(_'))\<close>) where
eberlm@68246
    55
  "\<Omega>(g) \<equiv> bigomega at_top g"
eberlm@68246
    56
wenzelm@69597
    57
abbreviation smallomega_at_top (\<open>(2\<omega>'(_'))\<close>) where
eberlm@68246
    58
  "\<omega>(g) \<equiv> smallomega at_top g"
eberlm@68246
    59
wenzelm@69597
    60
abbreviation bigtheta_at_top (\<open>(2\<Theta>'(_'))\<close>) where
eberlm@68246
    61
  "\<Theta>(g) \<equiv> bigtheta at_top g"
eberlm@68246
    62
    
eberlm@68246
    63
wenzelm@69272
    64
text \<open>The following is a set of properties that all Landau symbols satisfy.\<close>
eberlm@68246
    65
eberlm@68246
    66
named_theorems landau_divide_simps
eberlm@68246
    67
eberlm@68246
    68
locale landau_symbol =
eberlm@68246
    69
  fixes L  :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
eberlm@68246
    70
  and   L'  :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"
eberlm@68246
    71
  and   Lr  :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"
eberlm@68246
    72
  assumes bot': "L bot f = UNIV"
eberlm@68246
    73
  assumes filter_mono': "F1 \<le> F2 \<Longrightarrow> L F2 f \<subseteq> L F1 f"
eberlm@68246
    74
  assumes in_filtermap_iff: 
eberlm@68246
    75
    "f' \<in> L (filtermap h' F') g' \<longleftrightarrow> (\<lambda>x. f' (h' x)) \<in> L' F' (\<lambda>x. g' (h' x))"
eberlm@68246
    76
  assumes filtercomap: 
eberlm@68246
    77
    "f' \<in> L F'' g' \<Longrightarrow> (\<lambda>x. f' (h' x)) \<in> L' (filtercomap h' F'') (\<lambda>x. g' (h' x))"
eberlm@68246
    78
  assumes sup: "f \<in> L F1 g \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L (sup F1 F2) g"
eberlm@68246
    79
  assumes in_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"
eberlm@68246
    80
  assumes cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> L F (f) = L F (g)"
eberlm@68246
    81
  assumes cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> L F (f) = L F (g)"
eberlm@68246
    82
  assumes in_cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"
eberlm@68246
    83
  assumes cmult [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. c * f x) = L F (f)"
eberlm@68246
    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)"
eberlm@68246
    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)"
eberlm@68246
    86
  assumes inverse: "eventually (\<lambda>x. f x \<noteq> 0) F \<Longrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F \<Longrightarrow> 
eberlm@68246
    87
                        f \<in> L F (g) \<Longrightarrow> (\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))"
eberlm@68246
    88
  assumes subsetI: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"
eberlm@68246
    89
  assumes plus_subset1: "f \<in> o[F](g) \<Longrightarrow> L F (g) \<subseteq> L F (\<lambda>x. f x + g x)"
eberlm@68246
    90
  assumes trans: "f \<in> L F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
eberlm@68246
    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))"
eberlm@68246
    92
  assumes norm_iff [simp]: "(\<lambda>x. norm (f x)) \<in> Lr F (\<lambda>x. norm (g x)) \<longleftrightarrow> f \<in> L F (g)"
eberlm@68246
    93
  assumes abs [simp]: "Lr Fr (\<lambda>x. \<bar>fr x\<bar>) = Lr Fr fr"
eberlm@68246
    94
  assumes abs_in_iff [simp]: "(\<lambda>x. \<bar>fr x\<bar>) \<in> Lr Fr gr \<longleftrightarrow> fr \<in> Lr Fr gr"
eberlm@68246
    95
begin
eberlm@68246
    96
eberlm@68246
    97
lemma bot [simp]: "f \<in> L bot g" by (simp add: bot')
eberlm@68246
    98
  
eberlm@68246
    99
lemma filter_mono: "F1 \<le> F2 \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L F1 g"
eberlm@68246
   100
  using filter_mono'[of F1 F2] by blast
eberlm@68246
   101
eberlm@68246
   102
lemma cong_ex: 
eberlm@68246
   103
  "eventually (\<lambda>x. f1 x = f2 x) F \<Longrightarrow> eventually (\<lambda>x. g1 x = g2 x) F \<Longrightarrow>
eberlm@68246
   104
     f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" 
eberlm@68246
   105
  by (subst cong, assumption, subst in_cong, assumption, rule refl)
eberlm@68246
   106
eberlm@68246
   107
lemma cong_ex_bigtheta: 
eberlm@68246
   108
  "f1 \<in> \<Theta>[F](f2) \<Longrightarrow> g1 \<in> \<Theta>[F](g2) \<Longrightarrow> f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)" 
eberlm@68246
   109
  by (subst cong_bigtheta, assumption, subst in_cong_bigtheta, assumption, rule refl)
eberlm@68246
   110
eberlm@68246
   111
lemma bigtheta_trans1: 
eberlm@68246
   112
  "f \<in> L F (g) \<Longrightarrow> g \<in> \<Theta>[F](h) \<Longrightarrow> f \<in> L F (h)"
eberlm@68246
   113
  by (subst cong_bigtheta[symmetric])
eberlm@68246
   114
eberlm@68246
   115
lemma bigtheta_trans2: 
eberlm@68246
   116
  "f \<in> \<Theta>[F](g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
eberlm@68246
   117
  by (subst in_cong_bigtheta)
eberlm@68246
   118
   
eberlm@68246
   119
lemma cmult' [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x * c) = L F (f)"
eberlm@68246
   120
  by (subst mult.commute) (rule cmult)
eberlm@68246
   121
eberlm@68246
   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)"
eberlm@68246
   123
  by (subst mult.commute) (rule cmult_in_iff)
eberlm@68246
   124
eberlm@68246
   125
lemma cdiv [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x / c) = L F (f)"
eberlm@68246
   126
  using cmult'[of "inverse c" F f] by (simp add: field_simps)
eberlm@68246
   127
eberlm@68246
   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)"
eberlm@68246
   129
  using cmult_in_iff'[of "inverse c" f] by (simp add: field_simps)
eberlm@68246
   130
  
eberlm@68246
   131
lemma uminus [simp]: "L F (\<lambda>x. -g x) = L F (g)" using cmult[of "-1"] by simp
eberlm@68246
   132
eberlm@68246
   133
lemma uminus_in_iff [simp]: "(\<lambda>x. -f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
eberlm@68246
   134
  using cmult_in_iff[of "-1"] by simp
eberlm@68246
   135
eberlm@68246
   136
lemma const: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"
eberlm@68246
   137
  by (subst (2) cmult[symmetric]) simp_all
eberlm@68246
   138
eberlm@68246
   139
(* Simplifier loops without the NO_MATCH *)
eberlm@68246
   140
lemma const' [simp]: "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"
eberlm@68246
   141
  by (rule const)
eberlm@68246
   142
eberlm@68246
   143
lemma const_in_iff: "c \<noteq> 0 \<Longrightarrow> (\<lambda>_. c) \<in> L F (f) \<longleftrightarrow> (\<lambda>_. 1) \<in> L F (f)"
eberlm@68246
   144
  using cmult_in_iff'[of c "\<lambda>_. 1"] by simp
eberlm@68246
   145
eberlm@68246
   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)"
eberlm@68246
   147
  by (rule const_in_iff)
eberlm@68246
   148
eberlm@68246
   149
lemma plus_subset2: "g \<in> o[F](f) \<Longrightarrow> L F (f) \<subseteq> L F (\<lambda>x. f x + g x)"
eberlm@68246
   150
  by (subst add.commute) (rule plus_subset1)
eberlm@68246
   151
eberlm@68246
   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)"
eberlm@68246
   153
  using mult_left by (simp add: mult.commute)
eberlm@68246
   154
eberlm@68246
   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)"
eberlm@68246
   156
  by (rule trans, erule mult_left, erule mult_right)
eberlm@68246
   157
eberlm@68246
   158
lemma inverse_cancel:
eberlm@68246
   159
  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
eberlm@68246
   160
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
   161
  shows   "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> g \<in> L F (f)"
eberlm@68246
   162
proof
eberlm@68246
   163
  assume "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x))"
eberlm@68246
   164
  from inverse[OF _ _ this] assms show "g \<in> L F (f)" by simp
eberlm@68246
   165
qed (intro inverse assms)
eberlm@68246
   166
eberlm@68246
   167
lemma divide_right:
eberlm@68246
   168
  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
eberlm@68246
   169
  assumes "f \<in> L F (g)"
eberlm@68246
   170
  shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"
eberlm@68246
   171
  by (subst (1 2) divide_inverse) (intro mult_right inverse assms)
eberlm@68246
   172
eberlm@68246
   173
lemma divide_right_iff:
eberlm@68246
   174
  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
eberlm@68246
   175
  shows   "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> f \<in> L F (g)"
eberlm@68246
   176
proof
eberlm@68246
   177
  assume "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"
eberlm@68246
   178
  from mult_right[OF this, of h] assms show "f \<in> L F (g)"
eberlm@68246
   179
    by (subst (asm) cong_ex[of _ f F _ g]) (auto elim!: eventually_mono)
eberlm@68246
   180
qed (simp add: divide_right assms)
eberlm@68246
   181
eberlm@68246
   182
lemma divide_left:
eberlm@68246
   183
  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
eberlm@68246
   184
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
   185
  assumes "g \<in> L F(f)"
eberlm@68246
   186
  shows   "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"
eberlm@68246
   187
  by (subst (1 2) divide_inverse) (intro mult_left inverse assms)
eberlm@68246
   188
eberlm@68246
   189
lemma divide_left_iff:
eberlm@68246
   190
  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
eberlm@68246
   191
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
   192
  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
eberlm@68246
   193
  shows   "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x) \<longleftrightarrow> g \<in> L F (f)"
eberlm@68246
   194
proof
eberlm@68246
   195
  assume A: "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"
eberlm@68246
   196
  from assms have B: "eventually (\<lambda>x. h x / f x / h x = inverse (f x)) F"
eberlm@68246
   197
    by eventually_elim (simp add: divide_inverse)
eberlm@68246
   198
  from assms have C: "eventually (\<lambda>x. h x / g x / h x = inverse (g x)) F"
eberlm@68246
   199
    by eventually_elim (simp add: divide_inverse)
eberlm@68246
   200
  from divide_right[OF assms(3) A] assms show "g \<in> L F (f)"
eberlm@68246
   201
    by (subst (asm) cong_ex[OF B C]) (simp add: inverse_cancel)
eberlm@68246
   202
qed (simp add: divide_left assms)
eberlm@68246
   203
eberlm@68246
   204
lemma divide:
eberlm@68246
   205
  assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
eberlm@68246
   206
  assumes "eventually (\<lambda>x. g2 x \<noteq> 0) F"
eberlm@68246
   207
  assumes "f1 \<in> L F (f2)" "g2 \<in> L F (g1)"
eberlm@68246
   208
  shows   "(\<lambda>x. f1 x / g1 x) \<in> L F (\<lambda>x. f2 x / g2 x)"
eberlm@68246
   209
  by (subst (1 2) divide_inverse) (intro mult inverse assms)
eberlm@68246
   210
  
eberlm@68246
   211
lemma divide_eq1:
eberlm@68246
   212
  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
eberlm@68246
   213
  shows   "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
eberlm@68246
   214
proof-
eberlm@68246
   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)"
eberlm@68246
   216
    using assms by (intro in_cong) (auto elim: eventually_mono)
eberlm@68246
   217
  thus ?thesis by (simp only: divide_right_iff assms)
eberlm@68246
   218
qed
eberlm@68246
   219
eberlm@68246
   220
lemma divide_eq2:
eberlm@68246
   221
  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
eberlm@68246
   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)"
eberlm@68246
   223
proof-
eberlm@68246
   224
  have "L F (\<lambda>x. g x) = L F (\<lambda>x. g x * h x / h x)"
eberlm@68246
   225
    using assms by (intro cong) (auto elim: eventually_mono)
eberlm@68246
   226
  thus ?thesis by (simp only: divide_right_iff assms)
eberlm@68246
   227
qed
eberlm@68246
   228
eberlm@68246
   229
lemma inverse_eq1:
eberlm@68246
   230
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
   231
  shows   "f \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> (\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"
eberlm@68246
   232
  using divide_eq1[of g F f "\<lambda>_. 1"] by (simp add: divide_inverse assms)
eberlm@68246
   233
eberlm@68246
   234
lemma inverse_eq2:
eberlm@68246
   235
  assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
eberlm@68246
   236
  shows   "(\<lambda>x. inverse (f x)) \<in> L F (g) \<longleftrightarrow> (\<lambda>x. 1) \<in> L F (\<lambda>x. f x * g x)"
eberlm@68246
   237
  using divide_eq2[of f F "\<lambda>_. 1" g] by (simp add: divide_inverse assms mult_ac)
eberlm@68246
   238
eberlm@68246
   239
lemma inverse_flip:
eberlm@68246
   240
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
   241
  assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
eberlm@68246
   242
  assumes "(\<lambda>x. inverse (g x)) \<in> L F (h)"
eberlm@68246
   243
  shows   "(\<lambda>x. inverse (h x)) \<in> L F (g)"
eberlm@68246
   244
using assms by (simp add: divide_eq1 divide_eq2 inverse_eq_divide mult.commute)
eberlm@68246
   245
eberlm@68246
   246
lemma lift_trans:
eberlm@68246
   247
  assumes "f \<in> L F (g)"
eberlm@68246
   248
  assumes "(\<lambda>x. t x (g x)) \<in> L F (h)"
eberlm@68246
   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))"
eberlm@68246
   250
  shows   "(\<lambda>x. t x (f x)) \<in> L F (h)"
eberlm@68246
   251
  by (rule trans[OF assms(3)[OF assms(1)] assms(2)])
eberlm@68246
   252
eberlm@68246
   253
lemma lift_trans':
eberlm@68246
   254
  assumes "f \<in> L F (\<lambda>x. t x (g x))"
eberlm@68246
   255
  assumes "g \<in> L F (h)"
eberlm@68246
   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))"
eberlm@68246
   257
  shows   "f \<in> L F (\<lambda>x. t x (h x))"
eberlm@68246
   258
  by (rule trans[OF assms(1) assms(3)[OF assms(2)]])
eberlm@68246
   259
eberlm@68246
   260
lemma lift_trans_bigtheta:
eberlm@68246
   261
  assumes "f \<in> L F (g)"
eberlm@68246
   262
  assumes "(\<lambda>x. t x (g x)) \<in> \<Theta>[F](h)"
eberlm@68246
   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))"
eberlm@68246
   264
  shows   "(\<lambda>x. t x (f x)) \<in> L F (h)"
eberlm@68246
   265
  using cong_bigtheta[OF assms(2)] assms(3)[OF assms(1)] by simp
eberlm@68246
   266
eberlm@68246
   267
lemma lift_trans_bigtheta':
eberlm@68246
   268
  assumes "f \<in> L F (\<lambda>x. t x (g x))"
eberlm@68246
   269
  assumes "g \<in> \<Theta>[F](h)"
eberlm@68246
   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))"
eberlm@68246
   271
  shows   "f \<in> L F (\<lambda>x. t x (h x))"
eberlm@68246
   272
  using cong_bigtheta[OF assms(3)[OF assms(2)]] assms(1)  by simp
eberlm@68246
   273
eberlm@68246
   274
lemma (in landau_symbol) mult_in_1:
eberlm@68246
   275
  assumes "f \<in> L F (\<lambda>_. 1)" "g \<in> L F (\<lambda>_. 1)"
eberlm@68246
   276
  shows   "(\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"
eberlm@68246
   277
  using mult[OF assms] by simp
eberlm@68246
   278
eberlm@68246
   279
lemma (in landau_symbol) of_real_cancel:
eberlm@68246
   280
  "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<Longrightarrow> f \<in> Lr F g"
eberlm@68246
   281
  by (subst (asm) norm_iff [symmetric], subst (asm) (1 2) norm_of_real) simp_all
eberlm@68246
   282
eberlm@68246
   283
lemma (in landau_symbol) of_real_iff:
eberlm@68246
   284
  "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<longleftrightarrow> f \<in> Lr F g"
eberlm@68246
   285
  by (subst norm_iff [symmetric], subst (1 2) norm_of_real) simp_all
eberlm@68246
   286
eberlm@68246
   287
lemmas [landau_divide_simps] = 
eberlm@68246
   288
  inverse_cancel divide_left_iff divide_eq1 divide_eq2 inverse_eq1 inverse_eq2
eberlm@68246
   289
eberlm@68246
   290
end
eberlm@68246
   291
eberlm@68246
   292
wenzelm@69272
   293
text \<open>
eberlm@68246
   294
  The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with 
eberlm@68246
   295
  $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem.
eberlm@68246
   296
  The following locale captures this fact.
wenzelm@69272
   297
\<close>
eberlm@68246
   298
eberlm@68246
   299
locale landau_pair = 
eberlm@68246
   300
  fixes L l :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
eberlm@68246
   301
  fixes L' l' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"
eberlm@68246
   302
  fixes Lr lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"
eberlm@68246
   303
  and   R :: "real \<Rightarrow> real \<Rightarrow> bool"
eberlm@68246
   304
  assumes L_def: "L F g = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"
eberlm@68246
   305
  and     l_def: "l F g = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"
eberlm@68246
   306
  and     L'_def: "L' F' g' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"
eberlm@68246
   307
  and     l'_def: "l' F' g' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"
eberlm@68246
   308
  and     Lr_def: "Lr F'' g'' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"
eberlm@68246
   309
  and     lr_def: "lr F'' g'' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"
eberlm@68246
   310
  and     R:     "R = (\<le>) \<or> R = (\<ge>)"
eberlm@68246
   311
eberlm@68246
   312
interpretation landau_o: 
eberlm@68246
   313
    landau_pair bigo smallo bigo smallo bigo smallo "(\<le>)"
eberlm@68246
   314
  by unfold_locales (auto simp: bigo_def smallo_def intro!: ext)
eberlm@68246
   315
eberlm@68246
   316
interpretation landau_omega: 
eberlm@68246
   317
    landau_pair bigomega smallomega bigomega smallomega bigomega smallomega "(\<ge>)"
eberlm@68246
   318
  by unfold_locales (auto simp: bigomega_def smallomega_def intro!: ext)
eberlm@68246
   319
eberlm@68246
   320
eberlm@68246
   321
context landau_pair
eberlm@68246
   322
begin
eberlm@68246
   323
eberlm@68246
   324
lemmas R_E = disjE [OF R, case_names le ge]
eberlm@68246
   325
eberlm@68246
   326
lemma bigI:
eberlm@68246
   327
  "c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F \<Longrightarrow> f \<in> L F (g)"
eberlm@68246
   328
  unfolding L_def by blast
eberlm@68246
   329
eberlm@68246
   330
lemma bigE:
eberlm@68246
   331
  assumes "f \<in> L F (g)"
eberlm@68246
   332
  obtains c where "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"
eberlm@68246
   333
  using assms unfolding L_def by blast
eberlm@68246
   334
eberlm@68246
   335
lemma smallI:
eberlm@68246
   336
  "(\<And>c. c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F) \<Longrightarrow> f \<in> l F (g)"
eberlm@68246
   337
  unfolding l_def by blast
eberlm@68246
   338
eberlm@68246
   339
lemma smallD:
eberlm@68246
   340
  "f \<in> l F (g) \<Longrightarrow> c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"
eberlm@68246
   341
  unfolding l_def by blast
eberlm@68246
   342
    
eberlm@68246
   343
lemma bigE_nonneg_real:
eberlm@68246
   344
  assumes "f \<in> Lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F"
eberlm@68246
   345
  obtains c where "c > 0" "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
eberlm@68246
   346
proof-
eberlm@68246
   347
  from assms(1) obtain c where c: "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
eberlm@68246
   348
    by (auto simp: Lr_def)
eberlm@68246
   349
  from c(2) assms(2) have "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
eberlm@68246
   350
    by eventually_elim simp
eberlm@68246
   351
  from c(1) and this show ?thesis by (rule that)
eberlm@68246
   352
qed
eberlm@68246
   353
eberlm@68246
   354
lemma smallD_nonneg_real:
eberlm@68246
   355
  assumes "f \<in> lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F" "c > 0"
eberlm@68246
   356
  shows   "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
eberlm@68246
   357
  using assms by (auto simp: lr_def dest!: spec[of _ c] elim: eventually_elim2)
eberlm@68246
   358
eberlm@68246
   359
lemma small_imp_big: "f \<in> l F (g) \<Longrightarrow> f \<in> L F (g)"
eberlm@68246
   360
  by (rule bigI[OF _ smallD, of 1]) simp_all
eberlm@68246
   361
  
eberlm@68246
   362
lemma small_subset_big: "l F (g) \<subseteq> L F (g)"
eberlm@68246
   363
  using small_imp_big by blast
eberlm@68246
   364
eberlm@68246
   365
lemma R_refl [simp]: "R x x" using R by auto
eberlm@68246
   366
eberlm@68246
   367
lemma R_linear: "\<not>R x y \<Longrightarrow> R y x"
eberlm@68246
   368
  using R by auto
eberlm@68246
   369
eberlm@68246
   370
lemma R_trans [trans]: "R a b \<Longrightarrow> R b c \<Longrightarrow> R a c"
eberlm@68246
   371
  using R by auto
eberlm@68246
   372
eberlm@68246
   373
lemma R_mult_left_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (c*a) (c*b)"
eberlm@68246
   374
  using R by (auto simp: mult_left_mono)
eberlm@68246
   375
eberlm@68246
   376
lemma R_mult_right_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (a*c) (b*c)"
eberlm@68246
   377
  using R by (auto simp: mult_right_mono)
eberlm@68246
   378
eberlm@68246
   379
lemma big_trans:
eberlm@68246
   380
  assumes "f \<in> L F (g)" "g \<in> L F (h)"
eberlm@68246
   381
  shows   "f \<in> L F (h)"
eberlm@68246
   382
proof-
eberlm@68246
   383
  from assms(1) guess c by (elim bigE) note c = this
eberlm@68246
   384
  from assms(2) guess d by (elim bigE) note d = this
eberlm@68246
   385
  from c(2) d(2) have "eventually (\<lambda>x. R (norm (f x)) (c * d * (norm (h x)))) F"
eberlm@68246
   386
  proof eventually_elim
eberlm@68246
   387
    fix x assume "R (norm (f x)) (c * (norm (g x)))"
eberlm@68246
   388
    also assume "R (norm (g x)) (d * (norm (h x)))"
eberlm@68246
   389
    with c(1) have "R (c * (norm (g x))) (c * (d * (norm (h x))))"
eberlm@68246
   390
      by (intro R_mult_left_mono) simp_all
eberlm@68246
   391
    finally show "R (norm (f x)) (c * d * (norm (h x)))" by (simp add: algebra_simps)
eberlm@68246
   392
  qed
eberlm@68246
   393
  with c(1) d(1) show ?thesis by (intro bigI[of "c*d"]) simp_all
eberlm@68246
   394
qed
eberlm@68246
   395
eberlm@68246
   396
lemma big_small_trans:
eberlm@68246
   397
  assumes "f \<in> L F (g)" "g \<in> l F (h)"
eberlm@68246
   398
  shows   "f \<in> l F (h)"
eberlm@68246
   399
proof (rule smallI)
eberlm@68246
   400
  fix c :: real assume c: "c > 0"
eberlm@68246
   401
  from assms(1) guess d by (elim bigE) note d = this
eberlm@68246
   402
  note d(2)
eberlm@68246
   403
  moreover from c d assms(2) 
eberlm@68246
   404
    have "eventually (\<lambda>x. R (norm (g x)) (c * inverse d * norm (h x))) F" 
eberlm@68246
   405
    by (intro smallD) simp_all
eberlm@68246
   406
  ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * (norm (h x)))) F"
eberlm@68246
   407
    by eventually_elim (erule R_trans, insert R d(1), auto simp: field_simps)
eberlm@68246
   408
qed
eberlm@68246
   409
eberlm@68246
   410
lemma small_big_trans:
eberlm@68246
   411
  assumes "f \<in> l F (g)" "g \<in> L F (h)"
eberlm@68246
   412
  shows   "f \<in> l F (h)"
eberlm@68246
   413
proof (rule smallI)
eberlm@68246
   414
  fix c :: real assume c: "c > 0"
eberlm@68246
   415
  from assms(2) guess d by (elim bigE) note d = this
eberlm@68246
   416
  note d(2)
eberlm@68246
   417
  moreover from c d assms(1) 
eberlm@68246
   418
    have "eventually (\<lambda>x. R (norm (f x)) (c * inverse d * norm (g x))) F"
eberlm@68246
   419
    by (intro smallD) simp_all
eberlm@68246
   420
  ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * norm (h x))) F"
eberlm@68246
   421
    by eventually_elim (rotate_tac 2, erule R_trans, insert R c d(1), auto simp: field_simps)
eberlm@68246
   422
qed
eberlm@68246
   423
eberlm@68246
   424
lemma small_trans:
eberlm@68246
   425
  "f \<in> l F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> l F (h)"
eberlm@68246
   426
  by (rule big_small_trans[OF small_imp_big])
eberlm@68246
   427
eberlm@68246
   428
lemma small_big_trans':
eberlm@68246
   429
  "f \<in> l F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
eberlm@68246
   430
  by (rule small_imp_big[OF small_big_trans])
eberlm@68246
   431
eberlm@68246
   432
lemma big_small_trans':
eberlm@68246
   433
  "f \<in> L F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> L F (h)"
eberlm@68246
   434
  by (rule small_imp_big[OF big_small_trans])
eberlm@68246
   435
eberlm@68246
   436
lemma big_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"
eberlm@68246
   437
  by (intro subsetI) (drule (1) big_trans)
eberlm@68246
   438
eberlm@68246
   439
lemma small_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> l F (f) \<subseteq> l F (g)"
eberlm@68246
   440
  by (intro subsetI) (drule (1) small_big_trans)
eberlm@68246
   441
eberlm@68246
   442
lemma big_refl [simp]: "f \<in> L F (f)"
eberlm@68246
   443
  by (rule bigI[of 1]) simp_all
eberlm@68246
   444
eberlm@68246
   445
lemma small_refl_iff: "f \<in> l F (f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
   446
proof (rule iffI[OF _ smallI])
eberlm@68246
   447
  assume f: "f \<in> l F f"
eberlm@68246
   448
  have "(1/2::real) > 0" "(2::real) > 0" by simp_all
eberlm@68246
   449
  from smallD[OF f this(1)] smallD[OF f this(2)]
eberlm@68246
   450
    show "eventually (\<lambda>x. f x = 0) F" by eventually_elim (insert R, auto)
eberlm@68246
   451
next
eberlm@68246
   452
  fix c :: real assume "c > 0" "eventually (\<lambda>x. f x = 0) F"
eberlm@68246
   453
  from this(2) show "eventually (\<lambda>x. R (norm (f x)) (c * norm (f x))) F"
eberlm@68246
   454
    by eventually_elim simp_all
eberlm@68246
   455
qed
eberlm@68246
   456
eberlm@68246
   457
lemma big_small_asymmetric: "f \<in> L F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
   458
  by (drule (1) big_small_trans) (simp add: small_refl_iff)
eberlm@68246
   459
eberlm@68246
   460
lemma small_big_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> L F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
   461
  by (drule (1) small_big_trans) (simp add: small_refl_iff)
eberlm@68246
   462
eberlm@68246
   463
lemma small_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
   464
  by (drule (1) small_trans) (simp add: small_refl_iff)
eberlm@68246
   465
eberlm@68246
   466
eberlm@68246
   467
lemma plus_aux:
eberlm@68246
   468
  assumes "f \<in> o[F](g)"
eberlm@68246
   469
  shows "g \<in> L F (\<lambda>x. f x + g x)"
eberlm@68246
   470
proof (rule R_E)
eberlm@68246
   471
  assume [simp]: "R = (\<le>)"
eberlm@68246
   472
  have A: "1/2 > (0::real)" by simp
eberlm@68246
   473
  {
eberlm@68246
   474
    fix x assume "norm (f x) \<le> 1/2 * norm (g x)"
eberlm@68246
   475
    hence "1/2 * (norm (g x)) \<le> (norm (g x)) - (norm (f x))" by simp
eberlm@68246
   476
    also have "norm (g x) - norm (f x) \<le> norm (f x + g x)"
eberlm@68246
   477
      by (subst add.commute) (rule norm_diff_ineq)
eberlm@68246
   478
    finally have "1/2 * (norm (g x)) \<le> norm (f x + g x)" by simp
eberlm@68246
   479
  } note B = this
eberlm@68246
   480
  
eberlm@68246
   481
  show "g \<in> L F (\<lambda>x. f x + g x)"
eberlm@68246
   482
    apply (rule bigI[of "2"], simp)
eberlm@68246
   483
    using landau_o.smallD[OF assms A] apply eventually_elim
eberlm@68246
   484
    using B apply (simp add: algebra_simps) 
eberlm@68246
   485
    done
eberlm@68246
   486
next
eberlm@68246
   487
  assume [simp]: "R = (\<lambda>x y. x \<ge> y)"
eberlm@68246
   488
  show "g \<in> L F (\<lambda>x. f x + g x)"
eberlm@68246
   489
  proof (rule bigI[of "1/2"])
eberlm@68246
   490
    show "eventually (\<lambda>x. R (norm (g x)) (1/2 * norm (f x + g x))) F"
eberlm@68246
   491
      using landau_o.smallD[OF assms zero_less_one]
eberlm@68246
   492
    proof eventually_elim
eberlm@68246
   493
      case (elim x)
eberlm@68246
   494
      have "norm (f x + g x) \<le> norm (f x) + norm (g x)" by (rule norm_triangle_ineq)
eberlm@68246
   495
      also note elim
eberlm@68246
   496
      finally show ?case by simp
eberlm@68246
   497
    qed
eberlm@68246
   498
  qed simp_all
eberlm@68246
   499
qed
eberlm@68246
   500
eberlm@68246
   501
end
eberlm@68246
   502
eberlm@68246
   503
eberlm@68246
   504
eberlm@68246
   505
lemma bigomega_iff_bigo: "g \<in> \<Omega>[F](f) \<longleftrightarrow> f \<in> O[F](g)"
eberlm@68246
   506
proof
eberlm@68246
   507
  assume "f \<in> O[F](g)"
eberlm@68246
   508
  then guess c by (elim landau_o.bigE)
eberlm@68246
   509
  thus "g \<in> \<Omega>[F](f)" by (intro landau_omega.bigI[of "inverse c"]) (simp_all add: field_simps)
eberlm@68246
   510
next
eberlm@68246
   511
  assume "g \<in> \<Omega>[F](f)"
eberlm@68246
   512
  then guess c by (elim landau_omega.bigE)
eberlm@68246
   513
  thus "f \<in> O[F](g)" by (intro landau_o.bigI[of "inverse c"]) (simp_all add: field_simps)
eberlm@68246
   514
qed
eberlm@68246
   515
eberlm@68246
   516
lemma smallomega_iff_smallo: "g \<in> \<omega>[F](f) \<longleftrightarrow> f \<in> o[F](g)"
eberlm@68246
   517
proof
eberlm@68246
   518
  assume "f \<in> o[F](g)"
eberlm@68246
   519
  from landau_o.smallD[OF this, of "inverse c" for c]
eberlm@68246
   520
    show "g \<in> \<omega>[F](f)" by (intro landau_omega.smallI) (simp_all add: field_simps)
eberlm@68246
   521
next
eberlm@68246
   522
  assume "g \<in> \<omega>[F](f)"
eberlm@68246
   523
  from landau_omega.smallD[OF this, of "inverse c" for c]
eberlm@68246
   524
    show "f \<in> o[F](g)" by (intro landau_o.smallI) (simp_all add: field_simps)
eberlm@68246
   525
qed
eberlm@68246
   526
eberlm@68246
   527
eberlm@68246
   528
context landau_pair
eberlm@68246
   529
begin
eberlm@68246
   530
eberlm@68246
   531
lemma big_mono:
eberlm@68246
   532
  "eventually (\<lambda>x. R (norm (f x)) (norm (g x))) F \<Longrightarrow> f \<in> L F (g)"
eberlm@68246
   533
  by (rule bigI[OF zero_less_one]) simp
eberlm@68246
   534
eberlm@68246
   535
lemma big_mult:
eberlm@68246
   536
  assumes "f1 \<in> L F (g1)" "f2 \<in> L F (g2)"
eberlm@68246
   537
  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
eberlm@68246
   538
proof-
eberlm@68246
   539
  from assms(1) guess c1 by (elim bigE) note c1 = this
eberlm@68246
   540
  from assms(2) guess c2 by (elim bigE) note c2 = this
eberlm@68246
   541
  
eberlm@68246
   542
  from c1(1) and c2(1) have "c1 * c2 > 0" by simp
eberlm@68246
   543
  moreover have "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * c2 * norm (g1 x * g2 x))) F"
eberlm@68246
   544
    using c1(2) c2(2)
eberlm@68246
   545
  proof eventually_elim
eberlm@68246
   546
    case (elim x)
eberlm@68246
   547
    show ?case
eberlm@68246
   548
    proof (cases rule: R_E)
eberlm@68246
   549
      case le
eberlm@68246
   550
      have "norm (f1 x) * norm (f2 x) \<le> (c1 * norm (g1 x)) * (c2 * norm (g2 x))"
eberlm@68246
   551
        using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
eberlm@68246
   552
      with le show ?thesis by (simp add: le norm_mult mult_ac)
eberlm@68246
   553
    next
eberlm@68246
   554
      case ge
eberlm@68246
   555
      have "(c1 * norm (g1 x)) * (c2 * norm (g2 x)) \<le> norm (f1 x) * norm (f2 x)"
eberlm@68246
   556
        using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
eberlm@68246
   557
      with ge show ?thesis by (simp_all add: norm_mult mult_ac)
eberlm@68246
   558
    qed
eberlm@68246
   559
  qed
eberlm@68246
   560
  ultimately show ?thesis by (rule bigI)
eberlm@68246
   561
qed
eberlm@68246
   562
eberlm@68246
   563
lemma small_big_mult:
eberlm@68246
   564
  assumes "f1 \<in> l F (g1)" "f2 \<in> L F (g2)"
eberlm@68246
   565
  shows   "(\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"
eberlm@68246
   566
proof (rule smallI)
eberlm@68246
   567
  fix c1 :: real assume c1: "c1 > 0"
eberlm@68246
   568
  from assms(2) guess c2 by (elim bigE) note c2 = this
eberlm@68246
   569
  with c1 assms(1) have "eventually (\<lambda>x. R (norm (f1 x)) (c1 * inverse c2 * norm (g1 x))) F"
eberlm@68246
   570
    by (auto intro!: smallD)
eberlm@68246
   571
  thus "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * norm (g1 x * g2 x))) F" using c2(2)
eberlm@68246
   572
  proof eventually_elim
eberlm@68246
   573
    case (elim x)
eberlm@68246
   574
    show ?case
eberlm@68246
   575
    proof (cases rule: R_E)
eberlm@68246
   576
      case le
eberlm@68246
   577
      have "norm (f1 x) * norm (f2 x) \<le> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
eberlm@68246
   578
        using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
eberlm@68246
   579
      with le c2(1) show ?thesis by (simp add: le norm_mult field_simps)
eberlm@68246
   580
    next
eberlm@68246
   581
      case ge
eberlm@68246
   582
      have "norm (f1 x) * norm (f2 x) \<ge> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
eberlm@68246
   583
        using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
eberlm@68246
   584
      with ge c2(1) show ?thesis by (simp add: ge norm_mult field_simps)
eberlm@68246
   585
    qed
eberlm@68246
   586
  qed
eberlm@68246
   587
qed
eberlm@68246
   588
eberlm@68246
   589
lemma big_small_mult: 
eberlm@68246
   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)"
eberlm@68246
   591
  by (subst (1 2) mult.commute) (rule small_big_mult)
eberlm@68246
   592
eberlm@68246
   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)"
eberlm@68246
   594
  by (rule small_big_mult, assumption, rule small_imp_big)
eberlm@68246
   595
eberlm@68246
   596
lemmas mult = big_mult small_big_mult big_small_mult small_mult
eberlm@68246
   597
eberlm@68246
   598
eberlm@68246
   599
sublocale big: landau_symbol L L' Lr
eberlm@68246
   600
proof
eberlm@68246
   601
  have L: "L = bigo \<or> L = bigomega"
eberlm@68246
   602
    by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
eberlm@68246
   603
  {
eberlm@68246
   604
    fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
eberlm@68246
   605
    hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
eberlm@68246
   606
  } note A = this
eberlm@68246
   607
  {
eberlm@68246
   608
    fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
wenzelm@69272
   609
    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
eberlm@68246
   610
      show "L F (\<lambda>x. c * f x) = L F f" by (intro equalityI big_subsetI) (simp_all add: field_simps)
eberlm@68246
   611
  }
eberlm@68246
   612
  {
eberlm@68246
   613
    fix c :: 'b and F and f g :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
wenzelm@69272
   614
    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
eberlm@68246
   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)
eberlm@68246
   616
    thus "((\<lambda>x. c * f x) \<in> L F g) = (f \<in> L F g)" by (intro iffI) (erule (1) big_trans)+
eberlm@68246
   617
  }
eberlm@68246
   618
  {
eberlm@68246
   619
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> L F (g)"
eberlm@68246
   620
    assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
   621
    from A guess c by (elim bigE) note c = this
eberlm@68246
   622
    from c(2) B have "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
eberlm@68246
   623
      by eventually_elim (rule R_E, insert c(1), simp_all add: field_simps norm_inverse norm_divide)
eberlm@68246
   624
    with c(1) show "(\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))" by (rule bigI)
eberlm@68246
   625
  }
eberlm@68246
   626
  {
eberlm@68246
   627
    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
eberlm@68246
   628
    with plus_aux show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" by (blast intro!: big_subsetI) 
eberlm@68246
   629
  }
eberlm@68246
   630
  {
eberlm@68246
   631
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
eberlm@68246
   632
    show "L F (f) = L F (g)" unfolding L_def
eberlm@68246
   633
      by (subst eventually_subst'[OF A]) (rule refl)
eberlm@68246
   634
  }
eberlm@68246
   635
  {
eberlm@68246
   636
    fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
eberlm@68246
   637
    show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" unfolding L_def mem_Collect_eq
eberlm@68246
   638
      by (subst (1) eventually_subst'[OF A]) (rule refl)
eberlm@68246
   639
  }
eberlm@68246
   640
  {
eberlm@68246
   641
    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" thus "L F f \<subseteq> L F g" by (rule big_subsetI)
eberlm@68246
   642
  }
eberlm@68246
   643
  {
eberlm@68246
   644
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
eberlm@68246
   645
    with A L show "L F (f) = L F (g)" unfolding bigtheta_def
eberlm@68246
   646
      by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo)
eberlm@68246
   647
    fix h:: "'a \<Rightarrow> 'b"
eberlm@68246
   648
    show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" by (rule disjE[OF L]) 
eberlm@68246
   649
      (insert A, auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans)
eberlm@68246
   650
  }
eberlm@68246
   651
  {
eberlm@68246
   652
    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g"
eberlm@68246
   653
    thus "(\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" by (intro big_mult) simp
eberlm@68246
   654
  }
eberlm@68246
   655
  {
eberlm@68246
   656
    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" "g \<in> L F h"
eberlm@68246
   657
    thus "f \<in> L F (h)" by (rule big_trans)
eberlm@68246
   658
  }
eberlm@68246
   659
  {
eberlm@68246
   660
    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
eberlm@68246
   661
    assume "f \<in> L F g" and "filterlim h F G"
eberlm@68246
   662
    thus "(\<lambda>x. f (h x)) \<in> L' G (\<lambda>x. g (h x))" by (auto simp: L_def L'_def filterlim_iff)
eberlm@68246
   663
  }
eberlm@68246
   664
  {
eberlm@68246
   665
    fix f g :: "'a \<Rightarrow> 'b" and F G :: "'a filter"
eberlm@68246
   666
    assume "f \<in> L F g" "f \<in> L G g"
eberlm@68246
   667
    from this [THEN bigE] guess c1 c2 . note c12 = this
eberlm@68246
   668
    define c where "c = (if R c1 c2 then c2 else c1)"
eberlm@68246
   669
    from c12 have c: "R c1 c" "R c2 c" "c > 0" by (auto simp: c_def dest: R_linear)
eberlm@68246
   670
    with c12(2,4) have "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
eberlm@68246
   671
                     "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) G"
eberlm@68246
   672
      by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+
eberlm@68246
   673
    with c show "f \<in> L (sup F G) g" by (auto simp: L_def eventually_sup)
eberlm@68246
   674
  }
eberlm@68246
   675
  {
eberlm@68246
   676
    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
eberlm@68246
   677
    assume "(f \<in> L F g)"
eberlm@68246
   678
    thus "((\<lambda>x. f (h x)) \<in> L' (filtercomap h F) (\<lambda>x. g (h x)))"
eberlm@68246
   679
      unfolding L_def L'_def by auto
eberlm@68246
   680
  }
eberlm@68246
   681
qed (auto simp: L_def Lr_def eventually_filtermap L'_def
eberlm@68246
   682
          intro: filter_leD exI[of _ "1::real"])
eberlm@68246
   683
eberlm@68246
   684
sublocale small: landau_symbol l l' lr
eberlm@68246
   685
proof
eberlm@68246
   686
  {
eberlm@68246
   687
    fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
eberlm@68246
   688
    hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
eberlm@68246
   689
  } note A = this
eberlm@68246
   690
  {
eberlm@68246
   691
    fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
wenzelm@69272
   692
    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
eberlm@68246
   693
      show "l F (\<lambda>x. c * f x) = l F f" 
eberlm@68246
   694
        by (intro equalityI small_subsetI) (simp_all add: field_simps)
eberlm@68246
   695
  }
eberlm@68246
   696
  {
eberlm@68246
   697
    fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
wenzelm@69272
   698
    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
eberlm@68246
   699
      have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
eberlm@68246
   700
    thus "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" by (intro iffI) (erule (1) big_small_trans)+
eberlm@68246
   701
  }
eberlm@68246
   702
  {
eberlm@68246
   703
    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
eberlm@68246
   704
    with plus_aux show "l F g \<subseteq> l F (\<lambda>x. f x + g x)" by (blast intro!: small_subsetI) 
eberlm@68246
   705
  }
eberlm@68246
   706
  {
eberlm@68246
   707
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> l F (g)"
eberlm@68246
   708
    assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
   709
    show "(\<lambda>x. inverse (g x)) \<in> l F (\<lambda>x. inverse (f x))"
eberlm@68246
   710
    proof (rule smallI)
eberlm@68246
   711
      fix c :: real assume c: "c > 0"
eberlm@68246
   712
      from B smallD[OF A c] 
eberlm@68246
   713
        show "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
eberlm@68246
   714
        by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide)
eberlm@68246
   715
    qed
eberlm@68246
   716
  }
eberlm@68246
   717
  {
eberlm@68246
   718
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
eberlm@68246
   719
    show "l F (f) = l F (g)" unfolding l_def by (subst eventually_subst'[OF A]) (rule refl)
eberlm@68246
   720
  }
eberlm@68246
   721
  {
eberlm@68246
   722
    fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
eberlm@68246
   723
    show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" unfolding l_def mem_Collect_eq
eberlm@68246
   724
      by (subst (1) eventually_subst'[OF A]) (rule refl)
eberlm@68246
   725
  }
eberlm@68246
   726
  {
eberlm@68246
   727
    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" 
eberlm@68246
   728
    thus "l F f \<subseteq> l F g" by (intro small_subsetI small_imp_big)
eberlm@68246
   729
  }
eberlm@68246
   730
  {
eberlm@68246
   731
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
eberlm@68246
   732
    have L: "L = bigo \<or> L = bigomega"
eberlm@68246
   733
      by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
eberlm@68246
   734
    with A show "l F (f) = l F (g)" unfolding bigtheta_def
eberlm@68246
   735
      by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo)
eberlm@68246
   736
    have l: "l = smallo \<or> l = smallomega"
eberlm@68246
   737
      by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff)
eberlm@68246
   738
    fix h:: "'a \<Rightarrow> 'b"
eberlm@68246
   739
    show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" by (rule disjE[OF l]) 
eberlm@68246
   740
      (insert A, auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo 
eberlm@68246
   741
       intro: landau_o.big_small_trans landau_o.small_big_trans)
eberlm@68246
   742
  }
eberlm@68246
   743
  {
eberlm@68246
   744
    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g"
eberlm@68246
   745
    thus "(\<lambda>x. h x * f x) \<in> l F (\<lambda>x. h x * g x)" by (intro big_small_mult) simp
eberlm@68246
   746
  }
eberlm@68246
   747
  {
eberlm@68246
   748
    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" "g \<in> l F h"
eberlm@68246
   749
    thus "f \<in> l F (h)" by (rule small_trans)
eberlm@68246
   750
  }
eberlm@68246
   751
  {
eberlm@68246
   752
    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
eberlm@68246
   753
    assume "f \<in> l F g" and "filterlim h F G"
eberlm@68246
   754
    thus "(\<lambda>x. f (h x)) \<in> l' G (\<lambda>x. g (h x))"
eberlm@68246
   755
      by (auto simp: l_def l'_def filterlim_iff)
eberlm@68246
   756
  }
eberlm@68246
   757
  {
eberlm@68246
   758
    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
eberlm@68246
   759
    assume "(f \<in> l F g)"
eberlm@68246
   760
    thus "((\<lambda>x. f (h x)) \<in> l' (filtercomap h F) (\<lambda>x. g (h x)))"
eberlm@68246
   761
      unfolding l_def l'_def by auto
eberlm@68246
   762
  }
eberlm@68246
   763
qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)
eberlm@68246
   764
eberlm@68246
   765
wenzelm@69272
   766
text \<open>These rules allow chaining of Landau symbol propositions in Isar with "also".\<close>
eberlm@68246
   767
eberlm@68246
   768
lemma big_mult_1:    "f \<in> L F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
eberlm@68246
   769
  and big_mult_1':   "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
eberlm@68246
   770
  and small_mult_1:  "f \<in> l F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
eberlm@68246
   771
  and small_mult_1': "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> l F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
eberlm@68246
   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)"
eberlm@68246
   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)"
eberlm@68246
   774
  by (drule (1) big.mult big_small_mult small_big_mult, simp)+
eberlm@68246
   775
eberlm@68246
   776
lemma big_1_mult:    "f \<in> L F (g) \<Longrightarrow> h \<in> L F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
eberlm@68246
   777
  and big_1_mult':   "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
eberlm@68246
   778
  and small_1_mult:  "f \<in> l F (g) \<Longrightarrow> h \<in> L F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"
eberlm@68246
   779
  and small_1_mult': "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> l F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"
eberlm@68246
   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)"
eberlm@68246
   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)"
eberlm@68246
   782
  by (drule (1) big.mult big_small_mult small_big_mult, simp)+
eberlm@68246
   783
eberlm@68246
   784
lemmas mult_1_trans = 
eberlm@68246
   785
  big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1'''
eberlm@68246
   786
  big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult'''
eberlm@68246
   787
eberlm@68246
   788
lemma big_equal_iff_bigtheta: "L F (f) = L F (g) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
eberlm@68246
   789
proof
eberlm@68246
   790
  have L: "L = bigo \<or> L = bigomega"
eberlm@68246
   791
    by (rule R_E) (auto simp: fun_eq_iff L_def bigo_def bigomega_def)
eberlm@68246
   792
  fix f g :: "'a \<Rightarrow> 'b" assume "L F (f) = L F (g)"
eberlm@68246
   793
  with big_refl[of f F] big_refl[of g F] have "f \<in> L F (g)" "g \<in> L F (f)" by simp_all
eberlm@68246
   794
  thus "f \<in> \<Theta>[F](g)" using L unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
eberlm@68246
   795
qed (rule big.cong_bigtheta)
eberlm@68246
   796
eberlm@68246
   797
lemma big_prod:
eberlm@68246
   798
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (g x)"
eberlm@68246
   799
  shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>y. \<Prod>x\<in>A. g x y)"
eberlm@68246
   800
  using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult)
eberlm@68246
   801
eberlm@68246
   802
lemma big_prod_in_1:
eberlm@68246
   803
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (\<lambda>_. 1)"
eberlm@68246
   804
  shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>_. 1)"
eberlm@68246
   805
  using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult_in_1)
eberlm@68246
   806
eberlm@68246
   807
end
eberlm@68246
   808
eberlm@68246
   809
eberlm@68246
   810
context landau_symbol
eberlm@68246
   811
begin
eberlm@68246
   812
  
eberlm@68246
   813
lemma plus_absorb1:
eberlm@68246
   814
  assumes "f \<in> o[F](g)"
eberlm@68246
   815
  shows   "L F (\<lambda>x. f x + g x) = L F (g)"
eberlm@68246
   816
proof (intro equalityI)
eberlm@68246
   817
  from plus_subset1 and assms show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" .
eberlm@68246
   818
  from landau_o.small.plus_subset1[OF assms] and assms have "(\<lambda>x. -f x) \<in> o[F](\<lambda>x. f x + g x)"
eberlm@68246
   819
    by (auto simp: landau_o.small.uminus_in_iff)
eberlm@68246
   820
  from plus_subset1[OF this] show "L F (\<lambda>x. f x + g x) \<subseteq> L F (g)" by simp
eberlm@68246
   821
qed
eberlm@68246
   822
eberlm@68246
   823
lemma plus_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x + g x) = L F (f)"
eberlm@68246
   824
  using plus_absorb1[of g F f] by (simp add: add.commute)
eberlm@68246
   825
eberlm@68246
   826
lemma diff_absorb1: "f \<in> o[F](g) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (g)"
eberlm@68246
   827
  by (simp only: diff_conv_add_uminus plus_absorb1 landau_o.small.uminus uminus)
eberlm@68246
   828
eberlm@68246
   829
lemma diff_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (f)"
eberlm@68246
   830
  by (simp only: diff_conv_add_uminus plus_absorb2 landau_o.small.uminus_in_iff)
eberlm@68246
   831
eberlm@68246
   832
lemmas absorb = plus_absorb1 plus_absorb2 diff_absorb1 diff_absorb2
eberlm@68246
   833
eberlm@68246
   834
end
eberlm@68246
   835
eberlm@68246
   836
eberlm@68246
   837
lemma bigthetaI [intro]: "f \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> \<Theta>[F](g)"
eberlm@68246
   838
  unfolding bigtheta_def bigomega_def by blast
eberlm@68246
   839
eberlm@68246
   840
lemma bigthetaD1 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> O[F](g)" 
eberlm@68246
   841
  and bigthetaD2 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g)"
eberlm@68246
   842
  unfolding bigtheta_def bigo_def bigomega_def by blast+
eberlm@68246
   843
eberlm@68246
   844
lemma bigtheta_refl [simp]: "f \<in> \<Theta>[F](f)"
eberlm@68246
   845
  unfolding bigtheta_def by simp
eberlm@68246
   846
eberlm@68246
   847
lemma bigtheta_sym: "f \<in> \<Theta>[F](g) \<longleftrightarrow> g \<in> \<Theta>[F](f)"
eberlm@68246
   848
  unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
eberlm@68246
   849
eberlm@68246
   850
lemmas landau_flip =
eberlm@68246
   851
  bigomega_iff_bigo[symmetric] smallomega_iff_smallo[symmetric]
eberlm@68246
   852
  bigomega_iff_bigo smallomega_iff_smallo bigtheta_sym
eberlm@68246
   853
eberlm@68246
   854
eberlm@68246
   855
interpretation landau_theta: landau_symbol bigtheta bigtheta bigtheta
eberlm@68246
   856
proof
eberlm@68246
   857
  fix f g :: "'a \<Rightarrow> 'b" and F
eberlm@68246
   858
  assume "f \<in> o[F](g)"
eberlm@68246
   859
  hence "O[F](g) \<subseteq> O[F](\<lambda>x. f x + g x)" "\<Omega>[F](g) \<subseteq> \<Omega>[F](\<lambda>x. f x + g x)"
eberlm@68246
   860
    by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+
eberlm@68246
   861
  thus "\<Theta>[F](g) \<subseteq> \<Theta>[F](\<lambda>x. f x + g x)" unfolding bigtheta_def by blast
eberlm@68246
   862
next
eberlm@68246
   863
  fix f g :: "'a \<Rightarrow> 'b" and F 
eberlm@68246
   864
  assume "f \<in> \<Theta>[F](g)"
eberlm@68246
   865
  thus A: "\<Theta>[F](f) = \<Theta>[F](g)" 
eberlm@68246
   866
    apply (subst (1 2) bigtheta_def)
eberlm@68246
   867
    apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+
eberlm@68246
   868
    apply (rule refl)
eberlm@68246
   869
    done
eberlm@68246
   870
  thus "\<Theta>[F](f) \<subseteq> \<Theta>[F](g)" by simp
eberlm@68246
   871
  fix h :: "'a \<Rightarrow> 'b"
eberlm@68246
   872
  show "f \<in> \<Theta>[F](h) \<longleftrightarrow> g \<in> \<Theta>[F](h)" by (subst (1 2) bigtheta_sym) (simp add: A)
eberlm@68246
   873
next
eberlm@68246
   874
  fix f g h :: "'a \<Rightarrow> 'b" and F
eberlm@68246
   875
  assume "f \<in> \<Theta>[F](g)" "g \<in> \<Theta>[F](h)"
eberlm@68246
   876
  thus "f \<in> \<Theta>[F](h)" unfolding bigtheta_def
eberlm@68246
   877
    by (blast intro: landau_o.big.trans landau_omega.big.trans)
eberlm@68246
   878
next
eberlm@68246
   879
  fix f :: "'a \<Rightarrow> 'b" and F1 F2 :: "'a filter"
eberlm@68246
   880
  assume "F1 \<le> F2"
eberlm@68246
   881
  thus "\<Theta>[F2](f) \<subseteq> \<Theta>[F1](f)"
eberlm@68246
   882
    by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono)
eberlm@68246
   883
qed (auto simp: bigtheta_def landau_o.big.norm_iff 
eberlm@68246
   884
                landau_o.big.cmult landau_omega.big.cmult 
eberlm@68246
   885
                landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff 
eberlm@68246
   886
                landau_o.big.in_cong landau_omega.big.in_cong
eberlm@68246
   887
                landau_o.big.mult landau_omega.big.mult
eberlm@68246
   888
                landau_o.big.inverse landau_omega.big.inverse 
eberlm@68246
   889
                landau_o.big.compose landau_omega.big.compose
eberlm@68246
   890
                landau_o.big.bot' landau_omega.big.bot'
eberlm@68246
   891
                landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff
eberlm@68246
   892
                landau_o.big.sup landau_omega.big.sup
eberlm@68246
   893
                landau_o.big.filtercomap landau_omega.big.filtercomap
eberlm@68246
   894
          dest: landau_o.big.cong landau_omega.big.cong)
eberlm@68246
   895
eberlm@68246
   896
lemmas landau_symbols = 
eberlm@68246
   897
  landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms
eberlm@68246
   898
  landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms 
eberlm@68246
   899
  landau_theta.landau_symbol_axioms
eberlm@68246
   900
eberlm@68246
   901
lemma bigoI [intro]:
eberlm@68246
   902
  assumes "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
eberlm@68246
   903
  shows   "f \<in> O[F](g)"
eberlm@68246
   904
proof (rule landau_o.bigI)
eberlm@68246
   905
  show "max 1 c > 0" by simp
eberlm@68246
   906
  note assms
eberlm@68246
   907
  moreover have "\<And>x. c * (norm (g x)) \<le> max 1 c * (norm (g x))" by (simp add: mult_right_mono)
eberlm@68246
   908
  ultimately show "eventually (\<lambda>x. (norm (f x)) \<le> max 1 c * (norm (g x))) F"
eberlm@68246
   909
    by (auto elim!: eventually_mono dest: order.trans)
eberlm@68246
   910
qed
eberlm@68246
   911
eberlm@68246
   912
lemma smallomegaD [dest]:
eberlm@68246
   913
  assumes "f \<in> \<omega>[F](g)"
eberlm@68246
   914
  shows   "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
eberlm@68246
   915
proof (cases "c > 0")
eberlm@68246
   916
  case False
eberlm@68246
   917
  show ?thesis 
eberlm@68246
   918
    by (intro always_eventually allI, rule order.trans[of _ 0])
eberlm@68246
   919
       (insert False, auto intro!: mult_nonpos_nonneg)
eberlm@68246
   920
qed (blast dest: landau_omega.smallD[OF assms, of c])
eberlm@68246
   921
eberlm@68246
   922
  
eberlm@68246
   923
lemma bigthetaI':
eberlm@68246
   924
  assumes "c1 > 0" "c2 > 0"
eberlm@68246
   925
  assumes "eventually (\<lambda>x. c1 * (norm (g x)) \<le> (norm (f x)) \<and> (norm (f x)) \<le> c2 * (norm (g x))) F"
eberlm@68246
   926
  shows   "f \<in> \<Theta>[F](g)"
eberlm@68246
   927
apply (rule bigthetaI)
eberlm@68246
   928
apply (rule landau_o.bigI[OF assms(2)]) using assms(3) apply (eventually_elim, simp)
eberlm@68246
   929
apply (rule landau_omega.bigI[OF assms(1)]) using assms(3) apply (eventually_elim, simp)
eberlm@68246
   930
done
eberlm@68246
   931
eberlm@68246
   932
lemma bigthetaI_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> \<Theta>[F](g)"
eberlm@68246
   933
  by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono)
eberlm@68246
   934
eberlm@68246
   935
lemma (in landau_symbol) ev_eq_trans1: 
eberlm@68246
   936
  "f \<in> L F (\<lambda>x. g x (h x)) \<Longrightarrow> eventually (\<lambda>x. h x = h' x) F \<Longrightarrow> f \<in> L F (\<lambda>x. g x (h' x))"
eberlm@68246
   937
  by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono)
eberlm@68246
   938
eberlm@68246
   939
lemma (in landau_symbol) ev_eq_trans2: 
eberlm@68246
   940
  "eventually (\<lambda>x. f x = f' x) F \<Longrightarrow> (\<lambda>x. g x (f' x)) \<in> L F (h) \<Longrightarrow> (\<lambda>x. g x (f x)) \<in> L F (h)"
eberlm@68246
   941
  by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono)
eberlm@68246
   942
eberlm@68246
   943
declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro]
eberlm@68246
   944
declare landau_o.bigE landau_omega.bigE [elim]
eberlm@68246
   945
declare landau_o.smallD
eberlm@68246
   946
eberlm@68246
   947
lemma (in landau_symbol) bigtheta_trans1': 
eberlm@68246
   948
  "f \<in> L F (g) \<Longrightarrow> h \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h)"
eberlm@68246
   949
  by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym)
eberlm@68246
   950
eberlm@68246
   951
lemma (in landau_symbol) bigtheta_trans2': 
eberlm@68246
   952
  "g \<in> \<Theta>[F](f) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
eberlm@68246
   953
  by (rule bigtheta_trans2, subst bigtheta_sym)
eberlm@68246
   954
eberlm@68246
   955
lemma bigo_bigomega_trans:      "f \<in> O[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> O[F](h)"
eberlm@68246
   956
  and bigo_smallomega_trans:    "f \<in> O[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
eberlm@68246
   957
  and smallo_bigomega_trans:    "f \<in> o[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
eberlm@68246
   958
  and smallo_smallomega_trans:  "f \<in> o[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
eberlm@68246
   959
  and bigomega_bigo_trans:      "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](h)"
eberlm@68246
   960
  and bigomega_smallo_trans:    "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
eberlm@68246
   961
  and smallomega_bigo_trans:    "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
eberlm@68246
   962
  and smallomega_smallo_trans:  "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
eberlm@68246
   963
  by (unfold bigomega_iff_bigo smallomega_iff_smallo)
eberlm@68246
   964
     (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans 
eberlm@68246
   965
                landau_o.big_trans landau_o.small_trans)+
eberlm@68246
   966
eberlm@68246
   967
lemmas landau_trans_lift [trans] =
eberlm@68246
   968
  landau_symbols[THEN landau_symbol.lift_trans]
eberlm@68246
   969
  landau_symbols[THEN landau_symbol.lift_trans']
eberlm@68246
   970
  landau_symbols[THEN landau_symbol.lift_trans_bigtheta]
eberlm@68246
   971
  landau_symbols[THEN landau_symbol.lift_trans_bigtheta']
eberlm@68246
   972
eberlm@68246
   973
lemmas landau_mult_1_trans [trans] =
eberlm@68246
   974
  landau_o.mult_1_trans landau_omega.mult_1_trans
eberlm@68246
   975
eberlm@68246
   976
lemmas landau_trans [trans] = 
eberlm@68246
   977
  landau_symbols[THEN landau_symbol.bigtheta_trans1]
eberlm@68246
   978
  landau_symbols[THEN landau_symbol.bigtheta_trans2]
eberlm@68246
   979
  landau_symbols[THEN landau_symbol.bigtheta_trans1']
eberlm@68246
   980
  landau_symbols[THEN landau_symbol.bigtheta_trans2']
eberlm@68246
   981
  landau_symbols[THEN landau_symbol.ev_eq_trans1]
eberlm@68246
   982
  landau_symbols[THEN landau_symbol.ev_eq_trans2]
eberlm@68246
   983
eberlm@68246
   984
  landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans
eberlm@68246
   985
  landau_omega.big_trans landau_omega.small_trans 
eberlm@68246
   986
    landau_omega.small_big_trans landau_omega.big_small_trans
eberlm@68246
   987
eberlm@68246
   988
  bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans 
eberlm@68246
   989
  bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans
eberlm@68246
   990
eberlm@68246
   991
lemma bigtheta_inverse [simp]: 
eberlm@68246
   992
  shows "(\<lambda>x. inverse (f x)) \<in> \<Theta>[F](\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
eberlm@68246
   993
proof-
eberlm@68246
   994
  {
eberlm@68246
   995
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
eberlm@68246
   996
    then guess c1 c2 :: real unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
eberlm@68246
   997
    note c = this
eberlm@68246
   998
    from c(3) have "inverse c2 > 0" by simp
eberlm@68246
   999
    moreover from c(2,4)
eberlm@68246
  1000
      have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))) F"
eberlm@68246
  1001
    proof eventually_elim
eberlm@68246
  1002
      fix x assume A: "(norm (f x)) \<le> c1 * (norm (g x))" "c2 * (norm (g x)) \<le> (norm (f x))"
eberlm@68246
  1003
      from A c(1,3) have "f x = 0 \<longleftrightarrow> g x = 0" by (auto simp: field_simps mult_le_0_iff)
eberlm@68246
  1004
      with A c(1,3) show "norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))"
eberlm@68246
  1005
        by (force simp: field_simps norm_inverse norm_divide)
eberlm@68246
  1006
    qed
eberlm@68246
  1007
    ultimately have "(\<lambda>x. inverse (f x)) \<in> O[F](\<lambda>x. inverse (g x))" by (rule landau_o.bigI)
eberlm@68246
  1008
  }
eberlm@68246
  1009
  thus ?thesis unfolding bigtheta_def 
eberlm@68246
  1010
    by (force simp: bigomega_iff_bigo bigtheta_sym)
eberlm@68246
  1011
qed
eberlm@68246
  1012
eberlm@68246
  1013
lemma bigtheta_divide:
eberlm@68246
  1014
  assumes "f1 \<in> \<Theta>(f2)" "g1 \<in> \<Theta>(g2)"
eberlm@68246
  1015
  shows   "(\<lambda>x. f1 x / g1 x) \<in> \<Theta>(\<lambda>x. f2 x / g2 x)"
eberlm@68246
  1016
  by (subst (1 2) divide_inverse, intro landau_theta.mult) (simp_all add: bigtheta_inverse assms)
eberlm@68246
  1017
eberlm@68246
  1018
lemma eventually_nonzero_bigtheta:
eberlm@68246
  1019
  assumes "f \<in> \<Theta>[F](g)"
eberlm@68246
  1020
  shows   "eventually (\<lambda>x. f x \<noteq> 0) F \<longleftrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1021
proof-
eberlm@68246
  1022
  {
eberlm@68246
  1023
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)" and B: "eventually (\<lambda>x. f x \<noteq> 0) F"
eberlm@68246
  1024
    from A guess c1 c2 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
eberlm@68246
  1025
    from B this(2,4) have "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim auto
eberlm@68246
  1026
  }
eberlm@68246
  1027
  with assms show ?thesis by (force simp: bigtheta_sym)
eberlm@68246
  1028
qed
eberlm@68246
  1029
eberlm@68246
  1030
wenzelm@69272
  1031
subsection \<open>Landau symbols and limits\<close>
eberlm@68246
  1032
eberlm@68246
  1033
lemma bigoI_tendsto_norm:
eberlm@68246
  1034
  fixes f g
eberlm@68246
  1035
  assumes "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
eberlm@68246
  1036
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1037
  shows   "f \<in> O[F](g)"
eberlm@68246
  1038
proof (rule bigoI)
eberlm@68246
  1039
  from assms have "eventually (\<lambda>x. dist (norm (f x / g x)) c < 1) F" 
eberlm@68246
  1040
    using tendstoD by force
eberlm@68246
  1041
  thus "eventually (\<lambda>x. (norm (f x)) \<le> (norm c + 1) * (norm (g x))) F"
eberlm@68246
  1042
    unfolding dist_real_def using assms(2)
eberlm@68246
  1043
  proof eventually_elim
eberlm@68246
  1044
    case (elim x)
eberlm@68246
  1045
    have "(norm (f x)) - norm c * (norm (g x)) \<le> norm ((norm (f x)) - c * (norm (g x)))"
eberlm@68246
  1046
      unfolding norm_mult [symmetric] using norm_triangle_ineq2[of "norm (f x)" "c * norm (g x)"]
eberlm@68246
  1047
      by (simp add: norm_mult abs_mult)
eberlm@68246
  1048
    also from elim have "\<dots> = norm (norm (g x)) * norm (norm (f x / g x) - c)"
eberlm@68246
  1049
      unfolding norm_mult [symmetric] by (simp add: algebra_simps norm_divide)
eberlm@68246
  1050
    also from elim have "norm (norm (f x / g x) - c) \<le> 1" by simp
eberlm@68246
  1051
    hence "norm (norm (g x)) * norm (norm (f x / g x) - c) \<le> norm (norm (g x)) * 1" 
eberlm@68246
  1052
      by (rule mult_left_mono) simp_all
eberlm@68246
  1053
    finally show ?case by (simp add: algebra_simps)
eberlm@68246
  1054
  qed
eberlm@68246
  1055
qed
eberlm@68246
  1056
eberlm@68246
  1057
lemma bigoI_tendsto:
eberlm@68246
  1058
  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
eberlm@68246
  1059
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1060
  shows   "f \<in> O[F](g)"
eberlm@68246
  1061
  using assms by (rule bigoI_tendsto_norm[OF tendsto_norm])
eberlm@68246
  1062
eberlm@68246
  1063
lemma bigomegaI_tendsto_norm:
eberlm@68246
  1064
  assumes c_not_0:  "(c::real) \<noteq> 0"
eberlm@68246
  1065
  assumes lim:      "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
eberlm@68246
  1066
  shows   "f \<in> \<Omega>[F](g)"
eberlm@68246
  1067
proof (cases "F = bot")
eberlm@68246
  1068
  case False
eberlm@68246
  1069
  show ?thesis
eberlm@68246
  1070
  proof (rule landau_omega.bigI)
eberlm@68246
  1071
    from lim  have "c \<ge> 0" by (rule tendsto_lowerbound) (insert False, simp_all)
eberlm@68246
  1072
    with c_not_0 have "c > 0" by simp
eberlm@68246
  1073
    with c_not_0 show "c/2 > 0" by simp
eberlm@68246
  1074
    from lim have ev: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<epsilon>) F"
eberlm@68246
  1075
      by (subst (asm) tendsto_iff) (simp add: dist_real_def)
wenzelm@69272
  1076
    from ev[OF \<open>c/2 > 0\<close>] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
eberlm@68246
  1077
    proof (eventually_elim)
eberlm@68246
  1078
      fix x assume B: "norm (norm (f x / g x) - c) < c / 2"
eberlm@68246
  1079
      from B have g: "g x \<noteq> 0" by auto
eberlm@68246
  1080
      from B have "-c/2 < -norm (norm (f x / g x) - c)" by simp
eberlm@68246
  1081
      also have "... \<le> norm (f x / g x) - c" by simp
eberlm@68246
  1082
      finally show "(norm (f x)) \<ge> c/2 * (norm (g x))" using g 
eberlm@68246
  1083
        by (simp add: field_simps norm_mult norm_divide)
eberlm@68246
  1084
    qed
eberlm@68246
  1085
  qed
eberlm@68246
  1086
qed simp
eberlm@68246
  1087
eberlm@68246
  1088
lemma bigomegaI_tendsto:
eberlm@68246
  1089
  assumes c_not_0:  "(c::real) \<noteq> 0"
eberlm@68246
  1090
  assumes lim:      "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
eberlm@68246
  1091
  shows   "f \<in> \<Omega>[F](g)"
eberlm@68246
  1092
  by (rule bigomegaI_tendsto_norm[OF _ tendsto_norm, of c]) (insert assms, simp_all)
eberlm@68246
  1093
eberlm@68246
  1094
lemma smallomegaI_filterlim_at_top_norm:
eberlm@68246
  1095
  assumes lim: "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
eberlm@68246
  1096
  shows   "f \<in> \<omega>[F](g)"
eberlm@68246
  1097
proof (rule landau_omega.smallI)
eberlm@68246
  1098
  fix c :: real assume c_pos: "c > 0"
eberlm@68246
  1099
  from lim have ev: "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F"
eberlm@68246
  1100
    by (subst (asm) filterlim_at_top) simp
eberlm@68246
  1101
  thus "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
eberlm@68246
  1102
  proof eventually_elim
eberlm@68246
  1103
    fix x assume A: "norm (f x / g x) \<ge> c"
eberlm@68246
  1104
    from A c_pos have "g x \<noteq> 0" by auto
eberlm@68246
  1105
    with A show "(norm (f x)) \<ge> c * (norm (g x))" by (simp add: field_simps norm_divide)
eberlm@68246
  1106
  qed
eberlm@68246
  1107
qed
eberlm@68246
  1108
eberlm@68246
  1109
lemma smallomegaI_filterlim_at_infinity:
eberlm@68246
  1110
  assumes lim: "filterlim (\<lambda>x. f x / g x) at_infinity F"
eberlm@68246
  1111
  shows   "f \<in> \<omega>[F](g)"
eberlm@68246
  1112
proof (rule smallomegaI_filterlim_at_top_norm)
eberlm@68246
  1113
  from lim show "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
eberlm@68246
  1114
    by (rule filterlim_at_infinity_imp_norm_at_top)
eberlm@68246
  1115
qed
eberlm@68246
  1116
  
eberlm@68246
  1117
lemma smallomegaD_filterlim_at_top_norm:
eberlm@68246
  1118
  assumes "f \<in> \<omega>[F](g)"
eberlm@68246
  1119
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1120
  shows   "LIM x F. norm (f x / g x) :> at_top"
eberlm@68246
  1121
proof (subst filterlim_at_top_gt, clarify)
eberlm@68246
  1122
  fix c :: real assume c: "c > 0"
eberlm@68246
  1123
  from landau_omega.smallD[OF assms(1) this] assms(2) 
eberlm@68246
  1124
    show "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F" 
eberlm@68246
  1125
    by eventually_elim (simp add: field_simps norm_divide)
eberlm@68246
  1126
qed
eberlm@68246
  1127
  
eberlm@68246
  1128
lemma smallomegaD_filterlim_at_infinity:
eberlm@68246
  1129
  assumes "f \<in> \<omega>[F](g)"
eberlm@68246
  1130
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1131
  shows   "LIM x F. f x / g x :> at_infinity"
eberlm@68246
  1132
  using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm)
eberlm@68246
  1133
eberlm@68246
  1134
lemma smallomega_1_conv_filterlim: "f \<in> \<omega>[F](\<lambda>_. 1) \<longleftrightarrow> filterlim f at_infinity F"
eberlm@68246
  1135
  by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)
eberlm@68246
  1136
eberlm@68246
  1137
lemma smalloI_tendsto:
eberlm@68246
  1138
  assumes lim: "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
eberlm@68246
  1139
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1140
  shows   "f \<in> o[F](g)"
eberlm@68246
  1141
proof (rule landau_o.smallI)
eberlm@68246
  1142
  fix c :: real assume c_pos: "c > 0"
eberlm@68246
  1143
  from c_pos and lim have ev: "eventually (\<lambda>x. norm (f x / g x) < c) F"
eberlm@68246
  1144
    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
eberlm@68246
  1145
  with assms(2) show "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
eberlm@68246
  1146
    by eventually_elim (simp add: field_simps norm_divide)
eberlm@68246
  1147
qed
eberlm@68246
  1148
eberlm@68246
  1149
lemma smalloD_tendsto:
eberlm@68246
  1150
  assumes "f \<in> o[F](g)"
eberlm@68246
  1151
  shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
eberlm@68246
  1152
unfolding tendsto_iff
eberlm@68246
  1153
proof clarify
eberlm@68246
  1154
  fix e :: real assume e: "e > 0"
eberlm@68246
  1155
  hence "e/2 > 0" by simp
eberlm@68246
  1156
  from landau_o.smallD[OF assms this] show "eventually (\<lambda>x. dist (f x / g x) 0 < e) F"
eberlm@68246
  1157
  proof eventually_elim
eberlm@68246
  1158
    fix x assume "(norm (f x)) \<le> e/2 * (norm (g x))"
eberlm@68246
  1159
    with e have "dist (f x / g x) 0 \<le> e/2"
eberlm@68246
  1160
      by (cases "g x = 0") (simp_all add: dist_real_def norm_divide field_simps)
eberlm@68246
  1161
    also from e have "... < e" by simp
eberlm@68246
  1162
    finally show "dist (f x / g x) 0 < e" by simp
eberlm@68246
  1163
  qed
eberlm@68246
  1164
qed
eberlm@68246
  1165
eberlm@68246
  1166
lemma bigthetaI_tendsto_norm:
eberlm@68246
  1167
  assumes c_not_0: "(c::real) \<noteq> 0"
eberlm@68246
  1168
  assumes lim:     "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
eberlm@68246
  1169
  shows   "f \<in> \<Theta>[F](g)"
eberlm@68246
  1170
proof (rule bigthetaI)
eberlm@68246
  1171
  from c_not_0 have "\<bar>c\<bar> > 0" by simp
eberlm@68246
  1172
  with lim have "eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<bar>c\<bar>) F"
eberlm@68246
  1173
    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
eberlm@68246
  1174
  hence g: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim (auto simp add: field_simps)
eberlm@68246
  1175
eberlm@68246
  1176
  from lim g show "f \<in> O[F](g)" by (rule bigoI_tendsto_norm)
eberlm@68246
  1177
  from c_not_0 and lim show "f \<in> \<Omega>[F](g)" by (rule bigomegaI_tendsto_norm)
eberlm@68246
  1178
qed
eberlm@68246
  1179
eberlm@68246
  1180
lemma bigthetaI_tendsto:
eberlm@68246
  1181
  assumes c_not_0: "(c::real) \<noteq> 0"
eberlm@68246
  1182
  assumes lim:     "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
eberlm@68246
  1183
  shows   "f \<in> \<Theta>[F](g)"
eberlm@68246
  1184
  using assms by (intro bigthetaI_tendsto_norm[OF _ tendsto_norm, of "c"]) simp_all
eberlm@68246
  1185
eberlm@68246
  1186
lemma tendsto_add_smallo:
eberlm@68246
  1187
  assumes "(f1 \<longlongrightarrow> a) F"
eberlm@68246
  1188
  assumes "f2 \<in> o[F](f1)"
eberlm@68246
  1189
  shows   "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1190
proof (subst filterlim_cong[OF refl refl])
eberlm@68246
  1191
  from landau_o.smallD[OF assms(2) zero_less_one] 
eberlm@68246
  1192
    have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)) F" by simp
eberlm@68246
  1193
  thus "eventually (\<lambda>x. f1 x + f2 x = f1 x * (1 + f2 x / f1 x)) F"
eberlm@68246
  1194
    by eventually_elim (auto simp: field_simps)
eberlm@68246
  1195
next
eberlm@68246
  1196
  from assms(1) show "((\<lambda>x. f1 x * (1 + f2 x / f1 x)) \<longlongrightarrow> a) F"
eberlm@68246
  1197
    by (force intro: tendsto_eq_intros smalloD_tendsto[OF assms(2)])
eberlm@68246
  1198
qed
eberlm@68246
  1199
eberlm@68246
  1200
lemma tendsto_diff_smallo:
eberlm@68246
  1201
  shows "(f1 \<longlongrightarrow> a) F \<Longrightarrow> f2 \<in> o[F](f1) \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1202
  using tendsto_add_smallo[of f1 a F "\<lambda>x. -f2 x"] by simp
eberlm@68246
  1203
eberlm@68246
  1204
lemma tendsto_add_smallo_iff:
eberlm@68246
  1205
  assumes "f2 \<in> o[F](f1)"
eberlm@68246
  1206
  shows   "(f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1207
proof
eberlm@68246
  1208
  assume "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1209
  hence "((\<lambda>x. f1 x + f2 x - f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1210
    by (rule tendsto_diff_smallo) (simp add: landau_o.small.plus_absorb2 assms)
eberlm@68246
  1211
  thus "(f1 \<longlongrightarrow> a) F" by simp
eberlm@68246
  1212
qed (rule tendsto_add_smallo[OF _ assms])
eberlm@68246
  1213
eberlm@68246
  1214
lemma tendsto_diff_smallo_iff:
eberlm@68246
  1215
  shows "f2 \<in> o[F](f1) \<Longrightarrow> (f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1216
  using tendsto_add_smallo_iff[of "\<lambda>x. -f2 x" F f1 a] by simp
eberlm@68246
  1217
eberlm@68246
  1218
lemma tendsto_divide_smallo:
eberlm@68246
  1219
  assumes "((\<lambda>x. f1 x / g1 x) \<longlongrightarrow> a) F"
eberlm@68246
  1220
  assumes "f2 \<in> o[F](f1)" "g2 \<in> o[F](g1)"
eberlm@68246
  1221
  assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
eberlm@68246
  1222
  shows   "((\<lambda>x. (f1 x + f2 x) / (g1 x + g2 x)) \<longlongrightarrow> a) F" (is "(?f \<longlongrightarrow> _) _")
eberlm@68246
  1223
proof (subst tendsto_cong)
eberlm@68246
  1224
  let ?f' = "\<lambda>x. (f1 x / g1 x) * (1 + f2 x / f1 x) / (1 + g2 x / g1 x)"
eberlm@68246
  1225
eberlm@68246
  1226
  have "(?f' \<longlongrightarrow> a * (1 + 0) / (1 + 0)) F"
eberlm@68246
  1227
  by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const 
eberlm@68246
  1228
        smalloD_tendsto[OF assms(2)] smalloD_tendsto[OF assms(3)])+ simp_all
eberlm@68246
  1229
  thus "(?f' \<longlongrightarrow> a) F" by simp
eberlm@68246
  1230
eberlm@68246
  1231
  have "(1/2::real) > 0" by simp
eberlm@68246
  1232
  from landau_o.smallD[OF assms(2) this] landau_o.smallD[OF assms(3) this]
eberlm@68246
  1233
    have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)/2) F"
eberlm@68246
  1234
         "eventually (\<lambda>x. norm (g2 x) \<le> norm (g1 x)/2) F" by simp_all
eberlm@68246
  1235
  with assms(4) show "eventually (\<lambda>x. ?f x = ?f' x) F"
eberlm@68246
  1236
  proof eventually_elim
eberlm@68246
  1237
    fix x assume A: "norm (f2 x) \<le> norm (f1 x)/2" and 
eberlm@68246
  1238
                 B: "norm (g2 x) \<le> norm (g1 x)/2" and C: "g1 x \<noteq> 0"
eberlm@68246
  1239
    show "?f x = ?f' x"
eberlm@68246
  1240
    proof (cases "f1 x = 0")
eberlm@68246
  1241
      assume D: "f1 x \<noteq> 0"
eberlm@68246
  1242
      from D have "f1 x + f2 x = f1 x * (1 + f2 x/f1 x)" by (simp add: field_simps)
eberlm@68246
  1243
      moreover from C have "g1 x + g2 x = g1 x * (1 + g2 x/g1 x)" by (simp add: field_simps)
eberlm@68246
  1244
      ultimately have "?f x = (f1 x * (1 + f2 x/f1 x)) / (g1 x * (1 + g2 x/g1 x))" by (simp only:)
eberlm@68246
  1245
      also have "... = ?f' x" by simp
eberlm@68246
  1246
      finally show ?thesis .
eberlm@68246
  1247
    qed (insert A, simp)
eberlm@68246
  1248
  qed
eberlm@68246
  1249
qed
eberlm@68246
  1250
eberlm@68246
  1251
eberlm@68246
  1252
lemma bigo_powr:
eberlm@68246
  1253
  fixes f :: "'a \<Rightarrow> real"
eberlm@68246
  1254
  assumes "f \<in> O[F](g)" "p \<ge> 0"
eberlm@68246
  1255
  shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)"
eberlm@68246
  1256
proof-
eberlm@68246
  1257
  from assms(1) guess c by (elim landau_o.bigE landau_omega.bigE IntE)
eberlm@68246
  1258
  note c = this
eberlm@68246
  1259
  from c(2) assms(2) have "eventually (\<lambda>x. (norm (f x)) powr p \<le> (c * (norm (g x))) powr p) F"
eberlm@68246
  1260
    by (auto elim!: eventually_mono intro!: powr_mono2)
eberlm@68246
  1261
  thus "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" using c(1)
eberlm@68246
  1262
    by (intro bigoI[of _ "c powr p"]) (simp_all add: powr_mult)
eberlm@68246
  1263
qed
eberlm@68246
  1264
eberlm@68246
  1265
lemma smallo_powr:
eberlm@68246
  1266
  fixes f :: "'a \<Rightarrow> real"
eberlm@68246
  1267
  assumes "f \<in> o[F](g)" "p > 0"
eberlm@68246
  1268
  shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)"
eberlm@68246
  1269
proof (rule landau_o.smallI)
eberlm@68246
  1270
  fix c :: real assume c: "c > 0"
eberlm@68246
  1271
  hence "c powr (1/p) > 0" by simp
eberlm@68246
  1272
  from landau_o.smallD[OF assms(1) this] 
eberlm@68246
  1273
  show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F"
eberlm@68246
  1274
  proof eventually_elim
eberlm@68246
  1275
    fix x assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))"
eberlm@68246
  1276
    with assms(2) have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p"
eberlm@68246
  1277
      by (intro powr_mono2) simp_all
eberlm@68246
  1278
    also from assms(2) c have "... = c * (norm (g x)) powr p"
eberlm@68246
  1279
      by (simp add: field_simps powr_mult powr_powr)
eberlm@68246
  1280
    finally show "norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)" by simp
eberlm@68246
  1281
  qed
eberlm@68246
  1282
qed
eberlm@68246
  1283
eberlm@68246
  1284
lemma smallo_powr_nonneg:
eberlm@68246
  1285
  fixes f :: "'a \<Rightarrow> real"
eberlm@68246
  1286
  assumes "f \<in> o[F](g)" "p > 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
eberlm@68246
  1287
  shows   "(\<lambda>x. f x powr p) \<in> o[F](\<lambda>x. g x powr p)"
eberlm@68246
  1288
proof -
eberlm@68246
  1289
  from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
eberlm@68246
  1290
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1291
  also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro smallo_powr) fact+
eberlm@68246
  1292
  also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
eberlm@68246
  1293
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1294
  finally show ?thesis .
eberlm@68246
  1295
qed
eberlm@68246
  1296
eberlm@68246
  1297
lemma bigtheta_powr:
eberlm@68246
  1298
  fixes f :: "'a \<Rightarrow> real"
eberlm@68246
  1299
  shows "f \<in> \<Theta>[F](g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>g x\<bar> powr p)"
eberlm@68246
  1300
apply (cases "p < 0")
eberlm@68246
  1301
apply (subst bigtheta_inverse[symmetric], subst (1 2) powr_minus[symmetric])
eberlm@68246
  1302
unfolding bigtheta_def apply (auto simp: bigomega_iff_bigo intro!: bigo_powr)
eberlm@68246
  1303
done
eberlm@68246
  1304
eberlm@68246
  1305
lemma bigo_powr_nonneg:
eberlm@68246
  1306
  fixes f :: "'a \<Rightarrow> real"
eberlm@68246
  1307
  assumes "f \<in> O[F](g)" "p \<ge> 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
eberlm@68246
  1308
  shows   "(\<lambda>x. f x powr p) \<in> O[F](\<lambda>x. g x powr p)"
eberlm@68246
  1309
proof -
eberlm@68246
  1310
  from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
eberlm@68246
  1311
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1312
  also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro bigo_powr) fact+
eberlm@68246
  1313
  also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
eberlm@68246
  1314
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1315
  finally show ?thesis .
eberlm@68246
  1316
qed
eberlm@68246
  1317
eberlm@68246
  1318
lemma zero_in_smallo [simp]: "(\<lambda>_. 0) \<in> o[F](f)"
eberlm@68246
  1319
  by (intro landau_o.smallI) simp_all
eberlm@68246
  1320
eberlm@68246
  1321
lemma zero_in_bigo [simp]: "(\<lambda>_. 0) \<in> O[F](f)"
eberlm@68246
  1322
  by (intro landau_o.bigI[of 1]) simp_all
eberlm@68246
  1323
eberlm@68246
  1324
lemma in_bigomega_zero [simp]: "f \<in> \<Omega>[F](\<lambda>x. 0)"
eberlm@68246
  1325
  by (rule landau_omega.bigI[of 1]) simp_all
eberlm@68246
  1326
eberlm@68246
  1327
lemma in_smallomega_zero [simp]: "f \<in> \<omega>[F](\<lambda>x. 0)"
eberlm@68246
  1328
  by (simp add: smallomega_iff_smallo)
eberlm@68246
  1329
eberlm@68246
  1330
eberlm@68246
  1331
lemma in_smallo_zero_iff [simp]: "f \<in> o[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1332
proof
eberlm@68246
  1333
  assume "f \<in> o[F](\<lambda>_. 0)"
eberlm@68246
  1334
  from landau_o.smallD[OF this, of 1] show "eventually (\<lambda>x. f x = 0) F" by simp
eberlm@68246
  1335
next
eberlm@68246
  1336
  assume "eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1337
  hence "\<forall>c>0. eventually (\<lambda>x. (norm (f x)) \<le> c * \<bar>0\<bar>) F" by simp
eberlm@68246
  1338
  thus "f \<in> o[F](\<lambda>_. 0)" unfolding smallo_def by simp
eberlm@68246
  1339
qed
eberlm@68246
  1340
eberlm@68246
  1341
lemma in_bigo_zero_iff [simp]: "f \<in> O[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1342
proof
eberlm@68246
  1343
  assume "f \<in> O[F](\<lambda>_. 0)"
eberlm@68246
  1344
  thus "eventually (\<lambda>x. f x = 0) F" by (elim landau_o.bigE) simp
eberlm@68246
  1345
next
eberlm@68246
  1346
  assume "eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1347
  hence "eventually (\<lambda>x. (norm (f x)) \<le> 1 * \<bar>0\<bar>) F" by simp
eberlm@68246
  1348
  thus "f \<in> O[F](\<lambda>_. 0)" by (intro landau_o.bigI[of 1]) simp_all
eberlm@68246
  1349
qed
eberlm@68246
  1350
eberlm@68246
  1351
lemma zero_in_smallomega_iff [simp]: "(\<lambda>_. 0) \<in> \<omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1352
  by (simp add: smallomega_iff_smallo)
eberlm@68246
  1353
eberlm@68246
  1354
lemma zero_in_bigomega_iff [simp]: "(\<lambda>_. 0) \<in> \<Omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1355
  by (simp add: bigomega_iff_bigo)
eberlm@68246
  1356
eberlm@68246
  1357
lemma zero_in_bigtheta_iff [simp]: "(\<lambda>_. 0) \<in> \<Theta>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1358
  unfolding bigtheta_def by simp
eberlm@68246
  1359
eberlm@68246
  1360
lemma in_bigtheta_zero_iff [simp]: "f \<in> \<Theta>[F](\<lambda>x. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1361
  unfolding bigtheta_def by simp
eberlm@68246
  1362
eberlm@68246
  1363
eberlm@68246
  1364
lemma cmult_in_bigo_iff    [simp]:  "(\<lambda>x. c * f x) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
eberlm@68246
  1365
  and cmult_in_bigo_iff'   [simp]:  "(\<lambda>x. f x * c) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
eberlm@68246
  1366
  and cmult_in_smallo_iff  [simp]:  "(\<lambda>x. c * f x) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
eberlm@68246
  1367
  and cmult_in_smallo_iff' [simp]: "(\<lambda>x. f x * c) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
eberlm@68246
  1368
  by (cases "c = 0", simp, simp)+
eberlm@68246
  1369
eberlm@68246
  1370
lemma bigo_const [simp]: "(\<lambda>_. c) \<in> O[F](\<lambda>_. 1)" by (rule bigoI[of _ "norm c"]) simp
eberlm@68246
  1371
eberlm@68246
  1372
lemma bigo_const_iff [simp]: "(\<lambda>_. c1) \<in> O[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 = 0 \<or> c2 \<noteq> 0"
eberlm@68246
  1373
  by (cases "c1 = 0"; cases "c2 = 0")
eberlm@68246
  1374
     (auto simp: bigo_def eventually_False intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
eberlm@68246
  1375
eberlm@68246
  1376
lemma bigomega_const_iff [simp]: "(\<lambda>_. c1) \<in> \<Omega>[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 \<noteq> 0 \<or> c2 = 0"
eberlm@68246
  1377
  by (cases "c1 = 0"; cases "c2 = 0")
eberlm@68246
  1378
     (auto simp: bigomega_def eventually_False mult_le_0_iff 
eberlm@68246
  1379
           intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
eberlm@68246
  1380
eberlm@68246
  1381
lemma smallo_real_nat_transfer:
eberlm@68246
  1382
  "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))"
eberlm@68246
  1383
  by (rule landau_o.small.compose[OF _ filterlim_real_sequentially])
eberlm@68246
  1384
eberlm@68246
  1385
lemma bigo_real_nat_transfer:
eberlm@68246
  1386
  "(f :: real \<Rightarrow> real) \<in> O(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> O(\<lambda>x. g (real x))"
eberlm@68246
  1387
  by (rule landau_o.big.compose[OF _ filterlim_real_sequentially])
eberlm@68246
  1388
eberlm@68246
  1389
lemma smallomega_real_nat_transfer:
eberlm@68246
  1390
  "(f :: real \<Rightarrow> real) \<in> \<omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<omega>(\<lambda>x. g (real x))"
eberlm@68246
  1391
  by (rule landau_omega.small.compose[OF _ filterlim_real_sequentially])
eberlm@68246
  1392
eberlm@68246
  1393
lemma bigomega_real_nat_transfer:
eberlm@68246
  1394
  "(f :: real \<Rightarrow> real) \<in> \<Omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Omega>(\<lambda>x. g (real x))"
eberlm@68246
  1395
  by (rule landau_omega.big.compose[OF _ filterlim_real_sequentially])
eberlm@68246
  1396
eberlm@68246
  1397
lemma bigtheta_real_nat_transfer:
eberlm@68246
  1398
  "(f :: real \<Rightarrow> real) \<in> \<Theta>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Theta>(\<lambda>x. g (real x))"
eberlm@68246
  1399
  unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast
eberlm@68246
  1400
eberlm@68246
  1401
lemmas landau_real_nat_transfer [intro] = 
eberlm@68246
  1402
  bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer 
eberlm@68246
  1403
  smallomega_real_nat_transfer bigtheta_real_nat_transfer
eberlm@68246
  1404
eberlm@68246
  1405
eberlm@68246
  1406
lemma landau_symbol_if_at_top_eq [simp]:
eberlm@68246
  1407
  assumes "landau_symbol L L' Lr"
eberlm@68246
  1408
  shows   "L at_top (\<lambda>x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)"
eberlm@68246
  1409
apply (rule landau_symbol.cong[OF assms])
eberlm@68246
  1410
using less_add_one[of a] apply (auto intro: eventually_mono  eventually_ge_at_top[of "a + 1"])
eberlm@68246
  1411
done
eberlm@68246
  1412
eberlm@68246
  1413
lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq]
eberlm@68246
  1414
eberlm@68246
  1415
eberlm@68246
  1416
eberlm@68246
  1417
lemma sum_in_smallo:
eberlm@68246
  1418
  assumes "f \<in> o[F](h)" "g \<in> o[F](h)"
eberlm@68246
  1419
  shows   "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)"
eberlm@68246
  1420
proof-
eberlm@68246
  1421
  {
eberlm@68246
  1422
    fix f g assume fg: "f \<in> o[F](h)" "g \<in> o[F](h)"
eberlm@68246
  1423
    have "(\<lambda>x. f x + g x) \<in> o[F](h)"
eberlm@68246
  1424
    proof (rule landau_o.smallI)
eberlm@68246
  1425
      fix c :: real assume "c > 0"
eberlm@68246
  1426
      hence "c/2 > 0" by simp
eberlm@68246
  1427
      from fg[THEN landau_o.smallD[OF _ this]]
eberlm@68246
  1428
      show "eventually (\<lambda>x. norm (f x + g x) \<le> c * (norm (h x))) F"
eberlm@68246
  1429
        by eventually_elim (auto intro: order.trans[OF norm_triangle_ineq])
eberlm@68246
  1430
    qed
eberlm@68246
  1431
  }
eberlm@68246
  1432
  from this[of f g] this[of f "\<lambda>x. -g x"] assms
eberlm@68246
  1433
    show "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" by simp_all
eberlm@68246
  1434
qed
eberlm@68246
  1435
eberlm@68246
  1436
lemma big_sum_in_smallo:
eberlm@68246
  1437
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> o[F](g)"
eberlm@68246
  1438
  shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> o[F](g)"
eberlm@68246
  1439
  using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_smallo)
eberlm@68246
  1440
eberlm@68246
  1441
lemma sum_in_bigo:
eberlm@68246
  1442
  assumes "f \<in> O[F](h)" "g \<in> O[F](h)"
eberlm@68246
  1443
  shows   "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)"
eberlm@68246
  1444
proof-
eberlm@68246
  1445
  {
eberlm@68246
  1446
    fix f g assume fg: "f \<in> O[F](h)" "g \<in> O[F](h)"
eberlm@68246
  1447
    from fg(1) guess c1 by (elim landau_o.bigE) note c1 = this
eberlm@68246
  1448
    from fg(2) guess c2 by (elim landau_o.bigE) note c2 = this
eberlm@68246
  1449
    from c1(2) c2(2) have "eventually (\<lambda>x. norm (f x + g x) \<le> (c1 + c2) * (norm (h x))) F"
eberlm@68246
  1450
      by eventually_elim (auto simp: algebra_simps intro: order.trans[OF norm_triangle_ineq])
eberlm@68246
  1451
    hence "(\<lambda>x. f x + g x) \<in> O[F](h)" by (rule bigoI)
eberlm@68246
  1452
  }
eberlm@68246
  1453
  from this[of f g] this[of f "\<lambda>x. -g x"] assms
eberlm@68246
  1454
    show "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" by simp_all
eberlm@68246
  1455
qed
eberlm@68246
  1456
eberlm@68246
  1457
lemma big_sum_in_bigo:
eberlm@68246
  1458
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> O[F](g)"
eberlm@68246
  1459
  shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"
eberlm@68246
  1460
  using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)
eberlm@68246
  1461
eberlm@68246
  1462
context landau_symbol
eberlm@68246
  1463
begin
eberlm@68246
  1464
eberlm@68246
  1465
lemma mult_cancel_left:
eberlm@68246
  1466
  assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
eberlm@68246
  1467
  notes   [trans] = bigtheta_trans1 bigtheta_trans2
eberlm@68246
  1468
  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f2 \<in> L F (g2)"
eberlm@68246
  1469
proof
eberlm@68246
  1470
  assume A: "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
eberlm@68246
  1471
  from assms have nz: "eventually (\<lambda>x. f1 x \<noteq> 0) F" by (simp add: eventually_nonzero_bigtheta)
eberlm@68246
  1472
  hence "f2 \<in> \<Theta>[F](\<lambda>x. f1 x * f2 x / f1 x)"
eberlm@68246
  1473
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1474
  also from A assms nz have "(\<lambda>x. f1 x * f2 x / f1 x) \<in> L F (\<lambda>x. g1 x * g2 x / f1 x)" 
eberlm@68246
  1475
    by (intro divide_right) simp_all
eberlm@68246
  1476
  also from assms nz have "(\<lambda>x. g1 x * g2 x / f1 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x / g1 x)"
eberlm@68246
  1477
    by (intro landau_theta.mult landau_theta.divide) (simp_all add: bigtheta_sym)
eberlm@68246
  1478
  also from assms have "(\<lambda>x. g1 x * g2 x / g1 x) \<in> \<Theta>[F](g2)"
eberlm@68246
  1479
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1480
  finally show "f2 \<in> L F (g2)" .
eberlm@68246
  1481
next
eberlm@68246
  1482
  assume "f2 \<in> L F (g2)"
eberlm@68246
  1483
  hence "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. f1 x * g2 x)" by (rule mult_left)
eberlm@68246
  1484
  also have "(\<lambda>x. f1 x * g2 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x)"
eberlm@68246
  1485
    by (intro landau_theta.mult_right assms)
eberlm@68246
  1486
  finally show "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" .
eberlm@68246
  1487
qed
eberlm@68246
  1488
eberlm@68246
  1489
lemma mult_cancel_right:
eberlm@68246
  1490
  assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
eberlm@68246
  1491
  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
eberlm@68246
  1492
  by (subst (1 2) mult.commute) (rule mult_cancel_left[OF assms])
eberlm@68246
  1493
eberlm@68246
  1494
lemma divide_cancel_right:
eberlm@68246
  1495
  assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
eberlm@68246
  1496
  shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
eberlm@68246
  1497
  by (subst (1 2) divide_inverse, intro mult_cancel_right bigtheta_inverse) (simp_all add: assms)
eberlm@68246
  1498
eberlm@68246
  1499
lemma divide_cancel_left:
eberlm@68246
  1500
  assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
eberlm@68246
  1501
  shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> 
eberlm@68246
  1502
             (\<lambda>x. inverse (f2 x)) \<in> L F (\<lambda>x. inverse (g2 x))"
eberlm@68246
  1503
  by (simp only: divide_inverse mult_cancel_left[OF assms])
eberlm@68246
  1504
eberlm@68246
  1505
end
eberlm@68246
  1506
eberlm@68246
  1507
eberlm@68246
  1508
lemma powr_smallo_iff:
eberlm@68246
  1509
  assumes "filterlim g at_top F" "F \<noteq> bot"
eberlm@68246
  1510
  shows   "(\<lambda>x. g x powr p :: real) \<in> o[F](\<lambda>x. g x powr q) \<longleftrightarrow> p < q"
eberlm@68246
  1511
proof-
eberlm@68246
  1512
  from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
eberlm@68246
  1513
  hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
eberlm@68246
  1514
  have B: "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p) \<Longrightarrow> (\<lambda>x. g x powr p) \<notin> o[F](\<lambda>x. g x powr q)"
eberlm@68246
  1515
  proof
eberlm@68246
  1516
    assume "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)"
eberlm@68246
  1517
    from landau_o.big_small_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
eberlm@68246
  1518
    with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
eberlm@68246
  1519
    thus False by (simp add: eventually_False assms)
eberlm@68246
  1520
  qed
eberlm@68246
  1521
  show ?thesis
eberlm@68246
  1522
  proof (cases p q rule: linorder_cases)
eberlm@68246
  1523
    assume "p < q"
eberlm@68246
  1524
    hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
nipkow@68406
  1525
      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
wenzelm@69272
  1526
    with \<open>p < q\<close> show ?thesis by auto
eberlm@68246
  1527
  next
eberlm@68246
  1528
    assume "p = q"
eberlm@68246
  1529
    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
wenzelm@69272
  1530
    with B \<open>p = q\<close> show ?thesis by auto
eberlm@68246
  1531
  next
eberlm@68246
  1532
    assume "p > q"
eberlm@68246
  1533
    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
nipkow@68406
  1534
      by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)
wenzelm@69272
  1535
    with B \<open>p > q\<close> show ?thesis by auto
eberlm@68246
  1536
  qed
eberlm@68246
  1537
qed
eberlm@68246
  1538
eberlm@68246
  1539
lemma powr_bigo_iff:
eberlm@68246
  1540
  assumes "filterlim g at_top F" "F \<noteq> bot"
eberlm@68246
  1541
  shows   "(\<lambda>x. g x powr p :: real) \<in> O[F](\<lambda>x. g x powr q) \<longleftrightarrow> p \<le> q"
eberlm@68246
  1542
proof-
eberlm@68246
  1543
  from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
eberlm@68246
  1544
  hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
eberlm@68246
  1545
  have B: "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p) \<Longrightarrow> (\<lambda>x. g x powr p) \<notin> O[F](\<lambda>x. g x powr q)"
eberlm@68246
  1546
  proof
eberlm@68246
  1547
    assume "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" "(\<lambda>x. g x powr p) \<in> O[F](\<lambda>x. g x powr q)"
eberlm@68246
  1548
    from landau_o.small_big_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
eberlm@68246
  1549
    with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
eberlm@68246
  1550
    thus False by (simp add: eventually_False assms)
eberlm@68246
  1551
  qed
eberlm@68246
  1552
  show ?thesis
eberlm@68246
  1553
  proof (cases p q rule: linorder_cases)
eberlm@68246
  1554
    assume "p < q"
eberlm@68246
  1555
    hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
nipkow@68406
  1556
      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
wenzelm@69272
  1557
    with \<open>p < q\<close> show ?thesis by (auto intro: landau_o.small_imp_big)
eberlm@68246
  1558
  next
eberlm@68246
  1559
    assume "p = q"
eberlm@68246
  1560
    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
wenzelm@69272
  1561
    with B \<open>p = q\<close> show ?thesis by auto
eberlm@68246
  1562
  next
eberlm@68246
  1563
    assume "p > q"
eberlm@68246
  1564
    hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
nipkow@68406
  1565
      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
wenzelm@69272
  1566
    with B \<open>p > q\<close> show ?thesis by (auto intro: landau_o.small_imp_big)
eberlm@68246
  1567
  qed
eberlm@68246
  1568
qed
eberlm@68246
  1569
eberlm@68246
  1570
lemma powr_bigtheta_iff: 
eberlm@68246
  1571
  assumes "filterlim g at_top F" "F \<noteq> bot"
eberlm@68246
  1572
  shows   "(\<lambda>x. g x powr p :: real) \<in> \<Theta>[F](\<lambda>x. g x powr q) \<longleftrightarrow> p = q"
eberlm@68246
  1573
  using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff)
eberlm@68246
  1574
eberlm@68246
  1575
eberlm@68246
  1576
subsection \<open>Flatness of real functions\<close>
eberlm@68246
  1577
eberlm@68246
  1578
text \<open>
eberlm@68246
  1579
  Given two real-valued functions $f$ and $g$, we say that $f$ is flatter than $g$ if
eberlm@68246
  1580
  any power of $f(x)$ is asymptotically dominated by any positive power of $g(x)$. This is
eberlm@68246
  1581
  a useful notion since, given two products of powers of functions sorted by flatness, we can
eberlm@68246
  1582
  compare them asymptotically by simply comparing the exponent lists lexicographically.
eberlm@68246
  1583
eberlm@68246
  1584
  A simple sufficient criterion for flatness it that $\ln f(x) \in o(\ln g(x))$, which we show
eberlm@68246
  1585
  now.
eberlm@68246
  1586
\<close>
eberlm@68246
  1587
lemma ln_smallo_imp_flat:
eberlm@68246
  1588
  fixes f g :: "real \<Rightarrow> real"
eberlm@68246
  1589
  assumes lim_f: "filterlim f at_top at_top"
eberlm@68246
  1590
  assumes lim_g: "filterlim g at_top at_top"
eberlm@68246
  1591
  assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
eberlm@68246
  1592
  assumes q: "q > 0"
eberlm@68246
  1593
  shows   "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)"
eberlm@68246
  1594
proof (rule smalloI_tendsto)
eberlm@68246
  1595
  from lim_f have "eventually (\<lambda>x. f x > 0) at_top" 
eberlm@68246
  1596
    by (simp add: filterlim_at_top_dense)
eberlm@68246
  1597
  hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp
eberlm@68246
  1598
  
eberlm@68246
  1599
  from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top"
eberlm@68246
  1600
    by (simp add: filterlim_at_top_dense)
eberlm@68246
  1601
  hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp
eberlm@68246
  1602
  thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top"
eberlm@68246
  1603
    by eventually_elim simp
eberlm@68246
  1604
  
eberlm@68246
  1605
  have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) = 
eberlm@68246
  1606
                          p * ln (f x) - q * ln (g x)) at_top"
eberlm@68246
  1607
    using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps)
eberlm@68246
  1608
  have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top"
eberlm@68246
  1609
    by (insert q)
eberlm@68246
  1610
       (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult
eberlm@68246
  1611
              tendsto_const tendsto_diff smalloD_tendsto[OF ln_o_ln] lim_g
eberlm@68246
  1612
              filterlim_compose[OF ln_at_top] | simp)+
eberlm@68246
  1613
  hence "filterlim (\<lambda>x. p * ln (f x) - q * ln (g x)) at_bot at_top"
eberlm@68246
  1614
    by (subst (asm) filterlim_cong[OF refl refl eq])
eberlm@68246
  1615
  hence *: "((\<lambda>x. exp (p * ln (f x) - q * ln (g x))) \<longlongrightarrow> 0) at_top"
eberlm@68246
  1616
    by (rule filterlim_compose[OF exp_at_bot])
eberlm@68246
  1617
  have eq: "eventually (\<lambda>x. exp (p * ln (f x) - q * ln (g x)) = f x powr p / g x powr q) at_top"
eberlm@68246
  1618
    using f_nz g_nz by eventually_elim (simp add: powr_def exp_diff)
eberlm@68246
  1619
  show "((\<lambda>x. f x powr p / g x powr q) \<longlongrightarrow> 0) at_top"
eberlm@68246
  1620
    using * by (subst (asm) filterlim_cong[OF refl refl eq])
eberlm@68246
  1621
qed
eberlm@68246
  1622
eberlm@68246
  1623
lemma ln_smallo_imp_flat':
eberlm@68246
  1624
  fixes f g :: "real \<Rightarrow> real"
eberlm@68246
  1625
  assumes lim_f: "filterlim f at_top at_top"
eberlm@68246
  1626
  assumes lim_g: "filterlim g at_top at_top"
eberlm@68246
  1627
  assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
eberlm@68246
  1628
  assumes q: "q < 0"
eberlm@68246
  1629
  shows   "(\<lambda>x. g x powr q) \<in> o(\<lambda>x. f x powr p)"
eberlm@68246
  1630
proof -
eberlm@68246
  1631
  from lim_f lim_g have "eventually (\<lambda>x. f x > 0) at_top" "eventually (\<lambda>x. g x > 0) at_top"
eberlm@68246
  1632
    by (simp_all add: filterlim_at_top_dense)
eberlm@68246
  1633
  hence "eventually (\<lambda>x. f x \<noteq> 0) at_top" "eventually (\<lambda>x. g x \<noteq> 0) at_top"
eberlm@68246
  1634
    by (auto elim: eventually_mono)
eberlm@68246
  1635
  moreover from assms have "(\<lambda>x. f x powr -p) \<in> o(\<lambda>x. g x powr -q)"
eberlm@68246
  1636
    by (intro ln_smallo_imp_flat assms) simp_all
eberlm@68246
  1637
  ultimately show ?thesis unfolding powr_minus
eberlm@68246
  1638
    by (simp add: landau_o.small.inverse_cancel)
eberlm@68246
  1639
qed
eberlm@68246
  1640
eberlm@68246
  1641
eberlm@68246
  1642
subsection \<open>Asymptotic Equivalence\<close>
eberlm@68246
  1643
eberlm@68246
  1644
(* TODO Move *)
eberlm@68246
  1645
lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
eberlm@68246
  1646
  by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
eberlm@68246
  1647
eberlm@68246
  1648
named_theorems asymp_equiv_intros
eberlm@68246
  1649
named_theorems asymp_equiv_simps
eberlm@68246
  1650
eberlm@68246
  1651
definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
wenzelm@69597
  1652
  (\<open>_ \<sim>[_] _\<close> [51, 10, 51] 50)
eberlm@68246
  1653
  where "f \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
eberlm@68246
  1654
eberlm@68246
  1655
abbreviation (input) asymp_equiv_at_top where
eberlm@68246
  1656
  "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"
eberlm@68246
  1657
eberlm@68246
  1658
bundle asymp_equiv_notation
eberlm@68246
  1659
begin
wenzelm@69597
  1660
notation asymp_equiv_at_top (infix \<open>\<sim>\<close> 50) 
eberlm@68246
  1661
end
eberlm@68246
  1662
eberlm@68246
  1663
lemma asymp_equivI: "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F \<Longrightarrow> f \<sim>[F] g"
eberlm@68246
  1664
  by (simp add: asymp_equiv_def)
eberlm@68246
  1665
eberlm@68246
  1666
lemma asymp_equivD: "f \<sim>[F] g \<Longrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
eberlm@68246
  1667
  by (simp add: asymp_equiv_def)
eberlm@68246
  1668
eberlm@68246
  1669
lemma asymp_equiv_filtermap_iff:
eberlm@68246
  1670
  "f \<sim>[filtermap h F] g \<longleftrightarrow> (\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
eberlm@68246
  1671
  by (simp add: asymp_equiv_def filterlim_filtermap)
eberlm@68246
  1672
eberlm@68246
  1673
lemma asymp_equiv_refl [simp, asymp_equiv_intros]: "f \<sim>[F] f"
eberlm@68246
  1674
proof (intro asymp_equivI)
eberlm@68246
  1675
  have "eventually (\<lambda>x. 1 = (if f x = 0 \<and> f x = 0 then 1 else f x / f x)) F"
eberlm@68246
  1676
    by (intro always_eventually) simp
eberlm@68246
  1677
  moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
eberlm@68246
  1678
  ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
eberlm@68246
  1679
    by (rule Lim_transform_eventually)
eberlm@68246
  1680
qed
eberlm@68246
  1681
eberlm@68246
  1682
lemma asymp_equiv_symI: 
eberlm@68246
  1683
  assumes "f \<sim>[F] g"
eberlm@68246
  1684
  shows   "g \<sim>[F] f"
eberlm@68246
  1685
  using tendsto_inverse[OF asymp_equivD[OF assms]]
eberlm@68246
  1686
  by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong)
eberlm@68246
  1687
eberlm@68246
  1688
lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f"
eberlm@68246
  1689
  by (blast intro: asymp_equiv_symI)
eberlm@68246
  1690
eberlm@68246
  1691
lemma asymp_equivI': 
eberlm@68246
  1692
  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
eberlm@68246
  1693
  shows   "f \<sim>[F] g"
eberlm@68246
  1694
proof (cases "F = bot")
eberlm@68246
  1695
  case False
eberlm@68246
  1696
  have "eventually (\<lambda>x. f x \<noteq> 0) F"
eberlm@68246
  1697
  proof (rule ccontr)
eberlm@68246
  1698
    assume "\<not>eventually (\<lambda>x. f x \<noteq> 0) F"
eberlm@68246
  1699
    hence "frequently (\<lambda>x. f x = 0) F" by (simp add: frequently_def)
eberlm@68246
  1700
    hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1)
eberlm@68246
  1701
    from limit_frequently_eq[OF False this assms] show False by simp_all
eberlm@68246
  1702
  qed
eberlm@68246
  1703
  hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"
eberlm@68246
  1704
    by eventually_elim simp
eberlm@68246
  1705
  from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def 
eberlm@68246
  1706
    by (rule Lim_transform_eventually)
eberlm@68246
  1707
qed (simp_all add: asymp_equiv_def)
eberlm@68246
  1708
eberlm@68246
  1709
eberlm@68246
  1710
lemma asymp_equiv_cong:
eberlm@68246
  1711
  assumes "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
eberlm@68246
  1712
  shows   "f1 \<sim>[F] g1 \<longleftrightarrow> f2 \<sim>[F] g2"
eberlm@68246
  1713
  unfolding asymp_equiv_def
eberlm@68246
  1714
proof (rule tendsto_cong, goal_cases)
eberlm@68246
  1715
  case 1
eberlm@68246
  1716
  from assms show ?case by eventually_elim simp
eberlm@68246
  1717
qed
eberlm@68246
  1718
eberlm@68246
  1719
lemma asymp_equiv_eventually_zeros:
eberlm@68246
  1720
  fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
eberlm@68246
  1721
  assumes "f \<sim>[F] g"
eberlm@68246
  1722
  shows   "eventually (\<lambda>x. f x = 0 \<longleftrightarrow> g x = 0) F"
eberlm@68246
  1723
proof -
eberlm@68246
  1724
  let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  1725
  have "eventually (\<lambda>x. x \<noteq> 0) (nhds (1::'b))"
eberlm@68246
  1726
    by (rule t1_space_nhds) auto
eberlm@68246
  1727
  hence "eventually (\<lambda>x. x \<noteq> 0) (filtermap ?h F)"
eberlm@68246
  1728
    using assms unfolding asymp_equiv_def filterlim_def
eberlm@68246
  1729
    by (rule filter_leD [rotated])
eberlm@68246
  1730
  hence "eventually (\<lambda>x. ?h x \<noteq> 0) F" by (simp add: eventually_filtermap)
eberlm@68246
  1731
  thus ?thesis by eventually_elim (auto split: if_splits)
eberlm@68246
  1732
qed
eberlm@68246
  1733
eberlm@68246
  1734
lemma asymp_equiv_transfer:
eberlm@68246
  1735
  assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
eberlm@68246
  1736
  shows   "f2 \<sim>[F] g2"
eberlm@68246
  1737
  using assms(1) asymp_equiv_cong[OF assms(2,3)] by simp
eberlm@68246
  1738
eberlm@68246
  1739
lemma asymp_equiv_transfer_trans [trans]:
eberlm@68246
  1740
  assumes "(\<lambda>x. f x (h1 x)) \<sim>[F] (\<lambda>x. g x (h1 x))"
eberlm@68246
  1741
  assumes "eventually (\<lambda>x. h1 x = h2 x) F"
eberlm@68246
  1742
  shows   "(\<lambda>x. f x (h2 x)) \<sim>[F] (\<lambda>x. g x (h2 x))"
eberlm@68246
  1743
  by (rule asymp_equiv_transfer[OF assms(1)]) (insert assms(2), auto elim!: eventually_mono)
eberlm@68246
  1744
eberlm@68246
  1745
lemma asymp_equiv_trans [trans]:
eberlm@68246
  1746
  fixes f g h
eberlm@68246
  1747
  assumes "f \<sim>[F] g" "g \<sim>[F] h"
eberlm@68246
  1748
  shows   "f \<sim>[F] h"
eberlm@68246
  1749
proof -
eberlm@68246
  1750
  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  1751
  from assms[THEN asymp_equiv_eventually_zeros]
eberlm@68246
  1752
    have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
eberlm@68246
  1753
  moreover from tendsto_mult[OF assms[THEN asymp_equivD]] 
eberlm@68246
  1754
    have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
eberlm@68246
  1755
  ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
eberlm@68246
  1756
qed
eberlm@68246
  1757
eberlm@68246
  1758
lemma asymp_equiv_trans_lift1 [trans]:
eberlm@68246
  1759
  assumes "a \<sim>[F] f b" "b \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
eberlm@68246
  1760
  shows   "a \<sim>[F] f c"
eberlm@68246
  1761
  using assms by (blast intro: asymp_equiv_trans)
eberlm@68246
  1762
eberlm@68246
  1763
lemma asymp_equiv_trans_lift2 [trans]:
eberlm@68246
  1764
  assumes "f a \<sim>[F] b" "a \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
eberlm@68246
  1765
  shows   "f c \<sim>[F] b"
eberlm@68246
  1766
  using asymp_equiv_symI[OF assms(3)[OF assms(2)]] assms(1)
eberlm@68246
  1767
  by (blast intro: asymp_equiv_trans)
eberlm@68246
  1768
eberlm@68246
  1769
lemma asymp_equivD_const:
eberlm@68246
  1770
  assumes "f \<sim>[F] (\<lambda>_. c)"
eberlm@68246
  1771
  shows   "(f \<longlongrightarrow> c) F"
eberlm@68246
  1772
proof (cases "c = 0")
eberlm@68246
  1773
  case False
eberlm@68246
  1774
  with tendsto_mult_right[OF asymp_equivD[OF assms], of c] show ?thesis by simp
eberlm@68246
  1775
next
eberlm@68246
  1776
  case True
eberlm@68246
  1777
  with asymp_equiv_eventually_zeros[OF assms] show ?thesis
eberlm@68246
  1778
    by (simp add: Lim_eventually)
eberlm@68246
  1779
qed
eberlm@68246
  1780
eberlm@68246
  1781
lemma asymp_equiv_refl_ev:
eberlm@68246
  1782
  assumes "eventually (\<lambda>x. f x = g x) F"
eberlm@68246
  1783
  shows   "f \<sim>[F] g"
eberlm@68246
  1784
  by (intro asymp_equivI Lim_eventually)
eberlm@68246
  1785
     (insert assms, auto elim!: eventually_mono)
eberlm@68246
  1786
eberlm@68246
  1787
lemma asymp_equiv_sandwich:
eberlm@68246
  1788
  fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"
eberlm@68246
  1789
  assumes "eventually (\<lambda>x. f x \<ge> 0) F"
eberlm@68246
  1790
  assumes "eventually (\<lambda>x. f x \<le> g x) F"
eberlm@68246
  1791
  assumes "eventually (\<lambda>x. g x \<le> h x) F"
eberlm@68246
  1792
  assumes "f \<sim>[F] h"
eberlm@68246
  1793
  shows   "g \<sim>[F] f" "g \<sim>[F] h"
eberlm@68246
  1794
proof -
eberlm@68246
  1795
  show "g \<sim>[F] f"
eberlm@68246
  1796
  proof (rule asymp_equivI, rule tendsto_sandwich)
eberlm@68246
  1797
    from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
eberlm@68246
  1798
      show "eventually (\<lambda>n. (if h n = 0 \<and> f n = 0 then 1 else h n / f n) \<ge>
eberlm@68246
  1799
                              (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
eberlm@68246
  1800
        by eventually_elim (auto intro!: divide_right_mono)
eberlm@68246
  1801
    from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
eberlm@68246
  1802
      show "eventually (\<lambda>n. 1 \<le>
eberlm@68246
  1803
                              (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
eberlm@68246
  1804
        by eventually_elim (auto intro!: divide_right_mono)
eberlm@68246
  1805
  qed (insert asymp_equiv_symI[OF assms(4)], simp_all add: asymp_equiv_def)
eberlm@68246
  1806
  also note \<open>f \<sim>[F] h\<close>
eberlm@68246
  1807
  finally show "g \<sim>[F] h" .
eberlm@68246
  1808
qed
eberlm@68246
  1809
eberlm@68246
  1810
lemma asymp_equiv_imp_eventually_same_sign:
eberlm@68246
  1811
  fixes f g :: "real \<Rightarrow> real"
eberlm@68246
  1812
  assumes "f \<sim>[F] g"
eberlm@68246
  1813
  shows   "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
eberlm@68246
  1814
proof -
eberlm@68246
  1815
  from assms have "((\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> sgn 1) F"
eberlm@68246
  1816
    unfolding asymp_equiv_def by (rule tendsto_sgn) simp_all
eberlm@68246
  1817
  from order_tendstoD(1)[OF this, of "1/2"]
eberlm@68246
  1818
    have "eventually (\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x) > 1/2) F"
eberlm@68246
  1819
    by simp
eberlm@68246
  1820
  thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
eberlm@68246
  1821
  proof eventually_elim
eberlm@68246
  1822
    case (elim x)
eberlm@68246
  1823
    thus ?case
eberlm@68246
  1824
      by (cases "f x" "0 :: real" rule: linorder_cases; 
eberlm@68246
  1825
          cases "g x" "0 :: real" rule: linorder_cases) simp_all
eberlm@68246
  1826
  qed
eberlm@68246
  1827
qed
eberlm@68246
  1828
eberlm@68246
  1829
lemma
eberlm@68246
  1830
  fixes f g :: "_ \<Rightarrow> real"
eberlm@68246
  1831
  assumes "f \<sim>[F] g"
eberlm@68246
  1832
  shows   asymp_equiv_eventually_same_sign: "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" (is ?th1)
eberlm@68246
  1833
    and   asymp_equiv_eventually_neg_iff:   "eventually (\<lambda>x. f x < 0 \<longleftrightarrow> g x < 0) F" (is ?th2)
eberlm@68246
  1834
    and   asymp_equiv_eventually_pos_iff:   "eventually (\<lambda>x. f x > 0 \<longleftrightarrow> g x > 0) F" (is ?th3)
eberlm@68246
  1835
proof -
eberlm@68246
  1836
  from assms have "filterlim (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) (nhds 1) F"
eberlm@68246
  1837
    by (rule asymp_equivD)
eberlm@68246
  1838
  from order_tendstoD(1)[OF this zero_less_one]
eberlm@68246
  1839
    show ?th1 ?th2 ?th3
eberlm@68246
  1840
    by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+
eberlm@68246
  1841
qed
eberlm@68246
  1842
eberlm@68246
  1843
lemma asymp_equiv_tendsto_transfer:
eberlm@68246
  1844
  assumes "f \<sim>[F] g" and "(f \<longlongrightarrow> c) F"
eberlm@68246
  1845
  shows   "(g \<longlongrightarrow> c) F"
eberlm@68246
  1846
proof -
eberlm@68246
  1847
  let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"
eberlm@68246
  1848
  have "eventually (\<lambda>x. ?h x = g x) F"
eberlm@68246
  1849
    using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
eberlm@68246
  1850
  moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
eberlm@68246
  1851
  hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"
eberlm@68246
  1852
    by (rule asymp_equivD)
eberlm@68246
  1853
  from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp
eberlm@68246
  1854
  ultimately show ?thesis by (rule Lim_transform_eventually)
eberlm@68246
  1855
qed
eberlm@68246
  1856
eberlm@68246
  1857
lemma tendsto_asymp_equiv_cong:
eberlm@68246
  1858
  assumes "f \<sim>[F] g"
eberlm@68246
  1859
  shows   "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"
eberlm@68246
  1860
proof -
eberlm@68246
  1861
  {
eberlm@68246
  1862
    fix f g :: "'a \<Rightarrow> 'b"
eberlm@68246
  1863
    assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"
eberlm@68246
  1864
    have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"
eberlm@68246
  1865
      using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp
eberlm@68246
  1866
    moreover have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F"
eberlm@68246
  1867
      by (intro tendsto_intros asymp_equivD *)
eberlm@68246
  1868
    ultimately have "(f \<longlongrightarrow> c * 1) F"
eberlm@68246
  1869
      by (rule Lim_transform_eventually)
eberlm@68246
  1870
  }
eberlm@68246
  1871
  from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym)
eberlm@68246
  1872
qed
eberlm@68246
  1873
eberlm@68246
  1874
eberlm@68246
  1875
lemma smallo_imp_eventually_sgn:
eberlm@68246
  1876
  fixes f g :: "real \<Rightarrow> real"
eberlm@68246
  1877
  assumes "g \<in> o(f)"
eberlm@68246
  1878
  shows   "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top"
eberlm@68246
  1879
proof -
eberlm@68246
  1880
  have "0 < (1/2 :: real)" by simp
eberlm@68246
  1881
  from landau_o.smallD[OF assms, OF this] 
eberlm@68246
  1882
    have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp
eberlm@68246
  1883
  thus ?thesis
eberlm@68246
  1884
  proof eventually_elim
eberlm@68246
  1885
    case (elim x)
eberlm@68246
  1886
    thus ?case
eberlm@68246
  1887
      by (cases "f x" "0::real" rule: linorder_cases; 
eberlm@68246
  1888
          cases "f x + g x" "0::real" rule: linorder_cases) simp_all
eberlm@68246
  1889
  qed
eberlm@68246
  1890
qed
eberlm@68246
  1891
eberlm@68246
  1892
context
eberlm@68246
  1893
begin
eberlm@68246
  1894
eberlm@68246
  1895
private lemma asymp_equiv_add_rightI:
eberlm@68246
  1896
  assumes "f \<sim>[F] g" "h \<in> o[F](g)"
eberlm@68246
  1897
  shows   "(\<lambda>x. f x + h x) \<sim>[F] g"
eberlm@68246
  1898
proof -
eberlm@68246
  1899
  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  1900
  from landau_o.smallD[OF assms(2) zero_less_one]
eberlm@68246
  1901
    have ev: "eventually (\<lambda>x. g x = 0 \<longrightarrow> h x = 0) F" by eventually_elim auto
eberlm@68246
  1902
  have "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1) F"
eberlm@68246
  1903
    unfolding asymp_equiv_def using ev
eberlm@68246
  1904
    by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps)
eberlm@68246
  1905
  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1 + 0) F" by simp
eberlm@68246
  1906
  also have \<dots> by (intro tendsto_intros asymp_equivD assms smalloD_tendsto)
eberlm@68246
  1907
  finally show "(\<lambda>x. f x + h x) \<sim>[F] g" .
eberlm@68246
  1908
qed
eberlm@68246
  1909
eberlm@68246
  1910
lemma asymp_equiv_add_right [asymp_equiv_simps]:
eberlm@68246
  1911
  assumes "h \<in> o[F](g)"
eberlm@68246
  1912
  shows   "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
eberlm@68246
  1913
proof
eberlm@68246
  1914
  assume "(\<lambda>x. f x + h x) \<sim>[F] g"
eberlm@68246
  1915
  from asymp_equiv_add_rightI[OF this, of "\<lambda>x. -h x"] assms show "f \<sim>[F] g"
eberlm@68246
  1916
    by simp
eberlm@68246
  1917
qed (simp_all add: asymp_equiv_add_rightI assms)
eberlm@68246
  1918
eberlm@68246
  1919
end
eberlm@68246
  1920
eberlm@68246
  1921
lemma asymp_equiv_add_left [asymp_equiv_simps]: 
eberlm@68246
  1922
  assumes "h \<in> o[F](g)"
eberlm@68246
  1923
  shows   "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
eberlm@68246
  1924
  using asymp_equiv_add_right[OF assms] by (simp add: add.commute)
eberlm@68246
  1925
eberlm@68246
  1926
lemma asymp_equiv_add_right' [asymp_equiv_simps]:
eberlm@68246
  1927
  assumes "h \<in> o[F](g)"
eberlm@68246
  1928
  shows   "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f"
eberlm@68246
  1929
  using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym)
eberlm@68246
  1930
  
eberlm@68246
  1931
lemma asymp_equiv_add_left' [asymp_equiv_simps]:
eberlm@68246
  1932
  assumes "h \<in> o[F](g)"
eberlm@68246
  1933
  shows   "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f"
eberlm@68246
  1934
  using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym)
eberlm@68246
  1935
eberlm@68246
  1936
lemma smallo_imp_asymp_equiv:
eberlm@68246
  1937
  assumes "(\<lambda>x. f x - g x) \<in> o[F](g)"
eberlm@68246
  1938
  shows   "f \<sim>[F] g"
eberlm@68246
  1939
proof -
eberlm@68246
  1940
  from assms have "(\<lambda>x. f x - g x + g x) \<sim>[F] g"
eberlm@68246
  1941
    by (subst asymp_equiv_add_left) simp_all
eberlm@68246
  1942
  thus ?thesis by simp
eberlm@68246
  1943
qed
eberlm@68246
  1944
eberlm@68246
  1945
lemma asymp_equiv_uminus [asymp_equiv_intros]:
eberlm@68246
  1946
  "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. -f x) \<sim>[F] (\<lambda>x. -g x)"
eberlm@68246
  1947
  by (simp add: asymp_equiv_def cong: if_cong)
eberlm@68246
  1948
eberlm@68246
  1949
lemma asymp_equiv_uminus_iff [asymp_equiv_simps]:
eberlm@68246
  1950
  "(\<lambda>x. -f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] (\<lambda>x. -g x)"
eberlm@68246
  1951
  by (simp add: asymp_equiv_def cong: if_cong)
eberlm@68246
  1952
eberlm@68246
  1953
lemma asymp_equiv_mult [asymp_equiv_intros]:
eberlm@68246
  1954
  fixes f1 f2 g1 g2 :: "'a \<Rightarrow> 'b :: real_normed_field"
eberlm@68246
  1955
  assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
eberlm@68246
  1956
  shows   "(\<lambda>x. f1 x * f2 x) \<sim>[F] (\<lambda>x. g1 x * g2 x)"
eberlm@68246
  1957
proof -
eberlm@68246
  1958
  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  1959
  let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x
eberlm@68246
  1960
                   else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)"
eberlm@68246
  1961
  let ?S' = "\<lambda>x. ?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) x - ?T f1 g1 x * ?T f2 g2 x"
eberlm@68246
  1962
  {
eberlm@68246
  1963
    fix f g :: "'a \<Rightarrow> 'b" assume "f \<sim>[F] g"
eberlm@68246
  1964
    have "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F"
eberlm@68246
  1965
      by (rule tendsto_eq_intros refl asymp_equivD[OF \<open>f \<sim>[F] g\<close>])+ simp_all
eberlm@68246
  1966
  } note A = this    
eberlm@68246
  1967
eberlm@68246
  1968
  from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"
eberlm@68246
  1969
    by (intro tendsto_mult asymp_equivD)
eberlm@68246
  1970
  moreover {
eberlm@68246
  1971
    have "eventually (\<lambda>x. ?S x = ?S' x) F"
eberlm@68246
  1972
      using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
eberlm@68246
  1973
    moreover have "(?S \<longlongrightarrow> 0) F"
eberlm@68246
  1974
      by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])
eberlm@68246
  1975
         (auto intro: le_infI1 le_infI2)
eberlm@68246
  1976
    ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)
eberlm@68246
  1977
  }
eberlm@68246
  1978
  ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"
eberlm@68246
  1979
    by (rule Lim_transform)
eberlm@68246
  1980
  thus ?thesis by (simp add: asymp_equiv_def)
eberlm@68246
  1981
qed
eberlm@68246
  1982
eberlm@68246
  1983
lemma asymp_equiv_power [asymp_equiv_intros]:
eberlm@68246
  1984
  "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)"
eberlm@68246
  1985
  by (induction n) (simp_all add: asymp_equiv_mult)
eberlm@68246
  1986
eberlm@68246
  1987
lemma asymp_equiv_inverse [asymp_equiv_intros]:
eberlm@68246
  1988
  assumes "f \<sim>[F] g"
eberlm@68246
  1989
  shows   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
eberlm@68246
  1990
proof -
eberlm@68246
  1991
  from tendsto_inverse[OF asymp_equivD[OF assms]]
eberlm@68246
  1992
    have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) \<longlongrightarrow> 1) F"
eberlm@68246
  1993
    by (simp add: if_distrib cong: if_cong)
eberlm@68246
  1994
  also have "(\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) =
eberlm@68246
  1995
               (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else inverse (f x) / inverse (g x))"
eberlm@68246
  1996
    by (intro ext) (simp add: field_simps)
eberlm@68246
  1997
  finally show ?thesis by (simp add: asymp_equiv_def)
eberlm@68246
  1998
qed
eberlm@68246
  1999
eberlm@68246
  2000
lemma asymp_equiv_inverse_iff [asymp_equiv_simps]:
eberlm@68246
  2001
  "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<sim>[F] g"
eberlm@68246
  2002
proof
eberlm@68246
  2003
  assume "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
eberlm@68246
  2004
  hence "(\<lambda>x. inverse (inverse (f x))) \<sim>[F] (\<lambda>x. inverse (inverse (g x)))" (is ?P)
eberlm@68246
  2005
    by (rule asymp_equiv_inverse)
eberlm@68246
  2006
  also have "?P \<longleftrightarrow> f \<sim>[F] g" by (intro asymp_equiv_cong) simp_all
eberlm@68246
  2007
  finally show "f \<sim>[F] g" .
eberlm@68246
  2008
qed (simp_all add: asymp_equiv_inverse)
eberlm@68246
  2009
eberlm@68246
  2010
lemma asymp_equiv_divide [asymp_equiv_intros]:
eberlm@68246
  2011
  assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
eberlm@68246
  2012
  shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
eberlm@68246
  2013
  using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
eberlm@68246
  2014
eberlm@68246
  2015
lemma asymp_equiv_compose [asymp_equiv_intros]:
eberlm@68246
  2016
  assumes "f \<sim>[G] g" "filterlim h G F"
eberlm@68246
  2017
  shows   "f \<circ> h \<sim>[F] g \<circ> h"
eberlm@68246
  2018
proof -
eberlm@68246
  2019
  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  2020
  have "f \<circ> h \<sim>[F] g \<circ> h \<longleftrightarrow> ((?T f g \<circ> h) \<longlongrightarrow> 1) F"
eberlm@68246
  2021
    by (simp add: asymp_equiv_def o_def)
eberlm@68246
  2022
  also have "\<dots> \<longleftrightarrow> (?T f g \<longlongrightarrow> 1) (filtermap h F)"
eberlm@68246
  2023
    by (rule tendsto_compose_filtermap)
eberlm@68246
  2024
  also have "\<dots>"
eberlm@68246
  2025
    by (rule tendsto_mono[of _ G]) (insert assms, simp_all add: asymp_equiv_def filterlim_def)
eberlm@68246
  2026
  finally show ?thesis .
eberlm@68246
  2027
qed
eberlm@68246
  2028
eberlm@68246
  2029
lemma asymp_equiv_compose':
eberlm@68246
  2030
  assumes "f \<sim>[G] g" "filterlim h G F"
eberlm@68246
  2031
  shows   "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
eberlm@68246
  2032
  using asymp_equiv_compose[OF assms] by (simp add: o_def)
eberlm@68246
  2033
  
eberlm@68246
  2034
lemma asymp_equiv_powr_real [asymp_equiv_intros]:
eberlm@68246
  2035
  fixes f g :: "'a \<Rightarrow> real"
eberlm@68246
  2036
  assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
eberlm@68246
  2037
  shows   "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"
eberlm@68246
  2038
proof -
eberlm@68246
  2039
  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  2040
  have "eventually (\<lambda>x. ?T f g x powr y = ?T (\<lambda>x. f x powr y) (\<lambda>x. g x powr y) x) F"
eberlm@68246
  2041
    using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)
eberlm@68246
  2042
    by eventually_elim (auto simp: powr_divide)
eberlm@68246
  2043
  moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
eberlm@68246
  2044
    by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
eberlm@68246
  2045
  hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
eberlm@68246
  2046
  ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
eberlm@68246
  2047
qed
eberlm@68246
  2048
eberlm@68246
  2049
lemma asymp_equiv_norm [asymp_equiv_intros]:
eberlm@68246
  2050
  fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
eberlm@68246
  2051
  assumes "f \<sim>[F] g"
eberlm@68246
  2052
  shows   "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))"
eberlm@68246
  2053
  using tendsto_norm[OF asymp_equivD[OF assms]] 
eberlm@68246
  2054
  by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong)
eberlm@68246
  2055
eberlm@68246
  2056
lemma asymp_equiv_abs_real [asymp_equiv_intros]:
eberlm@68246
  2057
  fixes f g :: "'a \<Rightarrow> real"
eberlm@68246
  2058
  assumes "f \<sim>[F] g"
eberlm@68246
  2059
  shows   "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)"
eberlm@68246
  2060
  using tendsto_rabs[OF asymp_equivD[OF assms]] 
eberlm@68246
  2061
  by (simp add: if_distrib asymp_equiv_def cong: if_cong)
eberlm@68246
  2062
eberlm@68246
  2063
lemma asymp_equiv_imp_eventually_le:
eberlm@68246
  2064
  assumes "f \<sim>[F] g" "c > 1"
eberlm@68246
  2065
  shows   "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"
eberlm@68246
  2066
proof -
eberlm@68246
  2067
  from order_tendstoD(2)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
eberlm@68246
  2068
       asymp_equiv_eventually_zeros[OF assms(1)]
eberlm@68246
  2069
    show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
eberlm@68246
  2070
qed
eberlm@68246
  2071
eberlm@68246
  2072
lemma asymp_equiv_imp_eventually_ge:
eberlm@68246
  2073
  assumes "f \<sim>[F] g" "c < 1"
eberlm@68246
  2074
  shows   "eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F"
eberlm@68246
  2075
proof -
eberlm@68246
  2076
  from order_tendstoD(1)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
eberlm@68246
  2077
       asymp_equiv_eventually_zeros[OF assms(1)]
eberlm@68246
  2078
    show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
eberlm@68246
  2079
qed
eberlm@68246
  2080
eberlm@68246
  2081
lemma asymp_equiv_imp_bigo:
eberlm@68246
  2082
  assumes "f \<sim>[F] g"
eberlm@68246
  2083
  shows   "f \<in> O[F](g)"
eberlm@68246
  2084
proof (rule bigoI)
eberlm@68246
  2085
  have "(3/2::real) > 1" by simp
eberlm@68246
  2086
  from asymp_equiv_imp_eventually_le[OF assms this]
eberlm@68246
  2087
    show "eventually (\<lambda>x. norm (f x) \<le> 3/2 * norm (g x)) F"
eberlm@68246
  2088
    by eventually_elim simp
eberlm@68246
  2089
qed
eberlm@68246
  2090
eberlm@68246
  2091
lemma asymp_equiv_imp_bigomega:
eberlm@68246
  2092
  "f \<sim>[F] g \<Longrightarrow> f \<in> \<Omega>[F](g)"
eberlm@68246
  2093
  using asymp_equiv_imp_bigo[of g F f] by (simp add: asymp_equiv_sym bigomega_iff_bigo)
eberlm@68246
  2094
eberlm@68246
  2095
lemma asymp_equiv_imp_bigtheta:
eberlm@68246
  2096
  "f \<sim>[F] g \<Longrightarrow> f \<in> \<Theta>[F](g)"
eberlm@68246
  2097
  by (intro bigthetaI asymp_equiv_imp_bigo asymp_equiv_imp_bigomega)
eberlm@68246
  2098
eberlm@68246
  2099
lemma asymp_equiv_at_infinity_transfer:
eberlm@68246
  2100
  assumes "f \<sim>[F] g" "filterlim f at_infinity F"
eberlm@68246
  2101
  shows   "filterlim g at_infinity F"
eberlm@68246
  2102
proof -
eberlm@68246
  2103
  from assms(1) have "g \<in> \<Theta>[F](f)" by (rule asymp_equiv_imp_bigtheta[OF asymp_equiv_symI])
eberlm@68246
  2104
  also from assms have "f \<in> \<omega>[F](\<lambda>_. 1)" by (simp add: smallomega_1_conv_filterlim)
eberlm@68246
  2105
  finally show ?thesis by (simp add: smallomega_1_conv_filterlim)
eberlm@68246
  2106
qed
eberlm@68246
  2107
eberlm@68246
  2108
lemma asymp_equiv_at_top_transfer:
eberlm@68246
  2109
  fixes f g :: "_ \<Rightarrow> real"
eberlm@68246
  2110
  assumes "f \<sim>[F] g" "filterlim f at_top F"
eberlm@68246
  2111
  shows   "filterlim g at_top F"
eberlm@68246
  2112
proof (rule filterlim_at_infinity_imp_filterlim_at_top)
eberlm@68246
  2113
  show "filterlim g at_infinity F"
eberlm@68246
  2114
    by (rule asymp_equiv_at_infinity_transfer[OF assms(1) filterlim_mono[OF assms(2)]])
eberlm@68246
  2115
       (auto simp: at_top_le_at_infinity)
eberlm@68246
  2116
  from assms(2) have "eventually (\<lambda>x. f x > 0) F"
eberlm@68246
  2117
    using filterlim_at_top_dense by blast
eberlm@68246
  2118
  with asymp_equiv_eventually_pos_iff[OF assms(1)] show "eventually (\<lambda>x. g x > 0) F"
eberlm@68246
  2119
    by eventually_elim blast
eberlm@68246
  2120
qed
eberlm@68246
  2121
eberlm@68246
  2122
lemma asymp_equiv_at_bot_transfer:
eberlm@68246
  2123
  fixes f g :: "_ \<Rightarrow> real"
eberlm@68246
  2124
  assumes "f \<sim>[F] g" "filterlim f at_bot F"
eberlm@68246
  2125
  shows   "filterlim g at_bot F"
eberlm@68246
  2126
  unfolding filterlim_uminus_at_bot
eberlm@68246
  2127
  by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"])
eberlm@68246
  2128
     (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus)  
eberlm@68246
  2129
eberlm@68246
  2130
lemma asymp_equivI'_const:
eberlm@68246
  2131
  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0"
eberlm@68246
  2132
  shows   "f \<sim>[F] (\<lambda>x. c * g x)"
eberlm@68246
  2133
  using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2)
eberlm@68246
  2134
  by (intro asymp_equivI') (simp add: field_simps)
eberlm@68246
  2135
eberlm@68246
  2136
lemma asymp_equivI'_inverse_const:
eberlm@68246
  2137
  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> inverse c) F" "c \<noteq> 0"
eberlm@68246
  2138
  shows   "(\<lambda>x. c * f x) \<sim>[F] g"
eberlm@68246
  2139
  using tendsto_mult[OF assms(1) tendsto_const[of "c"]] assms(2)
eberlm@68246
  2140
  by (intro asymp_equivI') (simp add: field_simps)
eberlm@68246
  2141
eberlm@68246
  2142
lemma filterlim_at_bot_imp_at_infinity: "filterlim f at_bot F \<Longrightarrow> filterlim f at_infinity F"
eberlm@68246
  2143
  for f :: "_ \<Rightarrow> real" using at_bot_le_at_infinity filterlim_mono by blast
eberlm@68246
  2144
eberlm@68246
  2145
lemma asymp_equiv_imp_diff_smallo:
eberlm@68246
  2146
  assumes "f \<sim>[F] g"
eberlm@68246
  2147
  shows   "(\<lambda>x. f x - g x) \<in> o[F](g)"
eberlm@68246
  2148
proof (rule landau_o.smallI)
eberlm@68246
  2149
  fix c :: real assume "c > 0"
eberlm@68246
  2150
  hence c: "min c 1 > 0" by simp
eberlm@68246
  2151
  let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  2152
  from assms have "((\<lambda>x. ?h x - 1) \<longlongrightarrow> 1 - 1) F"
eberlm@68246
  2153
    by (intro tendsto_diff asymp_equivD tendsto_const)
eberlm@68246
  2154
  from tendstoD[OF this c] show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
eberlm@68246
  2155
  proof eventually_elim
eberlm@68246
  2156
    case (elim x)
eberlm@68246
  2157
    from elim have "norm (f x - g x) \<le> norm (f x / g x - 1) * norm (g x)"
eberlm@68246
  2158
      by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps)
eberlm@68246
  2159
    also have "norm (f x / g x - 1) * norm (g x) \<le> c * norm (g x)" using elim
eberlm@68246
  2160
      by (auto split: if_splits simp: mult_right_mono)
eberlm@68246
  2161
    finally show ?case .
eberlm@68246
  2162
  qed
eberlm@68246
  2163
qed
eberlm@68246
  2164
eberlm@68246
  2165
lemma asymp_equiv_altdef:
eberlm@68246
  2166
  "f \<sim>[F] g \<longleftrightarrow> (\<lambda>x. f x - g x) \<in> o[F](g)"
eberlm@68246
  2167
  by (rule iffI[OF asymp_equiv_imp_diff_smallo smallo_imp_asymp_equiv])
eberlm@68246
  2168
eberlm@68246
  2169
lemma asymp_equiv_0_left_iff [simp]: "(\<lambda>_. 0) \<sim>[F] f \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  2170
  and asymp_equiv_0_right_iff [simp]: "f \<sim>[F] (\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  2171
  by (simp_all add: asymp_equiv_altdef landau_o.small_refl_iff)
eberlm@68246
  2172
eberlm@68246
  2173
lemma asymp_equiv_sandwich_real:
eberlm@68246
  2174
  fixes f g l u :: "'a \<Rightarrow> real"
eberlm@68246
  2175
  assumes "l \<sim>[F] g" "u \<sim>[F] g" "eventually (\<lambda>x. f x \<in> {l x..u x}) F"
eberlm@68246
  2176
  shows   "f \<sim>[F] g"
eberlm@68246
  2177
  unfolding asymp_equiv_altdef
eberlm@68246
  2178
proof (rule landau_o.smallI)
eberlm@68246
  2179
  fix c :: real assume c: "c > 0"
eberlm@68246
  2180
  have "eventually (\<lambda>x. norm (f x - g x) \<le> max (norm (l x - g x)) (norm (u x - g x))) F"
eberlm@68246
  2181
    using assms(3) by eventually_elim auto
eberlm@68246
  2182
  moreover have "eventually (\<lambda>x. norm (l x - g x) \<le> c * norm (g x)) F"
eberlm@68246
  2183
                "eventually (\<lambda>x. norm (u x - g x) \<le> c * norm (g x)) F"
eberlm@68246
  2184
    using assms(1,2) by (auto simp: asymp_equiv_altdef dest: landau_o.smallD[OF _ c])
eberlm@68246
  2185
  hence "eventually (\<lambda>x. max (norm (l x - g x)) (norm (u x - g x)) \<le> c * norm (g x)) F"
eberlm@68246
  2186
    by eventually_elim simp
eberlm@68246
  2187
  ultimately show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
eberlm@68246
  2188
    by eventually_elim (rule order.trans)
eberlm@68246
  2189
qed
eberlm@68246
  2190
eberlm@68246
  2191
lemma asymp_equiv_sandwich_real':
eberlm@68246
  2192
  fixes f g l u :: "'a \<Rightarrow> real"
eberlm@68246
  2193
  assumes "f \<sim>[F] l" "f \<sim>[F] u" "eventually (\<lambda>x. g x \<in> {l x..u x}) F"
eberlm@68246
  2194
  shows   "f \<sim>[F] g"
eberlm@68246
  2195
  using asymp_equiv_sandwich_real[of l F f u g] assms by (simp add: asymp_equiv_sym)
eberlm@68246
  2196
eberlm@68246
  2197
lemma asymp_equiv_sandwich_real'':
eberlm@68246
  2198
  fixes f g l u :: "'a \<Rightarrow> real"
eberlm@68246
  2199
  assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"
eberlm@68246
  2200
          "eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"
eberlm@68246
  2201
  shows   "f \<sim>[F] g"
eberlm@68246
  2202
  by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]
eberlm@68246
  2203
             asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];
eberlm@68246
  2204
      blast intro: asymp_equiv_trans assms(1,2,3))+
eberlm@68246
  2205
eberlm@68246
  2206
end