--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Nov 16 12:09:59 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Nov 16 15:06:34 2009 +0100
@@ -379,6 +379,9 @@
shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
using assms unfolding convex_alt by auto
+lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
+ unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto
+
lemma convex_empty[intro]: "convex {}"
unfolding convex_def by simp
@@ -3379,6 +3382,4 @@
lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n::finite. norm(x - a) = r}"
using path_connected_sphere path_connected_imp_connected by auto
-(** In continuous_at_vec1_norm : Use \<And> instead of \<forall>. **)
-
end
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Nov 16 12:09:59 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Nov 16 15:06:34 2009 +0100
@@ -1642,6 +1642,9 @@
definition "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *s x) = c *s f x)"
+lemma linearI: assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *s x) = c *s f x"
+ shows "linear f" using assms unfolding linear_def by auto
+
lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. (c::'a::comm_semiring) *s f x)"
by (vector linear_def Cart_eq ring_simps)
@@ -1812,6 +1815,11 @@
by (simp add: f.add f.scaleR)
qed
+lemma bounded_linearI': fixes f::"real^'n::finite \<Rightarrow> real^'m::finite"
+ assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *s x) = c *s f x"
+ shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym]
+ by(rule linearI[OF assms])
+
subsection{* Bilinear functions. *}
definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))"
@@ -2470,6 +2478,11 @@
lemma vec1_cmul: "vec1(c* x) = c *s vec1 x " by (vector vec1_def)
lemma vec1_neg: "vec1(- x) = - vec1 x " by (vector vec1_def)
+lemma vec1_0[simp]:"vec1 0 = 0" unfolding vec1_def Cart_eq by auto
+
+lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
+ apply(rule_tac x="dest_vec1 x" in bexI) by auto
+
lemma vec1_setsum: assumes fS: "finite S"
shows "vec1(setsum f S) = setsum (vec1 o f) S"
apply (induct rule: finite_induct[OF fS])
@@ -2512,6 +2525,14 @@
lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
by (metis vec1_dest_vec1 norm_vec1)
+lemmas vec1_dest_vec1_simps = forall_vec1 vec1_add[THEN sym] dist_vec1 vec1_sub[THEN sym] vec1_dest_vec1 norm_vec1 dest_vec1_cmul
+ vec1_eq vec1_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
+
+lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
+ unfolding bounded_linear_def additive_def bounded_linear_axioms_def
+ unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
+ apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
+
lemma linear_vmul_dest_vec1:
fixes f:: "'a::semiring_1^'n \<Rightarrow> 'a^1"
shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 16 12:09:59 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 16 15:06:34 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Topology_Euclidian_Space.thy
+(* title: HOL/Library/Topology_Euclidian_Space.thy
Author: Amine Chaieb, University of Cambridge
Author: Robert Himmelmann, TU Muenchen
*)
@@ -275,6 +275,11 @@
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
+lemma openE[elim?]:
+ assumes "open S" "x\<in>S"
+ obtains e where "e>0" "ball x e \<subseteq> S"
+ using assms unfolding open_contains_ball by auto
+
lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
by (metis open_contains_ball subset_eq centre_in_ball)
@@ -4011,6 +4016,9 @@
shows "bounded_linear f ==> continuous_on s f"
using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
+lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
+ by(rule linear_continuous_on[OF bounded_linear_vec1])
+
text{* Also bilinear functions, in composition form. *}
lemma bilinear_continuous_at_compose:
@@ -4195,6 +4203,8 @@
shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net"
by (intro tendsto_intros)
+lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
+
lemma continuous_vmul:
fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
@@ -4621,6 +4631,15 @@
"(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
by(simp_all add: Cart_eq vector_less_def vector_less_eq_def dest_vec1_def forall_1)
+lemma vec1_interval:fixes a::"real" shows
+ "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
+ "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
+ apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval
+ unfolding forall_1 unfolding dest_vec1_def[THEN sym, of] unfolding vec1_dest_vec1_simps
+ apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
+ apply(rule_tac x="dest_vec1 x" in bexI) by auto
+
+
lemma interval_eq_empty: fixes a :: "real^'n::finite" shows
"({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
"({a .. b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
@@ -4802,6 +4821,12 @@
thus ?thesis unfolding open_dist using open_interval_lemma by auto
qed
+lemma open_interval_real: fixes a :: "real" shows "open {a<..<b}"
+ using open_interval[of "vec1 a" "vec1 b"] unfolding open_contains_ball
+ apply-apply(rule,erule_tac x="vec1 x" in ballE) apply(erule exE,rule_tac x=e in exI)
+ unfolding subset_eq mem_ball apply(rule) defer apply(rule,erule conjE,erule_tac x="vec1 xa" in ballE)
+ by(auto simp add: vec1_dest_vec1_simps vector_less_def forall_1)
+
lemma closed_interval: fixes a :: "real^'n::finite" shows "closed {a .. b}"
proof-
{ fix x i assume as:"\<forall>e>0. \<exists>x'\<in>{a..b}. x' \<noteq> x \<and> dist x' x < e"(* and xab:"a$i > x$i \<or> b$i < x$i"*)