Theory Function_Order
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
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:
"∃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