# Theory HahnBanachSupLemmas

Up to index of Isabelle/HOL/HOL-Complex/HahnBanach

theory HahnBanachSupLemmas
imports FunctionNorm ZornLemma
begin

    (*  Title:      HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
        ID:         $Id: HahnBanachSupLemmas.thy,v 1.21 2005/06/17 14:13:09 haftmann Exp $
        Author:     Gertrud Bauer, TU Munich
    *)

    header {* The supremum w.r.t.~the function order *}

    theory HahnBanachSupLemmas imports FunctionNorm ZornLemma 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 @{text E} be a real vector space with a seminorm
      @{text p} on @{text E}.  @{text F} is a subspace of @{text E} and
      @{text f} a linear form on @{text F}. We consider a chain @{text c}
      of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =
      graph H h"}.  We will show some properties about the limit function
      @{text h}, i.e.\ the supremum of the chain @{text c}.

      \medskip Let @{text c} be a chain of norm-preserving extensions of
      the function @{text f} and let @{text "graph H h"} be the supremum
      of @{text c}.  Every element in @{text H} is member of one of the
      elements of the chain.
    *}
    lemmas [dest?] = chainD
    lemmas chainE2 [elim?] = chainD2 [elim_format, standard]

    lemma some_H'h't:
      assumes M: "M = norm_pres_extensions E p F f"
        and cM: "c ∈ chain M"
        and u: "graph H h = \<Union>c"
        and x: "x ∈ H"
      shows "∃H' h'. graph H' h' ∈ c
        ∧ (x, h x) ∈ graph H' h'
        ∧ linearform H' h' ∧ H' \<unlhd> E
        ∧ F \<unlhd> 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 "… = \<Union>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' \<unlhd> E"  "F \<unlhd> 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 {*
      \medskip Let @{text c} be a chain of norm-preserving extensions of
      the function @{text f} and let @{text "graph H h"} be the supremum
      of @{text c}.  Every element in the domain @{text H} of the supremum
      function is member of the domain @{text H'} of some function @{text
      h'}, such that @{text h} extends @{text h'}.
    *}

    lemma some_H'h':
      assumes M: "M = norm_pres_extensions E p F f"
        and cM: "c ∈ chain M"
        and u: "graph H h = \<Union>c"
        and x: "x ∈ H"
      shows "∃H' h'. x ∈ H' ∧ graph H' h' ⊆ graph H h
        ∧ linearform H' h' ∧ H' \<unlhd> E ∧ F \<unlhd> 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' \<unlhd> E"  "F \<unlhd> 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 (simp only: chain_ball_Union_upper)
      ultimately show ?thesis using * by blast
    qed

    text {*
      \medskip Any two elements @{text x} and @{text y} in the domain
      @{text H} of the supremum function @{text h} are both in the domain
      @{text H'} of some function @{text h'}, such that @{text h} extends
      @{text h'}.
    *}

    lemma some_H'h'2:
      assumes M: "M = norm_pres_extensions E p F f"
        and cM: "c ∈ chain M"
        and u: "graph H h = \<Union>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' \<unlhd> E ∧ F \<unlhd> H'
        ∧ graph F f ⊆ graph H' h' ∧ (∀x ∈ H'. h' x ≤ p x)"
    proof -
      txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
      such that @{text h} extends @{text 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' \<unlhd> E"  "F \<unlhd> H'"
          "graph F f ⊆ graph H' h'"  "∀x ∈ H'. h' x ≤ p x"
        by (rule some_H'h't [elim_format]) blast

      txt {* @{text x} is in the domain @{text H'} of some function @{text h'},
        such that @{text h} extends @{text 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'' \<unlhd> E"  "F \<unlhd> 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 @{text h'} and @{text h''} are elements of the chain,
        @{text h''} is an extension of @{text h'} or vice versa. Thus both
        @{text x} and @{text y} are contained in the greater
        one. \label{cases1}*}

      from cM have "graph H'' h'' ⊆ graph H' h' ∨ graph H' h' ⊆ graph H'' h''"
        (is "?case1 ∨ ?case2") ..
      then show ?thesis
      proof
        assume ?case1
        have "(x, h x) ∈ graph H'' h''" .
        also have "... ⊆ graph H' h'" .
        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 (simp only: chain_ball_Union_upper)
        ultimately show ?thesis using * by blast
      next
        assume ?case2
        from x_hx have "x ∈ H''" ..
        moreover {
          from y_hy have "(y, h y) ∈ graph H' h'" .
          also have "… ⊆ graph H'' h''" .
          finally have "(y, h y) ∈ graph H'' h''" .
        } then have "y ∈ H''" ..
        moreover from cM u and c'' have "graph H'' h'' ⊆ graph H h"
          by (simp only: chain_ball_Union_upper)
        ultimately show ?thesis using ** by blast
      qed
    qed

    text {*
      \medskip The relation induced by the graph of the supremum of a
      chain @{text c} is definite, i.~e.~t is the graph of a function.
    *}

    lemma sup_definite:
      assumes M_def: "M ≡ norm_pres_extensions E p F f"
        and cM: "c ∈ chain M"
        and xy: "(x, y) ∈ \<Union>c"
        and xz: "(x, z) ∈ \<Union>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"
        by (unfold M_def) blast

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

      txt {* @{text "G1"} is contained in @{text "G2"}
        or vice versa, since both @{text "G1"} and @{text
        "G2"} are members of @{text c}. \label{cases2}*}

      from cM G1 G2 have "G1 ⊆ G2 ∨ G2 ⊆ G1" (is "?case1 ∨ ?case2") ..
      then show ?thesis
      proof
        assume ?case1
        with xy' G2_rep have "(x, y) ∈ graph H2 h2" by blast
        hence "y = h2 x" ..
        also
        from xz' G2_rep have "(x, z) ∈ graph H2 h2" by (simp only:)
        hence "z = h2 x" ..
        finally show ?thesis .
      next
        assume ?case2
        with xz' G1_rep have "(x, z) ∈ graph H1 h1" by blast
        hence "z = h1 x" ..
        also
        from xy' G1_rep have "(x, y) ∈ graph H1 h1" by (simp only:)
        hence "y = h1 x" ..
        finally show ?thesis ..
      qed
    qed

    text {*
      \medskip The limit function @{text h} is linear. Every element
      @{text x} in the domain of @{text h} is in the domain of a function
      @{text h'} in the chain of norm preserving extensions.  Furthermore,
      @{text h} is an extension of @{text h'} so the function values of
      @{text x} are identical for @{text h'} and @{text h}.  Finally, the
      function @{text h'} is linear by construction of @{text M}.
    *}

    lemma sup_lf:
      assumes M: "M = norm_pres_extensions E p F f"
        and cM: "c ∈ chain M"
        and u: "graph H h = \<Union>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' \<unlhd> 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' \<unlhd> 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 {*
      \medskip The limit of a non-empty chain of norm preserving
      extensions of @{text f} is an extension of @{text f}, since every
      element of the chain is an extension of @{text f} and the supremum
      is an extension for every element of the chain.
    *}

    lemma sup_ext:
      assumes graph: "graph H h = \<Union>c"
        and M: "M = norm_pres_extensions E p F f"
        and cM: "c ∈ chain 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 "… ⊆ \<Union>c" by blast
      also from graph have "… = graph H h" ..
      finally show ?thesis .
    qed

    text {*
      \medskip The domain @{text H} of the limit function is a superspace
      of @{text F}, since @{text F} is a subset of @{text H}. The
      existence of the @{text 0} element in @{text F} and the closure
      properties follow from the fact that @{text F} is a vector space.
    *}

    lemma sup_supF:
      assumes graph: "graph H h = \<Union>c"
        and M: "M = norm_pres_extensions E p F f"
        and cM: "c ∈ chain M"
        and ex: "∃x. x ∈ c"
        and FE: "F \<unlhd> E"
      shows "F \<unlhd> 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 {*
      \medskip The domain @{text H} of the limit function is a subspace of
      @{text E}.
    *}

    lemma sup_subE:
      assumes graph: "graph H h = \<Union>c"
        and M: "M = norm_pres_extensions E p F f"
        and cM: "c ∈ chain M"
        and ex: "∃x. x ∈ c"
        and FE: "F \<unlhd> E"
        and E: "vectorspace E"
      shows "H \<unlhd> E"
    proof
      show "H ≠ {}"
      proof -
        from FE E have "0 ∈ F" by (rule subspace.zero)
        also from graph M cM ex FE have "F \<unlhd> 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' h' where x: "x ∈ H'" and H'E: "H' \<unlhd> 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' \<unlhd> 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' \<unlhd> 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 {*
      \medskip The limit function is bounded by the norm @{text p} as
      well, since all elements in the chain are bounded by @{text p}.
    *}

    lemma sup_norm_pres:
      assumes graph: "graph H h = \<Union>c"
        and M: "M = norm_pres_extensions E p F f"
        and cM: "c ∈ chain 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 {*
      \medskip The following lemma is a property of linear forms on real
      vector spaces. It will be used for the lemma @{text abs_HahnBanach}
      (see page \pageref{abs-HahnBanach}). \label{abs-ineq-iff} For real
      vector spaces the following inequations are equivalent:
      \begin{center}
      \begin{tabular}{lll}
      @{text "∀x ∈ H. ¦h x¦ ≤ p x"} & and &
      @{text "∀x ∈ H. h x ≤ p x"} \\
      \end{tabular}
      \end{center}
    *}

    lemma abs_ineq_iff:
      includes subspace H E + vectorspace E + seminorm E p + linearform H h
      shows "(∀x ∈ H. ¦h x¦ ≤ p x) = (∀x ∈ H. h x ≤ p x)" (is "?L = ?R")
    proof
      have H: "vectorspace H" ..
      {
        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 "!!a b :: real. - a ≤ b ==> b ≤ a ==> ¦b¦ ≤ a"
            by arith
          have "linearform H h" .
          from this 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"
          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

lemmas

      [| c ∈ chain S; x ∈ c; y ∈ c |] ==> x ⊆ y ∨ y ⊆ x

lemmas

      [| c ∈ chain S; x ∈ c; y ∈ c |] ==> x ⊆ y ∨ y ⊆ x

lemmas chainE2:

      [| c ∈ chain S; c ⊆ S ==> PROP W |] ==> PROP W

lemmas chainE2:

      [| c ∈ chain S; c ⊆ S ==> PROP W |] ==> PROP W

lemma some_H'h't:

      [| M = norm_pres_extensions E p F f; c ∈ chain M; graph H h = Union c; x ∈ H |]
      ==> ∃H' h'.
             graph H' h' ∈ c ∧
             (x, h x) ∈ graph H' h' ∧
             linearform H' h' ∧
             subspace H' E ∧
             subspace F H' ∧ graph F f ⊆ graph H' h' ∧ (∀x∈H'. h' x ≤ p x)

lemma some_H'h':

      [| M = norm_pres_extensions E p F f; c ∈ chain M; graph H h = Union c; x ∈ H |]
      ==> ∃H' h'.
             x ∈ H' ∧
             graph H' h' ⊆ graph H h ∧
             linearform H' h' ∧
             subspace H' E ∧
             subspace F H' ∧ graph F f ⊆ graph H' h' ∧ (∀x∈H'. h' x ≤ p x)

lemma some_H'h'2:

      [| M = norm_pres_extensions E p F f; c ∈ chain M; graph H h = Union c; x ∈ H;
         y ∈ H |]
      ==> ∃H' h'.
             x ∈ H' ∧
             y ∈ H' ∧
             graph H' h' ⊆ graph H h ∧
             linearform H' h' ∧
             subspace H' E ∧
             subspace F H' ∧ graph F f ⊆ graph H' h' ∧ (∀x∈H'. h' x ≤ p x)

lemma sup_definite:

      [| M == norm_pres_extensions E p F f; c ∈ chain M; (x, y) ∈ Union c;
         (x, z) ∈ Union c |]
      ==> z = y

lemma sup_lf:

      [| M = norm_pres_extensions E p F f; c ∈ chain M; graph H h = Union c |]
      ==> linearform H h

lemma sup_ext:

      [| graph H h = Union c; M = norm_pres_extensions E p F f; c ∈ chain M;
         ∃x. x ∈ c |]
      ==> graph F f ⊆ graph H h

lemma sup_supF:

      [| graph H h = Union c; M = norm_pres_extensions E p F f; c ∈ chain M;
         ∃x. x ∈ c; subspace F E |]
      ==> subspace F H

lemma sup_subE:

      [| graph H h = Union c; M = norm_pres_extensions E p F f; c ∈ chain M;
         ∃x. x ∈ c; subspace F E; vectorspace E |]
      ==> subspace H E

lemma sup_norm_pres:

      [| graph H h = Union c; M = norm_pres_extensions E p F f; c ∈ chain M |]
      ==> ∀x∈H. h x ≤ p x

lemma abs_ineq_iff:

      [| subspace H E; vectorspace E; seminorm E p; linearform H h |]
      ==> (∀x∈H. ¦h x¦ ≤ p x) = (∀x∈H. h x ≤ p x)