author  paulson <lp15@cam.ac.uk> 
Thu, 12 Sep 2019 15:32:39 +0100  
changeset 70690  8518a750f7bb 
parent 70688  3d894e1cfc75 
child 70724  65371451fde8 
permissions  rwrr 
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 
"HOLLibrary.FuncSet" 
70690  12 
Elementary_Metric_Spaces Linear_Algebra 
69617  13 
Connected 
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

14 
begin 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

15 

70136  16 
subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas Combining Imports\<close> 
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

17 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

18 
lemma countable_PiE: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

19 
"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

20 
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

21 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

22 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

23 
lemma open_sums: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

24 
fixes T :: "('b::real_normed_vector) set" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

25 
assumes "open S \<or> open T" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

26 
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

27 
using assms 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

28 
proof 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

29 
assume S: "open S" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

30 
show ?thesis 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

31 
proof (clarsimp simp: open_dist) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

32 
fix x y 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

33 
assume "x \<in> S" "y \<in> T" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

34 
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

35 
by (auto simp: open_dist) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

36 
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

37 
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

38 
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

39 
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

40 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

41 
next 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

42 
assume T: "open T" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

43 
show ?thesis 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

44 
proof (clarsimp simp: open_dist) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

45 
fix x y 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

46 
assume "x \<in> S" "y \<in> T" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

47 
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

48 
by (auto simp: open_dist) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

49 
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

50 
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

51 
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

52 
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

53 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

54 
qed 
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 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

57 
subsection \<open>Support\<close> 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

58 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

59 
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

60 
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

61 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

62 
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

63 
by (simp add: support_on_def) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

64 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

65 
lemma support_on_simps[simp]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

66 
"support_on {} f = {}" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

67 
"support_on (insert x s) f = 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

68 
(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

69 
"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

70 
"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

71 
"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

72 
"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

73 
unfolding support_on_def by auto 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

74 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

75 
lemma support_on_cong: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

76 
"(\<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

77 
by (auto simp: support_on_def) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

78 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

79 
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

80 
by (auto simp: support_on_def) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

81 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

82 
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

83 
by (auto simp: support_on_def) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

84 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

85 
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

86 
unfolding support_on_def by auto 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

87 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

88 
(* 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

89 
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

90 
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

91 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

92 
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

93 
unfolding supp_sum_def by auto 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

94 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

95 
lemma supp_sum_insert[simp]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

96 
"finite (support_on S f) \<Longrightarrow> 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

97 
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

98 
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

99 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

100 
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

101 
by (cases "r = 0") 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

102 
(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

103 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

104 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

105 
subsection \<open>Intervals\<close> 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

106 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

107 
lemma image_affinity_interval: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

108 
fixes c :: "'a::ordered_real_vector" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

109 
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

110 
(if {a..b}={} then {} 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

111 
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

112 
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

113 
(is "?lhs = ?rhs") 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

114 
proof (cases "m=0") 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

115 
case True 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

116 
then show ?thesis 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

117 
by force 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

118 
next 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

119 
case False 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

120 
show ?thesis 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

121 
proof 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

122 
show "?lhs \<subseteq> ?rhs" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

123 
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

124 
show "?rhs \<subseteq> ?lhs" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

125 
proof (clarsimp, intro conjI impI subsetI) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

126 
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

127 
\<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

128 
apply (rule_tac x="inverse m *\<^sub>R (xc)" in rev_image_eqI) 
70630  129 
using False apply (auto simp: pos_le_divideR_eq pos_divideR_le_eq le_diff_eq diff_le_eq) 
130 
done 

69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

131 
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

132 
\<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

133 
apply (rule_tac x="inverse m *\<^sub>R (xc)" in rev_image_eqI) 
70630  134 
apply (auto simp add: neg_le_divideR_eq neg_divideR_le_eq not_le le_diff_eq diff_le_eq) 
70346  135 
done 
69544
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 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

139 

69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

140 
subsection \<open>Limit Points\<close> 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

141 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

142 
lemma islimpt_ball: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

143 
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

144 
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

145 
(is "?lhs \<longleftrightarrow> ?rhs") 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

146 
proof 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

147 
show ?rhs if ?lhs 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

148 
proof 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

149 
{ 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

150 
assume "e \<le> 0" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

151 
then have *: "ball x e = {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

152 
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

153 
have False using \<open>?lhs\<close> 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

154 
unfolding * using islimpt_EMPTY[of y] by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

155 
} 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

156 
then show "e > 0" by (metis not_less) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

157 
show "y \<in> cball x e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

158 
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

159 
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

160 
unfolding closed_limpt by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

161 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

162 
show ?lhs if ?rhs 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

163 
proof  
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

164 
from that have "e > 0" by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

165 
{ 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

166 
fix d :: real 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

167 
assume "d > 0" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

168 
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

169 
proof (cases "d \<le> dist x y") 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

170 
case True 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

171 
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

172 
proof (cases "x = y") 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

173 
case True 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

174 
then have False 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

175 
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

176 
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

177 
by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

178 
next 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

179 
case False 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

180 
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

181 
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

182 
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

183 
by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

184 
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

185 
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

186 
unfolding scaleR_minus_left scaleR_one 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

187 
by (auto simp: norm_minus_commute) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

188 
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

189 
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

190 
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

191 
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

192 
by (auto simp: dist_norm) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

193 
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

194 
by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

195 
moreover 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

196 
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

197 
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

198 
by (auto simp: dist_commute) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

199 
moreover 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

200 
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

201 
unfolding dist_norm 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

202 
apply simp 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

203 
unfolding norm_minus_cancel 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

204 
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

205 
unfolding dist_norm 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

206 
apply auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

207 
done 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

208 
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

209 
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

210 
apply auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

211 
done 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

212 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

213 
next 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

214 
case False 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

215 
then have "d > dist x y" by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

216 
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

217 
proof (cases "x = y") 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

218 
case True 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

219 
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

220 
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

221 
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

222 
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

223 
unfolding \<open>x = y\<close> 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

224 
using \<open>z \<noteq> y\<close> ** 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

225 
apply (rule_tac x=z in bexI) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

226 
apply (auto simp: dist_commute) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

227 
done 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

228 
next 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

229 
case False 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

230 
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

231 
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

232 
apply (rule_tac x=x in bexI, auto) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

233 
done 
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 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

236 
} 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

237 
then show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

238 
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

239 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

240 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

241 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

242 
lemma closure_ball_lemma: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

243 
fixes x y :: "'a::real_normed_vector" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

244 
assumes "x \<noteq> y" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

245 
shows "y islimpt ball x (dist x y)" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

246 
proof (rule islimptI) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

247 
fix T 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

248 
assume "y \<in> T" "open T" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

249 
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

250 
unfolding open_dist by fast 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

251 
(* 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

252 
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

253 
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

254 
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

255 
unfolding z_def by (simp add: algebra_simps) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

256 
have "dist z y < r" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

257 
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

258 
by (simp add: dist_norm min_def) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

259 
then have "z \<in> T" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

260 
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

261 
have "dist x z < dist x y" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

262 
unfolding z_def2 dist_norm 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

263 
apply (simp add: norm_minus_commute) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

264 
apply (simp only: dist_norm [symmetric]) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

265 
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

266 
apply (rule mult_strict_right_mono) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

267 
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

268 
apply (simp add: \<open>x \<noteq> y\<close>) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

269 
done 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

270 
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

271 
by simp 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

272 
have "z \<noteq> y" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

273 
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

274 
by (simp add: min_def) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

275 
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

276 
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

277 
by fast 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

278 
qed 
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 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

281 
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

282 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

283 
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

284 
for x :: "'a::real_normed_vector" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

285 
by (simp add: dist_norm) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

286 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

287 
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

288 
for x :: "'a::real_normed_vector" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

289 
by (simp add: dist_norm) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

290 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

291 
lemma closure_ball [simp]: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

292 
fixes x :: "'a::real_normed_vector" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

293 
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

294 
apply (rule equalityI) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

295 
apply (rule closure_minimal) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

296 
apply (rule ball_subset_cball) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

297 
apply (rule closed_cball) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

298 
apply (rule subsetI, rename_tac y) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

299 
apply (simp add: le_less [where 'a=real]) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

300 
apply (erule disjE) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

301 
apply (rule subsetD [OF closure_subset], simp) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

302 
apply (simp add: closure_def, clarify) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

303 
apply (rule closure_ball_lemma) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

304 
apply simp 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

305 
done 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

306 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

307 
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

308 
for x :: "'a::real_normed_vector" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

309 
by (simp add: dist_norm) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

310 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

311 
(* 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

312 
lemma interior_cball [simp]: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

313 
fixes x :: "'a::{real_normed_vector, perfect_space}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

314 
shows "interior (cball x e) = ball x e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

315 
proof (cases "e \<ge> 0") 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

316 
case False note cs = this 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

317 
from cs have null: "ball x e = {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

318 
using ball_empty[of e x] by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

319 
moreover 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

320 
have "cball x e = {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

321 
proof (rule equals0I) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

322 
fix y 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

323 
assume "y \<in> cball x e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

324 
then show False 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

325 
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

326 
subset_antisym subset_ball) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

327 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

328 
then have "interior (cball x e) = {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

329 
using interior_empty by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

330 
ultimately show ?thesis by blast 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

331 
next 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

332 
case True note cs = this 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

333 
have "ball x e \<subseteq> cball x e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

334 
using ball_subset_cball by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

335 
moreover 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

336 
{ 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

337 
fix S y 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

338 
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

339 
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

340 
unfolding open_dist by blast 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

341 
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

342 
using perfect_choose_dist [of d] by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

343 
have "xa \<in> S" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

344 
using d[THEN spec[where x = xa]] 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

345 
using xa by (auto simp: dist_commute) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

346 
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

347 
using as(1) by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

348 
then have "y \<in> ball x e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

349 
proof (cases "x = y") 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

350 
case True 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

351 
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

352 
then show "y \<in> ball x e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

353 
using \<open>x = y \<close> by simp 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

354 
next 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

355 
case False 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

356 
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

357 
unfolding dist_norm 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

358 
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

359 
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

360 
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

361 
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

362 
hence **:"d / (2 * norm (y  x)) > 0" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

363 
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

364 
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

365 
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

366 
by (auto simp: dist_norm algebra_simps) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

367 
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

368 
by (auto simp: algebra_simps) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

369 
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

370 
using ** by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

371 
also have "\<dots> = (dist y x) + d/2" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

372 
using ** by (auto simp: distrib_right dist_norm) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

373 
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

374 
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

375 
then show "y \<in> ball x e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

376 
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

377 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

378 
} 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

379 
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

380 
by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

381 
ultimately show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

382 
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

383 
using open_ball[of x e] 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

384 
by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

385 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

386 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

387 
lemma frontier_ball [simp]: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

388 
fixes a :: "'a::real_normed_vector" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

389 
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

390 
by (force simp: frontier_def) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

391 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

392 
lemma frontier_cball [simp]: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

393 
fixes a :: "'a::{real_normed_vector, perfect_space}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

394 
shows "frontier (cball a e) = sphere a e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

395 
by (force simp: frontier_def) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

396 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

397 
corollary compact_sphere [simp]: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

398 
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

399 
shows "compact (sphere a r)" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

400 
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

401 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

402 
corollary bounded_sphere [simp]: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

403 
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

404 
shows "bounded (sphere a r)" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

405 
by (simp add: compact_imp_bounded) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

406 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

407 
corollary closed_sphere [simp]: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

408 
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

409 
shows "closed (sphere a r)" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

410 
by (simp add: compact_imp_closed) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

411 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

412 
lemma image_add_ball [simp]: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

413 
fixes a :: "'a::real_normed_vector" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

414 
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

415 
apply (intro equalityI subsetI) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

416 
apply (force simp: dist_norm) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

417 
apply (rule_tac x="xb" in image_eqI) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

418 
apply (auto simp: dist_norm algebra_simps) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

419 
done 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

420 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

421 
lemma image_add_cball [simp]: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

422 
fixes a :: "'a::real_normed_vector" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

423 
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

424 
apply (intro equalityI subsetI) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

425 
apply (force simp: dist_norm) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

426 
apply (rule_tac x="xb" in image_eqI) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

427 
apply (auto simp: dist_norm algebra_simps) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

428 
done 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

429 

69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

430 

70136  431 
subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas on Normed Algebras\<close> 
69544
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 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

434 
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

435 
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

436 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

437 
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

438 
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

439 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

440 
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

441 
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

442 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

443 
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

444 
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

445 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

446 
lemma closed_subset_Ints: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

447 
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

448 
assumes "A \<subseteq> \<int>" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

449 
shows "closed A" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

450 
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

451 
case (1 x y) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

452 
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

453 
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

454 
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

455 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

456 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

457 
subsection \<open>Filters\<close> 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

458 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

459 
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

460 
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

461 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

462 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

463 
subsection \<open>Trivial Limits\<close> 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

464 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

465 
lemma trivial_limit_at_infinity: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

466 
"\<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

467 
unfolding trivial_limit_def eventually_at_infinity 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

468 
apply clarsimp 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

469 
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

470 
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

471 
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

472 
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

473 
done 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

474 

69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

475 
lemma at_within_ball_bot_iff: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

476 
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

477 
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

478 
unfolding trivial_limit_within 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

479 
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

480 
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

481 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

482 

69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

483 
subsection \<open>Limits\<close> 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

484 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

485 
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

486 
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

487 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

488 
corollary Lim_at_infinityI [intro?]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

489 
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

490 
shows "(f \<longlongrightarrow> l) at_infinity" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

491 
apply (simp add: Lim_at_infinity, clarify) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

492 
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

493 
done 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

494 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

495 
lemma Lim_transform_within_set_eq: 
70532
fcf3b891ccb1
new material; rotated premises of Lim_transform_eventually
paulson <lp15@cam.ac.uk>
parents:
70380
diff
changeset

496 
fixes a :: "'a::metric_space" and l :: "'b::metric_space" 
fcf3b891ccb1
new material; rotated premises of Lim_transform_eventually
paulson <lp15@cam.ac.uk>
parents:
70380
diff
changeset

497 
shows "eventually (\<lambda>x. x \<in> S \<longleftrightarrow> x \<in> T) (at a) 
fcf3b891ccb1
new material; rotated premises of Lim_transform_eventually
paulson <lp15@cam.ac.uk>
parents:
70380
diff
changeset

498 
\<Longrightarrow> ((f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within T))" 
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

499 
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

500 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

501 
lemma Lim_null: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

502 
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

503 
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

504 
by (simp add: Lim dist_norm) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

505 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

506 
lemma Lim_null_comparison: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

507 
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

508 
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

509 
shows "(f \<longlongrightarrow> 0) net" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

510 
using assms(2) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

511 
proof (rule metric_tendsto_imp_tendsto) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

512 
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

513 
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

514 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

515 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

516 
lemma Lim_transform_bound: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

517 
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

518 
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

519 
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

520 
and "(g \<longlongrightarrow> 0) net" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

521 
shows "(f \<longlongrightarrow> 0) net" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

522 
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

523 
by (rule Lim_null_comparison) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

524 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

525 
lemma lim_null_mult_right_bounded: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

526 
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

527 
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

528 
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

529 
proof  
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

530 
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

531 
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

532 
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

533 
apply (rule Lim_null_comparison [OF _ *]) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

534 
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

535 
done 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

536 
then show ?thesis 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

537 
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

538 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

539 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

540 
lemma lim_null_mult_left_bounded: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

541 
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

542 
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

543 
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

544 
proof  
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

545 
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

546 
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

547 
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

548 
apply (rule Lim_null_comparison [OF _ *]) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

549 
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

550 
done 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

551 
then show ?thesis 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

552 
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

553 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

554 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

555 
lemma lim_null_scaleR_bounded: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

556 
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

557 
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

558 
proof 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

559 
fix \<epsilon>::real 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

560 
assume "0 < \<epsilon>" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

561 
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

562 
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

563 
proof  
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

564 
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

565 
by (simp add: mult_left_mono g) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

566 
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

567 
by (simp add: mult_left_mono) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

568 
also have "\<dots> < \<epsilon>" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

569 
by (rule f) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

570 
finally show ?thesis . 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

571 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

572 
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

573 
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

574 
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

575 
done 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

576 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

577 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

578 
lemma Lim_norm_ubound: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

579 
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

580 
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

581 
shows "norm(l) \<le> e" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

582 
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

583 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

584 
lemma Lim_norm_lbound: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

585 
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

586 
assumes "\<not> trivial_limit net" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

587 
and "(f \<longlongrightarrow> l) net" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

588 
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

589 
shows "e \<le> norm l" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

590 
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

591 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

592 
text\<open>Limit under bilinear function\<close> 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

593 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

594 
lemma Lim_bilinear: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

595 
assumes "(f \<longlongrightarrow> l) net" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

596 
and "(g \<longlongrightarrow> m) net" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

597 
and "bounded_bilinear h" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

598 
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

599 
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

600 
by (rule bounded_bilinear.tendsto) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

601 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

602 
lemma Lim_at_zero: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

603 
fixes a :: "'a::real_normed_vector" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

604 
and l :: "'b::topological_space" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

605 
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

606 
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

607 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

608 

70136  609 
subsection\<^marker>\<open>tag unimportant\<close> \<open>Limit Point of Filter\<close> 
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

610 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

611 
lemma netlimit_at_vector: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

612 
fixes a :: "'a::real_normed_vector" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

613 
shows "netlimit (at a) = a" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

614 
proof (cases "\<exists>x. x \<noteq> a") 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

615 
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

616 
have "\<not> trivial_limit (at a)" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

617 
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

618 
apply clarsimp 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

619 
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

620 
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

621 
done 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

622 
then show ?thesis 
70065
cc89a395b5a3
Free_Abelian_Groups finally working; fixed some duplicates; cleaned up some proofs
paulson <lp15@cam.ac.uk>
parents:
69922
diff
changeset

623 
by (rule Lim_ident_at [of a UNIV]) 
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

624 
qed simp 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

625 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

626 
subsection \<open>Boundedness\<close> 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

627 

69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

628 
lemma continuous_on_closure_norm_le: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

629 
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

630 
assumes "continuous_on (closure s) f" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

631 
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

632 
and "x \<in> (closure s)" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

633 
shows "norm (f x) \<le> b" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

634 
proof  
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

635 
have *: "f ` s \<subseteq> cball 0 b" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

636 
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

637 
show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

638 
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

639 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

640 

69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

641 
lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x \<le> b)" 
70380
2b0dca68c3ee
More analysis / measure theory material
paulson <lp15@cam.ac.uk>
parents:
70346
diff
changeset

642 
unfolding bounded_iff 
2b0dca68c3ee
More analysis / measure theory material
paulson <lp15@cam.ac.uk>
parents:
70346
diff
changeset

643 
by (meson less_imp_le not_le order_trans zero_less_one) 
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

644 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

645 
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

646 
apply (simp add: bounded_pos) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

647 
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

648 
done 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

649 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

650 
lemma Bseq_eq_bounded: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

651 
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

652 
shows "Bseq f \<longleftrightarrow> bounded (range f)" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

653 
unfolding Bseq_def bounded_pos by auto 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

654 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

655 
lemma bounded_linear_image: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

656 
assumes "bounded S" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

657 
and "bounded_linear f" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

658 
shows "bounded (f ` S)" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

659 
proof  
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

660 
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

661 
unfolding bounded_pos by auto 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

662 
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

663 
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

664 
show ?thesis 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

665 
unfolding bounded_pos 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

666 
proof (intro exI, safe) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

667 
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

668 
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

669 
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

670 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

671 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

672 
lemma bounded_scaling: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

673 
fixes S :: "'a::real_normed_vector set" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

674 
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

675 
apply (rule bounded_linear_image, assumption) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

676 
apply (rule bounded_linear_scaleR_right) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

677 
done 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

678 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

679 
lemma bounded_scaleR_comp: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

680 
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

681 
assumes "bounded (f ` S)" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

682 
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

683 
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

684 
by (auto simp: image_image) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

685 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

686 
lemma bounded_translation: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

687 
fixes S :: "'a::real_normed_vector set" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

688 
assumes "bounded S" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

689 
shows "bounded ((\<lambda>x. a + x) ` S)" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

690 
proof  
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

691 
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

692 
unfolding bounded_pos by auto 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

693 
{ 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

694 
fix x 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

695 
assume "x \<in> S" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

696 
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

697 
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

698 
} 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

699 
then show ?thesis 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

700 
unfolding bounded_pos 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

701 
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

702 
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

703 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

704 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

705 
lemma bounded_translation_minus: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

706 
fixes S :: "'a::real_normed_vector set" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

707 
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

708 
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

709 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

710 
lemma bounded_uminus [simp]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

711 
fixes X :: "'a::real_normed_vector set" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

712 
shows "bounded (uminus ` X) \<longleftrightarrow> bounded X" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

713 
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

714 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

715 
lemma uminus_bounded_comp [simp]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

716 
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

717 
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

718 
using bounded_uminus[of "f ` S"] 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

719 
by (auto simp: image_image) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

720 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

721 
lemma bounded_plus_comp: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

722 
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

723 
assumes "bounded (f ` S)" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

724 
assumes "bounded (g ` S)" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

725 
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

726 
proof  
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

727 
{ 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

728 
fix B C 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

729 
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

730 
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

731 
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

732 
} then show ?thesis 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

733 
using assms by (fastforce simp: bounded_iff) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

734 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

735 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

736 
lemma bounded_plus: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

737 
fixes S ::"'a::real_normed_vector set" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

738 
assumes "bounded S" "bounded T" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

739 
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

740 
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

741 
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

742 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

743 
lemma bounded_minus_comp: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

744 
"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

745 
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

746 
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

747 
by auto 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

748 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

749 
lemma bounded_minus: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

750 
fixes S ::"'a::real_normed_vector set" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

751 
assumes "bounded S" "bounded T" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

752 
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

753 
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

754 
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

755 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

756 
lemma not_bounded_UNIV[simp]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

757 
"\<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

758 
proof (auto simp: bounded_pos not_le) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

759 
obtain x :: 'a where "x \<noteq> 0" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

760 
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

761 
fix b :: real 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

762 
assume b: "b >0" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

763 
have b1: "b +1 \<ge> 0" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

764 
using b by simp 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

765 
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

766 
by (simp add: norm_sgn) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

767 
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

768 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

769 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

770 
corollary cobounded_imp_unbounded: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

771 
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

772 
shows "bounded ( S) \<Longrightarrow> \<not> bounded S" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

773 
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

774 

70136  775 
subsection\<^marker>\<open>tag unimportant\<close>\<open>Relations among convergence and absolute convergence for power series\<close> 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

776 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

777 
lemma summable_imp_bounded: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

778 
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

779 
shows "summable f \<Longrightarrow> bounded (range f)" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

780 
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

781 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

782 
lemma summable_imp_sums_bounded: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

783 
"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

784 
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

785 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

786 
lemma power_series_conv_imp_absconv_weak: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

787 
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

788 
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

789 
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

790 
proof  
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

791 
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

792 
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

793 
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

794 
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

795 
show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

796 
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

797 
apply (simp only: summable_complex_of_real *) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

798 
apply (auto simp: norm_mult norm_power) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

799 
done 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

800 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

801 

69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

802 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

803 
subsection \<open>Normed spaces with the HeineBorel property\<close> 
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 
lemma not_compact_UNIV[simp]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

806 
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

807 
shows "\<not> compact (UNIV::'a set)" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

808 
by (simp add: compact_eq_bounded_closed) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

809 

69918
eddcc7c726f3
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
paulson <lp15@cam.ac.uk>
parents:
69745
diff
changeset

810 
lemma not_compact_space_euclideanreal [simp]: "\<not> compact_space euclideanreal" 
eddcc7c726f3
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
paulson <lp15@cam.ac.uk>
parents:
69745
diff
changeset

811 
by (simp add: compact_space_def) 
eddcc7c726f3
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
paulson <lp15@cam.ac.uk>
parents:
69745
diff
changeset

812 

69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

813 
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

814 
lemma closed_Union_compact_subsets: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

815 
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

816 
assumes "closed S" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

817 
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

818 
"(\<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

819 
proof 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

820 
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

821 
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

822 
next 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

823 
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

824 
by (auto simp: real_arch_simple) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

825 
next 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

826 
fix K :: "'a set" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

827 
assume "compact K" "K \<subseteq> S" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

828 
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

829 
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

830 
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

831 
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

832 
qed auto 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

833 

69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

834 
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

835 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

836 
proposition bounded_closed_chain: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

837 
fixes \<F> :: "'a::heine_borel set set" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

838 
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

839 
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

840 
shows "\<Inter>\<F> \<noteq> {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

841 
proof  
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

842 
have "B \<inter> \<Inter>\<F> \<noteq> {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

843 
proof (rule compact_imp_fip) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

844 
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

845 
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

846 
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

847 
proof (induction \<G> rule: finite_induct) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

848 
case empty 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

849 
with assms show ?case by force 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

850 
next 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

851 
case (insert U \<G>) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

852 
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

853 
then consider "B \<subseteq> U"  "U \<subseteq> B" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

854 
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

855 
then show ?case 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

856 
proof cases 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

857 
case 1 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

858 
then show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

859 
using Int_left_commute ne by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

860 
next 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

861 
case 2 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

862 
have "U \<noteq> {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

863 
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

864 
moreover 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

865 
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

866 
proof  
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

867 
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

868 
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

869 
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

870 
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

871 
moreover obtain x where "x \<in> \<Inter>\<G>" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

872 
by (metis Int_emptyI ne) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

873 
ultimately show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

874 
by (metis Inf_lower subset_eq that) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

875 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

876 
with 2 show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

877 
by blast 
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 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

881 
then show ?thesis by blast 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

882 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

883 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

884 
corollary compact_chain: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

885 
fixes \<F> :: "'a::heine_borel set set" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

886 
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

887 
"\<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

888 
shows "\<Inter> \<F> \<noteq> {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

889 
proof (cases "\<F> = {}") 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

890 
case True 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

891 
then show ?thesis by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

892 
next 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

893 
case False 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

894 
show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

895 
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

896 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

897 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

898 
lemma compact_nest: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

899 
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

900 
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" 
69745  901 
shows "\<Inter>(range F) \<noteq> {}" 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

902 
proof  
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

903 
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

904 
by (metis mono image_iff le_cases) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

905 
show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

906 
apply (rule compact_chain [OF _ _ *]) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

907 
using F apply (blast intro: dest: *)+ 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

908 
done 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

909 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

910 

42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

911 
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

912 
theorem Baire: 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

913 
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

914 
assumes "closed S" "countable \<G>" 
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

915 
and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (top_of_set S) T \<and> S \<subseteq> closure T" 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

916 
shows "S \<subseteq> closure(\<Inter>\<G>)" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

917 
proof (cases "\<G> = {}") 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

918 
case True 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

919 
then show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

920 
using closure_subset by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

921 
next 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

922 
let ?g = "from_nat_into \<G>" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

923 
case False 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

924 
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

925 
by (simp add: from_nat_into) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

926 
show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

927 
proof (clarsimp simp: closure_approachable) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

928 
fix x and e::real 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

929 
assume "x \<in> S" "0 < e" 
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

930 
obtain TF where opeF: "\<And>n. openin (top_of_set S) (TF n)" 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

931 
and ne: "\<And>n. TF n \<noteq> {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

932 
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

933 
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

934 
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

935 
proof  
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

936 
have *: "\<exists>Y. (openin (top_of_set S) Y \<and> Y \<noteq> {} \<and> 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

937 
S \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> U" 
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

938 
if opeU: "openin (top_of_set S) U" and "U \<noteq> {}" and cloU: "closure U \<subseteq> ball x e" for U n 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

939 
proof  
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

940 
obtain T where T: "open T" "U = T \<inter> S" 
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

941 
using \<open>openin (top_of_set S) U\<close> by (auto simp: openin_subtopology) 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

942 
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

943 
using gin ope by fastforce 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

944 
then have "T \<inter> ?g n \<noteq> {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

945 
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

946 
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

947 
using T ope [of "?g n", OF gin] by (blast dest: openin_imp_subset) 
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

948 
moreover have "openin (top_of_set S) (U \<inter> ?g n)" 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

949 
using gin ope opeU by blast 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

950 
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

951 
by (force simp: openin_contains_ball) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

952 
show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

953 
proof (intro exI conjI) 
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

954 
show "openin (top_of_set S) (S \<inter> ball y (d/2))" 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

955 
by (simp add: openin_open_Int) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

956 
show "S \<inter> ball y (d/2) \<noteq> {}" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

957 
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

958 
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

959 
using closure_mono by blast 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

960 
also have "... \<subseteq> ?g n" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

961 
using \<open>d > 0\<close> d by force 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

962 
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

963 
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

964 
proof  
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

965 
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

966 
using \<open>d > 0\<close> by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

967 
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

968 
by (meson closure_mono inf.cobounded2 subset_trans) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

969 
then show ?thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

970 
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

971 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

972 
also have "... \<subseteq> ball x e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

973 
using cloU closure_subset d by blast 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

974 
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

975 
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

976 
using ball_divide_subset_numeral d by blast 
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 
qed 
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

979 
let ?\<Phi> = "\<lambda>n X. openin (top_of_set S) X \<and> X \<noteq> {} \<and> 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

980 
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

981 
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

982 
by (simp add: closure_mono) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

983 
also have "... \<subseteq> ball x e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

984 
using \<open>e > 0\<close> by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

985 
finally have "closure (S \<inter> ball x (e / 2)) \<subseteq> ball x e" . 
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

986 
moreover have"openin (top_of_set S) (S \<inter> ball x (e / 2))" "S \<inter> ball x (e / 2) \<noteq> {}" 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

987 
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

988 
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

989 
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

990 
show thesis 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

991 
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

992 
show "\<exists>x. ?\<Phi> 0 x" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

993 
using Y by auto 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

994 
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

995 
using that by (blast intro: *) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

996 
qed (use that in metis) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

997 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

998 
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

999 
proof (rule compact_nest) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

1000 
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

1001 
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

1002 
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

1003 
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

1004 
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

1005 
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

1006 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

1007 
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

1008 
proof (clarsimp, intro conjI) 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

1009 
fix y 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

1010 
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

1011 
then show "\<forall>T\<in>\<G>. y \<in> T" 
69712  1012 
by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] subsetD subg) 
69611
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

1013 
show "dist y x < e" 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

1014 
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

1015 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

1016 
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

1017 
by auto 
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 
qed 
42cc3609fedf
moved some material from Connected.thy to more appropriate places
immler
parents:
69544
diff
changeset

1020 

69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1021 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1022 
subsection \<open>Continuity\<close> 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1023 

70136  1024 
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Structural rules for uniform continuity\<close> 
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1025 

69613
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1026 
lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]: 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1027 
fixes g :: "_::metric_space \<Rightarrow> _" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1028 
assumes "uniformly_continuous_on s g" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1029 
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

1030 
using assms unfolding uniformly_continuous_on_sequentially 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1031 
unfolding dist_norm tendsto_norm_zero_iff diff[symmetric] 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1032 
by (auto intro: tendsto_zero) 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1033 

69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1034 
lemma uniformly_continuous_on_dist[continuous_intros]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1035 
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

1036 
assumes "uniformly_continuous_on s f" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1037 
and "uniformly_continuous_on s g" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1038 
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

1039 
proof  
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1040 
{ 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1041 
fix a b c d :: 'b 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1042 
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

1043 
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

1044 
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

1045 
by arith 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1046 
} note le = this 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1047 
{ 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1048 
fix x y 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1049 
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

1050 
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

1051 
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

1052 
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

1053 
simp add: le) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1054 
} 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1055 
then show ?thesis 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1056 
using assms unfolding uniformly_continuous_on_sequentially 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1057 
unfolding dist_real_def by simp 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1058 
qed 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1059 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1060 
lemma uniformly_continuous_on_norm[continuous_intros]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1061 
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

1062 
assumes "uniformly_continuous_on s f" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1063 
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

1064 
unfolding norm_conv_dist using assms 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1065 
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

1066 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1067 
lemma uniformly_continuous_on_cmul[continuous_intros]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1068 
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

1069 
assumes "uniformly_continuous_on s f" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1070 
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

1071 
using bounded_linear_scaleR_right assms 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1072 
by (rule bounded_linear.uniformly_continuous_on) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1073 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1074 
lemma dist_minus: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1075 
fixes x y :: "'a::real_normed_vector" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1076 
shows "dist ( x) ( y) = dist x y" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1077 
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

1078 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1079 
lemma uniformly_continuous_on_minus[continuous_intros]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1080 
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

1081 
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

1082 
unfolding uniformly_continuous_on_def dist_minus . 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1083 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1084 
lemma uniformly_continuous_on_add[continuous_intros]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1085 
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

1086 
assumes "uniformly_continuous_on s f" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1087 
and "uniformly_continuous_on s g" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1088 
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

1089 
using assms 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1090 
unfolding uniformly_continuous_on_sequentially 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1091 
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

1092 
by (auto intro: tendsto_add_zero) 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1093 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1094 
lemma uniformly_continuous_on_diff[continuous_intros]: 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1095 
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

1096 
assumes "uniformly_continuous_on s f" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1097 
and "uniformly_continuous_on s g" 
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1098 
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

1099 
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

1100 
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

1101 

5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
diff
changeset

1102 

70136  1103 
subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic Preserves Topological Properties\<close> 
69613
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1104 

1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1105 
lemma open_scaling[intro]: 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1106 
fixes s :: "'a::real_normed_vector set" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1107 
assumes "c \<noteq> 0" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1108 
and "open s" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1109 
shows "open((\<lambda>x. c *\<^sub>R x) ` s)" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1110 
proof  
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1111 
{ 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1112 
fix x 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1113 
assume "x \<in> s" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1114 
then obtain e where "e>0" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1115 
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

1116 
by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1117 
have "e * \<bar>c\<bar> > 0" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1118 
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

1119 
moreover 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1120 
{ 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1121 
fix y 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1122 
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

1123 
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

1124 
unfolding dist_norm 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1125 
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

1126 
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

1127 
then have "y \<in> (*\<^sub>R) c ` s" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1128 
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

1129 
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

1130 
using assms(1) 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1131 
unfolding dist_norm scaleR_scaleR 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1132 
by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1133 
} 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1134 
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

1135 
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

1136 
done 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1137 
} 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1138 
then show ?thesis unfolding open_dist by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1139 
qed 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1140 

1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1141 
lemma minus_image_eq_vimage: 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1142 
fixes A :: "'a::ab_group_add set" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1143 
shows "(\<lambda>x.  x) ` A = (\<lambda>x.  x) ` A" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1144 
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

1145 

1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1146 
lemma open_negations: 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1147 
fixes S :: "'a::real_normed_vector set" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1148 
shows "open S \<Longrightarrow> open ((\<lambda>x.  x) ` S)" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1149 
using open_scaling [of " 1" S] by simp 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1150 

1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1151 
lemma open_translation: 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1152 
fixes S :: "'a::real_normed_vector set" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1153 
assumes "open S" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1154 
shows "open((\<lambda>x. a + x) ` S)" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1155 
proof  
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1156 
{ 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1157 
fix x 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1158 
have "continuous (at x) (\<lambda>x. x  a)" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1159 
by (intro continuous_diff continuous_ident continuous_const) 
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 
moreover have "{x. x  a \<in> S} = (+) a ` S" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1162 
by force 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1163 
ultimately show ?thesis 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1164 
by (metis assms continuous_open_vimage vimage_def) 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1165 
qed 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1166 

1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1167 
lemma open_neg_translation: 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1168 
fixes s :: "'a::real_normed_vector set" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1169 
assumes "open s" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1170 
shows "open((\<lambda>x. a  x) ` s)" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1171 
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

1172 
by (auto simp: image_image) 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1173 

1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1174 
lemma open_affinity: 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1175 
fixes S :: "'a::real_normed_vector set" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1176 
assumes "open S" "c \<noteq> 0" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1177 
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

1178 
proof  
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1179 
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

1180 
unfolding o_def .. 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1181 
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

1182 
by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1183 
then show ?thesis 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1184 
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

1185 
unfolding * 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1186 
by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1187 
qed 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1188 

1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1189 
lemma interior_translation: 
69661  1190 
"interior ((+) a ` S) = (+) a ` (interior S)" for S :: "'a::real_normed_vector set" 
69613
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1191 
proof (rule set_eqI, rule) 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1192 
fix x 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1193 
assume "x \<in> interior ((+) a ` S)" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1194 
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

1195 
unfolding mem_interior by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1196 
then have "ball (x  a) e \<subseteq> S" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1197 
unfolding subset_eq Ball_def mem_ball dist_norm 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1198 
by (auto simp: diff_diff_eq) 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1199 
then show "x \<in> (+) a ` interior S" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1200 
unfolding image_iff 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1201 
apply (rule_tac x="x  a" in bexI) 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1202 
unfolding mem_interior 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1203 
using \<open>e > 0\<close> 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1204 
apply auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1205 
done 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1206 
next 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1207 
fix x 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1208 
assume "x \<in> (+) a ` interior S" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1209 
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

1210 
unfolding image_iff Bex_def mem_interior by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1211 
{ 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1212 
fix z 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1213 
have *: "a + y  z = y + a  z" by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1214 
assume "z \<in> ball x e" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1215 
then have "z  a \<in> S" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1216 
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

1217 
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

1218 
by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1219 
then have "z \<in> (+) a ` S" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1220 
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

1221 
} 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1222 
then have "ball x e \<subseteq> (+) a ` S" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1223 
unfolding subset_eq by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1224 
then show "x \<in> interior ((+) a ` S)" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1225 
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

1226 
qed 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1227 

69661  1228 
lemma interior_translation_subtract: 
1229 
"interior ((\<lambda>x. x  a) ` S) = (\<lambda>x. x  a) ` interior S" for S :: "'a::real_normed_vector set" 

1230 
using interior_translation [of " a"] by (simp cong: image_cong_simp) 

1231 

1232 

69613
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1233 
lemma compact_scaling: 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1234 
fixes s :: "'a::real_normed_vector set" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1235 
assumes "compact s" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1236 
shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1237 
proof  
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1238 
let ?f = "\<lambda>x. scaleR c x" 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1239 
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

1240 
show ?thesis 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1241 
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

1242 
using linear_continuous_at[OF *] assms 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1243 
by auto 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1244 
qed 
1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset

1245 

1331e57b54c6
moved material from Connected.thy to more appropriate places
immler
parents:
69611
diff
changeset
