(* Title: HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
Author: Gertrud Bauer, TU Munich
*)
section ‹The supremum wrt.
\ the
function order
›
theory Hahn_Banach_Sup_Lemmas
imports Function_Norm Zorn_Lemma
begin
text ‹
This
section contains some
lemmas that will be used
in the
proof of the
Hahn-Banach
Theorem.
In this
section the following
context is presumed.
Let
‹E
› be a real vector space
with a seminorm
‹p
› on
‹E
›.
‹F
› is a subspace of
‹E
› and ‹f
› a linear form on
‹F
›. We consider a chain
‹c
› of norm-preserving
extensions of
‹f
›, such that
‹∪c = graph H h
›. We will
show some properties
about the limit
function ‹h
›, i.e.
\ the supremum of the chain
‹c
›.
🚫
Let ‹c
› be a chain of norm-preserving extensions of the
function ‹f
› and let
‹graph H h
› be the supremum of
‹c
›. Every element
in ‹H
› is member of one of
the elements of the chain.
›
lemmas [dest?] = chainsD
lemmas chainsE2 [elim?] = chainsD2 [elim_format]
lemma some_H
'h't:
assumes M:
"M = norm_pres_extensions E p F f"
and cM:
"c \ chains M"
and u:
"graph H h = \c"
and x:
"x \ H"
shows "\H' h'. graph H' h' \ c
∧ (x, h x)
∈ graph H
' h'
∧ linearform H
' h' ∧ H
' \ E
∧ F
⊴ H
' \ graph F f \ graph H' h
'
∧ (
∀x
∈ H
'. h' x
≤ p x)
"
proof -
from x
have "(x, h x) \ graph H h" ..
also from u
have "\ = \c" .
finally obtain g
where gc:
"g \ c" and gh:
"(x, h x) \ g" by blast
from cM
have "c \ M" ..
with gc
have "g \ M" ..
also from M
have "\ = norm_pres_extensions E p F f" .
finally obtain H
' and h' where g:
"g = graph H' h'"
and * :
"linearform H' h'" "H' \ E" "F \ H'"
"graph F f \ graph H' h'" "\x \ H'. h' x \ p x" ..
from gc
and g
have "graph H' h' \ c" by (simp only:)
moreover from gh
and g
have "(x, h x) \ graph H' h'" by (simp only:)
ultimately show ?thesis
using *
by blast
qed
text ‹
🚫
Let ‹c
› be a chain of norm-preserving extensions of the
function ‹f
› and let
‹graph H h
› be the supremum of
‹c
›. Every element
in the
domain ‹H
› of the
supremum
function is member of the
domain ‹H
'\ of some function \h'›, such
that
‹h
› extends
‹h
'\.
›
lemma some_H
'h':
assumes M:
"M = norm_pres_extensions E p F f"
and cM:
"c \ chains M"
and u:
"graph H h = \c"
and x:
"x \ H"
shows "\H' h'. x \ H' \ graph H' h' \ graph H h
∧ linearform H
' h' ∧ H
' \ E \ F \ H'
∧ graph F f
⊆ graph H
' h' ∧ (
∀x
∈ H
'. h' x
≤ p x)
"
proof -
from M cM u x
obtain H
' h' where
x_hx:
"(x, h x) \ graph H' h'"
and c:
"graph H' h' \ c"
and * :
"linearform H' h'" "H' \ E" "F \ H'"
"graph F f \ graph H' h'" "\x \ H'. h' x \ p x"
by (rule some_H
'h't [elim_format]) blast
from x_hx
have "x \ H'" ..
moreover from cM u c
have "graph H' h' \ graph H h" by blast
ultimately show ?thesis
using *
by blast
qed
text ‹
🚫
Any two elements
‹x
› and ‹y
› in the
domain ‹H
› of the supremum
function ‹h
›
are both
in the
domain ‹H
'\ of some function \h'›, such that
‹h
› extends
‹h
'\.
›
lemma some_H
'h'2:
assumes M:
"M = norm_pres_extensions E p F f"
and cM:
"c \ chains M"
and u:
"graph H h = \c"
and x:
"x \ H"
and y:
"y \ H"
shows "\H' h'. x \ H' \ y \ H'
∧ graph H
' h' ⊆ graph H h
∧ linearform H
' h' ∧ H
' \ E \ F \ H'
∧ graph F f
⊆ graph H
' h' ∧ (
∀x
∈ H
'. h' x
≤ p x)
"
proof -
txt ‹‹y
› is in the
domain ‹H
''› of some
function ‹h
''›, such that
‹h
›
extends
‹h
''›.
›
from M cM u
and y
obtain H
' h' where
y_hy:
"(y, h y) \ graph H' h'"
and c
': "graph H' h
' \ c"
and * :
"linearform H' h'" "H' \ E" "F \ H'"
"graph F f \ graph H' h'" "\x \ H'. h' x \ p x"
by (rule some_H
'h't [elim_format]) blast
txt ‹‹x
› is in the
domain ‹H
'\ of some function \h'›,
such that
‹h
› extends
‹h
'\.\
from M cM u
and x
obtain H
'' h
'' where
x_hx:
"(x, h x) \ graph H'' h''"
and c
'':
"graph H'' h'' \ c"
and ** :
"linearform H'' h''" "H'' \ E" "F \ H''"
"graph F f \ graph H'' h''" "\x \ H''. h'' x \ p x"
by (rule some_H
'h't [elim_format]) blast
txt ‹Since both
‹h
'\ and \h''\ are elements of the chain, \h''\ is an
extension of
‹h
'\ or vice versa. Thus both \x\ and \y\ are contained in
the greater one.
\label{cases1}
›
from cM c
'' c
' consider "graph H'' h'' \ graph H' h
'" | "graph H' h
' \ graph H'' h''"
by (blast dest: chainsD)
then show ?thesis
proof cases
case 1
have "(x, h x) \ graph H'' h''" by fact
also have "\ \ graph H' h'" by fact
finally have xh:
"(x, h x) \ graph H' h'" .
then have "x \ H'" ..
moreover from y_hy
have "y \ H'" ..
moreover from cM u
and c
' have "graph H' h
' \ graph H h" by blast
ultimately show ?thesis
using *
by blast
next
case 2
from x_hx
have "x \ H''" ..
moreover have "y \ H''"
proof -
have "(y, h y) \ graph H' h'" by (rule y_hy)
also have "\ \ graph H'' h''" by fact
finally have "(y, h y) \ graph H'' h''" .
then show ?thesis ..
qed
moreover from u c
'' have "graph H'' h'' \ graph H h" by blast
ultimately show ?thesis
using **
by blast
qed
qed
text ‹
🚫
The relation induced
by the graph of the supremum of a chain
‹c
› is
definite, i.e.
\ it
is the graph of a
function.
›
lemma sup_definite:
assumes M_def:
"M = norm_pres_extensions E p F f"
and cM:
"c \ chains M"
and xy:
"(x, y) \ \c"
and xz:
"(x, z) \ \c"
shows "z = y"
proof -
from cM
have c:
"c \ M" ..
from xy
obtain G1
where xy
': "(x, y) \ G1" and G1: "G1 \ c" ..
from xz
obtain G2
where xz
': "(x, z) \ G2" and G2: "G2 \ c" ..
from G1 c
have "G1 \ M" ..
then obtain H1 h1
where G1_rep:
"G1 = graph H1 h1"
unfolding M_def
by blast
from G2 c
have "G2 \ M" ..
then obtain H2 h2
where G2_rep:
"G2 = graph H2 h2"
unfolding M_def
by blast
txt ‹‹G
🚫1
› is contained
in ‹G
🚫2
› or vice versa, since both
‹G
🚫1
› and ‹G
🚫2
›
are members of
‹c
›.
\label{cases2}
›
from cM G1 G2 consider
"G1 \ G2" |
"G2 \ G1"
by (blast dest: chainsD)
then show ?thesis
proof cases
case 1
with xy
' G2_rep have "(x, y) \ graph H2 h2" by blast
then have "y = h2 x" ..
also
from xz
' G2_rep have "(x, z) \ graph H2 h2" by (simp only:)
then have "z = h2 x" ..
finally show ?thesis .
next
case 2
with xz
' G1_rep have "(x, z) \ graph H1 h1" by blast
then have "z = h1 x" ..
also
from xy
' G1_rep have "(x, y) \ graph H1 h1" by (simp only:)
then have "y = h1 x" ..
finally show ?thesis ..
qed
qed
text ‹
🚫
The limit
function ‹h
› is linear. Every element
‹x
› in the
domain of
‹h
› is
in the
domain of a
function ‹h
'\ in the chain of norm preserving extensions.
Furthermore,
‹h
› is an extension of
‹h
'\ so the function values of \x\ are
identical
for ‹h
'\ and \h\. Finally, the function \h'› is linear
by
construction of
‹M
›.
›
lemma sup_lf:
assumes M:
"M = norm_pres_extensions E p F f"
and cM:
"c \ chains M"
and u:
"graph H h = \c"
shows "linearform H h"
proof
fix x y
assume x:
"x \ H" and y:
"y \ H"
with M cM u
obtain H
' h' where
x
': "x \ H'" and y': "y
∈ H
'"
and b:
"graph H' h' \ graph H h"
and linearform:
"linearform H' h'"
and subspace:
"H' \ E"
by (rule some_H
'h'2 [elim_format]) blast
show "h (x + y) = h x + h y"
proof -
from linearform x
' y' have "h' (x + y) = h' x + h' y"
by (rule linearform.add)
also from b x
' have "h' x = h x
" ..
also from b y
' have "h' y = h y
" ..
also from subspace x
' y' have "x + y \ H'"
by (rule subspace.add_closed)
with b
have "h' (x + y) = h (x + y)" ..
finally show ?thesis .
qed
next
fix x a
assume x:
"x \ H"
with M cM u
obtain H
' h' where
x
': "x \ H'"
and b:
"graph H' h' \ graph H h"
and linearform:
"linearform H' h'"
and subspace:
"H' \ E"
by (rule some_H
'h' [elim_format]) blast
show "h (a \ x) = a * h x"
proof -
from linearform x
' have "h' (a
⋅ x) = a * h
' x"
by (rule linearform.mult)
also from b x
' have "h' x = h x
" ..
also from subspace x
' have "a \ x \ H'"
by (rule subspace.mult_closed)
with b
have "h' (a \ x) = h (a \ x)" ..
finally show ?thesis .
qed
qed
text ‹
🚫
The limit of a non-empty chain of norm preserving extensions of
‹f
› is an
extension of
‹f
›, since every element of the chain
is an extension of
‹f
›
and the supremum
is an extension
for every element of the chain.
›
lemma sup_ext:
assumes graph:
"graph H h = \c"
and M:
"M = norm_pres_extensions E p F f"
and cM:
"c \ chains M"
and ex:
"\x. x \ c"
shows "graph F f \ graph H h"
proof -
from ex
obtain x
where xc:
"x \ c" ..
from cM
have "c \ M" ..
with xc
have "x \ M" ..
with M
have "x \ norm_pres_extensions E p F f"
by (simp only:)
then obtain G g
where "x = graph G g" and "graph F f \ graph G g" ..
then have "graph F f \ x" by (simp only:)
also from xc
have "\ \ \c" by blast
also from graph
have "\ = graph H h" ..
finally show ?thesis .
qed
text ‹
🚫
The
domain ‹H
› of the limit
function is a superspace of
‹F
›, since
‹F
› is a
subset of
‹H
›. The existence of the
‹0
› element
in ‹F
› and the closure
properties follow
from the fact that
‹F
› is a vector space.
›
lemma sup_supF:
assumes graph:
"graph H h = \c"
and M:
"M = norm_pres_extensions E p F f"
and cM:
"c \ chains M"
and ex:
"\x. x \ c"
and FE:
"F \ E"
shows "F \ H"
proof
from FE
show "F \ {}" by (rule subspace.non_empty)
from graph M cM ex
have "graph F f \ graph H h" by (rule sup_ext)
then show "F \ H" ..
show "x + y \ F" if "x \ F" and "y \ F" for x y
using FE that
by (rule subspace.add_closed)
show "a \ x \ F" if "x \ F" for x a
using FE that
by (rule subspace.mult_closed)
qed
text ‹
🚫
The
domain ‹H
› of the limit
function is a subspace of
‹E
›.
›
lemma sup_subE:
assumes graph:
"graph H h = \c"
and M:
"M = norm_pres_extensions E p F f"
and cM:
"c \ chains M"
and ex:
"\x. x \ c"
and FE:
"F \ E"
and E:
"vectorspace E"
shows "H \ E"
proof
show "H \ {}"
proof -
from FE E
have "0 \ F" by (rule subspace.zero)
also from graph M cM ex FE
have "F \ H" by (rule sup_supF)
then have "F \ H" ..
finally show ?thesis
by blast
qed
show "H \ E"
proof
fix x
assume "x \ H"
with M cM graph
obtain H
' where x: "x \ H'" and H'E: "H
' \ E"
by (rule some_H
'h' [elim_format]) blast
from H
'E have "H' ⊆ E
" ..
with x
show "x \ E" ..
qed
fix x y
assume x:
"x \ H" and y:
"y \ H"
show "x + y \ H"
proof -
from M cM graph x y
obtain H
' h' where
x
': "x \ H'" and y': "y
∈ H
'" and H'E:
"H' \ E"
and graphs:
"graph H' h' \ graph H h"
by (rule some_H
'h'2 [elim_format]) blast
from H
'E x' y
' have "x + y \ H'"
by (rule subspace.add_closed)
also from graphs
have "H' \ H" ..
finally show ?thesis .
qed
next
fix x a
assume x:
"x \ H"
show "a \ x \ H"
proof -
from M cM graph x
obtain H
' h' where x
': "x \ H'" and H'E: "H
' \ E"
and graphs:
"graph H' h' \ graph H h"
by (rule some_H
'h' [elim_format]) blast
from H
'E x' have "a \ x \ H'" by (rule subspace.mult_closed)
also from graphs
have "H' \ H" ..
finally show ?thesis .
qed
qed
text ‹
🚫
The limit
function is bounded
by the norm
‹p
› as well, since all elements
in
the chain are bounded
by ‹p
›.
›
lemma sup_norm_pres:
assumes graph:
"graph H h = \c"
and M:
"M = norm_pres_extensions E p F f"
and cM:
"c \ chains M"
shows "\x \ H. h x \ p x"
proof
fix x
assume "x \ H"
with M cM graph
obtain H
' h' where x
': "x \ H'"
and graphs:
"graph H' h' \ graph H h"
and a:
"\x \ H'. h' x \ p x"
by (rule some_H
'h' [elim_format]) blast
from graphs x
' have [symmetric]: "h' x = h x
" ..
also from a x
' have "h' x
≤ p x
" ..
finally show "h x \ p x" .
qed
text ‹
🚫
The following
lemma is a property of linear forms on real vector spaces. It
will be used
for the
lemma ‹abs_Hahn_Banach
› (see page
\pageref{abs-Hahn-Banach}).
\label{abs-ineq-iff}
For real vector spaces the
following inequality are equivalent:
\begin{center}
\begin{tabular}{lll}
‹∀x
∈ H.
∣h x
∣ ≤ p x
› &
and &
‹∀x
∈ H. h x
≤ p x
› \\
\end{tabular}
\end{center}
›
lemma abs_ineq_iff:
assumes "subspace H E" and "vectorspace E" and "seminorm E p"
and "linearform H h"
shows "(\x \ H. \h x\ \ p x) = (\x \ H. h x \ p x)" (
is "?L = ?R")
proof
interpret subspace H E
by fact
interpret vectorspace E
by fact
interpret seminorm E p
by fact
interpret linearform H h
by fact
have H:
"vectorspace H" using ‹vectorspace E
› ..
show ?R
if l: ?L
proof
fix x
assume x:
"x \ H"
have "h x \ \h x\" by arith
also from l x
have "\ \ p x" ..
finally show "h x \ p x" .
qed
show ?L
if r: ?R
proof
fix x
assume x:
"x \ H"
show "\b\ \ a" when
"- a \ b" "b \ a" for a b :: real
using that
by arith
from ‹linearform H h
› and H x
have "- h x = h (- x)" by (rule linearform.neg [symmetric])
also
from H x
have "- x \ H" by (rule vectorspace.neg_closed)
with r
have "h (- x) \ p (- x)" ..
also have "\ = p x"
using ‹seminorm E p
› ‹vectorspace E
›
proof (rule seminorm.minus)
from x
show "x \ E" ..
qed
finally have "- h x \ p x" .
then show "- p x \ h x" by simp
from r x
show "h x \ p x" ..
qed
qed
end
