src/HOL/Library/Landau_Symbols.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 68406 6beb45f6cf67
child 68696 8a071eeddb2a
permissions -rw-r--r--
tuned equation
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
*)
eberlm@68246
     7
section {* Definition of Landau symbols *}
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
eberlm@68246
    19
subsection {* Definition of Landau symbols *}
eberlm@68246
    20
eberlm@68246
    21
text {*
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.
eberlm@68246
    26
*}
eberlm@68246
    27
eberlm@68246
    28
definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
eberlm@68246
    29
    ("(1O[_]'(_'))")
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" 
eberlm@68246
    33
    ("(1o[_]'(_'))")
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" 
eberlm@68246
    37
    ("(1\<Omega>[_]'(_'))")
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" 
eberlm@68246
    41
    ("(1\<omega>[_]'(_'))")
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" 
eberlm@68246
    45
    ("(1\<Theta>[_]'(_'))")
eberlm@68246
    46
  where "bigtheta F g = bigo F g \<inter> bigomega F g"
eberlm@68246
    47
eberlm@68246
    48
abbreviation bigo_at_top ("(2O'(_'))") where
eberlm@68246
    49
  "O(g) \<equiv> bigo at_top g"    
eberlm@68246
    50
eberlm@68246
    51
abbreviation smallo_at_top ("(2o'(_'))") where
eberlm@68246
    52
  "o(g) \<equiv> smallo at_top g"
eberlm@68246
    53
eberlm@68246
    54
abbreviation bigomega_at_top ("(2\<Omega>'(_'))") where
eberlm@68246
    55
  "\<Omega>(g) \<equiv> bigomega at_top g"
eberlm@68246
    56
eberlm@68246
    57
abbreviation smallomega_at_top ("(2\<omega>'(_'))") where
eberlm@68246
    58
  "\<omega>(g) \<equiv> smallomega at_top g"
eberlm@68246
    59
eberlm@68246
    60
abbreviation bigtheta_at_top ("(2\<Theta>'(_'))") where
eberlm@68246
    61
  "\<Theta>(g) \<equiv> bigtheta at_top g"
eberlm@68246
    62
    
eberlm@68246
    63
eberlm@68246
    64
text {* The following is a set of properties that all Landau symbols satisfy. *}
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
eberlm@68246
   293
text {* 
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.
eberlm@68246
   297
*}
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"
eberlm@68246
   609
    from `c \<noteq> 0` 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"
eberlm@68246
   614
    from `c \<noteq> 0` 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
      
eberlm@68246
   634
      thm eventually_subst A
eberlm@68246
   635
      by (subst eventually_subst'[OF A]) (rule refl)
eberlm@68246
   636
  }
eberlm@68246
   637
  {
eberlm@68246
   638
    fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
eberlm@68246
   639
    show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" unfolding L_def mem_Collect_eq
eberlm@68246
   640
      by (subst (1) eventually_subst'[OF A]) (rule refl)
eberlm@68246
   641
  }
eberlm@68246
   642
  {
eberlm@68246
   643
    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" thus "L F f \<subseteq> L F g" by (rule big_subsetI)
eberlm@68246
   644
  }
eberlm@68246
   645
  {
eberlm@68246
   646
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
eberlm@68246
   647
    with A L show "L F (f) = L F (g)" unfolding bigtheta_def
eberlm@68246
   648
      by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo)
eberlm@68246
   649
    fix h:: "'a \<Rightarrow> 'b"
eberlm@68246
   650
    show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" by (rule disjE[OF L]) 
eberlm@68246
   651
      (insert A, auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans)
eberlm@68246
   652
  }
eberlm@68246
   653
  {
eberlm@68246
   654
    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g"
eberlm@68246
   655
    thus "(\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" by (intro big_mult) simp
eberlm@68246
   656
  }
eberlm@68246
   657
  {
eberlm@68246
   658
    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" "g \<in> L F h"
eberlm@68246
   659
    thus "f \<in> L F (h)" by (rule big_trans)
eberlm@68246
   660
  }
eberlm@68246
   661
  {
eberlm@68246
   662
    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
eberlm@68246
   663
    assume "f \<in> L F g" and "filterlim h F G"
eberlm@68246
   664
    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
   665
  }
eberlm@68246
   666
  {
eberlm@68246
   667
    fix f g :: "'a \<Rightarrow> 'b" and F G :: "'a filter"
eberlm@68246
   668
    assume "f \<in> L F g" "f \<in> L G g"
eberlm@68246
   669
    from this [THEN bigE] guess c1 c2 . note c12 = this
eberlm@68246
   670
    define c where "c = (if R c1 c2 then c2 else c1)"
eberlm@68246
   671
    from c12 have c: "R c1 c" "R c2 c" "c > 0" by (auto simp: c_def dest: R_linear)
eberlm@68246
   672
    with c12(2,4) have "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
eberlm@68246
   673
                     "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) G"
eberlm@68246
   674
      by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+
eberlm@68246
   675
    with c show "f \<in> L (sup F G) g" by (auto simp: L_def eventually_sup)
eberlm@68246
   676
  }
eberlm@68246
   677
  {
eberlm@68246
   678
    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
eberlm@68246
   679
    assume "(f \<in> L F g)"
eberlm@68246
   680
    thus "((\<lambda>x. f (h x)) \<in> L' (filtercomap h F) (\<lambda>x. g (h x)))"
eberlm@68246
   681
      unfolding L_def L'_def by auto
eberlm@68246
   682
  }
eberlm@68246
   683
qed (auto simp: L_def Lr_def eventually_filtermap L'_def
eberlm@68246
   684
          intro: filter_leD exI[of _ "1::real"])
eberlm@68246
   685
eberlm@68246
   686
sublocale small: landau_symbol l l' lr
eberlm@68246
   687
proof
eberlm@68246
   688
  {
eberlm@68246
   689
    fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
eberlm@68246
   690
    hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
eberlm@68246
   691
  } note A = this
eberlm@68246
   692
  {
eberlm@68246
   693
    fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
eberlm@68246
   694
    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
eberlm@68246
   695
      show "l F (\<lambda>x. c * f x) = l F f" 
eberlm@68246
   696
        by (intro equalityI small_subsetI) (simp_all add: field_simps)
eberlm@68246
   697
  }
eberlm@68246
   698
  {
eberlm@68246
   699
    fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
eberlm@68246
   700
    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
eberlm@68246
   701
      have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
eberlm@68246
   702
    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
   703
  }
eberlm@68246
   704
  {
eberlm@68246
   705
    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
eberlm@68246
   706
    with plus_aux show "l F g \<subseteq> l F (\<lambda>x. f x + g x)" by (blast intro!: small_subsetI) 
eberlm@68246
   707
  }
eberlm@68246
   708
  {
eberlm@68246
   709
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> l F (g)"
eberlm@68246
   710
    assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
   711
    show "(\<lambda>x. inverse (g x)) \<in> l F (\<lambda>x. inverse (f x))"
eberlm@68246
   712
    proof (rule smallI)
eberlm@68246
   713
      fix c :: real assume c: "c > 0"
eberlm@68246
   714
      from B smallD[OF A c] 
eberlm@68246
   715
        show "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
eberlm@68246
   716
        by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide)
eberlm@68246
   717
    qed
eberlm@68246
   718
  }
eberlm@68246
   719
  {
eberlm@68246
   720
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
eberlm@68246
   721
    show "l F (f) = l F (g)" unfolding l_def by (subst eventually_subst'[OF A]) (rule refl)
eberlm@68246
   722
  }
eberlm@68246
   723
  {
eberlm@68246
   724
    fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
eberlm@68246
   725
    show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" unfolding l_def mem_Collect_eq
eberlm@68246
   726
      by (subst (1) eventually_subst'[OF A]) (rule refl)
eberlm@68246
   727
  }
eberlm@68246
   728
  {
eberlm@68246
   729
    fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" 
eberlm@68246
   730
    thus "l F f \<subseteq> l F g" by (intro small_subsetI small_imp_big)
eberlm@68246
   731
  }
eberlm@68246
   732
  {
eberlm@68246
   733
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
eberlm@68246
   734
    have L: "L = bigo \<or> L = bigomega"
eberlm@68246
   735
      by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
eberlm@68246
   736
    with A show "l F (f) = l F (g)" unfolding bigtheta_def
eberlm@68246
   737
      by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo)
eberlm@68246
   738
    have l: "l = smallo \<or> l = smallomega"
eberlm@68246
   739
      by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff)
eberlm@68246
   740
    fix h:: "'a \<Rightarrow> 'b"
eberlm@68246
   741
    show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" by (rule disjE[OF l]) 
eberlm@68246
   742
      (insert A, auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo 
eberlm@68246
   743
       intro: landau_o.big_small_trans landau_o.small_big_trans)
eberlm@68246
   744
  }
eberlm@68246
   745
  {
eberlm@68246
   746
    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g"
eberlm@68246
   747
    thus "(\<lambda>x. h x * f x) \<in> l F (\<lambda>x. h x * g x)" by (intro big_small_mult) simp
eberlm@68246
   748
  }
eberlm@68246
   749
  {
eberlm@68246
   750
    fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" "g \<in> l F h"
eberlm@68246
   751
    thus "f \<in> l F (h)" by (rule small_trans)
eberlm@68246
   752
  }
eberlm@68246
   753
  {
eberlm@68246
   754
    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
eberlm@68246
   755
    assume "f \<in> l F g" and "filterlim h F G"
eberlm@68246
   756
    thus "(\<lambda>x. f (h x)) \<in> l' G (\<lambda>x. g (h x))"
eberlm@68246
   757
      by (auto simp: l_def l'_def filterlim_iff)
eberlm@68246
   758
  }
eberlm@68246
   759
  {
eberlm@68246
   760
    fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
eberlm@68246
   761
    assume "(f \<in> l F g)"
eberlm@68246
   762
    thus "((\<lambda>x. f (h x)) \<in> l' (filtercomap h F) (\<lambda>x. g (h x)))"
eberlm@68246
   763
      unfolding l_def l'_def by auto
eberlm@68246
   764
  }
eberlm@68246
   765
qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)
eberlm@68246
   766
eberlm@68246
   767
eberlm@68246
   768
text {* These rules allow chaining of Landau symbol propositions in Isar with "also".*}
eberlm@68246
   769
eberlm@68246
   770
lemma big_mult_1:    "f \<in> L F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
eberlm@68246
   771
  and big_mult_1':   "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
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
  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
   775
  and small_mult_1''': "(\<lambda>_. 1) \<in> l F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
eberlm@68246
   776
  by (drule (1) big.mult big_small_mult small_big_mult, simp)+
eberlm@68246
   777
eberlm@68246
   778
lemma big_1_mult:    "f \<in> L F (g) \<Longrightarrow> h \<in> L F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
eberlm@68246
   779
  and big_1_mult':   "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
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
  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
   783
  and small_1_mult''': "h \<in> l F (\<lambda>_. 1) \<Longrightarrow> f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"
eberlm@68246
   784
  by (drule (1) big.mult big_small_mult small_big_mult, simp)+
eberlm@68246
   785
eberlm@68246
   786
lemmas mult_1_trans = 
eberlm@68246
   787
  big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1'''
eberlm@68246
   788
  big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult'''
eberlm@68246
   789
eberlm@68246
   790
lemma big_equal_iff_bigtheta: "L F (f) = L F (g) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
eberlm@68246
   791
proof
eberlm@68246
   792
  have L: "L = bigo \<or> L = bigomega"
eberlm@68246
   793
    by (rule R_E) (auto simp: fun_eq_iff L_def bigo_def bigomega_def)
eberlm@68246
   794
  fix f g :: "'a \<Rightarrow> 'b" assume "L F (f) = L F (g)"
eberlm@68246
   795
  with big_refl[of f F] big_refl[of g F] have "f \<in> L F (g)" "g \<in> L F (f)" by simp_all
eberlm@68246
   796
  thus "f \<in> \<Theta>[F](g)" using L unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
eberlm@68246
   797
qed (rule big.cong_bigtheta)
eberlm@68246
   798
eberlm@68246
   799
lemma big_prod:
eberlm@68246
   800
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (g x)"
eberlm@68246
   801
  shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>y. \<Prod>x\<in>A. g x y)"
eberlm@68246
   802
  using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult)
eberlm@68246
   803
eberlm@68246
   804
lemma big_prod_in_1:
eberlm@68246
   805
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (\<lambda>_. 1)"
eberlm@68246
   806
  shows   "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>_. 1)"
eberlm@68246
   807
  using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult_in_1)
eberlm@68246
   808
eberlm@68246
   809
end
eberlm@68246
   810
eberlm@68246
   811
eberlm@68246
   812
context landau_symbol
eberlm@68246
   813
begin
eberlm@68246
   814
  
eberlm@68246
   815
lemma plus_absorb1:
eberlm@68246
   816
  assumes "f \<in> o[F](g)"
eberlm@68246
   817
  shows   "L F (\<lambda>x. f x + g x) = L F (g)"
eberlm@68246
   818
proof (intro equalityI)
eberlm@68246
   819
  from plus_subset1 and assms show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" .
eberlm@68246
   820
  from landau_o.small.plus_subset1[OF assms] and assms have "(\<lambda>x. -f x) \<in> o[F](\<lambda>x. f x + g x)"
eberlm@68246
   821
    by (auto simp: landau_o.small.uminus_in_iff)
eberlm@68246
   822
  from plus_subset1[OF this] show "L F (\<lambda>x. f x + g x) \<subseteq> L F (g)" by simp
eberlm@68246
   823
qed
eberlm@68246
   824
eberlm@68246
   825
lemma plus_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x + g x) = L F (f)"
eberlm@68246
   826
  using plus_absorb1[of g F f] by (simp add: add.commute)
eberlm@68246
   827
eberlm@68246
   828
lemma diff_absorb1: "f \<in> o[F](g) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (g)"
eberlm@68246
   829
  by (simp only: diff_conv_add_uminus plus_absorb1 landau_o.small.uminus uminus)
eberlm@68246
   830
eberlm@68246
   831
lemma diff_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (f)"
eberlm@68246
   832
  by (simp only: diff_conv_add_uminus plus_absorb2 landau_o.small.uminus_in_iff)
eberlm@68246
   833
eberlm@68246
   834
lemmas absorb = plus_absorb1 plus_absorb2 diff_absorb1 diff_absorb2
eberlm@68246
   835
eberlm@68246
   836
end
eberlm@68246
   837
eberlm@68246
   838
eberlm@68246
   839
lemma bigthetaI [intro]: "f \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> \<Theta>[F](g)"
eberlm@68246
   840
  unfolding bigtheta_def bigomega_def by blast
eberlm@68246
   841
eberlm@68246
   842
lemma bigthetaD1 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> O[F](g)" 
eberlm@68246
   843
  and bigthetaD2 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g)"
eberlm@68246
   844
  unfolding bigtheta_def bigo_def bigomega_def by blast+
eberlm@68246
   845
eberlm@68246
   846
lemma bigtheta_refl [simp]: "f \<in> \<Theta>[F](f)"
eberlm@68246
   847
  unfolding bigtheta_def by simp
eberlm@68246
   848
eberlm@68246
   849
lemma bigtheta_sym: "f \<in> \<Theta>[F](g) \<longleftrightarrow> g \<in> \<Theta>[F](f)"
eberlm@68246
   850
  unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
eberlm@68246
   851
eberlm@68246
   852
lemmas landau_flip =
eberlm@68246
   853
  bigomega_iff_bigo[symmetric] smallomega_iff_smallo[symmetric]
eberlm@68246
   854
  bigomega_iff_bigo smallomega_iff_smallo bigtheta_sym
eberlm@68246
   855
eberlm@68246
   856
eberlm@68246
   857
interpretation landau_theta: landau_symbol bigtheta bigtheta bigtheta
eberlm@68246
   858
proof
eberlm@68246
   859
  fix f g :: "'a \<Rightarrow> 'b" and F
eberlm@68246
   860
  assume "f \<in> o[F](g)"
eberlm@68246
   861
  hence "O[F](g) \<subseteq> O[F](\<lambda>x. f x + g x)" "\<Omega>[F](g) \<subseteq> \<Omega>[F](\<lambda>x. f x + g x)"
eberlm@68246
   862
    by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+
eberlm@68246
   863
  thus "\<Theta>[F](g) \<subseteq> \<Theta>[F](\<lambda>x. f x + g x)" unfolding bigtheta_def by blast
eberlm@68246
   864
next
eberlm@68246
   865
  fix f g :: "'a \<Rightarrow> 'b" and F 
eberlm@68246
   866
  assume "f \<in> \<Theta>[F](g)"
eberlm@68246
   867
  thus A: "\<Theta>[F](f) = \<Theta>[F](g)" 
eberlm@68246
   868
    apply (subst (1 2) bigtheta_def)
eberlm@68246
   869
    apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+
eberlm@68246
   870
    apply (rule refl)
eberlm@68246
   871
    done
eberlm@68246
   872
  thus "\<Theta>[F](f) \<subseteq> \<Theta>[F](g)" by simp
eberlm@68246
   873
  fix h :: "'a \<Rightarrow> 'b"
eberlm@68246
   874
  show "f \<in> \<Theta>[F](h) \<longleftrightarrow> g \<in> \<Theta>[F](h)" by (subst (1 2) bigtheta_sym) (simp add: A)
eberlm@68246
   875
next
eberlm@68246
   876
  fix f g h :: "'a \<Rightarrow> 'b" and F
eberlm@68246
   877
  assume "f \<in> \<Theta>[F](g)" "g \<in> \<Theta>[F](h)"
eberlm@68246
   878
  thus "f \<in> \<Theta>[F](h)" unfolding bigtheta_def
eberlm@68246
   879
    by (blast intro: landau_o.big.trans landau_omega.big.trans)
eberlm@68246
   880
next
eberlm@68246
   881
  fix f :: "'a \<Rightarrow> 'b" and F1 F2 :: "'a filter"
eberlm@68246
   882
  assume "F1 \<le> F2"
eberlm@68246
   883
  thus "\<Theta>[F2](f) \<subseteq> \<Theta>[F1](f)"
eberlm@68246
   884
    by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono)
eberlm@68246
   885
qed (auto simp: bigtheta_def landau_o.big.norm_iff 
eberlm@68246
   886
                landau_o.big.cmult landau_omega.big.cmult 
eberlm@68246
   887
                landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff 
eberlm@68246
   888
                landau_o.big.in_cong landau_omega.big.in_cong
eberlm@68246
   889
                landau_o.big.mult landau_omega.big.mult
eberlm@68246
   890
                landau_o.big.inverse landau_omega.big.inverse 
eberlm@68246
   891
                landau_o.big.compose landau_omega.big.compose
eberlm@68246
   892
                landau_o.big.bot' landau_omega.big.bot'
eberlm@68246
   893
                landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff
eberlm@68246
   894
                landau_o.big.sup landau_omega.big.sup
eberlm@68246
   895
                landau_o.big.filtercomap landau_omega.big.filtercomap
eberlm@68246
   896
          dest: landau_o.big.cong landau_omega.big.cong)
eberlm@68246
   897
eberlm@68246
   898
lemmas landau_symbols = 
eberlm@68246
   899
  landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms
eberlm@68246
   900
  landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms 
eberlm@68246
   901
  landau_theta.landau_symbol_axioms
eberlm@68246
   902
eberlm@68246
   903
lemma bigoI [intro]:
eberlm@68246
   904
  assumes "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
eberlm@68246
   905
  shows   "f \<in> O[F](g)"
eberlm@68246
   906
proof (rule landau_o.bigI)
eberlm@68246
   907
  show "max 1 c > 0" by simp
eberlm@68246
   908
  note assms
eberlm@68246
   909
  moreover have "\<And>x. c * (norm (g x)) \<le> max 1 c * (norm (g x))" by (simp add: mult_right_mono)
eberlm@68246
   910
  ultimately show "eventually (\<lambda>x. (norm (f x)) \<le> max 1 c * (norm (g x))) F"
eberlm@68246
   911
    by (auto elim!: eventually_mono dest: order.trans)
eberlm@68246
   912
qed
eberlm@68246
   913
eberlm@68246
   914
lemma smallomegaD [dest]:
eberlm@68246
   915
  assumes "f \<in> \<omega>[F](g)"
eberlm@68246
   916
  shows   "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
eberlm@68246
   917
proof (cases "c > 0")
eberlm@68246
   918
  case False
eberlm@68246
   919
  show ?thesis 
eberlm@68246
   920
    by (intro always_eventually allI, rule order.trans[of _ 0])
eberlm@68246
   921
       (insert False, auto intro!: mult_nonpos_nonneg)
eberlm@68246
   922
qed (blast dest: landau_omega.smallD[OF assms, of c])
eberlm@68246
   923
eberlm@68246
   924
  
eberlm@68246
   925
lemma bigthetaI':
eberlm@68246
   926
  assumes "c1 > 0" "c2 > 0"
eberlm@68246
   927
  assumes "eventually (\<lambda>x. c1 * (norm (g x)) \<le> (norm (f x)) \<and> (norm (f x)) \<le> c2 * (norm (g x))) F"
eberlm@68246
   928
  shows   "f \<in> \<Theta>[F](g)"
eberlm@68246
   929
apply (rule bigthetaI)
eberlm@68246
   930
apply (rule landau_o.bigI[OF assms(2)]) using assms(3) apply (eventually_elim, simp)
eberlm@68246
   931
apply (rule landau_omega.bigI[OF assms(1)]) using assms(3) apply (eventually_elim, simp)
eberlm@68246
   932
done
eberlm@68246
   933
eberlm@68246
   934
lemma bigthetaI_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> \<Theta>[F](g)"
eberlm@68246
   935
  by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono)
eberlm@68246
   936
eberlm@68246
   937
lemma (in landau_symbol) ev_eq_trans1: 
eberlm@68246
   938
  "f \<in> L F (\<lambda>x. g x (h x)) \<Longrightarrow> eventually (\<lambda>x. h x = h' x) F \<Longrightarrow> f \<in> L F (\<lambda>x. g x (h' x))"
eberlm@68246
   939
  by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono)
eberlm@68246
   940
eberlm@68246
   941
lemma (in landau_symbol) ev_eq_trans2: 
eberlm@68246
   942
  "eventually (\<lambda>x. f x = f' x) F \<Longrightarrow> (\<lambda>x. g x (f' x)) \<in> L F (h) \<Longrightarrow> (\<lambda>x. g x (f x)) \<in> L F (h)"
eberlm@68246
   943
  by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono)
eberlm@68246
   944
eberlm@68246
   945
declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro]
eberlm@68246
   946
declare landau_o.bigE landau_omega.bigE [elim]
eberlm@68246
   947
declare landau_o.smallD
eberlm@68246
   948
eberlm@68246
   949
lemma (in landau_symbol) bigtheta_trans1': 
eberlm@68246
   950
  "f \<in> L F (g) \<Longrightarrow> h \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h)"
eberlm@68246
   951
  by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym)
eberlm@68246
   952
eberlm@68246
   953
lemma (in landau_symbol) bigtheta_trans2': 
eberlm@68246
   954
  "g \<in> \<Theta>[F](f) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
eberlm@68246
   955
  by (rule bigtheta_trans2, subst bigtheta_sym)
eberlm@68246
   956
eberlm@68246
   957
lemma bigo_bigomega_trans:      "f \<in> O[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> O[F](h)"
eberlm@68246
   958
  and bigo_smallomega_trans:    "f \<in> O[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
eberlm@68246
   959
  and smallo_bigomega_trans:    "f \<in> o[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
eberlm@68246
   960
  and smallo_smallomega_trans:  "f \<in> o[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
eberlm@68246
   961
  and bigomega_bigo_trans:      "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](h)"
eberlm@68246
   962
  and bigomega_smallo_trans:    "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
eberlm@68246
   963
  and smallomega_bigo_trans:    "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
eberlm@68246
   964
  and smallomega_smallo_trans:  "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
eberlm@68246
   965
  by (unfold bigomega_iff_bigo smallomega_iff_smallo)
eberlm@68246
   966
     (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans 
eberlm@68246
   967
                landau_o.big_trans landau_o.small_trans)+
eberlm@68246
   968
eberlm@68246
   969
lemmas landau_trans_lift [trans] =
eberlm@68246
   970
  landau_symbols[THEN landau_symbol.lift_trans]
eberlm@68246
   971
  landau_symbols[THEN landau_symbol.lift_trans']
eberlm@68246
   972
  landau_symbols[THEN landau_symbol.lift_trans_bigtheta]
eberlm@68246
   973
  landau_symbols[THEN landau_symbol.lift_trans_bigtheta']
eberlm@68246
   974
eberlm@68246
   975
lemmas landau_mult_1_trans [trans] =
eberlm@68246
   976
  landau_o.mult_1_trans landau_omega.mult_1_trans
eberlm@68246
   977
eberlm@68246
   978
lemmas landau_trans [trans] = 
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.bigtheta_trans1']
eberlm@68246
   982
  landau_symbols[THEN landau_symbol.bigtheta_trans2']
eberlm@68246
   983
  landau_symbols[THEN landau_symbol.ev_eq_trans1]
eberlm@68246
   984
  landau_symbols[THEN landau_symbol.ev_eq_trans2]
eberlm@68246
   985
eberlm@68246
   986
  landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans
eberlm@68246
   987
  landau_omega.big_trans landau_omega.small_trans 
eberlm@68246
   988
    landau_omega.small_big_trans landau_omega.big_small_trans
eberlm@68246
   989
eberlm@68246
   990
  bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans 
eberlm@68246
   991
  bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans
eberlm@68246
   992
eberlm@68246
   993
lemma bigtheta_inverse [simp]: 
eberlm@68246
   994
  shows "(\<lambda>x. inverse (f x)) \<in> \<Theta>[F](\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
eberlm@68246
   995
proof-
eberlm@68246
   996
  {
eberlm@68246
   997
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
eberlm@68246
   998
    then guess c1 c2 :: real unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
eberlm@68246
   999
    note c = this
eberlm@68246
  1000
    from c(3) have "inverse c2 > 0" by simp
eberlm@68246
  1001
    moreover from c(2,4)
eberlm@68246
  1002
      have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))) F"
eberlm@68246
  1003
    proof eventually_elim
eberlm@68246
  1004
      fix x assume A: "(norm (f x)) \<le> c1 * (norm (g x))" "c2 * (norm (g x)) \<le> (norm (f x))"
eberlm@68246
  1005
      from A c(1,3) have "f x = 0 \<longleftrightarrow> g x = 0" by (auto simp: field_simps mult_le_0_iff)
eberlm@68246
  1006
      with A c(1,3) show "norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))"
eberlm@68246
  1007
        by (force simp: field_simps norm_inverse norm_divide)
eberlm@68246
  1008
    qed
eberlm@68246
  1009
    ultimately have "(\<lambda>x. inverse (f x)) \<in> O[F](\<lambda>x. inverse (g x))" by (rule landau_o.bigI)
eberlm@68246
  1010
  }
eberlm@68246
  1011
  thus ?thesis unfolding bigtheta_def 
eberlm@68246
  1012
    by (force simp: bigomega_iff_bigo bigtheta_sym)
eberlm@68246
  1013
qed
eberlm@68246
  1014
eberlm@68246
  1015
lemma bigtheta_divide:
eberlm@68246
  1016
  assumes "f1 \<in> \<Theta>(f2)" "g1 \<in> \<Theta>(g2)"
eberlm@68246
  1017
  shows   "(\<lambda>x. f1 x / g1 x) \<in> \<Theta>(\<lambda>x. f2 x / g2 x)"
eberlm@68246
  1018
  by (subst (1 2) divide_inverse, intro landau_theta.mult) (simp_all add: bigtheta_inverse assms)
eberlm@68246
  1019
eberlm@68246
  1020
lemma eventually_nonzero_bigtheta:
eberlm@68246
  1021
  assumes "f \<in> \<Theta>[F](g)"
eberlm@68246
  1022
  shows   "eventually (\<lambda>x. f x \<noteq> 0) F \<longleftrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1023
proof-
eberlm@68246
  1024
  {
eberlm@68246
  1025
    fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)" and B: "eventually (\<lambda>x. f x \<noteq> 0) F"
eberlm@68246
  1026
    from A guess c1 c2 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
eberlm@68246
  1027
    from B this(2,4) have "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim auto
eberlm@68246
  1028
  }
eberlm@68246
  1029
  with assms show ?thesis by (force simp: bigtheta_sym)
eberlm@68246
  1030
qed
eberlm@68246
  1031
eberlm@68246
  1032
eberlm@68246
  1033
subsection {* Landau symbols and limits *}
eberlm@68246
  1034
eberlm@68246
  1035
lemma bigoI_tendsto_norm:
eberlm@68246
  1036
  fixes f g
eberlm@68246
  1037
  assumes "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
eberlm@68246
  1038
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1039
  shows   "f \<in> O[F](g)"
eberlm@68246
  1040
proof (rule bigoI)
eberlm@68246
  1041
  from assms have "eventually (\<lambda>x. dist (norm (f x / g x)) c < 1) F" 
eberlm@68246
  1042
    using tendstoD by force
eberlm@68246
  1043
  thus "eventually (\<lambda>x. (norm (f x)) \<le> (norm c + 1) * (norm (g x))) F"
eberlm@68246
  1044
    unfolding dist_real_def using assms(2)
eberlm@68246
  1045
  proof eventually_elim
eberlm@68246
  1046
    case (elim x)
eberlm@68246
  1047
    have "(norm (f x)) - norm c * (norm (g x)) \<le> norm ((norm (f x)) - c * (norm (g x)))"
eberlm@68246
  1048
      unfolding norm_mult [symmetric] using norm_triangle_ineq2[of "norm (f x)" "c * norm (g x)"]
eberlm@68246
  1049
      by (simp add: norm_mult abs_mult)
eberlm@68246
  1050
    also from elim have "\<dots> = norm (norm (g x)) * norm (norm (f x / g x) - c)"
eberlm@68246
  1051
      unfolding norm_mult [symmetric] by (simp add: algebra_simps norm_divide)
eberlm@68246
  1052
    also from elim have "norm (norm (f x / g x) - c) \<le> 1" by simp
eberlm@68246
  1053
    hence "norm (norm (g x)) * norm (norm (f x / g x) - c) \<le> norm (norm (g x)) * 1" 
eberlm@68246
  1054
      by (rule mult_left_mono) simp_all
eberlm@68246
  1055
    finally show ?case by (simp add: algebra_simps)
eberlm@68246
  1056
  qed
eberlm@68246
  1057
qed
eberlm@68246
  1058
eberlm@68246
  1059
lemma bigoI_tendsto:
eberlm@68246
  1060
  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
eberlm@68246
  1061
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1062
  shows   "f \<in> O[F](g)"
eberlm@68246
  1063
  using assms by (rule bigoI_tendsto_norm[OF tendsto_norm])
eberlm@68246
  1064
eberlm@68246
  1065
lemma bigomegaI_tendsto_norm:
eberlm@68246
  1066
  assumes c_not_0:  "(c::real) \<noteq> 0"
eberlm@68246
  1067
  assumes lim:      "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
eberlm@68246
  1068
  shows   "f \<in> \<Omega>[F](g)"
eberlm@68246
  1069
proof (cases "F = bot")
eberlm@68246
  1070
  case False
eberlm@68246
  1071
  show ?thesis
eberlm@68246
  1072
  proof (rule landau_omega.bigI)
eberlm@68246
  1073
    from lim  have "c \<ge> 0" by (rule tendsto_lowerbound) (insert False, simp_all)
eberlm@68246
  1074
    with c_not_0 have "c > 0" by simp
eberlm@68246
  1075
    with c_not_0 show "c/2 > 0" by simp
eberlm@68246
  1076
    from lim have ev: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<epsilon>) F"
eberlm@68246
  1077
      by (subst (asm) tendsto_iff) (simp add: dist_real_def)
eberlm@68246
  1078
    from ev[OF `c/2 > 0`] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
eberlm@68246
  1079
    proof (eventually_elim)
eberlm@68246
  1080
      fix x assume B: "norm (norm (f x / g x) - c) < c / 2"
eberlm@68246
  1081
      from B have g: "g x \<noteq> 0" by auto
eberlm@68246
  1082
      from B have "-c/2 < -norm (norm (f x / g x) - c)" by simp
eberlm@68246
  1083
      also have "... \<le> norm (f x / g x) - c" by simp
eberlm@68246
  1084
      finally show "(norm (f x)) \<ge> c/2 * (norm (g x))" using g 
eberlm@68246
  1085
        by (simp add: field_simps norm_mult norm_divide)
eberlm@68246
  1086
    qed
eberlm@68246
  1087
  qed
eberlm@68246
  1088
qed simp
eberlm@68246
  1089
eberlm@68246
  1090
lemma bigomegaI_tendsto:
eberlm@68246
  1091
  assumes c_not_0:  "(c::real) \<noteq> 0"
eberlm@68246
  1092
  assumes lim:      "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
eberlm@68246
  1093
  shows   "f \<in> \<Omega>[F](g)"
eberlm@68246
  1094
  by (rule bigomegaI_tendsto_norm[OF _ tendsto_norm, of c]) (insert assms, simp_all)
eberlm@68246
  1095
eberlm@68246
  1096
lemma smallomegaI_filterlim_at_top_norm:
eberlm@68246
  1097
  assumes lim: "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
eberlm@68246
  1098
  shows   "f \<in> \<omega>[F](g)"
eberlm@68246
  1099
proof (rule landau_omega.smallI)
eberlm@68246
  1100
  fix c :: real assume c_pos: "c > 0"
eberlm@68246
  1101
  from lim have ev: "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F"
eberlm@68246
  1102
    by (subst (asm) filterlim_at_top) simp
eberlm@68246
  1103
  thus "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
eberlm@68246
  1104
  proof eventually_elim
eberlm@68246
  1105
    fix x assume A: "norm (f x / g x) \<ge> c"
eberlm@68246
  1106
    from A c_pos have "g x \<noteq> 0" by auto
eberlm@68246
  1107
    with A show "(norm (f x)) \<ge> c * (norm (g x))" by (simp add: field_simps norm_divide)
eberlm@68246
  1108
  qed
eberlm@68246
  1109
qed
eberlm@68246
  1110
eberlm@68246
  1111
lemma smallomegaI_filterlim_at_infinity:
eberlm@68246
  1112
  assumes lim: "filterlim (\<lambda>x. f x / g x) at_infinity F"
eberlm@68246
  1113
  shows   "f \<in> \<omega>[F](g)"
eberlm@68246
  1114
proof (rule smallomegaI_filterlim_at_top_norm)
eberlm@68246
  1115
  from lim show "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
eberlm@68246
  1116
    by (rule filterlim_at_infinity_imp_norm_at_top)
eberlm@68246
  1117
qed
eberlm@68246
  1118
  
eberlm@68246
  1119
lemma smallomegaD_filterlim_at_top_norm:
eberlm@68246
  1120
  assumes "f \<in> \<omega>[F](g)"
eberlm@68246
  1121
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1122
  shows   "LIM x F. norm (f x / g x) :> at_top"
eberlm@68246
  1123
proof (subst filterlim_at_top_gt, clarify)
eberlm@68246
  1124
  fix c :: real assume c: "c > 0"
eberlm@68246
  1125
  from landau_omega.smallD[OF assms(1) this] assms(2) 
eberlm@68246
  1126
    show "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F" 
eberlm@68246
  1127
    by eventually_elim (simp add: field_simps norm_divide)
eberlm@68246
  1128
qed
eberlm@68246
  1129
  
eberlm@68246
  1130
lemma smallomegaD_filterlim_at_infinity:
eberlm@68246
  1131
  assumes "f \<in> \<omega>[F](g)"
eberlm@68246
  1132
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1133
  shows   "LIM x F. f x / g x :> at_infinity"
eberlm@68246
  1134
  using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm)
eberlm@68246
  1135
eberlm@68246
  1136
lemma smallomega_1_conv_filterlim: "f \<in> \<omega>[F](\<lambda>_. 1) \<longleftrightarrow> filterlim f at_infinity F"
eberlm@68246
  1137
  by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)
eberlm@68246
  1138
eberlm@68246
  1139
lemma smalloI_tendsto:
eberlm@68246
  1140
  assumes lim: "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
eberlm@68246
  1141
  assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
eberlm@68246
  1142
  shows   "f \<in> o[F](g)"
eberlm@68246
  1143
proof (rule landau_o.smallI)
eberlm@68246
  1144
  fix c :: real assume c_pos: "c > 0"
eberlm@68246
  1145
  from c_pos and lim have ev: "eventually (\<lambda>x. norm (f x / g x) < c) F"
eberlm@68246
  1146
    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
eberlm@68246
  1147
  with assms(2) show "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
eberlm@68246
  1148
    by eventually_elim (simp add: field_simps norm_divide)
eberlm@68246
  1149
qed
eberlm@68246
  1150
eberlm@68246
  1151
lemma smalloD_tendsto:
eberlm@68246
  1152
  assumes "f \<in> o[F](g)"
eberlm@68246
  1153
  shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
eberlm@68246
  1154
unfolding tendsto_iff
eberlm@68246
  1155
proof clarify
eberlm@68246
  1156
  fix e :: real assume e: "e > 0"
eberlm@68246
  1157
  hence "e/2 > 0" by simp
eberlm@68246
  1158
  from landau_o.smallD[OF assms this] show "eventually (\<lambda>x. dist (f x / g x) 0 < e) F"
eberlm@68246
  1159
  proof eventually_elim
eberlm@68246
  1160
    fix x assume "(norm (f x)) \<le> e/2 * (norm (g x))"
eberlm@68246
  1161
    with e have "dist (f x / g x) 0 \<le> e/2"
eberlm@68246
  1162
      by (cases "g x = 0") (simp_all add: dist_real_def norm_divide field_simps)
eberlm@68246
  1163
    also from e have "... < e" by simp
eberlm@68246
  1164
    finally show "dist (f x / g x) 0 < e" by simp
eberlm@68246
  1165
  qed
eberlm@68246
  1166
qed
eberlm@68246
  1167
eberlm@68246
  1168
lemma bigthetaI_tendsto_norm:
eberlm@68246
  1169
  assumes c_not_0: "(c::real) \<noteq> 0"
eberlm@68246
  1170
  assumes lim:     "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
eberlm@68246
  1171
  shows   "f \<in> \<Theta>[F](g)"
eberlm@68246
  1172
proof (rule bigthetaI)
eberlm@68246
  1173
  from c_not_0 have "\<bar>c\<bar> > 0" by simp
eberlm@68246
  1174
  with lim have "eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<bar>c\<bar>) F"
eberlm@68246
  1175
    by (subst (asm) tendsto_iff) (simp add: dist_real_def)
eberlm@68246
  1176
  hence g: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim (auto simp add: field_simps)
eberlm@68246
  1177
eberlm@68246
  1178
  from lim g show "f \<in> O[F](g)" by (rule bigoI_tendsto_norm)
eberlm@68246
  1179
  from c_not_0 and lim show "f \<in> \<Omega>[F](g)" by (rule bigomegaI_tendsto_norm)
eberlm@68246
  1180
qed
eberlm@68246
  1181
eberlm@68246
  1182
lemma bigthetaI_tendsto:
eberlm@68246
  1183
  assumes c_not_0: "(c::real) \<noteq> 0"
eberlm@68246
  1184
  assumes lim:     "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
eberlm@68246
  1185
  shows   "f \<in> \<Theta>[F](g)"
eberlm@68246
  1186
  using assms by (intro bigthetaI_tendsto_norm[OF _ tendsto_norm, of "c"]) simp_all
eberlm@68246
  1187
eberlm@68246
  1188
lemma tendsto_add_smallo:
eberlm@68246
  1189
  assumes "(f1 \<longlongrightarrow> a) F"
eberlm@68246
  1190
  assumes "f2 \<in> o[F](f1)"
eberlm@68246
  1191
  shows   "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1192
proof (subst filterlim_cong[OF refl refl])
eberlm@68246
  1193
  from landau_o.smallD[OF assms(2) zero_less_one] 
eberlm@68246
  1194
    have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)) F" by simp
eberlm@68246
  1195
  thus "eventually (\<lambda>x. f1 x + f2 x = f1 x * (1 + f2 x / f1 x)) F"
eberlm@68246
  1196
    by eventually_elim (auto simp: field_simps)
eberlm@68246
  1197
next
eberlm@68246
  1198
  from assms(1) show "((\<lambda>x. f1 x * (1 + f2 x / f1 x)) \<longlongrightarrow> a) F"
eberlm@68246
  1199
    by (force intro: tendsto_eq_intros smalloD_tendsto[OF assms(2)])
eberlm@68246
  1200
qed
eberlm@68246
  1201
eberlm@68246
  1202
lemma tendsto_diff_smallo:
eberlm@68246
  1203
  shows "(f1 \<longlongrightarrow> a) F \<Longrightarrow> f2 \<in> o[F](f1) \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1204
  using tendsto_add_smallo[of f1 a F "\<lambda>x. -f2 x"] by simp
eberlm@68246
  1205
eberlm@68246
  1206
lemma tendsto_add_smallo_iff:
eberlm@68246
  1207
  assumes "f2 \<in> o[F](f1)"
eberlm@68246
  1208
  shows   "(f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1209
proof
eberlm@68246
  1210
  assume "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1211
  hence "((\<lambda>x. f1 x + f2 x - f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1212
    by (rule tendsto_diff_smallo) (simp add: landau_o.small.plus_absorb2 assms)
eberlm@68246
  1213
  thus "(f1 \<longlongrightarrow> a) F" by simp
eberlm@68246
  1214
qed (rule tendsto_add_smallo[OF _ assms])
eberlm@68246
  1215
eberlm@68246
  1216
lemma tendsto_diff_smallo_iff:
eberlm@68246
  1217
  shows "f2 \<in> o[F](f1) \<Longrightarrow> (f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
eberlm@68246
  1218
  using tendsto_add_smallo_iff[of "\<lambda>x. -f2 x" F f1 a] by simp
eberlm@68246
  1219
eberlm@68246
  1220
lemma tendsto_divide_smallo:
eberlm@68246
  1221
  assumes "((\<lambda>x. f1 x / g1 x) \<longlongrightarrow> a) F"
eberlm@68246
  1222
  assumes "f2 \<in> o[F](f1)" "g2 \<in> o[F](g1)"
eberlm@68246
  1223
  assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
eberlm@68246
  1224
  shows   "((\<lambda>x. (f1 x + f2 x) / (g1 x + g2 x)) \<longlongrightarrow> a) F" (is "(?f \<longlongrightarrow> _) _")
eberlm@68246
  1225
proof (subst tendsto_cong)
eberlm@68246
  1226
  let ?f' = "\<lambda>x. (f1 x / g1 x) * (1 + f2 x / f1 x) / (1 + g2 x / g1 x)"
eberlm@68246
  1227
eberlm@68246
  1228
  have "(?f' \<longlongrightarrow> a * (1 + 0) / (1 + 0)) F"
eberlm@68246
  1229
  by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const 
eberlm@68246
  1230
        smalloD_tendsto[OF assms(2)] smalloD_tendsto[OF assms(3)])+ simp_all
eberlm@68246
  1231
  thus "(?f' \<longlongrightarrow> a) F" by simp
eberlm@68246
  1232
eberlm@68246
  1233
  have "(1/2::real) > 0" by simp
eberlm@68246
  1234
  from landau_o.smallD[OF assms(2) this] landau_o.smallD[OF assms(3) this]
eberlm@68246
  1235
    have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)/2) F"
eberlm@68246
  1236
         "eventually (\<lambda>x. norm (g2 x) \<le> norm (g1 x)/2) F" by simp_all
eberlm@68246
  1237
  with assms(4) show "eventually (\<lambda>x. ?f x = ?f' x) F"
eberlm@68246
  1238
  proof eventually_elim
eberlm@68246
  1239
    fix x assume A: "norm (f2 x) \<le> norm (f1 x)/2" and 
eberlm@68246
  1240
                 B: "norm (g2 x) \<le> norm (g1 x)/2" and C: "g1 x \<noteq> 0"
eberlm@68246
  1241
    show "?f x = ?f' x"
eberlm@68246
  1242
    proof (cases "f1 x = 0")
eberlm@68246
  1243
      assume D: "f1 x \<noteq> 0"
eberlm@68246
  1244
      from D have "f1 x + f2 x = f1 x * (1 + f2 x/f1 x)" by (simp add: field_simps)
eberlm@68246
  1245
      moreover from C have "g1 x + g2 x = g1 x * (1 + g2 x/g1 x)" by (simp add: field_simps)
eberlm@68246
  1246
      ultimately have "?f x = (f1 x * (1 + f2 x/f1 x)) / (g1 x * (1 + g2 x/g1 x))" by (simp only:)
eberlm@68246
  1247
      also have "... = ?f' x" by simp
eberlm@68246
  1248
      finally show ?thesis .
eberlm@68246
  1249
    qed (insert A, simp)
eberlm@68246
  1250
  qed
eberlm@68246
  1251
qed
eberlm@68246
  1252
eberlm@68246
  1253
eberlm@68246
  1254
lemma bigo_powr:
eberlm@68246
  1255
  fixes f :: "'a \<Rightarrow> real"
eberlm@68246
  1256
  assumes "f \<in> O[F](g)" "p \<ge> 0"
eberlm@68246
  1257
  shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)"
eberlm@68246
  1258
proof-
eberlm@68246
  1259
  from assms(1) guess c by (elim landau_o.bigE landau_omega.bigE IntE)
eberlm@68246
  1260
  note c = this
eberlm@68246
  1261
  from c(2) assms(2) have "eventually (\<lambda>x. (norm (f x)) powr p \<le> (c * (norm (g x))) powr p) F"
eberlm@68246
  1262
    by (auto elim!: eventually_mono intro!: powr_mono2)
eberlm@68246
  1263
  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
  1264
    by (intro bigoI[of _ "c powr p"]) (simp_all add: powr_mult)
eberlm@68246
  1265
qed
eberlm@68246
  1266
eberlm@68246
  1267
lemma smallo_powr:
eberlm@68246
  1268
  fixes f :: "'a \<Rightarrow> real"
eberlm@68246
  1269
  assumes "f \<in> o[F](g)" "p > 0"
eberlm@68246
  1270
  shows   "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)"
eberlm@68246
  1271
proof (rule landau_o.smallI)
eberlm@68246
  1272
  fix c :: real assume c: "c > 0"
eberlm@68246
  1273
  hence "c powr (1/p) > 0" by simp
eberlm@68246
  1274
  from landau_o.smallD[OF assms(1) this] 
eberlm@68246
  1275
  show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F"
eberlm@68246
  1276
  proof eventually_elim
eberlm@68246
  1277
    fix x assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))"
eberlm@68246
  1278
    with assms(2) have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p"
eberlm@68246
  1279
      by (intro powr_mono2) simp_all
eberlm@68246
  1280
    also from assms(2) c have "... = c * (norm (g x)) powr p"
eberlm@68246
  1281
      by (simp add: field_simps powr_mult powr_powr)
eberlm@68246
  1282
    finally show "norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)" by simp
eberlm@68246
  1283
  qed
eberlm@68246
  1284
qed
eberlm@68246
  1285
eberlm@68246
  1286
lemma smallo_powr_nonneg:
eberlm@68246
  1287
  fixes f :: "'a \<Rightarrow> real"
eberlm@68246
  1288
  assumes "f \<in> o[F](g)" "p > 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
eberlm@68246
  1289
  shows   "(\<lambda>x. f x powr p) \<in> o[F](\<lambda>x. g x powr p)"
eberlm@68246
  1290
proof -
eberlm@68246
  1291
  from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
eberlm@68246
  1292
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1293
  also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro smallo_powr) fact+
eberlm@68246
  1294
  also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
eberlm@68246
  1295
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1296
  finally show ?thesis .
eberlm@68246
  1297
qed
eberlm@68246
  1298
eberlm@68246
  1299
lemma bigtheta_powr:
eberlm@68246
  1300
  fixes f :: "'a \<Rightarrow> real"
eberlm@68246
  1301
  shows "f \<in> \<Theta>[F](g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>g x\<bar> powr p)"
eberlm@68246
  1302
apply (cases "p < 0")
eberlm@68246
  1303
apply (subst bigtheta_inverse[symmetric], subst (1 2) powr_minus[symmetric])
eberlm@68246
  1304
unfolding bigtheta_def apply (auto simp: bigomega_iff_bigo intro!: bigo_powr)
eberlm@68246
  1305
done
eberlm@68246
  1306
eberlm@68246
  1307
lemma bigo_powr_nonneg:
eberlm@68246
  1308
  fixes f :: "'a \<Rightarrow> real"
eberlm@68246
  1309
  assumes "f \<in> O[F](g)" "p \<ge> 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
eberlm@68246
  1310
  shows   "(\<lambda>x. f x powr p) \<in> O[F](\<lambda>x. g x powr p)"
eberlm@68246
  1311
proof -
eberlm@68246
  1312
  from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)" 
eberlm@68246
  1313
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1314
  also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro bigo_powr) fact+
eberlm@68246
  1315
  also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
eberlm@68246
  1316
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1317
  finally show ?thesis .
eberlm@68246
  1318
qed
eberlm@68246
  1319
eberlm@68246
  1320
lemma zero_in_smallo [simp]: "(\<lambda>_. 0) \<in> o[F](f)"
eberlm@68246
  1321
  by (intro landau_o.smallI) simp_all
eberlm@68246
  1322
eberlm@68246
  1323
lemma zero_in_bigo [simp]: "(\<lambda>_. 0) \<in> O[F](f)"
eberlm@68246
  1324
  by (intro landau_o.bigI[of 1]) simp_all
eberlm@68246
  1325
eberlm@68246
  1326
lemma in_bigomega_zero [simp]: "f \<in> \<Omega>[F](\<lambda>x. 0)"
eberlm@68246
  1327
  by (rule landau_omega.bigI[of 1]) simp_all
eberlm@68246
  1328
eberlm@68246
  1329
lemma in_smallomega_zero [simp]: "f \<in> \<omega>[F](\<lambda>x. 0)"
eberlm@68246
  1330
  by (simp add: smallomega_iff_smallo)
eberlm@68246
  1331
eberlm@68246
  1332
eberlm@68246
  1333
lemma in_smallo_zero_iff [simp]: "f \<in> o[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1334
proof
eberlm@68246
  1335
  assume "f \<in> o[F](\<lambda>_. 0)"
eberlm@68246
  1336
  from landau_o.smallD[OF this, of 1] show "eventually (\<lambda>x. f x = 0) F" by simp
eberlm@68246
  1337
next
eberlm@68246
  1338
  assume "eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1339
  hence "\<forall>c>0. eventually (\<lambda>x. (norm (f x)) \<le> c * \<bar>0\<bar>) F" by simp
eberlm@68246
  1340
  thus "f \<in> o[F](\<lambda>_. 0)" unfolding smallo_def by simp
eberlm@68246
  1341
qed
eberlm@68246
  1342
eberlm@68246
  1343
lemma in_bigo_zero_iff [simp]: "f \<in> O[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1344
proof
eberlm@68246
  1345
  assume "f \<in> O[F](\<lambda>_. 0)"
eberlm@68246
  1346
  thus "eventually (\<lambda>x. f x = 0) F" by (elim landau_o.bigE) simp
eberlm@68246
  1347
next
eberlm@68246
  1348
  assume "eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1349
  hence "eventually (\<lambda>x. (norm (f x)) \<le> 1 * \<bar>0\<bar>) F" by simp
eberlm@68246
  1350
  thus "f \<in> O[F](\<lambda>_. 0)" by (intro landau_o.bigI[of 1]) simp_all
eberlm@68246
  1351
qed
eberlm@68246
  1352
eberlm@68246
  1353
lemma zero_in_smallomega_iff [simp]: "(\<lambda>_. 0) \<in> \<omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1354
  by (simp add: smallomega_iff_smallo)
eberlm@68246
  1355
eberlm@68246
  1356
lemma zero_in_bigomega_iff [simp]: "(\<lambda>_. 0) \<in> \<Omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1357
  by (simp add: bigomega_iff_bigo)
eberlm@68246
  1358
eberlm@68246
  1359
lemma zero_in_bigtheta_iff [simp]: "(\<lambda>_. 0) \<in> \<Theta>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1360
  unfolding bigtheta_def by simp
eberlm@68246
  1361
eberlm@68246
  1362
lemma in_bigtheta_zero_iff [simp]: "f \<in> \<Theta>[F](\<lambda>x. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  1363
  unfolding bigtheta_def by simp
eberlm@68246
  1364
eberlm@68246
  1365
eberlm@68246
  1366
lemma cmult_in_bigo_iff    [simp]:  "(\<lambda>x. c * f x) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
eberlm@68246
  1367
  and cmult_in_bigo_iff'   [simp]:  "(\<lambda>x. f x * c) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
eberlm@68246
  1368
  and cmult_in_smallo_iff  [simp]:  "(\<lambda>x. c * f x) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
eberlm@68246
  1369
  and cmult_in_smallo_iff' [simp]: "(\<lambda>x. f x * c) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
eberlm@68246
  1370
  by (cases "c = 0", simp, simp)+
eberlm@68246
  1371
eberlm@68246
  1372
lemma bigo_const [simp]: "(\<lambda>_. c) \<in> O[F](\<lambda>_. 1)" by (rule bigoI[of _ "norm c"]) simp
eberlm@68246
  1373
eberlm@68246
  1374
lemma bigo_const_iff [simp]: "(\<lambda>_. c1) \<in> O[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 = 0 \<or> c2 \<noteq> 0"
eberlm@68246
  1375
  by (cases "c1 = 0"; cases "c2 = 0")
eberlm@68246
  1376
     (auto simp: bigo_def eventually_False intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
eberlm@68246
  1377
eberlm@68246
  1378
lemma bigomega_const_iff [simp]: "(\<lambda>_. c1) \<in> \<Omega>[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 \<noteq> 0 \<or> c2 = 0"
eberlm@68246
  1379
  by (cases "c1 = 0"; cases "c2 = 0")
eberlm@68246
  1380
     (auto simp: bigomega_def eventually_False mult_le_0_iff 
eberlm@68246
  1381
           intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
eberlm@68246
  1382
eberlm@68246
  1383
lemma smallo_real_nat_transfer:
eberlm@68246
  1384
  "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))"
eberlm@68246
  1385
  by (rule landau_o.small.compose[OF _ filterlim_real_sequentially])
eberlm@68246
  1386
eberlm@68246
  1387
lemma bigo_real_nat_transfer:
eberlm@68246
  1388
  "(f :: real \<Rightarrow> real) \<in> O(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> O(\<lambda>x. g (real x))"
eberlm@68246
  1389
  by (rule landau_o.big.compose[OF _ filterlim_real_sequentially])
eberlm@68246
  1390
eberlm@68246
  1391
lemma smallomega_real_nat_transfer:
eberlm@68246
  1392
  "(f :: real \<Rightarrow> real) \<in> \<omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<omega>(\<lambda>x. g (real x))"
eberlm@68246
  1393
  by (rule landau_omega.small.compose[OF _ filterlim_real_sequentially])
eberlm@68246
  1394
eberlm@68246
  1395
lemma bigomega_real_nat_transfer:
eberlm@68246
  1396
  "(f :: real \<Rightarrow> real) \<in> \<Omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Omega>(\<lambda>x. g (real x))"
eberlm@68246
  1397
  by (rule landau_omega.big.compose[OF _ filterlim_real_sequentially])
eberlm@68246
  1398
eberlm@68246
  1399
lemma bigtheta_real_nat_transfer:
eberlm@68246
  1400
  "(f :: real \<Rightarrow> real) \<in> \<Theta>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Theta>(\<lambda>x. g (real x))"
eberlm@68246
  1401
  unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast
eberlm@68246
  1402
eberlm@68246
  1403
lemmas landau_real_nat_transfer [intro] = 
eberlm@68246
  1404
  bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer 
eberlm@68246
  1405
  smallomega_real_nat_transfer bigtheta_real_nat_transfer
eberlm@68246
  1406
eberlm@68246
  1407
eberlm@68246
  1408
lemma landau_symbol_if_at_top_eq [simp]:
eberlm@68246
  1409
  assumes "landau_symbol L L' Lr"
eberlm@68246
  1410
  shows   "L at_top (\<lambda>x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)"
eberlm@68246
  1411
apply (rule landau_symbol.cong[OF assms])
eberlm@68246
  1412
using less_add_one[of a] apply (auto intro: eventually_mono  eventually_ge_at_top[of "a + 1"])
eberlm@68246
  1413
done
eberlm@68246
  1414
eberlm@68246
  1415
lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq]
eberlm@68246
  1416
eberlm@68246
  1417
eberlm@68246
  1418
eberlm@68246
  1419
lemma sum_in_smallo:
eberlm@68246
  1420
  assumes "f \<in> o[F](h)" "g \<in> o[F](h)"
eberlm@68246
  1421
  shows   "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)"
eberlm@68246
  1422
proof-
eberlm@68246
  1423
  {
eberlm@68246
  1424
    fix f g assume fg: "f \<in> o[F](h)" "g \<in> o[F](h)"
eberlm@68246
  1425
    have "(\<lambda>x. f x + g x) \<in> o[F](h)"
eberlm@68246
  1426
    proof (rule landau_o.smallI)
eberlm@68246
  1427
      fix c :: real assume "c > 0"
eberlm@68246
  1428
      hence "c/2 > 0" by simp
eberlm@68246
  1429
      from fg[THEN landau_o.smallD[OF _ this]]
eberlm@68246
  1430
      show "eventually (\<lambda>x. norm (f x + g x) \<le> c * (norm (h x))) F"
eberlm@68246
  1431
        by eventually_elim (auto intro: order.trans[OF norm_triangle_ineq])
eberlm@68246
  1432
    qed
eberlm@68246
  1433
  }
eberlm@68246
  1434
  from this[of f g] this[of f "\<lambda>x. -g x"] assms
eberlm@68246
  1435
    show "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" by simp_all
eberlm@68246
  1436
qed
eberlm@68246
  1437
eberlm@68246
  1438
lemma big_sum_in_smallo:
eberlm@68246
  1439
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> o[F](g)"
eberlm@68246
  1440
  shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> o[F](g)"
eberlm@68246
  1441
  using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_smallo)
eberlm@68246
  1442
eberlm@68246
  1443
lemma sum_in_bigo:
eberlm@68246
  1444
  assumes "f \<in> O[F](h)" "g \<in> O[F](h)"
eberlm@68246
  1445
  shows   "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)"
eberlm@68246
  1446
proof-
eberlm@68246
  1447
  {
eberlm@68246
  1448
    fix f g assume fg: "f \<in> O[F](h)" "g \<in> O[F](h)"
eberlm@68246
  1449
    from fg(1) guess c1 by (elim landau_o.bigE) note c1 = this
eberlm@68246
  1450
    from fg(2) guess c2 by (elim landau_o.bigE) note c2 = this
eberlm@68246
  1451
    from c1(2) c2(2) have "eventually (\<lambda>x. norm (f x + g x) \<le> (c1 + c2) * (norm (h x))) F"
eberlm@68246
  1452
      by eventually_elim (auto simp: algebra_simps intro: order.trans[OF norm_triangle_ineq])
eberlm@68246
  1453
    hence "(\<lambda>x. f x + g x) \<in> O[F](h)" by (rule bigoI)
eberlm@68246
  1454
  }
eberlm@68246
  1455
  from this[of f g] this[of f "\<lambda>x. -g x"] assms
eberlm@68246
  1456
    show "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" by simp_all
eberlm@68246
  1457
qed
eberlm@68246
  1458
eberlm@68246
  1459
lemma big_sum_in_bigo:
eberlm@68246
  1460
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> O[F](g)"
eberlm@68246
  1461
  shows   "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"
eberlm@68246
  1462
  using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)
eberlm@68246
  1463
eberlm@68246
  1464
context landau_symbol
eberlm@68246
  1465
begin
eberlm@68246
  1466
eberlm@68246
  1467
lemma mult_cancel_left:
eberlm@68246
  1468
  assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
eberlm@68246
  1469
  notes   [trans] = bigtheta_trans1 bigtheta_trans2
eberlm@68246
  1470
  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f2 \<in> L F (g2)"
eberlm@68246
  1471
proof
eberlm@68246
  1472
  assume A: "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
eberlm@68246
  1473
  from assms have nz: "eventually (\<lambda>x. f1 x \<noteq> 0) F" by (simp add: eventually_nonzero_bigtheta)
eberlm@68246
  1474
  hence "f2 \<in> \<Theta>[F](\<lambda>x. f1 x * f2 x / f1 x)"
eberlm@68246
  1475
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1476
  also from A assms nz have "(\<lambda>x. f1 x * f2 x / f1 x) \<in> L F (\<lambda>x. g1 x * g2 x / f1 x)" 
eberlm@68246
  1477
    by (intro divide_right) simp_all
eberlm@68246
  1478
  also from assms nz have "(\<lambda>x. g1 x * g2 x / f1 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x / g1 x)"
eberlm@68246
  1479
    by (intro landau_theta.mult landau_theta.divide) (simp_all add: bigtheta_sym)
eberlm@68246
  1480
  also from assms have "(\<lambda>x. g1 x * g2 x / g1 x) \<in> \<Theta>[F](g2)"
eberlm@68246
  1481
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
eberlm@68246
  1482
  finally show "f2 \<in> L F (g2)" .
eberlm@68246
  1483
next
eberlm@68246
  1484
  assume "f2 \<in> L F (g2)"
eberlm@68246
  1485
  hence "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. f1 x * g2 x)" by (rule mult_left)
eberlm@68246
  1486
  also have "(\<lambda>x. f1 x * g2 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x)"
eberlm@68246
  1487
    by (intro landau_theta.mult_right assms)
eberlm@68246
  1488
  finally show "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" .
eberlm@68246
  1489
qed
eberlm@68246
  1490
eberlm@68246
  1491
lemma mult_cancel_right:
eberlm@68246
  1492
  assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
eberlm@68246
  1493
  shows   "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
eberlm@68246
  1494
  by (subst (1 2) mult.commute) (rule mult_cancel_left[OF assms])
eberlm@68246
  1495
eberlm@68246
  1496
lemma divide_cancel_right:
eberlm@68246
  1497
  assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
eberlm@68246
  1498
  shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
eberlm@68246
  1499
  by (subst (1 2) divide_inverse, intro mult_cancel_right bigtheta_inverse) (simp_all add: assms)
eberlm@68246
  1500
eberlm@68246
  1501
lemma divide_cancel_left:
eberlm@68246
  1502
  assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
eberlm@68246
  1503
  shows   "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> 
eberlm@68246
  1504
             (\<lambda>x. inverse (f2 x)) \<in> L F (\<lambda>x. inverse (g2 x))"
eberlm@68246
  1505
  by (simp only: divide_inverse mult_cancel_left[OF assms])
eberlm@68246
  1506
eberlm@68246
  1507
end
eberlm@68246
  1508
eberlm@68246
  1509
eberlm@68246
  1510
lemma powr_smallo_iff:
eberlm@68246
  1511
  assumes "filterlim g at_top F" "F \<noteq> bot"
eberlm@68246
  1512
  shows   "(\<lambda>x. g x powr p :: real) \<in> o[F](\<lambda>x. g x powr q) \<longleftrightarrow> p < q"
eberlm@68246
  1513
proof-
eberlm@68246
  1514
  from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
eberlm@68246
  1515
  hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
eberlm@68246
  1516
  have B: "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p) \<Longrightarrow> (\<lambda>x. g x powr p) \<notin> o[F](\<lambda>x. g x powr q)"
eberlm@68246
  1517
  proof
eberlm@68246
  1518
    assume "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)"
eberlm@68246
  1519
    from landau_o.big_small_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
eberlm@68246
  1520
    with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
eberlm@68246
  1521
    thus False by (simp add: eventually_False assms)
eberlm@68246
  1522
  qed
eberlm@68246
  1523
  show ?thesis
eberlm@68246
  1524
  proof (cases p q rule: linorder_cases)
eberlm@68246
  1525
    assume "p < q"
eberlm@68246
  1526
    hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
nipkow@68406
  1527
      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
eberlm@68246
  1528
    with `p < q` show ?thesis by auto
eberlm@68246
  1529
  next
eberlm@68246
  1530
    assume "p = q"
eberlm@68246
  1531
    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
eberlm@68246
  1532
    with B `p = q` show ?thesis by auto
eberlm@68246
  1533
  next
eberlm@68246
  1534
    assume "p > q"
eberlm@68246
  1535
    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
nipkow@68406
  1536
      by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)
eberlm@68246
  1537
    with B `p > q` show ?thesis by auto
eberlm@68246
  1538
  qed
eberlm@68246
  1539
qed
eberlm@68246
  1540
eberlm@68246
  1541
lemma powr_bigo_iff:
eberlm@68246
  1542
  assumes "filterlim g at_top F" "F \<noteq> bot"
eberlm@68246
  1543
  shows   "(\<lambda>x. g x powr p :: real) \<in> O[F](\<lambda>x. g x powr q) \<longleftrightarrow> p \<le> q"
eberlm@68246
  1544
proof-
eberlm@68246
  1545
  from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
eberlm@68246
  1546
  hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
eberlm@68246
  1547
  have B: "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p) \<Longrightarrow> (\<lambda>x. g x powr p) \<notin> O[F](\<lambda>x. g x powr q)"
eberlm@68246
  1548
  proof
eberlm@68246
  1549
    assume "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" "(\<lambda>x. g x powr p) \<in> O[F](\<lambda>x. g x powr q)"
eberlm@68246
  1550
    from landau_o.small_big_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
eberlm@68246
  1551
    with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
eberlm@68246
  1552
    thus False by (simp add: eventually_False assms)
eberlm@68246
  1553
  qed
eberlm@68246
  1554
  show ?thesis
eberlm@68246
  1555
  proof (cases p q rule: linorder_cases)
eberlm@68246
  1556
    assume "p < q"
eberlm@68246
  1557
    hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
nipkow@68406
  1558
      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
eberlm@68246
  1559
    with `p < q` show ?thesis by (auto intro: landau_o.small_imp_big)
eberlm@68246
  1560
  next
eberlm@68246
  1561
    assume "p = q"
eberlm@68246
  1562
    hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
eberlm@68246
  1563
    with B `p = q` show ?thesis by auto
eberlm@68246
  1564
  next
eberlm@68246
  1565
    assume "p > q"
eberlm@68246
  1566
    hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
nipkow@68406
  1567
      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
eberlm@68246
  1568
    with B `p > q` show ?thesis by (auto intro: landau_o.small_imp_big)
eberlm@68246
  1569
  qed
eberlm@68246
  1570
qed
eberlm@68246
  1571
eberlm@68246
  1572
lemma powr_bigtheta_iff: 
eberlm@68246
  1573
  assumes "filterlim g at_top F" "F \<noteq> bot"
eberlm@68246
  1574
  shows   "(\<lambda>x. g x powr p :: real) \<in> \<Theta>[F](\<lambda>x. g x powr q) \<longleftrightarrow> p = q"
eberlm@68246
  1575
  using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff)
eberlm@68246
  1576
eberlm@68246
  1577
eberlm@68246
  1578
subsection \<open>Flatness of real functions\<close>
eberlm@68246
  1579
eberlm@68246
  1580
text \<open>
eberlm@68246
  1581
  Given two real-valued functions $f$ and $g$, we say that $f$ is flatter than $g$ if
eberlm@68246
  1582
  any power of $f(x)$ is asymptotically dominated by any positive power of $g(x)$. This is
eberlm@68246
  1583
  a useful notion since, given two products of powers of functions sorted by flatness, we can
eberlm@68246
  1584
  compare them asymptotically by simply comparing the exponent lists lexicographically.
eberlm@68246
  1585
eberlm@68246
  1586
  A simple sufficient criterion for flatness it that $\ln f(x) \in o(\ln g(x))$, which we show
eberlm@68246
  1587
  now.
eberlm@68246
  1588
\<close>
eberlm@68246
  1589
lemma ln_smallo_imp_flat:
eberlm@68246
  1590
  fixes f g :: "real \<Rightarrow> real"
eberlm@68246
  1591
  assumes lim_f: "filterlim f at_top at_top"
eberlm@68246
  1592
  assumes lim_g: "filterlim g at_top at_top"
eberlm@68246
  1593
  assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
eberlm@68246
  1594
  assumes q: "q > 0"
eberlm@68246
  1595
  shows   "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)"
eberlm@68246
  1596
proof (rule smalloI_tendsto)
eberlm@68246
  1597
  from lim_f have "eventually (\<lambda>x. f x > 0) at_top" 
eberlm@68246
  1598
    by (simp add: filterlim_at_top_dense)
eberlm@68246
  1599
  hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp
eberlm@68246
  1600
  
eberlm@68246
  1601
  from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top"
eberlm@68246
  1602
    by (simp add: filterlim_at_top_dense)
eberlm@68246
  1603
  hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp
eberlm@68246
  1604
  thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top"
eberlm@68246
  1605
    by eventually_elim simp
eberlm@68246
  1606
  
eberlm@68246
  1607
  have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) = 
eberlm@68246
  1608
                          p * ln (f x) - q * ln (g x)) at_top"
eberlm@68246
  1609
    using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps)
eberlm@68246
  1610
  have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top"
eberlm@68246
  1611
    by (insert q)
eberlm@68246
  1612
       (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult
eberlm@68246
  1613
              tendsto_const tendsto_diff smalloD_tendsto[OF ln_o_ln] lim_g
eberlm@68246
  1614
              filterlim_compose[OF ln_at_top] | simp)+
eberlm@68246
  1615
  hence "filterlim (\<lambda>x. p * ln (f x) - q * ln (g x)) at_bot at_top"
eberlm@68246
  1616
    by (subst (asm) filterlim_cong[OF refl refl eq])
eberlm@68246
  1617
  hence *: "((\<lambda>x. exp (p * ln (f x) - q * ln (g x))) \<longlongrightarrow> 0) at_top"
eberlm@68246
  1618
    by (rule filterlim_compose[OF exp_at_bot])
eberlm@68246
  1619
  have eq: "eventually (\<lambda>x. exp (p * ln (f x) - q * ln (g x)) = f x powr p / g x powr q) at_top"
eberlm@68246
  1620
    using f_nz g_nz by eventually_elim (simp add: powr_def exp_diff)
eberlm@68246
  1621
  show "((\<lambda>x. f x powr p / g x powr q) \<longlongrightarrow> 0) at_top"
eberlm@68246
  1622
    using * by (subst (asm) filterlim_cong[OF refl refl eq])
eberlm@68246
  1623
qed
eberlm@68246
  1624
eberlm@68246
  1625
lemma ln_smallo_imp_flat':
eberlm@68246
  1626
  fixes f g :: "real \<Rightarrow> real"
eberlm@68246
  1627
  assumes lim_f: "filterlim f at_top at_top"
eberlm@68246
  1628
  assumes lim_g: "filterlim g at_top at_top"
eberlm@68246
  1629
  assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
eberlm@68246
  1630
  assumes q: "q < 0"
eberlm@68246
  1631
  shows   "(\<lambda>x. g x powr q) \<in> o(\<lambda>x. f x powr p)"
eberlm@68246
  1632
proof -
eberlm@68246
  1633
  from lim_f lim_g have "eventually (\<lambda>x. f x > 0) at_top" "eventually (\<lambda>x. g x > 0) at_top"
eberlm@68246
  1634
    by (simp_all add: filterlim_at_top_dense)
eberlm@68246
  1635
  hence "eventually (\<lambda>x. f x \<noteq> 0) at_top" "eventually (\<lambda>x. g x \<noteq> 0) at_top"
eberlm@68246
  1636
    by (auto elim: eventually_mono)
eberlm@68246
  1637
  moreover from assms have "(\<lambda>x. f x powr -p) \<in> o(\<lambda>x. g x powr -q)"
eberlm@68246
  1638
    by (intro ln_smallo_imp_flat assms) simp_all
eberlm@68246
  1639
  ultimately show ?thesis unfolding powr_minus
eberlm@68246
  1640
    by (simp add: landau_o.small.inverse_cancel)
eberlm@68246
  1641
qed
eberlm@68246
  1642
eberlm@68246
  1643
eberlm@68246
  1644
subsection \<open>Asymptotic Equivalence\<close>
eberlm@68246
  1645
eberlm@68246
  1646
(* TODO Move *)
eberlm@68246
  1647
lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
eberlm@68246
  1648
  by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
eberlm@68246
  1649
eberlm@68246
  1650
named_theorems asymp_equiv_intros
eberlm@68246
  1651
named_theorems asymp_equiv_simps
eberlm@68246
  1652
eberlm@68246
  1653
definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
eberlm@68246
  1654
  ("_ \<sim>[_] _" [51, 10, 51] 50)
eberlm@68246
  1655
  where "f \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
eberlm@68246
  1656
eberlm@68246
  1657
abbreviation (input) asymp_equiv_at_top where
eberlm@68246
  1658
  "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"
eberlm@68246
  1659
eberlm@68246
  1660
bundle asymp_equiv_notation
eberlm@68246
  1661
begin
eberlm@68246
  1662
notation asymp_equiv_at_top (infix "\<sim>" 50) 
eberlm@68246
  1663
end
eberlm@68246
  1664
eberlm@68246
  1665
lemma asymp_equivI: "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F \<Longrightarrow> f \<sim>[F] g"
eberlm@68246
  1666
  by (simp add: asymp_equiv_def)
eberlm@68246
  1667
eberlm@68246
  1668
lemma asymp_equivD: "f \<sim>[F] g \<Longrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
eberlm@68246
  1669
  by (simp add: asymp_equiv_def)
eberlm@68246
  1670
eberlm@68246
  1671
lemma asymp_equiv_filtermap_iff:
eberlm@68246
  1672
  "f \<sim>[filtermap h F] g \<longleftrightarrow> (\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
eberlm@68246
  1673
  by (simp add: asymp_equiv_def filterlim_filtermap)
eberlm@68246
  1674
eberlm@68246
  1675
lemma asymp_equiv_refl [simp, asymp_equiv_intros]: "f \<sim>[F] f"
eberlm@68246
  1676
proof (intro asymp_equivI)
eberlm@68246
  1677
  have "eventually (\<lambda>x. 1 = (if f x = 0 \<and> f x = 0 then 1 else f x / f x)) F"
eberlm@68246
  1678
    by (intro always_eventually) simp
eberlm@68246
  1679
  moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
eberlm@68246
  1680
  ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
eberlm@68246
  1681
    by (rule Lim_transform_eventually)
eberlm@68246
  1682
qed
eberlm@68246
  1683
eberlm@68246
  1684
lemma asymp_equiv_symI: 
eberlm@68246
  1685
  assumes "f \<sim>[F] g"
eberlm@68246
  1686
  shows   "g \<sim>[F] f"
eberlm@68246
  1687
  using tendsto_inverse[OF asymp_equivD[OF assms]]
eberlm@68246
  1688
  by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong)
eberlm@68246
  1689
eberlm@68246
  1690
lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f"
eberlm@68246
  1691
  by (blast intro: asymp_equiv_symI)
eberlm@68246
  1692
eberlm@68246
  1693
lemma asymp_equivI': 
eberlm@68246
  1694
  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
eberlm@68246
  1695
  shows   "f \<sim>[F] g"
eberlm@68246
  1696
proof (cases "F = bot")
eberlm@68246
  1697
  case False
eberlm@68246
  1698
  have "eventually (\<lambda>x. f x \<noteq> 0) F"
eberlm@68246
  1699
  proof (rule ccontr)
eberlm@68246
  1700
    assume "\<not>eventually (\<lambda>x. f x \<noteq> 0) F"
eberlm@68246
  1701
    hence "frequently (\<lambda>x. f x = 0) F" by (simp add: frequently_def)
eberlm@68246
  1702
    hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1)
eberlm@68246
  1703
    from limit_frequently_eq[OF False this assms] show False by simp_all
eberlm@68246
  1704
  qed
eberlm@68246
  1705
  hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"
eberlm@68246
  1706
    by eventually_elim simp
eberlm@68246
  1707
  from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def 
eberlm@68246
  1708
    by (rule Lim_transform_eventually)
eberlm@68246
  1709
qed (simp_all add: asymp_equiv_def)
eberlm@68246
  1710
eberlm@68246
  1711
eberlm@68246
  1712
lemma asymp_equiv_cong:
eberlm@68246
  1713
  assumes "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
eberlm@68246
  1714
  shows   "f1 \<sim>[F] g1 \<longleftrightarrow> f2 \<sim>[F] g2"
eberlm@68246
  1715
  unfolding asymp_equiv_def
eberlm@68246
  1716
proof (rule tendsto_cong, goal_cases)
eberlm@68246
  1717
  case 1
eberlm@68246
  1718
  from assms show ?case by eventually_elim simp
eberlm@68246
  1719
qed
eberlm@68246
  1720
eberlm@68246
  1721
lemma asymp_equiv_eventually_zeros:
eberlm@68246
  1722
  fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
eberlm@68246
  1723
  assumes "f \<sim>[F] g"
eberlm@68246
  1724
  shows   "eventually (\<lambda>x. f x = 0 \<longleftrightarrow> g x = 0) F"
eberlm@68246
  1725
proof -
eberlm@68246
  1726
  let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  1727
  have "eventually (\<lambda>x. x \<noteq> 0) (nhds (1::'b))"
eberlm@68246
  1728
    by (rule t1_space_nhds) auto
eberlm@68246
  1729
  hence "eventually (\<lambda>x. x \<noteq> 0) (filtermap ?h F)"
eberlm@68246
  1730
    using assms unfolding asymp_equiv_def filterlim_def
eberlm@68246
  1731
    by (rule filter_leD [rotated])
eberlm@68246
  1732
  hence "eventually (\<lambda>x. ?h x \<noteq> 0) F" by (simp add: eventually_filtermap)
eberlm@68246
  1733
  thus ?thesis by eventually_elim (auto split: if_splits)
eberlm@68246
  1734
qed
eberlm@68246
  1735
eberlm@68246
  1736
lemma asymp_equiv_transfer:
eberlm@68246
  1737
  assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
eberlm@68246
  1738
  shows   "f2 \<sim>[F] g2"
eberlm@68246
  1739
  using assms(1) asymp_equiv_cong[OF assms(2,3)] by simp
eberlm@68246
  1740
eberlm@68246
  1741
lemma asymp_equiv_transfer_trans [trans]:
eberlm@68246
  1742
  assumes "(\<lambda>x. f x (h1 x)) \<sim>[F] (\<lambda>x. g x (h1 x))"
eberlm@68246
  1743
  assumes "eventually (\<lambda>x. h1 x = h2 x) F"
eberlm@68246
  1744
  shows   "(\<lambda>x. f x (h2 x)) \<sim>[F] (\<lambda>x. g x (h2 x))"
eberlm@68246
  1745
  by (rule asymp_equiv_transfer[OF assms(1)]) (insert assms(2), auto elim!: eventually_mono)
eberlm@68246
  1746
eberlm@68246
  1747
lemma asymp_equiv_trans [trans]:
eberlm@68246
  1748
  fixes f g h
eberlm@68246
  1749
  assumes "f \<sim>[F] g" "g \<sim>[F] h"
eberlm@68246
  1750
  shows   "f \<sim>[F] h"
eberlm@68246
  1751
proof -
eberlm@68246
  1752
  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  1753
  from assms[THEN asymp_equiv_eventually_zeros]
eberlm@68246
  1754
    have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
eberlm@68246
  1755
  moreover from tendsto_mult[OF assms[THEN asymp_equivD]] 
eberlm@68246
  1756
    have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
eberlm@68246
  1757
  ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
eberlm@68246
  1758
qed
eberlm@68246
  1759
eberlm@68246
  1760
lemma asymp_equiv_trans_lift1 [trans]:
eberlm@68246
  1761
  assumes "a \<sim>[F] f b" "b \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
eberlm@68246
  1762
  shows   "a \<sim>[F] f c"
eberlm@68246
  1763
  using assms by (blast intro: asymp_equiv_trans)
eberlm@68246
  1764
eberlm@68246
  1765
lemma asymp_equiv_trans_lift2 [trans]:
eberlm@68246
  1766
  assumes "f a \<sim>[F] b" "a \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
eberlm@68246
  1767
  shows   "f c \<sim>[F] b"
eberlm@68246
  1768
  using asymp_equiv_symI[OF assms(3)[OF assms(2)]] assms(1)
eberlm@68246
  1769
  by (blast intro: asymp_equiv_trans)
eberlm@68246
  1770
eberlm@68246
  1771
lemma asymp_equivD_const:
eberlm@68246
  1772
  assumes "f \<sim>[F] (\<lambda>_. c)"
eberlm@68246
  1773
  shows   "(f \<longlongrightarrow> c) F"
eberlm@68246
  1774
proof (cases "c = 0")
eberlm@68246
  1775
  case False
eberlm@68246
  1776
  with tendsto_mult_right[OF asymp_equivD[OF assms], of c] show ?thesis by simp
eberlm@68246
  1777
next
eberlm@68246
  1778
  case True
eberlm@68246
  1779
  with asymp_equiv_eventually_zeros[OF assms] show ?thesis
eberlm@68246
  1780
    by (simp add: Lim_eventually)
eberlm@68246
  1781
qed
eberlm@68246
  1782
eberlm@68246
  1783
lemma asymp_equiv_refl_ev:
eberlm@68246
  1784
  assumes "eventually (\<lambda>x. f x = g x) F"
eberlm@68246
  1785
  shows   "f \<sim>[F] g"
eberlm@68246
  1786
  by (intro asymp_equivI Lim_eventually)
eberlm@68246
  1787
     (insert assms, auto elim!: eventually_mono)
eberlm@68246
  1788
eberlm@68246
  1789
lemma asymp_equiv_sandwich:
eberlm@68246
  1790
  fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"
eberlm@68246
  1791
  assumes "eventually (\<lambda>x. f x \<ge> 0) F"
eberlm@68246
  1792
  assumes "eventually (\<lambda>x. f x \<le> g x) F"
eberlm@68246
  1793
  assumes "eventually (\<lambda>x. g x \<le> h x) F"
eberlm@68246
  1794
  assumes "f \<sim>[F] h"
eberlm@68246
  1795
  shows   "g \<sim>[F] f" "g \<sim>[F] h"
eberlm@68246
  1796
proof -
eberlm@68246
  1797
  show "g \<sim>[F] f"
eberlm@68246
  1798
  proof (rule asymp_equivI, rule tendsto_sandwich)
eberlm@68246
  1799
    from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
eberlm@68246
  1800
      show "eventually (\<lambda>n. (if h n = 0 \<and> f n = 0 then 1 else h n / f n) \<ge>
eberlm@68246
  1801
                              (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
eberlm@68246
  1802
        by eventually_elim (auto intro!: divide_right_mono)
eberlm@68246
  1803
    from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
eberlm@68246
  1804
      show "eventually (\<lambda>n. 1 \<le>
eberlm@68246
  1805
                              (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
eberlm@68246
  1806
        by eventually_elim (auto intro!: divide_right_mono)
eberlm@68246
  1807
  qed (insert asymp_equiv_symI[OF assms(4)], simp_all add: asymp_equiv_def)
eberlm@68246
  1808
  also note \<open>f \<sim>[F] h\<close>
eberlm@68246
  1809
  finally show "g \<sim>[F] h" .
eberlm@68246
  1810
qed
eberlm@68246
  1811
eberlm@68246
  1812
lemma asymp_equiv_imp_eventually_same_sign:
eberlm@68246
  1813
  fixes f g :: "real \<Rightarrow> real"
eberlm@68246
  1814
  assumes "f \<sim>[F] g"
eberlm@68246
  1815
  shows   "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
eberlm@68246
  1816
proof -
eberlm@68246
  1817
  from assms have "((\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> sgn 1) F"
eberlm@68246
  1818
    unfolding asymp_equiv_def by (rule tendsto_sgn) simp_all
eberlm@68246
  1819
  from order_tendstoD(1)[OF this, of "1/2"]
eberlm@68246
  1820
    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
  1821
    by simp
eberlm@68246
  1822
  thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
eberlm@68246
  1823
  proof eventually_elim
eberlm@68246
  1824
    case (elim x)
eberlm@68246
  1825
    thus ?case
eberlm@68246
  1826
      by (cases "f x" "0 :: real" rule: linorder_cases; 
eberlm@68246
  1827
          cases "g x" "0 :: real" rule: linorder_cases) simp_all
eberlm@68246
  1828
  qed
eberlm@68246
  1829
qed
eberlm@68246
  1830
eberlm@68246
  1831
lemma
eberlm@68246
  1832
  fixes f g :: "_ \<Rightarrow> real"
eberlm@68246
  1833
  assumes "f \<sim>[F] g"
eberlm@68246
  1834
  shows   asymp_equiv_eventually_same_sign: "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" (is ?th1)
eberlm@68246
  1835
    and   asymp_equiv_eventually_neg_iff:   "eventually (\<lambda>x. f x < 0 \<longleftrightarrow> g x < 0) F" (is ?th2)
eberlm@68246
  1836
    and   asymp_equiv_eventually_pos_iff:   "eventually (\<lambda>x. f x > 0 \<longleftrightarrow> g x > 0) F" (is ?th3)
eberlm@68246
  1837
proof -
eberlm@68246
  1838
  from assms have "filterlim (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) (nhds 1) F"
eberlm@68246
  1839
    by (rule asymp_equivD)
eberlm@68246
  1840
  from order_tendstoD(1)[OF this zero_less_one]
eberlm@68246
  1841
    show ?th1 ?th2 ?th3
eberlm@68246
  1842
    by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+
eberlm@68246
  1843
qed
eberlm@68246
  1844
eberlm@68246
  1845
lemma asymp_equiv_tendsto_transfer:
eberlm@68246
  1846
  assumes "f \<sim>[F] g" and "(f \<longlongrightarrow> c) F"
eberlm@68246
  1847
  shows   "(g \<longlongrightarrow> c) F"
eberlm@68246
  1848
proof -
eberlm@68246
  1849
  let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"
eberlm@68246
  1850
  have "eventually (\<lambda>x. ?h x = g x) F"
eberlm@68246
  1851
    using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
eberlm@68246
  1852
  moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
eberlm@68246
  1853
  hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"
eberlm@68246
  1854
    by (rule asymp_equivD)
eberlm@68246
  1855
  from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp
eberlm@68246
  1856
  ultimately show ?thesis by (rule Lim_transform_eventually)
eberlm@68246
  1857
qed
eberlm@68246
  1858
eberlm@68246
  1859
lemma tendsto_asymp_equiv_cong:
eberlm@68246
  1860
  assumes "f \<sim>[F] g"
eberlm@68246
  1861
  shows   "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"
eberlm@68246
  1862
proof -
eberlm@68246
  1863
  {
eberlm@68246
  1864
    fix f g :: "'a \<Rightarrow> 'b"
eberlm@68246
  1865
    assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"
eberlm@68246
  1866
    have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"
eberlm@68246
  1867
      using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp
eberlm@68246
  1868
    moreover have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F"
eberlm@68246
  1869
      by (intro tendsto_intros asymp_equivD *)
eberlm@68246
  1870
    ultimately have "(f \<longlongrightarrow> c * 1) F"
eberlm@68246
  1871
      by (rule Lim_transform_eventually)
eberlm@68246
  1872
  }
eberlm@68246
  1873
  from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym)
eberlm@68246
  1874
qed
eberlm@68246
  1875
eberlm@68246
  1876
eberlm@68246
  1877
lemma smallo_imp_eventually_sgn:
eberlm@68246
  1878
  fixes f g :: "real \<Rightarrow> real"
eberlm@68246
  1879
  assumes "g \<in> o(f)"
eberlm@68246
  1880
  shows   "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top"
eberlm@68246
  1881
proof -
eberlm@68246
  1882
  have "0 < (1/2 :: real)" by simp
eberlm@68246
  1883
  from landau_o.smallD[OF assms, OF this] 
eberlm@68246
  1884
    have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp
eberlm@68246
  1885
  thus ?thesis
eberlm@68246
  1886
  proof eventually_elim
eberlm@68246
  1887
    case (elim x)
eberlm@68246
  1888
    thus ?case
eberlm@68246
  1889
      by (cases "f x" "0::real" rule: linorder_cases; 
eberlm@68246
  1890
          cases "f x + g x" "0::real" rule: linorder_cases) simp_all
eberlm@68246
  1891
  qed
eberlm@68246
  1892
qed
eberlm@68246
  1893
eberlm@68246
  1894
context
eberlm@68246
  1895
begin
eberlm@68246
  1896
eberlm@68246
  1897
private lemma asymp_equiv_add_rightI:
eberlm@68246
  1898
  assumes "f \<sim>[F] g" "h \<in> o[F](g)"
eberlm@68246
  1899
  shows   "(\<lambda>x. f x + h x) \<sim>[F] g"
eberlm@68246
  1900
proof -
eberlm@68246
  1901
  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  1902
  from landau_o.smallD[OF assms(2) zero_less_one]
eberlm@68246
  1903
    have ev: "eventually (\<lambda>x. g x = 0 \<longrightarrow> h x = 0) F" by eventually_elim auto
eberlm@68246
  1904
  have "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1) F"
eberlm@68246
  1905
    unfolding asymp_equiv_def using ev
eberlm@68246
  1906
    by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps)
eberlm@68246
  1907
  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1 + 0) F" by simp
eberlm@68246
  1908
  also have \<dots> by (intro tendsto_intros asymp_equivD assms smalloD_tendsto)
eberlm@68246
  1909
  finally show "(\<lambda>x. f x + h x) \<sim>[F] g" .
eberlm@68246
  1910
qed
eberlm@68246
  1911
eberlm@68246
  1912
lemma asymp_equiv_add_right [asymp_equiv_simps]:
eberlm@68246
  1913
  assumes "h \<in> o[F](g)"
eberlm@68246
  1914
  shows   "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
eberlm@68246
  1915
proof
eberlm@68246
  1916
  assume "(\<lambda>x. f x + h x) \<sim>[F] g"
eberlm@68246
  1917
  from asymp_equiv_add_rightI[OF this, of "\<lambda>x. -h x"] assms show "f \<sim>[F] g"
eberlm@68246
  1918
    by simp
eberlm@68246
  1919
qed (simp_all add: asymp_equiv_add_rightI assms)
eberlm@68246
  1920
eberlm@68246
  1921
end
eberlm@68246
  1922
eberlm@68246
  1923
lemma asymp_equiv_add_left [asymp_equiv_simps]: 
eberlm@68246
  1924
  assumes "h \<in> o[F](g)"
eberlm@68246
  1925
  shows   "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
eberlm@68246
  1926
  using asymp_equiv_add_right[OF assms] by (simp add: add.commute)
eberlm@68246
  1927
eberlm@68246
  1928
lemma asymp_equiv_add_right' [asymp_equiv_simps]:
eberlm@68246
  1929
  assumes "h \<in> o[F](g)"
eberlm@68246
  1930
  shows   "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f"
eberlm@68246
  1931
  using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym)
eberlm@68246
  1932
  
eberlm@68246
  1933
lemma asymp_equiv_add_left' [asymp_equiv_simps]:
eberlm@68246
  1934
  assumes "h \<in> o[F](g)"
eberlm@68246
  1935
  shows   "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f"
eberlm@68246
  1936
  using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym)
eberlm@68246
  1937
eberlm@68246
  1938
lemma smallo_imp_asymp_equiv:
eberlm@68246
  1939
  assumes "(\<lambda>x. f x - g x) \<in> o[F](g)"
eberlm@68246
  1940
  shows   "f \<sim>[F] g"
eberlm@68246
  1941
proof -
eberlm@68246
  1942
  from assms have "(\<lambda>x. f x - g x + g x) \<sim>[F] g"
eberlm@68246
  1943
    by (subst asymp_equiv_add_left) simp_all
eberlm@68246
  1944
  thus ?thesis by simp
eberlm@68246
  1945
qed
eberlm@68246
  1946
eberlm@68246
  1947
lemma asymp_equiv_uminus [asymp_equiv_intros]:
eberlm@68246
  1948
  "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. -f x) \<sim>[F] (\<lambda>x. -g x)"
eberlm@68246
  1949
  by (simp add: asymp_equiv_def cong: if_cong)
eberlm@68246
  1950
eberlm@68246
  1951
lemma asymp_equiv_uminus_iff [asymp_equiv_simps]:
eberlm@68246
  1952
  "(\<lambda>x. -f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] (\<lambda>x. -g x)"
eberlm@68246
  1953
  by (simp add: asymp_equiv_def cong: if_cong)
eberlm@68246
  1954
eberlm@68246
  1955
lemma asymp_equiv_mult [asymp_equiv_intros]:
eberlm@68246
  1956
  fixes f1 f2 g1 g2 :: "'a \<Rightarrow> 'b :: real_normed_field"
eberlm@68246
  1957
  assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
eberlm@68246
  1958
  shows   "(\<lambda>x. f1 x * f2 x) \<sim>[F] (\<lambda>x. g1 x * g2 x)"
eberlm@68246
  1959
proof -
eberlm@68246
  1960
  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  1961
  let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x
eberlm@68246
  1962
                   else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)"
eberlm@68246
  1963
  let ?S' = "\<lambda>x. ?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) x - ?T f1 g1 x * ?T f2 g2 x"
eberlm@68246
  1964
  {
eberlm@68246
  1965
    fix f g :: "'a \<Rightarrow> 'b" assume "f \<sim>[F] g"
eberlm@68246
  1966
    have "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F"
eberlm@68246
  1967
      by (rule tendsto_eq_intros refl asymp_equivD[OF \<open>f \<sim>[F] g\<close>])+ simp_all
eberlm@68246
  1968
  } note A = this    
eberlm@68246
  1969
eberlm@68246
  1970
  from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"
eberlm@68246
  1971
    by (intro tendsto_mult asymp_equivD)
eberlm@68246
  1972
  moreover {
eberlm@68246
  1973
    have "eventually (\<lambda>x. ?S x = ?S' x) F"
eberlm@68246
  1974
      using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
eberlm@68246
  1975
    moreover have "(?S \<longlongrightarrow> 0) F"
eberlm@68246
  1976
      by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])
eberlm@68246
  1977
         (auto intro: le_infI1 le_infI2)
eberlm@68246
  1978
    ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)
eberlm@68246
  1979
  }
eberlm@68246
  1980
  ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"
eberlm@68246
  1981
    by (rule Lim_transform)
eberlm@68246
  1982
  thus ?thesis by (simp add: asymp_equiv_def)
eberlm@68246
  1983
qed
eberlm@68246
  1984
eberlm@68246
  1985
lemma asymp_equiv_power [asymp_equiv_intros]:
eberlm@68246
  1986
  "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)"
eberlm@68246
  1987
  by (induction n) (simp_all add: asymp_equiv_mult)
eberlm@68246
  1988
eberlm@68246
  1989
lemma asymp_equiv_inverse [asymp_equiv_intros]:
eberlm@68246
  1990
  assumes "f \<sim>[F] g"
eberlm@68246
  1991
  shows   "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
eberlm@68246
  1992
proof -
eberlm@68246
  1993
  from tendsto_inverse[OF asymp_equivD[OF assms]]
eberlm@68246
  1994
    have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) \<longlongrightarrow> 1) F"
eberlm@68246
  1995
    by (simp add: if_distrib cong: if_cong)
eberlm@68246
  1996
  also have "(\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) =
eberlm@68246
  1997
               (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else inverse (f x) / inverse (g x))"
eberlm@68246
  1998
    by (intro ext) (simp add: field_simps)
eberlm@68246
  1999
  finally show ?thesis by (simp add: asymp_equiv_def)
eberlm@68246
  2000
qed
eberlm@68246
  2001
eberlm@68246
  2002
lemma asymp_equiv_inverse_iff [asymp_equiv_simps]:
eberlm@68246
  2003
  "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<sim>[F] g"
eberlm@68246
  2004
proof
eberlm@68246
  2005
  assume "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
eberlm@68246
  2006
  hence "(\<lambda>x. inverse (inverse (f x))) \<sim>[F] (\<lambda>x. inverse (inverse (g x)))" (is ?P)
eberlm@68246
  2007
    by (rule asymp_equiv_inverse)
eberlm@68246
  2008
  also have "?P \<longleftrightarrow> f \<sim>[F] g" by (intro asymp_equiv_cong) simp_all
eberlm@68246
  2009
  finally show "f \<sim>[F] g" .
eberlm@68246
  2010
qed (simp_all add: asymp_equiv_inverse)
eberlm@68246
  2011
eberlm@68246
  2012
lemma asymp_equiv_divide [asymp_equiv_intros]:
eberlm@68246
  2013
  assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
eberlm@68246
  2014
  shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
eberlm@68246
  2015
  using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
eberlm@68246
  2016
eberlm@68246
  2017
lemma asymp_equiv_compose [asymp_equiv_intros]:
eberlm@68246
  2018
  assumes "f \<sim>[G] g" "filterlim h G F"
eberlm@68246
  2019
  shows   "f \<circ> h \<sim>[F] g \<circ> h"
eberlm@68246
  2020
proof -
eberlm@68246
  2021
  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  2022
  have "f \<circ> h \<sim>[F] g \<circ> h \<longleftrightarrow> ((?T f g \<circ> h) \<longlongrightarrow> 1) F"
eberlm@68246
  2023
    by (simp add: asymp_equiv_def o_def)
eberlm@68246
  2024
  also have "\<dots> \<longleftrightarrow> (?T f g \<longlongrightarrow> 1) (filtermap h F)"
eberlm@68246
  2025
    by (rule tendsto_compose_filtermap)
eberlm@68246
  2026
  also have "\<dots>"
eberlm@68246
  2027
    by (rule tendsto_mono[of _ G]) (insert assms, simp_all add: asymp_equiv_def filterlim_def)
eberlm@68246
  2028
  finally show ?thesis .
eberlm@68246
  2029
qed
eberlm@68246
  2030
eberlm@68246
  2031
lemma asymp_equiv_compose':
eberlm@68246
  2032
  assumes "f \<sim>[G] g" "filterlim h G F"
eberlm@68246
  2033
  shows   "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
eberlm@68246
  2034
  using asymp_equiv_compose[OF assms] by (simp add: o_def)
eberlm@68246
  2035
  
eberlm@68246
  2036
lemma asymp_equiv_powr_real [asymp_equiv_intros]:
eberlm@68246
  2037
  fixes f g :: "'a \<Rightarrow> real"
eberlm@68246
  2038
  assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
eberlm@68246
  2039
  shows   "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"
eberlm@68246
  2040
proof -
eberlm@68246
  2041
  let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  2042
  have "eventually (\<lambda>x. ?T f g x powr y = ?T (\<lambda>x. f x powr y) (\<lambda>x. g x powr y) x) F"
eberlm@68246
  2043
    using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)
eberlm@68246
  2044
    by eventually_elim (auto simp: powr_divide)
eberlm@68246
  2045
  moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
eberlm@68246
  2046
    by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
eberlm@68246
  2047
  hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
eberlm@68246
  2048
  ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
eberlm@68246
  2049
qed
eberlm@68246
  2050
eberlm@68246
  2051
lemma asymp_equiv_norm [asymp_equiv_intros]:
eberlm@68246
  2052
  fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
eberlm@68246
  2053
  assumes "f \<sim>[F] g"
eberlm@68246
  2054
  shows   "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))"
eberlm@68246
  2055
  using tendsto_norm[OF asymp_equivD[OF assms]] 
eberlm@68246
  2056
  by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong)
eberlm@68246
  2057
eberlm@68246
  2058
lemma asymp_equiv_abs_real [asymp_equiv_intros]:
eberlm@68246
  2059
  fixes f g :: "'a \<Rightarrow> real"
eberlm@68246
  2060
  assumes "f \<sim>[F] g"
eberlm@68246
  2061
  shows   "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)"
eberlm@68246
  2062
  using tendsto_rabs[OF asymp_equivD[OF assms]] 
eberlm@68246
  2063
  by (simp add: if_distrib asymp_equiv_def cong: if_cong)
eberlm@68246
  2064
eberlm@68246
  2065
lemma asymp_equiv_imp_eventually_le:
eberlm@68246
  2066
  assumes "f \<sim>[F] g" "c > 1"
eberlm@68246
  2067
  shows   "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"
eberlm@68246
  2068
proof -
eberlm@68246
  2069
  from order_tendstoD(2)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
eberlm@68246
  2070
       asymp_equiv_eventually_zeros[OF assms(1)]
eberlm@68246
  2071
    show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
eberlm@68246
  2072
qed
eberlm@68246
  2073
eberlm@68246
  2074
lemma asymp_equiv_imp_eventually_ge:
eberlm@68246
  2075
  assumes "f \<sim>[F] g" "c < 1"
eberlm@68246
  2076
  shows   "eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F"
eberlm@68246
  2077
proof -
eberlm@68246
  2078
  from order_tendstoD(1)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
eberlm@68246
  2079
       asymp_equiv_eventually_zeros[OF assms(1)]
eberlm@68246
  2080
    show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
eberlm@68246
  2081
qed
eberlm@68246
  2082
eberlm@68246
  2083
lemma asymp_equiv_imp_bigo:
eberlm@68246
  2084
  assumes "f \<sim>[F] g"
eberlm@68246
  2085
  shows   "f \<in> O[F](g)"
eberlm@68246
  2086
proof (rule bigoI)
eberlm@68246
  2087
  have "(3/2::real) > 1" by simp
eberlm@68246
  2088
  from asymp_equiv_imp_eventually_le[OF assms this]
eberlm@68246
  2089
    show "eventually (\<lambda>x. norm (f x) \<le> 3/2 * norm (g x)) F"
eberlm@68246
  2090
    by eventually_elim simp
eberlm@68246
  2091
qed
eberlm@68246
  2092
eberlm@68246
  2093
lemma asymp_equiv_imp_bigomega:
eberlm@68246
  2094
  "f \<sim>[F] g \<Longrightarrow> f \<in> \<Omega>[F](g)"
eberlm@68246
  2095
  using asymp_equiv_imp_bigo[of g F f] by (simp add: asymp_equiv_sym bigomega_iff_bigo)
eberlm@68246
  2096
eberlm@68246
  2097
lemma asymp_equiv_imp_bigtheta:
eberlm@68246
  2098
  "f \<sim>[F] g \<Longrightarrow> f \<in> \<Theta>[F](g)"
eberlm@68246
  2099
  by (intro bigthetaI asymp_equiv_imp_bigo asymp_equiv_imp_bigomega)
eberlm@68246
  2100
eberlm@68246
  2101
lemma asymp_equiv_at_infinity_transfer:
eberlm@68246
  2102
  assumes "f \<sim>[F] g" "filterlim f at_infinity F"
eberlm@68246
  2103
  shows   "filterlim g at_infinity F"
eberlm@68246
  2104
proof -
eberlm@68246
  2105
  from assms(1) have "g \<in> \<Theta>[F](f)" by (rule asymp_equiv_imp_bigtheta[OF asymp_equiv_symI])
eberlm@68246
  2106
  also from assms have "f \<in> \<omega>[F](\<lambda>_. 1)" by (simp add: smallomega_1_conv_filterlim)
eberlm@68246
  2107
  finally show ?thesis by (simp add: smallomega_1_conv_filterlim)
eberlm@68246
  2108
qed
eberlm@68246
  2109
eberlm@68246
  2110
lemma asymp_equiv_at_top_transfer:
eberlm@68246
  2111
  fixes f g :: "_ \<Rightarrow> real"
eberlm@68246
  2112
  assumes "f \<sim>[F] g" "filterlim f at_top F"
eberlm@68246
  2113
  shows   "filterlim g at_top F"
eberlm@68246
  2114
proof (rule filterlim_at_infinity_imp_filterlim_at_top)
eberlm@68246
  2115
  show "filterlim g at_infinity F"
eberlm@68246
  2116
    by (rule asymp_equiv_at_infinity_transfer[OF assms(1) filterlim_mono[OF assms(2)]])
eberlm@68246
  2117
       (auto simp: at_top_le_at_infinity)
eberlm@68246
  2118
  from assms(2) have "eventually (\<lambda>x. f x > 0) F"
eberlm@68246
  2119
    using filterlim_at_top_dense by blast
eberlm@68246
  2120
  with asymp_equiv_eventually_pos_iff[OF assms(1)] show "eventually (\<lambda>x. g x > 0) F"
eberlm@68246
  2121
    by eventually_elim blast
eberlm@68246
  2122
qed
eberlm@68246
  2123
eberlm@68246
  2124
lemma asymp_equiv_at_bot_transfer:
eberlm@68246
  2125
  fixes f g :: "_ \<Rightarrow> real"
eberlm@68246
  2126
  assumes "f \<sim>[F] g" "filterlim f at_bot F"
eberlm@68246
  2127
  shows   "filterlim g at_bot F"
eberlm@68246
  2128
  unfolding filterlim_uminus_at_bot
eberlm@68246
  2129
  by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"])
eberlm@68246
  2130
     (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus)  
eberlm@68246
  2131
eberlm@68246
  2132
lemma asymp_equivI'_const:
eberlm@68246
  2133
  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0"
eberlm@68246
  2134
  shows   "f \<sim>[F] (\<lambda>x. c * g x)"
eberlm@68246
  2135
  using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2)
eberlm@68246
  2136
  by (intro asymp_equivI') (simp add: field_simps)
eberlm@68246
  2137
eberlm@68246
  2138
lemma asymp_equivI'_inverse_const:
eberlm@68246
  2139
  assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> inverse c) F" "c \<noteq> 0"
eberlm@68246
  2140
  shows   "(\<lambda>x. c * f x) \<sim>[F] g"
eberlm@68246
  2141
  using tendsto_mult[OF assms(1) tendsto_const[of "c"]] assms(2)
eberlm@68246
  2142
  by (intro asymp_equivI') (simp add: field_simps)
eberlm@68246
  2143
eberlm@68246
  2144
lemma filterlim_at_bot_imp_at_infinity: "filterlim f at_bot F \<Longrightarrow> filterlim f at_infinity F"
eberlm@68246
  2145
  for f :: "_ \<Rightarrow> real" using at_bot_le_at_infinity filterlim_mono by blast
eberlm@68246
  2146
eberlm@68246
  2147
lemma asymp_equiv_imp_diff_smallo:
eberlm@68246
  2148
  assumes "f \<sim>[F] g"
eberlm@68246
  2149
  shows   "(\<lambda>x. f x - g x) \<in> o[F](g)"
eberlm@68246
  2150
proof (rule landau_o.smallI)
eberlm@68246
  2151
  fix c :: real assume "c > 0"
eberlm@68246
  2152
  hence c: "min c 1 > 0" by simp
eberlm@68246
  2153
  let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
eberlm@68246
  2154
  from assms have "((\<lambda>x. ?h x - 1) \<longlongrightarrow> 1 - 1) F"
eberlm@68246
  2155
    by (intro tendsto_diff asymp_equivD tendsto_const)
eberlm@68246
  2156
  from tendstoD[OF this c] show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
eberlm@68246
  2157
  proof eventually_elim
eberlm@68246
  2158
    case (elim x)
eberlm@68246
  2159
    from elim have "norm (f x - g x) \<le> norm (f x / g x - 1) * norm (g x)"
eberlm@68246
  2160
      by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps)
eberlm@68246
  2161
    also have "norm (f x / g x - 1) * norm (g x) \<le> c * norm (g x)" using elim
eberlm@68246
  2162
      by (auto split: if_splits simp: mult_right_mono)
eberlm@68246
  2163
    finally show ?case .
eberlm@68246
  2164
  qed
eberlm@68246
  2165
qed
eberlm@68246
  2166
eberlm@68246
  2167
lemma asymp_equiv_altdef:
eberlm@68246
  2168
  "f \<sim>[F] g \<longleftrightarrow> (\<lambda>x. f x - g x) \<in> o[F](g)"
eberlm@68246
  2169
  by (rule iffI[OF asymp_equiv_imp_diff_smallo smallo_imp_asymp_equiv])
eberlm@68246
  2170
eberlm@68246
  2171
lemma asymp_equiv_0_left_iff [simp]: "(\<lambda>_. 0) \<sim>[F] f \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  2172
  and asymp_equiv_0_right_iff [simp]: "f \<sim>[F] (\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
eberlm@68246
  2173
  by (simp_all add: asymp_equiv_altdef landau_o.small_refl_iff)
eberlm@68246
  2174
eberlm@68246
  2175
lemma asymp_equiv_sandwich_real:
eberlm@68246
  2176
  fixes f g l u :: "'a \<Rightarrow> real"
eberlm@68246
  2177
  assumes "l \<sim>[F] g" "u \<sim>[F] g" "eventually (\<lambda>x. f x \<in> {l x..u x}) F"
eberlm@68246
  2178
  shows   "f \<sim>[F] g"
eberlm@68246
  2179
  unfolding asymp_equiv_altdef
eberlm@68246
  2180
proof (rule landau_o.smallI)
eberlm@68246
  2181
  fix c :: real assume c: "c > 0"
eberlm@68246
  2182
  have "eventually (\<lambda>x. norm (f x - g x) \<le> max (norm (l x - g x)) (norm (u x - g x))) F"
eberlm@68246
  2183
    using assms(3) by eventually_elim auto
eberlm@68246
  2184
  moreover have "eventually (\<lambda>x. norm (l x - g x) \<le> c * norm (g x)) F"
eberlm@68246
  2185
                "eventually (\<lambda>x. norm (u x - g x) \<le> c * norm (g x)) F"
eberlm@68246
  2186
    using assms(1,2) by (auto simp: asymp_equiv_altdef dest: landau_o.smallD[OF _ c])
eberlm@68246
  2187
  hence "eventually (\<lambda>x. max (norm (l x - g x)) (norm (u x - g x)) \<le> c * norm (g x)) F"
eberlm@68246
  2188
    by eventually_elim simp
eberlm@68246
  2189
  ultimately show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
eberlm@68246
  2190
    by eventually_elim (rule order.trans)
eberlm@68246
  2191
qed
eberlm@68246
  2192
eberlm@68246
  2193
lemma asymp_equiv_sandwich_real':
eberlm@68246
  2194
  fixes f g l u :: "'a \<Rightarrow> real"
eberlm@68246
  2195
  assumes "f \<sim>[F] l" "f \<sim>[F] u" "eventually (\<lambda>x. g x \<in> {l x..u x}) F"
eberlm@68246
  2196
  shows   "f \<sim>[F] g"
eberlm@68246
  2197
  using asymp_equiv_sandwich_real[of l F f u g] assms by (simp add: asymp_equiv_sym)
eberlm@68246
  2198
eberlm@68246
  2199
lemma asymp_equiv_sandwich_real'':
eberlm@68246
  2200
  fixes f g l u :: "'a \<Rightarrow> real"
eberlm@68246
  2201
  assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"
eberlm@68246
  2202
          "eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"
eberlm@68246
  2203
  shows   "f \<sim>[F] g"
eberlm@68246
  2204
  by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]
eberlm@68246
  2205
             asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];
eberlm@68246
  2206
      blast intro: asymp_equiv_trans assms(1,2,3))+
eberlm@68246
  2207
eberlm@68246
  2208
end