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