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