add lemma tendsto_Complex
authorhuffman
Tue May 11 07:58:48 2010 -0700 (2010-05-11)
changeset 36825d9320cdcde73
parent 36824 2e9a866141b8
child 36826 4d4462d644ae
add lemma tendsto_Complex
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Tue May 11 06:30:48 2010 -0700
     1.2 +++ b/src/HOL/Complex.thy	Tue May 11 07:58:48 2010 -0700
     1.3 @@ -353,16 +353,26 @@
     1.4  apply (simp add: complex_norm_def)
     1.5  done
     1.6  
     1.7 +lemma tendsto_Complex [tendsto_intros]:
     1.8 +  assumes "(f ---> a) net" and "(g ---> b) net"
     1.9 +  shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) net"
    1.10 +proof (rule tendstoI)
    1.11 +  fix r :: real assume "0 < r"
    1.12 +  hence "0 < r / sqrt 2" by (simp add: divide_pos_pos)
    1.13 +  have "eventually (\<lambda>x. dist (f x) a < r / sqrt 2) net"
    1.14 +    using `(f ---> a) net` and `0 < r / sqrt 2` by (rule tendstoD)
    1.15 +  moreover
    1.16 +  have "eventually (\<lambda>x. dist (g x) b < r / sqrt 2) net"
    1.17 +    using `(g ---> b) net` and `0 < r / sqrt 2` by (rule tendstoD)
    1.18 +  ultimately
    1.19 +  show "eventually (\<lambda>x. dist (Complex (f x) (g x)) (Complex a b) < r) net"
    1.20 +    by (rule eventually_elim2)
    1.21 +       (simp add: dist_norm real_sqrt_sum_squares_less)
    1.22 +qed
    1.23 +
    1.24  lemma LIMSEQ_Complex:
    1.25    "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
    1.26 -apply (rule LIMSEQ_I)
    1.27 -apply (subgoal_tac "0 < r / sqrt 2")
    1.28 -apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
    1.29 -apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
    1.30 -apply (rename_tac M N, rule_tac x="max M N" in exI, safe)
    1.31 -apply (simp add: real_sqrt_sum_squares_less)
    1.32 -apply (simp add: divide_pos_pos)
    1.33 -done
    1.34 +by (rule tendsto_Complex)
    1.35  
    1.36  instance complex :: banach
    1.37  proof