# HG changeset patch
# User huffman
# Date 1244496489 25200
# Node ID 689f5dae1f417c8814dabdbf66247dd9206cd4ae
# Parent  c701f4085ca44ae4eb7256b5eed1fbb299ac4a75
lemmas about linear, bilinear

diff -r c701f4085ca4 -r 689f5dae1f41 src/HOL/Library/Euclidean_Space.thy
--- 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)"
diff -r c701f4085ca4 -r 689f5dae1f41 src/HOL/Library/Topology_Euclidean_Space.thy
--- 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. *}