src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44907 93943da0a010
parent 44905 3e8cc9046731
child 44909 1f5d6eb73549
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 12 11:39:29 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 12 11:54:20 2011 -0700
     1.3 @@ -967,11 +967,6 @@
     1.4    "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)"
     1.5    by (auto simp add: tendsto_iff eventually_at_infinity)
     1.6  
     1.7 -lemma Lim_sequentially:
     1.8 - "(S ---> l) sequentially \<longleftrightarrow>
     1.9 -          (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
    1.10 -  by (rule LIMSEQ_def) (* FIXME: redundant *)
    1.11 -
    1.12  lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
    1.13    by (rule topological_tendstoI, auto elim: eventually_rev_mono)
    1.14  
    1.15 @@ -1104,7 +1099,7 @@
    1.16    ultimately show ?rhs by fast
    1.17  next
    1.18    assume ?rhs
    1.19 -  then obtain f::"nat\<Rightarrow>'a"  where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding Lim_sequentially by auto
    1.20 +  then obtain f::"nat\<Rightarrow>'a"  where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding LIMSEQ_def by auto
    1.21    { fix e::real assume "e>0"
    1.22      then obtain N where "dist (f N) x < e" using f(2) by auto
    1.23      moreover have "f N\<in>S" "f N \<noteq> x" using f(1) by auto
    1.24 @@ -1987,7 +1982,7 @@
    1.25    hence "\<forall>m n. m \<le> n \<longrightarrow> (s m) \<le> (s n)" by auto
    1.26    then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar> (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a]
    1.27      unfolding monoseq_def by auto
    1.28 -  thus ?thesis unfolding Lim_sequentially apply(rule_tac x="l" in exI)
    1.29 +  thus ?thesis unfolding LIMSEQ_def apply(rule_tac x="l" in exI)
    1.30      unfolding dist_norm  by auto
    1.31  qed
    1.32  
    1.33 @@ -2184,7 +2179,7 @@
    1.34   "(s ---> l) sequentially ==> Cauchy s"
    1.35  proof(simp only: cauchy_def, rule, rule)
    1.36    fix e::real assume "e>0" "(s ---> l) sequentially"
    1.37 -  then obtain N::nat where N:"\<forall>n\<ge>N. dist (s n) l < e/2" unfolding Lim_sequentially by(erule_tac x="e/2" in allE) auto
    1.38 +  then obtain N::nat where N:"\<forall>n\<ge>N. dist (s n) l < e/2" unfolding LIMSEQ_def by(erule_tac x="e/2" in allE) auto
    1.39    thus "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"  using dist_triangle_half_l[of _ l e _] by (rule_tac x=N in exI) auto
    1.40  qed
    1.41  
    1.42 @@ -2211,14 +2206,14 @@
    1.43  
    1.44      { fix e::real assume "e>0"
    1.45        from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto
    1.46 -      from lr(3)[unfolded Lim_sequentially, THEN spec[where x="e/2"]] obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
    1.47 +      from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
    1.48        { fix n::nat assume n:"n \<ge> max N M"
    1.49          have "dist ((f \<circ> r) n) l < e/2" using n M by auto
    1.50          moreover have "r n \<ge> N" using lr'[of n] n by auto
    1.51          hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto
    1.52          ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute)  }
    1.53        hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast  }
    1.54 -    hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding Lim_sequentially by auto  }
    1.55 +    hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding LIMSEQ_def by auto  }
    1.56    thus ?thesis unfolding complete_def by auto
    1.57  qed
    1.58  
    1.59 @@ -2341,7 +2336,7 @@
    1.60      using assms(3)[THEN bspec[where x=b]] unfolding open_dist by auto
    1.61  
    1.62    then obtain N1 where N1:"\<forall>n\<ge>N1. dist ((f \<circ> r) n) l < e / 2"
    1.63 -    using lr[unfolded Lim_sequentially, THEN spec[where x="e/2"]] by auto
    1.64 +    using lr[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto
    1.65  
    1.66    obtain N2::nat where N2:"N2>0" "inverse (real N2) < e /2" using real_arch_inv[of "e/2"] and `e>0` by auto
    1.67    have N2':"inverse (real (r (N1 + N2) +1 )) < e/2"
    1.68 @@ -2476,8 +2471,8 @@
    1.69      apply (rule t_less, rule f_r_neq)
    1.70      done
    1.71    show "((f \<circ> r) ---> l) sequentially"
    1.72 -    unfolding Lim_sequentially o_def
    1.73 -    apply (clarify, rule_tac x="t e" in exI, clarify)
    1.74 +    unfolding LIMSEQ_def o_def
    1.75 +    apply (clarify, rename_tac e, rule_tac x="t e" in exI, clarify)
    1.76      apply (drule le_trans, rule seq_suble [OF `subseq r`])
    1.77      apply (case_tac n, simp_all add: r_simps dist_f_t_less' f_r_neq)
    1.78      done
    1.79 @@ -2912,7 +2907,7 @@
    1.80  
    1.81    { fix n::nat
    1.82      { fix e::real assume "e>0"
    1.83 -      with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e" unfolding Lim_sequentially by auto
    1.84 +      with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e" unfolding LIMSEQ_def by auto
    1.85        hence "dist ((x \<circ> r) (max N n)) l < e" by auto
    1.86        moreover
    1.87        have "r (max N n) \<ge> n" using lr(2) using subseq_bigger[of r "max N n"] by auto
    1.88 @@ -2951,7 +2946,7 @@
    1.89    then obtain l where l:"(t ---> l) sequentially" using complete_univ unfolding complete_def by auto
    1.90    { fix n::nat
    1.91      { fix e::real assume "e>0"
    1.92 -      then obtain N::nat where N:"\<forall>n\<ge>N. dist (t n) l < e" using l[unfolded Lim_sequentially] by auto
    1.93 +      then obtain N::nat where N:"\<forall>n\<ge>N. dist (t n) l < e" using l[unfolded LIMSEQ_def] by auto
    1.94        have "t (max n N) \<in> s n" using assms(3) unfolding subset_eq apply(erule_tac x=n in allE) apply (erule_tac x="max n N" in allE) using t by auto
    1.95        hence "\<exists>y\<in>s n. dist y l < e" apply(rule_tac x="t (max n N)" in bexI) using N by auto
    1.96      }
    1.97 @@ -3008,7 +3003,7 @@
    1.98        using `?rhs`[THEN spec[where x="e/2"]] by auto
    1.99      { fix x assume "P x"
   1.100        then obtain M where M:"\<forall>n\<ge>M. dist (s n x) (l x) < e/2"
   1.101 -        using l[THEN spec[where x=x], unfolded Lim_sequentially] using `e>0` by(auto elim!: allE[where x="e/2"])
   1.102 +        using l[THEN spec[where x=x], unfolded LIMSEQ_def] using `e>0` by(auto elim!: allE[where x="e/2"])
   1.103        fix n::nat assume "n\<ge>N"
   1.104        hence "dist(s n x)(l x) < e"  using `P x`and N[THEN spec[where x=n], THEN spec[where x="N+M"], THEN spec[where x=x]]
   1.105          using M[THEN spec[where x="N+M"]] and dist_triangle_half_l[of "s n x" "s (N+M) x" e "l x"] by (auto simp add: dist_commute)  }
   1.106 @@ -3027,7 +3022,7 @@
   1.107    moreover
   1.108    { fix x assume "P x"
   1.109      hence "l x = l' x" using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
   1.110 -      using l and assms(2) unfolding Lim_sequentially by blast  }
   1.111 +      using l and assms(2) unfolding LIMSEQ_def by blast  }
   1.112    ultimately show ?thesis by auto
   1.113  qed
   1.114  
   1.115 @@ -3260,13 +3255,13 @@
   1.116      { fix e::real assume "e>0"
   1.117        then obtain d where "d>0" and d:"\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
   1.118          using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
   1.119 -      obtain N where N:"\<forall>n\<ge>N. dist (x n) (y n) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
   1.120 +      obtain N where N:"\<forall>n\<ge>N. dist (x n) (y n) < d" using xy[unfolded LIMSEQ_def dist_norm] and `d>0` by auto
   1.121        { fix n assume "n\<ge>N"
   1.122          hence "dist (f (x n)) (f (y n)) < e"
   1.123            using N[THEN spec[where x=n]] using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] using x and y
   1.124            unfolding dist_commute by simp  }
   1.125        hence "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"  by auto  }
   1.126 -    hence "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially" unfolding Lim_sequentially and dist_real_def by auto  }
   1.127 +    hence "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially" unfolding LIMSEQ_def and dist_real_def by auto  }
   1.128    thus ?rhs by auto
   1.129  next
   1.130    assume ?rhs
   1.131 @@ -3287,7 +3282,7 @@
   1.132          finally have "inverse (real n + 1) < e" by auto
   1.133          hence "dist (x n) (y n) < e" using xy0[THEN spec[where x=n]] by auto  }
   1.134        hence "\<exists>N. \<forall>n\<ge>N. dist (x n) (y n) < e" by auto  }
   1.135 -    hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially dist_real_def by auto
   1.136 +    hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding LIMSEQ_def dist_real_def by auto
   1.137      hence False using fxy and `e>0` by auto  }
   1.138    thus ?lhs unfolding uniformly_continuous_on_def by blast
   1.139  qed
   1.140 @@ -3974,10 +3969,10 @@
   1.141      then obtain l r where "l\<in>s" and r:"subseq r" and lr:"((y \<circ> r) ---> l) sequentially" using assms(2)[unfolded compact_def, THEN spec[where x=y]] by auto
   1.142      { fix e::real assume "e>0"
   1.143        then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' l < d \<longrightarrow> dist (f x') (f l) < e" using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=l], OF `l\<in>s`] by auto
   1.144 -      then obtain N::nat where N:"\<forall>n\<ge>N. dist ((y \<circ> r) n) l < d" using lr[unfolded Lim_sequentially, THEN spec[where x=d]] by auto
   1.145 +      then obtain N::nat where N:"\<forall>n\<ge>N. dist ((y \<circ> r) n) l < d" using lr[unfolded LIMSEQ_def, THEN spec[where x=d]] by auto
   1.146        { fix n::nat assume "n\<ge>N" hence "dist ((x \<circ> r) n) (f l) < e" using N[THEN spec[where x=n]] d[THEN bspec[where x="y (r n)"]] y[THEN spec[where x="r n"]] by auto  }
   1.147        hence "\<exists>N. \<forall>n\<ge>N. dist ((x \<circ> r) n) (f l) < e" by auto  }
   1.148 -    hence "\<exists>l\<in>f ` s. \<exists>r. subseq r \<and> ((x \<circ> r) ---> l) sequentially" unfolding Lim_sequentially using r lr `l\<in>s` by auto  }
   1.149 +    hence "\<exists>l\<in>f ` s. \<exists>r. subseq r \<and> ((x \<circ> r) ---> l) sequentially" unfolding LIMSEQ_def using r lr `l\<in>s` by auto  }
   1.150    thus ?thesis unfolding compact_def by auto
   1.151  qed
   1.152  
   1.153 @@ -4403,11 +4398,11 @@
   1.154        { fix e::real assume "e>0"
   1.155          hence "0 < e *\<bar>c\<bar>"  using `c\<noteq>0` mult_pos_pos[of e "abs c"] by auto
   1.156          then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>"
   1.157 -          using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto
   1.158 +          using as(2)[unfolded LIMSEQ_def, THEN spec[where x="e * abs c"]] by auto
   1.159          hence "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e"
   1.160            unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym]
   1.161            using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto  }
   1.162 -      hence "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" unfolding Lim_sequentially by auto
   1.163 +      hence "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" unfolding LIMSEQ_def by auto
   1.164        ultimately have "l \<in> scaleR c ` s"
   1.165          using assms[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. scaleR (1/c) (x n)"], THEN spec[where x="scaleR (1/c) l"]]
   1.166          unfolding image_iff using `c\<noteq>0` apply(rule_tac x="scaleR (1 / c) l" in bexI) by auto  }
   1.167 @@ -4837,7 +4832,7 @@
   1.168          hence "\<forall>n\<ge>N. inverse (real n + 1) < e" by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero)
   1.169          hence "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto  }
   1.170        hence "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
   1.171 -        unfolding Lim_sequentially by(auto simp add: dist_norm)
   1.172 +        unfolding LIMSEQ_def by(auto simp add: dist_norm)
   1.173        hence "(f ---> x) sequentially" unfolding f_def
   1.174          using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
   1.175          using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto  }
   1.176 @@ -5734,7 +5729,7 @@
   1.177      assume "e \<noteq> 0" hence "e>0" unfolding e_def using zero_le_dist[of "f x" x]
   1.178        by (metis dist_eq_0_iff dist_nz e_def)
   1.179      then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e / 2"
   1.180 -      using x[unfolded Lim_sequentially, THEN spec[where x="e/2"]] by auto
   1.181 +      using x[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto
   1.182      hence N':"dist (z N) x < e / 2" by auto
   1.183  
   1.184      have *:"c * dist (z N) x \<le> dist (z N) x" unfolding mult_le_cancel_right2
   1.185 @@ -5831,7 +5826,7 @@
   1.186      { assume as:"dist a b > dist (f n x) (f n y)"
   1.187        then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
   1.188          and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
   1.189 -        using lima limb unfolding h_def Lim_sequentially by (fastforce simp del: less_divide_eq_number_of1)
   1.190 +        using lima limb unfolding h_def LIMSEQ_def by (fastforce simp del: less_divide_eq_number_of1)
   1.191        hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
   1.192          apply(erule_tac x="Na+Nb+n" in allE)
   1.193          apply(erule_tac x="Na+Nb+n" in allE) apply simp
   1.194 @@ -5852,8 +5847,8 @@
   1.195      def e \<equiv> "dist a b - dist (g a) (g b)"
   1.196      assume "a\<noteq>b" hence "e > 0" unfolding e_def using dist by fastforce
   1.197      hence "\<exists>n. dist (f n x) a < e/2 \<and> dist (f n y) b < e/2"
   1.198 -      using lima limb unfolding Lim_sequentially
   1.199 -      apply (auto elim!: allE[where x="e/2"]) apply(rule_tac x="r (max N Na)" in exI) unfolding h_def by fastforce
   1.200 +      using lima limb unfolding LIMSEQ_def
   1.201 +      apply (auto elim!: allE[where x="e/2"]) apply(rename_tac N N', rule_tac x="r (max N N')" in exI) unfolding h_def by fastforce
   1.202      then obtain n where n:"dist (f n x) a < e/2 \<and> dist (f n y) b < e/2" by auto
   1.203      have "dist (f (Suc n) x) (g a) \<le> dist (f n x) a"
   1.204        using dist[THEN bspec[where x="f n x"], THEN bspec[where x="a"]] and fs by auto