(* Title: HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
Author: Gertrud Bauer, TU Munich
*)
section ‹Extending non-maximal functions
›
theory Hahn_Banach_Ext_Lemmas
imports Function_Norm
begin
text ‹
In this
section the following
context is presumed.
Let ‹E
› be a real vector
space
with a seminorm
‹q
› on
‹E
›.
‹F
› is a subspace of
‹E
› and ‹f
› a linear
function on
‹F
›. We consider a subspace
‹H
› of
‹E
› that
is a superspace of
‹F
› and a linear form
‹h
› on
‹H
›.
‹H
› is a not equal
to ‹E
› and ‹x
🚫0
› is an
element
in ‹E - H
›.
‹H
› is extended
to the direct sum
‹H
' = H + lin x\<^sub>0\, so
for any
‹x
∈ H
'\ the decomposition of \x = y + a \ x\ with \y \ H\ is
unique.
‹h
'\ is defined on \H'› by ‹h
' x = h y + a \ \\ for a certain \\\.
Subsequently we
show some properties of this extension
‹h
'\ of \h\.
🚫
This
lemma will be used
to show the existence of a linear extension of
‹f
›
(see page
\pageref{ex-xi-use}). It
is a consequence of the completeness of
‹ℝ›.
To show
\begin{center}
\begin{tabular}{l}
‹∃ξ.
∀y
∈ F. a y
≤ ξ
∧ ξ
≤ b y
›
\end{tabular}
\end{center}
🚫 it suffices
to show that
\begin{center}
\begin{tabular}{l}
‹∀u
∈ F.
∀v
∈ F. a u
≤ b v
›
\end{tabular}
\end{center}
›
lemma ex_xi:
assumes "vectorspace F"
assumes r:
"\u v. u \ F \ v \ F \ a u \ b v"
shows "\xi::real. \y \ F. a y \ xi \ xi \ b y"
proof -
interpret vectorspace F
by fact
txt ‹From the completeness of the reals follows:
The set
‹S = {a u. u
∈ F}
› has a supremum,
if it
is
non-empty
and has an upper bound.
›
let ?S =
"{a u | u. u \ F}"
have "\xi. lub ?S xi"
proof (rule real_complete)
have "a 0 \ ?S" by blast
then show "\X. X \ ?S" ..
have "\y \ ?S. y \ b 0"
proof
fix y
assume y:
"y \ ?S"
then obtain u
where u:
"u \ F" and y:
"y = a u" by blast
from u
and zero
have "a u \ b 0" by (rule r)
with y
show "y \ b 0" by (simp only:)
qed
then show "\u. \y \ ?S. y \ u" ..
qed
then obtain xi
where xi:
"lub ?S xi" ..
have "a y \ xi" if "y \ F" for y
proof -
from that
have "a y \ ?S" by blast
with xi
show ?thesis
by (rule lub.upper)
qed
moreover have "xi \ b y" if y:
"y \ F" for y
proof -
from xi
show ?thesis
proof (rule lub.least)
fix au
assume "au \ ?S"
then obtain u
where u:
"u \ F" and au:
"au = a u" by blast
from u y
have "a u \ b y" by (rule r)
with au
show "au \ b y" by (simp only:)
qed
qed
ultimately show "\xi. \y \ F. a y \ xi \ xi \ b y" by blast
qed
text ‹
🚫
The
function ‹h
'\ is defined as a \h' x = h y + a
⋅ ξ
› where ‹x = y + a
⋅ ξ
›
is a linear extension of
‹h
› to ‹H
'\.
›
lemma h
'_lf:
assumes h
'_def: "\x. h' x = (
let (y, a) =
SOME (y, a). x = y + a
⋅ x0
∧ y
∈ H
in h y + a * xi)
"
and H
'_def: "H' = H + lin x0
"
and HE:
"H \ E"
assumes "linearform H h"
assumes x0:
"x0 \ H" "x0 \ E" "x0 \ 0"
assumes E:
"vectorspace E"
shows "linearform H' h'"
proof -
interpret linearform H h
by fact
interpret vectorspace E
by fact
show ?thesis
proof
note E =
‹vectorspace E
›
have H
': "vectorspace H'"
proof (unfold H
'_def)
from ‹x0
∈ E
›
have "lin x0 \ E" ..
with HE
show "vectorspace (H + lin x0)" using E ..
qed
show "h' (x1 + x2) = h' x1 + h' x2" if x1:
"x1 \ H'" and x2:
"x2 \ H'" for x1 x2
proof -
from H
' x1 x2 have "x1 + x2 \ H'"
by (rule vectorspace.add_closed)
with x1 x2
obtain y y1 y2 a a1 a2
where
x1x2:
"x1 + x2 = y + a \ x0" and y:
"y \ H"
and x1_rep:
"x1 = y1 + a1 \ x0" and y1:
"y1 \ H"
and x2_rep:
"x2 = y2 + a2 \ x0" and y2:
"y2 \ H"
unfolding H
'_def sum_def lin_def by blast
have ya:
"y1 + y2 = y \ a1 + a2 = a" using E HE _ y x0
proof (rule decomp_H
') text_raw \\label{decomp-H-use}\
from HE y1 y2
show "y1 + y2 \ H"
by (rule subspace.add_closed)
from x0
and HE y y1 y2
have "x0 \ E" "y \ E" "y1 \ E" "y2 \ E" by auto
with x1_rep x2_rep
have "(y1 + y2) + (a1 + a2) \ x0 = x1 + x2"
by (simp add: add_ac add_mult_distrib2)
also note x1x2
finally show "(y1 + y2) + (a1 + a2) \ x0 = y + a \ x0" .
qed
from h
'_def x1x2 E HE y x0
have "h' (x1 + x2) = h y + a * xi"
by (rule h
'_definite)
also have "\ = h (y1 + y2) + (a1 + a2) * xi"
by (simp only: ya)
also from y1 y2
have "h (y1 + y2) = h y1 + h y2"
by simp
also have "\ + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
by (simp add: distrib_right)
also from h
'_def x1_rep E HE y1 x0
have "h y1 + a1 * xi = h' x1"
by (rule h
'_definite [symmetric])
also from h
'_def x2_rep E HE y2 x0
have "h y2 + a2 * xi = h' x2"
by (rule h
'_definite [symmetric])
finally show ?thesis .
qed
show "h' (c \ x1) = c * (h' x1)" if x1:
"x1 \ H'" for x1 c
proof -
from H
' x1 have ax1: "c \ x1 \ H'"
by (rule vectorspace.mult_closed)
with x1
obtain y a y1 a1
where
cx1_rep:
"c \ x1 = y + a \ x0" and y:
"y \ H"
and x1_rep:
"x1 = y1 + a1 \ x0" and y1:
"y1 \ H"
unfolding H
'_def sum_def lin_def by blast
have ya:
"c \ y1 = y \ c * a1 = a" using E HE _ y x0
proof (rule decomp_H
')
from HE y1
show "c \ y1 \ H"
by (rule subspace.mult_closed)
from x0
and HE y y1
have "x0 \ E" "y \ E" "y1 \ E" by auto
with x1_rep
have "c \ y1 + (c * a1) \ x0 = c \ x1"
by (simp add: mult_assoc add_mult_distrib1)
also note cx1_rep
finally show "c \ y1 + (c * a1) \ x0 = y + a \ x0" .
qed
from h
'_def cx1_rep E HE y x0 have "h' (c
⋅ x1) = h y + a * xi
"
by (rule h
'_definite)
also have "\ = h (c \ y1) + (c * a1) * xi"
by (simp only: ya)
also from y1
have "h (c \ y1) = c * h y1"
by simp
also have "\ + (c * a1) * xi = c * (h y1 + a1 * xi)"
by (simp only: distrib_left)
also from h
'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1
"
by (rule h
'_definite [symmetric])
finally show ?thesis .
qed
qed
qed
text ‹
🚫
The linear extension
‹h
'\ of \h\ is bounded by the seminorm \p\.
›
lemma h
'_norm_pres:
assumes h
'_def: "\x. h' x = (
let (y, a) =
SOME (y, a). x = y + a
⋅ x0
∧ y
∈ H
in h y + a * xi)
"
and H
'_def: "H' = H + lin x0
"
and x0:
"x0 \ H" "x0 \ E" "x0 \ 0"
assumes E:
"vectorspace E" and HE:
"subspace H E"
and "seminorm E p" and "linearform H h"
assumes a:
"\y \ H. h y \ p y"
and a
': "\y \ H. - p (y + x0) - h y \ xi \ xi \ p (y + x0) - h y"
shows "\x \ H'. h' x \ p x"
proof -
interpret vectorspace E
by fact
interpret subspace H E
by fact
interpret seminorm E p
by fact
interpret linearform H h
by fact
show ?thesis
proof
fix x
assume x
': "x \ H'"
show "h' x \ p x"
proof -
from a
' have a1: "\ya \ H. - p (ya + x0) - h ya \ xi"
and a2:
"\ya \ H. xi \ p (ya + x0) - h ya" by auto
from x
' obtain y a where
x_rep:
"x = y + a \ x0" and y:
"y \ H"
unfolding H
'_def sum_def lin_def by blast
from y
have y
': "y \ E" ..
from y
have ay:
"inverse a \ y \ H" by simp
from h
'_def x_rep E HE y x0 have "h' x = h y + a * xi
"
by (rule h
'_definite)
also have "\ \ p (y + a \ x0)"
proof (rule linorder_cases)
assume z:
"a = 0"
then have "h y + a * xi = h y" by simp
also from a y
have "\ \ p y" ..
also from x0 y
' z have "p y = p (y + a \ x0)" by simp
finally show ?thesis .
next
txt ‹In the
case ‹a < 0
›, we
use ‹a
🚫1
›
with ‹ya
› taken as
‹y / a
›:
›
assume lz:
"a < 0" then have nz:
"a \ 0" by simp
from a1 ay
have "- p (inverse a \ y + x0) - h (inverse a \ y) \ xi" ..
with lz
have "a * xi \
a * (- p (inverse a
⋅ y + x0) - h (inverse a
⋅ y))
"
by (simp add: mult_left_mono_neg order_less_imp_le)
also have "\ =
- a * (p (inverse a
⋅ y + x0)) - a * (h (inverse a
⋅ y))
"
by (simp add: right_diff_distrib)
also from lz x0 y
' have "- a * (p (inverse a \ y + x0)) =
p (a
⋅ (inverse a
⋅ y + x0))
"
by (simp add: abs_homogenous)
also from nz x0 y
' have "\ = p (y + a \ x0)"
by (simp add: add_mult_distrib1 mult_assoc [symmetric])
also from nz y
have "a * (h (inverse a \ y)) = h y"
by simp
finally have "a * xi \ p (y + a \ x0) - h y" .
then show ?thesis
by simp
next
txt ‹In the
case ‹a > 0
›, we
use ‹a
🚫2
›
with ‹ya
› taken as
‹y / a
›:
›
assume gz:
"0 < a" then have nz:
"a \ 0" by simp
from a2 ay
have "xi \ p (inverse a \ y + x0) - h (inverse a \ y)" ..
with gz
have "a * xi \
a * (p (inverse a
⋅ y + x0) - h (inverse a
⋅ y))
"
by simp
also have "\ = a * p (inverse a \ y + x0) - a * h (inverse a \ y)"
by (simp add: right_diff_distrib)
also from gz x0 y
'
have "a * p (inverse a \ y + x0) = p (a \ (inverse a \ y + x0))"
by (simp add: abs_homogenous)
also from nz x0 y
' have "\ = p (y + a \ x0)"
by (simp add: add_mult_distrib1 mult_assoc [symmetric])
also from nz y
have "a * h (inverse a \ y) = h y"
by simp
finally have "a * xi \ p (y + a \ x0) - h y" .
then show ?thesis
by simp
qed
also from x_rep
have "\ = p x" by (simp only:)
finally show ?thesis .
qed
qed
qed
end
