--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Apr 28 19:46:09 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Apr 28 15:05:45 2010 -0700
@@ -1665,6 +1665,8 @@
using u
by (simp add: vector_eq_rdot[symmetric] adjoint_clauses[OF lf])
+subsection {* Matrix operations *}
+
text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}
definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m" (infixl "**" 70)
@@ -1928,145 +1930,6 @@
ultimately show ?thesis by metis
qed
-subsection{* Operator norm. *}
-
-definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
-
-lemma norm_bound_generalize:
- fixes f:: "real ^'n \<Rightarrow> real^'m"
- assumes lf: "linear f"
- shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
- {assume H: ?rhs
- {fix x :: "real^'n" assume x: "norm x = 1"
- from H[rule_format, of x] x have "norm (f x) \<le> b" by simp}
- then have ?lhs by blast }
-
- moreover
- {assume H: ?lhs
- from H[rule_format, of "basis arbitrary"]
- have bp: "b \<ge> 0" using norm_ge_zero[of "f (basis arbitrary)"]
- by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero])
- {fix x :: "real ^'n"
- {assume "x = 0"
- then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}
- moreover
- {assume x0: "x \<noteq> 0"
- hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
- let ?c = "1/ norm x"
- have "norm (?c*s x) = 1" using x0 by (simp add: n0)
- with H have "norm (f(?c*s x)) \<le> b" by blast
- hence "?c * norm (f x) \<le> b"
- by (simp add: linear_cmul[OF lf])
- hence "norm (f x) \<le> b * norm x"
- using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
- ultimately have "norm (f x) \<le> b * norm x" by blast}
- then have ?rhs by blast}
- ultimately show ?thesis by blast
-qed
-
-lemma onorm:
- fixes f:: "real ^'n \<Rightarrow> real ^'m"
- assumes lf: "linear f"
- shows "norm (f x) <= onorm f * norm x"
- and "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
-proof-
- {
- let ?S = "{norm (f x) |x. norm x = 1}"
- have Se: "?S \<noteq> {}" using norm_basis by auto
- from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
- unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
- {from Sup[OF Se b, unfolded onorm_def[symmetric]]
- show "norm (f x) <= onorm f * norm x"
- apply -
- apply (rule spec[where x = x])
- unfolding norm_bound_generalize[OF lf, symmetric]
- by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
- {
- show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
- using Sup[OF Se b, unfolded onorm_def[symmetric]]
- unfolding norm_bound_generalize[OF lf, symmetric]
- by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
- }
-qed
-
-lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" shows "0 <= onorm f"
- using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis arbitrary"], unfolded norm_basis] by simp
-
-lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)"
- shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
- using onorm[OF lf]
- apply (auto simp add: onorm_pos_le)
- apply atomize
- apply (erule allE[where x="0::real"])
- using onorm_pos_le[OF lf]
- apply arith
- done
-
-lemma onorm_const: "onorm(\<lambda>x::real^'n. (y::real ^'m)) = norm y"
-proof-
- let ?f = "\<lambda>x::real^'n. (y::real ^ 'm)"
- have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
- by(auto intro: vector_choose_size set_ext)
- show ?thesis
- unfolding onorm_def th
- apply (rule Sup_unique) by (simp_all add: setle_def)
-qed
-
-lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n \<Rightarrow> real ^'m)"
- shows "0 < onorm f \<longleftrightarrow> ~(\<forall>x. f x = 0)"
- unfolding onorm_eq_0[OF lf, symmetric]
- using onorm_pos_le[OF lf] by arith
-
-lemma onorm_compose:
- assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)"
- and lg: "linear (g::real^'k \<Rightarrow> real^'n)"
- shows "onorm (f o g) <= onorm f * onorm g"
- apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format])
- unfolding o_def
- apply (subst mult_assoc)
- apply (rule order_trans)
- apply (rule onorm(1)[OF lf])
- apply (rule mult_mono1)
- apply (rule onorm(1)[OF lg])
- apply (rule onorm_pos_le[OF lf])
- done
-
-lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
- shows "onorm (\<lambda>x. - f x) \<le> onorm f"
- using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
- unfolding norm_minus_cancel by metis
-
-lemma onorm_neg: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
- shows "onorm (\<lambda>x. - f x) = onorm f"
- using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]]
- by simp
-
-lemma onorm_triangle:
- assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" and lg: "linear g"
- shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"
- apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
- apply (rule order_trans)
- apply (rule norm_triangle_ineq)
- apply (simp add: distrib)
- apply (rule add_mono)
- apply (rule onorm(1)[OF lf])
- apply (rule onorm(1)[OF lg])
- done
-
-lemma onorm_triangle_le: "linear (f::real ^'n \<Rightarrow> real ^'m) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) <= e
- \<Longrightarrow> onorm(\<lambda>x. f x + g x) <= e"
- apply (rule order_trans)
- apply (rule onorm_triangle)
- apply assumption+
- done
-
-lemma onorm_triangle_lt: "linear (f::real ^'n \<Rightarrow> real ^'m) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) < e
- ==> onorm(\<lambda>x. f x + g x) < e"
- apply (rule order_le_less_trans)
- apply (rule onorm_triangle)
- by assumption+
-
lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
lemma vec_add: "vec(x + y) = vec x + vec y" by (vector vec_def)