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