--- a/src/HOL/Deriv.thy Tue Mar 26 12:20:58 2013 +0100
+++ b/src/HOL/Deriv.thy Tue Mar 26 12:20:58 2013 +0100
@@ -8,7 +8,7 @@
header{* Differentiation *}
theory Deriv
-imports Lim
+imports Limits
begin
text{*Standard Definitions*}
--- a/src/HOL/Library/Diagonal_Subsequence.thy Tue Mar 26 12:20:58 2013 +0100
+++ b/src/HOL/Library/Diagonal_Subsequence.thy Tue Mar 26 12:20:58 2013 +0100
@@ -3,7 +3,7 @@
header {* Sequence of Properties on Subsequences *}
theory Diagonal_Subsequence
-imports SEQ
+imports Complex_Main
begin
locale subseqs =
--- a/src/HOL/Lim.thy Tue Mar 26 12:20:58 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,225 +0,0 @@
-(* Title : Lim.thy
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
- Conversion to Isar and new proofs by Lawrence C Paulson, 2004
-*)
-
-header{* Limits and Continuity *}
-
-theory Lim
-imports SEQ
-begin
-
-subsection {* Limits of Functions *}
-
-lemma LIM_eq:
- fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
- shows "f -- a --> L =
- (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
-by (simp add: LIM_def dist_norm)
-
-lemma LIM_I:
- fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
- shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
- ==> f -- a --> L"
-by (simp add: LIM_eq)
-
-lemma LIM_D:
- fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
- shows "[| f -- a --> L; 0<r |]
- ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
-by (simp add: LIM_eq)
-
-lemma LIM_offset:
- fixes a :: "'a::real_normed_vector"
- shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
-apply (rule topological_tendstoI)
-apply (drule (2) topological_tendstoD)
-apply (simp only: eventually_at dist_norm)
-apply (clarify, rule_tac x=d in exI, safe)
-apply (drule_tac x="x + k" in spec)
-apply (simp add: algebra_simps)
-done
-
-lemma LIM_offset_zero:
- fixes a :: "'a::real_normed_vector"
- shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
-by (drule_tac k="a" in LIM_offset, simp add: add_commute)
-
-lemma LIM_offset_zero_cancel:
- fixes a :: "'a::real_normed_vector"
- shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
-by (drule_tac k="- a" in LIM_offset, simp)
-
-lemma LIM_zero:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
-unfolding tendsto_iff dist_norm by simp
-
-lemma LIM_zero_cancel:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
-unfolding tendsto_iff dist_norm by simp
-
-lemma LIM_zero_iff:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
-unfolding tendsto_iff dist_norm by simp
-
-lemma LIM_imp_LIM:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
- assumes f: "f -- a --> l"
- assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
- shows "g -- a --> m"
- by (rule metric_LIM_imp_LIM [OF f],
- simp add: dist_norm le)
-
-lemma LIM_equal2:
- fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
- assumes 1: "0 < R"
- assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
- shows "g -- a --> l \<Longrightarrow> f -- a --> l"
-by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
-
-lemma LIM_compose2:
- fixes a :: "'a::real_normed_vector"
- assumes f: "f -- a --> b"
- assumes g: "g -- b --> c"
- assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
- shows "(\<lambda>x. g (f x)) -- a --> c"
-by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
-
-lemma real_LIM_sandwich_zero:
- fixes f g :: "'a::topological_space \<Rightarrow> real"
- assumes f: "f -- a --> 0"
- assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
- assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
- shows "g -- a --> 0"
-proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
- fix x assume x: "x \<noteq> a"
- have "norm (g x - 0) = g x" by (simp add: 1 x)
- also have "g x \<le> f x" by (rule 2 [OF x])
- also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
- also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
- finally show "norm (g x - 0) \<le> norm (f x - 0)" .
-qed
-
-
-subsection {* Continuity *}
-
-lemma LIM_isCont_iff:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
- shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
-by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
-
-lemma isCont_iff:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
- shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
-by (simp add: isCont_def LIM_isCont_iff)
-
-lemma isCont_LIM_compose2:
- fixes a :: "'a::real_normed_vector"
- assumes f [unfolded isCont_def]: "isCont f a"
- assumes g: "g -- f a --> l"
- assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
- shows "(\<lambda>x. g (f x)) -- a --> l"
-by (rule LIM_compose2 [OF f g inj])
-
-
-lemma isCont_norm [simp]:
- fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
- shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
- by (fact continuous_norm)
-
-lemma isCont_rabs [simp]:
- fixes f :: "'a::t2_space \<Rightarrow> real"
- shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
- by (fact continuous_rabs)
-
-lemma isCont_add [simp]:
- fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
- shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
- by (fact continuous_add)
-
-lemma isCont_minus [simp]:
- fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
- shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
- by (fact continuous_minus)
-
-lemma isCont_diff [simp]:
- fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
- shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
- by (fact continuous_diff)
-
-lemma isCont_mult [simp]:
- fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
- shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
- by (fact continuous_mult)
-
-lemma (in bounded_linear) isCont:
- "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
- by (fact continuous)
-
-lemma (in bounded_bilinear) isCont:
- "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
- by (fact continuous)
-
-lemmas isCont_scaleR [simp] =
- bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
-
-lemmas isCont_of_real [simp] =
- bounded_linear.isCont [OF bounded_linear_of_real]
-
-lemma isCont_power [simp]:
- fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
- shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
- by (fact continuous_power)
-
-lemma isCont_setsum [simp]:
- fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
- shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
- by (auto intro: continuous_setsum)
-
-lemmas isCont_intros =
- isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
- isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
- isCont_of_real isCont_power isCont_sgn isCont_setsum
-
-subsection {* Uniform Continuity *}
-
-lemma (in bounded_linear) isUCont: "isUCont f"
-unfolding isUCont_def dist_norm
-proof (intro allI impI)
- fix r::real assume r: "0 < r"
- obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
- using pos_bounded by fast
- show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
- proof (rule exI, safe)
- from r K show "0 < r / K" by (rule divide_pos_pos)
- next
- fix x y :: 'a
- assume xy: "norm (x - y) < r / K"
- have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
- also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
- also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
- finally show "norm (f x - f y) < r" .
- qed
-qed
-
-lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
-by (rule isUCont [THEN isUCont_Cauchy])
-
-
-lemma LIM_less_bound:
- fixes f :: "real \<Rightarrow> real"
- assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
- shows "0 \<le> f x"
-proof (rule tendsto_le_const)
- show "(f ---> f x) (at_left x)"
- using `isCont f x` by (simp add: filterlim_at_split isCont_def)
- show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
- using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
-qed simp
-
-end
--- a/src/HOL/Limits.thy Tue Mar 26 12:20:58 2013 +0100
+++ b/src/HOL/Limits.thy Tue Mar 26 12:20:58 2013 +0100
@@ -1,13 +1,23 @@
-(* Title : Limits.thy
- Author : Brian Huffman
+(* Title: Limits.thy
+ Author: Brian Huffman
+ Author: Jacques D. Fleuriot, University of Cambridge
+ Author: Lawrence C Paulson
+ Author: Jeremy Avigad
+
*)
-header {* Filters and Limits *}
+header {* Limits on Real Vector Spaces *}
theory Limits
imports Real_Vector_Spaces
begin
+(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
+ Hence it was references as Limits.eventually_within, but now it is Basic_Topology.eventually_within *)
+lemmas eventually_within = eventually_within
+
+subsection {* Filter going to infinity norm *}
+
definition at_infinity :: "'a::real_normed_vector filter" where
"at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
@@ -1027,9 +1037,616 @@
qed simp
-(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
- Hence it was references as Limits.within, but now it is Basic_Topology.eventually_within *)
-lemmas eventually_within = eventually_within
+subsection {* Limits of Sequences *}
+
+lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
+ by simp
+
+lemma LIMSEQ_iff:
+ fixes L :: "'a::real_normed_vector"
+ shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
+unfolding LIMSEQ_def dist_norm ..
+
+lemma LIMSEQ_I:
+ fixes L :: "'a::real_normed_vector"
+ shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
+by (simp add: LIMSEQ_iff)
+
+lemma LIMSEQ_D:
+ fixes L :: "'a::real_normed_vector"
+ shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
+by (simp add: LIMSEQ_iff)
+
+lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
+ unfolding tendsto_def eventually_sequentially
+ by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
+
+lemma Bseq_inverse_lemma:
+ fixes x :: "'a::real_normed_div_algebra"
+ shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
+apply (subst nonzero_norm_inverse, clarsimp)
+apply (erule (1) le_imp_inverse_le)
+done
+
+lemma Bseq_inverse:
+ fixes a :: "'a::real_normed_div_algebra"
+ shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
+ by (rule Bfun_inverse)
+
+lemma LIMSEQ_diff_approach_zero:
+ fixes L :: "'a::real_normed_vector"
+ shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
+ by (drule (1) tendsto_add, simp)
+
+lemma LIMSEQ_diff_approach_zero2:
+ fixes L :: "'a::real_normed_vector"
+ shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
+ by (drule (1) tendsto_diff, simp)
+
+text{*An unbounded sequence's inverse tends to 0*}
+
+lemma LIMSEQ_inverse_zero:
+ "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
+ apply (rule filterlim_compose[OF tendsto_inverse_0])
+ apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
+ apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
+ done
+
+text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
+
+lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
+ by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
+ filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
+
+text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
+infinity is now easily proved*}
+
+lemma LIMSEQ_inverse_real_of_nat_add:
+ "(%n. r + inverse(real(Suc n))) ----> r"
+ using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
+
+lemma LIMSEQ_inverse_real_of_nat_add_minus:
+ "(%n. r + -inverse(real(Suc n))) ----> r"
+ using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
+ by auto
+
+lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
+ "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
+ using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
+ by auto
+
+subsection {* Convergence on sequences *}
+
+lemma convergent_add:
+ fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
+ assumes "convergent (\<lambda>n. X n)"
+ assumes "convergent (\<lambda>n. Y n)"
+ shows "convergent (\<lambda>n. X n + Y n)"
+ using assms unfolding convergent_def by (fast intro: tendsto_add)
+
+lemma convergent_setsum:
+ fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
+ assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
+ shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
+proof (cases "finite A")
+ case True from this and assms show ?thesis
+ by (induct A set: finite) (simp_all add: convergent_const convergent_add)
+qed (simp add: convergent_const)
+
+lemma (in bounded_linear) convergent:
+ assumes "convergent (\<lambda>n. X n)"
+ shows "convergent (\<lambda>n. f (X n))"
+ using assms unfolding convergent_def by (fast intro: tendsto)
+
+lemma (in bounded_bilinear) convergent:
+ assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
+ shows "convergent (\<lambda>n. X n ** Y n)"
+ using assms unfolding convergent_def by (fast intro: tendsto)
+
+lemma convergent_minus_iff:
+ fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+ shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
+apply (simp add: convergent_def)
+apply (auto dest: tendsto_minus)
+apply (drule tendsto_minus, auto)
+done
+
+subsection {* Bounded Monotonic Sequences *}
+
+subsubsection {* Bounded Sequences *}
+
+lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
+ by (intro BfunI) (auto simp: eventually_sequentially)
+
+lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
+ by (intro BfunI) (auto simp: eventually_sequentially)
+
+lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
+ unfolding Bfun_def eventually_sequentially
+proof safe
+ fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
+ then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
+ by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
+ (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
+qed auto
+
+lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+unfolding Bseq_def by auto
+
+lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
+by (simp add: Bseq_def)
+
+lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
+by (auto simp add: Bseq_def)
+
+lemma lemma_NBseq_def:
+ "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
+proof safe
+ fix K :: real
+ from reals_Archimedean2 obtain n :: nat where "K < real n" ..
+ then have "K \<le> real (Suc n)" by auto
+ moreover assume "\<forall>m. norm (X m) \<le> K"
+ ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
+ by (blast intro: order_trans)
+ then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
+qed (force simp add: real_of_nat_Suc)
+
+text{* alternative definition for Bseq *}
+lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
+apply (simp add: Bseq_def)
+apply (simp (no_asm) add: lemma_NBseq_def)
+done
+
+lemma lemma_NBseq_def2:
+ "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
+apply (subst lemma_NBseq_def, auto)
+apply (rule_tac x = "Suc N" in exI)
+apply (rule_tac [2] x = N in exI)
+apply (auto simp add: real_of_nat_Suc)
+ prefer 2 apply (blast intro: order_less_imp_le)
+apply (drule_tac x = n in spec, simp)
+done
+
+(* yet another definition for Bseq *)
+lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
+by (simp add: Bseq_def lemma_NBseq_def2)
+
+subsubsection{*A Few More Equivalence Theorems for Boundedness*}
+
+text{*alternative formulation for boundedness*}
+lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
+apply (unfold Bseq_def, safe)
+apply (rule_tac [2] x = "k + norm x" in exI)
+apply (rule_tac x = K in exI, simp)
+apply (rule exI [where x = 0], auto)
+apply (erule order_less_le_trans, simp)
+apply (drule_tac x=n in spec, fold diff_minus)
+apply (drule order_trans [OF norm_triangle_ineq2])
+apply simp
+done
+
+text{*alternative formulation for boundedness*}
+lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
+apply safe
+apply (simp add: Bseq_def, safe)
+apply (rule_tac x = "K + norm (X N)" in exI)
+apply auto
+apply (erule order_less_le_trans, simp)
+apply (rule_tac x = N in exI, safe)
+apply (drule_tac x = n in spec)
+apply (rule order_trans [OF norm_triangle_ineq], simp)
+apply (auto simp add: Bseq_iff2)
+done
+
+lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
+apply (simp add: Bseq_def)
+apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
+apply (drule_tac x = n in spec, arith)
+done
+
+subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
+
+lemma Bseq_isUb:
+ "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
+by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
+
+text{* Use completeness of reals (supremum property)
+ to show that any bounded sequence has a least upper bound*}
+
+lemma Bseq_isLub:
+ "!!(X::nat=>real). Bseq X ==>
+ \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
+by (blast intro: reals_complete Bseq_isUb)
+
+subsubsection{*A Bounded and Monotonic Sequence Converges*}
+
+(* TODO: delete *)
+(* FIXME: one use in NSA/HSEQ.thy *)
+lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
+ apply (rule_tac x="X m" in exI)
+ apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
+ unfolding eventually_sequentially
+ apply blast
+ done
+
+text {* A monotone sequence converges to its least upper bound. *}
+
+lemma isLub_mono_imp_LIMSEQ:
+ fixes X :: "nat \<Rightarrow> real"
+ assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
+ assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
+ shows "X ----> u"
+proof (rule LIMSEQ_I)
+ have 1: "\<forall>n. X n \<le> u"
+ using isLubD2 [OF u] by auto
+ have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
+ using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
+ hence 2: "\<forall>y<u. \<exists>n. y < X n"
+ by (metis not_le)
+ fix r :: real assume "0 < r"
+ hence "u - r < u" by simp
+ hence "\<exists>m. u - r < X m" using 2 by simp
+ then obtain m where "u - r < X m" ..
+ with X have "\<forall>n\<ge>m. u - r < X n"
+ by (fast intro: less_le_trans)
+ hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
+ thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
+ using 1 by (simp add: diff_less_eq add_commute)
+qed
+
+text{*A standard proof of the theorem for monotone increasing sequence*}
+
+lemma Bseq_mono_convergent:
+ "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
+ by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
+
+lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
+ by (simp add: Bseq_def)
+
+text{*Main monotonicity theorem*}
+
+lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
+ by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
+ Bseq_mono_convergent)
+
+lemma Cauchy_iff:
+ fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+ shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
+ unfolding Cauchy_def dist_norm ..
+
+lemma CauchyI:
+ fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+ 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"
+by (simp add: Cauchy_iff)
+
+lemma CauchyD:
+ fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+ shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
+by (simp add: Cauchy_iff)
+
+lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
+ apply (simp add: subset_eq)
+ apply (rule BseqI'[where K="max (norm a) (norm b)"])
+ apply (erule_tac x=n in allE)
+ apply auto
+ done
+
+lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> (B::real) \<Longrightarrow> Bseq X"
+ by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)
+
+lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
+ by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
+
+lemma incseq_convergent:
+ fixes X :: "nat \<Rightarrow> real"
+ assumes "incseq X" and "\<forall>i. X i \<le> B"
+ obtains L where "X ----> L" "\<forall>i. X i \<le> L"
+proof atomize_elim
+ from incseq_bounded[OF assms] `incseq X` Bseq_monoseq_convergent[of X]
+ obtain L where "X ----> L"
+ by (auto simp: convergent_def monoseq_def incseq_def)
+ with `incseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. X i \<le> L)"
+ by (auto intro!: exI[of _ L] incseq_le)
+qed
+
+lemma decseq_convergent:
+ fixes X :: "nat \<Rightarrow> real"
+ assumes "decseq X" and "\<forall>i. B \<le> X i"
+ obtains L where "X ----> L" "\<forall>i. L \<le> X i"
+proof atomize_elim
+ from decseq_bounded[OF assms] `decseq X` Bseq_monoseq_convergent[of X]
+ obtain L where "X ----> L"
+ by (auto simp: convergent_def monoseq_def decseq_def)
+ with `decseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. L \<le> X i)"
+ by (auto intro!: exI[of _ L] decseq_le)
+qed
+
+subsubsection {* Cauchy Sequences are Bounded *}
+
+text{*A Cauchy sequence is bounded -- this is the standard
+ proof mechanization rather than the nonstandard proof*}
+
+lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real)
+ ==> \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
+apply (clarify, drule spec, drule (1) mp)
+apply (simp only: norm_minus_commute)
+apply (drule order_le_less_trans [OF norm_triangle_ineq2])
+apply simp
+done
+
+class banach = real_normed_vector + complete_space
+
+instance real :: banach by default
+
+subsection {* Power Sequences *}
+
+text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
+"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and
+ also fact that bounded and monotonic sequence converges.*}
+
+lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
+apply (simp add: Bseq_def)
+apply (rule_tac x = 1 in exI)
+apply (simp add: power_abs)
+apply (auto dest: power_mono)
+done
+
+lemma monoseq_realpow: fixes x :: real shows "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
+apply (clarify intro!: mono_SucI2)
+apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
+done
+
+lemma convergent_realpow:
+ "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
+by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
+
+lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
+ by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp
+
+lemma LIMSEQ_realpow_zero:
+ "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
+proof cases
+ assume "0 \<le> x" and "x \<noteq> 0"
+ hence x0: "0 < x" by simp
+ assume x1: "x < 1"
+ from x0 x1 have "1 < inverse x"
+ by (rule one_less_inverse)
+ hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
+ by (rule LIMSEQ_inverse_realpow_zero)
+ thus ?thesis by (simp add: power_inverse)
+qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
+
+lemma LIMSEQ_power_zero:
+ fixes x :: "'a::{real_normed_algebra_1}"
+ shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
+apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
+apply (simp only: tendsto_Zfun_iff, erule Zfun_le)
+apply (simp add: power_abs norm_power_ineq)
+done
+
+lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
+ by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
+
+text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
+
+lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
+ by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
+
+lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
+ by (rule LIMSEQ_power_zero) simp
+
+
+subsection {* Limits of Functions *}
+
+lemma LIM_eq:
+ fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
+ shows "f -- a --> L =
+ (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
+by (simp add: LIM_def dist_norm)
+
+lemma LIM_I:
+ fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
+ shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
+ ==> f -- a --> L"
+by (simp add: LIM_eq)
+
+lemma LIM_D:
+ fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
+ shows "[| f -- a --> L; 0<r |]
+ ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
+by (simp add: LIM_eq)
+
+lemma LIM_offset:
+ fixes a :: "'a::real_normed_vector"
+ shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
+apply (rule topological_tendstoI)
+apply (drule (2) topological_tendstoD)
+apply (simp only: eventually_at dist_norm)
+apply (clarify, rule_tac x=d in exI, safe)
+apply (drule_tac x="x + k" in spec)
+apply (simp add: algebra_simps)
+done
+
+lemma LIM_offset_zero:
+ fixes a :: "'a::real_normed_vector"
+ shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
+by (drule_tac k="a" in LIM_offset, simp add: add_commute)
+
+lemma LIM_offset_zero_cancel:
+ fixes a :: "'a::real_normed_vector"
+ shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
+by (drule_tac k="- a" in LIM_offset, simp)
+
+lemma LIM_zero:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
+unfolding tendsto_iff dist_norm by simp
+
+lemma LIM_zero_cancel:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
+unfolding tendsto_iff dist_norm by simp
+
+lemma LIM_zero_iff:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
+unfolding tendsto_iff dist_norm by simp
+
+lemma LIM_imp_LIM:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
+ assumes f: "f -- a --> l"
+ assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
+ shows "g -- a --> m"
+ by (rule metric_LIM_imp_LIM [OF f],
+ simp add: dist_norm le)
+
+lemma LIM_equal2:
+ fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
+ assumes 1: "0 < R"
+ assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
+ shows "g -- a --> l \<Longrightarrow> f -- a --> l"
+by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
+
+lemma LIM_compose2:
+ fixes a :: "'a::real_normed_vector"
+ assumes f: "f -- a --> b"
+ assumes g: "g -- b --> c"
+ assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
+ shows "(\<lambda>x. g (f x)) -- a --> c"
+by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
+
+lemma real_LIM_sandwich_zero:
+ fixes f g :: "'a::topological_space \<Rightarrow> real"
+ assumes f: "f -- a --> 0"
+ assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
+ assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
+ shows "g -- a --> 0"
+proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
+ fix x assume x: "x \<noteq> a"
+ have "norm (g x - 0) = g x" by (simp add: 1 x)
+ also have "g x \<le> f x" by (rule 2 [OF x])
+ also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
+ also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
+ finally show "norm (g x - 0) \<le> norm (f x - 0)" .
+qed
+
+
+subsection {* Continuity *}
+
+lemma LIM_isCont_iff:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
+ shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
+by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
+
+lemma isCont_iff:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
+ shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
+by (simp add: isCont_def LIM_isCont_iff)
+
+lemma isCont_LIM_compose2:
+ fixes a :: "'a::real_normed_vector"
+ assumes f [unfolded isCont_def]: "isCont f a"
+ assumes g: "g -- f a --> l"
+ assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
+ shows "(\<lambda>x. g (f x)) -- a --> l"
+by (rule LIM_compose2 [OF f g inj])
+
+
+lemma isCont_norm [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
+ by (fact continuous_norm)
+
+lemma isCont_rabs [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> real"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
+ by (fact continuous_rabs)
+
+lemma isCont_add [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
+ by (fact continuous_add)
+
+lemma isCont_minus [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
+ by (fact continuous_minus)
+
+lemma isCont_diff [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
+ by (fact continuous_diff)
+
+lemma isCont_mult [simp]:
+ fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
+ shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
+ by (fact continuous_mult)
+
+lemma (in bounded_linear) isCont:
+ "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
+ by (fact continuous)
+
+lemma (in bounded_bilinear) isCont:
+ "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
+ by (fact continuous)
+
+lemmas isCont_scaleR [simp] =
+ bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
+
+lemmas isCont_of_real [simp] =
+ bounded_linear.isCont [OF bounded_linear_of_real]
+
+lemma isCont_power [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
+ by (fact continuous_power)
+
+lemma isCont_setsum [simp]:
+ fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
+ shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
+ by (auto intro: continuous_setsum)
+
+lemmas isCont_intros =
+ isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
+ isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
+ isCont_of_real isCont_power isCont_sgn isCont_setsum
+
+subsection {* Uniform Continuity *}
+
+lemma (in bounded_linear) isUCont: "isUCont f"
+unfolding isUCont_def dist_norm
+proof (intro allI impI)
+ fix r::real assume r: "0 < r"
+ obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
+ using pos_bounded by fast
+ show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
+ proof (rule exI, safe)
+ from r K show "0 < r / K" by (rule divide_pos_pos)
+ next
+ fix x y :: 'a
+ assume xy: "norm (x - y) < r / K"
+ have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
+ also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
+ also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
+ finally show "norm (f x - f y) < r" .
+ qed
+qed
+
+lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
+by (rule isUCont [THEN isUCont_Cauchy])
+
+
+lemma LIM_less_bound:
+ fixes f :: "real \<Rightarrow> real"
+ assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
+ shows "0 \<le> f x"
+proof (rule tendsto_le_const)
+ show "(f ---> f x) (at_left x)"
+ using `isCont f x` by (simp add: filterlim_at_split isCont_def)
+ show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
+ using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
+qed simp
end
--- a/src/HOL/SEQ.thy Tue Mar 26 12:20:58 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,415 +0,0 @@
-(* Title: HOL/SEQ.thy
- Author: Jacques D. Fleuriot, University of Cambridge
- Author: Lawrence C Paulson
- Author: Jeremy Avigad
- Author: Brian Huffman
-
-Convergence of sequences and series.
-*)
-
-header {* Sequences and Convergence *}
-
-theory SEQ
-imports Limits
-begin
-
-subsection {* Limits of Sequences *}
-
-lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
- by simp
-
-lemma LIMSEQ_iff:
- fixes L :: "'a::real_normed_vector"
- shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
-unfolding LIMSEQ_def dist_norm ..
-
-lemma LIMSEQ_I:
- fixes L :: "'a::real_normed_vector"
- shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
-by (simp add: LIMSEQ_iff)
-
-lemma LIMSEQ_D:
- fixes L :: "'a::real_normed_vector"
- shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
-by (simp add: LIMSEQ_iff)
-
-lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
- unfolding tendsto_def eventually_sequentially
- by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
-
-lemma Bseq_inverse_lemma:
- fixes x :: "'a::real_normed_div_algebra"
- shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
-apply (subst nonzero_norm_inverse, clarsimp)
-apply (erule (1) le_imp_inverse_le)
-done
-
-lemma Bseq_inverse:
- fixes a :: "'a::real_normed_div_algebra"
- shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
- by (rule Bfun_inverse)
-
-lemma LIMSEQ_diff_approach_zero:
- fixes L :: "'a::real_normed_vector"
- shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
- by (drule (1) tendsto_add, simp)
-
-lemma LIMSEQ_diff_approach_zero2:
- fixes L :: "'a::real_normed_vector"
- shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
- by (drule (1) tendsto_diff, simp)
-
-text{*An unbounded sequence's inverse tends to 0*}
-
-lemma LIMSEQ_inverse_zero:
- "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
- apply (rule filterlim_compose[OF tendsto_inverse_0])
- apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
- apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
- done
-
-text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
-
-lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
- by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
- filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
-
-text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
-infinity is now easily proved*}
-
-lemma LIMSEQ_inverse_real_of_nat_add:
- "(%n. r + inverse(real(Suc n))) ----> r"
- using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
-
-lemma LIMSEQ_inverse_real_of_nat_add_minus:
- "(%n. r + -inverse(real(Suc n))) ----> r"
- using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
- by auto
-
-lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
- "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
- using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
- by auto
-
-subsection {* Convergence *}
-
-lemma convergent_add:
- fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
- assumes "convergent (\<lambda>n. X n)"
- assumes "convergent (\<lambda>n. Y n)"
- shows "convergent (\<lambda>n. X n + Y n)"
- using assms unfolding convergent_def by (fast intro: tendsto_add)
-
-lemma convergent_setsum:
- fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
- assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
- shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
-proof (cases "finite A")
- case True from this and assms show ?thesis
- by (induct A set: finite) (simp_all add: convergent_const convergent_add)
-qed (simp add: convergent_const)
-
-lemma (in bounded_linear) convergent:
- assumes "convergent (\<lambda>n. X n)"
- shows "convergent (\<lambda>n. f (X n))"
- using assms unfolding convergent_def by (fast intro: tendsto)
-
-lemma (in bounded_bilinear) convergent:
- assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
- shows "convergent (\<lambda>n. X n ** Y n)"
- using assms unfolding convergent_def by (fast intro: tendsto)
-
-lemma convergent_minus_iff:
- fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
- shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
-apply (simp add: convergent_def)
-apply (auto dest: tendsto_minus)
-apply (drule tendsto_minus, auto)
-done
-
-
-subsection {* Bounded Monotonic Sequences *}
-
-subsubsection {* Bounded Sequences *}
-
-lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
- by (intro BfunI) (auto simp: eventually_sequentially)
-
-lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
- by (intro BfunI) (auto simp: eventually_sequentially)
-
-lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
- unfolding Bfun_def eventually_sequentially
-proof safe
- fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
- then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
- by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
- (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
-qed auto
-
-lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-unfolding Bseq_def by auto
-
-lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
-by (simp add: Bseq_def)
-
-lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
-by (auto simp add: Bseq_def)
-
-lemma lemma_NBseq_def:
- "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
-proof safe
- fix K :: real
- from reals_Archimedean2 obtain n :: nat where "K < real n" ..
- then have "K \<le> real (Suc n)" by auto
- moreover assume "\<forall>m. norm (X m) \<le> K"
- ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
- by (blast intro: order_trans)
- then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
-qed (force simp add: real_of_nat_Suc)
-
-text{* alternative definition for Bseq *}
-lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
-apply (simp add: Bseq_def)
-apply (simp (no_asm) add: lemma_NBseq_def)
-done
-
-lemma lemma_NBseq_def2:
- "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
-apply (subst lemma_NBseq_def, auto)
-apply (rule_tac x = "Suc N" in exI)
-apply (rule_tac [2] x = N in exI)
-apply (auto simp add: real_of_nat_Suc)
- prefer 2 apply (blast intro: order_less_imp_le)
-apply (drule_tac x = n in spec, simp)
-done
-
-(* yet another definition for Bseq *)
-lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
-by (simp add: Bseq_def lemma_NBseq_def2)
-
-subsubsection{*A Few More Equivalence Theorems for Boundedness*}
-
-text{*alternative formulation for boundedness*}
-lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
-apply (unfold Bseq_def, safe)
-apply (rule_tac [2] x = "k + norm x" in exI)
-apply (rule_tac x = K in exI, simp)
-apply (rule exI [where x = 0], auto)
-apply (erule order_less_le_trans, simp)
-apply (drule_tac x=n in spec, fold diff_minus)
-apply (drule order_trans [OF norm_triangle_ineq2])
-apply simp
-done
-
-text{*alternative formulation for boundedness*}
-lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
-apply safe
-apply (simp add: Bseq_def, safe)
-apply (rule_tac x = "K + norm (X N)" in exI)
-apply auto
-apply (erule order_less_le_trans, simp)
-apply (rule_tac x = N in exI, safe)
-apply (drule_tac x = n in spec)
-apply (rule order_trans [OF norm_triangle_ineq], simp)
-apply (auto simp add: Bseq_iff2)
-done
-
-lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
-apply (simp add: Bseq_def)
-apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
-apply (drule_tac x = n in spec, arith)
-done
-
-subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
-
-lemma Bseq_isUb:
- "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
-by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
-
-text{* Use completeness of reals (supremum property)
- to show that any bounded sequence has a least upper bound*}
-
-lemma Bseq_isLub:
- "!!(X::nat=>real). Bseq X ==>
- \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
-by (blast intro: reals_complete Bseq_isUb)
-
-subsubsection{*A Bounded and Monotonic Sequence Converges*}
-
-(* TODO: delete *)
-(* FIXME: one use in NSA/HSEQ.thy *)
-lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
- apply (rule_tac x="X m" in exI)
- apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
- unfolding eventually_sequentially
- apply blast
- done
-
-text {* A monotone sequence converges to its least upper bound. *}
-
-lemma isLub_mono_imp_LIMSEQ:
- fixes X :: "nat \<Rightarrow> real"
- assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
- assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
- shows "X ----> u"
-proof (rule LIMSEQ_I)
- have 1: "\<forall>n. X n \<le> u"
- using isLubD2 [OF u] by auto
- have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
- using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
- hence 2: "\<forall>y<u. \<exists>n. y < X n"
- by (metis not_le)
- fix r :: real assume "0 < r"
- hence "u - r < u" by simp
- hence "\<exists>m. u - r < X m" using 2 by simp
- then obtain m where "u - r < X m" ..
- with X have "\<forall>n\<ge>m. u - r < X n"
- by (fast intro: less_le_trans)
- hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
- thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
- using 1 by (simp add: diff_less_eq add_commute)
-qed
-
-text{*A standard proof of the theorem for monotone increasing sequence*}
-
-lemma Bseq_mono_convergent:
- "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
- by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
-
-lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
- by (simp add: Bseq_def)
-
-text{*Main monotonicity theorem*}
-
-lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
- by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
- Bseq_mono_convergent)
-
-lemma Cauchy_iff:
- fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
- shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
- unfolding Cauchy_def dist_norm ..
-
-lemma CauchyI:
- fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
- 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"
-by (simp add: Cauchy_iff)
-
-lemma CauchyD:
- fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
- shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
-by (simp add: Cauchy_iff)
-
-lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
- apply (simp add: subset_eq)
- apply (rule BseqI'[where K="max (norm a) (norm b)"])
- apply (erule_tac x=n in allE)
- apply auto
- done
-
-lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> (B::real) \<Longrightarrow> Bseq X"
- by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)
-
-lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
- by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
-
-lemma incseq_convergent:
- fixes X :: "nat \<Rightarrow> real"
- assumes "incseq X" and "\<forall>i. X i \<le> B"
- obtains L where "X ----> L" "\<forall>i. X i \<le> L"
-proof atomize_elim
- from incseq_bounded[OF assms] `incseq X` Bseq_monoseq_convergent[of X]
- obtain L where "X ----> L"
- by (auto simp: convergent_def monoseq_def incseq_def)
- with `incseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. X i \<le> L)"
- by (auto intro!: exI[of _ L] incseq_le)
-qed
-
-lemma decseq_convergent:
- fixes X :: "nat \<Rightarrow> real"
- assumes "decseq X" and "\<forall>i. B \<le> X i"
- obtains L where "X ----> L" "\<forall>i. L \<le> X i"
-proof atomize_elim
- from decseq_bounded[OF assms] `decseq X` Bseq_monoseq_convergent[of X]
- obtain L where "X ----> L"
- by (auto simp: convergent_def monoseq_def decseq_def)
- with `decseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. L \<le> X i)"
- by (auto intro!: exI[of _ L] decseq_le)
-qed
-
-subsubsection {* Cauchy Sequences are Bounded *}
-
-text{*A Cauchy sequence is bounded -- this is the standard
- proof mechanization rather than the nonstandard proof*}
-
-lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real)
- ==> \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
-apply (clarify, drule spec, drule (1) mp)
-apply (simp only: norm_minus_commute)
-apply (drule order_le_less_trans [OF norm_triangle_ineq2])
-apply simp
-done
-
-class banach = real_normed_vector + complete_space
-
-instance real :: banach by default
-
-subsection {* Power Sequences *}
-
-text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
-"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and
- also fact that bounded and monotonic sequence converges.*}
-
-lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
-apply (simp add: Bseq_def)
-apply (rule_tac x = 1 in exI)
-apply (simp add: power_abs)
-apply (auto dest: power_mono)
-done
-
-lemma monoseq_realpow: fixes x :: real shows "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
-apply (clarify intro!: mono_SucI2)
-apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
-done
-
-lemma convergent_realpow:
- "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
-by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
-
-lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
- by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp
-
-lemma LIMSEQ_realpow_zero:
- "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
-proof cases
- assume "0 \<le> x" and "x \<noteq> 0"
- hence x0: "0 < x" by simp
- assume x1: "x < 1"
- from x0 x1 have "1 < inverse x"
- by (rule one_less_inverse)
- hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
- by (rule LIMSEQ_inverse_realpow_zero)
- thus ?thesis by (simp add: power_inverse)
-qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
-
-lemma LIMSEQ_power_zero:
- fixes x :: "'a::{real_normed_algebra_1}"
- shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
-apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
-apply (simp only: tendsto_Zfun_iff, erule Zfun_le)
-apply (simp add: power_abs norm_power_ineq)
-done
-
-lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
- by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
-
-text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
-
-lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
- by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
-
-lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
- by (rule LIMSEQ_power_zero) simp
-
-end
--- a/src/HOL/Series.thy Tue Mar 26 12:20:58 2013 +0100
+++ b/src/HOL/Series.thy Tue Mar 26 12:20:58 2013 +0100
@@ -10,7 +10,7 @@
header{*Finite Summation and Infinite Series*}
theory Series
-imports SEQ Deriv
+imports Deriv
begin
definition