# HG changeset patch # User hoelzl # Date 1364296858 -3600 # Node ID 155263089e7b32975f72dbdb3604b58c2f2d214a # Parent d3d170a2887ff2a9344e797d074f6e5d25da840a move SEQ.thy and Lim.thy to Limits.thy diff -r d3d170a2887f -r 155263089e7b src/HOL/Deriv.thy --- 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*} diff -r d3d170a2887f -r 155263089e7b src/HOL/Library/Diagonal_Subsequence.thy --- 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 = diff -r d3d170a2887f -r 155263089e7b src/HOL/Lim.thy --- 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 = - (\r>0.\s>0.\x. x \ 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 \s>0.\x. x \ 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 \s>0.\x. x \ 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 \ (\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 \ (\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 "(\h. f (a + h)) -- 0 --> L \ f -- a --> L" -by (drule_tac k="- a" in LIM_offset, simp) - -lemma LIM_zero: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "(f ---> l) F \ ((\x. f x - l) ---> 0) F" -unfolding tendsto_iff dist_norm by simp - -lemma LIM_zero_cancel: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "((\x. f x - l) ---> 0) F \ (f ---> l) F" -unfolding tendsto_iff dist_norm by simp - -lemma LIM_zero_iff: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" - shows "((\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 \ 'b::real_normed_vector" - fixes g :: "'a::topological_space \ 'c::real_normed_vector" - assumes f: "f -- a --> l" - assumes le: "\x. x \ a \ norm (g x - m) \ 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 \ 'b::topological_space" - assumes 1: "0 < R" - assumes 2: "\x. \x \ a; norm (x - a) < R\ \ f x = g x" - shows "g -- a --> l \ 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: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ b" - shows "(\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 \ real" - assumes f: "f -- a --> 0" - assumes 1: "\x. x \ a \ 0 \ g x" - assumes 2: "\x. x \ a \ g x \ f x" - shows "g -- a --> 0" -proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *) - fix x assume x: "x \ a" - have "norm (g x - 0) = g x" by (simp add: 1 x) - also have "g x \ f x" by (rule 2 [OF x]) - also have "f x \ \f x\" by (rule abs_ge_self) - also have "\f x\ = norm (f x - 0)" by simp - finally show "norm (g x - 0) \ norm (f x - 0)" . -qed - - -subsection {* Continuity *} - -lemma LIM_isCont_iff: - fixes f :: "'a::real_normed_vector \ 'b::topological_space" - shows "(f -- a --> f a) = ((\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 \ 'b::topological_space" - shows "isCont f x = (\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: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ f a" - shows "(\x. g (f x)) -- a --> l" -by (rule LIM_compose2 [OF f g inj]) - - -lemma isCont_norm [simp]: - fixes f :: "'a::t2_space \ 'b::real_normed_vector" - shows "isCont f a \ isCont (\x. norm (f x)) a" - by (fact continuous_norm) - -lemma isCont_rabs [simp]: - fixes f :: "'a::t2_space \ real" - shows "isCont f a \ isCont (\x. \f x\) a" - by (fact continuous_rabs) - -lemma isCont_add [simp]: - fixes f :: "'a::t2_space \ 'b::real_normed_vector" - shows "\isCont f a; isCont g a\ \ isCont (\x. f x + g x) a" - by (fact continuous_add) - -lemma isCont_minus [simp]: - fixes f :: "'a::t2_space \ 'b::real_normed_vector" - shows "isCont f a \ isCont (\x. - f x) a" - by (fact continuous_minus) - -lemma isCont_diff [simp]: - fixes f :: "'a::t2_space \ 'b::real_normed_vector" - shows "\isCont f a; isCont g a\ \ isCont (\x. f x - g x) a" - by (fact continuous_diff) - -lemma isCont_mult [simp]: - fixes f g :: "'a::t2_space \ 'b::real_normed_algebra" - shows "\isCont f a; isCont g a\ \ isCont (\x. f x * g x) a" - by (fact continuous_mult) - -lemma (in bounded_linear) isCont: - "isCont g a \ isCont (\x. f (g x)) a" - by (fact continuous) - -lemma (in bounded_bilinear) isCont: - "\isCont f a; isCont g a\ \ isCont (\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 \ 'b::{power,real_normed_algebra}" - shows "isCont f a \ isCont (\x. f x ^ n) a" - by (fact continuous_power) - -lemma isCont_setsum [simp]: - fixes f :: "'a \ 'b::t2_space \ 'c::real_normed_vector" - shows "\i\A. isCont (f i) a \ isCont (\x. \i\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: "\x. norm (f x) \ norm x * K" - using pos_bounded by fast - show "\s>0. \x y. norm (x - y) < s \ 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 "\ \ norm (x - y) * K" by (rule norm_le) - also from K xy have "\ < 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 \ Cauchy (\n. f (X n))" -by (rule isUCont [THEN isUCont_Cauchy]) - - -lemma LIM_less_bound: - fixes f :: "real \ real" - assumes ev: "b < x" "\ x' \ { b <..< x}. 0 \ f x'" and "isCont f x" - shows "0 \ 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 (\x. 0 \ f x) (at_left x)" - using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"]) -qed simp - -end diff -r d3d170a2887f -r 155263089e7b src/HOL/Limits.thy --- 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 (\P. \r. \x. r \ norm x \ 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) = (\r>0. \no. \n \ no. norm (X n - L) < r)" +unfolding LIMSEQ_def dist_norm .. + +lemma LIMSEQ_I: + fixes L :: "'a::real_normed_vector" + shows "(\r. 0 < r \ \no. \n\no. norm (X n - L) < r) \ X ----> L" +by (simp add: LIMSEQ_iff) + +lemma LIMSEQ_D: + fixes L :: "'a::real_normed_vector" + shows "\X ----> L; 0 < r\ \ \no. \n\no. norm (X n - L) < r" +by (simp add: LIMSEQ_iff) + +lemma LIMSEQ_linear: "\ X ----> x ; l > 0 \ \ (\ 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 "\r \ norm x; 0 < r\ \ norm (inverse x) \ 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 "\X ----> a; a \ 0\ \ Bseq (\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: + "\r::real. \N. \n\N. r < X n \ (\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 \ 'a::real_normed_vector" + assumes "convergent (\n. X n)" + assumes "convergent (\n. Y n)" + shows "convergent (\n. X n + Y n)" + using assms unfolding convergent_def by (fast intro: tendsto_add) + +lemma convergent_setsum: + fixes X :: "'a \ nat \ 'b::real_normed_vector" + assumes "\i. i \ A \ convergent (\n. X i n)" + shows "convergent (\n. \i\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 (\n. X n)" + shows "convergent (\n. f (X n))" + using assms unfolding convergent_def by (fast intro: tendsto) + +lemma (in bounded_bilinear) convergent: + assumes "convergent (\n. X n)" and "convergent (\n. Y n)" + shows "convergent (\n. X n ** Y n)" + using assms unfolding convergent_def by (fast intro: tendsto) + +lemma convergent_minus_iff: + fixes X :: "nat \ 'a::real_normed_vector" + shows "convergent X \ convergent (\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': "(\n. norm (X n) \ K) \ Bseq X" + by (intro BfunI) (auto simp: eventually_sequentially) + +lemma BseqI2': "\n\N. norm (X n) \ K \ Bseq X" + by (intro BfunI) (auto simp: eventually_sequentially) + +lemma Bseq_def: "Bseq X \ (\K>0. \n. norm (X n) \ K)" + unfolding Bfun_def eventually_sequentially +proof safe + fix N K assume "0 < K" "\n\N. norm (X n) \ K" + then show "\K>0. \n. norm (X n) \ 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: "\Bseq X; \K. \0 < K; \n. norm (X n) \ K\ \ Q\ \ Q" +unfolding Bseq_def by auto + +lemma BseqD: "Bseq X ==> \K. 0 < K & (\n. norm (X n) \ K)" +by (simp add: Bseq_def) + +lemma BseqI: "[| 0 < K; \n. norm (X n) \ K |] ==> Bseq X" +by (auto simp add: Bseq_def) + +lemma lemma_NBseq_def: + "(\K > 0. \n. norm (X n) \ K) = (\N. \n. norm (X n) \ real(Suc N))" +proof safe + fix K :: real + from reals_Archimedean2 obtain n :: nat where "K < real n" .. + then have "K \ real (Suc n)" by auto + moreover assume "\m. norm (X m) \ K" + ultimately have "\m. norm (X m) \ real (Suc n)" + by (blast intro: order_trans) + then show "\N. \n. norm (X n) \ real (Suc N)" .. +qed (force simp add: real_of_nat_Suc) + +text{* alternative definition for Bseq *} +lemma Bseq_iff: "Bseq X = (\N. \n. norm (X n) \ real(Suc N))" +apply (simp add: Bseq_def) +apply (simp (no_asm) add: lemma_NBseq_def) +done + +lemma lemma_NBseq_def2: + "(\K > 0. \n. norm (X n) \ K) = (\N. \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 = (\N. \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 = (\k > 0. \x. \n. norm (X(n) + -x) \ 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 = (\k > 0. \N. \n. norm(X(n) + -X(N)) \ 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: "(\n. k \ f n & f n \ (K::real)) ==> Bseq f" +apply (simp add: Bseq_def) +apply (rule_tac x = " (\k\ + \K\) + 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 ==> \U. isUb (UNIV::real set) {x. \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 ==> + \U. isLub (UNIV::real set) {x. \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: "\n. m \ n --> X n = X m ==> \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 \ real" + assumes u: "isLub UNIV {x. \n. X n = x} u" (* FIXME: use 'range X' *) + assumes X: "\m n. m \ n \ X m \ X n" + shows "X ----> u" +proof (rule LIMSEQ_I) + have 1: "\n. X n \ u" + using isLubD2 [OF u] by auto + have "\y. (\n. X n \ y) \ u \ y" + using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def) + hence 2: "\yn. y < X n" + by (metis not_le) + fix r :: real assume "0 < r" + hence "u - r < u" by simp + hence "\m. u - r < X m" using 2 by simp + then obtain m where "u - r < X m" .. + with X have "\n\m. u - r < X n" + by (fast intro: less_le_trans) + hence "\m. \n\m. u - r < X n" .. + thus "\m. \n\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 \ \m. \n \ m. X m \ X n \ 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 \ monoseq X \ convergent (X::nat\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 \ 'a::real_normed_vector" + shows "Cauchy X \ (\e>0. \M. \m\M. \n\M. norm (X m - X n) < e)" + unfolding Cauchy_def dist_norm .. + +lemma CauchyI: + fixes X :: "nat \ 'a::real_normed_vector" + shows "(\e. 0 < e \ \M. \m\M. \n\M. norm (X m - X n) < e) \ Cauchy X" +by (simp add: Cauchy_iff) + +lemma CauchyD: + fixes X :: "nat \ 'a::real_normed_vector" + shows "\Cauchy X; 0 < e\ \ \M. \m\M. \n\M. norm (X m - X n) < e" +by (simp add: Cauchy_iff) + +lemma Bseq_eq_bounded: "range f \ {a .. b::real} \ 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 \ \i. X i \ (B::real) \ Bseq X" + by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def) + +lemma decseq_bounded: "decseq X \ \i. (B::real) \ X i \ Bseq X" + by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def) + +lemma incseq_convergent: + fixes X :: "nat \ real" + assumes "incseq X" and "\i. X i \ B" + obtains L where "X ----> L" "\i. X i \ 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 "\L. X ----> L \ (\i. X i \ L)" + by (auto intro!: exI[of _ L] incseq_le) +qed + +lemma decseq_convergent: + fixes X :: "nat \ real" + assumes "decseq X" and "\i. B \ X i" + obtains L where "X ----> L" "\i. L \ 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 "\L. X ----> L \ (\i. L \ 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: "\n \ M. norm (X M - X n) < (1::real) + ==> \n \ 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\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 \ (x::real); x \ 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 \ x; x \ 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 \ (x::real); x \ 1 |] ==> convergent (%n. x ^ n)" +by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) + +lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \ (\n. inverse (x ^ n)) ----> 0" + by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp + +lemma LIMSEQ_realpow_zero: + "\0 \ (x::real); x < 1\ \ (\n. x ^ n) ----> 0" +proof cases + assume "0 \ x" and "x \ 0" + hence x0: "0 < x" by simp + assume x1: "x < 1" + from x0 x1 have "1 < inverse x" + by (rule one_less_inverse) + hence "(\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 \ (\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 \ (\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"\c\ < 1"}*} + +lemma LIMSEQ_rabs_realpow_zero: "\c\ < 1 \ (\n. \c\ ^ n :: real) ----> 0" + by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) + +lemma LIMSEQ_rabs_realpow_zero2: "\c\ < 1 \ (\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 = + (\r>0.\s>0.\x. x \ 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 \s>0.\x. x \ 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 \s>0.\x. x \ 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 \ (\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 \ (\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 "(\h. f (a + h)) -- 0 --> L \ f -- a --> L" +by (drule_tac k="- a" in LIM_offset, simp) + +lemma LIM_zero: + fixes f :: "'a::topological_space \ 'b::real_normed_vector" + shows "(f ---> l) F \ ((\x. f x - l) ---> 0) F" +unfolding tendsto_iff dist_norm by simp + +lemma LIM_zero_cancel: + fixes f :: "'a::topological_space \ 'b::real_normed_vector" + shows "((\x. f x - l) ---> 0) F \ (f ---> l) F" +unfolding tendsto_iff dist_norm by simp + +lemma LIM_zero_iff: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + shows "((\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 \ 'b::real_normed_vector" + fixes g :: "'a::topological_space \ 'c::real_normed_vector" + assumes f: "f -- a --> l" + assumes le: "\x. x \ a \ norm (g x - m) \ 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 \ 'b::topological_space" + assumes 1: "0 < R" + assumes 2: "\x. \x \ a; norm (x - a) < R\ \ f x = g x" + shows "g -- a --> l \ 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: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ b" + shows "(\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 \ real" + assumes f: "f -- a --> 0" + assumes 1: "\x. x \ a \ 0 \ g x" + assumes 2: "\x. x \ a \ g x \ f x" + shows "g -- a --> 0" +proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *) + fix x assume x: "x \ a" + have "norm (g x - 0) = g x" by (simp add: 1 x) + also have "g x \ f x" by (rule 2 [OF x]) + also have "f x \ \f x\" by (rule abs_ge_self) + also have "\f x\ = norm (f x - 0)" by simp + finally show "norm (g x - 0) \ norm (f x - 0)" . +qed + + +subsection {* Continuity *} + +lemma LIM_isCont_iff: + fixes f :: "'a::real_normed_vector \ 'b::topological_space" + shows "(f -- a --> f a) = ((\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 \ 'b::topological_space" + shows "isCont f x = (\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: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ f a" + shows "(\x. g (f x)) -- a --> l" +by (rule LIM_compose2 [OF f g inj]) + + +lemma isCont_norm [simp]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + shows "isCont f a \ isCont (\x. norm (f x)) a" + by (fact continuous_norm) + +lemma isCont_rabs [simp]: + fixes f :: "'a::t2_space \ real" + shows "isCont f a \ isCont (\x. \f x\) a" + by (fact continuous_rabs) + +lemma isCont_add [simp]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + shows "\isCont f a; isCont g a\ \ isCont (\x. f x + g x) a" + by (fact continuous_add) + +lemma isCont_minus [simp]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + shows "isCont f a \ isCont (\x. - f x) a" + by (fact continuous_minus) + +lemma isCont_diff [simp]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + shows "\isCont f a; isCont g a\ \ isCont (\x. f x - g x) a" + by (fact continuous_diff) + +lemma isCont_mult [simp]: + fixes f g :: "'a::t2_space \ 'b::real_normed_algebra" + shows "\isCont f a; isCont g a\ \ isCont (\x. f x * g x) a" + by (fact continuous_mult) + +lemma (in bounded_linear) isCont: + "isCont g a \ isCont (\x. f (g x)) a" + by (fact continuous) + +lemma (in bounded_bilinear) isCont: + "\isCont f a; isCont g a\ \ isCont (\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 \ 'b::{power,real_normed_algebra}" + shows "isCont f a \ isCont (\x. f x ^ n) a" + by (fact continuous_power) + +lemma isCont_setsum [simp]: + fixes f :: "'a \ 'b::t2_space \ 'c::real_normed_vector" + shows "\i\A. isCont (f i) a \ isCont (\x. \i\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: "\x. norm (f x) \ norm x * K" + using pos_bounded by fast + show "\s>0. \x y. norm (x - y) < s \ 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 "\ \ norm (x - y) * K" by (rule norm_le) + also from K xy have "\ < 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 \ Cauchy (\n. f (X n))" +by (rule isUCont [THEN isUCont_Cauchy]) + + +lemma LIM_less_bound: + fixes f :: "real \ real" + assumes ev: "b < x" "\ x' \ { b <..< x}. 0 \ f x'" and "isCont f x" + shows "0 \ 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 (\x. 0 \ f x) (at_left x)" + using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"]) +qed simp end diff -r d3d170a2887f -r 155263089e7b src/HOL/SEQ.thy --- 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) = (\r>0. \no. \n \ no. norm (X n - L) < r)" -unfolding LIMSEQ_def dist_norm .. - -lemma LIMSEQ_I: - fixes L :: "'a::real_normed_vector" - shows "(\r. 0 < r \ \no. \n\no. norm (X n - L) < r) \ X ----> L" -by (simp add: LIMSEQ_iff) - -lemma LIMSEQ_D: - fixes L :: "'a::real_normed_vector" - shows "\X ----> L; 0 < r\ \ \no. \n\no. norm (X n - L) < r" -by (simp add: LIMSEQ_iff) - -lemma LIMSEQ_linear: "\ X ----> x ; l > 0 \ \ (\ 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 "\r \ norm x; 0 < r\ \ norm (inverse x) \ 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 "\X ----> a; a \ 0\ \ Bseq (\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: - "\r::real. \N. \n\N. r < X n \ (\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 \ 'a::real_normed_vector" - assumes "convergent (\n. X n)" - assumes "convergent (\n. Y n)" - shows "convergent (\n. X n + Y n)" - using assms unfolding convergent_def by (fast intro: tendsto_add) - -lemma convergent_setsum: - fixes X :: "'a \ nat \ 'b::real_normed_vector" - assumes "\i. i \ A \ convergent (\n. X i n)" - shows "convergent (\n. \i\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 (\n. X n)" - shows "convergent (\n. f (X n))" - using assms unfolding convergent_def by (fast intro: tendsto) - -lemma (in bounded_bilinear) convergent: - assumes "convergent (\n. X n)" and "convergent (\n. Y n)" - shows "convergent (\n. X n ** Y n)" - using assms unfolding convergent_def by (fast intro: tendsto) - -lemma convergent_minus_iff: - fixes X :: "nat \ 'a::real_normed_vector" - shows "convergent X \ convergent (\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': "(\n. norm (X n) \ K) \ Bseq X" - by (intro BfunI) (auto simp: eventually_sequentially) - -lemma BseqI2': "\n\N. norm (X n) \ K \ Bseq X" - by (intro BfunI) (auto simp: eventually_sequentially) - -lemma Bseq_def: "Bseq X \ (\K>0. \n. norm (X n) \ K)" - unfolding Bfun_def eventually_sequentially -proof safe - fix N K assume "0 < K" "\n\N. norm (X n) \ K" - then show "\K>0. \n. norm (X n) \ 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: "\Bseq X; \K. \0 < K; \n. norm (X n) \ K\ \ Q\ \ Q" -unfolding Bseq_def by auto - -lemma BseqD: "Bseq X ==> \K. 0 < K & (\n. norm (X n) \ K)" -by (simp add: Bseq_def) - -lemma BseqI: "[| 0 < K; \n. norm (X n) \ K |] ==> Bseq X" -by (auto simp add: Bseq_def) - -lemma lemma_NBseq_def: - "(\K > 0. \n. norm (X n) \ K) = (\N. \n. norm (X n) \ real(Suc N))" -proof safe - fix K :: real - from reals_Archimedean2 obtain n :: nat where "K < real n" .. - then have "K \ real (Suc n)" by auto - moreover assume "\m. norm (X m) \ K" - ultimately have "\m. norm (X m) \ real (Suc n)" - by (blast intro: order_trans) - then show "\N. \n. norm (X n) \ real (Suc N)" .. -qed (force simp add: real_of_nat_Suc) - -text{* alternative definition for Bseq *} -lemma Bseq_iff: "Bseq X = (\N. \n. norm (X n) \ real(Suc N))" -apply (simp add: Bseq_def) -apply (simp (no_asm) add: lemma_NBseq_def) -done - -lemma lemma_NBseq_def2: - "(\K > 0. \n. norm (X n) \ K) = (\N. \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 = (\N. \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 = (\k > 0. \x. \n. norm (X(n) + -x) \ 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 = (\k > 0. \N. \n. norm(X(n) + -X(N)) \ 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: "(\n. k \ f n & f n \ (K::real)) ==> Bseq f" -apply (simp add: Bseq_def) -apply (rule_tac x = " (\k\ + \K\) + 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 ==> \U. isUb (UNIV::real set) {x. \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 ==> - \U. isLub (UNIV::real set) {x. \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: "\n. m \ n --> X n = X m ==> \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 \ real" - assumes u: "isLub UNIV {x. \n. X n = x} u" (* FIXME: use 'range X' *) - assumes X: "\m n. m \ n \ X m \ X n" - shows "X ----> u" -proof (rule LIMSEQ_I) - have 1: "\n. X n \ u" - using isLubD2 [OF u] by auto - have "\y. (\n. X n \ y) \ u \ y" - using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def) - hence 2: "\yn. y < X n" - by (metis not_le) - fix r :: real assume "0 < r" - hence "u - r < u" by simp - hence "\m. u - r < X m" using 2 by simp - then obtain m where "u - r < X m" .. - with X have "\n\m. u - r < X n" - by (fast intro: less_le_trans) - hence "\m. \n\m. u - r < X n" .. - thus "\m. \n\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 \ \m. \n \ m. X m \ X n \ 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 \ monoseq X \ convergent (X::nat\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 \ 'a::real_normed_vector" - shows "Cauchy X \ (\e>0. \M. \m\M. \n\M. norm (X m - X n) < e)" - unfolding Cauchy_def dist_norm .. - -lemma CauchyI: - fixes X :: "nat \ 'a::real_normed_vector" - shows "(\e. 0 < e \ \M. \m\M. \n\M. norm (X m - X n) < e) \ Cauchy X" -by (simp add: Cauchy_iff) - -lemma CauchyD: - fixes X :: "nat \ 'a::real_normed_vector" - shows "\Cauchy X; 0 < e\ \ \M. \m\M. \n\M. norm (X m - X n) < e" -by (simp add: Cauchy_iff) - -lemma Bseq_eq_bounded: "range f \ {a .. b::real} \ 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 \ \i. X i \ (B::real) \ Bseq X" - by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def) - -lemma decseq_bounded: "decseq X \ \i. (B::real) \ X i \ Bseq X" - by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def) - -lemma incseq_convergent: - fixes X :: "nat \ real" - assumes "incseq X" and "\i. X i \ B" - obtains L where "X ----> L" "\i. X i \ 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 "\L. X ----> L \ (\i. X i \ L)" - by (auto intro!: exI[of _ L] incseq_le) -qed - -lemma decseq_convergent: - fixes X :: "nat \ real" - assumes "decseq X" and "\i. B \ X i" - obtains L where "X ----> L" "\i. L \ 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 "\L. X ----> L \ (\i. L \ 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: "\n \ M. norm (X M - X n) < (1::real) - ==> \n \ 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\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 \ (x::real); x \ 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 \ x; x \ 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 \ (x::real); x \ 1 |] ==> convergent (%n. x ^ n)" -by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) - -lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \ (\n. inverse (x ^ n)) ----> 0" - by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp - -lemma LIMSEQ_realpow_zero: - "\0 \ (x::real); x < 1\ \ (\n. x ^ n) ----> 0" -proof cases - assume "0 \ x" and "x \ 0" - hence x0: "0 < x" by simp - assume x1: "x < 1" - from x0 x1 have "1 < inverse x" - by (rule one_less_inverse) - hence "(\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 \ (\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 \ (\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"\c\ < 1"}*} - -lemma LIMSEQ_rabs_realpow_zero: "\c\ < 1 \ (\n. \c\ ^ n :: real) ----> 0" - by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) - -lemma LIMSEQ_rabs_realpow_zero2: "\c\ < 1 \ (\n. c ^ n :: real) ----> 0" - by (rule LIMSEQ_power_zero) simp - -end diff -r d3d170a2887f -r 155263089e7b src/HOL/Series.thy --- 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