--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Sun Jun 04 00:09:04 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Sun Jun 04 19:39:29 2000 +0200
@@ -3,43 +3,43 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* The norm of a function *};
+header {* The norm of a function *}
-theory FunctionNorm = NormedSpace + FunctionOrder:;
+theory FunctionNorm = NormedSpace + FunctionOrder:
-subsection {* Continuous linear forms*};
+subsection {* Continuous linear forms*}
text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$
is \emph{continuous}, iff it is bounded, i.~e.
\[\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}\]
In our application no other functions than linear forms are considered,
so we can define continuous linear forms as bounded linear forms:
-*};
+*}
constdefs
is_continuous ::
"['a::{minus, plus} set, 'a => real, 'a => real] => bool"
"is_continuous V norm f ==
- is_linearform V f & (EX c. ALL x:V. abs (f x) <= c * norm x)";
+ is_linearform V f & (EX c. ALL x:V. abs (f x) <= c * norm x)"
lemma continuousI [intro]:
"[| is_linearform V f; !! x. x:V ==> abs (f x) <= c * norm x |]
- ==> is_continuous V norm f";
-proof (unfold is_continuous_def, intro exI conjI ballI);
- assume r: "!! x. x:V ==> abs (f x) <= c * norm x";
- fix x; assume "x:V"; show "abs (f x) <= c * norm x"; by (rule r);
-qed;
+ ==> is_continuous V norm f"
+proof (unfold is_continuous_def, intro exI conjI ballI)
+ assume r: "!! x. x:V ==> abs (f x) <= c * norm x"
+ fix x assume "x:V" show "abs (f x) <= c * norm x" by (rule r)
+qed
lemma continuous_linearform [intro??]:
- "is_continuous V norm f ==> is_linearform V f";
- by (unfold is_continuous_def) force;
+ "is_continuous V norm f ==> is_linearform V f"
+ by (unfold is_continuous_def) force
lemma continuous_bounded [intro??]:
"is_continuous V norm f
- ==> EX c. ALL x:V. abs (f x) <= c * norm x";
- by (unfold is_continuous_def) force;
+ ==> EX c. ALL x:V. abs (f x) <= c * norm x"
+ by (unfold is_continuous_def) force
-subsection{* The norm of a linear form *};
+subsection{* The norm of a linear form *}
text{* The least real number $c$ for which holds
@@ -61,327 +61,327 @@
\[
\{ 0 \} \Un \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
\]
-*};
+*}
constdefs
B :: "[ 'a set, 'a => real, 'a => real ] => real set"
"B V norm f ==
- {(#0::real)} \Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}";
+ {#0} Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}"
text{* $n$ is the function norm of $f$, iff
$n$ is the supremum of $B$.
-*};
+*}
constdefs
is_function_norm ::
" ['a set, 'a => real, 'a => real] => real => bool"
- "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn";
+ "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn"
text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$,
-if the supremum exists. Otherwise it is undefined. *};
+if the supremum exists. Otherwise it is undefined. *}
constdefs
function_norm :: " ['a set, 'a => real, 'a => real] => real"
- "function_norm V norm f == Sup UNIV (B V norm f)";
+ "function_norm V norm f == Sup UNIV (B V norm f)"
-lemma B_not_empty: "(#0::real) : B V norm f";
- by (unfold B_def, force);
+lemma B_not_empty: "#0 : B V norm f"
+ by (unfold B_def, force)
text {* The following lemma states that every continuous linear form
-on a normed space $(V, \norm{\cdot})$ has a function norm. *};
+on a normed space $(V, \norm{\cdot})$ has a function norm. *}
lemma ex_fnorm [intro??]:
"[| is_normed_vectorspace V norm; is_continuous V norm f|]
- ==> is_function_norm V norm f (function_norm V norm f)";
+ ==> is_function_norm V norm f (function_norm V norm f)"
proof (unfold function_norm_def is_function_norm_def
- is_continuous_def Sup_def, elim conjE, rule selectI2EX);
- assume "is_normed_vectorspace V norm";
+ is_continuous_def Sup_def, elim conjE, rule selectI2EX)
+ assume "is_normed_vectorspace V norm"
assume "is_linearform V f"
- and e: "EX c. ALL x:V. abs (f x) <= c * norm x";
+ and e: "EX c. ALL x:V. abs (f x) <= c * norm x"
txt {* The existence of the supremum is shown using the
completeness of the reals. Completeness means, that
every non-empty bounded set of reals has a
- supremum. *};
- show "EX a. is_Sup UNIV (B V norm f) a";
- proof (unfold is_Sup_def, rule reals_complete);
+ supremum. *}
+ show "EX a. is_Sup UNIV (B V norm f) a"
+ proof (unfold is_Sup_def, rule reals_complete)
- txt {* First we have to show that $B$ is non-empty: *};
+ txt {* First we have to show that $B$ is non-empty: *}
- show "EX X. X : B V norm f";
- proof (intro exI);
- show "(#0::real) : (B V norm f)"; by (unfold B_def, force);
- qed;
+ show "EX X. X : B V norm f"
+ proof (intro exI)
+ show "#0 : (B V norm f)" by (unfold B_def, force)
+ qed
- txt {* Then we have to show that $B$ is bounded: *};
+ txt {* Then we have to show that $B$ is bounded: *}
- from e; show "EX Y. isUb UNIV (B V norm f) Y";
- proof;
+ from e show "EX Y. isUb UNIV (B V norm f) Y"
+ proof
- txt {* We know that $f$ is bounded by some value $c$. *};
+ txt {* We know that $f$ is bounded by some value $c$. *}
- fix c; assume a: "ALL x:V. abs (f x) <= c * norm x";
- def b == "max c (#0::real)";
+ fix c assume a: "ALL x:V. abs (f x) <= c * norm x"
+ def b == "max c #0"
- show "?thesis";
+ show "?thesis"
proof (intro exI isUbI setleI ballI, unfold B_def,
- elim UnE CollectE exE conjE singletonE);
+ elim UnE CollectE exE conjE singletonE)
txt{* To proof the thesis, we have to show that there is
some constant $b$, such that $y \leq b$ for all $y\in B$.
Due to the definition of $B$ there are two cases for
- $y\in B$. If $y = 0$ then $y \leq idt{max}\ap c\ap 0$: *};
+ $y\in B$. If $y = 0$ then $y \leq idt{max}\ap c\ap 0$: *}
- fix y; assume "y = (#0::real)";
- show "y <= b"; by (simp! add: le_max2);
+ fix y assume "y = (#0::real)"
+ show "y <= b" by (simp! add: le_max2)
txt{* The second case is
$y = {|f\ap x|}/{\norm x}$ for some
- $x\in V$ with $x \neq \zero$. *};
+ $x\in V$ with $x \neq \zero$. *}
- next;
- fix x y;
- assume "x:V" "x ~= 00"; (***
+ next
+ fix x y
+ assume "x:V" "x ~= 00" (***
- have ge: "(#0::real) <= rinv (norm x)";
+ have ge: "#0 <= rinv (norm x)";
by (rule real_less_imp_le, rule real_rinv_gt_zero,
- rule normed_vs_norm_gt_zero); (***
+ rule normed_vs_norm_gt_zero); ( ***
proof (rule real_less_imp_le);
- show "(#0::real) < rinv (norm x)";
+ show "#0 < rinv (norm x)";
proof (rule real_rinv_gt_zero);
- show "(#0::real) < norm x"; ..;
+ show "#0 < norm x"; ..;
qed;
- qed; ***)
- have nz: "norm x ~= (#0::real)";
+ qed; *** )
+ have nz: "norm x ~= #0"
by (rule not_sym, rule lt_imp_not_eq,
- rule normed_vs_norm_gt_zero); (***
+ rule normed_vs_norm_gt_zero) (***
proof (rule not_sym);
- show "(#0::real) ~= norm x";
+ show "#0 ~= norm x";
proof (rule lt_imp_not_eq);
- show "(#0::real) < norm x"; ..;
+ show "#0 < norm x"; ..;
qed;
qed; ***)***)
txt {* The thesis follows by a short calculation using the
- fact that $f$ is bounded. *};
+ fact that $f$ is bounded. *}
- assume "y = abs (f x) * rinv (norm x)";
- also; have "... <= c * norm x * rinv (norm x)";
- proof (rule real_mult_le_le_mono2);
- show "(#0::real) <= rinv (norm x)";
+ assume "y = abs (f x) * rinv (norm x)"
+ also have "... <= c * norm x * rinv (norm x)"
+ proof (rule real_mult_le_le_mono2)
+ show "#0 <= rinv (norm x)"
by (rule real_less_imp_le, rule real_rinv_gt_zero1,
- rule normed_vs_norm_gt_zero);
- from a; show "abs (f x) <= c * norm x"; ..;
- qed;
- also; have "... = c * (norm x * rinv (norm x))";
- by (rule real_mult_assoc);
- also; have "(norm x * rinv (norm x)) = (#1::real)";
- proof (rule real_mult_inv_right1);
- show nz: "norm x ~= (#0::real)";
+ rule normed_vs_norm_gt_zero)
+ from a show "abs (f x) <= c * norm x" ..
+ qed
+ also have "... = c * (norm x * rinv (norm x))"
+ by (rule real_mult_assoc)
+ also have "(norm x * rinv (norm x)) = (#1::real)"
+ proof (rule real_mult_inv_right1)
+ show nz: "norm x ~= #0"
by (rule not_sym, rule lt_imp_not_eq,
- rule normed_vs_norm_gt_zero);
- qed;
- also; have "c * ... <= b "; by (simp! add: le_max1);
- finally; show "y <= b"; .;
- qed simp;
- qed;
- qed;
-qed;
+ rule normed_vs_norm_gt_zero)
+ qed
+ also have "c * ... <= b " by (simp! add: le_max1)
+ finally show "y <= b" .
+ qed simp
+ qed
+ qed
+qed
-text {* The norm of a continuous function is always $\geq 0$. *};
+text {* The norm of a continuous function is always $\geq 0$. *}
lemma fnorm_ge_zero [intro??]:
"[| is_continuous V norm f; is_normed_vectorspace V norm|]
- ==> (#0::real) <= function_norm V norm f";
-proof -;
+ ==> #0 <= function_norm V norm f"
+proof -
assume c: "is_continuous V norm f"
- and n: "is_normed_vectorspace V norm";
+ and n: "is_normed_vectorspace V norm"
txt {* The function norm is defined as the supremum of $B$.
So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided
- the supremum exists and $B$ is not empty. *};
+ the supremum exists and $B$ is not empty. *}
- show ?thesis;
- proof (unfold function_norm_def, rule sup_ub1);
- show "ALL x:(B V norm f). (#0::real) <= x";
+ show ?thesis
+ proof (unfold function_norm_def, rule sup_ub1)
+ show "ALL x:(B V norm f). #0 <= x"
proof (intro ballI, unfold B_def,
- elim UnE singletonE CollectE exE conjE);
- fix x r;
+ elim UnE singletonE CollectE exE conjE)
+ fix x r
assume "x : V" "x ~= 00"
- and r: "r = abs (f x) * rinv (norm x)";
+ and r: "r = abs (f x) * rinv (norm x)"
- have ge: "(#0::real) <= abs (f x)"; by (simp! only: abs_ge_zero);
- have "(#0::real) <= rinv (norm x)";
- by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule);(***
+ have ge: "#0 <= abs (f x)" by (simp! only: abs_ge_zero)
+ have "#0 <= rinv (norm x)"
+ by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(***
proof (rule real_less_imp_le);
- show "(#0::real) < rinv (norm x)";
+ show "#0 < rinv (norm x)";
proof (rule real_rinv_gt_zero);
- show "(#0::real) < norm x"; ..;
+ show "#0 < norm x"; ..;
qed;
qed; ***)
- with ge; show "(#0::real) <= r";
- by (simp only: r, rule real_le_mult_order1a);
- qed (simp!);
+ with ge show "#0 <= r"
+ by (simp only: r, rule real_le_mult_order1a)
+ qed (simp!)
- txt {* Since $f$ is continuous the function norm exists: *};
+ txt {* Since $f$ is continuous the function norm exists: *}
- have "is_function_norm V norm f (function_norm V norm f)"; ..;
- thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
- by (unfold is_function_norm_def function_norm_def);
+ have "is_function_norm V norm f (function_norm V norm f)" ..
+ thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
+ by (unfold is_function_norm_def function_norm_def)
- txt {* $B$ is non-empty by construction: *};
+ txt {* $B$ is non-empty by construction: *}
- show "(#0::real) : B V norm f"; by (rule B_not_empty);
- qed;
-qed;
+ show "#0 : B V norm f" by (rule B_not_empty)
+ qed
+qed
text{* \medskip The fundamental property of function norms is:
\begin{matharray}{l}
| f\ap x | \leq {\fnorm {f}} \cdot {\norm x}
\end{matharray}
-*};
+*}
lemma norm_fx_le_norm_f_norm_x:
"[| is_normed_vectorspace V norm; x:V; is_continuous V norm f |]
- ==> abs (f x) <= function_norm V norm f * norm x";
-proof -;
+ ==> abs (f x) <= function_norm V norm f * norm x"
+proof -
assume "is_normed_vectorspace V norm" "x:V"
- and c: "is_continuous V norm f";
- have v: "is_vectorspace V"; ..;
- assume "x:V";
+ and c: "is_continuous V norm f"
+ have v: "is_vectorspace V" ..
+ assume "x:V"
- txt{* The proof is by case analysis on $x$. *};
+ txt{* The proof is by case analysis on $x$. *}
- show ?thesis;
- proof cases;
+ show ?thesis
+ proof cases
txt {* For the case $x = \zero$ the thesis follows
from the linearity of $f$: for every linear function
- holds $f\ap \zero = 0$. *};
+ holds $f\ap \zero = 0$. *}
- assume "x = 00";
- have "abs (f x) = abs (f 00)"; by (simp!);
- also; from v continuous_linearform; have "f 00 = (#0::real)"; ..;
- also; note abs_zero;
- also; have "(#0::real) <= function_norm V norm f * norm x";
- proof (rule real_le_mult_order1a);
- show "(#0::real) <= function_norm V norm f"; ..;
- show "(#0::real) <= norm x"; ..;
- qed;
- finally;
- show "abs (f x) <= function_norm V norm f * norm x"; .;
+ assume "x = 00"
+ have "abs (f x) = abs (f 00)" by (simp!)
+ also from v continuous_linearform have "f 00 = #0" ..
+ also note abs_zero
+ also have "#0 <= function_norm V norm f * norm x"
+ proof (rule real_le_mult_order1a)
+ show "#0 <= function_norm V norm f" ..
+ show "#0 <= norm x" ..
+ qed
+ finally
+ show "abs (f x) <= function_norm V norm f * norm x" .
- next;
- assume "x ~= 00";
- have n: "(#0::real) <= norm x"; ..;
- have nz: "norm x ~= (#0::real)";
- proof (rule lt_imp_not_eq [RS not_sym]);
- show "(#0::real) < norm x"; ..;
- qed;
+ next
+ assume "x ~= 00"
+ have n: "#0 <= norm x" ..
+ have nz: "norm x ~= #0"
+ proof (rule lt_imp_not_eq [RS not_sym])
+ show "#0 < norm x" ..
+ qed
txt {* For the case $x\neq \zero$ we derive the following
- fact from the definition of the function norm:*};
+ fact from the definition of the function norm:*}
- have l: "abs (f x) * rinv (norm x) <= function_norm V norm f";
- proof (unfold function_norm_def, rule sup_ub);
- from ex_fnorm [OF _ c];
- show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
- by (simp! add: is_function_norm_def function_norm_def);
- show "abs (f x) * rinv (norm x) : B V norm f";
+ have l: "abs (f x) * rinv (norm x) <= function_norm V norm f"
+ proof (unfold function_norm_def, rule sup_ub)
+ from ex_fnorm [OF _ c]
+ show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
+ by (simp! add: is_function_norm_def function_norm_def)
+ show "abs (f x) * rinv (norm x) : B V norm f"
by (unfold B_def, intro UnI2 CollectI exI [of _ x]
- conjI, simp);
- qed;
+ conjI, simp)
+ qed
- txt {* The thesis now follows by a short calculation: *};
+ txt {* The thesis now follows by a short calculation: *}
- have "abs (f x) = abs (f x) * (#1::real)"; by (simp!);
- also; from nz; have "(#1::real) = rinv (norm x) * norm x";
- by (rule real_mult_inv_left1 [RS sym]);
- also;
- have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x";
- by (simp! add: real_mult_assoc [of "abs (f x)"]);
- also; have "... <= function_norm V norm f * norm x";
- by (rule real_mult_le_le_mono2 [OF n l]);
- finally;
- show "abs (f x) <= function_norm V norm f * norm x"; .;
- qed;
-qed;
+ have "abs (f x) = abs (f x) * (#1::real)" by (simp!)
+ also from nz have "(#1::real) = rinv (norm x) * norm x"
+ by (rule real_mult_inv_left1 [RS sym])
+ also
+ have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x"
+ by (simp! add: real_mult_assoc [of "abs (f x)"])
+ also have "... <= function_norm V norm f * norm x"
+ by (rule real_mult_le_le_mono2 [OF n l])
+ finally
+ show "abs (f x) <= function_norm V norm f * norm x" .
+ qed
+qed
text{* \medskip The function norm is the least positive real number for
which the following inequation holds:
\begin{matharray}{l}
| f\ap x | \leq c \cdot {\norm x}
\end{matharray}
-*};
+*}
lemma fnorm_le_ub:
"[| is_normed_vectorspace V norm; is_continuous V norm f;
- ALL x:V. abs (f x) <= c * norm x; (#0::real) <= c |]
- ==> function_norm V norm f <= c";
-proof (unfold function_norm_def);
- assume "is_normed_vectorspace V norm";
- assume c: "is_continuous V norm f";
+ ALL x:V. abs (f x) <= c * norm x; #0 <= c |]
+ ==> function_norm V norm f <= c"
+proof (unfold function_norm_def)
+ assume "is_normed_vectorspace V norm"
+ assume c: "is_continuous V norm f"
assume fb: "ALL x:V. abs (f x) <= c * norm x"
- and "(#0::real) <= c";
+ and "#0 <= c"
txt {* Suppose the inequation holds for some $c\geq 0$.
If $c$ is an upper bound of $B$, then $c$ is greater
than the function norm since the function norm is the
least upper bound.
- *};
+ *}
- show "Sup UNIV (B V norm f) <= c";
- proof (rule sup_le_ub);
- from ex_fnorm [OF _ c];
- show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
- by (simp! add: is_function_norm_def function_norm_def);
+ show "Sup UNIV (B V norm f) <= c"
+ proof (rule sup_le_ub)
+ from ex_fnorm [OF _ c]
+ show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
+ by (simp! add: is_function_norm_def function_norm_def)
txt {* $c$ is an upper bound of $B$, i.~e.~every
- $y\in B$ is less than $c$. *};
+ $y\in B$ is less than $c$. *}
- show "isUb UNIV (B V norm f) c";
- proof (intro isUbI setleI ballI);
- fix y; assume "y: B V norm f";
- thus le: "y <= c";
- proof (unfold B_def, elim UnE CollectE exE conjE singletonE);
+ show "isUb UNIV (B V norm f) c"
+ proof (intro isUbI setleI ballI)
+ fix y assume "y: B V norm f"
+ thus le: "y <= c"
+ proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
- txt {* The first case for $y\in B$ is $y=0$. *};
+ txt {* The first case for $y\in B$ is $y=0$. *}
- assume "y = (#0::real)";
- show "y <= c"; by (force!);
+ assume "y = #0"
+ show "y <= c" by (force!)
txt{* The second case is
$y = {|f\ap x|}/{\norm x}$ for some
- $x\in V$ with $x \neq \zero$. *};
+ $x\in V$ with $x \neq \zero$. *}
- next;
- fix x;
- assume "x : V" "x ~= 00";
+ next
+ fix x
+ assume "x : V" "x ~= 00"
- have lz: "(#0::real) < norm x";
- by (simp! add: normed_vs_norm_gt_zero);
+ have lz: "#0 < norm x"
+ by (simp! add: normed_vs_norm_gt_zero)
- have nz: "norm x ~= (#0::real)";
- proof (rule not_sym);
- from lz; show "(#0::real) ~= norm x";
- by (simp! add: order_less_imp_not_eq);
- qed;
+ have nz: "norm x ~= #0"
+ proof (rule not_sym)
+ from lz show "#0 ~= norm x"
+ by (simp! add: order_less_imp_not_eq)
+ qed
- from lz; have "(#0::real) < rinv (norm x)";
- by (simp! add: real_rinv_gt_zero1);
- hence rinv_gez: "(#0::real) <= rinv (norm x)";
- by (rule real_less_imp_le);
+ from lz have "#0 < rinv (norm x)"
+ by (simp! add: real_rinv_gt_zero1)
+ hence rinv_gez: "#0 <= rinv (norm x)"
+ by (rule real_less_imp_le)
- assume "y = abs (f x) * rinv (norm x)";
- also; from rinv_gez; have "... <= c * norm x * rinv (norm x)";
- proof (rule real_mult_le_le_mono2);
- show "abs (f x) <= c * norm x"; by (rule bspec);
- qed;
- also; have "... <= c"; by (simp add: nz real_mult_assoc);
- finally; show ?thesis; .;
- qed;
- qed force;
- qed;
-qed;
+ assume "y = abs (f x) * rinv (norm x)"
+ also from rinv_gez have "... <= c * norm x * rinv (norm x)"
+ proof (rule real_mult_le_le_mono2)
+ show "abs (f x) <= c * norm x" by (rule bspec)
+ qed
+ also have "... <= c" by (simp add: nz real_mult_assoc)
+ finally show ?thesis .
+ qed
+ qed force
+ qed
+qed
-end;
\ No newline at end of file
+end
\ No newline at end of file