Theory Function_Order

(*  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