(* Title: HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
ID: $Id$
Author: Gertrud Bauer, TU Munich
*)
header {* The supremum w.r.t.~the function order *}
theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:
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 @{text E} be a real vector space with a seminorm
@{text p} on @{text E}. @{text F} is a subspace of @{text E} and
@{text f} a linear form on @{text F}. We consider a chain @{text c}
of norm-preserving extensions of @{text f}, such that
@{text "\<Union>c = graph H h"}. We will show some properties about the
limit function @{text h}, i.e.\ the supremum of the chain @{text c}.
*}
text {*
Let @{text c} be a chain of norm-preserving extensions of the
function @{text f} and let @{text "graph H h"} be the supremum of
@{text c}. Every element in @{text H} is member of one of the
elements of the chain.
*}
lemma some_H'h't:
"M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
graph H h = \<Union>c \<Longrightarrow> x \<in> H
\<Longrightarrow> \<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
\<and> is_linearform H' h' \<and> is_subspace H' E
\<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
\<and> (\<forall>x \<in> H'. h' x \<le> p x)"
proof -
assume m: "M = norm_pres_extensions E p F f" and "c \<in> chain M"
and u: "graph H h = \<Union>c" "x \<in> H"
have h: "(x, h x) \<in> graph H h" ..
with u have "(x, h x) \<in> \<Union>c" by simp
hence ex1: "\<exists>g \<in> c. (x, h x) \<in> g"
by (simp only: Union_iff)
thus ?thesis
proof (elim bexE)
fix g assume g: "g \<in> c" "(x, h x) \<in> g"
have "c \<subseteq> M" by (rule chainD2)
hence "g \<in> M" ..
hence "g \<in> norm_pres_extensions E p F f" by (simp only: m)
hence "\<exists>H' h'. graph H' h' = g
\<and> is_linearform H' h'
\<and> is_subspace H' E
\<and> is_subspace F H'
\<and> graph F f \<subseteq> graph H' h'
\<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule norm_pres_extension_D)
thus ?thesis
proof (elim exE conjE)
fix H' h'
assume "graph H' h' = g" "is_linearform H' h'"
"is_subspace H' E" "is_subspace F H'"
"graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
show ?thesis
proof (intro exI conjI)
show "graph H' h' \<in> c" by (simp!)
show "(x, h x) \<in> graph H' h'" by (simp!)
qed
qed
qed
qed
text {*
\medskip Let @{text c} be a chain of norm-preserving extensions of
the function @{text f} and let @{text "graph H h"} be the supremum
of @{text c}. Every element in the domain @{text H} of the supremum
function is member of the domain @{text H'} of some function @{text
h'}, such that @{text h} extends @{text h'}.
*}
lemma some_H'h':
"M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
graph H h = \<Union>c \<Longrightarrow> x \<in> H
\<Longrightarrow> \<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
\<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
\<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
proof -
assume "M = norm_pres_extensions E p F f" and cM: "c \<in> chain M"
and u: "graph H h = \<Union>c" "x \<in> H"
have "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
\<and> is_linearform H' h' \<and> is_subspace H' E
\<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
\<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h't)
thus ?thesis
proof (elim exE conjE)
fix H' h' assume "(x, h x) \<in> graph H' h'" "graph H' h' \<in> c"
"is_linearform H' h'" "is_subspace H' E" "is_subspace F H'"
"graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
show ?thesis
proof (intro exI conjI)
show "x \<in> H'" by (rule graphD1)
from cM u show "graph H' h' \<subseteq> graph H h"
by (simp! only: chain_ball_Union_upper)
qed
qed
qed
text {*
\medskip Any two elements @{text x} and @{text y} in the domain
@{text H} of the supremum function @{text h} are both in the domain
@{text H'} of some function @{text h'}, such that @{text h} extends
@{text h'}.
*}
lemma some_H'h'2:
"M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
graph H h = \<Union>c \<Longrightarrow> x \<in> H \<Longrightarrow> y \<in> H
\<Longrightarrow> \<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
\<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
\<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
proof -
assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
"graph H h = \<Union>c" "x \<in> H" "y \<in> H"
txt {*
@{text x} is in the domain @{text H'} of some function @{text h'},
such that @{text h} extends @{text h'}. *}
have e1: "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
\<and> is_linearform H' h' \<and> is_subspace H' E
\<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
\<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h't)
txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
such that @{text h} extends @{text h''}. *}
have e2: "\<exists>H'' h''. graph H'' h'' \<in> c \<and> (y, h y) \<in> graph H'' h''
\<and> is_linearform H'' h'' \<and> is_subspace H'' E
\<and> is_subspace F H'' \<and> graph F f \<subseteq> graph H'' h''
\<and> (\<forall>x \<in> H''. h'' x \<le> p x)"
by (rule some_H'h't)
from e1 e2 show ?thesis
proof (elim exE conjE)
fix H' h' assume "(y, h y) \<in> graph H' h'" "graph H' h' \<in> c"
"is_linearform H' h'" "is_subspace H' E" "is_subspace F H'"
"graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
fix H'' h'' assume "(x, h x) \<in> graph H'' h''" "graph H'' h'' \<in> c"
"is_linearform H'' h''" "is_subspace H'' E" "is_subspace F H''"
"graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x"
txt {* Since both @{text h'} and @{text h''} are elements of the chain,
@{text h''} is an extension of @{text h'} or vice versa. Thus both
@{text x} and @{text y} are contained in the greater one. \label{cases1}*}
have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
(is "?case1 \<or> ?case2")
by (rule chainD)
thus ?thesis
proof
assume ?case1
show ?thesis
proof (intro exI conjI)
have "(x, h x) \<in> graph H'' h''" .
also have "... \<subseteq> graph H' h'" .
finally have xh:"(x, h x) \<in> graph H' h'" .
thus x: "x \<in> H'" ..
show y: "y \<in> H'" ..
show "graph H' h' \<subseteq> graph H h"
by (simp! only: chain_ball_Union_upper)
qed
next
assume ?case2
show ?thesis
proof (intro exI conjI)
show x: "x \<in> H''" ..
have "(y, h y) \<in> graph H' h'" by (simp!)
also have "... \<subseteq> graph H'' h''" .
finally have yh: "(y, h y) \<in> graph H'' h''" .
thus y: "y \<in> H''" ..
show "graph H'' h'' \<subseteq> graph H h"
by (simp! only: chain_ball_Union_upper)
qed
qed
qed
qed
text {*
\medskip The relation induced by the graph of the supremum of a
chain @{text c} is definite, i.~e.~t is the graph of a function. *}
lemma sup_definite:
"M \<equiv> norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
(x, y) \<in> \<Union>c \<Longrightarrow> (x, z) \<in> \<Union>c \<Longrightarrow> z = y"
proof -
assume "c \<in> chain M" "M \<equiv> norm_pres_extensions E p F f"
"(x, y) \<in> \<Union>c" "(x, z) \<in> \<Union>c"
thus ?thesis
proof (elim UnionE chainE2)
txt {* Since both @{text "(x, y) \<in> \<Union>c"} and @{text "(x, z) \<in> \<Union>c"}
they are members of some graphs @{text "G\<^sub>1"} and @{text
"G\<^sub>2"}, resp., such that both @{text "G\<^sub>1"} and @{text
"G\<^sub>2"} are members of @{text c}.*}
fix G1 G2 assume
"(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \<subseteq> M"
have "G1 \<in> M" ..
hence e1: "\<exists>H1 h1. graph H1 h1 = G1"
by (blast! dest: norm_pres_extension_D)
have "G2 \<in> M" ..
hence e2: "\<exists>H2 h2. graph H2 h2 = G2"
by (blast! dest: norm_pres_extension_D)
from e1 e2 show ?thesis
proof (elim exE)
fix H1 h1 H2 h2
assume "graph H1 h1 = G1" "graph H2 h2 = G2"
txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
or vice versa, since both @{text "G\<^sub>1"} and @{text
"G\<^sub>2"} are members of @{text c}. \label{cases2}*}
have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
thus ?thesis
proof
assume ?case1
have "(x, y) \<in> graph H2 h2" by (blast!)
hence "y = h2 x" ..
also have "(x, z) \<in> graph H2 h2" by (simp!)
hence "z = h2 x" ..
finally show ?thesis .
next
assume ?case2
have "(x, y) \<in> graph H1 h1" by (simp!)
hence "y = h1 x" ..
also have "(x, z) \<in> graph H1 h1" by (blast!)
hence "z = h1 x" ..
finally show ?thesis .
qed
qed
qed
qed
text {*
\medskip The limit function @{text h} is linear. Every element
@{text x} in the domain of @{text h} is in the domain of a function
@{text h'} in the chain of norm preserving extensions. Furthermore,
@{text h} is an extension of @{text h'} so the function values of
@{text x} are identical for @{text h'} and @{text h}. Finally, the
function @{text h'} is linear by construction of @{text M}.
*}
lemma sup_lf:
"M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
graph H h = \<Union>c \<Longrightarrow> is_linearform H h"
proof -
assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
"graph H h = \<Union>c"
show "is_linearform H h"
proof
fix x y assume "x \<in> H" "y \<in> H"
have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
\<and> is_linearform H' h' \<and> is_subspace H' E
\<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
\<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h'2)
txt {* We have to show that @{text h} is additive. *}
thus "h (x + y) = h x + h y"
proof (elim exE conjE)
fix H' h' assume "x \<in> H'" "y \<in> H'"
and b: "graph H' h' \<subseteq> graph H h"
and "is_linearform H' h'" "is_subspace H' E"
have "h' (x + y) = h' x + h' y"
by (rule linearform_add)
also have "h' x = h x" ..
also have "h' y = h y" ..
also have "x + y \<in> H'" ..
with b have "h' (x + y) = h (x + y)" ..
finally show ?thesis .
qed
next
fix a x assume "x \<in> H"
have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
\<and> is_linearform H' h' \<and> is_subspace H' E
\<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
\<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h')
txt{* We have to show that @{text h} is multiplicative. *}
thus "h (a \<cdot> x) = a * h x"
proof (elim exE conjE)
fix H' h' assume "x \<in> H'"
and b: "graph H' h' \<subseteq> graph H h"
and "is_linearform H' h'" "is_subspace H' E"
have "h' (a \<cdot> x) = a * h' x"
by (rule linearform_mult)
also have "h' x = h x" ..
also have "a \<cdot> x \<in> H'" ..
with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
finally show ?thesis .
qed
qed
qed
text {*
\medskip The limit of a non-empty chain of norm preserving
extensions of @{text f} is an extension of @{text f}, since every
element of the chain is an extension of @{text f} and the supremum
is an extension for every element of the chain.
*}
lemma sup_ext:
"graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
c \<in> chain M \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> graph F f \<subseteq> graph H h"
proof -
assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
"graph H h = \<Union>c"
assume "\<exists>x. x \<in> c"
thus ?thesis
proof
fix x assume "x \<in> c"
have "c \<subseteq> M" by (rule chainD2)
hence "x \<in> M" ..
hence "x \<in> norm_pres_extensions E p F f" by (simp!)
hence "\<exists>G g. graph G g = x
\<and> is_linearform G g
\<and> is_subspace G E
\<and> is_subspace F G
\<and> graph F f \<subseteq> graph G g
\<and> (\<forall>x \<in> G. g x \<le> p x)"
by (simp! add: norm_pres_extension_D)
thus ?thesis
proof (elim exE conjE)
fix G g assume "graph F f \<subseteq> graph G g"
also assume "graph G g = x"
also have "... \<in> c" .
hence "x \<subseteq> \<Union>c" by fast
also have [symmetric]: "graph H h = \<Union>c" .
finally show ?thesis .
qed
qed
qed
text {*
\medskip The domain @{text H} of the limit function is a superspace
of @{text F}, since @{text F} is a subset of @{text H}. The
existence of the @{text 0} element in @{text F} and the closure
properties follow from the fact that @{text F} is a vector space.
*}
lemma sup_supF:
"graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
c \<in> chain M \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> is_subspace F E \<Longrightarrow> is_vectorspace E
\<Longrightarrow> is_subspace F H"
proof -
assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c"
"graph H h = \<Union>c" "is_subspace F E" "is_vectorspace E"
show ?thesis
proof
show "0 \<in> F" ..
show "F \<subseteq> H"
proof (rule graph_extD2)
show "graph F f \<subseteq> graph H h"
by (rule sup_ext)
qed
show "\<forall>x \<in> F. \<forall>y \<in> F. x + y \<in> F"
proof (intro ballI)
fix x y assume "x \<in> F" "y \<in> F"
show "x + y \<in> F" by (simp!)
qed
show "\<forall>x \<in> F. \<forall>a. a \<cdot> x \<in> F"
proof (intro ballI allI)
fix x a assume "x\<in>F"
show "a \<cdot> x \<in> F" by (simp!)
qed
qed
qed
text {*
\medskip The domain @{text H} of the limit function is a subspace of
@{text E}.
*}
lemma sup_subE:
"graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
c \<in> chain M \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> is_subspace F E \<Longrightarrow> is_vectorspace E
\<Longrightarrow> is_subspace H E"
proof -
assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c"
"graph H h = \<Union>c" "is_subspace F E" "is_vectorspace E"
show ?thesis
proof
txt {* The @{text 0} element is in @{text H}, as @{text F} is a
subset of @{text H}: *}
have "0 \<in> F" ..
also have "is_subspace F H" by (rule sup_supF)
hence "F \<subseteq> H" ..
finally show "0 \<in> H" .
txt {* @{text H} is a subset of @{text E}: *}
show "H \<subseteq> E"
proof
fix x assume "x \<in> H"
have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
\<and> is_linearform H' h' \<and> is_subspace H' E
\<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
\<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h')
thus "x \<in> E"
proof (elim exE conjE)
fix H' h' assume "x \<in> H'" "is_subspace H' E"
have "H' \<subseteq> E" ..
thus "x \<in> E" ..
qed
qed
txt {* @{text H} is closed under addition: *}
show "\<forall>x \<in> H. \<forall>y \<in> H. x + y \<in> H"
proof (intro ballI)
fix x y assume "x \<in> H" "y \<in> H"
have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
\<and> is_linearform H' h' \<and> is_subspace H' E
\<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
\<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h'2)
thus "x + y \<in> H"
proof (elim exE conjE)
fix H' h'
assume "x \<in> H'" "y \<in> H'" "is_subspace H' E"
"graph H' h' \<subseteq> graph H h"
have "x + y \<in> H'" ..
also have "H' \<subseteq> H" ..
finally show ?thesis .
qed
qed
txt {* @{text H} is closed under scalar multiplication: *}
show "\<forall>x \<in> H. \<forall>a. a \<cdot> x \<in> H"
proof (intro ballI allI)
fix x a assume "x \<in> H"
have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
\<and> is_linearform H' h' \<and> is_subspace H' E
\<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
\<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h')
thus "a \<cdot> x \<in> H"
proof (elim exE conjE)
fix H' h'
assume "x \<in> H'" "is_subspace H' E" "graph H' h' \<subseteq> graph H h"
have "a \<cdot> x \<in> H'" ..
also have "H' \<subseteq> H" ..
finally show ?thesis .
qed
qed
qed
qed
text {*
\medskip The limit function is bounded by the norm @{text p} as
well, since all elements in the chain are bounded by @{text p}.
*}
lemma sup_norm_pres:
"graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
c \<in> chain M \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x"
proof
assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
"graph H h = \<Union>c"
fix x assume "x \<in> H"
have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
\<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
\<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h')
thus "h x \<le> p x"
proof (elim exE conjE)
fix H' h'
assume "x \<in> H'" "graph H' h' \<subseteq> graph H h"
and a: "\<forall>x \<in> H'. h' x \<le> p x"
have [symmetric]: "h' x = h x" ..
also from a have "h' x \<le> p x " ..
finally show ?thesis .
qed
qed
text {*
\medskip The following lemma is a property of linear forms on real
vector spaces. It will be used for the lemma @{text abs_HahnBanach}
(see page \pageref{abs-HahnBanach}). \label{abs-ineq-iff} For real
vector spaces the following inequations are equivalent:
\begin{center}
\begin{tabular}{lll}
@{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
@{text "\<forall>x \<in> H. h x \<le> p x"} \\
\end{tabular}
\end{center}
*}
lemma abs_ineq_iff:
"is_subspace H E \<Longrightarrow> is_vectorspace E \<Longrightarrow> is_seminorm E p \<Longrightarrow>
is_linearform H h
\<Longrightarrow> (\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)"
(concl is "?L = ?R")
proof -
assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p"
"is_linearform H h"
have h: "is_vectorspace H" ..
show ?thesis
proof
assume l: ?L
show ?R
proof
fix x assume x: "x \<in> H"
have "h x \<le> \<bar>h x\<bar>" by (rule abs_ge_self)
also from l have "... \<le> p x" ..
finally show "h x \<le> p x" .
qed
next
assume r: ?R
show ?L
proof
fix x assume "x \<in> H"
show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
by arith
show "- p x \<le> h x"
proof (rule real_minus_le)
from h have "- h x = h (- x)"
by (rule linearform_neg [symmetric])
also from r have "... \<le> p (- x)" by (simp!)
also have "... = p x"
proof (rule seminorm_minus)
show "x \<in> E" ..
qed
finally show "- h x \<le> p x" .
qed
from r show "h x \<le> p x" ..
qed
qed
qed
end