Quelle  Function_Order.thy   Sprache: Isabelle

(*  Title:      HOL/Hahn_Banach/Function_Order.thy
    Author:     Gertrud Bauer, TU Munich
*)

section ‹An order on functions›

theory Function_Order
imports Subspace Linearform
begin

subsection ‹The graph of a function›

text ‹
  We define the 🚫‹graph› of a (real) function ‹f› with domain ‹F› as the set
  \begin{center}
  ‹{(x, f x). x ∈ F}›
  \end{center}
  So we are modeling partial functions by specifying the domain and the
  mapping function. We use the term ``function'' also for its graph.
›

type_synonym 'a graph = "('a × 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 ‹Functions ordered by domain extension›

text ‹
  A function ‹h'\ is an extension of \h\, iff the graph of \h\ is a subset of
  the graph of ‹h'\.
›

lemma graph_extI:
  "(\x. x \ H \ h x = h' x) \ H \ H'
    ==> graph H h ⊆ 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 ‹Domain and function of a graph›

text ‹
  The inverse functions to ‹graph› are ‹domain› and ‹funct›.
›

definition domain :: "'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 ‹
  The following lemma states that ‹g› is the graph of a function if the
  relation induced by ‹g› is unique.
›

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 ‹Norm-preserving extensions of a function›

text ‹
  Given a linear form ‹f› on the space ‹F› and a seminorm ‹p› on ‹E›. The set
  of all linear extensions of ‹f›, to superspaces ‹H› of ‹F›, which are
  bounded by ‹p›, is defined as follows.
›

definition
  norm_pres_extensions ::
    "'a::{plus,minus,uminus,zero} set \ ('a \ real) \ 'a set \ ('a \ real)
      ==> 'a graph set"
where
  "norm_pres_extensions E p F f
    = {g. ∃H h. g = graph H h
        ∧ linearform H h
        ∧ H ⊴ E
        ∧ F ⊴ H
        ∧ graph F f ⊆ graph H h
        ∧ (∀x ∈ H. h x ≤ 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
    ==> graph F f ⊆ graph H h ==> ∀x ∈ H. h x ≤ p x
    ==> graph H h ∈ 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
    ∧ linearform H h
    ∧ H ⊴ E
    ∧ F ⊴ H
    ∧ graph F f ⊆ graph H h
    ∧ (∀x ∈ H. h x ≤ p x) ==> g ∈ norm_pres_extensions E p F f"
  unfolding norm_pres_extensions_def by blast

end