# HG changeset patch # User hoelzl # Date 1258380394 -3600 # Node ID eb2574ac417369914543eb7f04e2226e146686e7 # Parent ffc5176a91051d98d513ba039d8b90b6c62ce81e Added new lemmas to Euclidean Space by Robert Himmelmann diff -r ffc5176a9105 -r eb2574ac4173 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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) \ 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 \ CARD('n) \ 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 \ instead of \. **) - end diff -r ffc5176a9105 -r eb2574ac4173 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- 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 \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *s x) = c *s f x)" +lemma linearI: assumes "\x y. f (x + y) = f x + f y" "\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 (\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 \ real^'m::finite" + assumes "\x y. f (x + y) = f x + f y" "\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 \ (\x. linear(\y. f x y)) \ (\y. linear(\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 = \dest_vec1 x\" 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\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 \ 'a^1" shows "linear f \ linear (\x. dest_vec1(f x) *s v)" diff -r ffc5176a9105 -r eb2574ac4173 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 \ (\x\S. \e>0. ball x e \ S)" unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. +lemma openE[elim?]: + assumes "open S" "x\S" + obtains e where "e>0" "ball x e \ S" + using assms unfolding open_contains_ball by auto + lemma open_contains_ball_eq: "open S \ \x. x\S \ (\e>0. ball x e \ 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\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 ==> ((\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 \ real" and v :: "'b::real_normed_vector" shows "continuous net c ==> continuous net (\x. c(x) *\<^sub>R v)" @@ -4621,6 +4631,15 @@ "(x \ {a<.. dest_vec1 a < dest_vec1 x \ 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<.. (\i. b$i \ a$i))" (is ?th1) and "({a .. b} = {} \ (\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<..e>0. \x'\{a..b}. x' \ x \ dist x' x < e"(* and xab:"a$i > x$i \ b$i < x$i"*)