# Theory Function_Order

theory Function_Order
imports Subspace Linearform
(*  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