src/HOL/SEQ.thy
author hoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51474 1e9e68247ad1
parent 51472 adb441e4b9e9
child 51477 2990382dc066
permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
     1 (*  Title:      HOL/SEQ.thy
     2     Author:     Jacques D. Fleuriot, University of Cambridge
     3     Author:     Lawrence C Paulson
     4     Author:     Jeremy Avigad
     5     Author:     Brian Huffman
     6 
     7 Convergence of sequences and series.
     8 *)
     9 
    10 header {* Sequences and Convergence *}
    11 
    12 theory SEQ
    13 imports Limits
    14 begin
    15 
    16 subsection {* Limits of Sequences *}
    17 
    18 lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
    19   by simp
    20 
    21 lemma LIMSEQ_iff:
    22   fixes L :: "'a::real_normed_vector"
    23   shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
    24 unfolding LIMSEQ_def dist_norm ..
    25 
    26 lemma LIMSEQ_I:
    27   fixes L :: "'a::real_normed_vector"
    28   shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
    29 by (simp add: LIMSEQ_iff)
    30 
    31 lemma LIMSEQ_D:
    32   fixes L :: "'a::real_normed_vector"
    33   shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
    34 by (simp add: LIMSEQ_iff)
    35 
    36 lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
    37   unfolding tendsto_def eventually_sequentially
    38   by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
    39 
    40 lemma Bseq_inverse_lemma:
    41   fixes x :: "'a::real_normed_div_algebra"
    42   shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
    43 apply (subst nonzero_norm_inverse, clarsimp)
    44 apply (erule (1) le_imp_inverse_le)
    45 done
    46 
    47 lemma Bseq_inverse:
    48   fixes a :: "'a::real_normed_div_algebra"
    49   shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
    50   by (rule Bfun_inverse)
    51 
    52 lemma LIMSEQ_diff_approach_zero:
    53   fixes L :: "'a::real_normed_vector"
    54   shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
    55   by (drule (1) tendsto_add, simp)
    56 
    57 lemma LIMSEQ_diff_approach_zero2:
    58   fixes L :: "'a::real_normed_vector"
    59   shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
    60   by (drule (1) tendsto_diff, simp)
    61 
    62 text{*An unbounded sequence's inverse tends to 0*}
    63 
    64 lemma LIMSEQ_inverse_zero:
    65   "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
    66   apply (rule filterlim_compose[OF tendsto_inverse_0])
    67   apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
    68   apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
    69   done
    70 
    71 text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
    72 
    73 lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
    74   by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
    75             filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
    76 
    77 text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
    78 infinity is now easily proved*}
    79 
    80 lemma LIMSEQ_inverse_real_of_nat_add:
    81      "(%n. r + inverse(real(Suc n))) ----> r"
    82   using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
    83 
    84 lemma LIMSEQ_inverse_real_of_nat_add_minus:
    85      "(%n. r + -inverse(real(Suc n))) ----> r"
    86   using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
    87   by auto
    88 
    89 lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
    90      "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
    91   using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
    92   by auto
    93 
    94 subsection {* Convergence *}
    95 
    96 lemma convergent_add:
    97   fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
    98   assumes "convergent (\<lambda>n. X n)"
    99   assumes "convergent (\<lambda>n. Y n)"
   100   shows "convergent (\<lambda>n. X n + Y n)"
   101   using assms unfolding convergent_def by (fast intro: tendsto_add)
   102 
   103 lemma convergent_setsum:
   104   fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
   105   assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
   106   shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
   107 proof (cases "finite A")
   108   case True from this and assms show ?thesis
   109     by (induct A set: finite) (simp_all add: convergent_const convergent_add)
   110 qed (simp add: convergent_const)
   111 
   112 lemma (in bounded_linear) convergent:
   113   assumes "convergent (\<lambda>n. X n)"
   114   shows "convergent (\<lambda>n. f (X n))"
   115   using assms unfolding convergent_def by (fast intro: tendsto)
   116 
   117 lemma (in bounded_bilinear) convergent:
   118   assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
   119   shows "convergent (\<lambda>n. X n ** Y n)"
   120   using assms unfolding convergent_def by (fast intro: tendsto)
   121 
   122 lemma convergent_minus_iff:
   123   fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   124   shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
   125 apply (simp add: convergent_def)
   126 apply (auto dest: tendsto_minus)
   127 apply (drule tendsto_minus, auto)
   128 done
   129 
   130 
   131 subsection {* Bounded Monotonic Sequences *}
   132 
   133 subsubsection {* Bounded Sequences *}
   134 
   135 lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
   136   by (intro BfunI) (auto simp: eventually_sequentially)
   137 
   138 lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
   139   by (intro BfunI) (auto simp: eventually_sequentially)
   140 
   141 lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
   142   unfolding Bfun_def eventually_sequentially
   143 proof safe
   144   fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
   145   then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
   146     by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
   147        (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
   148 qed auto
   149 
   150 lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   151 unfolding Bseq_def by auto
   152 
   153 lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
   154 by (simp add: Bseq_def)
   155 
   156 lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
   157 by (auto simp add: Bseq_def)
   158 
   159 lemma lemma_NBseq_def:
   160   "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   161 proof safe
   162   fix K :: real
   163   from reals_Archimedean2 obtain n :: nat where "K < real n" ..
   164   then have "K \<le> real (Suc n)" by auto
   165   moreover assume "\<forall>m. norm (X m) \<le> K"
   166   ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
   167     by (blast intro: order_trans)
   168   then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
   169 qed (force simp add: real_of_nat_Suc)
   170 
   171 text{* alternative definition for Bseq *}
   172 lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   173 apply (simp add: Bseq_def)
   174 apply (simp (no_asm) add: lemma_NBseq_def)
   175 done
   176 
   177 lemma lemma_NBseq_def2:
   178      "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   179 apply (subst lemma_NBseq_def, auto)
   180 apply (rule_tac x = "Suc N" in exI)
   181 apply (rule_tac [2] x = N in exI)
   182 apply (auto simp add: real_of_nat_Suc)
   183  prefer 2 apply (blast intro: order_less_imp_le)
   184 apply (drule_tac x = n in spec, simp)
   185 done
   186 
   187 (* yet another definition for Bseq *)
   188 lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   189 by (simp add: Bseq_def lemma_NBseq_def2)
   190 
   191 subsubsection{*A Few More Equivalence Theorems for Boundedness*}
   192 
   193 text{*alternative formulation for boundedness*}
   194 lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
   195 apply (unfold Bseq_def, safe)
   196 apply (rule_tac [2] x = "k + norm x" in exI)
   197 apply (rule_tac x = K in exI, simp)
   198 apply (rule exI [where x = 0], auto)
   199 apply (erule order_less_le_trans, simp)
   200 apply (drule_tac x=n in spec, fold diff_minus)
   201 apply (drule order_trans [OF norm_triangle_ineq2])
   202 apply simp
   203 done
   204 
   205 text{*alternative formulation for boundedness*}
   206 lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
   207 apply safe
   208 apply (simp add: Bseq_def, safe)
   209 apply (rule_tac x = "K + norm (X N)" in exI)
   210 apply auto
   211 apply (erule order_less_le_trans, simp)
   212 apply (rule_tac x = N in exI, safe)
   213 apply (drule_tac x = n in spec)
   214 apply (rule order_trans [OF norm_triangle_ineq], simp)
   215 apply (auto simp add: Bseq_iff2)
   216 done
   217 
   218 lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
   219 apply (simp add: Bseq_def)
   220 apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
   221 apply (drule_tac x = n in spec, arith)
   222 done
   223 
   224 subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
   225 
   226 lemma Bseq_isUb:
   227   "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
   228 by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
   229 
   230 text{* Use completeness of reals (supremum property)
   231    to show that any bounded sequence has a least upper bound*}
   232 
   233 lemma Bseq_isLub:
   234   "!!(X::nat=>real). Bseq X ==>
   235    \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
   236 by (blast intro: reals_complete Bseq_isUb)
   237 
   238 subsubsection{*A Bounded and Monotonic Sequence Converges*}
   239 
   240 (* TODO: delete *)
   241 (* FIXME: one use in NSA/HSEQ.thy *)
   242 lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
   243   apply (rule_tac x="X m" in exI)
   244   apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
   245   unfolding eventually_sequentially
   246   apply blast
   247   done
   248 
   249 text {* A monotone sequence converges to its least upper bound. *}
   250 
   251 lemma isLub_mono_imp_LIMSEQ:
   252   fixes X :: "nat \<Rightarrow> real"
   253   assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
   254   assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
   255   shows "X ----> u"
   256 proof (rule LIMSEQ_I)
   257   have 1: "\<forall>n. X n \<le> u"
   258     using isLubD2 [OF u] by auto
   259   have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
   260     using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
   261   hence 2: "\<forall>y<u. \<exists>n. y < X n"
   262     by (metis not_le)
   263   fix r :: real assume "0 < r"
   264   hence "u - r < u" by simp
   265   hence "\<exists>m. u - r < X m" using 2 by simp
   266   then obtain m where "u - r < X m" ..
   267   with X have "\<forall>n\<ge>m. u - r < X n"
   268     by (fast intro: less_le_trans)
   269   hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
   270   thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
   271     using 1 by (simp add: diff_less_eq add_commute)
   272 qed
   273 
   274 text{*A standard proof of the theorem for monotone increasing sequence*}
   275 
   276 lemma Bseq_mono_convergent:
   277    "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
   278   by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
   279 
   280 lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
   281   by (simp add: Bseq_def)
   282 
   283 text{*Main monotonicity theorem*}
   284 
   285 lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
   286   by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
   287             Bseq_mono_convergent)
   288 
   289 lemma Cauchy_iff:
   290   fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   291   shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
   292   unfolding Cauchy_def dist_norm ..
   293 
   294 lemma CauchyI:
   295   fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   296   shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
   297 by (simp add: Cauchy_iff)
   298 
   299 lemma CauchyD:
   300   fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   301   shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
   302 by (simp add: Cauchy_iff)
   303 
   304 subsubsection {* Cauchy Sequences are Bounded *}
   305 
   306 text{*A Cauchy sequence is bounded -- this is the standard
   307   proof mechanization rather than the nonstandard proof*}
   308 
   309 lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real)
   310           ==>  \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
   311 apply (clarify, drule spec, drule (1) mp)
   312 apply (simp only: norm_minus_commute)
   313 apply (drule order_le_less_trans [OF norm_triangle_ineq2])
   314 apply simp
   315 done
   316 
   317 class banach = real_normed_vector + complete_space
   318 
   319 instance real :: banach by default
   320 
   321 subsection {* Power Sequences *}
   322 
   323 text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
   324 "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
   325   also fact that bounded and monotonic sequence converges.*}
   326 
   327 lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
   328 apply (simp add: Bseq_def)
   329 apply (rule_tac x = 1 in exI)
   330 apply (simp add: power_abs)
   331 apply (auto dest: power_mono)
   332 done
   333 
   334 lemma monoseq_realpow: fixes x :: real shows "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
   335 apply (clarify intro!: mono_SucI2)
   336 apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
   337 done
   338 
   339 lemma convergent_realpow:
   340   "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
   341 by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
   342 
   343 lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
   344   by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp
   345 
   346 lemma LIMSEQ_realpow_zero:
   347   "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
   348 proof cases
   349   assume "0 \<le> x" and "x \<noteq> 0"
   350   hence x0: "0 < x" by simp
   351   assume x1: "x < 1"
   352   from x0 x1 have "1 < inverse x"
   353     by (rule one_less_inverse)
   354   hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
   355     by (rule LIMSEQ_inverse_realpow_zero)
   356   thus ?thesis by (simp add: power_inverse)
   357 qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
   358 
   359 lemma LIMSEQ_power_zero:
   360   fixes x :: "'a::{real_normed_algebra_1}"
   361   shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
   362 apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
   363 apply (simp only: tendsto_Zfun_iff, erule Zfun_le)
   364 apply (simp add: power_abs norm_power_ineq)
   365 done
   366 
   367 lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
   368   by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
   369 
   370 text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
   371 
   372 lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
   373   by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
   374 
   375 lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
   376   by (rule LIMSEQ_power_zero) simp
   377 
   378 end