author huffman Thu, 26 Sep 2013 16:33:34 -0700 changeset 53939 eb25bddf6a22 parent 53938 eb93cca4589a child 53942 fc631b2831d3 child 53943 2b761d9a74f5
tuned proofs
```--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Sep 26 16:33:32 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Sep 26 16:33:34 2013 -0700
@@ -106,7 +106,7 @@
from `0 < e` have "y \<noteq> x"
unfolding y_def by (auto intro!: nonzero_Basis)
from `0 < e` have "dist y x < e"
-      unfolding y_def by (simp add: dist_norm norm_Basis)
+      unfolding y_def by (simp add: dist_norm)
from `y \<noteq> x` and `dist y x < e` show "False"
using e by simp
qed
@@ -123,7 +123,7 @@
[simp]: "Basis = {1::real}"

instance
-  by default (auto simp add: Basis_real_def)
+  by default auto

end
```
```--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 26 16:33:32 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 26 16:33:34 2013 -0700
@@ -193,7 +193,7 @@

lemma setsum_group:
assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
-  shows "setsum (\<lambda>y. setsum g {x. x\<in> S \<and> f x = y}) T = setsum g S"
+  shows "setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) T = setsum g S"
apply (subst setsum_image_gen[OF fS, of g f])
apply (rule setsum_mono_zero_right[OF fT fST])
apply (auto intro: setsum_0')
@@ -475,7 +475,7 @@
assumes lf: "linear f"
by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]

fixes f:: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
@@ -1505,13 +1505,9 @@
apply (simp add: inner_Basis inner_setsum_right eq_commute)
done

-lemma span_Basis[simp]: "span Basis = (UNIV :: 'a::euclidean_space set)"
-  apply (subst span_finite)
-  apply simp
-  apply (safe intro!: UNIV_I)
-  apply (rule_tac x="inner x" in exI)
-  done
+lemma span_Basis [simp]: "span Basis = UNIV"
+  unfolding span_finite [OF finite_Basis]
+  by (fast intro: euclidean_representation)

lemma in_span_Basis: "x \<in> span Basis"
unfolding span_Basis ..
@@ -1566,70 +1562,33 @@
fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"
shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
-proof -
+proof
let ?B = "\<Sum>b\<in>Basis. norm (f b)"
-  {
+  show "\<forall>x. norm (f x) \<le> ?B * norm x"
+  proof
fix x :: 'a
let ?g = "\<lambda>b. (x \<bullet> b) *\<^sub>R f b"
have "norm (f x) = norm (f (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b))"
unfolding euclidean_representation ..
also have "\<dots> = norm (setsum ?g Basis)"
-      using linear_setsum[OF lf finite_Basis, of "\<lambda>b. (x \<bullet> b) *\<^sub>R b", unfolded o_def] linear_cmul[OF lf]
-      by auto
+      by (simp add: linear_setsum [OF lf] linear_cmul [OF lf])
finally have th0: "norm (f x) = norm (setsum ?g Basis)" .
-    {
+    have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x"
+    proof
fix i :: 'a
assume i: "i \<in> Basis"
from Basis_le_norm[OF i, of x]
-      have "norm (?g i) \<le> norm (f i) * norm x"
+      show "norm (?g i) \<le> norm (f i) * norm x"
unfolding norm_scaleR
apply (subst mult_commute)
apply (rule mult_mono)
done
-    }
-    then have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x"
-      by metis
+    qed
from setsum_norm_le[of _ ?g, OF th]
-    have "norm (f x) \<le> ?B * norm x"
+    show "norm (f x) \<le> ?B * norm x"
unfolding th0 setsum_left_distrib by metis
-  }
-  then show ?thesis by blast
-qed
-
-lemma linear_bounded_pos:
-  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes lf: "linear f"
-  shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
-proof -
-  from linear_bounded[OF lf] obtain B where
-    B: "\<forall>x. norm (f x) \<le> B * norm x" by blast
-  let ?K = "\<bar>B\<bar> + 1"
-  have Kp: "?K > 0" by arith
-  {
-    assume C: "B < 0"
-    def One \<equiv> "\<Sum>Basis ::'a"
-    then have "One \<noteq> 0"
-      unfolding euclidean_eq_iff[where 'a='a]
-      by (simp add: inner_setsum_left inner_Basis setsum_cases)
-    then have "norm One > 0" by auto
-    with C have "B * norm One < 0"
-    with B[rule_format, of One] norm_ge_zero[of "f One"]
-    have False by simp
-  }
-  then have Bp: "B \<ge> 0"
-    by (metis not_leE)
-  {
-    fix x::"'a"
-    have "norm (f x) \<le> ?K *  norm x"
-      using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
-      apply (erule order_trans, simp)
-      done
-  }
-  then show ?thesis
-    using Kp by blast
+  qed
qed

lemma linear_conv_bounded_linear:
@@ -1637,16 +1596,9 @@
shows "linear f \<longleftrightarrow> bounded_linear f"
proof
assume "linear f"
+  then interpret f: linear f .
show "bounded_linear f"
proof
-    fix x y
-    show "f (x + y) = f x + f y"
-      using `linear f` unfolding linear_iff by simp
-  next
-    fix r x
-    show "f (scaleR r x) = scaleR r (f x)"
-      using `linear f` unfolding linear_iff by simp
-  next
have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
using `linear f` by (rule linear_bounded)
then show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
@@ -1655,7 +1607,19 @@
next
assume "bounded_linear f"
then interpret f: bounded_linear f .
+  show "linear f" ..
+qed
+
+lemma linear_bounded_pos:
+  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  assumes lf: "linear f"
+  shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
+proof -
+  have "\<exists>B > 0. \<forall>x. norm (f x) \<le> norm x * B"
+    using lf unfolding linear_conv_bounded_linear
+    by (rule bounded_linear.pos_bounded)
+  then show ?thesis
+    by (simp only: mult_commute)
qed

lemma bounded_linearI':
@@ -1694,30 +1658,6 @@
done
qed

-lemma bilinear_bounded_pos:
-  fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
-  assumes bh: "bilinear h"
-  shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
-proof -
-  from bilinear_bounded[OF bh] obtain B where
-    B: "\<forall>x y. norm (h x y) \<le> B * norm x * norm y" by blast
-  let ?K = "\<bar>B\<bar> + 1"
-  have Kp: "?K > 0" by arith
-  have KB: "B < ?K" by arith
-  {
-    fix x :: 'a
-    fix y :: 'b
-    from KB Kp have "B * norm x * norm y \<le> ?K * norm x * norm y"
-      apply -
-      apply (rule mult_right_mono, rule mult_right_mono)
-      apply auto
-      done
-    then have "norm (h x y) \<le> ?K * norm x * norm y"
-      using B[rule_format, of x y] by simp
-  }
-  with Kp show ?thesis by blast
-qed
-
lemma bilinear_conv_bounded_bilinear:
fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
@@ -1756,6 +1696,18 @@
using h.bounded_linear_left h.bounded_linear_right by simp
qed

+lemma bilinear_bounded_pos:
+  fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
+  assumes bh: "bilinear h"
+  shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
+proof -
+  have "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> norm x * norm y * B"
+    using bh [unfolded bilinear_conv_bounded_bilinear]
+    by (rule bounded_bilinear.pos_bounded)
+  then show ?thesis
+    by (simp only: mult_ac)
+qed
+

subsection {* We continue. *}
```