limits of Pair using filters
authorhuffman
Mon Jun 01 16:59:56 2009 -0700 (2009-06-01)
changeset 31388e0c05b595d1f
parent 31357 df6acdd9dd37
child 31389 3affcbc60c6d
limits of Pair using filters
src/HOL/Library/Product_Vector.thy
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Mon Jun 01 16:27:54 2009 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Mon Jun 01 16:59:56 2009 -0700
     1.3 @@ -202,25 +202,40 @@
     1.4  qed
     1.5  
     1.6  text {*
     1.7 -  TODO: The next three proofs are nearly identical to each other.
     1.8 +  TODO: The "tendsto" notion generalizes LIM and LIMSEQ.
     1.9 +  But the Cauchy proof still requires a lot of duplication.
    1.10    Is there a good way to factor out the common parts?
    1.11  *}
    1.12  
    1.13 +lemma tendsto_Pair:
    1.14 +  assumes "tendsto X a net" and "tendsto Y b net"
    1.15 +  shows "tendsto (\<lambda>i. (X i, Y i)) (a, b) net"
    1.16 +proof (rule tendstoI)
    1.17 +  fix r :: real assume "0 < r"
    1.18 +  then have "0 < r / sqrt 2" (is "0 < ?s")
    1.19 +    by (simp add: divide_pos_pos)
    1.20 +  have "eventually (\<lambda>i. dist (X i) a < ?s) net"
    1.21 +    using `tendsto X a net` `0 < ?s` by (rule tendstoD)
    1.22 +  moreover
    1.23 +  have "eventually (\<lambda>i. dist (Y i) b < ?s) net"
    1.24 +    using `tendsto Y b net` `0 < ?s` by (rule tendstoD)
    1.25 +  ultimately
    1.26 +  show "eventually (\<lambda>i. dist (X i, Y i) (a, b) < r) net"
    1.27 +    by (rule eventually_elim2)
    1.28 +       (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
    1.29 +qed
    1.30 +
    1.31  lemma LIMSEQ_Pair:
    1.32    assumes "X ----> a" and "Y ----> b"
    1.33    shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
    1.34 -proof (rule metric_LIMSEQ_I)
    1.35 -  fix r :: real assume "0 < r"
    1.36 -  then have "0 < r / sqrt 2" (is "0 < ?s")
    1.37 -    by (simp add: divide_pos_pos)
    1.38 -  obtain M where M: "\<forall>n\<ge>M. dist (X n) a < ?s"
    1.39 -    using metric_LIMSEQ_D [OF `X ----> a` `0 < ?s`] ..
    1.40 -  obtain N where N: "\<forall>n\<ge>N. dist (Y n) b < ?s"
    1.41 -    using metric_LIMSEQ_D [OF `Y ----> b` `0 < ?s`] ..
    1.42 -  have "\<forall>n\<ge>max M N. dist (X n, Y n) (a, b) < r"
    1.43 -    using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
    1.44 -  then show "\<exists>n0. \<forall>n\<ge>n0. dist (X n, Y n) (a, b) < r" ..
    1.45 -qed
    1.46 +using assms unfolding LIMSEQ_conv_tendsto
    1.47 +by (rule tendsto_Pair)
    1.48 +
    1.49 +lemma LIM_Pair:
    1.50 +  assumes "f -- x --> a" and "g -- x --> b"
    1.51 +  shows "(\<lambda>x. (f x, g x)) -- x --> (a, b)"
    1.52 +using assms unfolding LIM_conv_tendsto
    1.53 +by (rule tendsto_Pair)
    1.54  
    1.55  lemma Cauchy_Pair:
    1.56    assumes "Cauchy X" and "Cauchy Y"
    1.57 @@ -238,26 +253,6 @@
    1.58    then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
    1.59  qed
    1.60  
    1.61 -lemma LIM_Pair:
    1.62 -  assumes "f -- x --> a" and "g -- x --> b"
    1.63 -  shows "(\<lambda>x. (f x, g x)) -- x --> (a, b)"
    1.64 -proof (rule metric_LIM_I)
    1.65 -  fix r :: real assume "0 < r"
    1.66 -  then have "0 < r / sqrt 2" (is "0 < ?e")
    1.67 -    by (simp add: divide_pos_pos)
    1.68 -  obtain s where s: "0 < s"
    1.69 -    "\<forall>z. z \<noteq> x \<and> dist z x < s \<longrightarrow> dist (f z) a < ?e"
    1.70 -    using metric_LIM_D [OF `f -- x --> a` `0 < ?e`] by fast
    1.71 -  obtain t where t: "0 < t"
    1.72 -    "\<forall>z. z \<noteq> x \<and> dist z x < t \<longrightarrow> dist (g z) b < ?e"
    1.73 -    using metric_LIM_D [OF `g -- x --> b` `0 < ?e`] by fast
    1.74 -  have "0 < min s t \<and>
    1.75 -    (\<forall>z. z \<noteq> x \<and> dist z x < min s t \<longrightarrow> dist (f z, g z) (a, b) < r)"
    1.76 -    using s t by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
    1.77 -  then show
    1.78 -    "\<exists>s>0. \<forall>z. z \<noteq> x \<and> dist z x < s \<longrightarrow> dist (f z, g z) (a, b) < r" ..
    1.79 -qed
    1.80 -
    1.81  lemma isCont_Pair [simp]:
    1.82    "\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
    1.83    unfolding isCont_def by (rule LIM_Pair)