src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 44584 08ad27488983 parent 44571 bd91b77c4cd6 child 44628 bd17b7543af1
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 29 22:10:08 2011 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 29 13:50:47 2011 -0700
1.3 @@ -443,27 +443,24 @@
1.4    obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x"
1.5    using assms unfolding islimpt_def by auto
1.6
1.7 -lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def)
1.8 +lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
1.9 +  unfolding islimpt_def eventually_at_topological by auto
1.10 +
1.11 +lemma islimpt_subset: "\<lbrakk>x islimpt S; S \<subseteq> T\<rbrakk> \<Longrightarrow> x islimpt T"
1.12 +  unfolding islimpt_def by fast
1.13
1.14  lemma islimpt_approachable:
1.15    fixes x :: "'a::metric_space"
1.16    shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"
1.17 -  unfolding islimpt_def
1.18 -  apply auto
1.19 -  apply(erule_tac x="ball x e" in allE)
1.20 -  apply auto
1.21 -  apply(rule_tac x=y in bexI)
1.22 -  apply (auto simp add: dist_commute)
1.23 -  apply (simp add: open_dist, drule (1) bspec)
1.24 -  apply (clarify, drule spec, drule (1) mp, auto)
1.25 -  done
1.26 +  unfolding islimpt_iff_eventually eventually_at by fast
1.27
1.28  lemma islimpt_approachable_le:
1.29    fixes x :: "'a::metric_space"
1.30    shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
1.31    unfolding islimpt_approachable
1.32 -  using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
1.33 -  by metis
1.34 +  using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x",
1.35 +    THEN arg_cong [where f=Not]]
1.36 +  by (simp add: Bex_def conj_commute conj_left_commute)
1.37
1.38  lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
1.39    unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
1.40 @@ -1058,65 +1055,11 @@
1.41    using assms by (simp only: at_within_open)
1.42
1.43  lemma Lim_within_LIMSEQ:
1.44 -  fixes a :: real and L :: "'a::metric_space"
1.45 +  fixes a :: "'a::metric_space"
1.46    assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
1.47    shows "(X ---> L) (at a within T)"
1.48 -proof (rule ccontr)
1.49 -  assume "\<not> (X ---> L) (at a within T)"
1.50 -  hence "\<exists>r>0. \<forall>s>0. \<exists>x\<in>T. x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> r \<le> dist (X x) L"
1.51 -    unfolding tendsto_iff eventually_within dist_norm by (simp add: not_less[symmetric])
1.52 -  then obtain r where r: "r > 0" "\<And>s. s > 0 \<Longrightarrow> \<exists>x\<in>T-{a}. \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r" by blast
1.53 -
1.54 -  let ?F = "\<lambda>n::nat. SOME x. x \<in> T \<and> x \<noteq> a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
1.55 -  have "\<And>n. \<exists>x. x \<in> T \<and> x \<noteq> a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
1.56 -    using r by (simp add: Bex_def)
1.57 -  hence F: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r"
1.58 -    by (rule someI_ex)
1.59 -  hence F1: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a"
1.60 -    and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
1.61 -    and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
1.62 -    by fast+
1.63 -
1.64 -  have "?F ----> a"
1.65 -  proof (rule LIMSEQ_I, unfold real_norm_def)
1.66 -      fix e::real
1.67 -      assume "0 < e"
1.68 -        (* choose no such that inverse (real (Suc n)) < e *)
1.69 -      then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
1.70 -      then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
1.71 -      show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
1.72 -      proof (intro exI allI impI)
1.73 -        fix n
1.74 -        assume mlen: "m \<le> n"
1.75 -        have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
1.76 -          by (rule F2)
1.77 -        also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
1.78 -          using mlen by auto
1.79 -        also from nodef have
1.80 -          "inverse (real (Suc m)) < e" .
1.81 -        finally show "\<bar>?F n - a\<bar> < e" .
1.82 -      qed
1.83 -  qed
1.84 -  moreover note `\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
1.85 -  ultimately have "(\<lambda>n. X (?F n)) ----> L" using F1 by simp
1.86 -
1.87 -  moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
1.88 -  proof -
1.89 -    {
1.90 -      fix no::nat
1.91 -      obtain n where "n = no + 1" by simp
1.92 -      then have nolen: "no \<le> n" by simp
1.93 -        (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
1.94 -      have "dist (X (?F n)) L \<ge> r"
1.95 -        by (rule F3)
1.96 -      with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
1.97 -    }
1.98 -    then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
1.99 -    with r have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
1.100 -    thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
1.101 -  qed
1.102 -  ultimately show False by simp
1.103 -qed
1.104 +  using assms unfolding tendsto_def [where l=L]
1.105 +  by (simp add: sequentially_imp_eventually_within)
1.106
1.107  lemma Lim_right_bound:
1.108    fixes f :: "real \<Rightarrow> real"
1.109 @@ -1160,21 +1103,18 @@
1.110  proof
1.111    assume ?lhs
1.112    then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y"
1.113 -    unfolding islimpt_approachable using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto
1.114 -  { fix n::nat
1.115 -    have "f (inverse (real n + 1)) \<in> S - {x}" using f by auto
1.116 -  }
1.117 -  moreover
1.118 -  { fix e::real assume "e>0"
1.119 -    hence "\<exists>N::nat. inverse (real (N + 1)) < e" using real_arch_inv[of e] apply (auto simp add: Suc_pred') apply(rule_tac x="n - 1" in exI) by auto
1.120 -    then obtain N::nat where "inverse (real (N + 1)) < e" by auto
1.121 -    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.122 -    moreover have "\<forall>n\<ge>N. dist (f (inverse (real n + 1))) x < (inverse (real n + 1))" using f `e>0` by auto
1.123 -    ultimately have "\<exists>N::nat. \<forall>n\<ge>N. dist (f (inverse (real n + 1))) x < e" apply(rule_tac x=N in exI) apply auto apply(erule_tac x=n in allE)+ by auto
1.124 -  }
1.125 -  hence " ((\<lambda>n. f (inverse (real n + 1))) ---> x) sequentially"
1.126 -    unfolding Lim_sequentially using f by auto
1.127 -  ultimately show ?rhs apply (rule_tac x="(\<lambda>n::nat. f (inverse (real n + 1)))" in exI) by auto
1.128 +    unfolding islimpt_approachable
1.129 +    using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto
1.130 +  let ?I = "\<lambda>n. inverse (real (Suc n))"
1.131 +  have "\<forall>n. f (?I n) \<in> S - {x}" using f by simp
1.132 +  moreover have "(\<lambda>n. f (?I n)) ----> x"
1.133 +  proof (rule metric_tendsto_imp_tendsto)
1.134 +    show "?I ----> 0"
1.135 +      by (rule LIMSEQ_inverse_real_of_nat)
1.136 +    show "eventually (\<lambda>n. dist (f (?I n)) x \<le> dist (?I n) 0) sequentially"
1.137 +      by (simp add: norm_conv_dist [symmetric] less_imp_le f)
1.138 +  qed
1.139 +  ultimately show ?rhs by fast
1.140  next
1.141    assume ?rhs
1.142    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.143 @@ -1331,7 +1271,7 @@
1.144    shows "netlimit (at a) = a"
1.145    apply (subst within_UNIV[symmetric])
1.146    using netlimit_within[of a UNIV]
1.147 -  by (simp add: trivial_limit_at within_UNIV)
1.148 +  by (simp add: within_UNIV)
1.149
1.150  lemma lim_within_interior:
1.151    "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
1.152 @@ -1480,8 +1420,7 @@
1.153  lemma seq_offset:
1.154    assumes "(f ---> l) sequentially"
1.155    shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
1.156 -  using assms unfolding tendsto_def
1.157 -  by clarify (rule sequentially_offset, simp)
1.158 +  using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *)
1.159
1.160  lemma seq_offset_neg:
1.161    "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
1.162 @@ -1494,21 +1433,10 @@
1.163
1.164  lemma seq_offset_rev:
1.165    "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
1.166 -  apply (rule topological_tendstoI)
1.167 -  apply (drule (2) topological_tendstoD)
1.168 -  apply (simp only: eventually_sequentially)
1.169 -  apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
1.170 -  by metis arith
1.171 +  by (rule LIMSEQ_offset) (* FIXME: redundant *)
1.172
1.173  lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
1.174 -proof-
1.175 -  { fix e::real assume "e>0"
1.176 -    hence "\<exists>N::nat. \<forall>n::nat\<ge>N. inverse (real n) < e"
1.177 -      using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI)
1.178 -      by (metis le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
1.179 -  }
1.180 -  thus ?thesis unfolding Lim_sequentially dist_norm by simp
1.181 -qed
1.182 +  using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc)
1.183
1.184  subsection {* More properties of closed balls *}
1.185
1.186 @@ -3154,7 +3082,7 @@
1.187  lemma continuous_within_eps_delta:
1.188    "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"
1.189    unfolding continuous_within and Lim_within
1.190 -  apply auto unfolding dist_nz[THEN sym] apply(auto elim!:allE) apply(rule_tac x=d in exI) by auto
1.191 +  apply auto unfolding dist_nz[THEN sym] apply(auto del: allE elim!:allE) apply(rule_tac x=d in exI) by auto
1.192
1.193  lemma continuous_at_eps_delta: "continuous (at x) f \<longleftrightarrow>  (\<forall>e>0. \<exists>d>0.
1.194                             \<forall>x'. dist x' x < d --> dist(f x')(f x) < e)"
1.195 @@ -4408,7 +4336,7 @@
1.196    note * = this
1.197    { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
1.198      have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s`
1.199 -      by simp (blast intro!: Sup_upper *) }
1.200 +      by simp (blast del: Sup_upper intro!: * Sup_upper) }
1.201    moreover
1.202    { fix d::real assume "d>0" "d < diameter s"
1.203      hence "s\<noteq>{}" unfolding diameter_def by auto
1.204 @@ -4667,39 +4595,26 @@
1.205    "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a\$\$i < b\$\$i)"
1.206    unfolding interval_eq_empty[of a b] by fastsimp+
1.207
1.208 -lemma interval_sing: fixes a :: "'a::ordered_euclidean_space" shows
1.209 - "{a .. a} = {a}" "{a<..<a} = {}"
1.210 -  apply(auto simp add: set_eq_iff euclidean_eq[where 'a='a] eucl_less[where 'a='a] eucl_le[where 'a='a])
1.211 -  apply (simp add: order_eq_iff) apply(rule_tac x=0 in exI) by (auto simp add: not_less less_imp_le)
1.212 +lemma interval_sing:
1.213 +  fixes a :: "'a::ordered_euclidean_space"
1.214 +  shows "{a .. a} = {a}" and "{a<..<a} = {}"
1.215 +  unfolding set_eq_iff mem_interval eq_iff [symmetric]
1.216 +  by (auto simp add: euclidean_eq[where 'a='a] eq_commute
1.217 +    eucl_less[where 'a='a] eucl_le[where 'a='a])
1.218
1.219  lemma subset_interval_imp: fixes a :: "'a::ordered_euclidean_space" shows
1.220   "(\<forall>i<DIM('a). a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" and
1.221   "(\<forall>i<DIM('a). a\$\$i < c\$\$i \<and> d\$\$i < b\$\$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}" and
1.222   "(\<forall>i<DIM('a). a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}" and
1.223   "(\<forall>i<DIM('a). a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
1.224 -  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
1.225 -  by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
1.226 -
1.227 -lemma interval_open_subset_closed:  fixes a :: "'a::ordered_euclidean_space" shows
1.228 - "{a<..<b} \<subseteq> {a .. b}"
1.230 -  fix x
1.231 -  assume x:"x \<in>{a<..<b}"
1.232 -  { fix i assume "i<DIM('a)"
1.233 -    hence "a \$\$ i \<le> x \$\$ i"
1.234 -      using x order_less_imp_le[of "a\$\$i" "x\$\$i"]
1.235 -      by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
1.236 -  }
1.237 -  moreover
1.238 -  { fix i assume "i<DIM('a)"
1.239 -    hence "x \$\$ i \<le> b \$\$ i"
1.240 -      using x order_less_imp_le[of "x\$\$i" "b\$\$i"]
1.241 -      by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
1.242 -  }
1.243 -  ultimately
1.244 -  show "a \<le> x \<and> x \<le> b"
1.245 -    by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
1.246 -qed
1.247 +  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
1.248 +  by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
1.249 +
1.250 +lemma interval_open_subset_closed:
1.251 +  fixes a :: "'a::ordered_euclidean_space"
1.252 +  shows "{a<..<b} \<subseteq> {a .. b}"
1.253 +  unfolding subset_eq [unfolded Ball_def] mem_interval
1.254 +  by (fast intro: less_imp_le)
1.255
1.256  lemma subset_interval: fixes a :: "'a::ordered_euclidean_space" shows
1.257   "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i<DIM('a). c\$\$i \<le> d\$\$i) --> (\<forall>i<DIM('a). a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i)" (is ?th1) and
1.258 @@ -4825,7 +4740,7 @@
1.259                       "(x + (e / 2) *\<^sub>R basis i) \$\$ i \<le> b \$\$ i"
1.260          using e[THEN spec[where x="x - (e/2) *\<^sub>R basis i"]]
1.261          and   e[THEN spec[where x="x + (e/2) *\<^sub>R basis i"]]
1.262 -        unfolding mem_interval by (auto elim!: allE[where x=i])
1.263 +        unfolding mem_interval using i by blast+
1.264        hence "a \$\$ i < x \$\$ i" and "x \$\$ i < b \$\$ i" unfolding euclidean_simps
1.265          unfolding basis_component using `e>0` i by auto  }
1.266      hence "x \<in> {a<..<b}" unfolding mem_interval by auto  }
1.267 @@ -5009,9 +4924,8 @@
1.268
1.269  lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
1.270    "is_interval {a<..<b}" (is ?th2) proof -
1.271 -  have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
1.272    show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
1.273 -    by(meson order_trans le_less_trans less_le_trans *)+ qed
1.274 +    by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
1.275
1.276  lemma is_interval_empty:
1.277   "is_interval {}"
```