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