src/HOL/NthRoot.thy
changeset 60141 833adf7db7d8
parent 59741 5b762cd73a8e
child 60615 e5fa1d5d3952
     1.1 --- a/src/HOL/NthRoot.thy	Mon Apr 20 13:46:36 2015 +0100
     1.2 +++ b/src/HOL/NthRoot.thy	Tue Apr 21 17:19:00 2015 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  section {* Nth Roots of Real Numbers *}
     1.5  
     1.6  theory NthRoot
     1.7 -imports Deriv
     1.8 +imports Deriv Binomial
     1.9  begin
    1.10  
    1.11  lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"
    1.12 @@ -644,6 +644,90 @@
    1.13    apply auto 
    1.14    done
    1.15    
    1.16 +lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1"
    1.17 +proof -
    1.18 +  def x \<equiv> "\<lambda>n. root n n - 1"
    1.19 +  have "x ----> sqrt 0"
    1.20 +  proof (rule tendsto_sandwich[OF _ _ tendsto_const])
    1.21 +    show "(\<lambda>x. sqrt (2 / x)) ----> sqrt 0"
    1.22 +      by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
    1.23 +         (simp_all add: at_infinity_eq_at_top_bot)
    1.24 +    { fix n :: nat assume "2 < n"
    1.25 +      have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
    1.26 +        using `2 < n` unfolding gbinomial_def binomial_gbinomial
    1.27 +        by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric])
    1.28 +      also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
    1.29 +        by (simp add: x_def)
    1.30 +      also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    1.31 +        using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
    1.32 +      also have "\<dots> = (x n + 1) ^ n"
    1.33 +        by (simp add: binomial_ring)
    1.34 +      also have "\<dots> = n"
    1.35 +        using `2 < n` by (simp add: x_def)
    1.36 +      finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1"
    1.37 +        by simp
    1.38 +      then have "(x n)\<^sup>2 \<le> 2 / real n"
    1.39 +        using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps)
    1.40 +      from real_sqrt_le_mono[OF this] have "x n \<le> sqrt (2 / real n)"
    1.41 +        by simp }
    1.42 +    then show "eventually (\<lambda>n. x n \<le> sqrt (2 / real n)) sequentially"
    1.43 +      by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
    1.44 +    show "eventually (\<lambda>n. sqrt 0 \<le> x n) sequentially"
    1.45 +      by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
    1.46 +  qed
    1.47 +  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis
    1.48 +    by (simp add: x_def)
    1.49 +qed
    1.50 +
    1.51 +lemma LIMSEQ_root_const:
    1.52 +  assumes "0 < c"
    1.53 +  shows "(\<lambda>n. root n c) ----> 1"
    1.54 +proof -
    1.55 +  { fix c :: real assume "1 \<le> c"
    1.56 +    def x \<equiv> "\<lambda>n. root n c - 1"
    1.57 +    have "x ----> 0"
    1.58 +    proof (rule tendsto_sandwich[OF _ _ tendsto_const])
    1.59 +      show "(\<lambda>n. c / n) ----> 0"
    1.60 +        by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
    1.61 +           (simp_all add: at_infinity_eq_at_top_bot)
    1.62 +      { fix n :: nat assume "1 < n"
    1.63 +        have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
    1.64 +          using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric])
    1.65 +        also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
    1.66 +          by (simp add: x_def)
    1.67 +        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    1.68 +          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.69 +        also have "\<dots> = (x n + 1) ^ n"
    1.70 +          by (simp add: binomial_ring)
    1.71 +        also have "\<dots> = c"
    1.72 +          using `1 < n` `1 \<le> c` by (simp add: x_def)
    1.73 +        finally have "x n \<le> c / n"
    1.74 +          using `1 \<le> c` `1 < n` by (simp add: field_simps) }
    1.75 +      then show "eventually (\<lambda>n. x n \<le> c / n) sequentially"
    1.76 +        by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
    1.77 +      show "eventually (\<lambda>n. 0 \<le> x n) sequentially"
    1.78 +        using `1 \<le> c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
    1.79 +    qed
    1.80 +    from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) ----> 1"
    1.81 +      by (simp add: x_def) }
    1.82 +  note ge_1 = this
    1.83 +
    1.84 +  show ?thesis
    1.85 +  proof cases
    1.86 +    assume "1 \<le> c" with ge_1 show ?thesis by blast
    1.87 +  next
    1.88 +    assume "\<not> 1 \<le> c"
    1.89 +    with `0 < c` have "1 \<le> 1 / c"
    1.90 +      by simp
    1.91 +    then have "(\<lambda>n. 1 / root n (1 / c)) ----> 1 / 1"
    1.92 +      by (intro tendsto_divide tendsto_const ge_1 `1 \<le> 1 / c` one_neq_zero)
    1.93 +    then show ?thesis
    1.94 +      by (rule filterlim_cong[THEN iffD1, rotated 3])
    1.95 +         (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide)
    1.96 +  qed
    1.97 +qed
    1.98 +
    1.99 +
   1.100  text "Legacy theorem names:"
   1.101  lemmas real_root_pos2 = real_root_power_cancel
   1.102  lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]