author | bauerg |
Mon, 17 Jul 2000 18:17:54 +0200 | |
changeset 9379 | 21cfeae6659d |
parent 9374 | 153853af318b |
child 9408 | d3d56e1d2ec1 |
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 |
|
9035 | 6 |
header {* An order on functions *} |
7808 | 7 |
|
9035 | 8 |
theory FunctionOrder = Subspace + Linearform: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
9 |
|
9035 | 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 |
\[ |
9374 | 15 |
\{(x, f\ap x). \ap x \in F\} |
7927 | 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. |
|
9035 | 19 |
*} |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
20 |
|
9035 | 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 " |
9379 | 25 |
"graph F f == {(x, f x) | x. x \\<in> F}" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
26 |
|
9379 | 27 |
lemma graphI [intro??]: "x \\<in> F ==> (x, f x) \\<in> graph F f" |
9035 | 28 |
by (unfold graph_def, intro CollectI exI) force |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
29 |
|
9379 | 30 |
lemma graphI2 [intro??]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)" |
9035 | 31 |
by (unfold graph_def, force) |
7566 | 32 |
|
9379 | 33 |
lemma graphD1 [intro??]: "(x, y) \\<in> graph F f ==> x \\<in> F" |
9035 | 34 |
by (unfold graph_def, elim CollectE exE) force |
7566 | 35 |
|
9379 | 36 |
lemma graphD2 [intro??]: "(x, y) \\<in> graph H h ==> y = h x" |
9035 | 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 |
|
9035 | 39 |
subsection {* Functions ordered by domain extension *} |
7917 | 40 |
|
7978 | 41 |
text{* A function $h'$ is an extension of $h$, iff the graph of |
9035 | 42 |
$h$ is a subset of the graph of $h'$.*} |
7917 | 43 |
|
44 |
lemma graph_extI: |
|
9379 | 45 |
"[| !! x. x \\<in> H ==> h x = h' x; H <= H'|] |
9035 | 46 |
==> graph H h <= graph H' h'" |
47 |
by (unfold graph_def, force) |
|
7917 | 48 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
49 |
lemma graph_extD1 [intro??]: |
9379 | 50 |
"[| graph H h <= graph H' h'; x \\<in> H |] ==> h x = h' x" |
9035 | 51 |
by (unfold graph_def, force) |
7566 | 52 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
53 |
lemma graph_extD2 [intro??]: |
9035 | 54 |
"[| graph H h <= graph H' h' |] ==> H <= H'" |
55 |
by (unfold graph_def, force) |
|
7566 | 56 |
|
9035 | 57 |
subsection {* Domain and function of a graph *} |
7917 | 58 |
|
59 |
text{* The inverse functions to $\idt{graph}$ are $\idt{domain}$ and |
|
9035 | 60 |
$\idt{funct}$.*} |
7917 | 61 |
|
62 |
constdefs |
|
63 |
domain :: "'a graph => 'a set" |
|
9379 | 64 |
"domain g == {x. \\<exists>y. (x, y) \\<in> g}" |
7917 | 65 |
|
66 |
funct :: "'a graph => ('a => real)" |
|
9379 | 67 |
"funct g == \\<lambda>x. (SOME y. (x, y) \\<in> g)" |
7917 | 68 |
|
69 |
||
70 |
text {* The following lemma states that $g$ is the graph of a function |
|
9035 | 71 |
if the relation induced by $g$ is unique. *} |
7566 | 72 |
|
73 |
lemma graph_domain_funct: |
|
9379 | 74 |
"(!!x y z. (x, y) \\<in> g ==> (x, z) \\<in> g ==> z = y) |
9035 | 75 |
==> graph (domain g) (funct g) = g" |
76 |
proof (unfold domain_def funct_def graph_def, auto) |
|
9379 | 77 |
fix a b assume "(a, b) \\<in> g" |
78 |
show "(a, SOME y. (a, y) \\<in> g) \\<in> g" by (rule selectI2) |
|
79 |
show "\\<exists>y. (a, y) \\<in> g" .. |
|
80 |
assume uniq: "!!x y z. (x, y) \\<in> g ==> (x, z) \\<in> g ==> z = y" |
|
81 |
show "b = (SOME y. (a, y) \\<in> g)" |
|
9035 | 82 |
proof (rule select_equality [RS sym]) |
9379 | 83 |
fix y assume "(a, y) \\<in> g" show "y = b" by (rule uniq) |
9035 | 84 |
qed |
85 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
86 |
|
7808 | 87 |
|
88 |
||
9035 | 89 |
subsection {* Norm-preserving extensions of a function *} |
7917 | 90 |
|
7978 | 91 |
text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on |
7917 | 92 |
$E$. The set of all linear extensions of $f$, to superspaces $H$ of |
9035 | 93 |
$F$, which are bounded by $p$, is defined as follows. *} |
7808 | 94 |
|
95 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
96 |
constdefs |
7656 | 97 |
norm_pres_extensions :: |
9374 | 98 |
"['a::{plus, minus, zero} set, 'a => real, 'a set, 'a => real] |
7917 | 99 |
=> 'a graph set" |
100 |
"norm_pres_extensions E p F f |
|
9379 | 101 |
== {g. \\<exists>H h. graph H h = g |
102 |
\\<and> is_linearform H h |
|
103 |
\\<and> is_subspace H E |
|
104 |
\\<and> is_subspace F H |
|
105 |
\\<and> graph F f <= graph H h |
|
106 |
\\<and> (\\<forall>x \\<in> H. h x <= p x)}" |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
107 |
|
7656 | 108 |
lemma norm_pres_extension_D: |
9379 | 109 |
"g \\<in> norm_pres_extensions E p F f |
110 |
==> \\<exists>H h. graph H h = g |
|
111 |
\\<and> is_linearform H h |
|
112 |
\\<and> is_subspace H E |
|
113 |
\\<and> is_subspace F H |
|
114 |
\\<and> graph F f <= graph H h |
|
115 |
\\<and> (\\<forall>x \\<in> H. h x <= p x)" |
|
9035 | 116 |
by (unfold norm_pres_extensions_def) force |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
117 |
|
7656 | 118 |
lemma norm_pres_extensionI2 [intro]: |
7917 | 119 |
"[| is_linearform H h; is_subspace H E; is_subspace F H; |
9379 | 120 |
graph F f <= graph H h; \\<forall>x \\<in> H. h x <= p x |] |
121 |
==> (graph H h \\<in> norm_pres_extensions E p F f)" |
|
9035 | 122 |
by (unfold norm_pres_extensions_def) force |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
123 |
|
7656 | 124 |
lemma norm_pres_extensionI [intro]: |
9379 | 125 |
"\\<exists>H h. graph H h = g |
126 |
\\<and> is_linearform H h |
|
127 |
\\<and> is_subspace H E |
|
128 |
\\<and> is_subspace F H |
|
129 |
\\<and> graph F f <= graph H h |
|
130 |
\\<and> (\\<forall>x \\<in> H. h x <= p x) |
|
131 |
==> g \\<in> norm_pres_extensions E p F f" |
|
9035 | 132 |
by (unfold norm_pres_extensions_def) force |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
133 |
|
9035 | 134 |
end |