author | wenzelm |
Mon, 07 Feb 2000 18:38:51 +0100 | |
changeset 8203 | 2fcc6017cb72 |
parent 7978 | 1b99ee57d131 |
child 9035 | 371f023d3dbd |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/FunctionOrder.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
5 |
|
7978 | 6 |
header {* An order on functions *}; |
7808 | 7 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
8 |
theory FunctionOrder = Subspace + Linearform:; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
9 |
|
7917 | 10 |
subsection {* The graph of a function *}; |
7808 | 11 |
|
7978 | 12 |
text{* We define the \emph{graph} of a (real) function $f$ with |
7917 | 13 |
domain $F$ as the set |
7927 | 14 |
\[ |
15 |
\{(x, f\ap x). \ap x:F\} |
|
16 |
\] |
|
7978 | 17 |
So we are modeling partial functions by specifying the domain and |
18 |
the mapping function. We use the term ``function'' also for its graph. |
|
7917 | 19 |
*}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
20 |
|
7978 | 21 |
types 'a graph = "('a * real) set"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
23 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
24 |
graph :: "['a set, 'a => real] => 'a graph " |
7978 | 25 |
"graph F f == {(x, f x) | x. x:F}"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
26 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
27 |
lemma graphI [intro??]: "x:F ==> (x, f x) : graph F f"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
28 |
by (unfold graph_def, intro CollectI exI) force; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
29 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
30 |
lemma graphI2 [intro??]: "x:F ==> EX t: (graph F f). t = (x, f x)"; |
7566 | 31 |
by (unfold graph_def, force); |
32 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
33 |
lemma graphD1 [intro??]: "(x, y): graph F f ==> x:F"; |
7566 | 34 |
by (unfold graph_def, elim CollectE exE) force; |
35 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
36 |
lemma graphD2 [intro??]: "(x, y): graph H h ==> y = h x"; |
7566 | 37 |
by (unfold graph_def, elim CollectE exE) force; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
38 |
|
7917 | 39 |
subsection {* Functions ordered by domain extension *}; |
40 |
||
7978 | 41 |
text{* A function $h'$ is an extension of $h$, iff the graph of |
7917 | 42 |
$h$ is a subset of the graph of $h'$.*}; |
43 |
||
44 |
lemma graph_extI: |
|
45 |
"[| !! x. x: H ==> h x = h' x; H <= H'|] |
|
46 |
==> graph H h <= graph H' h'"; |
|
47 |
by (unfold graph_def, force); |
|
48 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
49 |
lemma graph_extD1 [intro??]: |
7808 | 50 |
"[| graph H h <= graph H' h'; x:H |] ==> h x = h' x"; |
7566 | 51 |
by (unfold graph_def, force); |
52 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
53 |
lemma graph_extD2 [intro??]: |
7917 | 54 |
"[| graph H h <= graph H' h' |] ==> H <= H'"; |
7566 | 55 |
by (unfold graph_def, force); |
56 |
||
7917 | 57 |
subsection {* Domain and function of a graph *}; |
58 |
||
59 |
text{* The inverse functions to $\idt{graph}$ are $\idt{domain}$ and |
|
60 |
$\idt{funct}$.*}; |
|
61 |
||
62 |
constdefs |
|
63 |
domain :: "'a graph => 'a set" |
|
64 |
"domain g == {x. EX y. (x, y):g}" |
|
65 |
||
66 |
funct :: "'a graph => ('a => real)" |
|
67 |
"funct g == \<lambda>x. (SOME y. (x, y):g)"; |
|
68 |
||
69 |
(*text{* The equations |
|
70 |
\begin{matharray} |
|
71 |
\idt{domain} graph F f = F {\rm and}\\ |
|
72 |
\idt{funct} graph F f = f |
|
73 |
\end{matharray} |
|
74 |
hold, but are not proved here. |
|
75 |
*};*) |
|
76 |
||
77 |
text {* The following lemma states that $g$ is the graph of a function |
|
78 |
if the relation induced by $g$ is unique. *}; |
|
7566 | 79 |
|
80 |
lemma graph_domain_funct: |
|
7808 | 81 |
"(!!x y z. (x, y):g ==> (x, z):g ==> z = y) |
82 |
==> graph (domain g) (funct g) = g"; |
|
7978 | 83 |
proof (unfold domain_def funct_def graph_def, auto); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
84 |
fix a b; assume "(a, b) : g"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
85 |
show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
86 |
show "EX y. (a, y) : g"; ..; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
87 |
assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
88 |
show "b = (SOME y. (a, y) : g)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
89 |
proof (rule select_equality [RS sym]); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
90 |
fix y; assume "(a, y):g"; show "y = b"; by (rule uniq); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
91 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
92 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
93 |
|
7808 | 94 |
|
95 |
||
7978 | 96 |
subsection {* Norm-preserving extensions of a function *}; |
7917 | 97 |
|
7978 | 98 |
text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on |
7917 | 99 |
$E$. The set of all linear extensions of $f$, to superspaces $H$ of |
100 |
$F$, which are bounded by $p$, is defined as follows. *}; |
|
7808 | 101 |
|
102 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
103 |
constdefs |
7656 | 104 |
norm_pres_extensions :: |
7917 | 105 |
"['a::{minus, plus} set, 'a => real, 'a set, 'a => real] |
106 |
=> 'a graph set" |
|
107 |
"norm_pres_extensions E p F f |
|
108 |
== {g. EX H h. graph H h = g |
|
109 |
& is_linearform H h |
|
110 |
& is_subspace H E |
|
111 |
& is_subspace F H |
|
112 |
& graph F f <= graph H h |
|
113 |
& (ALL x:H. h x <= p x)}"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
114 |
|
7656 | 115 |
lemma norm_pres_extension_D: |
7917 | 116 |
"g : norm_pres_extensions E p F f |
117 |
==> EX H h. graph H h = g |
|
118 |
& is_linearform H h |
|
119 |
& is_subspace H E |
|
120 |
& is_subspace F H |
|
121 |
& graph F f <= graph H h |
|
122 |
& (ALL x:H. h x <= p x)"; |
|
123 |
by (unfold norm_pres_extensions_def) force; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
124 |
|
7656 | 125 |
lemma norm_pres_extensionI2 [intro]: |
7917 | 126 |
"[| is_linearform H h; is_subspace H E; is_subspace F H; |
127 |
graph F f <= graph H h; ALL x:H. h x <= p x |] |
|
128 |
==> (graph H h : norm_pres_extensions E p F f)"; |
|
7656 | 129 |
by (unfold norm_pres_extensions_def) force; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
130 |
|
7656 | 131 |
lemma norm_pres_extensionI [intro]: |
7917 | 132 |
"EX H h. graph H h = g |
133 |
& is_linearform H h |
|
134 |
& is_subspace H E |
|
135 |
& is_subspace F H |
|
136 |
& graph F f <= graph H h |
|
137 |
& (ALL x:H. h x <= p x) |
|
138 |
==> g: norm_pres_extensions E p F f"; |
|
139 |
by (unfold norm_pres_extensions_def) force; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
140 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
141 |
end; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
142 |