(* Title: HOL/Hahn_Banach/Function_Order.thy Author: Gertrud Bauer, TU Munich
*)
section \<open>An order on functions\<close>
theory Function_Order imports Subspace Linearform begin
subsection \<open>The graph of a function\<close>
text\<open>
We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with domain \<open>F\<close> as the set \begin{center} \<open>{(x, f x). x \<in> F}\<close> \end{center}
So we are modeling partial functions by specifying the domainand the
mapping function. We use the term ``function''alsofor its graph. \<close>
type_synonym'a graph = "('a \<times> real) set"
definition graph :: "'a set \ ('a \ real) \ 'a graph" where"graph F f = {(x, f x) | x. x \ F}"
lemma graphI [intro]: "x \ F \ (x, f x) \ graph F f" unfolding graph_def by blast
lemma graphI2 [intro?]: "x \ F \ \t \ graph F f. t = (x, f x)" unfolding graph_def by blast
lemma graphE [elim?]: assumes"(x, y) \ graph F f" obtains"x \ F" and "y = f x" using assms unfolding graph_def by blast
subsection \<open>Functions ordered by domain extension\<close>
text\<open>
A function\<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of \<open>h\<close> is a subset of
the graph of \<open>h'\<close>. \<close>
lemma graph_extI: "(\x. x \ H \ h x = h' x) \ H \ H' \<Longrightarrow> graph H h \<subseteq> graph H' h'" unfolding graph_def by blast
lemma graph_extD1 [dest?]: "graph H h \ graph H' h' \ x \ H \ h x = h' x" unfolding graph_def by blast
lemma graph_extD2 [dest?]: "graph H h \ graph H' h' \ H \ H'" unfolding graph_def by blast
subsection \<open>Domain and function of a graph\<close>
text\<open>
The inverse functions to\<open>graph\<close> are \<open>domain\<close> and \<open>funct\<close>. \<close>
definitiondomain :: "'a graph \ 'a set" where"domain g = {x. \y. (x, y) \ g}"
definition funct :: "'a graph \ ('a \ real)" where"funct g = (\x. (SOME y. (x, y) \ g))"
text\<open>
The following lemmastates that \<open>g\<close> is the graph of a function if the
relation induced by\<open>g\<close> is unique. \<close>
lemma graph_domain_funct: assumes uniq: "\x y z. (x, y) \ g \ (x, z) \ g \ z = y" shows"graph (domain g) (funct g) = g" unfolding domain_def funct_def graph_def proof auto (* FIXME !? *) fix a b assume g: "(a, b) \ g" from g show"(a, SOME y. (a, y) \ g) \ g" by (rule someI2) from g show"\y. (a, y) \ g" .. from g show"b = (SOME y. (a, y) \ g)" proof (rule some_equality [symmetric]) fix y assume"(a, y) \ g" with g show"y = b"by (rule uniq) qed qed
subsection \<open>Norm-preserving extensions of a function\<close>
text\<open>
Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The set
of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
bounded by\<open>p\<close>, is defined as follows. \<close>
definition
norm_pres_extensions :: "'a::{plus,minus,uminus,zero} set \ ('a \ real) \ 'a set \ ('a \ real) \<Rightarrow> 'a graph set" where "norm_pres_extensions E p F f
= {g. \<exists>H h. g = graph H h \<and> linearform H h \<and> H \<unlhd> E \<and> F \<unlhd> H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x \<in> H. h x \<le> p x)}"
lemma norm_pres_extensionE [elim]: assumes"g \ norm_pres_extensions E p F f" obtains H h where"g = graph H h" and"linearform H h" and"H \ E" and"F \ H" and"graph F f \ graph H h" and"\x \ H. h x \ p x" using assms unfolding norm_pres_extensions_def by blast
lemma norm_pres_extensionI2 [intro]: "linearform H h \ H \ E \ F \ H \<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x \<Longrightarrow> graph H h \<in> norm_pres_extensions E p F f" unfolding norm_pres_extensions_def by blast
lemma norm_pres_extensionI: (* FIXME ? *) "\H h. g = graph H h \<and> linearform H h \<and> H \<unlhd> E \<and> F \<unlhd> H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x \<in> H. h x \<le> p x) \<Longrightarrow> g \<in> norm_pres_extensions E p F f" unfolding norm_pres_extensions_def by blast
end
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
