249 apply (rule ln_bound) |
249 apply (rule ln_bound) |
250 apply (erule ge_one_powr_ge_zero) |
250 apply (erule ge_one_powr_ge_zero) |
251 apply (erule order_less_imp_le) |
251 apply (erule order_less_imp_le) |
252 done |
252 done |
253 |
253 |
254 lemma ln_powr_bound2: "1 < x ==> 0 < a ==> (ln x) powr a <= (a powr a) * x" |
254 lemma ln_powr_bound2: |
|
255 assumes "1 < x" and "0 < a" |
|
256 shows "(ln x) powr a <= (a powr a) * x" |
255 proof - |
257 proof - |
256 assume "1 < x" and "0 < a" |
258 from assms have "ln x <= (x powr (1 / a)) / (1 / a)" |
257 then have "ln x <= (x powr (1 / a)) / (1 / a)" |
|
258 apply (intro ln_powr_bound) |
259 apply (intro ln_powr_bound) |
259 apply (erule order_less_imp_le) |
260 apply (erule order_less_imp_le) |
260 apply (rule divide_pos_pos) |
261 apply (rule divide_pos_pos) |
261 apply simp_all |
262 apply simp_all |
262 done |
263 done |
263 also have "... = a * (x powr (1 / a))" |
264 also have "... = a * (x powr (1 / a))" |
264 by simp |
265 by simp |
265 finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a" |
266 finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a" |
266 apply (intro powr_mono2) |
267 apply (intro powr_mono2) |
267 apply (rule order_less_imp_le, rule prems) |
268 apply (rule order_less_imp_le, rule assms) |
268 apply (rule ln_gt_zero) |
269 apply (rule ln_gt_zero) |
269 apply (rule prems) |
270 apply (rule assms) |
270 apply assumption |
271 apply assumption |
271 done |
272 done |
272 also have "... = (a powr a) * ((x powr (1 / a)) powr a)" |
273 also have "... = (a powr a) * ((x powr (1 / a)) powr a)" |
273 apply (rule powr_mult) |
274 apply (rule powr_mult) |
274 apply (rule prems) |
275 apply (rule assms) |
275 apply (rule powr_gt_zero) |
276 apply (rule powr_gt_zero) |
276 done |
277 done |
277 also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)" |
278 also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)" |
278 by (rule powr_powr) |
279 by (rule powr_powr) |
279 also have "... = x" |
280 also have "... = x" |
280 apply simp |
281 apply simp |
281 apply (subgoal_tac "a ~= 0") |
282 apply (subgoal_tac "a ~= 0") |
282 apply (insert prems, auto) |
283 using assms apply auto |
283 done |
284 done |
284 finally show ?thesis . |
285 finally show ?thesis . |
285 qed |
286 qed |
286 |
287 |
287 lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0" |
288 lemma LIMSEQ_neg_powr: |
|
289 assumes s: "0 < s" |
|
290 shows "(%x. (real x) powr - s) ----> 0" |
288 apply (unfold LIMSEQ_iff) |
291 apply (unfold LIMSEQ_iff) |
289 apply clarsimp |
292 apply clarsimp |
290 apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI) |
293 apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI) |
291 apply clarify |
294 apply clarify |
292 proof - |
295 proof - |
293 fix r fix n |
296 fix r fix n |
294 assume "0 < s" and "0 < r" and "natfloor (r powr (1 / - s)) + 1 <= n" |
297 assume r: "0 < r" and n: "natfloor (r powr (1 / - s)) + 1 <= n" |
295 have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1" |
298 have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1" |
296 by (rule real_natfloor_add_one_gt) |
299 by (rule real_natfloor_add_one_gt) |
297 also have "... = real(natfloor(r powr (1 / -s)) + 1)" |
300 also have "... = real(natfloor(r powr (1 / -s)) + 1)" |
298 by simp |
301 by simp |
299 also have "... <= real n" |
302 also have "... <= real n" |
300 apply (subst real_of_nat_le_iff) |
303 apply (subst real_of_nat_le_iff) |
301 apply (rule prems) |
304 apply (rule n) |
302 done |
305 done |
303 finally have "r powr (1 / - s) < real n". |
306 finally have "r powr (1 / - s) < real n". |
304 then have "real n powr (- s) < (r powr (1 / - s)) powr - s" |
307 then have "real n powr (- s) < (r powr (1 / - s)) powr - s" |
305 apply (intro powr_less_mono2_neg) |
308 apply (intro powr_less_mono2_neg) |
306 apply (auto simp add: prems) |
309 apply (auto simp add: s) |
307 done |
310 done |
308 also have "... = r" |
311 also have "... = r" |
309 by (simp add: powr_powr prems less_imp_neq [THEN not_sym]) |
312 by (simp add: powr_powr s r less_imp_neq [THEN not_sym]) |
310 finally show "real n powr - s < r" . |
313 finally show "real n powr - s < r" . |
311 qed |
314 qed |
312 |
315 |
313 end |
316 end |