author | immler |
Mon, 07 Jan 2019 12:31:08 +0100 | |
changeset 69615 | e502cd4d7062 |
parent 69613 | 1331e57b54c6 |
child 69617 | 63ee37c519a3 |
permissions | -rw-r--r-- |
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1 |
(* Author: L C Paulson, University of Cambridge |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
2 |
Author: Amine Chaieb, University of Cambridge |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
3 |
Author: Robert Himmelmann, TU Muenchen |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
4 |
Author: Brian Huffman, Portland State University |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
5 |
*) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
6 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
7 |
section \<open>Elementary Normed Vector Spaces\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
8 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
9 |
theory Elementary_Normed_Spaces |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
10 |
imports |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
11 |
"HOL-Library.FuncSet" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
12 |
Elementary_Metric_Spaces |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
13 |
begin |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
14 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
15 |
subsection%unimportant \<open>Various Lemmas Combining Imports\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
16 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
17 |
lemma countable_PiE: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
18 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
19 |
by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
20 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
21 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
22 |
lemma open_sums: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
23 |
fixes T :: "('b::real_normed_vector) set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
24 |
assumes "open S \<or> open T" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
25 |
shows "open (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
26 |
using assms |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
27 |
proof |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
28 |
assume S: "open S" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
29 |
show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
30 |
proof (clarsimp simp: open_dist) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
31 |
fix x y |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
32 |
assume "x \<in> S" "y \<in> T" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
33 |
with S obtain e where "e > 0" and e: "\<And>x'. dist x' x < e \<Longrightarrow> x' \<in> S" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
34 |
by (auto simp: open_dist) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
35 |
then have "\<And>z. dist z (x + y) < e \<Longrightarrow> \<exists>x\<in>S. \<exists>y\<in>T. z = x + y" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
36 |
by (metis \<open>y \<in> T\<close> diff_add_cancel dist_add_cancel2) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
37 |
then show "\<exists>e>0. \<forall>z. dist z (x + y) < e \<longrightarrow> (\<exists>x\<in>S. \<exists>y\<in>T. z = x + y)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
38 |
using \<open>0 < e\<close> \<open>x \<in> S\<close> by blast |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
39 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
40 |
next |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
41 |
assume T: "open T" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
42 |
show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
43 |
proof (clarsimp simp: open_dist) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
44 |
fix x y |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
45 |
assume "x \<in> S" "y \<in> T" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
46 |
with T obtain e where "e > 0" and e: "\<And>x'. dist x' y < e \<Longrightarrow> x' \<in> T" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
47 |
by (auto simp: open_dist) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
48 |
then have "\<And>z. dist z (x + y) < e \<Longrightarrow> \<exists>x\<in>S. \<exists>y\<in>T. z = x + y" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
49 |
by (metis \<open>x \<in> S\<close> add_diff_cancel_left' add_diff_eq diff_diff_add dist_norm) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
50 |
then show "\<exists>e>0. \<forall>z. dist z (x + y) < e \<longrightarrow> (\<exists>x\<in>S. \<exists>y\<in>T. z = x + y)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
51 |
using \<open>0 < e\<close> \<open>y \<in> T\<close> by blast |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
52 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
53 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
54 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
55 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
56 |
subsection \<open>Support\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
57 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
58 |
definition (in monoid_add) support_on :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'b set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
59 |
where "support_on s f = {x\<in>s. f x \<noteq> 0}" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
60 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
61 |
lemma in_support_on: "x \<in> support_on s f \<longleftrightarrow> x \<in> s \<and> f x \<noteq> 0" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
62 |
by (simp add: support_on_def) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
63 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
64 |
lemma support_on_simps[simp]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
65 |
"support_on {} f = {}" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
66 |
"support_on (insert x s) f = |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
67 |
(if f x = 0 then support_on s f else insert x (support_on s f))" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
68 |
"support_on (s \<union> t) f = support_on s f \<union> support_on t f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
69 |
"support_on (s \<inter> t) f = support_on s f \<inter> support_on t f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
70 |
"support_on (s - t) f = support_on s f - support_on t f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
71 |
"support_on (f ` s) g = f ` (support_on s (g \<circ> f))" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
72 |
unfolding support_on_def by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
73 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
74 |
lemma support_on_cong: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
75 |
"(\<And>x. x \<in> s \<Longrightarrow> f x = 0 \<longleftrightarrow> g x = 0) \<Longrightarrow> support_on s f = support_on s g" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
76 |
by (auto simp: support_on_def) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
77 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
78 |
lemma support_on_if: "a \<noteq> 0 \<Longrightarrow> support_on A (\<lambda>x. if P x then a else 0) = {x\<in>A. P x}" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
79 |
by (auto simp: support_on_def) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
80 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
81 |
lemma support_on_if_subset: "support_on A (\<lambda>x. if P x then a else 0) \<subseteq> {x \<in> A. P x}" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
82 |
by (auto simp: support_on_def) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
83 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
84 |
lemma finite_support[intro]: "finite S \<Longrightarrow> finite (support_on S f)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
85 |
unfolding support_on_def by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
86 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
87 |
(* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
88 |
definition (in comm_monoid_add) supp_sum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
89 |
where "supp_sum f S = (\<Sum>x\<in>support_on S f. f x)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
90 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
91 |
lemma supp_sum_empty[simp]: "supp_sum f {} = 0" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
92 |
unfolding supp_sum_def by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
93 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
94 |
lemma supp_sum_insert[simp]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
95 |
"finite (support_on S f) \<Longrightarrow> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
96 |
supp_sum f (insert x S) = (if x \<in> S then supp_sum f S else f x + supp_sum f S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
97 |
by (simp add: supp_sum_def in_support_on insert_absorb) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
98 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
99 |
lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (\<lambda>n. f n / r) A" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
100 |
by (cases "r = 0") |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
101 |
(auto simp: supp_sum_def sum_divide_distrib intro!: sum.cong support_on_cong) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
102 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
103 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
104 |
subsection \<open>Intervals\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
105 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
106 |
lemma image_affinity_interval: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
107 |
fixes c :: "'a::ordered_real_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
108 |
shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
109 |
(if {a..b}={} then {} |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
110 |
else if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
111 |
else {m *\<^sub>R b + c .. m *\<^sub>R a + c})" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
112 |
(is "?lhs = ?rhs") |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
113 |
proof (cases "m=0") |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
114 |
case True |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
115 |
then show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
116 |
by force |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
117 |
next |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
118 |
case False |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
119 |
show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
120 |
proof |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
121 |
show "?lhs \<subseteq> ?rhs" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
122 |
by (auto simp: scaleR_left_mono scaleR_left_mono_neg) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
123 |
show "?rhs \<subseteq> ?lhs" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
124 |
proof (clarsimp, intro conjI impI subsetI) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
125 |
show "\<lbrakk>0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}\<rbrakk> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
126 |
\<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
127 |
apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
128 |
using False apply (auto simp: le_diff_eq pos_le_divideRI) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
129 |
using diff_le_eq pos_le_divideR_eq by force |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
130 |
show "\<lbrakk>\<not> 0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R b + c..m *\<^sub>R a + c}\<rbrakk> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
131 |
\<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
132 |
apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
133 |
apply (auto simp: diff_le_eq neg_le_divideR_eq) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
134 |
using diff_eq_diff_less_eq linordered_field_class.sign_simps(11) minus_diff_eq not_less scaleR_le_cancel_left_neg by fastforce |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
135 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
136 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
137 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
138 |
|
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
139 |
subsection \<open>Limit Points\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
140 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
141 |
lemma islimpt_ball: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
142 |
fixes x y :: "'a::{real_normed_vector,perfect_space}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
143 |
shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
144 |
(is "?lhs \<longleftrightarrow> ?rhs") |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
145 |
proof |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
146 |
show ?rhs if ?lhs |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
147 |
proof |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
148 |
{ |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
149 |
assume "e \<le> 0" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
150 |
then have *: "ball x e = {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
151 |
using ball_eq_empty[of x e] by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
152 |
have False using \<open>?lhs\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
153 |
unfolding * using islimpt_EMPTY[of y] by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
154 |
} |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
155 |
then show "e > 0" by (metis not_less) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
156 |
show "y \<in> cball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
157 |
using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"] |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
158 |
ball_subset_cball[of x e] \<open>?lhs\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
159 |
unfolding closed_limpt by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
160 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
161 |
show ?lhs if ?rhs |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
162 |
proof - |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
163 |
from that have "e > 0" by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
164 |
{ |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
165 |
fix d :: real |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
166 |
assume "d > 0" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
167 |
have "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
168 |
proof (cases "d \<le> dist x y") |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
169 |
case True |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
170 |
then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
171 |
proof (cases "x = y") |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
172 |
case True |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
173 |
then have False |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
174 |
using \<open>d \<le> dist x y\<close> \<open>d>0\<close> by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
175 |
then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
176 |
by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
177 |
next |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
178 |
case False |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
179 |
have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) = |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
180 |
norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
181 |
unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric] |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
182 |
by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
183 |
also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
184 |
using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"] |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
185 |
unfolding scaleR_minus_left scaleR_one |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
186 |
by (auto simp: norm_minus_commute) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
187 |
also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
188 |
unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]] |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
189 |
unfolding distrib_right using \<open>x\<noteq>y\<close> by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
190 |
also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
191 |
by (auto simp: dist_norm) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
192 |
finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
193 |
by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
194 |
moreover |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
195 |
have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
196 |
using \<open>x\<noteq>y\<close>[unfolded dist_nz] \<open>d>0\<close> unfolding scaleR_eq_0_iff |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
197 |
by (auto simp: dist_commute) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
198 |
moreover |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
199 |
have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
200 |
unfolding dist_norm |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
201 |
apply simp |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
202 |
unfolding norm_minus_cancel |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
203 |
using \<open>d > 0\<close> \<open>x\<noteq>y\<close>[unfolded dist_nz] dist_commute[of x y] |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
204 |
unfolding dist_norm |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
205 |
apply auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
206 |
done |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
207 |
ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
208 |
apply (rule_tac x = "y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
209 |
apply auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
210 |
done |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
211 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
212 |
next |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
213 |
case False |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
214 |
then have "d > dist x y" by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
215 |
show "\<exists>x' \<in> ball x e. x' \<noteq> y \<and> dist x' y < d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
216 |
proof (cases "x = y") |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
217 |
case True |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
218 |
obtain z where **: "z \<noteq> y" "dist z y < min e d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
219 |
using perfect_choose_dist[of "min e d" y] |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
220 |
using \<open>d > 0\<close> \<open>e>0\<close> by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
221 |
show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
222 |
unfolding \<open>x = y\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
223 |
using \<open>z \<noteq> y\<close> ** |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
224 |
apply (rule_tac x=z in bexI) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
225 |
apply (auto simp: dist_commute) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
226 |
done |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
227 |
next |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
228 |
case False |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
229 |
then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
230 |
using \<open>d>0\<close> \<open>d > dist x y\<close> \<open>?rhs\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
231 |
apply (rule_tac x=x in bexI, auto) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
232 |
done |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
233 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
234 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
235 |
} |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
236 |
then show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
237 |
unfolding mem_cball islimpt_approachable mem_ball by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
238 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
239 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
240 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
241 |
lemma closure_ball_lemma: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
242 |
fixes x y :: "'a::real_normed_vector" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
243 |
assumes "x \<noteq> y" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
244 |
shows "y islimpt ball x (dist x y)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
245 |
proof (rule islimptI) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
246 |
fix T |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
247 |
assume "y \<in> T" "open T" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
248 |
then obtain r where "0 < r" "\<forall>z. dist z y < r \<longrightarrow> z \<in> T" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
249 |
unfolding open_dist by fast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
250 |
(* choose point between x and y, within distance r of y. *) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
251 |
define k where "k = min 1 (r / (2 * dist x y))" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
252 |
define z where "z = y + scaleR k (x - y)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
253 |
have z_def2: "z = x + scaleR (1 - k) (y - x)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
254 |
unfolding z_def by (simp add: algebra_simps) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
255 |
have "dist z y < r" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
256 |
unfolding z_def k_def using \<open>0 < r\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
257 |
by (simp add: dist_norm min_def) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
258 |
then have "z \<in> T" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
259 |
using \<open>\<forall>z. dist z y < r \<longrightarrow> z \<in> T\<close> by simp |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
260 |
have "dist x z < dist x y" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
261 |
unfolding z_def2 dist_norm |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
262 |
apply (simp add: norm_minus_commute) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
263 |
apply (simp only: dist_norm [symmetric]) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
264 |
apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
265 |
apply (rule mult_strict_right_mono) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
266 |
apply (simp add: k_def \<open>0 < r\<close> \<open>x \<noteq> y\<close>) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
267 |
apply (simp add: \<open>x \<noteq> y\<close>) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
268 |
done |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
269 |
then have "z \<in> ball x (dist x y)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
270 |
by simp |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
271 |
have "z \<noteq> y" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
272 |
unfolding z_def k_def using \<open>x \<noteq> y\<close> \<open>0 < r\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
273 |
by (simp add: min_def) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
274 |
show "\<exists>z\<in>ball x (dist x y). z \<in> T \<and> z \<noteq> y" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
275 |
using \<open>z \<in> ball x (dist x y)\<close> \<open>z \<in> T\<close> \<open>z \<noteq> y\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
276 |
by fast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
277 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
278 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
279 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
280 |
subsection \<open>Balls and Spheres in Normed Spaces\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
281 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
282 |
lemma mem_ball_0 [simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
283 |
for x :: "'a::real_normed_vector" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
284 |
by (simp add: dist_norm) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
285 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
286 |
lemma mem_cball_0 [simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
287 |
for x :: "'a::real_normed_vector" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
288 |
by (simp add: dist_norm) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
289 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
290 |
lemma closure_ball [simp]: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
291 |
fixes x :: "'a::real_normed_vector" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
292 |
shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
293 |
apply (rule equalityI) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
294 |
apply (rule closure_minimal) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
295 |
apply (rule ball_subset_cball) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
296 |
apply (rule closed_cball) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
297 |
apply (rule subsetI, rename_tac y) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
298 |
apply (simp add: le_less [where 'a=real]) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
299 |
apply (erule disjE) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
300 |
apply (rule subsetD [OF closure_subset], simp) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
301 |
apply (simp add: closure_def, clarify) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
302 |
apply (rule closure_ball_lemma) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
303 |
apply simp |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
304 |
done |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
305 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
306 |
lemma mem_sphere_0 [simp]: "x \<in> sphere 0 e \<longleftrightarrow> norm x = e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
307 |
for x :: "'a::real_normed_vector" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
308 |
by (simp add: dist_norm) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
309 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
310 |
(* In a trivial vector space, this fails for e = 0. *) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
311 |
lemma interior_cball [simp]: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
312 |
fixes x :: "'a::{real_normed_vector, perfect_space}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
313 |
shows "interior (cball x e) = ball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
314 |
proof (cases "e \<ge> 0") |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
315 |
case False note cs = this |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
316 |
from cs have null: "ball x e = {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
317 |
using ball_empty[of e x] by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
318 |
moreover |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
319 |
have "cball x e = {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
320 |
proof (rule equals0I) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
321 |
fix y |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
322 |
assume "y \<in> cball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
323 |
then show False |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
324 |
by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
325 |
subset_antisym subset_ball) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
326 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
327 |
then have "interior (cball x e) = {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
328 |
using interior_empty by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
329 |
ultimately show ?thesis by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
330 |
next |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
331 |
case True note cs = this |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
332 |
have "ball x e \<subseteq> cball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
333 |
using ball_subset_cball by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
334 |
moreover |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
335 |
{ |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
336 |
fix S y |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
337 |
assume as: "S \<subseteq> cball x e" "open S" "y\<in>S" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
338 |
then obtain d where "d>0" and d: "\<forall>x'. dist x' y < d \<longrightarrow> x' \<in> S" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
339 |
unfolding open_dist by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
340 |
then obtain xa where xa_y: "xa \<noteq> y" and xa: "dist xa y < d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
341 |
using perfect_choose_dist [of d] by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
342 |
have "xa \<in> S" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
343 |
using d[THEN spec[where x = xa]] |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
344 |
using xa by (auto simp: dist_commute) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
345 |
then have xa_cball: "xa \<in> cball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
346 |
using as(1) by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
347 |
then have "y \<in> ball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
348 |
proof (cases "x = y") |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
349 |
case True |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
350 |
then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
351 |
then show "y \<in> ball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
352 |
using \<open>x = y \<close> by simp |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
353 |
next |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
354 |
case False |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
355 |
have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
356 |
unfolding dist_norm |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
357 |
using \<open>d>0\<close> norm_ge_zero[of "y - x"] \<open>x \<noteq> y\<close> by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
358 |
then have *: "y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
359 |
using d as(1)[unfolded subset_eq] by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
360 |
have "y - x \<noteq> 0" using \<open>x \<noteq> y\<close> by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
361 |
hence **:"d / (2 * norm (y - x)) > 0" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
362 |
unfolding zero_less_norm_iff[symmetric] using \<open>d>0\<close> by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
363 |
have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x = |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
364 |
norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
365 |
by (auto simp: dist_norm algebra_simps) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
366 |
also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *\<^sub>R (y - x))" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
367 |
by (auto simp: algebra_simps) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
368 |
also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
369 |
using ** by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
370 |
also have "\<dots> = (dist y x) + d/2" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
371 |
using ** by (auto simp: distrib_right dist_norm) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
372 |
finally have "e \<ge> dist x y +d/2" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
373 |
using *[unfolded mem_cball] by (auto simp: dist_commute) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
374 |
then show "y \<in> ball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
375 |
unfolding mem_ball using \<open>d>0\<close> by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
376 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
377 |
} |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
378 |
then have "\<forall>S \<subseteq> cball x e. open S \<longrightarrow> S \<subseteq> ball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
379 |
by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
380 |
ultimately show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
381 |
using interior_unique[of "ball x e" "cball x e"] |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
382 |
using open_ball[of x e] |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
383 |
by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
384 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
385 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
386 |
lemma frontier_ball [simp]: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
387 |
fixes a :: "'a::real_normed_vector" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
388 |
shows "0 < e \<Longrightarrow> frontier (ball a e) = sphere a e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
389 |
by (force simp: frontier_def) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
390 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
391 |
lemma frontier_cball [simp]: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
392 |
fixes a :: "'a::{real_normed_vector, perfect_space}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
393 |
shows "frontier (cball a e) = sphere a e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
394 |
by (force simp: frontier_def) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
395 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
396 |
corollary compact_sphere [simp]: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
397 |
fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
398 |
shows "compact (sphere a r)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
399 |
using compact_frontier [of "cball a r"] by simp |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
400 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
401 |
corollary bounded_sphere [simp]: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
402 |
fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
403 |
shows "bounded (sphere a r)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
404 |
by (simp add: compact_imp_bounded) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
405 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
406 |
corollary closed_sphere [simp]: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
407 |
fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
408 |
shows "closed (sphere a r)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
409 |
by (simp add: compact_imp_closed) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
410 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
411 |
lemma image_add_ball [simp]: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
412 |
fixes a :: "'a::real_normed_vector" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
413 |
shows "(+) b ` ball a r = ball (a+b) r" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
414 |
apply (intro equalityI subsetI) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
415 |
apply (force simp: dist_norm) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
416 |
apply (rule_tac x="x-b" in image_eqI) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
417 |
apply (auto simp: dist_norm algebra_simps) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
418 |
done |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
419 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
420 |
lemma image_add_cball [simp]: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
421 |
fixes a :: "'a::real_normed_vector" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
422 |
shows "(+) b ` cball a r = cball (a+b) r" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
423 |
apply (intro equalityI subsetI) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
424 |
apply (force simp: dist_norm) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
425 |
apply (rule_tac x="x-b" in image_eqI) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
426 |
apply (auto simp: dist_norm algebra_simps) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
427 |
done |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
428 |
|
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
429 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
430 |
subsection%unimportant \<open>Various Lemmas on Normed Algebras\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
431 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
432 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
433 |
lemma closed_of_nat_image: "closed (of_nat ` A :: 'a::real_normed_algebra_1 set)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
434 |
by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_nat) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
435 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
436 |
lemma closed_of_int_image: "closed (of_int ` A :: 'a::real_normed_algebra_1 set)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
437 |
by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_int) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
438 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
439 |
lemma closed_Nats [simp]: "closed (\<nat> :: 'a :: real_normed_algebra_1 set)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
440 |
unfolding Nats_def by (rule closed_of_nat_image) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
441 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
442 |
lemma closed_Ints [simp]: "closed (\<int> :: 'a :: real_normed_algebra_1 set)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
443 |
unfolding Ints_def by (rule closed_of_int_image) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
444 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
445 |
lemma closed_subset_Ints: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
446 |
fixes A :: "'a :: real_normed_algebra_1 set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
447 |
assumes "A \<subseteq> \<int>" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
448 |
shows "closed A" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
449 |
proof (intro discrete_imp_closed[OF zero_less_one] ballI impI, goal_cases) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
450 |
case (1 x y) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
451 |
with assms have "x \<in> \<int>" and "y \<in> \<int>" by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
452 |
with \<open>dist y x < 1\<close> show "y = x" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
453 |
by (auto elim!: Ints_cases simp: dist_of_int) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
454 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
455 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
456 |
subsection \<open>Filters\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
457 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
458 |
definition indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter" (infixr "indirection" 70) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
459 |
where "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
460 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
461 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
462 |
subsection \<open>Trivial Limits\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
463 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
464 |
lemma trivial_limit_at_infinity: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
465 |
"\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) filter)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
466 |
unfolding trivial_limit_def eventually_at_infinity |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
467 |
apply clarsimp |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
468 |
apply (subgoal_tac "\<exists>x::'a. x \<noteq> 0", clarify) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
469 |
apply (rule_tac x="scaleR (b / norm x) x" in exI, simp) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
470 |
apply (cut_tac islimpt_UNIV [of "0::'a", unfolded islimpt_def]) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
471 |
apply (drule_tac x=UNIV in spec, simp) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
472 |
done |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
473 |
|
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
474 |
lemma at_within_ball_bot_iff: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
475 |
fixes x y :: "'a::{real_normed_vector,perfect_space}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
476 |
shows "at x within ball y r = bot \<longleftrightarrow> (r=0 \<or> x \<notin> cball y r)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
477 |
unfolding trivial_limit_within |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
478 |
apply (auto simp add:trivial_limit_within islimpt_ball ) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
479 |
by (metis le_less_trans less_eq_real_def zero_le_dist) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
480 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
481 |
|
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
482 |
subsection \<open>Limits\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
483 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
484 |
proposition Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
485 |
by (auto simp: tendsto_iff eventually_at_infinity) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
486 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
487 |
corollary Lim_at_infinityI [intro?]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
488 |
assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>B. \<forall>x. norm x \<ge> B \<longrightarrow> dist (f x) l \<le> e" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
489 |
shows "(f \<longlongrightarrow> l) at_infinity" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
490 |
apply (simp add: Lim_at_infinity, clarify) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
491 |
apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
492 |
done |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
493 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
494 |
lemma Lim_transform_within_set_eq: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
495 |
fixes a l :: "'a::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
496 |
shows "eventually (\<lambda>x. x \<in> s \<longleftrightarrow> x \<in> t) (at a) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
497 |
\<Longrightarrow> ((f \<longlongrightarrow> l) (at a within s) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within t))" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
498 |
by (force intro: Lim_transform_within_set elim: eventually_mono) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
499 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
500 |
lemma Lim_null: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
501 |
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
502 |
shows "(f \<longlongrightarrow> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) \<longlongrightarrow> 0) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
503 |
by (simp add: Lim dist_norm) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
504 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
505 |
lemma Lim_null_comparison: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
506 |
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
507 |
assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g \<longlongrightarrow> 0) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
508 |
shows "(f \<longlongrightarrow> 0) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
509 |
using assms(2) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
510 |
proof (rule metric_tendsto_imp_tendsto) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
511 |
show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
512 |
using assms(1) by (rule eventually_mono) (simp add: dist_norm) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
513 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
514 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
515 |
lemma Lim_transform_bound: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
516 |
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
517 |
and g :: "'a \<Rightarrow> 'c::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
518 |
assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
519 |
and "(g \<longlongrightarrow> 0) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
520 |
shows "(f \<longlongrightarrow> 0) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
521 |
using assms(1) tendsto_norm_zero [OF assms(2)] |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
522 |
by (rule Lim_null_comparison) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
523 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
524 |
lemma lim_null_mult_right_bounded: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
525 |
fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
526 |
assumes f: "(f \<longlongrightarrow> 0) F" and g: "eventually (\<lambda>x. norm(g x) \<le> B) F" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
527 |
shows "((\<lambda>z. f z * g z) \<longlongrightarrow> 0) F" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
528 |
proof - |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
529 |
have *: "((\<lambda>x. norm (f x) * B) \<longlongrightarrow> 0) F" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
530 |
by (simp add: f tendsto_mult_left_zero tendsto_norm_zero) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
531 |
have "((\<lambda>x. norm (f x) * norm (g x)) \<longlongrightarrow> 0) F" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
532 |
apply (rule Lim_null_comparison [OF _ *]) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
533 |
apply (simp add: eventually_mono [OF g] mult_left_mono) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
534 |
done |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
535 |
then show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
536 |
by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
537 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
538 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
539 |
lemma lim_null_mult_left_bounded: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
540 |
fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
541 |
assumes g: "eventually (\<lambda>x. norm(g x) \<le> B) F" and f: "(f \<longlongrightarrow> 0) F" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
542 |
shows "((\<lambda>z. g z * f z) \<longlongrightarrow> 0) F" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
543 |
proof - |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
544 |
have *: "((\<lambda>x. B * norm (f x)) \<longlongrightarrow> 0) F" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
545 |
by (simp add: f tendsto_mult_right_zero tendsto_norm_zero) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
546 |
have "((\<lambda>x. norm (g x) * norm (f x)) \<longlongrightarrow> 0) F" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
547 |
apply (rule Lim_null_comparison [OF _ *]) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
548 |
apply (simp add: eventually_mono [OF g] mult_right_mono) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
549 |
done |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
550 |
then show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
551 |
by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
552 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
553 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
554 |
lemma lim_null_scaleR_bounded: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
555 |
assumes f: "(f \<longlongrightarrow> 0) net" and gB: "eventually (\<lambda>a. f a = 0 \<or> norm(g a) \<le> B) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
556 |
shows "((\<lambda>n. f n *\<^sub>R g n) \<longlongrightarrow> 0) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
557 |
proof |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
558 |
fix \<epsilon>::real |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
559 |
assume "0 < \<epsilon>" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
560 |
then have B: "0 < \<epsilon> / (abs B + 1)" by simp |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
561 |
have *: "\<bar>f x\<bar> * norm (g x) < \<epsilon>" if f: "\<bar>f x\<bar> * (\<bar>B\<bar> + 1) < \<epsilon>" and g: "norm (g x) \<le> B" for x |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
562 |
proof - |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
563 |
have "\<bar>f x\<bar> * norm (g x) \<le> \<bar>f x\<bar> * B" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
564 |
by (simp add: mult_left_mono g) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
565 |
also have "\<dots> \<le> \<bar>f x\<bar> * (\<bar>B\<bar> + 1)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
566 |
by (simp add: mult_left_mono) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
567 |
also have "\<dots> < \<epsilon>" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
568 |
by (rule f) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
569 |
finally show ?thesis . |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
570 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
571 |
show "\<forall>\<^sub>F x in net. dist (f x *\<^sub>R g x) 0 < \<epsilon>" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
572 |
apply (rule eventually_mono [OF eventually_conj [OF tendstoD [OF f B] gB] ]) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
573 |
apply (auto simp: \<open>0 < \<epsilon>\<close> divide_simps * split: if_split_asm) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
574 |
done |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
575 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
576 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
577 |
lemma Lim_norm_ubound: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
578 |
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
579 |
assumes "\<not>(trivial_limit net)" "(f \<longlongrightarrow> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
580 |
shows "norm(l) \<le> e" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
581 |
using assms by (fast intro: tendsto_le tendsto_intros) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
582 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
583 |
lemma Lim_norm_lbound: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
584 |
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
585 |
assumes "\<not> trivial_limit net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
586 |
and "(f \<longlongrightarrow> l) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
587 |
and "eventually (\<lambda>x. e \<le> norm (f x)) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
588 |
shows "e \<le> norm l" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
589 |
using assms by (fast intro: tendsto_le tendsto_intros) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
590 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
591 |
text\<open>Limit under bilinear function\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
592 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
593 |
lemma Lim_bilinear: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
594 |
assumes "(f \<longlongrightarrow> l) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
595 |
and "(g \<longlongrightarrow> m) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
596 |
and "bounded_bilinear h" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
597 |
shows "((\<lambda>x. h (f x) (g x)) \<longlongrightarrow> (h l m)) net" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
598 |
using \<open>bounded_bilinear h\<close> \<open>(f \<longlongrightarrow> l) net\<close> \<open>(g \<longlongrightarrow> m) net\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
599 |
by (rule bounded_bilinear.tendsto) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
600 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
601 |
lemma Lim_at_zero: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
602 |
fixes a :: "'a::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
603 |
and l :: "'b::topological_space" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
604 |
shows "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) \<longlongrightarrow> l) (at 0)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
605 |
using LIM_offset_zero LIM_offset_zero_cancel .. |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
606 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
607 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
608 |
subsection%unimportant \<open>Limit Point of Filter\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
609 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
610 |
lemma netlimit_at_vector: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
611 |
fixes a :: "'a::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
612 |
shows "netlimit (at a) = a" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
613 |
proof (cases "\<exists>x. x \<noteq> a") |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
614 |
case True then obtain x where x: "x \<noteq> a" .. |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
615 |
have "\<not> trivial_limit (at a)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
616 |
unfolding trivial_limit_def eventually_at dist_norm |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
617 |
apply clarsimp |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
618 |
apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
619 |
apply (simp add: norm_sgn sgn_zero_iff x) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
620 |
done |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
621 |
then show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
622 |
by (rule netlimit_within [of a UNIV]) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
623 |
qed simp |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
624 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
625 |
subsection \<open>Boundedness\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
626 |
|
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
627 |
lemma continuous_on_closure_norm_le: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
628 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
629 |
assumes "continuous_on (closure s) f" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
630 |
and "\<forall>y \<in> s. norm(f y) \<le> b" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
631 |
and "x \<in> (closure s)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
632 |
shows "norm (f x) \<le> b" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
633 |
proof - |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
634 |
have *: "f ` s \<subseteq> cball 0 b" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
635 |
using assms(2)[unfolded mem_cball_0[symmetric]] by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
636 |
show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
637 |
by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
638 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
639 |
|
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
640 |
lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x \<le> b)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
641 |
apply (simp add: bounded_iff) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
642 |
apply (subgoal_tac "\<And>x (y::real). 0 < 1 + \<bar>y\<bar> \<and> (x \<le> y \<longrightarrow> x \<le> 1 + \<bar>y\<bar>)") |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
643 |
apply metis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
644 |
apply arith |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
645 |
done |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
646 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
647 |
lemma bounded_pos_less: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x < b)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
648 |
apply (simp add: bounded_pos) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
649 |
apply (safe; rule_tac x="b+1" in exI; force) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
650 |
done |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
651 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
652 |
lemma Bseq_eq_bounded: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
653 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
654 |
shows "Bseq f \<longleftrightarrow> bounded (range f)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
655 |
unfolding Bseq_def bounded_pos by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
656 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
657 |
lemma bounded_linear_image: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
658 |
assumes "bounded S" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
659 |
and "bounded_linear f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
660 |
shows "bounded (f ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
661 |
proof - |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
662 |
from assms(1) obtain b where "b > 0" and b: "\<forall>x\<in>S. norm x \<le> b" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
663 |
unfolding bounded_pos by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
664 |
from assms(2) obtain B where B: "B > 0" "\<forall>x. norm (f x) \<le> B * norm x" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
665 |
using bounded_linear.pos_bounded by (auto simp: ac_simps) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
666 |
show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
667 |
unfolding bounded_pos |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
668 |
proof (intro exI, safe) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
669 |
show "norm (f x) \<le> B * b" if "x \<in> S" for x |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
670 |
by (meson B b less_imp_le mult_left_mono order_trans that) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
671 |
qed (use \<open>b > 0\<close> \<open>B > 0\<close> in auto) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
672 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
673 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
674 |
lemma bounded_scaling: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
675 |
fixes S :: "'a::real_normed_vector set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
676 |
shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
677 |
apply (rule bounded_linear_image, assumption) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
678 |
apply (rule bounded_linear_scaleR_right) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
679 |
done |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
680 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
681 |
lemma bounded_scaleR_comp: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
682 |
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
683 |
assumes "bounded (f ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
684 |
shows "bounded ((\<lambda>x. r *\<^sub>R f x) ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
685 |
using bounded_scaling[of "f ` S" r] assms |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
686 |
by (auto simp: image_image) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
687 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
688 |
lemma bounded_translation: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
689 |
fixes S :: "'a::real_normed_vector set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
690 |
assumes "bounded S" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
691 |
shows "bounded ((\<lambda>x. a + x) ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
692 |
proof - |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
693 |
from assms obtain b where b: "b > 0" "\<forall>x\<in>S. norm x \<le> b" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
694 |
unfolding bounded_pos by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
695 |
{ |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
696 |
fix x |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
697 |
assume "x \<in> S" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
698 |
then have "norm (a + x) \<le> b + norm a" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
699 |
using norm_triangle_ineq[of a x] b by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
700 |
} |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
701 |
then show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
702 |
unfolding bounded_pos |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
703 |
using norm_ge_zero[of a] b(1) and add_strict_increasing[of b 0 "norm a"] |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
704 |
by (auto intro!: exI[of _ "b + norm a"]) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
705 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
706 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
707 |
lemma bounded_translation_minus: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
708 |
fixes S :: "'a::real_normed_vector set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
709 |
shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. x - a) ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
710 |
using bounded_translation [of S "-a"] by simp |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
711 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
712 |
lemma bounded_uminus [simp]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
713 |
fixes X :: "'a::real_normed_vector set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
714 |
shows "bounded (uminus ` X) \<longleftrightarrow> bounded X" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
715 |
by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp: add.commute norm_minus_commute) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
716 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
717 |
lemma uminus_bounded_comp [simp]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
718 |
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
719 |
shows "bounded ((\<lambda>x. - f x) ` S) \<longleftrightarrow> bounded (f ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
720 |
using bounded_uminus[of "f ` S"] |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
721 |
by (auto simp: image_image) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
722 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
723 |
lemma bounded_plus_comp: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
724 |
fixes f g::"'a \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
725 |
assumes "bounded (f ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
726 |
assumes "bounded (g ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
727 |
shows "bounded ((\<lambda>x. f x + g x) ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
728 |
proof - |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
729 |
{ |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
730 |
fix B C |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
731 |
assume "\<And>x. x\<in>S \<Longrightarrow> norm (f x) \<le> B" "\<And>x. x\<in>S \<Longrightarrow> norm (g x) \<le> C" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
732 |
then have "\<And>x. x \<in> S \<Longrightarrow> norm (f x + g x) \<le> B + C" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
733 |
by (auto intro!: norm_triangle_le add_mono) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
734 |
} then show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
735 |
using assms by (fastforce simp: bounded_iff) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
736 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
737 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
738 |
lemma bounded_plus: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
739 |
fixes S ::"'a::real_normed_vector set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
740 |
assumes "bounded S" "bounded T" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
741 |
shows "bounded ((\<lambda>(x,y). x + y) ` (S \<times> T))" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
742 |
using bounded_plus_comp [of fst "S \<times> T" snd] assms |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
743 |
by (auto simp: split_def split: if_split_asm) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
744 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
745 |
lemma bounded_minus_comp: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
746 |
"bounded (f ` S) \<Longrightarrow> bounded (g ` S) \<Longrightarrow> bounded ((\<lambda>x. f x - g x) ` S)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
747 |
for f g::"'a \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
748 |
using bounded_plus_comp[of "f" S "\<lambda>x. - g x"] |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
749 |
by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
750 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
751 |
lemma bounded_minus: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
752 |
fixes S ::"'a::real_normed_vector set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
753 |
assumes "bounded S" "bounded T" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
754 |
shows "bounded ((\<lambda>(x,y). x - y) ` (S \<times> T))" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
755 |
using bounded_minus_comp [of fst "S \<times> T" snd] assms |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
756 |
by (auto simp: split_def split: if_split_asm) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
757 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
758 |
lemma not_bounded_UNIV[simp]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
759 |
"\<not> bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
760 |
proof (auto simp: bounded_pos not_le) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
761 |
obtain x :: 'a where "x \<noteq> 0" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
762 |
using perfect_choose_dist [OF zero_less_one] by fast |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
763 |
fix b :: real |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
764 |
assume b: "b >0" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
765 |
have b1: "b +1 \<ge> 0" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
766 |
using b by simp |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
767 |
with \<open>x \<noteq> 0\<close> have "b < norm (scaleR (b + 1) (sgn x))" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
768 |
by (simp add: norm_sgn) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
769 |
then show "\<exists>x::'a. b < norm x" .. |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
770 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
771 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
772 |
corollary cobounded_imp_unbounded: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
773 |
fixes S :: "'a::{real_normed_vector, perfect_space} set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
774 |
shows "bounded (- S) \<Longrightarrow> \<not> bounded S" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
775 |
using bounded_Un [of S "-S"] by (simp add: sup_compl_top) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
776 |
|
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
777 |
subsection%unimportant\<open>Relations among convergence and absolute convergence for power series\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
778 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
779 |
lemma summable_imp_bounded: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
780 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
781 |
shows "summable f \<Longrightarrow> bounded (range f)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
782 |
by (frule summable_LIMSEQ_zero) (simp add: convergent_imp_bounded) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
783 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
784 |
lemma summable_imp_sums_bounded: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
785 |
"summable f \<Longrightarrow> bounded (range (\<lambda>n. sum f {..<n}))" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
786 |
by (auto simp: summable_def sums_def dest: convergent_imp_bounded) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
787 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
788 |
lemma power_series_conv_imp_absconv_weak: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
789 |
fixes a:: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}" and w :: 'a |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
790 |
assumes sum: "summable (\<lambda>n. a n * z ^ n)" and no: "norm w < norm z" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
791 |
shows "summable (\<lambda>n. of_real(norm(a n)) * w ^ n)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
792 |
proof - |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
793 |
obtain M where M: "\<And>x. norm (a x * z ^ x) \<le> M" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
794 |
using summable_imp_bounded [OF sum] by (force simp: bounded_iff) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
795 |
then have *: "summable (\<lambda>n. norm (a n) * norm w ^ n)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
796 |
by (rule_tac M=M in Abel_lemma) (auto simp: norm_mult norm_power intro: no) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
797 |
show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
798 |
apply (rule series_comparison_complex [of "(\<lambda>n. of_real(norm(a n) * norm w ^ n))"]) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
799 |
apply (simp only: summable_complex_of_real *) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
800 |
apply (auto simp: norm_mult norm_power) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
801 |
done |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
802 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
803 |
|
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
804 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
805 |
subsection \<open>Normed spaces with the Heine-Borel property\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
806 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
807 |
lemma not_compact_UNIV[simp]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
808 |
fixes s :: "'a::{real_normed_vector,perfect_space,heine_borel} set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
809 |
shows "\<not> compact (UNIV::'a set)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
810 |
by (simp add: compact_eq_bounded_closed) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
811 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
812 |
text\<open>Representing sets as the union of a chain of compact sets.\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
813 |
lemma closed_Union_compact_subsets: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
814 |
fixes S :: "'a::{heine_borel,real_normed_vector} set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
815 |
assumes "closed S" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
816 |
obtains F where "\<And>n. compact(F n)" "\<And>n. F n \<subseteq> S" "\<And>n. F n \<subseteq> F(Suc n)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
817 |
"(\<Union>n. F n) = S" "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n \<ge> N. K \<subseteq> F n" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
818 |
proof |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
819 |
show "compact (S \<inter> cball 0 (of_nat n))" for n |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
820 |
using assms compact_eq_bounded_closed by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
821 |
next |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
822 |
show "(\<Union>n. S \<inter> cball 0 (real n)) = S" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
823 |
by (auto simp: real_arch_simple) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
824 |
next |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
825 |
fix K :: "'a set" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
826 |
assume "compact K" "K \<subseteq> S" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
827 |
then obtain N where "K \<subseteq> cball 0 N" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
828 |
by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
829 |
then show "\<exists>N. \<forall>n\<ge>N. K \<subseteq> S \<inter> cball 0 (real n)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
830 |
by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
831 |
qed auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
832 |
|
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
833 |
subsection \<open>Intersecting chains of compact sets and the Baire property\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
834 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
835 |
proposition bounded_closed_chain: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
836 |
fixes \<F> :: "'a::heine_borel set set" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
837 |
assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
838 |
and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
839 |
shows "\<Inter>\<F> \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
840 |
proof - |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
841 |
have "B \<inter> \<Inter>\<F> \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
842 |
proof (rule compact_imp_fip) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
843 |
show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
844 |
by (simp_all add: assms compact_eq_bounded_closed) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
845 |
show "\<lbrakk>finite \<G>; \<G> \<subseteq> \<F>\<rbrakk> \<Longrightarrow> B \<inter> \<Inter>\<G> \<noteq> {}" for \<G> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
846 |
proof (induction \<G> rule: finite_induct) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
847 |
case empty |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
848 |
with assms show ?case by force |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
849 |
next |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
850 |
case (insert U \<G>) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
851 |
then have "U \<in> \<F>" and ne: "B \<inter> \<Inter>\<G> \<noteq> {}" by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
852 |
then consider "B \<subseteq> U" | "U \<subseteq> B" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
853 |
using \<open>B \<in> \<F>\<close> chain by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
854 |
then show ?case |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
855 |
proof cases |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
856 |
case 1 |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
857 |
then show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
858 |
using Int_left_commute ne by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
859 |
next |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
860 |
case 2 |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
861 |
have "U \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
862 |
using \<open>U \<in> \<F>\<close> \<open>{} \<notin> \<F>\<close> by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
863 |
moreover |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
864 |
have False if "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. x \<notin> Y" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
865 |
proof - |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
866 |
have "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. Y \<subseteq> U" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
867 |
by (metis chain contra_subsetD insert.prems insert_subset that) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
868 |
then obtain Y where "Y \<in> \<G>" "Y \<subseteq> U" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
869 |
by (metis all_not_in_conv \<open>U \<noteq> {}\<close>) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
870 |
moreover obtain x where "x \<in> \<Inter>\<G>" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
871 |
by (metis Int_emptyI ne) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
872 |
ultimately show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
873 |
by (metis Inf_lower subset_eq that) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
874 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
875 |
with 2 show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
876 |
by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
877 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
878 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
879 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
880 |
then show ?thesis by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
881 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
882 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
883 |
corollary compact_chain: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
884 |
fixes \<F> :: "'a::heine_borel set set" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
885 |
assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
886 |
"\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
887 |
shows "\<Inter> \<F> \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
888 |
proof (cases "\<F> = {}") |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
889 |
case True |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
890 |
then show ?thesis by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
891 |
next |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
892 |
case False |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
893 |
show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
894 |
by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
895 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
896 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
897 |
lemma compact_nest: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
898 |
fixes F :: "'a::linorder \<Rightarrow> 'b::heine_borel set" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
899 |
assumes F: "\<And>n. compact(F n)" "\<And>n. F n \<noteq> {}" and mono: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
900 |
shows "\<Inter>range F \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
901 |
proof - |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
902 |
have *: "\<And>S T. S \<in> range F \<and> T \<in> range F \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
903 |
by (metis mono image_iff le_cases) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
904 |
show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
905 |
apply (rule compact_chain [OF _ _ *]) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
906 |
using F apply (blast intro: dest: *)+ |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
907 |
done |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
908 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
909 |
|
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
910 |
text\<open>The Baire property of dense sets\<close> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
911 |
theorem Baire: |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
912 |
fixes S::"'a::{real_normed_vector,heine_borel} set" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
913 |
assumes "closed S" "countable \<G>" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
914 |
and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
915 |
shows "S \<subseteq> closure(\<Inter>\<G>)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
916 |
proof (cases "\<G> = {}") |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
917 |
case True |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
918 |
then show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
919 |
using closure_subset by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
920 |
next |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
921 |
let ?g = "from_nat_into \<G>" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
922 |
case False |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
923 |
then have gin: "?g n \<in> \<G>" for n |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
924 |
by (simp add: from_nat_into) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
925 |
show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
926 |
proof (clarsimp simp: closure_approachable) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
927 |
fix x and e::real |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
928 |
assume "x \<in> S" "0 < e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
929 |
obtain TF where opeF: "\<And>n. openin (subtopology euclidean S) (TF n)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
930 |
and ne: "\<And>n. TF n \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
931 |
and subg: "\<And>n. S \<inter> closure(TF n) \<subseteq> ?g n" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
932 |
and subball: "\<And>n. closure(TF n) \<subseteq> ball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
933 |
and decr: "\<And>n. TF(Suc n) \<subseteq> TF n" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
934 |
proof - |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
935 |
have *: "\<exists>Y. (openin (subtopology euclidean S) Y \<and> Y \<noteq> {} \<and> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
936 |
S \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> U" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
937 |
if opeU: "openin (subtopology euclidean S) U" and "U \<noteq> {}" and cloU: "closure U \<subseteq> ball x e" for U n |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
938 |
proof - |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
939 |
obtain T where T: "open T" "U = T \<inter> S" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
940 |
using \<open>openin (subtopology euclidean S) U\<close> by (auto simp: openin_subtopology) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
941 |
with \<open>U \<noteq> {}\<close> have "T \<inter> closure (?g n) \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
942 |
using gin ope by fastforce |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
943 |
then have "T \<inter> ?g n \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
944 |
using \<open>open T\<close> open_Int_closure_eq_empty by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
945 |
then obtain y where "y \<in> U" "y \<in> ?g n" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
946 |
using T ope [of "?g n", OF gin] by (blast dest: openin_imp_subset) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
947 |
moreover have "openin (subtopology euclidean S) (U \<inter> ?g n)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
948 |
using gin ope opeU by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
949 |
ultimately obtain d where U: "U \<inter> ?g n \<subseteq> S" and "d > 0" and d: "ball y d \<inter> S \<subseteq> U \<inter> ?g n" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
950 |
by (force simp: openin_contains_ball) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
951 |
show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
952 |
proof (intro exI conjI) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
953 |
show "openin (subtopology euclidean S) (S \<inter> ball y (d/2))" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
954 |
by (simp add: openin_open_Int) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
955 |
show "S \<inter> ball y (d/2) \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
956 |
using \<open>0 < d\<close> \<open>y \<in> U\<close> opeU openin_imp_subset by fastforce |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
957 |
have "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> closure (ball y (d/2))" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
958 |
using closure_mono by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
959 |
also have "... \<subseteq> ?g n" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
960 |
using \<open>d > 0\<close> d by force |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
961 |
finally show "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> ?g n" . |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
962 |
have "closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> ball y d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
963 |
proof - |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
964 |
have "closure (ball y (d/2)) \<subseteq> ball y d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
965 |
using \<open>d > 0\<close> by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
966 |
then have "closure (S \<inter> ball y (d/2)) \<subseteq> ball y d" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
967 |
by (meson closure_mono inf.cobounded2 subset_trans) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
968 |
then show ?thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
969 |
by (simp add: \<open>closed S\<close> closure_minimal) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
970 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
971 |
also have "... \<subseteq> ball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
972 |
using cloU closure_subset d by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
973 |
finally show "closure (S \<inter> ball y (d/2)) \<subseteq> ball x e" . |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
974 |
show "S \<inter> ball y (d/2) \<subseteq> U" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
975 |
using ball_divide_subset_numeral d by blast |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
976 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
977 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
978 |
let ?\<Phi> = "\<lambda>n X. openin (subtopology euclidean S) X \<and> X \<noteq> {} \<and> |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
979 |
S \<inter> closure X \<subseteq> ?g n \<and> closure X \<subseteq> ball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
980 |
have "closure (S \<inter> ball x (e / 2)) \<subseteq> closure(ball x (e/2))" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
981 |
by (simp add: closure_mono) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
982 |
also have "... \<subseteq> ball x e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
983 |
using \<open>e > 0\<close> by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
984 |
finally have "closure (S \<inter> ball x (e / 2)) \<subseteq> ball x e" . |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
985 |
moreover have"openin (subtopology euclidean S) (S \<inter> ball x (e / 2))" "S \<inter> ball x (e / 2) \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
986 |
using \<open>0 < e\<close> \<open>x \<in> S\<close> by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
987 |
ultimately obtain Y where Y: "?\<Phi> 0 Y \<and> Y \<subseteq> S \<inter> ball x (e / 2)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
988 |
using * [of "S \<inter> ball x (e/2)" 0] by metis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
989 |
show thesis |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
990 |
proof (rule exE [OF dependent_nat_choice [of ?\<Phi> "\<lambda>n X Y. Y \<subseteq> X"]]) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
991 |
show "\<exists>x. ?\<Phi> 0 x" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
992 |
using Y by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
993 |
show "\<exists>Y. ?\<Phi> (Suc n) Y \<and> Y \<subseteq> X" if "?\<Phi> n X" for X n |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
994 |
using that by (blast intro: *) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
995 |
qed (use that in metis) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
996 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
997 |
have "(\<Inter>n. S \<inter> closure (TF n)) \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
998 |
proof (rule compact_nest) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
999 |
show "\<And>n. compact (S \<inter> closure (TF n))" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1000 |
by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF \<open>closed S\<close>]) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1001 |
show "\<And>n. S \<inter> closure (TF n) \<noteq> {}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1002 |
by (metis Int_absorb1 opeF \<open>closed S\<close> closure_eq_empty closure_minimal ne openin_imp_subset) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1003 |
show "\<And>m n. m \<le> n \<Longrightarrow> S \<inter> closure (TF n) \<subseteq> S \<inter> closure (TF m)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1004 |
by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1005 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1006 |
moreover have "(\<Inter>n. S \<inter> closure (TF n)) \<subseteq> {y \<in> \<Inter>\<G>. dist y x < e}" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1007 |
proof (clarsimp, intro conjI) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1008 |
fix y |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1009 |
assume "y \<in> S" and y: "\<forall>n. y \<in> closure (TF n)" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1010 |
then show "\<forall>T\<in>\<G>. y \<in> T" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1011 |
by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] set_mp subg) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1012 |
show "dist y x < e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1013 |
by (metis y dist_commute mem_ball subball subsetCE) |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1014 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1015 |
ultimately show "\<exists>y \<in> \<Inter>\<G>. dist y x < e" |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1016 |
by auto |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1017 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1018 |
qed |
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset
|
1019 |
|
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1020 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1021 |
subsection \<open>Continuity\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1022 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1023 |
subsubsection%unimportant \<open>Structural rules for uniform continuity\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1024 |
|
69613
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1025 |
lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1026 |
fixes g :: "_::metric_space \<Rightarrow> _" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1027 |
assumes "uniformly_continuous_on s g" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1028 |
shows "uniformly_continuous_on s (\<lambda>x. f (g x))" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1029 |
using assms unfolding uniformly_continuous_on_sequentially |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1030 |
unfolding dist_norm tendsto_norm_zero_iff diff[symmetric] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1031 |
by (auto intro: tendsto_zero) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1032 |
|
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1033 |
lemma uniformly_continuous_on_dist[continuous_intros]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1034 |
fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1035 |
assumes "uniformly_continuous_on s f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1036 |
and "uniformly_continuous_on s g" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1037 |
shows "uniformly_continuous_on s (\<lambda>x. dist (f x) (g x))" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1038 |
proof - |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1039 |
{ |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1040 |
fix a b c d :: 'b |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1041 |
have "\<bar>dist a b - dist c d\<bar> \<le> dist a c + dist b d" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1042 |
using dist_triangle2 [of a b c] dist_triangle2 [of b c d] |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1043 |
using dist_triangle3 [of c d a] dist_triangle [of a d b] |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1044 |
by arith |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1045 |
} note le = this |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1046 |
{ |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1047 |
fix x y |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1048 |
assume f: "(\<lambda>n. dist (f (x n)) (f (y n))) \<longlonglongrightarrow> 0" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1049 |
assume g: "(\<lambda>n. dist (g (x n)) (g (y n))) \<longlonglongrightarrow> 0" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1050 |
have "(\<lambda>n. \<bar>dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))\<bar>) \<longlonglongrightarrow> 0" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1051 |
by (rule Lim_transform_bound [OF _ tendsto_add_zero [OF f g]], |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1052 |
simp add: le) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1053 |
} |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1054 |
then show ?thesis |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1055 |
using assms unfolding uniformly_continuous_on_sequentially |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1056 |
unfolding dist_real_def by simp |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1057 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1058 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1059 |
lemma uniformly_continuous_on_norm[continuous_intros]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1060 |
fixes f :: "'a :: metric_space \<Rightarrow> 'b :: real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1061 |
assumes "uniformly_continuous_on s f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1062 |
shows "uniformly_continuous_on s (\<lambda>x. norm (f x))" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1063 |
unfolding norm_conv_dist using assms |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1064 |
by (intro uniformly_continuous_on_dist uniformly_continuous_on_const) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1065 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1066 |
lemma uniformly_continuous_on_cmul[continuous_intros]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1067 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1068 |
assumes "uniformly_continuous_on s f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1069 |
shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1070 |
using bounded_linear_scaleR_right assms |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1071 |
by (rule bounded_linear.uniformly_continuous_on) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1072 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1073 |
lemma dist_minus: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1074 |
fixes x y :: "'a::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1075 |
shows "dist (- x) (- y) = dist x y" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1076 |
unfolding dist_norm minus_diff_minus norm_minus_cancel .. |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1077 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1078 |
lemma uniformly_continuous_on_minus[continuous_intros]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1079 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1080 |
shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. - f x)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1081 |
unfolding uniformly_continuous_on_def dist_minus . |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1082 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1083 |
lemma uniformly_continuous_on_add[continuous_intros]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1084 |
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1085 |
assumes "uniformly_continuous_on s f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1086 |
and "uniformly_continuous_on s g" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1087 |
shows "uniformly_continuous_on s (\<lambda>x. f x + g x)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1088 |
using assms |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1089 |
unfolding uniformly_continuous_on_sequentially |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1090 |
unfolding dist_norm tendsto_norm_zero_iff add_diff_add |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1091 |
by (auto intro: tendsto_add_zero) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1092 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1093 |
lemma uniformly_continuous_on_diff[continuous_intros]: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1094 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1095 |
assumes "uniformly_continuous_on s f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1096 |
and "uniformly_continuous_on s g" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1097 |
shows "uniformly_continuous_on s (\<lambda>x. f x - g x)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1098 |
using assms uniformly_continuous_on_add [of s f "- g"] |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1099 |
by (simp add: fun_Compl_def uniformly_continuous_on_minus) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1100 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1101 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1102 |
subsection%unimportant \<open>Topological properties of linear functions\<close> |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1103 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1104 |
lemma linear_lim_0: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1105 |
assumes "bounded_linear f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1106 |
shows "(f \<longlongrightarrow> 0) (at (0))" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1107 |
proof - |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1108 |
interpret f: bounded_linear f by fact |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1109 |
have "(f \<longlongrightarrow> f 0) (at 0)" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1110 |
using tendsto_ident_at by (rule f.tendsto) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1111 |
then show ?thesis unfolding f.zero . |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1112 |
qed |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1113 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1114 |
lemma linear_continuous_at: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1115 |
assumes "bounded_linear f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1116 |
shows "continuous (at a) f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1117 |
unfolding continuous_at using assms |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1118 |
apply (rule bounded_linear.tendsto) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1119 |
apply (rule tendsto_ident_at) |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1120 |
done |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1121 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1122 |
lemma linear_continuous_within: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1123 |
"bounded_linear f \<Longrightarrow> continuous (at x within s) f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1124 |
using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1125 |
|
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1126 |
lemma linear_continuous_on: |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1127 |
"bounded_linear f \<Longrightarrow> continuous_on s f" |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1128 |
using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto |
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1129 |
|
69613
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1130 |
subsection%unimportant \<open>Arithmetic Preserves Topological Properties\<close> |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1131 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1132 |
lemma open_scaling[intro]: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1133 |
fixes s :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1134 |
assumes "c \<noteq> 0" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1135 |
and "open s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1136 |
shows "open((\<lambda>x. c *\<^sub>R x) ` s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1137 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1138 |
{ |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1139 |
fix x |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1140 |
assume "x \<in> s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1141 |
then obtain e where "e>0" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1142 |
and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1143 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1144 |
have "e * \<bar>c\<bar> > 0" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1145 |
using assms(1)[unfolded zero_less_abs_iff[symmetric]] \<open>e>0\<close> by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1146 |
moreover |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1147 |
{ |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1148 |
fix y |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1149 |
assume "dist y (c *\<^sub>R x) < e * \<bar>c\<bar>" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1150 |
then have "norm ((1 / c) *\<^sub>R y - x) < e" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1151 |
unfolding dist_norm |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1152 |
using norm_scaleR[of c "(1 / c) *\<^sub>R y - x", unfolded scaleR_right_diff_distrib, unfolded scaleR_scaleR] assms(1) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1153 |
assms(1)[unfolded zero_less_abs_iff[symmetric]] by (simp del:zero_less_abs_iff) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1154 |
then have "y \<in> (*\<^sub>R) c ` s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1155 |
using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "(*\<^sub>R) c"] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1156 |
using e[THEN spec[where x="(1 / c) *\<^sub>R y"]] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1157 |
using assms(1) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1158 |
unfolding dist_norm scaleR_scaleR |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1159 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1160 |
} |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1161 |
ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> (*\<^sub>R) c ` s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1162 |
apply (rule_tac x="e * \<bar>c\<bar>" in exI, auto) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1163 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1164 |
} |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1165 |
then show ?thesis unfolding open_dist by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1166 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1167 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1168 |
lemma minus_image_eq_vimage: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1169 |
fixes A :: "'a::ab_group_add set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1170 |
shows "(\<lambda>x. - x) ` A = (\<lambda>x. - x) -` A" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1171 |
by (auto intro!: image_eqI [where f="\<lambda>x. - x"]) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1172 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1173 |
lemma open_negations: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1174 |
fixes S :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1175 |
shows "open S \<Longrightarrow> open ((\<lambda>x. - x) ` S)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1176 |
using open_scaling [of "- 1" S] by simp |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1177 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1178 |
lemma open_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1179 |
fixes S :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1180 |
assumes "open S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1181 |
shows "open((\<lambda>x. a + x) ` S)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1182 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1183 |
{ |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1184 |
fix x |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1185 |
have "continuous (at x) (\<lambda>x. x - a)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1186 |
by (intro continuous_diff continuous_ident continuous_const) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1187 |
} |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1188 |
moreover have "{x. x - a \<in> S} = (+) a ` S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1189 |
by force |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1190 |
ultimately show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1191 |
by (metis assms continuous_open_vimage vimage_def) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1192 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1193 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1194 |
lemma open_neg_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1195 |
fixes s :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1196 |
assumes "open s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1197 |
shows "open((\<lambda>x. a - x) ` s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1198 |
using open_translation[OF open_negations[OF assms], of a] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1199 |
by (auto simp: image_image) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1200 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1201 |
lemma open_affinity: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1202 |
fixes S :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1203 |
assumes "open S" "c \<noteq> 0" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1204 |
shows "open ((\<lambda>x. a + c *\<^sub>R x) ` S)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1205 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1206 |
have *: "(\<lambda>x. a + c *\<^sub>R x) = (\<lambda>x. a + x) \<circ> (\<lambda>x. c *\<^sub>R x)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1207 |
unfolding o_def .. |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1208 |
have "(+) a ` (*\<^sub>R) c ` S = ((+) a \<circ> (*\<^sub>R) c) ` S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1209 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1210 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1211 |
using assms open_translation[of "(*\<^sub>R) c ` S" a] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1212 |
unfolding * |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1213 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1214 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1215 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1216 |
lemma interior_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1217 |
fixes S :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1218 |
shows "interior ((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (interior S)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1219 |
proof (rule set_eqI, rule) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1220 |
fix x |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1221 |
assume "x \<in> interior ((+) a ` S)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1222 |
then obtain e where "e > 0" and e: "ball x e \<subseteq> (+) a ` S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1223 |
unfolding mem_interior by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1224 |
then have "ball (x - a) e \<subseteq> S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1225 |
unfolding subset_eq Ball_def mem_ball dist_norm |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1226 |
by (auto simp: diff_diff_eq) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1227 |
then show "x \<in> (+) a ` interior S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1228 |
unfolding image_iff |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1229 |
apply (rule_tac x="x - a" in bexI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1230 |
unfolding mem_interior |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1231 |
using \<open>e > 0\<close> |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1232 |
apply auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1233 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1234 |
next |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1235 |
fix x |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1236 |
assume "x \<in> (+) a ` interior S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1237 |
then obtain y e where "e > 0" and e: "ball y e \<subseteq> S" and y: "x = a + y" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1238 |
unfolding image_iff Bex_def mem_interior by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1239 |
{ |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1240 |
fix z |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1241 |
have *: "a + y - z = y + a - z" by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1242 |
assume "z \<in> ball x e" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1243 |
then have "z - a \<in> S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1244 |
using e[unfolded subset_eq, THEN bspec[where x="z - a"]] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1245 |
unfolding mem_ball dist_norm y group_add_class.diff_diff_eq2 * |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1246 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1247 |
then have "z \<in> (+) a ` S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1248 |
unfolding image_iff by (auto intro!: bexI[where x="z - a"]) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1249 |
} |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1250 |
then have "ball x e \<subseteq> (+) a ` S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1251 |
unfolding subset_eq by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1252 |
then show "x \<in> interior ((+) a ` S)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1253 |
unfolding mem_interior using \<open>e > 0\<close> by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1254 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1255 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1256 |
lemma compact_scaling: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1257 |
fixes s :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1258 |
assumes "compact s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1259 |
shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1260 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1261 |
let ?f = "\<lambda>x. scaleR c x" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1262 |
have *: "bounded_linear ?f" by (rule bounded_linear_scaleR_right) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1263 |
show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1264 |
using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1265 |
using linear_continuous_at[OF *] assms |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1266 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1267 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1268 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1269 |
lemma compact_negations: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1270 |
fixes s :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1271 |
assumes "compact s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1272 |
shows "compact ((\<lambda>x. - x) ` s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1273 |
using compact_scaling [OF assms, of "- 1"] by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1274 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1275 |
lemma compact_sums: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1276 |
fixes s t :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1277 |
assumes "compact s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1278 |
and "compact t" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1279 |
shows "compact {x + y | x y. x \<in> s \<and> y \<in> t}" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1280 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1281 |
have *: "{x + y | x y. x \<in> s \<and> y \<in> t} = (\<lambda>z. fst z + snd z) ` (s \<times> t)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1282 |
apply auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1283 |
unfolding image_iff |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1284 |
apply (rule_tac x="(xa, y)" in bexI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1285 |
apply auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1286 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1287 |
have "continuous_on (s \<times> t) (\<lambda>z. fst z + snd z)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1288 |
unfolding continuous_on by (rule ballI) (intro tendsto_intros) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1289 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1290 |
unfolding * using compact_continuous_image compact_Times [OF assms] by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1291 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1292 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1293 |
lemma compact_differences: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1294 |
fixes s t :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1295 |
assumes "compact s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1296 |
and "compact t" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1297 |
shows "compact {x - y | x y. x \<in> s \<and> y \<in> t}" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1298 |
proof- |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1299 |
have "{x - y | x y. x\<in>s \<and> y \<in> t} = {x + y | x y. x \<in> s \<and> y \<in> (uminus ` t)}" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1300 |
apply auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1301 |
apply (rule_tac x= xa in exI, auto) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1302 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1303 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1304 |
using compact_sums[OF assms(1) compact_negations[OF assms(2)]] by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1305 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1306 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1307 |
lemma compact_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1308 |
fixes s :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1309 |
assumes "compact s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1310 |
shows "compact ((\<lambda>x. a + x) ` s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1311 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1312 |
have "{x + y |x y. x \<in> s \<and> y \<in> {a}} = (\<lambda>x. a + x) ` s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1313 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1314 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1315 |
using compact_sums[OF assms compact_sing[of a]] by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1316 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1317 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1318 |
lemma compact_affinity: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1319 |
fixes s :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1320 |
assumes "compact s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1321 |
shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1322 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1323 |
have "(+) a ` (*\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1324 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1325 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1326 |
using compact_translation[OF compact_scaling[OF assms], of a c] by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1327 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1328 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1329 |
lemma closed_scaling: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1330 |
fixes S :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1331 |
assumes "closed S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1332 |
shows "closed ((\<lambda>x. c *\<^sub>R x) ` S)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1333 |
proof (cases "c = 0") |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1334 |
case True then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1335 |
by (auto simp: image_constant_conv) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1336 |
next |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1337 |
case False |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1338 |
from assms have "closed ((\<lambda>x. inverse c *\<^sub>R x) -` S)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1339 |
by (simp add: continuous_closed_vimage) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1340 |
also have "(\<lambda>x. inverse c *\<^sub>R x) -` S = (\<lambda>x. c *\<^sub>R x) ` S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1341 |
using \<open>c \<noteq> 0\<close> by (auto elim: image_eqI [rotated]) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1342 |
finally show ?thesis . |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1343 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1344 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1345 |
lemma closed_negations: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1346 |
fixes S :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1347 |
assumes "closed S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1348 |
shows "closed ((\<lambda>x. -x) ` S)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1349 |
using closed_scaling[OF assms, of "- 1"] by simp |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1350 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1351 |
lemma compact_closed_sums: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1352 |
fixes S :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1353 |
assumes "compact S" and "closed T" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1354 |
shows "closed (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1355 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1356 |
let ?S = "{x + y |x y. x \<in> S \<and> y \<in> T}" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1357 |
{ |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1358 |
fix x l |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1359 |
assume as: "\<forall>n. x n \<in> ?S" "(x \<longlongrightarrow> l) sequentially" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1360 |
from as(1) obtain f where f: "\<forall>n. x n = fst (f n) + snd (f n)" "\<forall>n. fst (f n) \<in> S" "\<forall>n. snd (f n) \<in> T" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1361 |
using choice[of "\<lambda>n y. x n = (fst y) + (snd y) \<and> fst y \<in> S \<and> snd y \<in> T"] by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1362 |
obtain l' r where "l'\<in>S" and r: "strict_mono r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) \<longlongrightarrow> l') sequentially" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1363 |
using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1364 |
have "((\<lambda>n. snd (f (r n))) \<longlongrightarrow> l - l') sequentially" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1365 |
using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1366 |
unfolding o_def |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1367 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1368 |
then have "l - l' \<in> T" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1369 |
using assms(2)[unfolded closed_sequential_limits, |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1370 |
THEN spec[where x="\<lambda> n. snd (f (r n))"], |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1371 |
THEN spec[where x="l - l'"]] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1372 |
using f(3) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1373 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1374 |
then have "l \<in> ?S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1375 |
using \<open>l' \<in> S\<close> |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1376 |
apply auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1377 |
apply (rule_tac x=l' in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1378 |
apply (rule_tac x="l - l'" in exI, auto) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1379 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1380 |
} |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1381 |
moreover have "?S = (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1382 |
by force |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1383 |
ultimately show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1384 |
unfolding closed_sequential_limits |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1385 |
by (metis (no_types, lifting)) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1386 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1387 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1388 |
lemma closed_compact_sums: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1389 |
fixes S T :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1390 |
assumes "closed S" "compact T" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1391 |
shows "closed (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1392 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1393 |
have "(\<Union>x\<in> T. \<Union>y \<in> S. {x + y}) = (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1394 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1395 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1396 |
using compact_closed_sums[OF assms(2,1)] by simp |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1397 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1398 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1399 |
lemma compact_closed_differences: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1400 |
fixes S T :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1401 |
assumes "compact S" "closed T" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1402 |
shows "closed (\<Union>x\<in> S. \<Union>y \<in> T. {x - y})" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1403 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1404 |
have "(\<Union>x\<in> S. \<Union>y \<in> uminus ` T. {x + y}) = (\<Union>x\<in> S. \<Union>y \<in> T. {x - y})" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1405 |
by force |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1406 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1407 |
using compact_closed_sums[OF assms(1) closed_negations[OF assms(2)]] by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1408 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1409 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1410 |
lemma closed_compact_differences: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1411 |
fixes S T :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1412 |
assumes "closed S" "compact T" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1413 |
shows "closed (\<Union>x\<in> S. \<Union>y \<in> T. {x - y})" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1414 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1415 |
have "(\<Union>x\<in> S. \<Union>y \<in> uminus ` T. {x + y}) = {x - y |x y. x \<in> S \<and> y \<in> T}" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1416 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1417 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1418 |
using closed_compact_sums[OF assms(1) compact_negations[OF assms(2)]] by simp |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1419 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1420 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1421 |
lemma closed_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1422 |
fixes a :: "'a::real_normed_vector" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1423 |
assumes "closed S" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1424 |
shows "closed ((\<lambda>x. a + x) ` S)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1425 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1426 |
have "(\<Union>x\<in> {a}. \<Union>y \<in> S. {x + y}) = ((+) a ` S)" by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1427 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1428 |
using compact_closed_sums[OF compact_sing[of a] assms] by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1429 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1430 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1431 |
lemma closure_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1432 |
fixes a :: "'a::real_normed_vector" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1433 |
shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1434 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1435 |
have *: "(+) a ` (- s) = - (+) a ` s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1436 |
by (auto intro!: image_eqI[where x="x - a" for x]) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1437 |
show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1438 |
unfolding closure_interior translation_Compl |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1439 |
using interior_translation[of a "- s"] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1440 |
unfolding * |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1441 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1442 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1443 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1444 |
lemma frontier_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1445 |
fixes a :: "'a::real_normed_vector" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1446 |
shows "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1447 |
unfolding frontier_def translation_diff interior_translation closure_translation |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1448 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1449 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1450 |
lemma sphere_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1451 |
fixes a :: "'n::real_normed_vector" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1452 |
shows "sphere (a+c) r = (+) a ` sphere c r" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1453 |
by (auto simp: dist_norm algebra_simps intro!: image_eqI[where x="x - a" for x]) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1454 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1455 |
lemma cball_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1456 |
fixes a :: "'n::real_normed_vector" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1457 |
shows "cball (a+c) r = (+) a ` cball c r" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1458 |
by (auto simp: dist_norm algebra_simps intro!: image_eqI[where x="x - a" for x]) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1459 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1460 |
lemma ball_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1461 |
fixes a :: "'n::real_normed_vector" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1462 |
shows "ball (a+c) r = (+) a ` ball c r" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1463 |
by (auto simp: dist_norm algebra_simps intro!: image_eqI[where x="x - a" for x]) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1464 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1465 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1466 |
subsection%unimportant\<open>Homeomorphisms\<close> |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1467 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1468 |
lemma homeomorphic_scaling: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1469 |
fixes s :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1470 |
assumes "c \<noteq> 0" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1471 |
shows "s homeomorphic ((\<lambda>x. c *\<^sub>R x) ` s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1472 |
unfolding homeomorphic_minimal |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1473 |
apply (rule_tac x="\<lambda>x. c *\<^sub>R x" in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1474 |
apply (rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1475 |
using assms |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1476 |
apply (auto simp: continuous_intros) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1477 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1478 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1479 |
lemma homeomorphic_translation: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1480 |
fixes s :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1481 |
shows "s homeomorphic ((\<lambda>x. a + x) ` s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1482 |
unfolding homeomorphic_minimal |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1483 |
apply (rule_tac x="\<lambda>x. a + x" in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1484 |
apply (rule_tac x="\<lambda>x. -a + x" in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1485 |
using continuous_on_add [OF continuous_on_const continuous_on_id, of s a] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1486 |
continuous_on_add [OF continuous_on_const continuous_on_id, of "plus a ` s" "- a"] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1487 |
apply auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1488 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1489 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1490 |
lemma homeomorphic_affinity: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1491 |
fixes s :: "'a::real_normed_vector set" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1492 |
assumes "c \<noteq> 0" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1493 |
shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1494 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1495 |
have *: "(+) a ` (*\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1496 |
show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1497 |
using homeomorphic_trans |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1498 |
using homeomorphic_scaling[OF assms, of s] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1499 |
using homeomorphic_translation[of "(\<lambda>x. c *\<^sub>R x) ` s" a] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1500 |
unfolding * |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1501 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1502 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1503 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1504 |
lemma homeomorphic_balls: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1505 |
fixes a b ::"'a::real_normed_vector" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1506 |
assumes "0 < d" "0 < e" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1507 |
shows "(ball a d) homeomorphic (ball b e)" (is ?th) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1508 |
and "(cball a d) homeomorphic (cball b e)" (is ?cth) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1509 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1510 |
show ?th unfolding homeomorphic_minimal |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1511 |
apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1512 |
apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1513 |
using assms |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1514 |
apply (auto intro!: continuous_intros |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1515 |
simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1516 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1517 |
show ?cth unfolding homeomorphic_minimal |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1518 |
apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1519 |
apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1520 |
using assms |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1521 |
apply (auto intro!: continuous_intros |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1522 |
simp: dist_commute dist_norm pos_divide_le_eq mult_strict_left_mono) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1523 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1524 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1525 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1526 |
lemma homeomorphic_spheres: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1527 |
fixes a b ::"'a::real_normed_vector" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1528 |
assumes "0 < d" "0 < e" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1529 |
shows "(sphere a d) homeomorphic (sphere b e)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1530 |
unfolding homeomorphic_minimal |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1531 |
apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1532 |
apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1533 |
using assms |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1534 |
apply (auto intro!: continuous_intros |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1535 |
simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1536 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1537 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1538 |
lemma homeomorphic_ball01_UNIV: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1539 |
"ball (0::'a::real_normed_vector) 1 homeomorphic (UNIV:: 'a set)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1540 |
(is "?B homeomorphic ?U") |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1541 |
proof |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1542 |
have "x \<in> (\<lambda>z. z /\<^sub>R (1 - norm z)) ` ball 0 1" for x::'a |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1543 |
apply (rule_tac x="x /\<^sub>R (1 + norm x)" in image_eqI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1544 |
apply (auto simp: divide_simps) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1545 |
using norm_ge_zero [of x] apply linarith+ |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1546 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1547 |
then show "(\<lambda>z::'a. z /\<^sub>R (1 - norm z)) ` ?B = ?U" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1548 |
by blast |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1549 |
have "x \<in> range (\<lambda>z. (1 / (1 + norm z)) *\<^sub>R z)" if "norm x < 1" for x::'a |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1550 |
apply (rule_tac x="x /\<^sub>R (1 - norm x)" in image_eqI) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1551 |
using that apply (auto simp: divide_simps) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1552 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1553 |
then show "(\<lambda>z::'a. z /\<^sub>R (1 + norm z)) ` ?U = ?B" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1554 |
by (force simp: divide_simps dest: add_less_zeroD) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1555 |
show "continuous_on (ball 0 1) (\<lambda>z. z /\<^sub>R (1 - norm z))" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1556 |
by (rule continuous_intros | force)+ |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1557 |
show "continuous_on UNIV (\<lambda>z. z /\<^sub>R (1 + norm z))" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1558 |
apply (intro continuous_intros) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1559 |
apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1560 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1561 |
show "\<And>x. x \<in> ball 0 1 \<Longrightarrow> |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1562 |
x /\<^sub>R (1 - norm x) /\<^sub>R (1 + norm (x /\<^sub>R (1 - norm x))) = x" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1563 |
by (auto simp: divide_simps) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1564 |
show "\<And>y. y /\<^sub>R (1 + norm y) /\<^sub>R (1 - norm (y /\<^sub>R (1 + norm y))) = y" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1565 |
apply (auto simp: divide_simps) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1566 |
apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1567 |
done |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1568 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1569 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1570 |
proposition homeomorphic_ball_UNIV: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1571 |
fixes a ::"'a::real_normed_vector" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1572 |
assumes "0 < r" shows "ball a r homeomorphic (UNIV:: 'a set)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1573 |
using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1574 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1575 |
|
69615
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1576 |
subsection%unimportant \<open>Discrete\<close> |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1577 |
|
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1578 |
lemma finite_implies_discrete: |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1579 |
fixes S :: "'a::topological_space set" |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1580 |
assumes "finite (f ` S)" |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1581 |
shows "(\<forall>x \<in> S. \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))" |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1582 |
proof - |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1583 |
have "\<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> S" for x |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1584 |
proof (cases "f ` S - {f x} = {}") |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1585 |
case True |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1586 |
with zero_less_numeral show ?thesis |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1587 |
by (fastforce simp add: Set.image_subset_iff cong: conj_cong) |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1588 |
next |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1589 |
case False |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1590 |
then obtain z where z: "z \<in> S" "f z \<noteq> f x" |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1591 |
by blast |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1592 |
have finn: "finite {norm (z - f x) |z. z \<in> f ` S - {f x}}" |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1593 |
using assms by simp |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1594 |
then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` S - {f x}}" |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1595 |
apply (rule finite_imp_less_Inf) |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1596 |
using z apply force+ |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1597 |
done |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1598 |
show ?thesis |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1599 |
by (force intro!: * cInf_le_finite [OF finn]) |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1600 |
qed |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1601 |
with assms show ?thesis |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1602 |
by blast |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1603 |
qed |
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1604 |
|
e502cd4d7062
moved material from Connected.thy to more appropriate places
immler
parents:
69613
diff
changeset
|
1605 |
|
69613
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1606 |
subsection%unimportant \<open>Completeness of "Isometry" (up to constant bounds)\<close> |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1607 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1608 |
lemma cauchy_isometric:\<comment> \<open>TODO: rename lemma to \<open>Cauchy_isometric\<close>\<close> |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1609 |
assumes e: "e > 0" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1610 |
and s: "subspace s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1611 |
and f: "bounded_linear f" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1612 |
and normf: "\<forall>x\<in>s. norm (f x) \<ge> e * norm x" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1613 |
and xs: "\<forall>n. x n \<in> s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1614 |
and cf: "Cauchy (f \<circ> x)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1615 |
shows "Cauchy x" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1616 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1617 |
interpret f: bounded_linear f by fact |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1618 |
have "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" if "d > 0" for d :: real |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1619 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1620 |
from that obtain N where N: "\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1621 |
using cf[unfolded Cauchy_def o_def dist_norm, THEN spec[where x="e*d"]] e |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1622 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1623 |
have "norm (x n - x N) < d" if "n \<ge> N" for n |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1624 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1625 |
have "e * norm (x n - x N) \<le> norm (f (x n - x N))" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1626 |
using subspace_diff[OF s, of "x n" "x N"] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1627 |
using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1628 |
using normf[THEN bspec[where x="x n - x N"]] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1629 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1630 |
also have "norm (f (x n - x N)) < e * d" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1631 |
using \<open>N \<le> n\<close> N unfolding f.diff[symmetric] by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1632 |
finally show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1633 |
using \<open>e>0\<close> by simp |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1634 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1635 |
then show ?thesis by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1636 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1637 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1638 |
by (simp add: Cauchy_altdef2 dist_norm) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1639 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1640 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1641 |
lemma complete_isometric_image: |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1642 |
assumes "0 < e" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1643 |
and s: "subspace s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1644 |
and f: "bounded_linear f" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1645 |
and normf: "\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1646 |
and cs: "complete s" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1647 |
shows "complete (f ` s)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1648 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1649 |
have "\<exists>l\<in>f ` s. (g \<longlongrightarrow> l) sequentially" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1650 |
if as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"Cauchy g" for g |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1651 |
proof - |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1652 |
from that obtain x where "\<forall>n. x n \<in> s \<and> g n = f (x n)" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1653 |
using choice[of "\<lambda> n xa. xa \<in> s \<and> g n = f xa"] by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1654 |
then have x: "\<forall>n. x n \<in> s" "\<forall>n. g n = f (x n)" by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1655 |
then have "f \<circ> x = g" by (simp add: fun_eq_iff) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1656 |
then obtain l where "l\<in>s" and l:"(x \<longlongrightarrow> l) sequentially" |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1657 |
using cs[unfolded complete_def, THEN spec[where x=x]] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1658 |
using cauchy_isometric[OF \<open>0 < e\<close> s f normf] and cfg and x(1) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1659 |
by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1660 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1661 |
using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l] |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1662 |
by (auto simp: \<open>f \<circ> x = g\<close>) |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1663 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1664 |
then show ?thesis |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1665 |
unfolding complete_def by auto |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1666 |
qed |
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1667 |
|
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
|
1668 |
|
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset
|
1669 |
end |