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