author | wenzelm |
Tue, 25 Aug 2020 15:02:56 +0200 | |
changeset 72207 | b2f6fdff21fa |
parent 70817 | dd675800469d |
permissions | -rw-r--r-- |
68630 | 1 |
section \<open>Examples for the \<open>real_asymp\<close> method\<close> |
2 |
theory Real_Asymp_Examples |
|
3 |
imports Real_Asymp |
|
4 |
begin |
|
5 |
||
6 |
context |
|
7 |
includes asymp_equiv_notation |
|
8 |
begin |
|
9 |
||
10 |
subsection \<open>Dominik Gruntz's examples\<close> |
|
11 |
||
12 |
lemma "((\<lambda>x::real. exp x * (exp (1/x - exp (-x)) - exp (1/x))) \<longlongrightarrow> -1) at_top" |
|
13 |
by real_asymp |
|
14 |
||
15 |
lemma "((\<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 |
||
19 |
lemma "filterlim (\<lambda>x::real. exp (exp (x - exp (-x)) / (1 - 1/x)) - exp (exp x)) at_top at_top" |
|
20 |
by real_asymp |
|
21 |
||
22 |
text \<open>This example is notable because it produces an expansion of level 9.\<close> |
|
23 |
lemma "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 |
||
27 |
lemma "filterlim (\<lambda>x::real. exp (exp (exp (x + exp (-x)))) / exp (exp (exp x))) at_top at_top" |
|
28 |
by real_asymp |
|
29 |
||
30 |
lemma "filterlim (\<lambda>x::real. exp (exp (exp x)) / (exp (exp (exp (x - exp (-exp x)))))) at_top at_top" |
|
31 |
by real_asymp |
|
32 |
||
33 |
lemma "((\<lambda>x::real. exp (exp (exp x)) / exp (exp (exp x - exp (-exp (exp x))))) \<longlongrightarrow> 1) at_top" |
|
34 |
by real_asymp |
|
35 |
||
36 |
lemma "((\<lambda>x::real. exp (exp x) / exp (exp x - exp (-exp (exp x)))) \<longlongrightarrow> 1) at_top" |
|
37 |
by real_asymp |
|
38 |
||
39 |
lemma "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 |
||
43 |
lemma "((\<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 |
||
47 |
lemma "((\<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 |
||
51 |
lemma "((\<lambda>x::real. (3 powr x + 5 powr x) powr (1/x)) \<longlongrightarrow> 5) at_top" |
|
52 |
by real_asymp |
|
53 |
||
54 |
lemma "filterlim (\<lambda>x::real. x / (ln (x powr (ln x powr (ln 2 / ln x))))) at_top at_top" |
|
55 |
by real_asymp |
|
56 |
||
57 |
lemma "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 |
||
61 |
lemma "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 |
||
66 |
lemma "((\<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 |
||
70 |
lemma "((\<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 |
||
73 |
lemma "((\<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 |
||
78 |
lemma "((\<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 |
||
82 |
lemma "((\<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 |
||
86 |
lemma "((\<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 |
||
89 |
lemma "((\<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 |
||
92 |
lemma "((\<lambda>x::real. max x (exp x) / ln (min (exp (-x)) (exp (-exp x)))) \<longlongrightarrow> -1) at_top" |
|
93 |
by real_asymp |
|
94 |
||
95 |
text \<open>The following example is taken from the paper by Richardson \<^emph>\<open>et al\<close>.\<close> |
|
96 |
lemma |
|
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 |
||
68680 | 103 |
subsection \<open>Asymptotic inequalities related to the Akra--Bazzi theorem\<close> |
68630 | 104 |
|
105 |
definition "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)" |
|
108 |
definition "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)" |
|
111 |
definition "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)" |
|
114 |
definition "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)" |
|
117 |
definition "akra_bazzi_asymptotic3 e x \<longleftrightarrow> (1 + (ln x powr (-e/2))) / 2 \<le> (1::real)" |
|
118 |
definition "akra_bazzi_asymptotic4 e x \<longleftrightarrow> (1 - (ln x powr (-e/2))) * 2 \<ge> (1::real)" |
|
119 |
definition "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 |
||
122 |
definition "akra_bazzi_asymptotic6 b hb e x \<longleftrightarrow> hb / ln x powr (1 + e :: real) < b/2" |
|
123 |
definition "akra_bazzi_asymptotic7 b hb e x \<longleftrightarrow> hb / ln x powr (1 + e :: real) < (1 - b) / 2" |
|
124 |
definition "akra_bazzi_asymptotic8 b hb e x \<longleftrightarrow> x*(1 - b - hb / ln x powr (1 + e :: real)) > 1" |
|
125 |
||
126 |
definition "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 |
||
133 |
lemmas 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 |
||
139 |
lemma 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" |
|
142 |
proof (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) |
|
148 |
qed simp |
|
149 |
||
150 |
lemma |
|
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 |
||
158 |
context |
|
159 |
fixes b e p :: real |
|
160 |
assumes assms: "b > 0" "e > 0" |
|
161 |
begin |
|
162 |
||
163 |
lemmas [simp] = mult_neg_pos |
|
164 |
||
165 |
real_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 |
||
170 |
end |
|
171 |
||
172 |
context |
|
173 |
fixes b \<epsilon> :: real |
|
174 |
assumes assms: "b > 0" "\<epsilon> > 0" "\<epsilon> < 1 / 4" |
|
175 |
begin |
|
176 |
||
177 |
real_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 |
||
183 |
end |
|
184 |
||
185 |
context |
|
186 |
fixes e :: real |
|
187 |
assumes e: "e > 0" "e < 1 / 4" |
|
188 |
begin |
|
189 |
||
190 |
real_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 |
||
196 |
end |
|
197 |
||
198 |
||
199 |
subsection \<open>Concrete Mathematics\<close> |
|
200 |
||
201 |
text \<open>The following inequalities are discussed on p.\ 441 in Concrete Mathematics.\<close> |
|
202 |
lemma |
|
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 |
||
216 |
subsection \<open>Stack Exchange\<close> |
|
217 |
||
218 |
text \<open> |
|
219 |
http://archives.math.utk.edu/visual.calculus/1/limits.15/ |
|
220 |
\<close> |
|
221 |
lemma "filterlim (\<lambda>x::real. (x * sin x) / abs x) (at_right 0) (at 0)" |
|
222 |
by real_asymp |
|
223 |
||
224 |
lemma "filterlim (\<lambda>x::real. x^2 / (sqrt (x^2 + 12) - sqrt (12))) (nhds (12 / sqrt 3)) (at 0)" |
|
225 |
proof - |
|
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 |
|
231 |
qed |
|
232 |
||
233 |
||
69597 | 234 |
text \<open>\<^url>\<open>http://math.stackexchange.com/questions/625574\<close>\<close> |
68630 | 235 |
lemma "(\<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 |
||
69597 | 239 |
text \<open>\<^url>\<open>http://math.stackexchange.com/questions/122967\<close>\<close> |
68630 | 240 |
|
241 |
real_limit "\<lambda>x. (x + 1) powr (1 + 1 / x) - x powr (1 + 1 / (x + a))" |
|
242 |
||
243 |
lemma "((\<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 |
||
247 |
real_limit "\<lambda>x. x ^ 2 * (arctan x - pi / 2) + x" |
|
248 |
||
249 |
lemma "filterlim (\<lambda>x::real. x^2 * (arctan x - pi/2) + x) (at_right 0) at_top" |
|
250 |
by real_asymp |
|
251 |
||
252 |
||
253 |
real_limit "\<lambda>x. (root 3 (x ^ 3 + x ^ 2 + x + 1) - sqrt (x ^ 2 + x + 1) * ln (exp x + x) / x)" |
|
254 |
||
255 |
lemma "((\<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 |
||
260 |
context |
|
261 |
fixes a b :: real |
|
262 |
assumes ab: "a > 0" "b > 0" |
|
263 |
begin |
|
264 |
real_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 |
|
266 |
real_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 |
|
268 |
lemma "(\<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 |
|
270 |
end |
|
271 |
||
272 |
||
69597 | 273 |
text \<open>\<^url>\<open>http://math.stackexchange.com/questions/547538\<close>\<close> |
68630 | 274 |
lemma "(\<lambda>x::real. ((x+4) powr (3/2) + exp x - 9) / x) \<midarrow>0\<rightarrow> 4" |
275 |
by real_asymp |
|
276 |
||
69597 | 277 |
text \<open>\<^url>\<open>https://www.freemathhelp.com/forum/threads/93513\<close>\<close> |
68630 | 278 |
lemma "((\<lambda>x::real. ((3 powr x + 4 powr x) / 4) powr (1/x)) \<longlongrightarrow> 4) at_top" |
279 |
by real_asymp |
|
280 |
||
281 |
lemma "((\<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 |
||
69597 | 285 |
text \<open>\<^url>\<open>https://www.math.ucdavis.edu/~kouba/CalcOneDIRECTORY/limcondirectory/LimitConstant.html\<close>\<close> |
68630 | 286 |
lemma "(\<lambda>x::real. (cos (2*x) - 1) / (cos x - 1)) \<midarrow>0\<rightarrow> 4" |
287 |
by real_asymp |
|
288 |
||
289 |
lemma "(\<lambda>x::real. tan (2*x) / (x - pi/2)) \<midarrow>pi/2\<rightarrow> 2" |
|
290 |
by real_asymp |
|
291 |
||
292 |
||
293 |
text \<open>@url{"https://www.math.ucdavis.edu/~kouba/CalcOneDIRECTORY/liminfdirectory/LimitInfinity.html"}\<close> |
|
294 |
lemma "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 |
||
69597 | 297 |
text \<open>\<^url>\<open>https://www.math.ucdavis.edu/~kouba/CalcOneDIRECTORY/lhopitaldirectory/LHopital.html\<close>\<close> |
68630 | 298 |
lemma "filterlim (\<lambda>x::real. (x^2 - 1) / (x^2 + 3*x - 4)) (nhds (2/5)) (at 1)" |
299 |
by real_asymp |
|
300 |
||
301 |
lemma "filterlim (\<lambda>x::real. (x - 4) / (sqrt x - 2)) (nhds 4) (at 4)" |
|
302 |
by real_asymp |
|
303 |
||
304 |
lemma "filterlim (\<lambda>x::real. sin x / x) (at_left 1) (at 0)" |
|
305 |
by real_asymp |
|
306 |
||
307 |
lemma "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 |
||
310 |
lemma "filterlim (\<lambda>x::real. (1/x - 1/3) / (x^2 - 9)) (nhds (-1/54)) (at 3)" |
|
311 |
by real_asymp |
|
312 |
||
313 |
lemma "filterlim (\<lambda>x::real. (x * tan x) / sin (3*x)) (nhds 0) (at 0)" |
|
314 |
by real_asymp |
|
315 |
||
316 |
lemma "filterlim (\<lambda>x::real. sin (x^2) / (x * tan x)) (at 1) (at 0)" |
|
317 |
by real_asymp |
|
318 |
||
319 |
lemma "filterlim (\<lambda>x::real. (x^2 * exp x) / tan x ^ 2) (at 1) (at 0)" |
|
320 |
by real_asymp |
|
321 |
||
322 |
lemma "filterlim (\<lambda>x::real. exp (-1/x^2) / x^2) (at 0) (at 0)" |
|
323 |
by real_asymp |
|
324 |
||
325 |
lemma "filterlim (\<lambda>x::real. exp x / (5 * x + 200)) at_top at_top" |
|
326 |
by real_asymp |
|
327 |
||
328 |
lemma "filterlim (\<lambda>x::real. (3 + ln x) / (x^2 + 7)) (at 0) at_top" |
|
329 |
by real_asymp |
|
330 |
||
331 |
lemma "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 |
||
334 |
lemma "filterlim (\<lambda>x::real. (ln x ^ 2) / exp (2*x)) (at_right 0) at_top" |
|
335 |
by real_asymp |
|
336 |
||
337 |
lemma "filterlim (\<lambda>x::real. (3 * x + 2 powr x) / (2 * x + 3 powr x)) (at 0) at_top" |
|
338 |
by real_asymp |
|
339 |
||
340 |
lemma "filterlim (\<lambda>x::real. (exp x + 2 / x) / (exp x + 5 / x)) (at_left 1) at_top" |
|
341 |
by real_asymp |
|
342 |
||
343 |
lemma "filterlim (\<lambda>x::real. sqrt (x^2 + 1) - sqrt (x + 1)) at_top at_top" |
|
344 |
by real_asymp |
|
345 |
||
346 |
||
347 |
lemma "filterlim (\<lambda>x::real. x * ln x) (at_left 0) (at_right 0)" |
|
348 |
by real_asymp |
|
349 |
||
350 |
lemma "filterlim (\<lambda>x::real. x * ln x ^ 2) (at_right 0) (at_right 0)" |
|
351 |
by real_asymp |
|
352 |
||
353 |
lemma "filterlim (\<lambda>x::real. ln x * tan x) (at_left 0) (at_right 0)" |
|
354 |
by real_asymp |
|
355 |
||
356 |
lemma "filterlim (\<lambda>x::real. x powr sin x) (at_left 1) (at_right 0)" |
|
357 |
by real_asymp |
|
358 |
||
359 |
lemma "filterlim (\<lambda>x::real. (1 + 3 / x) powr x) (at_left (exp 3)) at_top" |
|
360 |
by real_asymp |
|
361 |
||
362 |
lemma "filterlim (\<lambda>x::real. (1 - x) powr (1 / x)) (at_left (exp (-1))) (at_right 0)" |
|
363 |
by real_asymp |
|
364 |
||
365 |
lemma "filterlim (\<lambda>x::real. (tan x) powr x^2) (at_left 1) (at_right 0)" |
|
366 |
by real_asymp |
|
367 |
||
368 |
lemma "filterlim (\<lambda>x::real. x powr (1 / sqrt x)) (at_right 1) at_top" |
|
369 |
by real_asymp |
|
370 |
||
371 |
lemma "filterlim (\<lambda>x::real. ln x powr (1/x)) (at_right 1) at_top" |
|
372 |
by (real_asymp (verbose)) |
|
373 |
||
374 |
lemma "filterlim (\<lambda>x::real. x powr (x powr x)) (at_right 0) (at_right 0)" |
|
375 |
by (real_asymp (verbose)) |
|
376 |
||
377 |
||
69597 | 378 |
text \<open>\<^url>\<open>http://calculus.nipissingu.ca/problems/limit_problems.html\<close>\<close> |
68630 | 379 |
lemma "((\<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 |
||
383 |
lemma "((\<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 |
||
69597 | 388 |
text \<open>\<^url>\<open>https://math.stackexchange.com/questions/547538\<close>\<close> |
68630 | 389 |
|
390 |
lemma "(\<lambda>x::real. ((x + 4) powr (3/2) + exp x - 9) / x) \<midarrow>0\<rightarrow> 4" |
|
391 |
by real_asymp |
|
392 |
||
69597 | 393 |
text \<open>\<^url>\<open>https://math.stackexchange.com/questions/625574\<close>\<close> |
68630 | 394 |
lemma "(\<lambda>x::real. (1 - x^2 / 2 - cos (x / (1 - x^2))) / x^4) \<midarrow>0\<rightarrow> 23/24" |
395 |
by real_asymp |
|
396 |
||
69597 | 397 |
text \<open>\<^url>\<open>https://www.mapleprimes.com/questions/151308-A-Hard-Limit-Question\<close>\<close> |
68630 | 398 |
lemma "(\<lambda>x::real. x / (x - 1) - 1 / ln x) \<midarrow>1\<rightarrow> 1 / 2" |
399 |
by real_asymp |
|
400 |
||
69597 | 401 |
text \<open>\<^url>\<open>https://www.freemathhelp.com/forum/threads/93513-two-extremely-difficult-limit-problems\<close>\<close> |
68630 | 402 |
lemma "((\<lambda>x::real. ((3 powr x + 4 powr x) / 4) powr (1/x)) \<longlongrightarrow> 4) at_top" |
403 |
by real_asymp |
|
404 |
||
405 |
lemma "((\<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 |
||
69597 | 408 |
text \<open>\<^url>\<open>https://math.stackexchange.com/questions/1390833\<close>\<close> |
68630 | 409 |
context |
410 |
fixes a b :: real |
|
411 |
assumes ab: "a + b > 0" "a + b = 1" |
|
412 |
begin |
|
413 |
real_limit "\<lambda>x. (a * x powr (1 / x) + b) powr (x / ln x)" |
|
414 |
facts: ab |
|
415 |
end |
|
416 |
||
417 |
||
418 |
subsection \<open>Unsorted examples\<close> |
|
419 |
||
420 |
context |
|
421 |
fixes a :: real |
|
422 |
assumes a: "a > 1" |
|
423 |
begin |
|
424 |
||
425 |
text \<open> |
|
426 |
It seems that Mathematica fails to expand the following example when \<open>a\<close> is a variable. |
|
427 |
\<close> |
|
428 |
lemma "(\<lambda>x. 1 - (1 - 1 / x powr a) powr x) \<sim> (\<lambda>x. x powr (1 - a))" |
|
429 |
using a by real_asymp |
|
430 |
||
431 |
real_limit "\<lambda>x. (1 - (1 - 1 / x powr a) powr x) * x powr (a - 1)" |
|
432 |
facts: a |
|
433 |
||
434 |
lemma "(\<lambda>n. log 2 (real ((n + 3) choose 3) / 4) + 1) \<sim> (\<lambda>n. 3 / ln 2 * ln n)" |
|
435 |
proof - |
|
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)" |
|
70817
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
69597
diff
changeset
|
441 |
by (real_asymp simp: field_split_simps) |
68630 | 442 |
ultimately show ?thesis by simp |
443 |
qed |
|
444 |
||
445 |
end |
|
446 |
||
447 |
lemma "(\<lambda>x::real. exp (sin x) / ln (cos x)) \<sim>[at 0] (\<lambda>x. -2 / x ^ 2)" |
|
448 |
by real_asymp |
|
449 |
||
450 |
real_limit "\<lambda>x. ln (1 + 1 / x) * x" |
|
451 |
real_limit "\<lambda>x. ln x powr ln x / x" |
|
452 |
real_limit "\<lambda>x. (arctan x - pi/2) * x" |
|
453 |
real_limit "\<lambda>x. arctan (1/x) * x" |
|
454 |
||
455 |
context |
|
456 |
fixes c :: real assumes c: "c \<ge> 2" |
|
457 |
begin |
|
458 |
lemma c': "c^2 - 3 > 0" |
|
459 |
proof - |
|
460 |
from c have "c^2 \<ge> 2^2" by (rule power_mono) auto |
|
461 |
thus ?thesis by simp |
|
462 |
qed |
|
463 |
||
464 |
real_limit "\<lambda>x. (c^2 - 3) * exp (-x)" |
|
465 |
real_limit "\<lambda>x. (c^2 - 3) * exp (-x)" facts: c' |
|
466 |
end |
|
467 |
||
468 |
lemma "c < 0 \<Longrightarrow> ((\<lambda>x::real. exp (c*x)) \<longlongrightarrow> 0) at_top" |
|
469 |
by real_asymp |
|
470 |
||
471 |
lemma "filterlim (\<lambda>x::real. -exp (1/x)) (at_left 0) (at_left 0)" |
|
472 |
by real_asymp |
|
473 |
||
474 |
lemma "((\<lambda>t::real. t^2 / (exp t - 1)) \<longlongrightarrow> 0) at_top" |
|
475 |
by real_asymp |
|
476 |
||
477 |
lemma "(\<lambda>n. (1 + 1 / real n) ^ n) \<longlonglongrightarrow> exp 1" |
|
478 |
by real_asymp |
|
479 |
||
480 |
lemma "((\<lambda>x::real. (1 + y / x) powr x) \<longlongrightarrow> exp y) at_top" |
|
481 |
by real_asymp |
|
482 |
||
483 |
lemma "eventually (\<lambda>x::real. x < x^2) at_top" |
|
484 |
by real_asymp |
|
485 |
||
486 |
lemma "eventually (\<lambda>x::real. 1 / x^2 \<ge> 1 / x) (at_left 0)" |
|
487 |
by real_asymp |
|
488 |
||
489 |
lemma "A > 1 \<Longrightarrow> (\<lambda>n. ((1 + 1 / sqrt A) / 2) powr real_of_int (2 ^ Suc n)) \<longlonglongrightarrow> 0" |
|
70817
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
69597
diff
changeset
|
490 |
by (real_asymp simp: field_split_simps add_pos_pos) |
68630 | 491 |
|
492 |
lemma |
|
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 |
||
497 |
lemma "(\<lambda>x::real. exp (-(x^4))) \<in> o(\<lambda>x. exp (-(x^4)) + 1 / x ^ n)" |
|
498 |
by real_asymp |
|
499 |
||
500 |
lemma "(\<lambda>x::real. x^2) \<in> o[at_right 0](\<lambda>x. x)" |
|
501 |
by real_asymp |
|
502 |
||
503 |
lemma "(\<lambda>x::real. x^2) \<in> o[at_left 0](\<lambda>x. x)" |
|
504 |
by real_asymp |
|
505 |
||
506 |
lemma "(\<lambda>x::real. 2 * x + x ^ 2) \<in> \<Theta>[at_left 0](\<lambda>x. x)" |
|
507 |
by real_asymp |
|
508 |
||
509 |
lemma "(\<lambda>x::real. inverse (x - 1)^2) \<in> \<omega>[at 1](\<lambda>x. x)" |
|
510 |
by real_asymp |
|
511 |
||
512 |
lemma "(\<lambda>x::real. sin (1 / x)) \<sim> (\<lambda>x::real. 1 / x)" |
|
513 |
by real_asymp |
|
514 |
||
515 |
lemma |
|
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 |
||
520 |
context |
|
521 |
fixes x k :: real |
|
522 |
assumes xk: "x > 1" "k > 0" |
|
523 |
begin |
|
524 |
||
525 |
lemmas [simp] = add_pos_pos |
|
526 |
||
527 |
real_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 |
||
530 |
lemma |
|
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 |
||
535 |
end |
|
536 |
||
537 |
lemma "(\<lambda>x. (2 * x^3 - 128) / (sqrt x - 2)) \<midarrow>4\<rightarrow> 384" |
|
538 |
by real_asymp |
|
539 |
||
540 |
lemma |
|
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 |
||
545 |
lemma "(\<lambda>x::real. (root 3 x - 1) / (sqrt x - 1)) \<midarrow>1\<rightarrow> 2/3" |
|
546 |
by real_asymp |
|
547 |
||
548 |
lemma |
|
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 |
||
555 |
context |
|
556 |
fixes a b :: real |
|
557 |
assumes ab: "a > 0" "b > 0" |
|
558 |
begin |
|
559 |
||
560 |
lemma |
|
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 |
||
565 |
end |
|
566 |
||
567 |
real_limit "\<lambda>x. 1 / sin (1/x) ^ 2 + 1 / tan (1/x) ^ 2 - 2 * x ^ 2" |
|
568 |
||
569 |
real_limit "\<lambda>x. ((1 / x + 4) powr 1.5 + exp (1 / x) - 9) * x" |
|
570 |
||
571 |
lemma "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 |
||
575 |
lemma "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 |
||
579 |
lemma "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 |
||
583 |
lemma "(\<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 *) |
|
588 |
lemma "filterlim (\<lambda>x::real. (sin (tan x) - tan (sin x))) (at 0) (at 0)" |
|
589 |
by real_asymp |
|
590 |
||
591 |
(* SLOW *) |
|
592 |
lemma "(\<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 |
||
595 |
lemma "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 |
||
600 |
real_expansion "\<lambda>x. arctan (sin (1 / x))" |
|
601 |
||
602 |
real_expansion "\<lambda>x. ln (1 + 1 / x)" |
|
603 |
terms: 5 (strict) |
|
604 |
||
605 |
real_expansion "\<lambda>x. sqrt (x + 1) - sqrt (x - 1)" |
|
606 |
terms: 3 (strict) |
|
607 |
||
608 |
||
609 |
text \<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> |
|
613 |
real_limit "\<lambda>x. (tan (sin x) - sin (tan x)) / x ^ 7" limit: "at_right 0" |
|
614 |
||
615 |
(* SLOW *) |
|
616 |
real_expansion "\<lambda>x. sin (tan (1/x)) - tan (sin (1/x))" |
|
617 |
terms: 1 (strict) |
|
618 |
||
619 |
(* SLOW *) |
|
620 |
real_expansion "\<lambda>x. tan (1 / x)" |
|
621 |
terms: 6 |
|
622 |
||
623 |
real_expansion "\<lambda>x::real. arctan x" |
|
624 |
||
625 |
real_expansion "\<lambda>x. sin (tan (1/x))" |
|
626 |
||
627 |
real_expansion "\<lambda>x. (sin (-1 / x) ^ 2) powr sin (-1/x)" |
|
628 |
||
629 |
real_limit "\<lambda>x. exp (max (sin x) 1)" |
|
630 |
||
631 |
lemma "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 |
||
635 |
lemma "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 |
||
638 |
lemma "filterlim (\<lambda>i::real. i powr (-i/(i-1)) - i powr (-1/(i-1))) (at_right (-1)) at_top" |
|
639 |
by real_asymp |
|
640 |
||
641 |
lemma "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 |
||
645 |
end |
|
646 |
||
647 |
||
648 |
subsection \<open>Interval arithmetic tests\<close> |
|
649 |
||
650 |
lemma "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 |
||
655 |
lemma "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 |
||
693 |
lemma "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 |
||
699 |
lemma "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 |
||
708 |
lemma "(\<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 |
||
712 |
lemma |
|
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 |
||
716 |
lemma |
|
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 |
||
720 |
end |