src/HOL/Analysis/Operator_Norm.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69607 7cd977863194
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      HOL/Analysis/Operator_Norm.thy
     2     Author:     Amine Chaieb, University of Cambridge
     3     Author:     Brian Huffman
     4 *)
     5 
     6 section \<open>Operator Norm\<close>
     7 
     8 theory Operator_Norm
     9 imports Complex_Main
    10 begin
    11 
    12 text \<open>This formulation yields zero if \<open>'a\<close> is the trivial vector space.\<close>
    13 
    14 text%important \<open>%whitespace\<close>
    15 definition%important
    16 onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real" where
    17 "onorm f = (SUP x. norm (f x) / norm x)"
    18 
    19 proposition onorm_bound:
    20   assumes "0 \<le> b" and "\<And>x. norm (f x) \<le> b * norm x"
    21   shows "onorm f \<le> b"
    22   unfolding onorm_def
    23 proof (rule cSUP_least)
    24   fix x
    25   show "norm (f x) / norm x \<le> b"
    26     using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq)
    27 qed simp
    28 
    29 text \<open>In non-trivial vector spaces, the first assumption is redundant.\<close>
    30 
    31 lemma onorm_le:
    32   fixes f :: "'a::{real_normed_vector, perfect_space} \<Rightarrow> 'b::real_normed_vector"
    33   assumes "\<And>x. norm (f x) \<le> b * norm x"
    34   shows "onorm f \<le> b"
    35 proof (rule onorm_bound [OF _ assms])
    36   have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
    37   then obtain a :: 'a where "a \<noteq> 0" by fast
    38   have "0 \<le> b * norm a"
    39     by (rule order_trans [OF norm_ge_zero assms])
    40   with \<open>a \<noteq> 0\<close> show "0 \<le> b"
    41     by (simp add: zero_le_mult_iff)
    42 qed
    43 
    44 lemma le_onorm:
    45   assumes "bounded_linear f"
    46   shows "norm (f x) / norm x \<le> onorm f"
    47 proof -
    48   interpret f: bounded_linear f by fact
    49   obtain b where "0 \<le> b" and "\<forall>x. norm (f x) \<le> norm x * b"
    50     using f.nonneg_bounded by auto
    51   then have "\<forall>x. norm (f x) / norm x \<le> b"
    52     by (clarify, case_tac "x = 0",
    53       simp_all add: f.zero pos_divide_le_eq mult.commute)
    54   then have "bdd_above (range (\<lambda>x. norm (f x) / norm x))"
    55     unfolding bdd_above_def by fast
    56   with UNIV_I show ?thesis
    57     unfolding onorm_def by (rule cSUP_upper)
    58 qed
    59 
    60 lemma onorm:
    61   assumes "bounded_linear f"
    62   shows "norm (f x) \<le> onorm f * norm x"
    63 proof -
    64   interpret f: bounded_linear f by fact
    65   show ?thesis
    66   proof (cases)
    67     assume "x = 0"
    68     then show ?thesis by (simp add: f.zero)
    69   next
    70     assume "x \<noteq> 0"
    71     have "norm (f x) / norm x \<le> onorm f"
    72       by (rule le_onorm [OF assms])
    73     then show "norm (f x) \<le> onorm f * norm x"
    74       by (simp add: pos_divide_le_eq \<open>x \<noteq> 0\<close>)
    75   qed
    76 qed
    77 
    78 lemma onorm_pos_le:
    79   assumes f: "bounded_linear f"
    80   shows "0 \<le> onorm f"
    81   using le_onorm [OF f, where x=0] by simp
    82 
    83 lemma onorm_zero: "onorm (\<lambda>x. 0) = 0"
    84 proof (rule order_antisym)
    85   show "onorm (\<lambda>x. 0) \<le> 0"
    86     by (simp add: onorm_bound)
    87   show "0 \<le> onorm (\<lambda>x. 0)"
    88     using bounded_linear_zero by (rule onorm_pos_le)
    89 qed
    90 
    91 lemma onorm_eq_0:
    92   assumes f: "bounded_linear f"
    93   shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
    94   using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero)
    95 
    96 lemma onorm_pos_lt:
    97   assumes f: "bounded_linear f"
    98   shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)"
    99   by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f])
   100 
   101 lemma onorm_id_le: "onorm (\<lambda>x. x) \<le> 1"
   102   by (rule onorm_bound) simp_all
   103 
   104 lemma onorm_id: "onorm (\<lambda>x. x::'a::{real_normed_vector, perfect_space}) = 1"
   105 proof (rule antisym[OF onorm_id_le])
   106   have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
   107   then obtain x :: 'a where "x \<noteq> 0" by fast
   108   hence "1 \<le> norm x / norm x"
   109     by simp
   110   also have "\<dots> \<le> onorm (\<lambda>x::'a. x)"
   111     by (rule le_onorm) (rule bounded_linear_ident)
   112   finally show "1 \<le> onorm (\<lambda>x::'a. x)" .
   113 qed
   114 
   115 lemma onorm_compose:
   116   assumes f: "bounded_linear f"
   117   assumes g: "bounded_linear g"
   118   shows "onorm (f \<circ> g) \<le> onorm f * onorm g"
   119 proof (rule onorm_bound)
   120   show "0 \<le> onorm f * onorm g"
   121     by (intro mult_nonneg_nonneg onorm_pos_le f g)
   122 next
   123   fix x
   124   have "norm (f (g x)) \<le> onorm f * norm (g x)"
   125     by (rule onorm [OF f])
   126   also have "onorm f * norm (g x) \<le> onorm f * (onorm g * norm x)"
   127     by (rule mult_left_mono [OF onorm [OF g] onorm_pos_le [OF f]])
   128   finally show "norm ((f \<circ> g) x) \<le> onorm f * onorm g * norm x"
   129     by (simp add: mult.assoc)
   130 qed
   131 
   132 lemma onorm_scaleR_lemma:
   133   assumes f: "bounded_linear f"
   134   shows "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
   135 proof (rule onorm_bound)
   136   show "0 \<le> \<bar>r\<bar> * onorm f"
   137     by (intro mult_nonneg_nonneg onorm_pos_le abs_ge_zero f)
   138 next
   139   fix x
   140   have "\<bar>r\<bar> * norm (f x) \<le> \<bar>r\<bar> * (onorm f * norm x)"
   141     by (intro mult_left_mono onorm abs_ge_zero f)
   142   then show "norm (r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f * norm x"
   143     by (simp only: norm_scaleR mult.assoc)
   144 qed
   145 
   146 lemma onorm_scaleR:
   147   assumes f: "bounded_linear f"
   148   shows "onorm (\<lambda>x. r *\<^sub>R f x) = \<bar>r\<bar> * onorm f"
   149 proof (cases "r = 0")
   150   assume "r \<noteq> 0"
   151   show ?thesis
   152   proof (rule order_antisym)
   153     show "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
   154       using f by (rule onorm_scaleR_lemma)
   155   next
   156     have "bounded_linear (\<lambda>x. r *\<^sub>R f x)"
   157       using bounded_linear_scaleR_right f by (rule bounded_linear_compose)
   158     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)"
   159       by (rule onorm_scaleR_lemma)
   160     with \<open>r \<noteq> 0\<close> show "\<bar>r\<bar> * onorm f \<le> onorm (\<lambda>x. r *\<^sub>R f x)"
   161       by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
   162   qed
   163 qed (simp add: onorm_zero)
   164 
   165 lemma onorm_scaleR_left_lemma:
   166   assumes r: "bounded_linear r"
   167   shows "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
   168 proof (rule onorm_bound)
   169   fix x
   170   have "norm (r x *\<^sub>R f) = norm (r x) * norm f"
   171     by simp
   172   also have "\<dots> \<le> onorm r * norm x * norm f"
   173     by (intro mult_right_mono onorm r norm_ge_zero)
   174   finally show "norm (r x *\<^sub>R f) \<le> onorm r * norm f * norm x"
   175     by (simp add: ac_simps)
   176 qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le r)
   177 
   178 lemma onorm_scaleR_left:
   179   assumes f: "bounded_linear r"
   180   shows "onorm (\<lambda>x. r x *\<^sub>R f) = onorm r * norm f"
   181 proof (cases "f = 0")
   182   assume "f \<noteq> 0"
   183   show ?thesis
   184   proof (rule order_antisym)
   185     show "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
   186       using f by (rule onorm_scaleR_left_lemma)
   187   next
   188     have bl1: "bounded_linear (\<lambda>x. r x *\<^sub>R f)"
   189       by (metis bounded_linear_scaleR_const f)
   190     have "bounded_linear (\<lambda>x. r x * norm f)"
   191       by (metis bounded_linear_mult_const f)
   192     from onorm_scaleR_left_lemma[OF this, of "inverse (norm f)"]
   193     have "onorm r \<le> onorm (\<lambda>x. r x * norm f) * inverse (norm f)"
   194       using \<open>f \<noteq> 0\<close>
   195       by (simp add: inverse_eq_divide)
   196     also have "onorm (\<lambda>x. r x * norm f) \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
   197       by (rule onorm_bound)
   198         (auto simp: abs_mult bl1 onorm_pos_le intro!: order_trans[OF _ onorm])
   199     finally show "onorm r * norm f \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
   200       using \<open>f \<noteq> 0\<close>
   201       by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
   202   qed
   203 qed (simp add: onorm_zero)
   204 
   205 lemma onorm_neg:
   206   shows "onorm (\<lambda>x. - f x) = onorm f"
   207   unfolding onorm_def by simp
   208 
   209 lemma onorm_triangle:
   210   assumes f: "bounded_linear f"
   211   assumes g: "bounded_linear g"
   212   shows "onorm (\<lambda>x. f x + g x) \<le> onorm f + onorm g"
   213 proof (rule onorm_bound)
   214   show "0 \<le> onorm f + onorm g"
   215     by (intro add_nonneg_nonneg onorm_pos_le f g)
   216 next
   217   fix x
   218   have "norm (f x + g x) \<le> norm (f x) + norm (g x)"
   219     by (rule norm_triangle_ineq)
   220   also have "norm (f x) + norm (g x) \<le> onorm f * norm x + onorm g * norm x"
   221     by (intro add_mono onorm f g)
   222   finally show "norm (f x + g x) \<le> (onorm f + onorm g) * norm x"
   223     by (simp only: distrib_right)
   224 qed
   225 
   226 lemma onorm_triangle_le:
   227   assumes "bounded_linear f"
   228   assumes "bounded_linear g"
   229   assumes "onorm f + onorm g \<le> e"
   230   shows "onorm (\<lambda>x. f x + g x) \<le> e"
   231   using assms by (rule onorm_triangle [THEN order_trans])
   232 
   233 lemma onorm_triangle_lt:
   234   assumes "bounded_linear f"
   235   assumes "bounded_linear g"
   236   assumes "onorm f + onorm g < e"
   237   shows "onorm (\<lambda>x. f x + g x) < e"
   238   using assms by (rule onorm_triangle [THEN order_le_less_trans])
   239 
   240 lemma onorm_sum:
   241   assumes "finite S"
   242   assumes "\<And>s. s \<in> S \<Longrightarrow> bounded_linear (f s)"
   243   shows "onorm (\<lambda>x. sum (\<lambda>s. f s x) S) \<le> sum (\<lambda>s. onorm (f s)) S"
   244   using assms
   245   by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
   246 
   247 lemmas onorm_sum_le = onorm_sum[THEN order_trans]
   248 
   249 end