1(* Title: HOL/Hahn_Banach/Function_Norm.thy 2 Author: Gertrud Bauer, TU Munich 3*) 4 5section \<open>The norm of a function\<close> 6 7theory Function_Norm 8imports Normed_Space Function_Order 9begin 10 11subsection \<open>Continuous linear forms\<close> 12 13text \<open> 14 A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>, iff 15 it is bounded, i.e. 16 \begin{center} 17 \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> 18 \end{center} 19 In our application no other functions than linear forms are considered, so 20 we can define continuous linear forms as bounded linear forms: 21\<close> 22 23locale continuous = linearform + 24 fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>") 25 assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" 26 27declare continuous.intro [intro?] continuous_axioms.intro [intro?] 28 29lemma continuousI [intro]: 30 fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>") 31 assumes "linearform V f" 32 assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" 33 shows "continuous V f norm" 34proof 35 show "linearform V f" by fact 36 from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast 37 then show "continuous_axioms V f norm" .. 38qed 39 40 41subsection \<open>The norm of a linear form\<close> 42 43text \<open> 44 The least real number \<open>c\<close> for which holds 45 \begin{center} 46 \<open>\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> 47 \end{center} 48 is called the \<^emph>\<open>norm\<close> of \<open>f\<close>. 49 50 For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as 51 \begin{center} 52 \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> 53 \end{center} 54 55 For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. Since 56 \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this situation it 57 must be guaranteed that there is an element in this set. This element must 58 be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. Furthermore it does 59 not have to change the norm in all other cases, so it must be \<open>0\<close>, as all 60 other elements are \<open>{} \<ge> 0\<close>. 61 62 Thus we define the set \<open>B\<close> where the supremum is taken from as follows: 63 \begin{center} 64 \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close> 65 \end{center} 66 67 \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists (otherwise 68 it is undefined). 69\<close> 70 71locale fn_norm = 72 fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>") 73 fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}" 74 fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999) 75 defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)" 76 77locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm 78 79lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f" 80 by (simp add: B_def) 81 82text \<open> 83 The following lemma states that every continuous linear form on a normed 84 space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm. 85\<close> 86 87lemma (in normed_vectorspace_with_fn_norm) fn_norm_works: 88 assumes "continuous V f norm" 89 shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 90proof - 91 interpret continuous V f norm by fact 92 txt \<open>The existence of the supremum is shown using the 93 completeness of the reals. Completeness means, that every 94 non-empty bounded set of reals has a supremum.\<close> 95 have "\<exists>a. lub (B V f) a" 96 proof (rule real_complete) 97 txt \<open>First we have to show that \<open>B\<close> is non-empty:\<close> 98 have "0 \<in> B V f" .. 99 then show "\<exists>x. x \<in> B V f" .. 100 101 txt \<open>Then we have to show that \<open>B\<close> is bounded:\<close> 102 show "\<exists>c. \<forall>y \<in> B V f. y \<le> c" 103 proof - 104 txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close> 105 from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. 106 107 txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such 108 that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are 109 two cases.\<close> 110 111 define b where "b = max c 0" 112 have "\<forall>y \<in> B V f. y \<le> b" 113 proof 114 fix y assume y: "y \<in> B V f" 115 show "y \<le> b" 116 proof cases 117 assume "y = 0" 118 then show ?thesis unfolding b_def by arith 119 next 120 txt \<open>The second case is \<open>y = \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> for some 121 \<open>x \<in> V\<close> with \<open>x \<noteq> 0\<close>.\<close> 122 assume "y \<noteq> 0" 123 with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" 124 and x: "x \<in> V" and neq: "x \<noteq> 0" 125 by (auto simp add: B_def divide_inverse) 126 from x neq have gt: "0 < \<parallel>x\<parallel>" .. 127 128 txt \<open>The thesis follows by a short calculation using the 129 fact that \<open>f\<close> is bounded.\<close> 130 131 note y_rep 132 also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" 133 proof (rule mult_right_mono) 134 from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. 135 from gt have "0 < inverse \<parallel>x\<parallel>" 136 by (rule positive_imp_inverse_positive) 137 then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le) 138 qed 139 also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)" 140 by (rule Groups.mult.assoc) 141 also 142 from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp 143 then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 144 also have "c * 1 \<le> b" by (simp add: b_def) 145 finally show "y \<le> b" . 146 qed 147 qed 148 then show ?thesis .. 149 qed 150 qed 151 then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex) 152qed 153 154lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]: 155 assumes "continuous V f norm" 156 assumes b: "b \<in> B V f" 157 shows "b \<le> \<parallel>f\<parallel>\<hyphen>V" 158proof - 159 interpret continuous V f norm by fact 160 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 161 using \<open>continuous V f norm\<close> by (rule fn_norm_works) 162 from this and b show ?thesis .. 163qed 164 165lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB: 166 assumes "continuous V f norm" 167 assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y" 168 shows "\<parallel>f\<parallel>\<hyphen>V \<le> y" 169proof - 170 interpret continuous V f norm by fact 171 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 172 using \<open>continuous V f norm\<close> by (rule fn_norm_works) 173 from this and b show ?thesis .. 174qed 175 176text \<open>The norm of a continuous function is always \<open>\<ge> 0\<close>.\<close> 177 178lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]: 179 assumes "continuous V f norm" 180 shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V" 181proof - 182 interpret continuous V f norm by fact 183 txt \<open>The function norm is defined as the supremum of \<open>B\<close>. 184 So it is \<open>\<ge> 0\<close> if all elements in \<open>B\<close> are \<open>\<ge> 185 0\<close>, provided the supremum exists and \<open>B\<close> is not empty.\<close> 186 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 187 using \<open>continuous V f norm\<close> by (rule fn_norm_works) 188 moreover have "0 \<in> B V f" .. 189 ultimately show ?thesis .. 190qed 191 192text \<open> 193 \<^medskip> 194 The fundamental property of function norms is: 195 \begin{center} 196 \<open>\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close> 197 \end{center} 198\<close> 199 200lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong: 201 assumes "continuous V f norm" "linearform V f" 202 assumes x: "x \<in> V" 203 shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" 204proof - 205 interpret continuous V f norm by fact 206 interpret linearform V f by fact 207 show ?thesis 208 proof cases 209 assume "x = 0" 210 then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp 211 also have "f 0 = 0" by rule unfold_locales 212 also have "\<bar>\<dots>\<bar> = 0" by simp 213 also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V" 214 using \<open>continuous V f norm\<close> by (rule fn_norm_ge_zero) 215 from x have "0 \<le> norm x" .. 216 with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff) 217 finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" . 218 next 219 assume "x \<noteq> 0" 220 with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp 221 then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp 222 also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" 223 proof (rule mult_right_mono) 224 from x show "0 \<le> \<parallel>x\<parallel>" .. 225 from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f" 226 by (auto simp add: B_def divide_inverse) 227 with \<open>continuous V f norm\<close> show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V" 228 by (rule fn_norm_ub) 229 qed 230 finally show ?thesis . 231 qed 232qed 233 234text \<open> 235 \<^medskip> 236 The function norm is the least positive real number for which the 237 following inequality holds: 238 \begin{center} 239 \<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> 240 \end{center} 241\<close> 242 243lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]: 244 assumes "continuous V f norm" 245 assumes ineq: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c" 246 shows "\<parallel>f\<parallel>\<hyphen>V \<le> c" 247proof - 248 interpret continuous V f norm by fact 249 show ?thesis 250 proof (rule fn_norm_leastB [folded B_def fn_norm_def]) 251 fix b assume b: "b \<in> B V f" 252 show "b \<le> c" 253 proof cases 254 assume "b = 0" 255 with ge show ?thesis by simp 256 next 257 assume "b \<noteq> 0" 258 with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" 259 and x_neq: "x \<noteq> 0" and x: "x \<in> V" 260 by (auto simp add: B_def divide_inverse) 261 note b_rep 262 also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" 263 proof (rule mult_right_mono) 264 have "0 < \<parallel>x\<parallel>" using x x_neq .. 265 then show "0 \<le> inverse \<parallel>x\<parallel>" by simp 266 from x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by (rule ineq) 267 qed 268 also have "\<dots> = c" 269 proof - 270 from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp 271 then show ?thesis by simp 272 qed 273 finally show ?thesis . 274 qed 275 qed (insert \<open>continuous V f norm\<close>, simp_all add: continuous_def) 276qed 277 278end 279