1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/HahnBanach/FunctionNorm.thy Tue Dec 30 11:10:01 2008 +0100
1.3 @@ -0,0 +1,278 @@
1.4 +(* Title: HOL/Real/HahnBanach/FunctionNorm.thy
1.5 + Author: Gertrud Bauer, TU Munich
1.6 +*)
1.7 +
1.8 +header {* The norm of a function *}
1.9 +
1.10 +theory FunctionNorm
1.11 +imports NormedSpace FunctionOrder
1.12 +begin
1.13 +
1.14 +subsection {* Continuous linear forms*}
1.15 +
1.16 +text {*
1.17 + A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
1.18 + is \emph{continuous}, iff it is bounded, i.e.
1.19 + \begin{center}
1.20 + @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
1.21 + \end{center}
1.22 + In our application no other functions than linear forms are
1.23 + considered, so we can define continuous linear forms as bounded
1.24 + linear forms:
1.25 +*}
1.26 +
1.27 +locale continuous = var_V + norm_syntax + linearform +
1.28 + assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
1.29 +
1.30 +declare continuous.intro [intro?] continuous_axioms.intro [intro?]
1.31 +
1.32 +lemma continuousI [intro]:
1.33 + fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>")
1.34 + assumes "linearform V f"
1.35 + assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
1.36 + shows "continuous V norm f"
1.37 +proof
1.38 + show "linearform V f" by fact
1.39 + from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
1.40 + then show "continuous_axioms V norm f" ..
1.41 +qed
1.42 +
1.43 +
1.44 +subsection {* The norm of a linear form *}
1.45 +
1.46 +text {*
1.47 + The least real number @{text c} for which holds
1.48 + \begin{center}
1.49 + @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
1.50 + \end{center}
1.51 + is called the \emph{norm} of @{text f}.
1.52 +
1.53 + For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
1.54 + defined as
1.55 + \begin{center}
1.56 + @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
1.57 + \end{center}
1.58 +
1.59 + For the case @{text "V = {0}"} the supremum would be taken from an
1.60 + empty set. Since @{text \<real>} is unbounded, there would be no supremum.
1.61 + To avoid this situation it must be guaranteed that there is an
1.62 + element in this set. This element must be @{text "{} \<ge> 0"} so that
1.63 + @{text fn_norm} has the norm properties. Furthermore it does not
1.64 + have to change the norm in all other cases, so it must be @{text 0},
1.65 + as all other elements are @{text "{} \<ge> 0"}.
1.66 +
1.67 + Thus we define the set @{text B} where the supremum is taken from as
1.68 + follows:
1.69 + \begin{center}
1.70 + @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
1.71 + \end{center}
1.72 +
1.73 + @{text fn_norm} is equal to the supremum of @{text B}, if the
1.74 + supremum exists (otherwise it is undefined).
1.75 +*}
1.76 +
1.77 +locale fn_norm = norm_syntax +
1.78 + fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
1.79 + fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
1.80 + defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
1.81 +
1.82 +locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm
1.83 +
1.84 +lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
1.85 + by (simp add: B_def)
1.86 +
1.87 +text {*
1.88 + The following lemma states that every continuous linear form on a
1.89 + normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
1.90 +*}
1.91 +
1.92 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
1.93 + assumes "continuous V norm f"
1.94 + shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
1.95 +proof -
1.96 + interpret continuous V norm f by fact
1.97 + txt {* The existence of the supremum is shown using the
1.98 + completeness of the reals. Completeness means, that every
1.99 + non-empty bounded set of reals has a supremum. *}
1.100 + have "\<exists>a. lub (B V f) a"
1.101 + proof (rule real_complete)
1.102 + txt {* First we have to show that @{text B} is non-empty: *}
1.103 + have "0 \<in> B V f" ..
1.104 + then show "\<exists>x. x \<in> B V f" ..
1.105 +
1.106 + txt {* Then we have to show that @{text B} is bounded: *}
1.107 + show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
1.108 + proof -
1.109 + txt {* We know that @{text f} is bounded by some value @{text c}. *}
1.110 + from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
1.111 +
1.112 + txt {* To prove the thesis, we have to show that there is some
1.113 + @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
1.114 + B"}. Due to the definition of @{text B} there are two cases. *}
1.115 +
1.116 + def b \<equiv> "max c 0"
1.117 + have "\<forall>y \<in> B V f. y \<le> b"
1.118 + proof
1.119 + fix y assume y: "y \<in> B V f"
1.120 + show "y \<le> b"
1.121 + proof cases
1.122 + assume "y = 0"
1.123 + then show ?thesis unfolding b_def by arith
1.124 + next
1.125 + txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
1.126 + @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
1.127 + assume "y \<noteq> 0"
1.128 + with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
1.129 + and x: "x \<in> V" and neq: "x \<noteq> 0"
1.130 + by (auto simp add: B_def real_divide_def)
1.131 + from x neq have gt: "0 < \<parallel>x\<parallel>" ..
1.132 +
1.133 + txt {* The thesis follows by a short calculation using the
1.134 + fact that @{text f} is bounded. *}
1.135 +
1.136 + note y_rep
1.137 + also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
1.138 + proof (rule mult_right_mono)
1.139 + from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
1.140 + from gt have "0 < inverse \<parallel>x\<parallel>"
1.141 + by (rule positive_imp_inverse_positive)
1.142 + then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
1.143 + qed
1.144 + also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
1.145 + by (rule real_mult_assoc)
1.146 + also
1.147 + from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
1.148 + then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp
1.149 + also have "c * 1 \<le> b" by (simp add: b_def le_maxI1)
1.150 + finally show "y \<le> b" .
1.151 + qed
1.152 + qed
1.153 + then show ?thesis ..
1.154 + qed
1.155 + qed
1.156 + then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
1.157 +qed
1.158 +
1.159 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
1.160 + assumes "continuous V norm f"
1.161 + assumes b: "b \<in> B V f"
1.162 + shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
1.163 +proof -
1.164 + interpret continuous V norm f by fact
1.165 + have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
1.166 + using `continuous V norm f` by (rule fn_norm_works)
1.167 + from this and b show ?thesis ..
1.168 +qed
1.169 +
1.170 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
1.171 + assumes "continuous V norm f"
1.172 + assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
1.173 + shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
1.174 +proof -
1.175 + interpret continuous V norm f by fact
1.176 + have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
1.177 + using `continuous V norm f` by (rule fn_norm_works)
1.178 + from this and b show ?thesis ..
1.179 +qed
1.180 +
1.181 +text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
1.182 +
1.183 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
1.184 + assumes "continuous V norm f"
1.185 + shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
1.186 +proof -
1.187 + interpret continuous V norm f by fact
1.188 + txt {* The function norm is defined as the supremum of @{text B}.
1.189 + So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
1.190 + 0"}, provided the supremum exists and @{text B} is not empty. *}
1.191 + have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
1.192 + using `continuous V norm f` by (rule fn_norm_works)
1.193 + moreover have "0 \<in> B V f" ..
1.194 + ultimately show ?thesis ..
1.195 +qed
1.196 +
1.197 +text {*
1.198 + \medskip The fundamental property of function norms is:
1.199 + \begin{center}
1.200 + @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
1.201 + \end{center}
1.202 +*}
1.203 +
1.204 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
1.205 + assumes "continuous V norm f" "linearform V f"
1.206 + assumes x: "x \<in> V"
1.207 + shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
1.208 +proof -
1.209 + interpret continuous V norm f by fact
1.210 + interpret linearform V f .
1.211 + show ?thesis
1.212 + proof cases
1.213 + assume "x = 0"
1.214 + then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
1.215 + also have "f 0 = 0" by rule unfold_locales
1.216 + also have "\<bar>\<dots>\<bar> = 0" by simp
1.217 + also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
1.218 + using `continuous V norm f` by (rule fn_norm_ge_zero)
1.219 + from x have "0 \<le> norm x" ..
1.220 + with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
1.221 + finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
1.222 + next
1.223 + assume "x \<noteq> 0"
1.224 + with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
1.225 + then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
1.226 + also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
1.227 + proof (rule mult_right_mono)
1.228 + from x show "0 \<le> \<parallel>x\<parallel>" ..
1.229 + from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
1.230 + by (auto simp add: B_def real_divide_def)
1.231 + with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
1.232 + by (rule fn_norm_ub)
1.233 + qed
1.234 + finally show ?thesis .
1.235 + qed
1.236 +qed
1.237 +
1.238 +text {*
1.239 + \medskip The function norm is the least positive real number for
1.240 + which the following inequation holds:
1.241 + \begin{center}
1.242 + @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
1.243 + \end{center}
1.244 +*}
1.245 +
1.246 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
1.247 + assumes "continuous V norm f"
1.248 + assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
1.249 + shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
1.250 +proof -
1.251 + interpret continuous V norm f by fact
1.252 + show ?thesis
1.253 + proof (rule fn_norm_leastB [folded B_def fn_norm_def])
1.254 + fix b assume b: "b \<in> B V f"
1.255 + show "b \<le> c"
1.256 + proof cases
1.257 + assume "b = 0"
1.258 + with ge show ?thesis by simp
1.259 + next
1.260 + assume "b \<noteq> 0"
1.261 + with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
1.262 + and x_neq: "x \<noteq> 0" and x: "x \<in> V"
1.263 + by (auto simp add: B_def real_divide_def)
1.264 + note b_rep
1.265 + also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
1.266 + proof (rule mult_right_mono)
1.267 + have "0 < \<parallel>x\<parallel>" using x x_neq ..
1.268 + then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
1.269 + from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
1.270 + qed
1.271 + also have "\<dots> = c"
1.272 + proof -
1.273 + from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
1.274 + then show ?thesis by simp
1.275 + qed
1.276 + finally show ?thesis .
1.277 + qed
1.278 + qed (insert `continuous V norm f`, simp_all add: continuous_def)
1.279 +qed
1.280 +
1.281 +end