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