(*  Title:      HOL/Multivariate_Analysis/Operator_Norm.thy

     Author:     Amine Chaieb, University of Cambridge

 *)

 header {* Operator Norm *}

 theory Operator_Norm

 imports Linear_Algebra

 begin

 definition "onorm f = (SUP x:{x. norm x = 1}. norm (f x))"

 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

 qed

 lemma onorm:

   fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"

   assumes lf: "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)

 qed

 lemma onorm_pos_le:

   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"

   assumes lf: "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)

 lemma onorm_eq_0:

   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"

   assumes lf: "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)

 lemma onorm_pos_lt:

   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"

   assumes lf: "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

 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"

   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

 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_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

 lemma onorm_triangle:

   fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"

   assumes lf: "linear f"

     and lg: "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

 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"

   shows "onorm (\<lambda>x. f x + g x) \<le> e"

   apply (rule order_trans)

   apply (rule onorm_triangle)

   apply (rule assms)+

   done

 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"

   shows "onorm (\<lambda>x. f x + g x) < e"

   apply (rule order_le_less_trans)

   apply (rule onorm_triangle)

   apply (rule assms)+

   done

 end