--- a/src/HOL/Library/Euclidean_Space.thy Mon Jun 08 12:09:43 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy Mon Jun 08 14:28:09 2009 -0700
@@ -1828,6 +1828,36 @@
then show ?thesis using Kp by blast
qed
+lemma smult_conv_scaleR: "c *s x = scaleR c x"
+ unfolding vector_scalar_mult_def vector_scaleR_def by simp
+
+lemma linear_conv_bounded_linear:
+ fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+ shows "linear f \<longleftrightarrow> bounded_linear f"
+proof
+ assume "linear f"
+ show "bounded_linear f"
+ proof
+ fix x y show "f (x + y) = f x + f y"
+ using `linear f` unfolding linear_def by simp
+ next
+ fix r x show "f (scaleR r x) = scaleR r (f x)"
+ using `linear f` unfolding linear_def
+ by (simp add: smult_conv_scaleR)
+ next
+ have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
+ using `linear f` by (rule linear_bounded)
+ thus "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
+ by (simp add: mult_commute)
+ qed
+next
+ assume "bounded_linear f"
+ then interpret f: bounded_linear f .
+ show "linear f"
+ unfolding linear_def smult_conv_scaleR
+ by (simp add: f.add f.scaleR)
+qed
+
subsection{* Bilinear functions. *}
definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))"
@@ -1931,6 +1961,41 @@
with Kp show ?thesis by blast
qed
+lemma bilinear_conv_bounded_bilinear:
+ fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
+ shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
+proof
+ assume "bilinear h"
+ show "bounded_bilinear h"
+ proof
+ fix x y z show "h (x + y) z = h x z + h y z"
+ using `bilinear h` unfolding bilinear_def linear_def by simp
+ next
+ fix x y z show "h x (y + z) = h x y + h x z"
+ using `bilinear h` unfolding bilinear_def linear_def by simp
+ next
+ fix r x y show "h (scaleR r x) y = scaleR r (h x y)"
+ using `bilinear h` unfolding bilinear_def linear_def
+ by (simp add: smult_conv_scaleR)
+ next
+ fix r x y show "h x (scaleR r y) = scaleR r (h x y)"
+ using `bilinear h` unfolding bilinear_def linear_def
+ by (simp add: smult_conv_scaleR)
+ next
+ have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
+ using `bilinear h` by (rule bilinear_bounded)
+ thus "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
+ by (simp add: mult_ac)
+ qed
+next
+ assume "bounded_bilinear h"
+ then interpret h: bounded_bilinear h .
+ show "bilinear h"
+ unfolding bilinear_def linear_conv_bounded_linear
+ using h.bounded_linear_left h.bounded_linear_right
+ by simp
+qed
+
subsection{* Adjoints. *}
definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Jun 08 12:09:43 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Jun 08 14:28:09 2009 -0700
@@ -1241,22 +1241,9 @@
lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)"
assumes "(f ---> l) net" "linear h"
shows "((\<lambda>x. h (f x)) ---> h l) net"
-proof -
- obtain b where b: "b>0" "\<forall>x. norm (h x) \<le> b * norm x"
- using assms(2) using linear_bounded_pos[of h] by auto
- { fix e::real assume "e >0"
- hence "e/b > 0" using `b>0` by (metis divide_pos_pos)
- with `(f ---> l) net` have "eventually (\<lambda>x. dist (f x) l < e/b) net"
- by (rule tendstoD)
- then have "eventually (\<lambda>x. dist (h (f x)) (h l) < e) net"
- apply (rule eventually_rev_mono [rule_format])
- apply (simp add: dist_norm linear_sub [OF `linear h`, symmetric])
- apply (rule le_less_trans [OF b(2) [rule_format]])
- apply (simp add: pos_less_divide_eq `0 < b` mult_commute)
- done
- }
- thus ?thesis unfolding tendsto_iff by simp
-qed
+using `linear h` `(f ---> l) net`
+unfolding linear_conv_bounded_linear
+by (rule bounded_linear.tendsto)
lemma Lim_const: "((\<lambda>x. a) ---> a) net"
by (rule tendsto_const)
@@ -1432,76 +1419,15 @@
shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
unfolding Lim_def using Lim_unique[of net f] by auto
-text{* Limit under bilinear function (surprisingly tedious, but important) *}
-
-lemma norm_bound_lemma:
- "0 < e \<Longrightarrow> \<exists>d>0. \<forall>(x'::real^'b::finite) y'::real^'a::finite. norm(x' - (x::real^'b)) < d \<and> norm(y' - y) < d \<longrightarrow> norm(x') * norm(y' - y) + norm(x' - x) * norm(y) < e"
-proof-
- assume e: "0 < e"
- have th1: "(2 * norm x + 2 * norm y + 2) > 0" using norm_ge_zero[of x] norm_ge_zero[of y] by norm
- hence th0: "0 < e / (2 * norm x + 2 * norm y + 2)" using `e>0` using divide_pos_pos by auto
- moreover
- { fix x' y'
- assume h: "norm (x' - x) < 1" "norm (x' - x) < e / (2 * norm x + 2 * norm y + 2)"
- "norm (y' - y) < 1" "norm (y' - y) < e / (2 * norm x + 2 * norm y + 2)"
- have th: "\<And>a b (c::real). a \<ge> 0 \<Longrightarrow> c \<ge> 0 \<Longrightarrow> a + (b + c) < e ==> b < e " by arith
- from h have thx: "norm (x' - x) * norm y < e / 2"
- using th0 th1 apply (simp add: field_simps)
- apply (rule th) defer defer apply assumption
- by (simp_all add: norm_ge_zero zero_le_mult_iff)
-
- have "norm x' - norm x < 1" apply(rule le_less_trans)
- using h(1) using norm_triangle_ineq2[of x' x] by auto
- hence *:"norm x' < 1 + norm x" by auto
-
- have thy: "norm (y' - y) * norm x' < e / (2 * norm x + 2 * norm y + 2) * (1 + norm x)"
- using mult_strict_mono'[OF h(4) * norm_ge_zero norm_ge_zero] by auto
- also have "\<dots> \<le> e/2" apply simp unfolding divide_le_eq
- using th1 th0 `e>0` by auto
-
- finally have "norm x' * norm (y' - y) + norm (x' - x) * norm y < e"
- using thx and e by (simp add: field_simps) }
- ultimately show ?thesis apply(rule_tac x="min 1 (e / 2 / (norm x + norm y + 1))" in exI) by auto
-qed
+text{* Limit under bilinear function *}
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"
shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
-proof -
- obtain B where "B>0" and B:"\<forall>x y. norm (h x y) \<le> B * norm x * norm y" using bilinear_bounded_pos[OF assms(3)] by auto
- { fix e::real assume "e>0"
- obtain d where "d>0" and d:"\<forall>x' y'. norm (x' - l) < d \<and> norm (y' - m) < d \<longrightarrow> norm x' * norm (y' - m) + norm (x' - l) * norm m < e / B" using `B>0` `e>0`
- using norm_bound_lemma[of "e / B" l m] using divide_pos_pos by auto
-
- have *:"\<And>x y. h (f x) (g x) - h l m = h (f x) (g x - m) + h (f x - l) m"
- unfolding bilinear_rsub[OF assms(3)]
- unfolding bilinear_lsub[OF assms(3)] by auto
-
- have "eventually (\<lambda>x. dist (f x) l < d) net"
- using assms(1) `d>0` by (rule tendstoD)
- moreover
- have "eventually (\<lambda>x. dist (g x) m < d) net"
- using assms(2) `d>0` by (rule tendstoD)
- ultimately
- have "eventually (\<lambda>x. dist (f x) l < d \<and> dist (g x) m < d) net"
- by (rule eventually_conjI)
- moreover
- { fix x assume "dist (f x) l < d \<and> dist (g x) m < d"
- hence **:"norm (f x) * norm (g x - m) + norm (f x - l) * norm m < e / B"
- using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_norm by auto
- have "norm (h (f x) (g x - m)) + norm (h (f x - l) m) \<le> B * norm (f x) * norm (g x - m) + B * norm (f x - l) * norm m"
- using B[THEN spec[where x="f x"], THEN spec[where x="g x - m"]]
- using B[THEN spec[where x="f x - l"], THEN spec[where x="m"]] by auto
- also have "\<dots> < e" using ** and `B>0` by(auto simp add: field_simps)
- finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_norm and * using norm_triangle_lt by auto
- }
- ultimately have "eventually (\<lambda>x. dist (h (f x) (g x)) (h l m) < e) net"
- by (auto elim: eventually_rev_mono)
- }
- thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net"
- unfolding tendsto_iff by simp
-qed
+using `bilinear h` `(f ---> l) net` `(g ---> m) net`
+unfolding bilinear_conv_bounded_bilinear
+by (rule bounded_bilinear.tendsto)
text{* These are special for limits out of the same vector space. *}