# HG changeset patch
# User huffman
# Date 1395287424 25200
# Node ID 7696903b9e61efd2b8630a77dd4e716e48fc0a0a
# Parent  6599c627854544640bf07b88d6866c5b4fbe9fc6
generalize theory of operator norms to work with class real_normed_vector

diff -r 6599c6278545 -r 7696903b9e61 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Mar 19 23:13:45 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Mar 19 20:50:24 2014 -0700
@@ -269,7 +269,7 @@
     case goal1
     then show ?case
       using differentiable_bound[OF assms(1) d0', of 0 x y] and `x \<in> s`
-      unfolding onorm_const
+      unfolding onorm_zero
       by auto
   qed
   then show ?thesis 
@@ -1128,11 +1128,10 @@
       and "x \<in> s"  "y \<in> s"
     shows "norm(f x - f y) \<le> B * norm(x - y)"
   apply (rule differentiable_bound [OF cvs])
-  using assms
-  apply (auto simp: has_field_derivative_def Ball_def onorm_def)
-  apply (rule cSUP_least)
-  apply (auto simp: norm_mult)
-  apply (metis norm_one)
+  apply (rule ballI, erule df [unfolded has_field_derivative_def])
+  apply (rule ballI, rule onorm_le, simp add: norm_mult mult_right_mono dn)
+  apply fact
+  apply fact
   done
 
 subsection{*Inverse function theorem for complex derivatives.*}
@@ -1405,4 +1404,3 @@
 qed
 
 end
-
diff -r 6599c6278545 -r 7696903b9e61 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Mar 19 23:13:45 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Mar 19 20:50:24 2014 -0700
@@ -766,7 +766,7 @@
 text {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *}
 
 lemma mvt_general:
-  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  fixes f :: "real \<Rightarrow> 'a::real_inner"
   assumes "a < b"
     and "continuous_on {a .. b} f"
     and "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
@@ -813,7 +813,7 @@
 text {* Still more general bound theorem. *}
 
 lemma differentiable_bound:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
   assumes "convex s"
     and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
     and "\<forall>x\<in>s. onorm (f' x) \<le> B"
@@ -863,7 +863,7 @@
   proof -
     case goal1
     have "norm (f' x y) \<le> onorm (f' x) * norm y"
-      by (rule onorm(1)[OF derivative_is_linear[OF assms(2)[rule_format,OF goal1]]])
+      by (rule onorm[OF derivative_linear[OF assms(2)[rule_format,OF goal1]]])
     also have "\<dots> \<le> B * norm y"
       apply (rule mult_right_mono)
       using assms(3)[rule_format,OF goal1]
@@ -885,19 +885,6 @@
     by (auto simp add: norm_minus_commute)
 qed
 
-lemma differentiable_bound_real:
-  fixes f :: "real \<Rightarrow> real"
-  assumes "convex s"
-    and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
-    and "\<forall>x\<in>s. onorm (f' x) \<le> B"
-    and x: "x \<in> s"
-    and y: "y \<in> s"
-  shows "norm (f x - f y) \<le> B * norm (x - y)"
-  using differentiable_bound[of s f f' B x y]
-  unfolding Ball_def image_iff o_def
-  using assms
-  by auto
-
 text {* In particular. *}
 
 lemma has_derivative_zero_constant:
@@ -913,8 +900,8 @@
   proof -
     case goal1
     then show ?case
-      using differentiable_bound_real[OF assms(1-2), of 0 x y] and `x \<in> s`
-      unfolding onorm_const
+      using differentiable_bound[OF assms(1-2), of 0 x y] and `x \<in> s`
+      unfolding onorm_zero
       by auto
   qed
   then show ?thesis
@@ -1526,7 +1513,7 @@
     apply auto
     done
   then have *: "0 < onorm g'"
-    unfolding onorm_pos_lt[OF assms(3)[unfolded linear_linear]]
+    unfolding onorm_pos_lt[OF assms(3)]
     by fastforce
   def k \<equiv> "1 / onorm g' / 2"
   have *: "k > 0"
@@ -1590,14 +1577,13 @@
         have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)"
           unfolding *
           apply (rule onorm_compose)
-          unfolding linear_conv_bounded_linear
           apply (rule assms(3) **)+
           done
         also have "\<dots> \<le> onorm g' * k"
           apply (rule mult_left_mono)
           using d1(2)[of u]
-          using onorm_neg[OF **(1)[unfolded linear_linear]]
-          using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]]
+          using onorm_neg[where f="\<lambda>x. f' u x - f' a x"]
+          using d and u and onorm_pos_le[OF assms(3)]
           apply (auto simp add: algebra_simps)
           done
         also have "\<dots> \<le> 1 / 2"
@@ -1652,10 +1638,7 @@
     }
     then show "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e"
       apply -
-      apply (rule onorm(2))
-      apply (rule linear_compose_sub)
-      unfolding linear_conv_bounded_linear
-      using assms(2)[rule_format,OF `x \<in> s`, THEN derivative_linear]
+      apply (rule onorm_le)
       apply auto
       done
   qed
diff -r 6599c6278545 -r 7696903b9e61 src/HOL/Multivariate_Analysis/Operator_Norm.thy
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Wed Mar 19 23:13:45 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Wed Mar 19 20:50:24 2014 -0700
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Multivariate_Analysis/Operator_Norm.thy
     Author:     Amine Chaieb, University of Cambridge
+    Author:     Brian Huffman
 *)
 
 header {* Operator Norm *}
@@ -8,176 +9,176 @@
 imports Linear_Algebra
 begin
 
-definition "onorm f = (SUP x:{x. norm x = 1}. norm (f x))"
+text {* This formulation yields zero if @{text 'a} is the trivial vector space. *}
+
+definition onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real"
+  where "onorm f = (SUP x. norm (f x) / norm x)"
+
+lemma onorm_bound:
+  assumes "0 \<le> b" and "\<And>x. norm (f x) \<le> b * norm x"
+  shows "onorm f \<le> b"
+  unfolding onorm_def
+proof (rule cSUP_least)
+  fix x
+  show "norm (f x) / norm x \<le> b"
+    using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq)
+qed simp
+
+text {* In non-trivial vector spaces, the first assumption is redundant. *}
 
-lemma norm_bound_generalize:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  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 :: "'a"
-    assume x: "norm x = 1"
-    from H[rule_format, of x] x have "norm (f x) \<le> b"
-      by simp
-  }
-  then show ?lhs by blast
-next
-  assume H: ?lhs
-  have bp: "b \<ge> 0"
-    apply -
-    apply (rule order_trans [OF norm_ge_zero])
-    apply (rule H[rule_format, of "SOME x::'a. x \<in> Basis"])
-    apply (auto intro: SOME_Basis norm_Basis)
-    done
-  {
-    fix x :: "'a"
-    {
-      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"
-      then have n0: "norm x \<noteq> 0"
-        by (metis norm_eq_zero)
-      let ?c = "1/ norm x"
-      have "norm (?c *\<^sub>R x) = 1"
-        using x0 by (simp add: n0)
-      with H have "norm (f (?c *\<^sub>R x)) \<le> b"
-        by blast
-      then have "?c * norm (f x) \<le> b"
-        by (simp add: linear_cmul[OF lf])
-      then have "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 show ?rhs by blast
+lemma onorm_le:
+  fixes f :: "'a::{real_normed_vector, perfect_space} \<Rightarrow> 'b::real_normed_vector"
+  assumes "\<And>x. norm (f x) \<le> b * norm x"
+  shows "onorm f \<le> b"
+proof (rule onorm_bound [OF _ assms])
+  have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
+  then obtain a :: 'a where "a \<noteq> 0" by fast
+  have "0 \<le> b * norm a"
+    by (rule order_trans [OF norm_ge_zero assms])
+  with `a \<noteq> 0` show "0 \<le> b"
+    by (simp add: zero_le_mult_iff)
+qed
+
+lemma le_onorm:
+  assumes "bounded_linear f"
+  shows "norm (f x) / norm x \<le> onorm f"
+proof -
+  interpret f: bounded_linear f by fact
+  obtain b where "0 \<le> b" and "\<forall>x. norm (f x) \<le> norm x * b"
+    using f.nonneg_bounded by auto
+  then have "\<forall>x. norm (f x) / norm x \<le> b"
+    by (clarify, case_tac "x = 0",
+      simp_all add: f.zero pos_divide_le_eq mult_commute)
+  then have "bdd_above (range (\<lambda>x. norm (f x) / norm x))"
+    unfolding bdd_above_def by fast
+  with UNIV_I show ?thesis
+    unfolding onorm_def by (rule cSUP_upper)
 qed
 
 lemma onorm:
-  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes lf: "linear f"
+  assumes "bounded_linear f"
   shows "norm (f x) \<le> onorm f * norm x"
-    and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
 proof -
-  let ?S = "(\<lambda>x. norm (f x))`{x. norm x = 1}"
-  have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
-    by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
-  then have Se: "?S \<noteq> {}"
-    by auto
-  from linear_bounded[OF lf] have b: "bdd_above ?S"
-    unfolding norm_bound_generalize[OF lf, symmetric] by auto
-  then show "norm (f x) \<le> onorm f * norm x"
-    apply -
-    apply (rule spec[where x = x])
-    unfolding norm_bound_generalize[OF lf, symmetric]
-    apply (auto simp: onorm_def intro!: cSUP_upper)
-    done
-  show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
-    unfolding norm_bound_generalize[OF lf, symmetric]
-    using Se by (auto simp: onorm_def intro!: cSUP_least b)
+  interpret f: bounded_linear f by fact
+  show ?thesis
+  proof (cases)
+    assume "x = 0"
+    then show ?thesis by (simp add: f.zero)
+  next
+    assume "x \<noteq> 0"
+    have "norm (f x) / norm x \<le> onorm f"
+      by (rule le_onorm [OF assms])
+    then show "norm (f x) \<le> onorm f * norm x"
+      by (simp add: pos_divide_le_eq `x \<noteq> 0`)
+  qed
 qed
 
 lemma onorm_pos_le:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes lf: "linear f"
+  assumes f: "bounded_linear f"
   shows "0 \<le> onorm f"
-  using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \<in> Basis"]]
-  by (simp add: SOME_Basis)
+  using le_onorm [OF f, where x=0] by simp
+
+lemma onorm_zero: "onorm (\<lambda>x. 0) = 0"
+proof (rule order_antisym)
+  show "onorm (\<lambda>x. 0) \<le> 0"
+    by (simp add: onorm_bound)
+  show "0 \<le> onorm (\<lambda>x. 0)"
+    using bounded_linear_zero by (rule onorm_pos_le)
+qed
 
 lemma onorm_eq_0:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes lf: "linear f"
+  assumes f: "bounded_linear f"
   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::'a::euclidean_space. y::'b::euclidean_space) = norm y"
-  using SOME_Basis by (auto simp add: onorm_def intro!: cSUP_const norm_Basis)
+  using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero)
 
 lemma onorm_pos_lt:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes lf: "linear f"
+  assumes f: "bounded_linear f"
   shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)"
-  unfolding onorm_eq_0[OF lf, symmetric]
-  using onorm_pos_le[OF lf] by arith
+  by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f])
 
 lemma onorm_compose:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-    and g :: "'k::euclidean_space \<Rightarrow> 'n::euclidean_space"
-  assumes lf: "linear f"
-    and lg: "linear g"
+  assumes f: "bounded_linear f"
+  assumes g: "bounded_linear g"
   shows "onorm (f \<circ> g) \<le> 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_left_mono)
-    apply (rule onorm(1)[OF lg])
-    apply (rule onorm_pos_le[OF lf])
-    done
+proof (rule onorm_bound)
+  show "0 \<le> onorm f * onorm g"
+    by (intro mult_nonneg_nonneg onorm_pos_le f g)
+next
+  fix x
+  have "norm (f (g x)) \<le> onorm f * norm (g x)"
+    by (rule onorm [OF f])
+  also have "onorm f * norm (g x) \<le> onorm f * (onorm g * norm x)"
+    by (rule mult_left_mono [OF onorm [OF g] onorm_pos_le [OF f]])
+  finally show "norm ((f \<circ> g) x) \<le> onorm f * onorm g * norm x"
+    by (simp add: mult_assoc)
+qed
 
-lemma onorm_neg_lemma:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes lf: "linear f"
-  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_scaleR_lemma:
+  assumes f: "bounded_linear f"
+  shows "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
+proof (rule onorm_bound)
+  show "0 \<le> \<bar>r\<bar> * onorm f"
+    by (intro mult_nonneg_nonneg onorm_pos_le abs_ge_zero f)
+next
+  fix x
+  have "\<bar>r\<bar> * norm (f x) \<le> \<bar>r\<bar> * (onorm f * norm x)"
+    by (intro mult_left_mono onorm abs_ge_zero f)
+  then show "norm (r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f * norm x"
+    by (simp only: norm_scaleR mult_assoc)
+qed
+
+lemma onorm_scaleR:
+  assumes f: "bounded_linear f"
+  shows "onorm (\<lambda>x. r *\<^sub>R f x) = \<bar>r\<bar> * onorm f"
+proof (cases "r = 0")
+  assume "r \<noteq> 0"
+  show ?thesis
+  proof (rule order_antisym)
+    show "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
+      using f by (rule onorm_scaleR_lemma)
+  next
+    have "bounded_linear (\<lambda>x. r *\<^sub>R f x)"
+      using bounded_linear_scaleR_right f by (rule bounded_linear_compose)
+    then have "onorm (\<lambda>x. inverse r *\<^sub>R r *\<^sub>R f x) \<le> \<bar>inverse r\<bar> * onorm (\<lambda>x. r *\<^sub>R f x)"
+      by (rule onorm_scaleR_lemma)
+    with `r \<noteq> 0` show "\<bar>r\<bar> * onorm f \<le> onorm (\<lambda>x. r *\<^sub>R f x)"
+      by (simp add: inverse_eq_divide pos_le_divide_eq mult_commute)
+  qed
+qed (simp add: onorm_zero)
 
 lemma onorm_neg:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes lf: "linear f"
   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
+  unfolding onorm_def by simp
 
 lemma onorm_triangle:
-  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes lf: "linear f"
-    and lg: "linear g"
+  assumes f: "bounded_linear f"
+  assumes g: "bounded_linear g"
   shows "onorm (\<lambda>x. f x + g x) \<le> 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
+proof (rule onorm_bound)
+  show "0 \<le> onorm f + onorm g"
+    by (intro add_nonneg_nonneg onorm_pos_le f g)
+next
+  fix x
+  have "norm (f x + g x) \<le> norm (f x) + norm (g x)"
+    by (rule norm_triangle_ineq)
+  also have "norm (f x) + norm (g x) \<le> onorm f * norm x + onorm g * norm x"
+    by (intro add_mono onorm f g)
+  finally show "norm (f x + g x) \<le> (onorm f + onorm g) * norm x"
+    by (simp only: distrib_right)
+qed
 
 lemma onorm_triangle_le:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "linear f"
-    and "linear g"
-    and "onorm f + onorm g \<le> e"
+  assumes "bounded_linear f"
+  assumes "bounded_linear g"
+  assumes "onorm f + onorm g \<le> e"
   shows "onorm (\<lambda>x. f x + g x) \<le> e"
-  apply (rule order_trans)
-  apply (rule onorm_triangle)
-  apply (rule assms)+
-  done
+  using assms by (rule onorm_triangle [THEN order_trans])
 
 lemma onorm_triangle_lt:
-  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "linear f"
-    and "linear g"
-    and "onorm f + onorm g < e"
+  assumes "bounded_linear f"
+  assumes "bounded_linear g"
+  assumes "onorm f + onorm g < e"
   shows "onorm (\<lambda>x. f x + g x) < e"
-  apply (rule order_le_less_trans)
-  apply (rule onorm_triangle)
-  apply (rule assms)+
-  done
+  using assms by (rule onorm_triangle [THEN order_le_less_trans])
 
 end