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