# HG changeset patch # User huffman # Date 1243900796 25200 # Node ID e0c05b595d1f7863dba009ccfe98904b787faaf1 # Parent df6acdd9dd379eb65eb82224eb526ad455789063 limits of Pair using filters diff -r df6acdd9dd37 -r e0c05b595d1f src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Mon Jun 01 16:27:54 2009 -0700 +++ b/src/HOL/Library/Product_Vector.thy Mon Jun 01 16:59:56 2009 -0700 @@ -202,25 +202,40 @@ qed text {* - TODO: The next three proofs are nearly identical to each other. + TODO: The "tendsto" notion generalizes LIM and LIMSEQ. + But the Cauchy proof still requires a lot of duplication. Is there a good way to factor out the common parts? *} +lemma tendsto_Pair: + assumes "tendsto X a net" and "tendsto Y b net" + shows "tendsto (\i. (X i, Y i)) (a, b) net" +proof (rule tendstoI) + fix r :: real assume "0 < r" + then have "0 < r / sqrt 2" (is "0 < ?s") + by (simp add: divide_pos_pos) + have "eventually (\i. dist (X i) a < ?s) net" + using `tendsto X a net` `0 < ?s` by (rule tendstoD) + moreover + have "eventually (\i. dist (Y i) b < ?s) net" + using `tendsto Y b net` `0 < ?s` by (rule tendstoD) + ultimately + show "eventually (\i. dist (X i, Y i) (a, b) < r) net" + by (rule eventually_elim2) + (simp add: real_sqrt_sum_squares_less dist_Pair_Pair) +qed + lemma LIMSEQ_Pair: assumes "X ----> a" and "Y ----> b" shows "(\n. (X n, Y n)) ----> (a, b)" -proof (rule metric_LIMSEQ_I) - fix r :: real assume "0 < r" - then have "0 < r / sqrt 2" (is "0 < ?s") - by (simp add: divide_pos_pos) - obtain M where M: "\n\M. dist (X n) a < ?s" - using metric_LIMSEQ_D [OF `X ----> a` `0 < ?s`] .. - obtain N where N: "\n\N. dist (Y n) b < ?s" - using metric_LIMSEQ_D [OF `Y ----> b` `0 < ?s`] .. - have "\n\max M N. dist (X n, Y n) (a, b) < r" - using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair) - then show "\n0. \n\n0. dist (X n, Y n) (a, b) < r" .. -qed +using assms unfolding LIMSEQ_conv_tendsto +by (rule tendsto_Pair) + +lemma LIM_Pair: + assumes "f -- x --> a" and "g -- x --> b" + shows "(\x. (f x, g x)) -- x --> (a, b)" +using assms unfolding LIM_conv_tendsto +by (rule tendsto_Pair) lemma Cauchy_Pair: assumes "Cauchy X" and "Cauchy Y" @@ -238,26 +253,6 @@ then show "\n0. \m\n0. \n\n0. dist (X m, Y m) (X n, Y n) < r" .. qed -lemma LIM_Pair: - assumes "f -- x --> a" and "g -- x --> b" - shows "(\x. (f x, g x)) -- x --> (a, b)" -proof (rule metric_LIM_I) - fix r :: real assume "0 < r" - then have "0 < r / sqrt 2" (is "0 < ?e") - by (simp add: divide_pos_pos) - obtain s where s: "0 < s" - "\z. z \ x \ dist z x < s \ dist (f z) a < ?e" - using metric_LIM_D [OF `f -- x --> a` `0 < ?e`] by fast - obtain t where t: "0 < t" - "\z. z \ x \ dist z x < t \ dist (g z) b < ?e" - using metric_LIM_D [OF `g -- x --> b` `0 < ?e`] by fast - have "0 < min s t \ - (\z. z \ x \ dist z x < min s t \ dist (f z, g z) (a, b) < r)" - using s t by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair) - then show - "\s>0. \z. z \ x \ dist z x < s \ dist (f z, g z) (a, b) < r" .. -qed - lemma isCont_Pair [simp]: "\isCont f x; isCont g x\ \ isCont (\x. (f x, g x)) x" unfolding isCont_def by (rule LIM_Pair)