Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Function_Norm.thy
Sprache: Unknown
(* Title: HOL/Hahn_Banach/Function_Norm.thy
Author: Gertrud Bauer, TU Munich
*)
section \<open>The norm of a function\<close>
theory Function_Norm
imports Normed_Space Function_Order
begin
subsection \<open>Continuous linear forms\<close>
text \<open>
A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>, iff
it is bounded, i.e.
\begin{center}
\<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
\end{center}
In our application no other functions than linear forms are considered, so
we can define continuous linear forms as bounded linear forms:
\<close>
locale continuous = linearform +
fixes norm :: "_ \ real" ("\_\")
assumes bounded: "\c. \x \ V. \f x\ \ c * \x\"
declare continuous.intro [intro?] continuous_axioms.intro [intro?]
lemma continuousI [intro]:
fixes norm :: "_ \ real" ("\_\")
assumes "linearform V f"
assumes r: "\x. x \ V \ \f x\ \ c * \x\"
shows "continuous V f norm"
proof
show "linearform V f" by fact
from r have "\c. \x\V. \f x\ \ c * \x\" by blast
then show "continuous_axioms V f norm" ..
qed
subsection \<open>The norm of a linear form\<close>
text \<open>
The least real number \<open>c\<close> for which holds
\begin{center}
\<open>\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
\end{center}
is called the \<^emph>\<open>norm\<close> of \<open>f\<close>.
For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as
\begin{center}
\<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close>
\end{center}
For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. Since
\<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this situation it
must be guaranteed that there is an element in this set. This element must
be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. Furthermore it does
not have to change the norm in all other cases, so it must be \<open>0\<close>, as all
other elements are \<open>{} \<ge> 0\<close>.
Thus we define the set \<open>B\<close> where the supremum is taken from as follows:
\begin{center}
\<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close>
\end{center}
\<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists (otherwise
it is undefined).
\<close>
locale fn_norm =
fixes norm :: "_ \ real" ("\_\")
fixes B defines "B V f \ {0} \ {\f x\ / \x\ | x. x \ 0 \ x \ V}"
fixes fn_norm ("\_\\_" [0, 1000] 999)
defines "\f\\V \ \(B V f)"
locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm
lemma (in fn_norm) B_not_empty [intro]: "0 \ B V f"
by (simp add: B_def)
text \<open>
The following lemma states that every continuous linear form on a normed
space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.
\<close>
lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
assumes "continuous V f norm"
shows "lub (B V f) (\f\\V)"
proof -
interpret continuous V f norm by fact
txt \<open>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.\<close>
have "\a. lub (B V f) a"
proof (rule real_complete)
txt \<open>First we have to show that \<open>B\<close> is non-empty:\<close>
have "0 \ B V f" ..
then show "\x. x \ B V f" ..
txt \<open>Then we have to show that \<open>B\<close> is bounded:\<close>
show "\c. \y \ B V f. y \ c"
proof -
txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close>
from bounded obtain c where c: "\x \ V. \f x\ \ c * \x\" ..
txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such
that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are
two cases.\<close>
define b where "b = max c 0"
have "\y \ B V f. y \ b"
proof
fix y assume y: "y \ B V f"
show "y \ b"
proof cases
assume "y = 0"
then show ?thesis unfolding b_def by arith
next
txt \<open>The second case is \<open>y = \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> for some
\<open>x \<in> V\<close> with \<open>x \<noteq> 0\<close>.\<close>
assume "y \ 0"
with y obtain x where y_rep: "y = \f x\ * inverse \x\"
and x: "x \ V" and neq: "x \ 0"
by (auto simp add: B_def divide_inverse)
from x neq have gt: "0 < \x\" ..
txt \<open>The thesis follows by a short calculation using the
fact that \<open>f\<close> is bounded.\<close>
note y_rep
also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\"
proof (rule mult_right_mono)
from c x show "\f x\ \ c * \x\" ..
from gt have "0 < inverse \x\"
by (rule positive_imp_inverse_positive)
then show "0 \ inverse \x\" by (rule order_less_imp_le)
qed
also have "\ = c * (\x\ * inverse \x\)"
by (rule Groups.mult.assoc)
also
from gt have "\x\ \ 0" by simp
then have "\x\ * inverse \x\ = 1" by simp
also have "c * 1 \ b" by (simp add: b_def)
finally show "y \ b" .
qed
qed
then show ?thesis ..
qed
qed
then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
qed
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
assumes "continuous V f norm"
assumes b: "b \ B V f"
shows "b \ \f\\V"
proof -
interpret continuous V f norm by fact
have "lub (B V f) (\f\\V)"
using \<open>continuous V f norm\<close> by (rule fn_norm_works)
from this and b show ?thesis ..
qed
lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
assumes "continuous V f norm"
assumes b: "\b. b \ B V f \ b \ y"
shows "\f\\V \ y"
proof -
interpret continuous V f norm by fact
have "lub (B V f) (\f\\V)"
using \<open>continuous V f norm\<close> by (rule fn_norm_works)
from this and b show ?thesis ..
qed
text \<open>The norm of a continuous function is always \<open>\<ge> 0\<close>.\<close>
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
assumes "continuous V f norm"
shows "0 \ \f\\V"
proof -
interpret continuous V f norm by fact
txt \<open>The function norm is defined as the supremum of \<open>B\<close>.
So it is \<open>\<ge> 0\<close> if all elements in \<open>B\<close> are \<open>\<ge>
0\<close>, provided the supremum exists and \<open>B\<close> is not empty.\<close>
have "lub (B V f) (\f\\V)"
using \<open>continuous V f norm\<close> by (rule fn_norm_works)
moreover have "0 \ B V f" ..
ultimately show ?thesis ..
qed
text \<open>
\<^medskip>
The fundamental property of function norms is:
\begin{center}
\<open>\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
\end{center}
\<close>
lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
assumes "continuous V f norm" "linearform V f"
assumes x: "x \ V"
shows "\f x\ \ \f\\V * \x\"
proof -
interpret continuous V f norm by fact
interpret linearform V f by fact
show ?thesis
proof cases
assume "x = 0"
then have "\f x\ = \f 0\" by simp
also have "f 0 = 0" by rule unfold_locales
also have "\\\ = 0" by simp
also have a: "0 \ \f\\V"
using \<open>continuous V f norm\<close> by (rule fn_norm_ge_zero)
from x have "0 \ norm x" ..
with a have "0 \ \f\\V * \x\" by (simp add: zero_le_mult_iff)
finally show "\f x\ \ \f\\V * \x\" .
next
assume "x \ 0"
with x have neq: "\x\ \ 0" by simp
then have "\f x\ = (\f x\ * inverse \x\) * \x\" by simp
also have "\ \ \f\\V * \x\"
proof (rule mult_right_mono)
from x show "0 \ \x\" ..
from x and neq have "\f x\ * inverse \x\ \ B V f"
by (auto simp add: B_def divide_inverse)
with \<open>continuous V f norm\<close> show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
by (rule fn_norm_ub)
qed
finally show ?thesis .
qed
qed
text \<open>
\<^medskip>
The function norm is the least positive real number for which the
following inequality holds:
\begin{center}
\<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
\end{center}
\<close>
lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
assumes "continuous V f norm"
assumes ineq: "\x. x \ V \ \f x\ \ c * \x\" and ge: "0 \ c"
shows "\f\\V \ c"
proof -
interpret continuous V f norm by fact
show ?thesis
proof (rule fn_norm_leastB [folded B_def fn_norm_def])
fix b assume b: "b \ B V f"
show "b \ c"
proof cases
assume "b = 0"
with ge show ?thesis by simp
next
assume "b \ 0"
with b obtain x where b_rep: "b = \f x\ * inverse \x\"
and x_neq: "x \ 0" and x: "x \ V"
by (auto simp add: B_def divide_inverse)
note b_rep
also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\"
proof (rule mult_right_mono)
have "0 < \x\" using x x_neq ..
then show "0 \ inverse \x\" by simp
from x show "\f x\ \ c * \x\" by (rule ineq)
qed
also have "\ = c"
proof -
from x_neq and x have "\x\ \ 0" by simp
then show ?thesis by simp
qed
finally show ?thesis .
qed
qed (insert \<open>continuous V f norm\<close>, simp_all add: continuous_def)
qed
end
[ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
]
|
|
