src/HOL/Library/NthRoot_Limits.thy
 changeset 60141 833adf7db7d8 parent 60140 a948ee5fb5f4 child 60142 3275dddf356f child 60144 50eb4fdd5860
```     1.1 --- a/src/HOL/Library/NthRoot_Limits.thy	Mon Apr 20 13:46:36 2015 +0100
1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,88 +0,0 @@
1.4 -theory NthRoot_Limits
1.5 -  imports Complex_Main
1.6 -begin
1.7 -
1.8 -lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1"
1.9 -proof -
1.10 -  def x \<equiv> "\<lambda>n. root n n - 1"
1.11 -  have "x ----> sqrt 0"
1.12 -  proof (rule tendsto_sandwich[OF _ _ tendsto_const])
1.13 -    show "(\<lambda>x. sqrt (2 / x)) ----> sqrt 0"
1.14 -      by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
1.16 -    { fix n :: nat assume "2 < n"
1.17 -      have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
1.18 -        using `2 < n` unfolding gbinomial_def binomial_gbinomial
1.19 -        by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric])
1.20 -      also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
1.21 -        by (simp add: x_def)
1.22 -      also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
1.23 -        using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
1.24 -      also have "\<dots> = (x n + 1) ^ n"
1.25 -        by (simp add: binomial_ring)
1.26 -      also have "\<dots> = n"
1.27 -        using `2 < n` by (simp add: x_def)
1.28 -      finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1"
1.29 -        by simp
1.30 -      then have "(x n)\<^sup>2 \<le> 2 / real n"
1.31 -        using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps)
1.32 -      from real_sqrt_le_mono[OF this] have "x n \<le> sqrt (2 / real n)"
1.33 -        by simp }
1.34 -    then show "eventually (\<lambda>n. x n \<le> sqrt (2 / real n)) sequentially"
1.35 -      by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
1.36 -    show "eventually (\<lambda>n. sqrt 0 \<le> x n) sequentially"
1.37 -      by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
1.38 -  qed
1.39 -  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis
1.40 -    by (simp add: x_def)
1.41 -qed
1.42 -
1.43 -lemma LIMSEQ_root_const:
1.44 -  assumes "0 < c"
1.45 -  shows "(\<lambda>n. root n c) ----> 1"
1.46 -proof -
1.47 -  { fix c :: real assume "1 \<le> c"
1.48 -    def x \<equiv> "\<lambda>n. root n c - 1"
1.49 -    have "x ----> 0"
1.50 -    proof (rule tendsto_sandwich[OF _ _ tendsto_const])
1.51 -      show "(\<lambda>n. c / n) ----> 0"
1.52 -        by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
1.54 -      { fix n :: nat assume "1 < n"
1.55 -        have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
1.56 -          using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric])
1.57 -        also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
1.58 -          by (simp add: x_def)
1.59 -        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
1.60 -          using `1 < n` `1 \<le> c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
1.61 -        also have "\<dots> = (x n + 1) ^ n"
1.62 -          by (simp add: binomial_ring)
1.63 -        also have "\<dots> = c"
1.64 -          using `1 < n` `1 \<le> c` by (simp add: x_def)
1.65 -        finally have "x n \<le> c / n"
1.66 -          using `1 \<le> c` `1 < n` by (simp add: field_simps) }
1.67 -      then show "eventually (\<lambda>n. x n \<le> c / n) sequentially"
1.68 -        by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
1.69 -      show "eventually (\<lambda>n. 0 \<le> x n) sequentially"
1.70 -        using `1 \<le> c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
1.71 -    qed
1.72 -    from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) ----> 1"
1.73 -      by (simp add: x_def) }
1.74 -  note ge_1 = this
1.75 -
1.76 -  show ?thesis
1.77 -  proof cases
1.78 -    assume "1 \<le> c" with ge_1 show ?thesis by blast
1.79 -  next
1.80 -    assume "\<not> 1 \<le> c"
1.81 -    with `0 < c` have "1 \<le> 1 / c"
1.82 -      by simp
1.83 -    then have "(\<lambda>n. 1 / root n (1 / c)) ----> 1 / 1"
1.84 -      by (intro tendsto_divide tendsto_const ge_1 `1 \<le> 1 / c` one_neq_zero)
1.85 -    then show ?thesis
1.86 -      by (rule filterlim_cong[THEN iffD1, rotated 3])
1.87 -         (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide)
1.88 -  qed
1.89 -qed
1.90 -
1.91 -end
```