Theory Hahn_Banach_Sup_Lemmas

theory Hahn_Banach_Sup_Lemmas
imports Function_Norm Zorn_Lemma
(*  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"
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'"
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" ..
fix x y assume "x ∈ F" and "y ∈ F"
with FE show "x + y ∈ F" by (rule subspace.add_closed)
next
fix x a assume "x ∈ F"
with FE show "a ⋅ x ∈ F" 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'"
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› ..
{
assume l: ?L
show ?R
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
next
assume r: ?R
show ?L
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