Theory Hahn_Banach_Sup_Lemmas

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

section ‹The supremum wrt.\ the function order›

theory Hahn_Banach_Sup_Lemmas
imports Function_Norm Zorn_Lemma
begin

text ‹
  This section contains some lemmas that will be used in the proof of the
  Hahn-Banach Theorem. In this section the following context is presumed. Let
  ‹E› be a real vector space with a seminorm ‹p› on ‹E›. ‹F› is a subspace of
  ‹E› and ‹f› a linear form on ‹F›. We consider a chain ‹c› of norm-preserving
  extensions of ‹f›, such that ‹⋃c = graph H h›. We will show some properties
  about the limit function ‹h›, i.e.\ the supremum of the chain ‹c›.

  ┉
  Let ‹c› be a chain of norm-preserving extensions of the function ‹f› and let
  ‹graph H h› be the supremum of ‹c›. Every element in ‹H› is member of one of
  the elements of the chain.
›

lemmas [dest?] = chainsD
lemmas chainsE2 [elim?] = chainsD2 [elim_format]

lemma some_H'h't:
  assumes M: "M = norm_pres_extensions E p F f"
    and cM: "c ∈ chains M"
    and u: "graph H h = ⋃c"
    and x: "x ∈ H"
  shows "∃H' h'. graph H' h' ∈ c
    ∧ (x, h x) ∈ graph H' h'
    ∧ linearform H' h' ∧ H' ⊴ E
    ∧ F ⊴ H' ∧ graph F f ⊆ graph H' h'
    ∧ (∀x ∈ H'. h' x ≤ p x)"
proof -
  from x have "(x, h x) ∈ graph H h" ..
  also from u have "… = ⋃c" .
  finally obtain g where gc: "g ∈ c" and gh: "(x, h x) ∈ g" by blast

  from cM have "c ⊆ M" ..
  with gc have "g ∈ M" ..
  also from M have "… = norm_pres_extensions E p F f" .
  finally obtain H' and h' where g: "g = graph H' h'"
    and * : "linearform H' h'"  "H' ⊴ E"  "F ⊴ H'"
      "graph F f ⊆ graph H' h'"  "∀x ∈ H'. h' x ≤ p x" ..

  from gc and g have "graph H' h' ∈ c" by (simp only:)
  moreover from gh and g have "(x, h x) ∈ graph H' h'" by (simp only:)
  ultimately show ?thesis using * by blast
qed

text ‹
  ┉
  Let ‹c› be a chain of norm-preserving extensions of the function ‹f› and let
  ‹graph H h› be the supremum of ‹c›. Every element in the domain ‹H› of the
  supremum function is member of the domain ‹H'› of some function ‹h'›, such
  that ‹h› extends ‹h'›.
›

lemma some_H'h':
  assumes M: "M = norm_pres_extensions E p F f"
    and cM: "c ∈ chains M"
    and u: "graph H h = ⋃c"
    and x: "x ∈ H"
  shows "∃H' h'. x ∈ H' ∧ graph H' h' ⊆ graph H h
    ∧ linearform H' h' ∧ H' ⊴ E ∧ F ⊴ H'
    ∧ graph F f ⊆ graph H' h' ∧ (∀x ∈ H'. h' x ≤ p x)"
proof -
  from M cM u x obtain H' h' where
      x_hx: "(x, h x) ∈ graph H' h'"
    and c: "graph H' h' ∈ c"
    and * : "linearform H' h'"  "H' ⊴ E"  "F ⊴ H'"
      "graph F f ⊆ graph H' h'"  "∀x ∈ H'. h' x ≤ p x"
    by (rule some_H'h't [elim_format]) blast
  from x_hx have "x ∈ H'" ..
  moreover from cM u c have "graph H' h' ⊆ graph H h" by blast
  ultimately show ?thesis using * by blast
qed

text ‹
  ┉
  Any two elements ‹x› and ‹y› in the domain ‹H› of the supremum function ‹h›
  are both in the domain ‹H'› of some function ‹h'›, such that ‹h› extends
  ‹h'›.
›

lemma some_H'h'2:
  assumes M: "M = norm_pres_extensions E p F f"
    and cM: "c ∈ chains M"
    and u: "graph H h = ⋃c"
    and x: "x ∈ H"
    and y: "y ∈ H"
  shows "∃H' h'. x ∈ H' ∧ y ∈ H'
    ∧ graph H' h' ⊆ graph H h
    ∧ linearform H' h' ∧ H' ⊴ E ∧ F ⊴ H'
    ∧ graph F f ⊆ graph H' h' ∧ (∀x ∈ H'. h' x ≤ p x)"
proof -
  txt ‹‹y› is in the domain ‹H''› of some function ‹h''›, such that ‹h›
    extends ‹h''›.›

  from M cM u and y obtain H' h' where
      y_hy: "(y, h y) ∈ graph H' h'"
    and c': "graph H' h' ∈ c"
    and * :
      "linearform H' h'"  "H' ⊴ E"  "F ⊴ H'"
      "graph F f ⊆ graph H' h'"  "∀x ∈ H'. h' x ≤ p x"
    by (rule some_H'h't [elim_format]) blast

  txt ‹‹x› is in the domain ‹H'› of some function ‹h'›,
    such that ‹h› extends ‹h'›.›

  from M cM u and x obtain H'' h'' where
      x_hx: "(x, h x) ∈ graph H'' h''"
    and c'': "graph H'' h'' ∈ c"
    and ** :
      "linearform H'' h''"  "H'' ⊴ E"  "F ⊴ H''"
      "graph F f ⊆ graph H'' h''"  "∀x ∈ H''. h'' x ≤ p x"
    by (rule some_H'h't [elim_format]) blast

  txt ‹Since both ‹h'› and ‹h''› are elements of the chain, ‹h''› is an
    extension of ‹h'› or vice versa. Thus both ‹x› and ‹y› are contained in
    the greater one. \label{cases1}›

  from cM c'' c' consider "graph H'' h'' ⊆ graph H' h'" | "graph H' h' ⊆ graph H'' h''"
    by (blast dest: chainsD)
  then show ?thesis
  proof cases
    case 1
    have "(x, h x) ∈ graph H'' h''" by fact
    also have "… ⊆ graph H' h'" by fact
    finally have xh:"(x, h x) ∈ graph H' h'" .
    then have "x ∈ H'" ..
    moreover from y_hy have "y ∈ H'" ..
    moreover from cM u and c' have "graph H' h' ⊆ graph H h" by blast
    ultimately show ?thesis using * by blast
  next
    case 2
    from x_hx have "x ∈ H''" ..
    moreover have "y ∈ H''"
    proof -
      have "(y, h y) ∈ graph H' h'" by (rule y_hy)
      also have "… ⊆ graph H'' h''" by fact
      finally have "(y, h y) ∈ graph H'' h''" .
      then show ?thesis ..
    qed
    moreover from u c'' have "graph H'' h'' ⊆ graph H h" by blast
    ultimately show ?thesis using ** by blast
  qed
qed

text ‹
  ┉
  The relation induced by the graph of the supremum of a chain ‹c› is
  definite, i.e.\ it is the graph of a function.
›

lemma sup_definite:
  assumes M_def: "M = norm_pres_extensions E p F f"
    and cM: "c ∈ chains M"
    and xy: "(x, y) ∈ ⋃c"
    and xz: "(x, z) ∈ ⋃c"
  shows "z = y"
proof -
  from cM have c: "c ⊆ M" ..
  from xy obtain G1 where xy': "(x, y) ∈ G1" and G1: "G1 ∈ c" ..
  from xz obtain G2 where xz': "(x, z) ∈ G2" and G2: "G2 ∈ c" ..

  from G1 c have "G1 ∈ M" ..
  then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
    unfolding M_def by blast

  from G2 c have "G2 ∈ M" ..
  then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
    unfolding M_def by blast

  txt ‹‹G⇩1› is contained in ‹G⇩2› or vice versa, since both ‹G⇩1› and ‹G⇩2›
    are members of ‹c›. \label{cases2}›

  from cM G1 G2 consider "G1 ⊆ G2" | "G2 ⊆ G1"
    by (blast dest: chainsD)
  then show ?thesis
  proof cases
    case 1
    with xy' G2_rep have "(x, y) ∈ graph H2 h2" by blast
    then have "y = h2 x" ..
    also
    from xz' G2_rep have "(x, z) ∈ graph H2 h2" by (simp only:)
    then have "z = h2 x" ..
    finally show ?thesis .
  next
    case 2
    with xz' G1_rep have "(x, z) ∈ graph H1 h1" by blast
    then have "z = h1 x" ..
    also
    from xy' G1_rep have "(x, y) ∈ graph H1 h1" by (simp only:)
    then have "y = h1 x" ..
    finally show ?thesis ..
  qed
qed

text ‹
  ┉
  The limit function ‹h› is linear. Every element ‹x› in the domain of ‹h› is
  in the domain of a function ‹h'› in the chain of norm preserving extensions.
  Furthermore, ‹h› is an extension of ‹h'› so the function values of ‹x› are
  identical for ‹h'› and ‹h›. Finally, the function ‹h'› is linear by
  construction of ‹M›.
›

lemma sup_lf:
  assumes M: "M = norm_pres_extensions E p F f"
    and cM: "c ∈ chains M"
    and u: "graph H h = ⋃c"
  shows "linearform H h"
proof
  fix x y assume x: "x ∈ H" and y: "y ∈ H"
  with M cM u obtain H' h' where
        x': "x ∈ H'" and y': "y ∈ H'"
      and b: "graph H' h' ⊆ graph H h"
      and linearform: "linearform H' h'"
      and subspace: "H' ⊴ E"
    by (rule some_H'h'2 [elim_format]) blast

  show "h (x + y) = h x + h y"
  proof -
    from linearform x' y' have "h' (x + y) = h' x + h' y"
      by (rule linearform.add)
    also from b x' have "h' x = h x" ..
    also from b y' have "h' y = h y" ..
    also from subspace x' y' have "x + y ∈ H'"
      by (rule subspace.add_closed)
    with b have "h' (x + y) = h (x + y)" ..
    finally show ?thesis .
  qed
next
  fix x a assume x: "x ∈ H"
  with M cM u obtain H' h' where
        x': "x ∈ H'"
      and b: "graph H' h' ⊆ graph H h"
      and linearform: "linearform H' h'"
      and subspace: "H' ⊴ E"
    by (rule some_H'h' [elim_format]) blast

  show "h (a ⋅ x) = a * h x"
  proof -
    from linearform x' have "h' (a ⋅ x) = a * h' x"
      by (rule linearform.mult)
    also from b x' have "h' x = h x" ..
    also from subspace x' have "a ⋅ x ∈ H'"
      by (rule subspace.mult_closed)
    with b have "h' (a ⋅ x) = h (a ⋅ x)" ..
    finally show ?thesis .
  qed
qed

text ‹
  ┉
  The limit of a non-empty chain of norm preserving extensions of ‹f› is an
  extension of ‹f›, since every element of the chain is an extension of ‹f›
  and the supremum is an extension for every element of the chain.
›

lemma sup_ext:
  assumes graph: "graph H h = ⋃c"
    and M: "M = norm_pres_extensions E p F f"
    and cM: "c ∈ chains M"
    and ex: "∃x. x ∈ c"
  shows "graph F f ⊆ graph H h"
proof -
  from ex obtain x where xc: "x ∈ c" ..
  from cM have "c ⊆ M" ..
  with xc have "x ∈ M" ..
  with M have "x ∈ norm_pres_extensions E p F f"
    by (simp only:)
  then obtain G g where "x = graph G g" and "graph F f ⊆ graph G g" ..
  then have "graph F f ⊆ x" by (simp only:)
  also from xc have "… ⊆ ⋃c" by blast
  also from graph have "… = graph H h" ..
  finally show ?thesis .
qed

text ‹
  ┉
  The domain ‹H› of the limit function is a superspace of ‹F›, since ‹F› is a
  subset of ‹H›. The existence of the ‹0› element in ‹F› and the closure
  properties follow from the fact that ‹F› is a vector space.
›

lemma sup_supF:
  assumes graph: "graph H h = ⋃c"
    and M: "M = norm_pres_extensions E p F f"
    and cM: "c ∈ chains M"
    and ex: "∃x. x ∈ c"
    and FE: "F ⊴ E"
  shows "F ⊴ H"
proof
  from FE show "F ≠ {}" by (rule subspace.non_empty)
  from graph M cM ex have "graph F f ⊆ graph H h" by (rule sup_ext)
  then show "F ⊆ H" ..
  fix x y assume "x ∈ F" and "y ∈ F"
  with FE show "x + y ∈ F" by (rule subspace.add_closed)
next
  fix x a assume "x ∈ F"
  with FE show "a ⋅ x ∈ F" by (rule subspace.mult_closed)
qed

text ‹
  ┉
  The domain ‹H› of the limit function is a subspace of ‹E›.
›

lemma sup_subE:
  assumes graph: "graph H h = ⋃c"
    and M: "M = norm_pres_extensions E p F f"
    and cM: "c ∈ chains M"
    and ex: "∃x. x ∈ c"
    and FE: "F ⊴ E"
    and E: "vectorspace E"
  shows "H ⊴ E"
proof
  show "H ≠ {}"
  proof -
    from FE E have "0 ∈ F" by (rule subspace.zero)
    also from graph M cM ex FE have "F ⊴ H" by (rule sup_supF)
    then have "F ⊆ H" ..
    finally show ?thesis by blast
  qed
  show "H ⊆ E"
  proof
    fix x assume "x ∈ H"
    with M cM graph
    obtain H' where x: "x ∈ H'" and H'E: "H' ⊴ E"
      by (rule some_H'h' [elim_format]) blast
    from H'E have "H' ⊆ E" ..
    with x show "x ∈ E" ..
  qed
  fix x y assume x: "x ∈ H" and y: "y ∈ H"
  show "x + y ∈ H"
  proof -
    from M cM graph x y obtain H' h' where
          x': "x ∈ H'" and y': "y ∈ H'" and H'E: "H' ⊴ E"
        and graphs: "graph H' h' ⊆ graph H h"
      by (rule some_H'h'2 [elim_format]) blast
    from H'E x' y' have "x + y ∈ H'"
      by (rule subspace.add_closed)
    also from graphs have "H' ⊆ H" ..
    finally show ?thesis .
  qed
next
  fix x a assume x: "x ∈ H"
  show "a ⋅ x ∈ H"
  proof -
    from M cM graph x
    obtain H' h' where x': "x ∈ H'" and H'E: "H' ⊴ E"
        and graphs: "graph H' h' ⊆ graph H h"
      by (rule some_H'h' [elim_format]) blast
    from H'E x' have "a ⋅ x ∈ H'" by (rule subspace.mult_closed)
    also from graphs have "H' ⊆ H" ..
    finally show ?thesis .
  qed
qed

text ‹
  ┉
  The limit function is bounded by the norm ‹p› as well, since all elements in
  the chain are bounded by ‹p›.
›

lemma sup_norm_pres:
  assumes graph: "graph H h = ⋃c"
    and M: "M = norm_pres_extensions E p F f"
    and cM: "c ∈ chains M"
  shows "∀x ∈ H. h x ≤ p x"
proof
  fix x assume "x ∈ H"
  with M cM graph obtain H' h' where x': "x ∈ H'"
      and graphs: "graph H' h' ⊆ graph H h"
      and a: "∀x ∈ H'. h' x ≤ p x"
    by (rule some_H'h' [elim_format]) blast
  from graphs x' have [symmetric]: "h' x = h x" ..
  also from a x' have "h' x ≤ p x " ..
  finally show "h x ≤ p x" .
qed

text ‹
  ┉
  The following lemma is a property of linear forms on real vector spaces. It
  will be used for the lemma ‹abs_Hahn_Banach› (see page
  \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces the
  following inequality are equivalent:
  \begin{center}
  \begin{tabular}{lll}
  ‹∀x ∈ H. ¦h x¦ ≤ p x› & and &
  ‹∀x ∈ H. h x ≤ p x› \\
  \end{tabular}
  \end{center}
›

lemma abs_ineq_iff:
  assumes "subspace H E" and "vectorspace E" and "seminorm E p"
    and "linearform H h"
  shows "(∀x ∈ H. ¦h x¦ ≤ p x) = (∀x ∈ H. h x ≤ p x)" (is "?L = ?R")
proof
  interpret subspace H E by fact
  interpret vectorspace E by fact
  interpret seminorm E p by fact
  interpret linearform H h by fact
  have H: "vectorspace H" using ‹vectorspace E› ..
  {
    assume l: ?L
    show ?R
    proof
      fix x assume x: "x ∈ H"
      have "h x ≤ ¦h x¦" by arith
      also from l x have "… ≤ p x" ..
      finally show "h x ≤ p x" .
    qed
  next
    assume r: ?R
    show ?L
    proof
      fix x assume x: "x ∈ H"
      show "¦b¦ ≤ a" when "- a ≤ b" "b ≤ a" for a b :: real
        using that by arith
      from ‹linearform H h› and H x
      have "- h x = h (- x)" by (rule linearform.neg [symmetric])
      also
      from H x have "- x ∈ H" by (rule vectorspace.neg_closed)
      with r have "h (- x) ≤ p (- x)" ..
      also have "… = p x"
        using ‹seminorm E p› ‹vectorspace E›
      proof (rule seminorm.minus)
        from x show "x ∈ E" ..
      qed
      finally have "- h x ≤ p x" .
      then show "- p x ≤ h x" by simp
      from r x show "h x ≤ p x" ..
    qed
  }
qed

end