src/HOL/Limits.thy
changeset 61524 f2e51e704a96
parent 61169 4de9ff3ea29a
child 61531 ab2e862263e7
     1.1 --- a/src/HOL/Limits.thy	Tue Oct 27 23:18:32 2015 +0100
     1.2 +++ b/src/HOL/Limits.thy	Thu Oct 29 15:40:52 2015 +0100
     1.3 @@ -1436,6 +1436,39 @@
     1.4    using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
     1.5    by auto
     1.6  
     1.7 +lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) ---> (0::'a::real_normed_field)) sequentially"
     1.8 +proof (subst lim_sequentially, intro allI impI exI)
     1.9 +  fix e :: real assume e: "e > 0"
    1.10 +  fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
    1.11 +  have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
    1.12 +  also note n
    1.13 +  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e 
    1.14 +    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
    1.15 +qed
    1.16 +
    1.17 +lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) ---> (0::'a::real_normed_field)) sequentially"
    1.18 +  using lim_1_over_n by (simp add: inverse_eq_divide)
    1.19 +
    1.20 +lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) ----> 1"
    1.21 +proof (rule Lim_transform_eventually)
    1.22 +  show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"
    1.23 +    using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: field_simps)
    1.24 +  have "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) ----> 1 + 0"
    1.25 +    by (intro tendsto_add tendsto_const lim_inverse_n)
    1.26 +  thus "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) ----> 1" by simp
    1.27 +qed
    1.28 +
    1.29 +lemma LIMSEQ_n_over_Suc_n: "(\<lambda>n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) ----> 1"
    1.30 +proof (rule Lim_transform_eventually)
    1.31 +  show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) = 
    1.32 +                        of_nat n / of_nat (Suc n)) sequentially"
    1.33 +    using eventually_gt_at_top[of "0::nat"] 
    1.34 +    by eventually_elim (simp add: field_simps del: of_nat_Suc)
    1.35 +  have "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) ----> inverse 1"
    1.36 +    by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all
    1.37 +  thus "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) ----> 1" by simp
    1.38 +qed
    1.39 +
    1.40  subsection \<open>Convergence on sequences\<close>
    1.41  
    1.42  lemma convergent_add: