--- a/src/HOL/Library/Convex_Euclidean_Space.thy Sat Jun 13 08:29:34 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Sat Jun 13 11:56:41 2009 -0700
@@ -714,13 +714,16 @@
proof- have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto
thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed
-lemma convex_linear_image: assumes c:"convex s" and l:"linear f" shows "convex(f ` s)"
+lemma convex_linear_image:
+ assumes c:"convex s" and l:"bounded_linear f"
+ shows "convex(f ` s)"
proof(auto simp add: convex_def)
+ interpret f: bounded_linear f by fact
fix x y assume xy:"x \<in> s" "y \<in> s"
fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
show "u *\<^sub>R f x + v *\<^sub>R f y \<in> f ` s" unfolding image_iff
apply(rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in bexI)
- unfolding linear_add[OF l] linear_cmul[OF l, unfolded smult_conv_scaleR]
+ unfolding f.add f.scaleR
using c[unfolded convex_def] xy uv by auto
qed
@@ -1915,20 +1918,23 @@
subsection {* Convex hull is "preserved" by a linear function. *}
lemma convex_hull_linear_image:
- assumes "linear f"
+ assumes "bounded_linear f"
shows "f ` (convex hull s) = convex hull (f ` s)"
apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
-proof- show "convex {x. f x \<in> convex hull f ` s}"
- unfolding convex_def by(auto simp add: linear_cmul[OF assms, unfolded smult_conv_scaleR] linear_add[OF assms]
- convex_convex_hull[unfolded convex_def, rule_format]) next
+proof-
+ interpret f: bounded_linear f by fact
+ show "convex {x. f x \<in> convex hull f ` s}"
+ unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next
+ interpret f: bounded_linear f by fact
show "convex {x. x \<in> f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s]
- unfolding convex_def by (auto simp add: linear_cmul[OF assms, THEN sym, unfolded smult_conv_scaleR] linear_add[OF assms, THEN sym])
+ unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
qed auto
lemma in_convex_hull_linear_image:
- assumes "linear f" "x \<in> convex hull s" shows "(f x) \<in> convex hull (f ` s)"
+ assumes "bounded_linear f" "x \<in> convex hull s"
+ shows "(f x) \<in> convex hull (f ` s)"
using convex_hull_linear_image[OF assms(1)] assms(2) by auto
subsection {* Homeomorphism of all convex compact sets with nonempty interior. *}
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Sat Jun 13 08:29:34 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Sat Jun 13 11:56:41 2009 -0700
@@ -1239,10 +1239,9 @@
text{* Basic arithmetical combining theorems for limits. *}
lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)"
- assumes "(f ---> l) net" "linear h"
+ assumes "(f ---> l) net" "bounded_linear h"
shows "((\<lambda>x. h (f x)) ---> h l) net"
-using `linear h` `(f ---> l) net`
-unfolding linear_conv_bounded_linear
+using `bounded_linear h` `(f ---> l) net`
by (rule bounded_linear.tendsto)
lemma Lim_ident_at: "((\<lambda>x. x) ---> a) (at a)"
@@ -1435,10 +1434,9 @@
lemma Lim_bilinear:
fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite"
- assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h"
+ assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
-using `bilinear h` `(f ---> l) net` `(g ---> m) net`
-unfolding bilinear_conv_bounded_bilinear
+using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net`
by (rule bounded_bilinear.tendsto)
text{* These are special for limits out of the same vector space. *}
@@ -2065,11 +2063,11 @@
lemma bounded_linear_image:
fixes f :: "real^'m::finite \<Rightarrow> real^'n::finite"
- assumes "bounded S" "linear f"
+ assumes "bounded S" "bounded_linear f"
shows "bounded(f ` S)"
proof-
from assms(1) obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
- from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x" using linear_bounded_pos by auto
+ from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x" using bounded_linear.pos_bounded by (auto simp add: mult_ac)
{ fix x assume "x\<in>S"
hence "norm x \<le> b" using b by auto
hence "norm (f x) \<le> B * b" using B(2) apply(erule_tac x=x in allE)
@@ -2083,7 +2081,6 @@
fixes S :: "(real ^ 'n::finite) set"
shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
apply (rule bounded_linear_image, assumption)
- apply (simp only: linear_conv_bounded_linear)
apply (rule scaleR.bounded_linear_right)
done
@@ -4025,58 +4022,53 @@
subsection{* Topological properties of linear functions. *}
lemma linear_lim_0: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
- assumes "linear f" shows "(f ---> 0) (at (0))"
+ assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
proof-
- obtain B where "B>0" and B:"\<forall>x. norm (f x) \<le> B * norm x" using linear_bounded_pos[OF assms] by auto
- { fix e::real assume "e>0"
- { fix x::"real^'a" assume "norm x < e / B"
- hence "B * norm x < e" using `B>0` using mult_strict_right_mono[of "norm x" " e / B" B] unfolding real_mult_commute by auto
- hence "norm (f x) < e" using B[THEN spec[where x=x]] `B>0` using order_le_less_trans[of "norm (f x)" "B * norm x" e] by auto }
- moreover have "e / B > 0" using `e>0` `B>0` divide_pos_pos by auto
- ultimately have "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f x) 0 < e" unfolding dist_norm by auto }
- thus ?thesis unfolding Lim_at by auto
+ interpret f: bounded_linear f by fact
+ have "(f ---> f 0) (at 0)"
+ using tendsto_ident_at by (rule f.tendsto)
+ thus ?thesis unfolding f.zero .
qed
lemma bounded_linear_continuous_at:
assumes "bounded_linear f" shows "continuous (at a) f"
unfolding continuous_at using assms
apply (rule bounded_linear.tendsto)
- apply (rule Lim_at_id [unfolded id_def])
+ apply (rule tendsto_ident_at)
done
lemma linear_continuous_at:
fixes f :: "real ^ _ \<Rightarrow> real ^ _"
- assumes "linear f" shows "continuous (at a) f"
- using assms unfolding linear_conv_bounded_linear
- by (rule bounded_linear_continuous_at)
+ assumes "bounded_linear f" shows "continuous (at a) f"
+ using assms by (rule bounded_linear_continuous_at)
lemma linear_continuous_within:
fixes f :: "real ^ _ \<Rightarrow> real ^ _"
- shows "linear f ==> continuous (at x within s) f"
+ shows "bounded_linear f ==> continuous (at x within s) f"
using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
lemma linear_continuous_on:
fixes f :: "real ^ _ \<Rightarrow> real ^ _"
- shows "linear f ==> continuous_on s f"
+ 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
text{* Also bilinear functions, in composition form. *}
lemma bilinear_continuous_at_compose:
- fixes f :: "real ^ _ \<Rightarrow> real ^ _"
- shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bilinear h
+ fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
+ shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
==> continuous (at x) (\<lambda>x. h (f x) (g x))"
unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
lemma bilinear_continuous_within_compose:
fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
- shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bilinear h
+ shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
lemma bilinear_continuous_on_compose:
fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
- shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bilinear h
+ shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
==> continuous_on s (\<lambda>x. h (f x) (g x))"
unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
using bilinear_continuous_within_compose[of _ s f g h] by auto
@@ -5482,14 +5474,15 @@
lemma cauchy_isometric:
fixes x :: "nat \<Rightarrow> real ^ 'n::finite"
- assumes e:"0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"Cauchy(f o x)"
+ assumes e:"0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"Cauchy(f o x)"
shows "Cauchy x"
proof-
+ interpret f: bounded_linear f by fact
{ fix d::real assume "d>0"
then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
{ fix n assume "n\<ge>N"
- hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding linear_sub[OF f, THEN sym] by auto
+ hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding f.diff[THEN sym] by auto
moreover have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
using subspace_sub[OF s, of "x n" "x N"] using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
using normf[THEN bspec[where x="x n - x N"]] by auto
@@ -5501,7 +5494,7 @@
lemma complete_isometric_image:
fixes f :: "real ^ _ \<Rightarrow> real ^ _"
- assumes "0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and cs:"complete s"
+ assumes "0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and cs:"complete s"
shows "complete(f ` s)"
proof-
{ fix g assume as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"Cauchy g"
@@ -5524,7 +5517,7 @@
unfolding dist_norm by simp
lemma injective_imp_isometric: fixes f::"real^'m::finite \<Rightarrow> real^'n::finite"
- assumes s:"closed s" "subspace s" and f:"linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
+ assumes s:"closed s" "subspace s" and f:"bounded_linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm(x)"
proof(cases "s \<subseteq> {0::real^'m}")
case True
@@ -5533,6 +5526,7 @@
hence "norm x \<le> norm (f x)" by auto }
thus ?thesis by(auto intro!: exI[where x=1])
next
+ interpret f: bounded_linear f by fact
case False
then obtain a where a:"a\<noteq>0" "a\<in>s" by auto
from False have "s \<noteq> {}" by auto
@@ -5566,7 +5560,7 @@
have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s" using s[unfolded subspace_def smult_conv_scaleR] by auto
hence "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}" using `x\<in>s` and `x\<noteq>0` by auto
thus "norm (f b) / norm b * norm x \<le> norm (f x)" using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
- unfolding linear_cmul[OF f(1), unfolded smult_conv_scaleR] and ba using `x\<noteq>0` `a\<noteq>0`
+ unfolding f.scaleR and ba using `x\<noteq>0` `a\<noteq>0`
by (auto simp add: real_mult_commute pos_le_divide_eq pos_divide_le_eq)
qed }
ultimately
@@ -5574,8 +5568,8 @@
qed
lemma closed_injective_image_subspace:
- fixes s :: "(real ^ _) set"
- assumes "subspace s" "linear f" "\<forall>x\<in>s. f x = 0 --> x = 0" "closed s"
+ fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+ assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 --> x = 0" "closed s"
shows "closed(f ` s)"
proof-
obtain e where "e>0" and e:"\<forall>x\<in>s. e * norm x \<le> norm (f x)" using injective_imp_isometric[OF assms(4,1,2,3)] by auto
@@ -5683,10 +5677,11 @@
then obtain d::"'n set" where t: "card d = dim s"
using closed_subspace_lemma by auto
let ?t = "{x::real^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0}"
- obtain f where f:"linear f" "f ` ?t = s" "inj_on f ?t"
- using subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"] assms]
+ obtain f where f:"bounded_linear f" "f ` ?t = s" "inj_on f ?t"
+ using subspace_isomorphism[unfolded linear_conv_bounded_linear, OF subspace_substandard[of "\<lambda>i. i \<notin> d"] assms]
using dim_substandard[of d] and t by auto
- have "\<forall>x\<in>?t. f x = 0 \<longrightarrow> x = 0" using linear_0[OF f(1)] using f(3)[unfolded inj_on_def]
+ interpret f: bounded_linear f by fact
+ have "\<forall>x\<in>?t. f x = 0 \<longrightarrow> x = 0" using f.zero using f(3)[unfolded inj_on_def]
by(erule_tac x=0 in ballE) auto
moreover have "closed ?t" using closed_substandard .
moreover have "subspace ?t" using subspace_substandard .