author huffman Mon Jun 01 16:59:56 2009 -0700 (2009-06-01) changeset 31388 e0c05b595d1f parent 31357 df6acdd9dd37 child 31389 3affcbc60c6d
limits of Pair using filters
```     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)
```