--- 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"
shows "linear (adjoint f)"
by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
- adjoint_clauses[OF lf] inner_simps)
+ adjoint_clauses[OF lf] inner_distrib)
lemma adjoint_adjoint:
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)
- apply (simp add: euclidean_representation)
- 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)
apply (auto simp add: field_simps)
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"
- by (simp add: mult_less_0_iff)
- 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 (auto simp add: field_simps split add: abs_split)
- 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" by (simp add: f.add f.scaleR linear_iff)
+ 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. *}