author | wenzelm |
Thu, 14 Jun 2007 00:22:45 +0200 | |
changeset 23378 | 1d138d6bb461 |
parent 21404 | eb85850d3eb7 |
child 25762 | c03e9d04b3e4 |
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 |
|
16417 | 8 |
theory FunctionOrder imports Subspace Linearform begin |
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 |
|
10687 | 12 |
text {* |
13 |
We define the \emph{graph} of a (real) function @{text f} with |
|
14 |
domain @{text F} as the set |
|
15 |
\begin{center} |
|
16 |
@{text "{(x, f x). x \<in> F}"} |
|
17 |
\end{center} |
|
18 |
So we are modeling partial functions by specifying the domain and |
|
19 |
the mapping function. We use the term ``function'' also for its |
|
20 |
graph. |
|
9035 | 21 |
*} |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
|
13515 | 23 |
types 'a graph = "('a \<times> real) set" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
24 |
|
19736 | 25 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
26 |
graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where |
19736 | 27 |
"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
|
28 |
|
13515 | 29 |
lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f" |
11472 | 30 |
by (unfold graph_def) blast |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
31 |
|
13515 | 32 |
lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)" |
10687 | 33 |
by (unfold graph_def) blast |
7566 | 34 |
|
13515 | 35 |
lemma graphE [elim?]: |
36 |
"(x, y) \<in> graph F f \<Longrightarrow> (x \<in> F \<Longrightarrow> y = f x \<Longrightarrow> C) \<Longrightarrow> C" |
|
10687 | 37 |
by (unfold graph_def) blast |
38 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
39 |
|
9035 | 40 |
subsection {* Functions ordered by domain extension *} |
7917 | 41 |
|
13515 | 42 |
text {* |
43 |
A function @{text h'} is an extension of @{text h}, iff the graph of |
|
44 |
@{text h} is a subset of the graph of @{text h'}. |
|
45 |
*} |
|
7917 | 46 |
|
10687 | 47 |
lemma graph_extI: |
48 |
"(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H' |
|
13515 | 49 |
\<Longrightarrow> graph H h \<subseteq> graph H' h'" |
10687 | 50 |
by (unfold graph_def) blast |
7917 | 51 |
|
13515 | 52 |
lemma graph_extD1 [dest?]: |
10687 | 53 |
"graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x" |
54 |
by (unfold graph_def) blast |
|
7566 | 55 |
|
13515 | 56 |
lemma graph_extD2 [dest?]: |
10687 | 57 |
"graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'" |
58 |
by (unfold graph_def) blast |
|
7566 | 59 |
|
13515 | 60 |
|
9035 | 61 |
subsection {* Domain and function of a graph *} |
7917 | 62 |
|
10687 | 63 |
text {* |
13515 | 64 |
The inverse functions to @{text graph} are @{text domain} and @{text |
65 |
funct}. |
|
10687 | 66 |
*} |
7917 | 67 |
|
19736 | 68 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
69 |
"domain" :: "'a graph \<Rightarrow> 'a set" where |
19736 | 70 |
"domain g = {x. \<exists>y. (x, y) \<in> g}" |
7917 | 71 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
72 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
73 |
funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)" where |
19736 | 74 |
"funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))" |
7917 | 75 |
|
10687 | 76 |
text {* |
77 |
The following lemma states that @{text g} is the graph of a function |
|
78 |
if the relation induced by @{text g} is unique. |
|
79 |
*} |
|
7566 | 80 |
|
10687 | 81 |
lemma graph_domain_funct: |
13515 | 82 |
assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y" |
83 |
shows "graph (domain g) (funct g) = g" |
|
84 |
proof (unfold domain_def funct_def graph_def, auto) (* FIXME !? *) |
|
23378 | 85 |
fix a b assume g: "(a, b) \<in> g" |
86 |
from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2) |
|
87 |
from g show "\<exists>y. (a, y) \<in> g" .. |
|
88 |
from g show "b = (SOME y. (a, y) \<in> g)" |
|
9969 | 89 |
proof (rule some_equality [symmetric]) |
13515 | 90 |
fix y assume "(a, y) \<in> g" |
23378 | 91 |
with g show "y = b" by (rule uniq) |
9035 | 92 |
qed |
93 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
94 |
|
7808 | 95 |
|
9035 | 96 |
subsection {* Norm-preserving extensions of a function *} |
7917 | 97 |
|
10687 | 98 |
text {* |
99 |
Given a linear form @{text f} on the space @{text F} and a seminorm |
|
100 |
@{text p} on @{text E}. The set of all linear extensions of @{text |
|
101 |
f}, to superspaces @{text H} of @{text F}, which are bounded by |
|
102 |
@{text p}, is defined as follows. |
|
103 |
*} |
|
7808 | 104 |
|
19736 | 105 |
definition |
10687 | 106 |
norm_pres_extensions :: |
107 |
"'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
108 |
\<Rightarrow> 'a graph set" where |
10687 | 109 |
"norm_pres_extensions E p F f |
19736 | 110 |
= {g. \<exists>H h. g = graph H h |
13515 | 111 |
\<and> linearform H h |
112 |
\<and> H \<unlhd> E |
|
113 |
\<and> F \<unlhd> H |
|
114 |
\<and> graph F f \<subseteq> graph H h |
|
115 |
\<and> (\<forall>x \<in> H. h x \<le> p x)}" |
|
10687 | 116 |
|
13515 | 117 |
lemma norm_pres_extensionE [elim]: |
9503 | 118 |
"g \<in> norm_pres_extensions E p F f |
13515 | 119 |
\<Longrightarrow> (\<And>H h. g = graph H h \<Longrightarrow> linearform H h |
120 |
\<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H \<Longrightarrow> graph F f \<subseteq> graph H h |
|
121 |
\<Longrightarrow> \<forall>x \<in> H. h x \<le> p x \<Longrightarrow> C) \<Longrightarrow> C" |
|
10687 | 122 |
by (unfold norm_pres_extensions_def) blast |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
123 |
|
10687 | 124 |
lemma norm_pres_extensionI2 [intro]: |
13515 | 125 |
"linearform H h \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H |
126 |
\<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x |
|
127 |
\<Longrightarrow> graph H h \<in> norm_pres_extensions E p F f" |
|
128 |
by (unfold norm_pres_extensions_def) blast |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
129 |
|
13515 | 130 |
lemma norm_pres_extensionI: (* FIXME ? *) |
131 |
"\<exists>H h. g = graph H h |
|
132 |
\<and> linearform H h |
|
133 |
\<and> H \<unlhd> E |
|
134 |
\<and> F \<unlhd> H |
|
135 |
\<and> graph F f \<subseteq> graph H h |
|
136 |
\<and> (\<forall>x \<in> H. h x \<le> p x) \<Longrightarrow> g \<in> norm_pres_extensions E p F f" |
|
10687 | 137 |
by (unfold norm_pres_extensions_def) blast |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
138 |
|
10687 | 139 |
end |