author | Andreas Lochbihler |
Wed, 08 Apr 2015 15:02:40 +0200 | |
changeset 59956 | e936c2828bec |
parent 59667 | 651ea265d568 |
permissions | -rw-r--r-- |
57025 | 1 |
theory NthRoot_Limits |
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
57025
diff
changeset
|
2 |
imports Complex_Main |
57025 | 3 |
begin |
4 |
||
5 |
lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1" |
|
6 |
proof - |
|
7 |
def x \<equiv> "\<lambda>n. root n n - 1" |
|
8 |
have "x ----> sqrt 0" |
|
9 |
proof (rule tendsto_sandwich[OF _ _ tendsto_const]) |
|
10 |
show "(\<lambda>x. sqrt (2 / x)) ----> sqrt 0" |
|
11 |
by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) |
|
12 |
(simp_all add: at_infinity_eq_at_top_bot) |
|
13 |
{ fix n :: nat assume "2 < n" |
|
14 |
have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2" |
|
15 |
using `2 < n` unfolding gbinomial_def binomial_gbinomial |
|
16 |
by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric]) |
|
17 |
also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)" |
|
18 |
by (simp add: x_def) |
|
19 |
also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)" |
|
20 |
using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) |
|
21 |
also have "\<dots> = (x n + 1) ^ n" |
|
22 |
by (simp add: binomial_ring) |
|
23 |
also have "\<dots> = n" |
|
24 |
using `2 < n` by (simp add: x_def) |
|
25 |
finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1" |
|
26 |
by simp |
|
27 |
then have "(x n)\<^sup>2 \<le> 2 / real n" |
|
28 |
using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps) |
|
29 |
from real_sqrt_le_mono[OF this] have "x n \<le> sqrt (2 / real n)" |
|
30 |
by simp } |
|
31 |
then show "eventually (\<lambda>n. x n \<le> sqrt (2 / real n)) sequentially" |
|
32 |
by (auto intro!: exI[of _ 3] simp: eventually_sequentially) |
|
33 |
show "eventually (\<lambda>n. sqrt 0 \<le> x n) sequentially" |
|
34 |
by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def) |
|
35 |
qed |
|
36 |
from tendsto_add[OF this tendsto_const[of 1]] show ?thesis |
|
37 |
by (simp add: x_def) |
|
38 |
qed |
|
39 |
||
40 |
lemma LIMSEQ_root_const: |
|
41 |
assumes "0 < c" |
|
42 |
shows "(\<lambda>n. root n c) ----> 1" |
|
43 |
proof - |
|
44 |
{ fix c :: real assume "1 \<le> c" |
|
45 |
def x \<equiv> "\<lambda>n. root n c - 1" |
|
46 |
have "x ----> 0" |
|
47 |
proof (rule tendsto_sandwich[OF _ _ tendsto_const]) |
|
48 |
show "(\<lambda>n. c / n) ----> 0" |
|
49 |
by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) |
|
50 |
(simp_all add: at_infinity_eq_at_top_bot) |
|
51 |
{ fix n :: nat assume "1 < n" |
|
52 |
have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1" |
|
53 |
using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric]) |
|
54 |
also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)" |
|
55 |
by (simp add: x_def) |
|
56 |
also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)" |
|
57 |
using `1 < n` `1 \<le> c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) |
|
58 |
also have "\<dots> = (x n + 1) ^ n" |
|
59 |
by (simp add: binomial_ring) |
|
60 |
also have "\<dots> = c" |
|
61 |
using `1 < n` `1 \<le> c` by (simp add: x_def) |
|
62 |
finally have "x n \<le> c / n" |
|
63 |
using `1 \<le> c` `1 < n` by (simp add: field_simps) } |
|
64 |
then show "eventually (\<lambda>n. x n \<le> c / n) sequentially" |
|
65 |
by (auto intro!: exI[of _ 3] simp: eventually_sequentially) |
|
66 |
show "eventually (\<lambda>n. 0 \<le> x n) sequentially" |
|
67 |
using `1 \<le> c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def) |
|
68 |
qed |
|
69 |
from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) ----> 1" |
|
70 |
by (simp add: x_def) } |
|
71 |
note ge_1 = this |
|
72 |
||
73 |
show ?thesis |
|
74 |
proof cases |
|
75 |
assume "1 \<le> c" with ge_1 show ?thesis by blast |
|
76 |
next |
|
77 |
assume "\<not> 1 \<le> c" |
|
78 |
with `0 < c` have "1 \<le> 1 / c" |
|
79 |
by simp |
|
80 |
then have "(\<lambda>n. 1 / root n (1 / c)) ----> 1 / 1" |
|
81 |
by (intro tendsto_divide tendsto_const ge_1 `1 \<le> 1 / c` one_neq_zero) |
|
82 |
then show ?thesis |
|
83 |
by (rule filterlim_cong[THEN iffD1, rotated 3]) |
|
84 |
(auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide) |
|
85 |
qed |
|
86 |
qed |
|
87 |
||
88 |
end |