1section \<open>Examples for the \<open>real_asymp\<close> method\<close> 2theory Real_Asymp_Examples 3 imports Real_Asymp 4begin 5 6context 7 includes asymp_equiv_notation 8begin 9 10subsection \<open>Dominik Gruntz's examples\<close> 11 12lemma "((\<lambda>x::real. exp x * (exp (1/x - exp (-x)) - exp (1/x))) \<longlongrightarrow> -1) at_top" 13 by real_asymp 14 15lemma "((\<lambda>x::real. exp x * (exp (1/x + exp (-x) + exp (-(x^2))) - 16 exp (1/x - exp (-exp x)))) \<longlongrightarrow> 1) at_top" 17 by real_asymp 18 19lemma "filterlim (\<lambda>x::real. exp (exp (x - exp (-x)) / (1 - 1/x)) - exp (exp x)) at_top at_top" 20 by real_asymp 21 22text \<open>This example is notable because it produces an expansion of level 9.\<close> 23lemma "filterlim (\<lambda>x::real. exp (exp (exp x / (1 - 1/x))) - 24 exp (exp (exp x / (1 - 1/x - ln x powr (-ln x))))) at_bot at_top" 25 by real_asymp 26 27lemma "filterlim (\<lambda>x::real. exp (exp (exp (x + exp (-x)))) / exp (exp (exp x))) at_top at_top" 28 by real_asymp 29 30lemma "filterlim (\<lambda>x::real. exp (exp (exp x)) / (exp (exp (exp (x - exp (-exp x)))))) at_top at_top" 31 by real_asymp 32 33lemma "((\<lambda>x::real. exp (exp (exp x)) / exp (exp (exp x - exp (-exp (exp x))))) \<longlongrightarrow> 1) at_top" 34 by real_asymp 35 36lemma "((\<lambda>x::real. exp (exp x) / exp (exp x - exp (-exp (exp x)))) \<longlongrightarrow> 1) at_top" 37 by real_asymp 38 39lemma "filterlim (\<lambda>x::real. ln x ^ 2 * exp (sqrt (ln x) * ln (ln x) ^ 2 * 40 exp (sqrt (ln (ln x)) * ln (ln (ln x)) ^ 3)) / sqrt x) (at_right 0) at_top" 41 by real_asymp 42 43lemma "((\<lambda>x::real. (x * ln x * ln (x * exp x - x^2) ^ 2) / 44 ln (ln (x^2 + 2*exp (exp (3*x^3*ln x))))) \<longlongrightarrow> 1/3) at_top" 45 by real_asymp 46 47lemma "((\<lambda>x::real. (exp (x * exp (-x) / (exp (-x) + exp (-(2*x^2)/(x+1)))) - exp x) / x) 48 \<longlongrightarrow> -exp 2) at_top" 49 by real_asymp 50 51lemma "((\<lambda>x::real. (3 powr x + 5 powr x) powr (1/x)) \<longlongrightarrow> 5) at_top" 52 by real_asymp 53 54lemma "filterlim (\<lambda>x::real. x / (ln (x powr (ln x powr (ln 2 / ln x))))) at_top at_top" 55 by real_asymp 56 57lemma "filterlim (\<lambda>x::real. exp (exp (2*ln (x^5 + x) * ln (ln x))) / 58 exp (exp (10*ln x * ln (ln x)))) at_top at_top" 59 by real_asymp 60 61lemma "filterlim (\<lambda>x::real. 4/9 * (exp (exp (5/2*x powr (-5/7) + 21/8*x powr (6/11) + 62 2*x powr (-8) + 54/17*x powr (49/45))) ^ 8) / (ln (ln (-ln (4/3*x powr (-5/14)))))) 63 at_top at_top" 64 by real_asymp 65 66lemma "((\<lambda>x::real. (exp (4*x*exp (-x) / 67 (1/exp x + 1/exp (2*x^2/(x+1)))) - exp x) / ((exp x)^4)) \<longlongrightarrow> 1) at_top " 68 by real_asymp 69 70lemma "((\<lambda>x::real. exp (x*exp (-x) / (exp (-x) + exp (-2*x^2/(x+1))))/exp x) \<longlongrightarrow> 1) at_top" 71 by real_asymp 72 73lemma "((\<lambda>x::real. exp (exp (-x/(1+exp (-x)))) * exp (-x/(1+exp (-x/(1+exp (-x))))) * 74 exp (exp (-x+exp (-x/(1+exp (-x))))) / (exp (-x/(1+exp (-x))))^2 - exp x + x) 75 \<longlongrightarrow> 2) at_top" 76 by real_asymp 77 78lemma "((\<lambda>x::real. (ln(ln x + ln (ln x)) - ln (ln x)) / 79 (ln (ln x + ln (ln (ln x)))) * ln x) \<longlongrightarrow> 1) at_top" 80 by real_asymp 81 82lemma "((\<lambda>x::real. exp (ln (ln (x + exp (ln x * ln (ln x)))) / 83 (ln (ln (ln (exp x + x + ln x)))))) \<longlongrightarrow> exp 1) at_top" 84 by real_asymp 85 86lemma "((\<lambda>x::real. exp x * (sin (1/x + exp (-x)) - sin (1/x + exp (-(x^2))))) \<longlongrightarrow> 1) at_top" 87 by real_asymp 88 89lemma "((\<lambda>x::real. exp (exp x) * (exp (sin (1/x + exp (-exp x))) - exp (sin (1/x)))) \<longlongrightarrow> 1) at_top" 90 by real_asymp 91 92lemma "((\<lambda>x::real. max x (exp x) / ln (min (exp (-x)) (exp (-exp x)))) \<longlongrightarrow> -1) at_top" 93 by real_asymp 94 95text \<open>The following example is taken from the paper by Richardson \<^emph>\<open>et al\<close>.\<close> 96lemma 97 defines "f \<equiv> (\<lambda>x::real. ln (ln (x * exp (x * exp x) + 1)) - exp (exp (ln (ln x) + 1 / x)))" 98 shows "(f \<longlongrightarrow> 0) at_top" (is ?thesis1) 99 "f \<sim> (\<lambda>x. -(ln x ^ 2) / (2*x))" (is ?thesis2) 100 unfolding f_def by real_asymp+ 101 102 103subsection \<open>Asymptotic inequalities related to the Akra--Bazzi theorem\<close> 104 105definition "akra_bazzi_asymptotic1 b hb e p x \<longleftrightarrow> 106 (1 - hb * inverse b * ln x powr -(1+e)) powr p * (1 + ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2)) 107 \<ge> 1 + (ln x powr (-e/2) :: real)" 108definition "akra_bazzi_asymptotic1' b hb e p x \<longleftrightarrow> 109 (1 + hb * inverse b * ln x powr -(1+e)) powr p * (1 + ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2)) 110 \<ge> 1 + (ln x powr (-e/2) :: real)" 111definition "akra_bazzi_asymptotic2 b hb e p x \<longleftrightarrow> 112 (1 + hb * inverse b * ln x powr -(1+e)) powr p * (1 - ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2)) 113 \<le> 1 - ln x powr (-e/2 :: real)" 114definition "akra_bazzi_asymptotic2' b hb e p x \<longleftrightarrow> 115 (1 - hb * inverse b * ln x powr -(1+e)) powr p * (1 - ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2)) 116 \<le> 1 - ln x powr (-e/2 :: real)" 117definition "akra_bazzi_asymptotic3 e x \<longleftrightarrow> (1 + (ln x powr (-e/2))) / 2 \<le> (1::real)" 118definition "akra_bazzi_asymptotic4 e x \<longleftrightarrow> (1 - (ln x powr (-e/2))) * 2 \<ge> (1::real)" 119definition "akra_bazzi_asymptotic5 b hb e x \<longleftrightarrow> 120 ln (b*x - hb*x*ln x powr -(1+e)) powr (-e/2::real) < 1" 121 122definition "akra_bazzi_asymptotic6 b hb e x \<longleftrightarrow> hb / ln x powr (1 + e :: real) < b/2" 123definition "akra_bazzi_asymptotic7 b hb e x \<longleftrightarrow> hb / ln x powr (1 + e :: real) < (1 - b) / 2" 124definition "akra_bazzi_asymptotic8 b hb e x \<longleftrightarrow> x*(1 - b - hb / ln x powr (1 + e :: real)) > 1" 125 126definition "akra_bazzi_asymptotics b hb e p x \<longleftrightarrow> 127 akra_bazzi_asymptotic1 b hb e p x \<and> akra_bazzi_asymptotic1' b hb e p x \<and> 128 akra_bazzi_asymptotic2 b hb e p x \<and> akra_bazzi_asymptotic2' b hb e p x \<and> 129 akra_bazzi_asymptotic3 e x \<and> akra_bazzi_asymptotic4 e x \<and> akra_bazzi_asymptotic5 b hb e x \<and> 130 akra_bazzi_asymptotic6 b hb e x \<and> akra_bazzi_asymptotic7 b hb e x \<and> 131 akra_bazzi_asymptotic8 b hb e x" 132 133lemmas akra_bazzi_asymptotic_defs = 134 akra_bazzi_asymptotic1_def akra_bazzi_asymptotic1'_def 135 akra_bazzi_asymptotic2_def akra_bazzi_asymptotic2'_def akra_bazzi_asymptotic3_def 136 akra_bazzi_asymptotic4_def akra_bazzi_asymptotic5_def akra_bazzi_asymptotic6_def 137 akra_bazzi_asymptotic7_def akra_bazzi_asymptotic8_def akra_bazzi_asymptotics_def 138 139lemma akra_bazzi_asymptotics: 140 assumes "\<And>b. b \<in> set bs \<Longrightarrow> b \<in> {0<..<1}" and "e > 0" 141 shows "eventually (\<lambda>x. \<forall>b\<in>set bs. akra_bazzi_asymptotics b hb e p x) at_top" 142proof (intro eventually_ball_finite ballI) 143 fix b assume "b \<in> set bs" 144 with assms have "b \<in> {0<..<1}" by simp 145 with \<open>e > 0\<close> show "eventually (\<lambda>x. akra_bazzi_asymptotics b hb e p x) at_top" 146 unfolding akra_bazzi_asymptotic_defs 147 by (intro eventually_conj; real_asymp simp: mult_neg_pos) 148qed simp 149 150lemma 151 fixes b \<epsilon> :: real 152 assumes "b \<in> {0<..<1}" and "\<epsilon> > 0" 153 shows "filterlim (\<lambda>x. (1 - H / (b * ln x powr (1 + \<epsilon>))) powr p * 154 (1 + ln (b * x + H * x / ln x powr (1+\<epsilon>)) powr (-\<epsilon>/2)) - 155 (1 + ln x powr (-\<epsilon>/2))) (at_right 0) at_top" 156 using assms by (real_asymp simp: mult_neg_pos) 157 158context 159 fixes b e p :: real 160 assumes assms: "b > 0" "e > 0" 161begin 162 163lemmas [simp] = mult_neg_pos 164 165real_limit "(\<lambda>x. ((1 - 1 / (b * ln x powr (1 + e))) powr p * 166 (1 + ln (b * x + x / ln x powr (1+e)) powr (-e/2)) - 167 (1 + ln x powr (-e/2))) * ln x powr ((e / 2) + 1))" 168 facts: assms 169 170end 171 172context 173 fixes b \<epsilon> :: real 174 assumes assms: "b > 0" "\<epsilon> > 0" "\<epsilon> < 1 / 4" 175begin 176 177real_expansion "(\<lambda>x. (1 - H / (b * ln x powr (1 + \<epsilon>))) powr p * 178 (1 + ln (b * x + H * x / ln x powr (1+\<epsilon>)) powr (-\<epsilon>/2)) - 179 (1 + ln x powr (-\<epsilon>/2)))" 180 terms: 10 (strict) 181 facts: assms 182 183end 184 185context 186 fixes e :: real 187 assumes e: "e > 0" "e < 1 / 4" 188begin 189 190real_expansion "(\<lambda>x. (1 - 1 / (1/2 * ln x powr (1 + e))) * 191 (1 + ln (1/2 * x + x / ln x powr (1+e)) powr (-e/2)) - 192 (1 + ln x powr (-e/2)))" 193 terms: 10 (strict) 194 facts: e 195 196end 197 198 199subsection \<open>Concrete Mathematics\<close> 200 201text \<open>The following inequalities are discussed on p.\ 441 in Concrete Mathematics.\<close> 202lemma 203 fixes c \<epsilon> :: real 204 assumes "0 < \<epsilon>" "\<epsilon> < 1" "1 < c" 205 shows "(\<lambda>_::real. 1) \<in> o(\<lambda>x. ln (ln x))" 206 and "(\<lambda>x::real. ln (ln x)) \<in> o(\<lambda>x. ln x)" 207 and "(\<lambda>x::real. ln x) \<in> o(\<lambda>x. x powr \<epsilon>)" 208 and "(\<lambda>x::real. x powr \<epsilon>) \<in> o(\<lambda>x. x powr c)" 209 and "(\<lambda>x. x powr c) \<in> o(\<lambda>x. x powr ln x)" 210 and "(\<lambda>x. x powr ln x) \<in> o(\<lambda>x. c powr x)" 211 and "(\<lambda>x. c powr x) \<in> o(\<lambda>x. x powr x)" 212 and "(\<lambda>x. x powr x) \<in> o(\<lambda>x. c powr (c powr x))" 213 using assms by (real_asymp (verbose))+ 214 215 216subsection \<open>Stack Exchange\<close> 217 218text \<open> 219 http://archives.math.utk.edu/visual.calculus/1/limits.15/ 220\<close> 221lemma "filterlim (\<lambda>x::real. (x * sin x) / abs x) (at_right 0) (at 0)" 222 by real_asymp 223 224lemma "filterlim (\<lambda>x::real. x^2 / (sqrt (x^2 + 12) - sqrt (12))) (nhds (12 / sqrt 3)) (at 0)" 225proof - 226 note [simp] = powr_half_sqrt sqrt_def (* TODO: Better simproc for sqrt/root? *) 227 have "sqrt (12 :: real) = sqrt (4 * 3)" 228 by simp 229 also have "\<dots> = 2 * sqrt 3" by (subst real_sqrt_mult) simp 230 finally show ?thesis by real_asymp 231qed 232 233 234text \<open>\<^url>\<open>http://math.stackexchange.com/questions/625574\<close>\<close> 235lemma "(\<lambda>x::real. (1 - 1/2 * x^2 - cos (x / (1 - x^2))) / x^4) \<midarrow>0\<rightarrow> 23/24" 236 by real_asymp 237 238 239text \<open>\<^url>\<open>http://math.stackexchange.com/questions/122967\<close>\<close> 240 241real_limit "\<lambda>x. (x + 1) powr (1 + 1 / x) - x powr (1 + 1 / (x + a))" 242 243lemma "((\<lambda>x::real. ((x + 1) powr (1 + 1/x) - x powr (1 + 1 / (x + a)))) \<longlongrightarrow> 1) at_top" 244 by real_asymp 245 246 247real_limit "\<lambda>x. x ^ 2 * (arctan x - pi / 2) + x" 248 249lemma "filterlim (\<lambda>x::real. x^2 * (arctan x - pi/2) + x) (at_right 0) at_top" 250 by real_asymp 251 252 253real_limit "\<lambda>x. (root 3 (x ^ 3 + x ^ 2 + x + 1) - sqrt (x ^ 2 + x + 1) * ln (exp x + x) / x)" 254 255lemma "((\<lambda>x::real. root 3 (x^3 + x^2 + x + 1) - sqrt (x^2 + x + 1) * ln (exp x + x) / x) 256 \<longlongrightarrow> -1/6) at_top" 257 by real_asymp 258 259 260context 261 fixes a b :: real 262 assumes ab: "a > 0" "b > 0" 263begin 264real_limit "\<lambda>x. ((a powr x - x * ln a) / (b powr x - x * ln b)) powr (1 / x ^ 2)" 265 limit: "at_right 0" facts: ab 266real_limit "\<lambda>x. ((a powr x - x * ln a) / (b powr x - x * ln b)) powr (1 / x ^ 2)" 267 limit: "at_left 0" facts: ab 268lemma "(\<lambda>x. ((a powr x - x * ln a) / (b powr x - x * ln b)) powr (1 / x ^ 2)) 269 \<midarrow>0\<rightarrow> exp (ln a * ln a / 2 - ln b * ln b / 2)" using ab by real_asymp 270end 271 272 273text \<open>\<^url>\<open>http://math.stackexchange.com/questions/547538\<close>\<close> 274lemma "(\<lambda>x::real. ((x+4) powr (3/2) + exp x - 9) / x) \<midarrow>0\<rightarrow> 4" 275 by real_asymp 276 277text \<open>\<^url>\<open>https://www.freemathhelp.com/forum/threads/93513\<close>\<close> 278lemma "((\<lambda>x::real. ((3 powr x + 4 powr x) / 4) powr (1/x)) \<longlongrightarrow> 4) at_top" 279 by real_asymp 280 281lemma "((\<lambda>x::real. x powr (3/2) * (sqrt (x + 1) + sqrt (x - 1) - 2 * sqrt x)) \<longlongrightarrow> -1/4) at_top" 282 by real_asymp 283 284 285text \<open>\<^url>\<open>https://www.math.ucdavis.edu/~kouba/CalcOneDIRECTORY/limcondirectory/LimitConstant.html\<close>\<close> 286lemma "(\<lambda>x::real. (cos (2*x) - 1) / (cos x - 1)) \<midarrow>0\<rightarrow> 4" 287 by real_asymp 288 289lemma "(\<lambda>x::real. tan (2*x) / (x - pi/2)) \<midarrow>pi/2\<rightarrow> 2" 290 by real_asymp 291 292 293text \<open>@url{"https://www.math.ucdavis.edu/~kouba/CalcOneDIRECTORY/liminfdirectory/LimitInfinity.html"}\<close> 294lemma "filterlim (\<lambda>x::real. (3 powr x + 3 powr (2*x)) powr (1/x)) (nhds 9) at_top" 295 using powr_def[of 3 "2::real"] by real_asymp 296 297text \<open>\<^url>\<open>https://www.math.ucdavis.edu/~kouba/CalcOneDIRECTORY/lhopitaldirectory/LHopital.html\<close>\<close> 298lemma "filterlim (\<lambda>x::real. (x^2 - 1) / (x^2 + 3*x - 4)) (nhds (2/5)) (at 1)" 299 by real_asymp 300 301lemma "filterlim (\<lambda>x::real. (x - 4) / (sqrt x - 2)) (nhds 4) (at 4)" 302 by real_asymp 303 304lemma "filterlim (\<lambda>x::real. sin x / x) (at_left 1) (at 0)" 305 by real_asymp 306 307lemma "filterlim (\<lambda>x::real. (3 powr x - 2 powr x) / (x^2 - x)) (nhds (ln (2/3))) (at 0)" 308 by (real_asymp simp: ln_div) 309 310lemma "filterlim (\<lambda>x::real. (1/x - 1/3) / (x^2 - 9)) (nhds (-1/54)) (at 3)" 311 by real_asymp 312 313lemma "filterlim (\<lambda>x::real. (x * tan x) / sin (3*x)) (nhds 0) (at 0)" 314 by real_asymp 315 316lemma "filterlim (\<lambda>x::real. sin (x^2) / (x * tan x)) (at 1) (at 0)" 317 by real_asymp 318 319lemma "filterlim (\<lambda>x::real. (x^2 * exp x) / tan x ^ 2) (at 1) (at 0)" 320 by real_asymp 321 322lemma "filterlim (\<lambda>x::real. exp (-1/x^2) / x^2) (at 0) (at 0)" 323 by real_asymp 324 325lemma "filterlim (\<lambda>x::real. exp x / (5 * x + 200)) at_top at_top" 326 by real_asymp 327 328lemma "filterlim (\<lambda>x::real. (3 + ln x) / (x^2 + 7)) (at 0) at_top" 329 by real_asymp 330 331lemma "filterlim (\<lambda>x::real. (x^2 + 3*x - 10) / (7*x^2 - 5*x + 4)) (at_right (1/7)) at_top" 332 by real_asymp 333 334lemma "filterlim (\<lambda>x::real. (ln x ^ 2) / exp (2*x)) (at_right 0) at_top" 335 by real_asymp 336 337lemma "filterlim (\<lambda>x::real. (3 * x + 2 powr x) / (2 * x + 3 powr x)) (at 0) at_top" 338 by real_asymp 339 340lemma "filterlim (\<lambda>x::real. (exp x + 2 / x) / (exp x + 5 / x)) (at_left 1) at_top" 341 by real_asymp 342 343lemma "filterlim (\<lambda>x::real. sqrt (x^2 + 1) - sqrt (x + 1)) at_top at_top" 344 by real_asymp 345 346 347lemma "filterlim (\<lambda>x::real. x * ln x) (at_left 0) (at_right 0)" 348 by real_asymp 349 350lemma "filterlim (\<lambda>x::real. x * ln x ^ 2) (at_right 0) (at_right 0)" 351 by real_asymp 352 353lemma "filterlim (\<lambda>x::real. ln x * tan x) (at_left 0) (at_right 0)" 354 by real_asymp 355 356lemma "filterlim (\<lambda>x::real. x powr sin x) (at_left 1) (at_right 0)" 357 by real_asymp 358 359lemma "filterlim (\<lambda>x::real. (1 + 3 / x) powr x) (at_left (exp 3)) at_top" 360 by real_asymp 361 362lemma "filterlim (\<lambda>x::real. (1 - x) powr (1 / x)) (at_left (exp (-1))) (at_right 0)" 363 by real_asymp 364 365lemma "filterlim (\<lambda>x::real. (tan x) powr x^2) (at_left 1) (at_right 0)" 366 by real_asymp 367 368lemma "filterlim (\<lambda>x::real. x powr (1 / sqrt x)) (at_right 1) at_top" 369 by real_asymp 370 371lemma "filterlim (\<lambda>x::real. ln x powr (1/x)) (at_right 1) at_top" 372 by (real_asymp (verbose)) 373 374lemma "filterlim (\<lambda>x::real. x powr (x powr x)) (at_right 0) (at_right 0)" 375 by (real_asymp (verbose)) 376 377 378text \<open>\<^url>\<open>http://calculus.nipissingu.ca/problems/limit_problems.html\<close>\<close> 379lemma "((\<lambda>x::real. (x^2 - 1) / \<bar>x - 1\<bar>) \<longlongrightarrow> -2) (at_left 1)" 380 "((\<lambda>x::real. (x^2 - 1) / \<bar>x - 1\<bar>) \<longlongrightarrow> 2) (at_right 1)" 381 by real_asymp+ 382 383lemma "((\<lambda>x::real. (root 3 x - 1) / \<bar>sqrt x - 1\<bar>) \<longlongrightarrow> -2 / 3) (at_left 1)" 384 "((\<lambda>x::real. (root 3 x - 1) / \<bar>sqrt x - 1\<bar>) \<longlongrightarrow> 2 / 3) (at_right 1)" 385 by real_asymp+ 386 387 388text \<open>\<^url>\<open>https://math.stackexchange.com/questions/547538\<close>\<close> 389 390lemma "(\<lambda>x::real. ((x + 4) powr (3/2) + exp x - 9) / x) \<midarrow>0\<rightarrow> 4" 391 by real_asymp 392 393text \<open>\<^url>\<open>https://math.stackexchange.com/questions/625574\<close>\<close> 394lemma "(\<lambda>x::real. (1 - x^2 / 2 - cos (x / (1 - x^2))) / x^4) \<midarrow>0\<rightarrow> 23/24" 395 by real_asymp 396 397text \<open>\<^url>\<open>https://www.mapleprimes.com/questions/151308-A-Hard-Limit-Question\<close>\<close> 398lemma "(\<lambda>x::real. x / (x - 1) - 1 / ln x) \<midarrow>1\<rightarrow> 1 / 2" 399 by real_asymp 400 401text \<open>\<^url>\<open>https://www.freemathhelp.com/forum/threads/93513-two-extremely-difficult-limit-problems\<close>\<close> 402lemma "((\<lambda>x::real. ((3 powr x + 4 powr x) / 4) powr (1/x)) \<longlongrightarrow> 4) at_top" 403 by real_asymp 404 405lemma "((\<lambda>x::real. x powr 1.5 * (sqrt (x + 1) + sqrt (x - 1) - 2 * sqrt x)) \<longlongrightarrow> -1/4) at_top" 406 by real_asymp 407 408text \<open>\<^url>\<open>https://math.stackexchange.com/questions/1390833\<close>\<close> 409context 410 fixes a b :: real 411 assumes ab: "a + b > 0" "a + b = 1" 412begin 413real_limit "\<lambda>x. (a * x powr (1 / x) + b) powr (x / ln x)" 414 facts: ab 415end 416 417 418subsection \<open>Unsorted examples\<close> 419 420context 421 fixes a :: real 422 assumes a: "a > 1" 423begin 424 425text \<open> 426 It seems that Mathematica fails to expand the following example when \<open>a\<close> is a variable. 427\<close> 428lemma "(\<lambda>x. 1 - (1 - 1 / x powr a) powr x) \<sim> (\<lambda>x. x powr (1 - a))" 429 using a by real_asymp 430 431real_limit "\<lambda>x. (1 - (1 - 1 / x powr a) powr x) * x powr (a - 1)" 432 facts: a 433 434lemma "(\<lambda>n. log 2 (real ((n + 3) choose 3) / 4) + 1) \<sim> (\<lambda>n. 3 / ln 2 * ln n)" 435proof - 436 have "(\<lambda>n. log 2 (real ((n + 3) choose 3) / 4) + 1) = 437 (\<lambda>n. log 2 ((real n + 1) * (real n + 2) * (real n + 3) / 24) + 1)" 438 by (subst binomial_gbinomial) 439 (simp add: gbinomial_pochhammer' numeral_3_eq_3 pochhammer_Suc add_ac) 440 moreover have "\<dots> \<sim> (\<lambda>n. 3 / ln 2 * ln n)" 441 by (real_asymp simp: field_split_simps) 442 ultimately show ?thesis by simp 443qed 444 445end 446 447lemma "(\<lambda>x::real. exp (sin x) / ln (cos x)) \<sim>[at 0] (\<lambda>x. -2 / x ^ 2)" 448 by real_asymp 449 450real_limit "\<lambda>x. ln (1 + 1 / x) * x" 451real_limit "\<lambda>x. ln x powr ln x / x" 452real_limit "\<lambda>x. (arctan x - pi/2) * x" 453real_limit "\<lambda>x. arctan (1/x) * x" 454 455context 456 fixes c :: real assumes c: "c \<ge> 2" 457begin 458lemma c': "c^2 - 3 > 0" 459proof - 460 from c have "c^2 \<ge> 2^2" by (rule power_mono) auto 461 thus ?thesis by simp 462qed 463 464real_limit "\<lambda>x. (c^2 - 3) * exp (-x)" 465real_limit "\<lambda>x. (c^2 - 3) * exp (-x)" facts: c' 466end 467 468lemma "c < 0 \<Longrightarrow> ((\<lambda>x::real. exp (c*x)) \<longlongrightarrow> 0) at_top" 469 by real_asymp 470 471lemma "filterlim (\<lambda>x::real. -exp (1/x)) (at_left 0) (at_left 0)" 472 by real_asymp 473 474lemma "((\<lambda>t::real. t^2 / (exp t - 1)) \<longlongrightarrow> 0) at_top" 475 by real_asymp 476 477lemma "(\<lambda>n. (1 + 1 / real n) ^ n) \<longlonglongrightarrow> exp 1" 478 by real_asymp 479 480lemma "((\<lambda>x::real. (1 + y / x) powr x) \<longlongrightarrow> exp y) at_top" 481 by real_asymp 482 483lemma "eventually (\<lambda>x::real. x < x^2) at_top" 484 by real_asymp 485 486lemma "eventually (\<lambda>x::real. 1 / x^2 \<ge> 1 / x) (at_left 0)" 487 by real_asymp 488 489lemma "A > 1 \<Longrightarrow> (\<lambda>n. ((1 + 1 / sqrt A) / 2) powr real_of_int (2 ^ Suc n)) \<longlonglongrightarrow> 0" 490 by (real_asymp simp: field_split_simps add_pos_pos) 491 492lemma 493 assumes "c > (1 :: real)" "k \<noteq> 0" 494 shows "(\<lambda>n. real n ^ k) \<in> o(\<lambda>n. c ^ n)" 495 using assms by (real_asymp (verbose)) 496 497lemma "(\<lambda>x::real. exp (-(x^4))) \<in> o(\<lambda>x. exp (-(x^4)) + 1 / x ^ n)" 498 by real_asymp 499 500lemma "(\<lambda>x::real. x^2) \<in> o[at_right 0](\<lambda>x. x)" 501 by real_asymp 502 503lemma "(\<lambda>x::real. x^2) \<in> o[at_left 0](\<lambda>x. x)" 504 by real_asymp 505 506lemma "(\<lambda>x::real. 2 * x + x ^ 2) \<in> \<Theta>[at_left 0](\<lambda>x. x)" 507 by real_asymp 508 509lemma "(\<lambda>x::real. inverse (x - 1)^2) \<in> \<omega>[at 1](\<lambda>x. x)" 510 by real_asymp 511 512lemma "(\<lambda>x::real. sin (1 / x)) \<sim> (\<lambda>x::real. 1 / x)" 513 by real_asymp 514 515lemma 516 assumes "q \<in> {0<..<1}" 517 shows "LIM x at_left 1. log q (1 - x) :> at_top" 518 using assms by real_asymp 519 520context 521 fixes x k :: real 522 assumes xk: "x > 1" "k > 0" 523begin 524 525lemmas [simp] = add_pos_pos 526 527real_expansion "\<lambda>l. sqrt (1 + l * (l + 1) * 4 * pi^2 * k^2 * (log x (l + 1) - log x l)^2)" 528 terms: 2 facts: xk 529 530lemma 531 "(\<lambda>l. sqrt (1 + l * (l + 1) * 4 * pi^2 * k^2 * (log x (l + 1) - log x l)^2) - 532 sqrt (1 + 4 * pi\<^sup>2 * k\<^sup>2 / (ln x ^ 2))) \<in> O(\<lambda>l. 1 / l ^ 2)" 533 using xk by (real_asymp simp: inverse_eq_divide power_divide root_powr_inverse) 534 535end 536 537lemma "(\<lambda>x. (2 * x^3 - 128) / (sqrt x - 2)) \<midarrow>4\<rightarrow> 384" 538 by real_asymp 539 540lemma 541 "((\<lambda>x::real. (x^2 - 1) / abs (x - 1)) \<longlongrightarrow> 2) (at_right 1)" 542 "((\<lambda>x::real. (x^2 - 1) / abs (x - 1)) \<longlongrightarrow> -2) (at_left 1)" 543 by real_asymp+ 544 545lemma "(\<lambda>x::real. (root 3 x - 1) / (sqrt x - 1)) \<midarrow>1\<rightarrow> 2/3" 546 by real_asymp 547 548lemma 549 fixes a b :: real 550 assumes "a > 1" "b > 1" "a \<noteq> b" 551 shows "((\<lambda>x. ((a powr x - x * ln a) / (b powr x - x * ln b)) powr (1/x^3)) \<longlongrightarrow> 1) at_top" 552 using assms by real_asymp 553 554 555context 556 fixes a b :: real 557 assumes ab: "a > 0" "b > 0" 558begin 559 560lemma 561 "((\<lambda>x. ((a powr x - x * ln a) / (b powr x - x * ln b)) powr (1 / x ^ 2)) \<longlongrightarrow> 562 exp ((ln a ^ 2 - ln b ^ 2) / 2)) (at 0)" 563 using ab by (real_asymp simp: power2_eq_square) 564 565end 566 567real_limit "\<lambda>x. 1 / sin (1/x) ^ 2 + 1 / tan (1/x) ^ 2 - 2 * x ^ 2" 568 569real_limit "\<lambda>x. ((1 / x + 4) powr 1.5 + exp (1 / x) - 9) * x" 570 571lemma "x > (1 :: real) \<Longrightarrow> 572 ((\<lambda>n. abs (x powr n / (n * (1 + x powr (2 * n)))) powr (1 / n)) \<longlongrightarrow> 1 / x) at_top" 573 by (real_asymp simp add: exp_minus field_simps) 574 575lemma "x = (1 :: real) \<Longrightarrow> 576 ((\<lambda>n. abs (x powr n / (n * (1 + x powr (2 * n)))) powr (1 / n)) \<longlongrightarrow> 1 / x) at_top" 577 by (real_asymp simp add: exp_minus field_simps) 578 579lemma "x > (0 :: real) \<Longrightarrow> x < 1 \<Longrightarrow> 580 ((\<lambda>n. abs (x powr n / (n * (1 + x powr (2 * n)))) powr (1 / n)) \<longlongrightarrow> x) at_top" 581 by real_asymp 582 583lemma "(\<lambda>x. (exp (sin b) - exp (sin (b * x))) * tan (pi * x / 2)) \<midarrow>1\<rightarrow> 584 (2*b/pi * exp (sin b) * cos b)" 585 by real_asymp 586 587(* SLOW *) 588lemma "filterlim (\<lambda>x::real. (sin (tan x) - tan (sin x))) (at 0) (at 0)" 589 by real_asymp 590 591(* SLOW *) 592lemma "(\<lambda>x::real. 1 / sin x powr (tan x ^ 2)) \<midarrow>pi/2\<rightarrow> exp (1 / 2)" 593 by (real_asymp simp: exp_minus) 594 595lemma "a > 0 \<Longrightarrow> b > 0 \<Longrightarrow> c > 0 \<Longrightarrow> 596 filterlim (\<lambda>x::real. ((a powr x + b powr x + c powr x) / 3) powr (3 / x)) 597 (nhds (a * b * c)) (at 0)" 598 by (real_asymp simp: exp_add add_divide_distrib exp_minus algebra_simps) 599 600real_expansion "\<lambda>x. arctan (sin (1 / x))" 601 602real_expansion "\<lambda>x. ln (1 + 1 / x)" 603 terms: 5 (strict) 604 605real_expansion "\<lambda>x. sqrt (x + 1) - sqrt (x - 1)" 606 terms: 3 (strict) 607 608 609text \<open> 610 In this example, the first 7 terms of \<open>tan (sin x)\<close> and \<open>sin (tan x)\<close> coincide, which makes 611 the calculation a bit slow. 612\<close> 613real_limit "\<lambda>x. (tan (sin x) - sin (tan x)) / x ^ 7" limit: "at_right 0" 614 615(* SLOW *) 616real_expansion "\<lambda>x. sin (tan (1/x)) - tan (sin (1/x))" 617 terms: 1 (strict) 618 619(* SLOW *) 620real_expansion "\<lambda>x. tan (1 / x)" 621 terms: 6 622 623real_expansion "\<lambda>x::real. arctan x" 624 625real_expansion "\<lambda>x. sin (tan (1/x))" 626 627real_expansion "\<lambda>x. (sin (-1 / x) ^ 2) powr sin (-1/x)" 628 629real_limit "\<lambda>x. exp (max (sin x) 1)" 630 631lemma "filterlim (\<lambda>x::real. 1 - 1 / x + ln x) at_top at_top" 632 by (force intro: tendsto_diff filterlim_tendsto_add_at_top 633 real_tendsto_divide_at_top filterlim_ident ln_at_top) 634 635lemma "filterlim (\<lambda>i::real. i powr (-i/(i-1)) - i powr (-1/(i-1))) (at_left 1) (at_right 0)" 636 by real_asymp 637 638lemma "filterlim (\<lambda>i::real. i powr (-i/(i-1)) - i powr (-1/(i-1))) (at_right (-1)) at_top" 639 by real_asymp 640 641lemma "eventually (\<lambda>i::real. i powr (-i/(i-1)) - i powr (-1/(i-1)) < 1) (at_right 0)" 642 and "eventually (\<lambda>i::real. i powr (-i/(i-1)) - i powr (-1/(i-1)) > -1) at_top" 643 by real_asymp+ 644 645end 646 647 648subsection \<open>Interval arithmetic tests\<close> 649 650lemma "filterlim (\<lambda>x::real. x + sin x) at_top at_top" 651 "filterlim (\<lambda>x::real. sin x + x) at_top at_top" 652 "filterlim (\<lambda>x::real. x + (sin x + sin x)) at_top at_top" 653 by real_asymp+ 654 655lemma "filterlim (\<lambda>x::real. 2 * x + sin x * x) at_infinity at_top" 656 "filterlim (\<lambda>x::real. 2 * x + (sin x + 1) * x) at_infinity at_top" 657 "filterlim (\<lambda>x::real. 3 * x + (sin x - 1) * x) at_infinity at_top" 658 "filterlim (\<lambda>x::real. 2 * x + x * sin x) at_infinity at_top" 659 "filterlim (\<lambda>x::real. 2 * x + x * (sin x + 1)) at_infinity at_top" 660 "filterlim (\<lambda>x::real. 3 * x + x * (sin x - 1)) at_infinity at_top" 661 662 "filterlim (\<lambda>x::real. x + sin x * sin x) at_infinity at_top" 663 "filterlim (\<lambda>x::real. x + sin x * (sin x + 1)) at_infinity at_top" 664 "filterlim (\<lambda>x::real. x + sin x * (sin x - 1)) at_infinity at_top" 665 "filterlim (\<lambda>x::real. x + sin x * (sin x + 2)) at_infinity at_top" 666 "filterlim (\<lambda>x::real. x + sin x * (sin x - 2)) at_infinity at_top" 667 668 "filterlim (\<lambda>x::real. x + (sin x - 1) * sin x) at_infinity at_top" 669 "filterlim (\<lambda>x::real. x + (sin x - 1) * (sin x + 1)) at_infinity at_top" 670 "filterlim (\<lambda>x::real. x + (sin x - 1) * (sin x - 1)) at_infinity at_top" 671 "filterlim (\<lambda>x::real. x + (sin x - 1) * (sin x + 2)) at_infinity at_top" 672 "filterlim (\<lambda>x::real. x + (sin x - 1) * (sin x - 2)) at_infinity at_top" 673 674 "filterlim (\<lambda>x::real. x + (sin x - 2) * sin x) at_infinity at_top" 675 "filterlim (\<lambda>x::real. x + (sin x - 2) * (sin x + 1)) at_infinity at_top" 676 "filterlim (\<lambda>x::real. x + (sin x - 2) * (sin x - 1)) at_infinity at_top" 677 "filterlim (\<lambda>x::real. x + (sin x - 2) * (sin x + 2)) at_infinity at_top" 678 "filterlim (\<lambda>x::real. x + (sin x - 2) * (sin x - 2)) at_infinity at_top" 679 680 "filterlim (\<lambda>x::real. x + (sin x + 1) * sin x) at_infinity at_top" 681 "filterlim (\<lambda>x::real. x + (sin x + 1) * (sin x + 1)) at_infinity at_top" 682 "filterlim (\<lambda>x::real. x + (sin x + 1) * (sin x - 1)) at_infinity at_top" 683 "filterlim (\<lambda>x::real. x + (sin x + 1) * (sin x + 2)) at_infinity at_top" 684 "filterlim (\<lambda>x::real. x + (sin x + 1) * (sin x - 2)) at_infinity at_top" 685 686 "filterlim (\<lambda>x::real. x + (sin x + 2) * sin x) at_infinity at_top" 687 "filterlim (\<lambda>x::real. x + (sin x + 2) * (sin x + 1)) at_infinity at_top" 688 "filterlim (\<lambda>x::real. x + (sin x + 2) * (sin x - 1)) at_infinity at_top" 689 "filterlim (\<lambda>x::real. x + (sin x + 2) * (sin x + 2)) at_infinity at_top" 690 "filterlim (\<lambda>x::real. x + (sin x + 2) * (sin x - 2)) at_infinity at_top" 691 by real_asymp+ 692 693lemma "filterlim (\<lambda>x::real. x * inverse (sin x + 2)) at_top at_top" 694 "filterlim (\<lambda>x::real. x * inverse (sin x - 2)) at_bot at_top" 695 "filterlim (\<lambda>x::real. x / inverse (sin x + 2)) at_top at_top" 696 "filterlim (\<lambda>x::real. x / inverse (sin x - 2)) at_bot at_top" 697 by real_asymp+ 698 699lemma "filterlim (\<lambda>x::real. \<lfloor>x\<rfloor>) at_top at_top" 700 "filterlim (\<lambda>x::real. \<lceil>x\<rceil>) at_top at_top" 701 "filterlim (\<lambda>x::real. nat \<lfloor>x\<rfloor>) at_top at_top" 702 "filterlim (\<lambda>x::real. nat \<lceil>x\<rceil>) at_top at_top" 703 "filterlim (\<lambda>x::int. nat x) at_top at_top" 704 "filterlim (\<lambda>x::int. nat x) at_top at_top" 705 "filterlim (\<lambda>n::nat. real (n mod 42) + real n) at_top at_top" 706 by real_asymp+ 707 708lemma "(\<lambda>n. real_of_int \<lfloor>n\<rfloor>) \<sim>[at_top] (\<lambda>n. real_of_int n)" 709 "(\<lambda>n. sqrt \<lfloor>n\<rfloor>) \<sim>[at_top] (\<lambda>n. sqrt n)" 710 by real_asymp+ 711 712lemma 713 "c > 1 \<Longrightarrow> (\<lambda>n::nat. 2 ^ (n div c) :: int) \<in> o(\<lambda>n. 2 ^ n)" 714 by (real_asymp simp: field_simps) 715 716lemma 717 "c > 1 \<Longrightarrow> (\<lambda>n::nat. 2 ^ (n div c) :: nat) \<in> o(\<lambda>n. 2 ^ n)" 718 by (real_asymp simp: field_simps) 719 720end