1section \<open>Asymptotic real interval arithmetic\<close> 2(* 3 File: Multiseries_Expansion_Bounds.thy 4 Author: Manuel Eberl, TU M��nchen 5 6 Automatic computation of upper and lower expansions for real-valued functions. 7 Allows limited handling of functions involving oscillating functions like sin, cos, floor, etc. 8*) 9theory Multiseries_Expansion_Bounds 10imports 11 Multiseries_Expansion 12begin 13 14lemma expands_to_cong_reverse: 15 "eventually (\<lambda>x. f x = g x) at_top \<Longrightarrow> (g expands_to F) bs \<Longrightarrow> (f expands_to F) bs" 16 using expands_to_cong[of g F bs f] by (simp add: eq_commute) 17 18lemma expands_to_trivial_bounds: "(f expands_to F) bs \<Longrightarrow> eventually (\<lambda>x. f x \<in> {f x..f x}) at_top" 19 by simp 20 21lemma eventually_in_atLeastAtMostI: 22 assumes "eventually (\<lambda>x. f x \<ge> l x) at_top" "eventually (\<lambda>x. f x \<le> u x) at_top" 23 shows "eventually (\<lambda>x. f x \<in> {l x..u x}) at_top" 24 using assms by eventually_elim simp_all 25 26lemma tendsto_sandwich': 27 fixes l f u :: "'a \<Rightarrow> 'b :: order_topology" 28 shows "eventually (\<lambda>x. l x \<le> f x) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> u x) F \<Longrightarrow> 29 (l \<longlongrightarrow> L1) F \<Longrightarrow> (u \<longlongrightarrow> L2) F \<Longrightarrow> L1 = L2 \<Longrightarrow> (f \<longlongrightarrow> L1) F" 30 using tendsto_sandwich[of l f F u L1] by simp 31 32(* TODO: Move? *) 33lemma filterlim_at_bot_mono: 34 fixes l f u :: "'a \<Rightarrow> 'b :: linorder_topology" 35 assumes "filterlim u at_bot F" and "eventually (\<lambda>x. f x \<le> u x) F" 36 shows "filterlim f at_bot F" 37 unfolding filterlim_at_bot 38proof 39 fix Z :: 'b 40 from assms(1) have "eventually (\<lambda>x. u x \<le> Z) F" by (auto simp: filterlim_at_bot) 41 with assms(2) show "eventually (\<lambda>x. f x \<le> Z) F" by eventually_elim simp 42qed 43 44context 45begin 46 47qualified lemma eq_zero_imp_nonneg: "x = (0::real) \<Longrightarrow> x \<ge> 0" 48 by simp 49 50qualified lemma exact_to_bound: "(f expands_to F) bs \<Longrightarrow> eventually (\<lambda>x. f x \<le> f x) at_top" 51 by simp 52 53qualified lemma expands_to_abs_nonneg: "(f expands_to F) bs \<Longrightarrow> eventually (\<lambda>x. abs (f x) \<ge> 0) at_top" 54 by simp 55 56qualified lemma eventually_nonpos_flip: "eventually (\<lambda>x. f x \<le> (0::real)) F \<Longrightarrow> eventually (\<lambda>x. -f x \<ge> 0) F" 57 by simp 58 59qualified lemma bounds_uminus: 60 fixes a b :: "real \<Rightarrow> real" 61 assumes "eventually (\<lambda>x. a x \<le> b x) at_top" 62 shows "eventually (\<lambda>x. -b x \<le> -a x) at_top" 63 using assms by eventually_elim simp 64 65qualified lemma 66 fixes a b c d :: "real \<Rightarrow> real" 67 assumes "eventually (\<lambda>x. a x \<le> b x) at_top" "eventually (\<lambda>x. c x \<le> d x) at_top" 68 shows combine_bounds_add: "eventually (\<lambda>x. a x + c x \<le> b x + d x) at_top" 69 and combine_bounds_diff: "eventually (\<lambda>x. a x - d x \<le> b x - c x) at_top" 70 by (use assms in eventually_elim; simp add: add_mono diff_mono)+ 71 72qualified lemma 73 fixes a b c d :: "real \<Rightarrow> real" 74 assumes "eventually (\<lambda>x. a x \<le> b x) at_top" "eventually (\<lambda>x. c x \<le> d x) at_top" 75 shows combine_bounds_min: "eventually (\<lambda>x. min (a x) (c x) \<le> min (b x) (d x)) at_top" 76 and combine_bounds_max: "eventually (\<lambda>x. max (a x) (c x) \<le> max (b x) (d x)) at_top" 77 by (blast intro: eventually_elim2[OF assms] min.mono max.mono)+ 78 79 80qualified lemma trivial_bounds_sin: "\<forall>x::real. sin x \<in> {-1..1}" 81 and trivial_bounds_cos: "\<forall>x::real. cos x \<in> {-1..1}" 82 and trivial_bounds_frac: "\<forall>x::real. frac x \<in> {0..1}" 83 by (auto simp: less_imp_le[OF frac_lt_1]) 84 85qualified lemma trivial_boundsI: 86 fixes f g:: "real \<Rightarrow> real" 87 assumes "\<forall>x. f x \<in> {l..u}" and "g \<equiv> g" 88 shows "eventually (\<lambda>x. f (g x) \<ge> l) at_top" "eventually (\<lambda>x. f (g x) \<le> u) at_top" 89 using assms by auto 90 91qualified lemma 92 fixes f f' :: "real \<Rightarrow> real" 93 shows transfer_lower_bound: 94 "eventually (\<lambda>x. g x \<ge> l x) at_top \<Longrightarrow> f \<equiv> g \<Longrightarrow> eventually (\<lambda>x. f x \<ge> l x) at_top" 95 and transfer_upper_bound: 96 "eventually (\<lambda>x. g x \<le> u x) at_top \<Longrightarrow> f \<equiv> g \<Longrightarrow> eventually (\<lambda>x. f x \<le> u x) at_top" 97 by simp_all 98 99qualified lemma mono_bound: 100 fixes f g h :: "real \<Rightarrow> real" 101 assumes "mono h" "eventually (\<lambda>x. f x \<le> g x) at_top" 102 shows "eventually (\<lambda>x. h (f x) \<le> h (g x)) at_top" 103 by (intro eventually_mono[OF assms(2)] monoD[OF assms(1)]) 104 105qualified lemma 106 fixes f l :: "real \<Rightarrow> real" 107 assumes "(l expands_to L) bs" "trimmed_pos L" "basis_wf bs" "eventually (\<lambda>x. l x \<le> f x) at_top" 108 shows expands_to_lb_ln: "eventually (\<lambda>x. ln (l x) \<le> ln (f x)) at_top" 109 and expands_to_ub_ln: 110 "eventually (\<lambda>x. f x \<le> u x) at_top \<Longrightarrow> eventually (\<lambda>x. ln (f x) \<le> ln (u x)) at_top" 111proof - 112 from assms(3,1,2) have pos: "eventually (\<lambda>x. l x > 0) at_top" 113 by (rule expands_to_imp_eventually_pos) 114 from pos and assms(4) 115 show "eventually (\<lambda>x. ln (l x) \<le> ln (f x)) at_top" by eventually_elim simp 116 assume "eventually (\<lambda>x. f x \<le> u x) at_top" 117 with pos and assms(4) show "eventually (\<lambda>x. ln (f x) \<le> ln (u x)) at_top" 118 by eventually_elim simp 119qed 120 121qualified lemma eventually_sgn_ge_1D: 122 assumes "eventually (\<lambda>x::real. sgn (f x) \<ge> l x) at_top" 123 "(l expands_to (const_expansion 1 :: 'a :: multiseries)) bs" 124 shows "((\<lambda>x. sgn (f x)) expands_to (const_expansion 1 :: 'a)) bs" 125proof (rule expands_to_cong) 126 from assms(2) have "eventually (\<lambda>x. l x = 1) at_top" 127 by (simp add: expands_to.simps) 128 with assms(1) show "eventually (\<lambda>x. 1 = sgn (f x)) at_top" 129 by eventually_elim (auto simp: sgn_if split: if_splits) 130qed (insert assms, auto simp: expands_to.simps) 131 132qualified lemma eventually_sgn_le_neg1D: 133 assumes "eventually (\<lambda>x::real. sgn (f x) \<le> u x) at_top" 134 "(u expands_to (const_expansion (-1) :: 'a :: multiseries)) bs" 135 shows "((\<lambda>x. sgn (f x)) expands_to (const_expansion (-1) :: 'a)) bs" 136proof (rule expands_to_cong) 137 from assms(2) have "eventually (\<lambda>x. u x = -1) at_top" 138 by (simp add: expands_to.simps eq_commute) 139 with assms(1) show "eventually (\<lambda>x. -1 = sgn (f x)) at_top" 140 by eventually_elim (auto simp: sgn_if split: if_splits) 141qed (insert assms, auto simp: expands_to.simps) 142 143 144qualified lemma expands_to_squeeze: 145 assumes "eventually (\<lambda>x. l x \<le> f x) at_top" "eventually (\<lambda>x. f x \<le> g x) at_top" 146 "(l expands_to L) bs" "(g expands_to L) bs" 147 shows "(f expands_to L) bs" 148proof (rule expands_to_cong[OF assms(3)]) 149 from assms have "eventually (\<lambda>x. eval L x = l x) at_top" "eventually (\<lambda>x. eval L x = g x) at_top" 150 by (simp_all add: expands_to.simps) 151 with assms(1,2) show "eventually (\<lambda>x. l x = f x) at_top" 152 by eventually_elim simp 153qed 154 155 156qualified lemma mono_exp_real: "mono (exp :: real \<Rightarrow> real)" 157 by (auto intro!: monoI) 158 159qualified lemma mono_sgn_real: "mono (sgn :: real \<Rightarrow> real)" 160 by (auto intro!: monoI simp: sgn_if) 161 162qualified lemma mono_arctan_real: "mono (arctan :: real \<Rightarrow> real)" 163 by (auto intro!: monoI arctan_monotone') 164 165qualified lemma mono_root_real: "n \<equiv> n \<Longrightarrow> mono (root n :: real \<Rightarrow> real)" 166 by (cases n) (auto simp: mono_def) 167 168qualified lemma mono_rfloor: "mono rfloor" and mono_rceil: "mono rceil" 169 by (auto intro!: monoI simp: rfloor_def floor_mono rceil_def ceiling_mono) 170 171qualified lemma lower_bound_cong: 172 "eventually (\<lambda>x. f x = g x) at_top \<Longrightarrow> eventually (\<lambda>x. l x \<le> g x) at_top \<Longrightarrow> 173 eventually (\<lambda>x. l x \<le> f x) at_top" 174 by (erule (1) eventually_elim2) simp 175 176qualified lemma upper_bound_cong: 177 "eventually (\<lambda>x. f x = g x) at_top \<Longrightarrow> eventually (\<lambda>x. g x \<le> u x) at_top \<Longrightarrow> 178 eventually (\<lambda>x. f x \<le> u x) at_top" 179 by (erule (1) eventually_elim2) simp 180 181qualified lemma 182 assumes "eventually (\<lambda>x. f x = (g x :: real)) at_top" 183 shows eventually_eq_min: "eventually (\<lambda>x. min (f x) (g x) = f x) at_top" 184 and eventually_eq_max: "eventually (\<lambda>x. max (f x) (g x) = f x) at_top" 185 by (rule eventually_mono[OF assms]; simp)+ 186 187qualified lemma rfloor_bound: 188 "eventually (\<lambda>x. l x \<le> f x) at_top \<Longrightarrow> eventually (\<lambda>x. l x - 1 \<le> rfloor (f x)) at_top" 189 "eventually (\<lambda>x. f x \<le> u x) at_top \<Longrightarrow> eventually (\<lambda>x. rfloor (f x) \<le> u x) at_top" 190 and rceil_bound: 191 "eventually (\<lambda>x. l x \<le> f x) at_top \<Longrightarrow> eventually (\<lambda>x. l x \<le> rceil (f x)) at_top" 192 "eventually (\<lambda>x. f x \<le> u x) at_top \<Longrightarrow> eventually (\<lambda>x. rceil (f x) \<le> u x + 1) at_top" 193 unfolding rfloor_def rceil_def by (erule eventually_mono, linarith)+ 194 195qualified lemma natmod_trivial_lower_bound: 196 fixes f g :: "real \<Rightarrow> real" 197 assumes "f \<equiv> f" "g \<equiv> g" 198 shows "eventually (\<lambda>x. rnatmod (f x) (g x) \<ge> 0) at_top" 199 by (simp add: rnatmod_def) 200 201qualified lemma natmod_upper_bound: 202 fixes f g :: "real \<Rightarrow> real" 203 assumes "f \<equiv> f" and "eventually (\<lambda>x. l2 x \<le> g x) at_top" and "eventually (\<lambda>x. g x \<le> u2 x) at_top" 204 assumes "eventually (\<lambda>x. l2 x - 1 \<ge> 0) at_top" 205 shows "eventually (\<lambda>x. rnatmod (f x) (g x) \<le> u2 x - 1) at_top" 206 using assms(2-) 207proof eventually_elim 208 case (elim x) 209 have "rnatmod (f x) (g x) = real (nat \<lfloor>f x\<rfloor> mod nat \<lfloor>g x\<rfloor>)" 210 by (simp add: rnatmod_def) 211 also have "nat \<lfloor>f x\<rfloor> mod nat \<lfloor>g x\<rfloor> < nat \<lfloor>g x\<rfloor>" 212 using elim by (intro mod_less_divisor) auto 213 hence "real (nat \<lfloor>f x\<rfloor> mod nat \<lfloor>g x\<rfloor>) \<le> u2 x - 1" 214 using elim by linarith 215 finally show ?case . 216qed 217 218qualified lemma natmod_upper_bound': 219 fixes f g :: "real \<Rightarrow> real" 220 assumes "g \<equiv> g" "eventually (\<lambda>x. u1 x \<ge> 0) at_top" and "eventually (\<lambda>x. f x \<le> u1 x) at_top" 221 shows "eventually (\<lambda>x. rnatmod (f x) (g x) \<le> u1 x) at_top" 222 using assms(2-) 223proof eventually_elim 224 case (elim x) 225 have "rnatmod (f x) (g x) = real (nat \<lfloor>f x\<rfloor> mod nat \<lfloor>g x\<rfloor>)" 226 by (simp add: rnatmod_def) 227 also have "nat \<lfloor>f x\<rfloor> mod nat \<lfloor>g x\<rfloor> \<le> nat \<lfloor>f x\<rfloor>" 228 by auto 229 hence "real (nat \<lfloor>f x\<rfloor> mod nat \<lfloor>g x\<rfloor>) \<le> real (nat \<lfloor>f x\<rfloor>)" 230 by simp 231 also have "\<dots> \<le> u1 x" using elim by linarith 232 finally show "rnatmod (f x) (g x) \<le> \<dots>" . 233qed 234 235qualified lemma expands_to_natmod_nonpos: 236 fixes f g :: "real \<Rightarrow> real" 237 assumes "g \<equiv> g" "eventually (\<lambda>x. u1 x \<le> 0) at_top" "eventually (\<lambda>x. f x \<le> u1 x) at_top" 238 "((\<lambda>_. 0) expands_to C) bs" 239 shows "((\<lambda>x. rnatmod (f x) (g x)) expands_to C) bs" 240 by (rule expands_to_cong[OF assms(4)]) 241 (insert assms, auto elim: eventually_elim2 simp: rnatmod_def) 242 243 244qualified lemma eventually_atLeastAtMostI: 245 fixes f l r :: "real \<Rightarrow> real" 246 assumes "eventually (\<lambda>x. l x \<le> f x) at_top" "eventually (\<lambda>x. f x \<le> u x) at_top" 247 shows "eventually (\<lambda>x. f x \<in> {l x..u x}) at_top" 248 using assms by eventually_elim simp 249 250qualified lemma eventually_atLeastAtMostD: 251 fixes f l r :: "real \<Rightarrow> real" 252 assumes "eventually (\<lambda>x. f x \<in> {l x..u x}) at_top" 253 shows "eventually (\<lambda>x. l x \<le> f x) at_top" "eventually (\<lambda>x. f x \<le> u x) at_top" 254 using assms by (simp_all add: eventually_conj_iff) 255 256qualified lemma eventually_0_imp_prod_zero: 257 fixes f g :: "real \<Rightarrow> real" 258 assumes "eventually (\<lambda>x. f x = 0) at_top" 259 shows "eventually (\<lambda>x. f x * g x = 0) at_top" "eventually (\<lambda>x. g x * f x = 0) at_top" 260 by (use assms in eventually_elim; simp)+ 261 262qualified lemma mult_right_bounds: 263 fixes f g :: "real \<Rightarrow> real" 264 shows "\<forall>x. f x \<in> {l x..u x} \<longrightarrow> g x \<ge> 0 \<longrightarrow> f x * g x \<in> {l x * g x..u x * g x}" 265 and "\<forall>x. f x \<in> {l x..u x} \<longrightarrow> g x \<le> 0 \<longrightarrow> f x * g x \<in> {u x * g x..l x * g x}" 266 by (auto intro: mult_right_mono mult_right_mono_neg) 267 268qualified lemma mult_left_bounds: 269 fixes f g :: "real \<Rightarrow> real" 270 shows "\<forall>x. g x \<in> {l x..u x} \<longrightarrow> f x \<ge> 0 \<longrightarrow> f x * g x \<in> {f x * l x..f x * u x}" 271 and "\<forall>x. g x \<in> {l x..u x} \<longrightarrow> f x \<le> 0 \<longrightarrow> f x * g x \<in> {f x * u x..f x * l x}" 272 by (auto intro: mult_left_mono mult_left_mono_neg) 273 274qualified lemma mult_mono_nonpos_nonneg: 275 "a \<le> c \<Longrightarrow> d \<le> b \<Longrightarrow> a \<le> 0 \<Longrightarrow> d \<ge> 0 \<Longrightarrow> a * b \<le> c * (d :: 'a :: linordered_ring)" 276 using mult_mono[of "-c" "-a" d b] by simp 277 278qualified lemma mult_mono_nonneg_nonpos: 279 "c \<le> a \<Longrightarrow> b \<le> d \<Longrightarrow> a \<ge> 0 \<Longrightarrow> d \<le> 0 \<Longrightarrow> a * b \<le> c * (d :: 'a :: {comm_ring, linordered_ring})" 280 using mult_mono[of c a "-d" "-b"] by (simp add: mult.commute) 281 282qualified lemma mult_mono_nonpos_nonpos: 283 "c \<le> a \<Longrightarrow> d \<le> b \<Longrightarrow> c \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> c * (d :: 'a :: linordered_ring)" 284 using mult_mono[of "-a" "-c" "-b" "-d"] by simp 285 286qualified lemmas mult_monos = 287 mult_mono mult_mono_nonpos_nonneg mult_mono_nonneg_nonpos mult_mono_nonpos_nonpos 288 289 290qualified lemma mult_bounds_real: 291 fixes f g l1 u1 l2 u2 l u :: "real \<Rightarrow> real" 292 defines "P \<equiv> \<lambda>l u x. f x \<in> {l1 x..u1 x} \<longrightarrow> g x \<in> {l2 x..u2 x} \<longrightarrow> f x * g x \<in> {l..u}" 293 shows "\<forall>x. l1 x \<ge> 0 \<longrightarrow> l2 x \<ge> 0 \<longrightarrow> P (l1 x * l2 x) (u1 x * u2 x) x" 294 and "\<forall>x. u1 x \<le> 0 \<longrightarrow> l2 x \<ge> 0 \<longrightarrow> P (l1 x * u2 x) (u1 x * l2 x) x" 295 and "\<forall>x. l1 x \<ge> 0 \<longrightarrow> u2 x \<le> 0 \<longrightarrow> P (u1 x * l2 x) (l1 x * u2 x) x" 296 and "\<forall>x. u1 x \<le> 0 \<longrightarrow> u2 x \<le> 0 \<longrightarrow> P (u1 x * u2 x) (l1 x * l2 x) x" 297 298 and "\<forall>x. l1 x \<le> 0 \<longrightarrow> u1 x \<ge> 0 \<longrightarrow> l2 x \<ge> 0 \<longrightarrow> P (l1 x * u2 x) (u1 x * u2 x) x" 299 and "\<forall>x. l1 x \<le> 0 \<longrightarrow> u1 x \<ge> 0 \<longrightarrow> u2 x \<le> 0 \<longrightarrow> P (u1 x * l2 x) (l1 x * l2 x) x" 300 and "\<forall>x. l1 x \<ge> 0 \<longrightarrow> l2 x \<le> 0 \<longrightarrow> u2 x \<ge> 0 \<longrightarrow> P (u1 x * l2 x) (u1 x * u2 x) x" 301 and "\<forall>x. u1 x \<le> 0 \<longrightarrow> l2 x \<le> 0 \<longrightarrow> u2 x \<ge> 0 \<longrightarrow> P (l1 x * u2 x) (l1 x * l2 x) x" 302 303 and "\<forall>x. l1 x \<le> 0 \<longrightarrow> u1 x \<ge> 0 \<longrightarrow> l2 x \<le> 0 \<longrightarrow> u2 x \<ge> 0 \<longrightarrow> l x \<le> l1 x * u2 x \<longrightarrow> 304 l x \<le> u1 x * l2 x \<longrightarrow> u x \<ge> l1 x* l2 x \<longrightarrow> u x \<ge> u1 x * u2 x \<longrightarrow> P (l x) (u x) x" 305proof goal_cases 306 case 1 307 show ?case by (auto intro: mult_mono simp: P_def) 308next 309 case 2 310 show ?case by (auto intro: mult_monos(2) simp: P_def) 311next 312 case 3 313 show ?case unfolding P_def 314 by (subst (1 2 3) mult.commute) (auto intro: mult_monos(2) simp: P_def) 315next 316 case 4 317 show ?case by (auto intro: mult_monos(4) simp: P_def) 318next 319 case 5 320 show ?case by (auto intro: mult_monos(1,2) simp: P_def) 321next 322 case 6 323 show ?case by (auto intro: mult_monos(3,4) simp: P_def) 324next 325 case 7 326 show ?case unfolding P_def 327 by (subst (1 2 3) mult.commute) (auto intro: mult_monos(1,2)) 328next 329 case 8 330 show ?case unfolding P_def 331 by (subst (1 2 3) mult.commute) (auto intro: mult_monos(3,4)) 332next 333 case 9 334 show ?case 335 proof (safe, goal_cases) 336 case (1 x) 337 from 1(1-4) show ?case unfolding P_def 338 by (cases "f x \<ge> 0"; cases "g x \<ge> 0"; 339 fastforce intro: mult_monos 1(5,6)[THEN order.trans] 1(7,8)[THEN order.trans[rotated]]) 340 qed 341qed 342 343 344qualified lemma powr_bounds_real: 345 fixes f g l1 u1 l2 u2 l u :: "real \<Rightarrow> real" 346 defines "P \<equiv> \<lambda>l u x. f x \<in> {l1 x..u1 x} \<longrightarrow> g x \<in> {l2 x..u2 x} \<longrightarrow> f x powr g x \<in> {l..u}" 347 shows "\<forall>x. l1 x \<ge> 0 \<longrightarrow> l1 x \<ge> 1 \<longrightarrow> l2 x \<ge> 0 \<longrightarrow> P (l1 x powr l2 x) (u1 x powr u2 x) x" 348 and "\<forall>x. l1 x \<ge> 0 \<longrightarrow> u1 x \<le> 1 \<longrightarrow> l2 x \<ge> 0 \<longrightarrow> P (l1 x powr u2 x) (u1 x powr l2 x) x" 349 and "\<forall>x. l1 x \<ge> 0 \<longrightarrow> l1 x \<ge> 1 \<longrightarrow> u2 x \<le> 0 \<longrightarrow> P (u1 x powr l2 x) (l1 x powr u2 x) x" 350 and "\<forall>x. l1 x > 0 \<longrightarrow> u1 x \<le> 1 \<longrightarrow> u2 x \<le> 0 \<longrightarrow> P (u1 x powr u2 x) (l1 x powr l2 x) x" 351 352 and "\<forall>x. l1 x \<ge> 0 \<longrightarrow> l1 x \<le> 1 \<longrightarrow> u1 x \<ge> 1 \<longrightarrow> l2 x \<ge> 0 \<longrightarrow> P (l1 x powr u2 x) (u1 x powr u2 x) x" 353 and "\<forall>x. l1 x > 0 \<longrightarrow> l1 x \<le> 1 \<longrightarrow> u1 x \<ge> 1 \<longrightarrow> u2 x \<le> 0 \<longrightarrow> P (u1 x powr l2 x) (l1 x powr l2 x) x" 354 and "\<forall>x. l1 x \<ge> 0 \<longrightarrow> l1 x \<ge> 1 \<longrightarrow> l2 x \<le> 0 \<longrightarrow> u2 x \<ge> 0 \<longrightarrow> P (u1 x powr l2 x) (u1 x powr u2 x) x" 355 and "\<forall>x. l1 x > 0 \<longrightarrow> u1 x \<le> 1 \<longrightarrow> l2 x \<le> 0 \<longrightarrow> u2 x \<ge> 0 \<longrightarrow> P (l1 x powr u2 x) (l1 x powr l2 x) x" 356 357 and "\<forall>x. l1 x > 0 \<longrightarrow> l1 x \<le> 1 \<longrightarrow> u1 x \<ge> 1 \<longrightarrow> l2 x \<le> 0 \<longrightarrow> u2 x \<ge> 0 \<longrightarrow> l x \<le> l1 x powr u2 x \<longrightarrow> 358 l x \<le> u1 x powr l2 x \<longrightarrow> u x \<ge> l1 x powr l2 x \<longrightarrow> u x \<ge> u1 x powr u2 x \<longrightarrow> P (l x) (u x) x" 359proof goal_cases 360 case 1 361 show ?case by (auto simp: P_def powr_def intro: mult_monos) 362next 363 case 2 364 show ?case by (auto simp: P_def powr_def intro: mult_monos) 365next 366 case 3 367 show ?case by (auto simp: P_def powr_def intro: mult_monos) 368next 369 case 4 370 show ?case by (auto simp: P_def powr_def intro: mult_monos) 371next 372 case 5 373 note comm = mult.commute[of _ "ln x" for x :: real] 374 show ?case by (auto simp: P_def powr_def comm intro: mult_monos) 375next 376 case 6 377 note comm = mult.commute[of _ "ln x" for x :: real] 378 show ?case by (auto simp: P_def powr_def comm intro: mult_monos) 379next 380 case 7 381 show ?case by (auto simp: P_def powr_def intro: mult_monos) 382next 383 case 8 384 show ?case 385 by (auto simp: P_def powr_def intro: mult_monos) 386next 387 case 9 388 show ?case unfolding P_def 389 proof (safe, goal_cases) 390 case (1 x) 391 define l' where "l' = (\<lambda>x. min (ln (l1 x) * u2 x) (ln (u1 x) * l2 x))" 392 define u' where "u' = (\<lambda>x. max (ln (l1 x) * l2 x) (ln (u1 x) * u2 x))" 393 from 1 spec[OF mult_bounds_real(9)[of "\<lambda>x. ln (l1 x)" "\<lambda>x. ln (u1 x)" l2 u2 l' u' 394 "\<lambda>x. ln (f x)" g], of x] 395 have "ln (f x) * g x \<in> {l' x..u' x}" by (auto simp: powr_def mult.commute l'_def u'_def) 396 with 1 have "f x powr g x \<in> {exp (l' x)..exp (u' x)}" 397 by (auto simp: powr_def mult.commute) 398 also from 1 have "exp (l' x) = min (l1 x powr u2 x) (u1 x powr l2 x)" 399 by (auto simp add: l'_def powr_def min_def mult.commute) 400 also from 1 have "exp (u' x) = max (l1 x powr l2 x) (u1 x powr u2 x)" 401 by (auto simp add: u'_def powr_def max_def mult.commute) 402 finally show ?case using 1(5-9) by auto 403 qed 404qed 405 406qualified lemma powr_right_bounds: 407 fixes f g :: "real \<Rightarrow> real" 408 shows "\<forall>x. l x \<ge> 0 \<longrightarrow> f x \<in> {l x..u x} \<longrightarrow> g x \<ge> 0 \<longrightarrow> f x powr g x \<in> {l x powr g x..u x powr g x}" 409 and "\<forall>x. l x > 0 \<longrightarrow> f x \<in> {l x..u x} \<longrightarrow> g x \<le> 0 \<longrightarrow> f x powr g x \<in> {u x powr g x..l x powr g x}" 410 by (auto intro: powr_mono2 powr_mono2') 411 412(* TODO Move *) 413lemma powr_mono': "a \<le> (b::real) \<Longrightarrow> x \<ge> 0 \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr b \<le> x powr a" 414 using powr_mono[of "-b" "-a" "inverse x"] by (auto simp: powr_def ln_inverse ln_div field_split_simps) 415 416qualified lemma powr_left_bounds: 417 fixes f g :: "real \<Rightarrow> real" 418 shows "\<forall>x. f x > 0 \<longrightarrow> g x \<in> {l x..u x} \<longrightarrow> f x \<ge> 1 \<longrightarrow> f x powr g x \<in> {f x powr l x..f x powr u x}" 419 and "\<forall>x. f x > 0 \<longrightarrow> g x \<in> {l x..u x} \<longrightarrow> f x \<le> 1 \<longrightarrow> f x powr g x \<in> {f x powr u x..f x powr l x}" 420 by (auto intro: powr_mono powr_mono') 421 422qualified lemma powr_nat_bounds_transfer_ge: 423 "\<forall>x. l1 x \<ge> 0 \<longrightarrow> f x \<ge> l1 x \<longrightarrow> f x powr g x \<ge> l x \<longrightarrow> powr_nat (f x) (g x) \<ge> l x" 424 by (auto simp: powr_nat_def) 425 426qualified lemma powr_nat_bounds_transfer_le: 427 "\<forall>x. l1 x > 0 \<longrightarrow> f x \<ge> l1 x \<longrightarrow> f x powr g x \<le> u x \<longrightarrow> powr_nat (f x) (g x) \<le> u x" 428 "\<forall>x. l1 x \<ge> 0 \<longrightarrow> l2 x > 0 \<longrightarrow> f x \<ge> l1 x \<longrightarrow> g x \<ge> l2 x \<longrightarrow> 429 f x powr g x \<le> u x \<longrightarrow> powr_nat (f x) (g x) \<le> u x" 430 "\<forall>x. l1 x \<ge> 0 \<longrightarrow> u2 x < 0 \<longrightarrow> f x \<ge> l1 x \<longrightarrow> g x \<le> u2 x \<longrightarrow> 431 f x powr g x \<le> u x \<longrightarrow> powr_nat (f x) (g x) \<le> u x" 432 "\<forall>x. l1 x \<ge> 0 \<longrightarrow> f x \<ge> l1 x \<longrightarrow> f x powr g x \<le> u x \<longrightarrow> u x \<le> u' x \<longrightarrow> 1 \<le> u' x \<longrightarrow> 433 powr_nat (f x) (g x) \<le> u' x" 434 by (auto simp: powr_nat_def) 435 436lemma abs_powr_nat_le: "abs (powr_nat x y) \<le> powr_nat (abs x) y" 437 by (simp add: powr_nat_def abs_mult) 438 439qualified lemma powr_nat_bounds_ge_neg: 440 assumes "powr_nat (abs x) y \<le> u" 441 shows "powr_nat x y \<ge> -u" "powr_nat x y \<le> u" 442proof - 443 have "abs (powr_nat x y) \<le> powr_nat (abs x) y" 444 by (rule abs_powr_nat_le) 445 also have "\<dots> \<le> u" using assms by auto 446 finally show "powr_nat x y \<ge> -u" "powr_nat x y \<le> u" by auto 447qed 448 449qualified lemma powr_nat_bounds_transfer_abs [eventuallized]: 450 "\<forall>x. powr_nat (abs (f x)) (g x) \<le> u x \<longrightarrow> powr_nat (f x) (g x) \<ge> -u x" 451 "\<forall>x. powr_nat (abs (f x)) (g x) \<le> u x \<longrightarrow> powr_nat (f x) (g x) \<le> u x" 452 using powr_nat_bounds_ge_neg by blast+ 453 454qualified lemma eventually_powr_const_nonneg: 455 "f \<equiv> f \<Longrightarrow> p \<equiv> p \<Longrightarrow> eventually (\<lambda>x. f x powr p \<ge> (0::real)) at_top" 456 by simp 457 458qualified lemma eventually_powr_const_mono_nonneg: 459 assumes "p \<ge> (0 :: real)" "eventually (\<lambda>x. l x \<ge> 0) at_top" "eventually (\<lambda>x. l x \<le> f x) at_top" 460 "eventually (\<lambda>x. f x \<le> g x) at_top" 461 shows "eventually (\<lambda>x. f x powr p \<le> g x powr p) at_top" 462 using assms(2-4) by eventually_elim (auto simp: assms(1) intro!: powr_mono2) 463 464qualified lemma eventually_powr_const_mono_nonpos: 465 assumes "p \<le> (0 :: real)" "eventually (\<lambda>x. l x > 0) at_top" "eventually (\<lambda>x. l x \<le> f x) at_top" 466 "eventually (\<lambda>x. f x \<le> g x) at_top" 467 shows "eventually (\<lambda>x. f x powr p \<ge> g x powr p) at_top" 468 using assms(2-4) by eventually_elim (auto simp: assms(1) intro!: powr_mono2') 469 470 471qualified lemma eventually_power_mono: 472 assumes "eventually (\<lambda>x. 0 \<le> l x) at_top" "eventually (\<lambda>x. l x \<le> f x) at_top" 473 "eventually (\<lambda>x. f x \<le> g x) at_top" "n \<equiv> n" 474 shows "eventually (\<lambda>x. f x ^ n \<le> (g x :: real) ^ n) at_top" 475 using assms(1-3) by eventually_elim (auto intro: power_mono) 476 477qualified lemma eventually_mono_power_odd: 478 assumes "odd n" "eventually (\<lambda>x. f x \<le> (g x :: real)) at_top" 479 shows "eventually (\<lambda>x. f x ^ n \<le> g x ^ n) at_top" 480 using assms(2) by eventually_elim (insert assms(1), auto intro: power_mono_odd) 481 482 483qualified lemma eventually_lower_bound_power_even_nonpos: 484 assumes "even n" "eventually (\<lambda>x. u x \<le> (0::real)) at_top" 485 "eventually (\<lambda>x. f x \<le> u x) at_top" 486 shows "eventually (\<lambda>x. u x ^ n \<le> f x ^ n) at_top" 487 using assms(2-) by eventually_elim (rule power_mono_even, auto simp: assms(1)) 488 489qualified lemma eventually_upper_bound_power_even_nonpos: 490 assumes "even n" "eventually (\<lambda>x. u x \<le> (0::real)) at_top" 491 "eventually (\<lambda>x. l x \<le> f x) at_top" "eventually (\<lambda>x. f x \<le> u x) at_top" 492 shows "eventually (\<lambda>x. f x ^ n \<le> l x ^ n) at_top" 493 using assms(2-) by eventually_elim (rule power_mono_even, auto simp: assms(1)) 494 495qualified lemma eventually_lower_bound_power_even_indet: 496 assumes "even n" "f \<equiv> f" 497 shows "eventually (\<lambda>x. (0::real) \<le> f x ^ n) at_top" 498 using assms by (simp add: zero_le_even_power) 499 500 501qualified lemma eventually_lower_bound_power_indet: 502 assumes "eventually (\<lambda>x. l x \<le> f x) at_top" 503 assumes "eventually (\<lambda>x. l' x \<le> l x ^ n) at_top" "eventually (\<lambda>x. l' x \<le> 0) at_top" 504 shows "eventually (\<lambda>x. l' x \<le> (f x ^ n :: real)) at_top" 505 using assms 506proof eventually_elim 507 case (elim x) 508 thus ?case 509 using power_mono_odd[of n "l x" "f x"] zero_le_even_power[of n "f x"] 510 by (cases "even n") auto 511qed 512 513qualified lemma eventually_upper_bound_power_indet: 514 assumes "eventually (\<lambda>x. l x \<le> f x) at_top" "eventually (\<lambda>x. f x \<le> u x) at_top" 515 "eventually (\<lambda>x. u' x \<ge> -l x) at_top" "eventually (\<lambda>x. u' x \<ge> u x) at_top" "n \<equiv> n" 516 shows "eventually (\<lambda>x. f x ^ n \<le> (u' x ^ n :: real)) at_top" 517 using assms(1-4) 518proof eventually_elim 519 case (elim x) 520 have "f x ^ n \<le> \<bar>f x ^ n\<bar>" by simp 521 also have "\<dots> = \<bar>f x\<bar> ^ n" by (simp add: power_abs) 522 also from elim have "\<dots> \<le> u' x ^ n" by (intro power_mono) auto 523 finally show ?case . 524qed 525 526qualified lemma expands_to_imp_exp_ln_eq: 527 assumes "(l expands_to L) bs" "eventually (\<lambda>x. l x \<le> f x) at_top" 528 "trimmed_pos L" "basis_wf bs" 529 shows "eventually (\<lambda>x. exp (ln (f x)) = f x) at_top" 530proof - 531 from expands_to_imp_eventually_pos[of bs l L] assms 532 have "eventually (\<lambda>x. l x > 0) at_top" by simp 533 with assms(2) show ?thesis by eventually_elim simp 534qed 535 536qualified lemma expands_to_imp_ln_powr_eq: 537 assumes "(l expands_to L) bs" "eventually (\<lambda>x. l x \<le> f x) at_top" 538 "trimmed_pos L" "basis_wf bs" 539 shows "eventually (\<lambda>x. ln (f x powr g x) = ln (f x) * g x) at_top" 540proof - 541 from expands_to_imp_eventually_pos[of bs l L] assms 542 have "eventually (\<lambda>x. l x > 0) at_top" by simp 543 with assms(2) show ?thesis by eventually_elim (simp add: powr_def) 544qed 545 546qualified lemma inverse_bounds_real: 547 fixes f l u :: "real \<Rightarrow> real" 548 shows "\<forall>x. l x > 0 \<longrightarrow> l x \<le> f x \<longrightarrow> f x \<le> u x \<longrightarrow> inverse (f x) \<in> {inverse (u x)..inverse (l x)}" 549 and "\<forall>x. u x < 0 \<longrightarrow> l x \<le> f x \<longrightarrow> f x \<le> u x \<longrightarrow> inverse (f x) \<in> {inverse (u x)..inverse (l x)}" 550 by (auto simp: field_simps) 551 552qualified lemma pos_imp_inverse_pos: "\<forall>x::real. f x > 0 \<longrightarrow> inverse (f x) > (0::real)" 553 and neg_imp_inverse_neg: "\<forall>x::real. f x < 0 \<longrightarrow> inverse (f x) < (0::real)" 554 by auto 555 556qualified lemma transfer_divide_bounds: 557 fixes f g :: "real \<Rightarrow> real" 558 shows "Trueprop (eventually (\<lambda>x. f x \<in> {h x * inverse (i x)..j x}) at_top) \<equiv> 559 Trueprop (eventually (\<lambda>x. f x \<in> {h x / i x..j x}) at_top)" 560 and "Trueprop (eventually (\<lambda>x. f x \<in> {j x..h x * inverse (i x)}) at_top) \<equiv> 561 Trueprop (eventually (\<lambda>x. f x \<in> {j x..h x / i x}) at_top)" 562 and "Trueprop (eventually (\<lambda>x. f x * inverse (g x) \<in> A x) at_top) \<equiv> 563 Trueprop (eventually (\<lambda>x. f x / g x \<in> A x) at_top)" 564 and "Trueprop (((\<lambda>x. f x * inverse (g x)) expands_to F) bs) \<equiv> 565 Trueprop (((\<lambda>x. f x / g x) expands_to F) bs)" 566 by (simp_all add: field_simps) 567 568qualified lemma eventually_le_self: "eventually (\<lambda>x::real. f x \<le> (f x :: real)) at_top" 569 by simp 570 571qualified lemma max_eventually_eq: 572 "eventually (\<lambda>x. f x = (g x :: real)) at_top \<Longrightarrow> eventually (\<lambda>x. max (f x) (g x) = f x) at_top" 573 by (erule eventually_mono) simp 574 575qualified lemma min_eventually_eq: 576 "eventually (\<lambda>x. f x = (g x :: real)) at_top \<Longrightarrow> eventually (\<lambda>x. min (f x) (g x) = f x) at_top" 577 by (erule eventually_mono) simp 578 579qualified lemma 580 assumes "eventually (\<lambda>x. f x = (g x :: 'a :: preorder)) F" 581 shows eventually_eq_imp_ge: "eventually (\<lambda>x. f x \<ge> g x) F" 582 and eventually_eq_imp_le: "eventually (\<lambda>x. f x \<le> g x) F" 583 by (use assms in eventually_elim; simp)+ 584 585qualified lemma eventually_less_imp_le: 586 assumes "eventually (\<lambda>x. f x < (g x :: 'a :: order)) F" 587 shows "eventually (\<lambda>x. f x \<le> g x) F" 588 using assms by eventually_elim auto 589 590qualified lemma 591 fixes f :: "real \<Rightarrow> real" 592 shows eventually_abs_ge_0: "eventually (\<lambda>x. abs (f x) \<ge> 0) at_top" 593 and nonneg_abs_bounds: "\<forall>x. l x \<ge> 0 \<longrightarrow> f x \<in> {l x..u x} \<longrightarrow> abs (f x) \<in> {l x..u x}" 594 and nonpos_abs_bounds: "\<forall>x. u x \<le> 0 \<longrightarrow> f x \<in> {l x..u x} \<longrightarrow> abs (f x) \<in> {-u x..-l x}" 595 and indet_abs_bounds: 596 "\<forall>x. l x \<le> 0 \<longrightarrow> u x \<ge> 0 \<longrightarrow> f x \<in> {l x..u x} \<longrightarrow> -l x \<le> h x \<longrightarrow> u x \<le> h x \<longrightarrow> 597 abs (f x) \<in> {0..h x}" 598 by auto 599 600qualified lemma eventually_le_abs_nonneg: 601 "eventually (\<lambda>x. l x \<ge> 0) at_top \<Longrightarrow> eventually (\<lambda>x. f x \<ge> l x) at_top \<Longrightarrow> 602 eventually (\<lambda>x::real. l x \<le> (\<bar>f x\<bar> :: real)) at_top" 603 by (auto elim: eventually_elim2) 604 605qualified lemma eventually_le_abs_nonpos: 606 "eventually (\<lambda>x. u x \<le> 0) at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> u x) at_top \<Longrightarrow> 607 eventually (\<lambda>x::real. -u x \<le> (\<bar>f x\<bar> :: real)) at_top" 608 by (auto elim: eventually_elim2) 609 610qualified lemma 611 fixes f g h :: "'a \<Rightarrow> 'b :: order" 612 shows eventually_le_less:"eventually (\<lambda>x. f x \<le> g x) F \<Longrightarrow> eventually (\<lambda>x. g x < h x) F \<Longrightarrow> 613 eventually (\<lambda>x. f x < h x) F" 614 and eventually_less_le:"eventually (\<lambda>x. f x < g x) F \<Longrightarrow> eventually (\<lambda>x. g x \<le> h x) F \<Longrightarrow> 615 eventually (\<lambda>x. f x < h x) F" 616 by (erule (1) eventually_elim2; erule (1) order.trans le_less_trans less_le_trans)+ 617 618qualified lemma eventually_pos_imp_nz [eventuallized]: "\<forall>x. f x > 0 \<longrightarrow> f x \<noteq> (0 :: 'a :: linordered_semiring)" 619 and eventually_neg_imp_nz [eventuallized]: "\<forall>x. f x < 0 \<longrightarrow> f x \<noteq> 0" 620 by auto 621 622qualified lemma 623 fixes f g l1 l2 u1 :: "'a \<Rightarrow> real" 624 assumes "eventually (\<lambda>x. l1 x \<le> f x) F" 625 assumes "eventually (\<lambda>x. f x \<le> u1 x) F" 626 assumes "eventually (\<lambda>x. abs (g x) \<ge> l2 x) F" 627 assumes "eventually (\<lambda>x. l2 x \<ge> 0) F" 628 shows bounds_smallo_imp_smallo: "l1 \<in> o[F](l2) \<Longrightarrow> u1 \<in> o[F](l2) \<Longrightarrow> f \<in> o[F](g)" 629 and bounds_bigo_imp_bigo: "l1 \<in> O[F](l2) \<Longrightarrow> u1 \<in> O[F](l2) \<Longrightarrow> f \<in> O[F](g)" 630proof - 631 assume *: "l1 \<in> o[F](l2)" "u1 \<in> o[F](l2)" 632 show "f \<in> o[F](g)" 633 proof (rule landau_o.smallI, goal_cases) 634 case (1 c) 635 from *[THEN landau_o.smallD[OF _ 1]] and assms show ?case 636 proof eventually_elim 637 case (elim x) 638 from elim have "norm (f x) \<le> c * l2 x" by simp 639 also have "\<dots> \<le> c * norm (g x)" using 1 elim by (intro mult_left_mono) auto 640 finally show ?case . 641 qed 642 qed 643next 644 assume *: "l1 \<in> O[F](l2)" "u1 \<in> O[F](l2)" 645 then obtain C1 C2 where **: "C1 > 0" "C2 > 0" "eventually (\<lambda>x. norm (l1 x) \<le> C1 * norm (l2 x)) F" 646 "eventually (\<lambda>x. norm (u1 x) \<le> C2 * norm (l2 x)) F" by (auto elim!: landau_o.bigE) 647 from this(3,4) and assms have "eventually (\<lambda>x. norm (f x) \<le> max C1 C2 * norm (g x)) F" 648 proof eventually_elim 649 case (elim x) 650 from elim have "norm (f x) \<le> max C1 C2 * l2 x" by (subst max_mult_distrib_right) auto 651 also have "\<dots> \<le> max C1 C2 * norm (g x)" using elim ** by (intro mult_left_mono) auto 652 finally show ?case . 653 qed 654 thus "f \<in> O[F](g)" by (rule bigoI) 655qed 656 657qualified lemma real_root_mono: "mono (root n)" 658 by (cases n) (auto simp: mono_def) 659 660(* TODO: support for rintmod *) 661 662ML_file \<open>multiseries_expansion_bounds.ML\<close> 663 664method_setup real_asymp = \<open> 665let 666 type flags = {verbose : bool, fallback : bool} 667 fun join_flags 668 {verbose = verbose1, fallback = fallback1} 669 {verbose = verbose2, fallback = fallback2} = 670 {verbose = verbose1 orelse verbose2, fallback = fallback1 orelse fallback2} 671 val parse_flag = 672 (Args.$$$ "verbose" >> K {verbose = true, fallback = false}) || 673 (Args.$$$ "fallback" >> K {verbose = false, fallback = true}) 674 val default_flags = {verbose = false, fallback = false} 675 val parse_flags = 676 Scan.optional (Args.parens (Parse.list1 parse_flag)) [] >> 677 (fn xs => fold join_flags xs default_flags) 678in 679 Scan.lift parse_flags --| Method.sections Simplifier.simp_modifiers >> 680 (fn flags => SIMPLE_METHOD' o 681 (if #fallback flags then Real_Asymp_Basic.tac else Real_Asymp_Bounds.tac) (#verbose flags)) 682end 683\<close> "Semi-automatic decision procedure for asymptotics of exp-log functions" 684 685end 686 687lemma "filterlim (\<lambda>x::real. sin x / x) (nhds 0) at_top" 688 by real_asymp 689 690lemma "(\<lambda>x::real. exp (sin x)) \<in> O(\<lambda>_. 1)" 691 by real_asymp 692 693lemma "(\<lambda>x::real. exp (real_of_int (floor x))) \<in> \<Theta>(\<lambda>x. exp x)" 694 by real_asymp 695 696lemma "(\<lambda>n::nat. n div 2 * ln (n div 2)) \<in> \<Theta>(\<lambda>n::nat. n * ln n)" 697 by real_asymp 698 699end 700