# Theory HahnBanachExtLemmas

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

theory HahnBanachExtLemmas
imports FunctionNorm
begin

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

    header {* Extending non-maximal functions *}

    theory HahnBanachExtLemmas imports FunctionNorm begin

    text {*
      In this section the following context is presumed.  Let @{text E} be
      a real vector space with a seminorm @{text q} on @{text E}. @{text
      F} is a subspace of @{text E} and @{text f} a linear function on
      @{text F}. We consider a subspace @{text H} of @{text E} that is a
      superspace of @{text F} and a linear form @{text h} on @{text
      H}. @{text H} is a not equal to @{text E} and @{text "x0"} is
      an element in @{text "E - H"}.  @{text H} is extended to the direct
      sum @{text "H' = H + lin x0"}, so for any @{text "x ∈ H'"}
      the decomposition of @{text "x = y + a · x"} with @{text "y ∈ H"} is
      unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +
      a · ξ"} for a certain @{text ξ}.

      Subsequently we show some properties of this extension @{text h'} of
      @{text h}.

      \medskip This lemma will be used to show the existence of a linear
      extension of @{text f} (see page \pageref{ex-xi-use}). It is a
      consequence of the completeness of @{text \<real>}. To show
      \begin{center}
      \begin{tabular}{l}
      @{text "∃ξ. ∀y ∈ F. a y ≤ ξ ∧ ξ ≤ b y"}
      \end{tabular}
      \end{center}
      \noindent it suffices to show that
      \begin{center}
      \begin{tabular}{l}
      @{text "∀u ∈ F. ∀v ∈ F. a u ≤ b v"}
      \end{tabular}
      \end{center}
    *}

    lemma ex_xi:
      includes vectorspace F
      assumes r: "!!u v. u ∈ F ==> v ∈ F ==> a u ≤ b v"
      shows "∃xi::real. ∀y ∈ F. a y ≤ xi ∧ xi ≤ b y"
    proof -
      txt {* From the completeness of the reals follows:
        The set @{text "S = {a u. u ∈ F}"} has a supremum, if it is
        non-empty and has an upper bound. *}

      let ?S = "{a u | u. u ∈ F}"
      have "∃xi. lub ?S xi"
      proof (rule real_complete)
        have "a 0 ∈ ?S" by blast
        then show "∃X. X ∈ ?S" ..
        have "∀y ∈ ?S. y ≤ b 0"
        proof
          fix y assume y: "y ∈ ?S"
          then obtain u where u: "u ∈ F" and y: "y = a u" by blast
          from u and zero have "a u ≤ b 0" by (rule r)
          with y show "y ≤ b 0" by (simp only:)
        qed
        then show "∃u. ∀y ∈ ?S. y ≤ u" ..
      qed
      then obtain xi where xi: "lub ?S xi" ..
      {
        fix y assume "y ∈ F"
        then have "a y ∈ ?S" by blast
        with xi have "a y ≤ xi" by (rule lub.upper)
      } moreover {
        fix y assume y: "y ∈ F"
        from xi have "xi ≤ b y"
        proof (rule lub.least)
          fix au assume "au ∈ ?S"
          then obtain u where u: "u ∈ F" and au: "au = a u" by blast
          from u y have "a u ≤ b y" by (rule r)
          with au show "au ≤ b y" by (simp only:)
        qed
      } ultimately show "∃xi. ∀y ∈ F. a y ≤ xi ∧ xi ≤ b y" by blast
    qed

    text {*
      \medskip The function @{text h'} is defined as a @{text "h' x = h y
      + a · ξ"} where @{text "x = y + a · ξ"} is a linear extension of
      @{text h} to @{text H'}.
    *}

    lemma h'_lf:
      includes var H + var h + var E
      assumes h'_def: "h' ≡ λx. let (y, a) =
          SOME (y, a). x = y + a · x0 ∧ y ∈ H in h y + a * xi"
        and H'_def: "H' ≡ H + lin x0"
        and HE: "H \<unlhd> E"
      includes linearform H h
      assumes x0: "x0 ∉ H"  "x0 ∈ E"  "x0 ≠ 0"
      includes vectorspace E
      shows "linearform H' h'"
    proof
      have H': "vectorspace H'"
      proof (unfold H'_def)
        have "x0 ∈ E" .
        then have "lin x0 \<unlhd> E" ..
        with HE show "vectorspace (H + lin x0)" ..
      qed
      {
        fix x1 x2 assume x1: "x1 ∈ H'" and x2: "x2 ∈ H'"
        show "h' (x1 + x2) = h' x1 + h' x2"
        proof -
          from H' x1 x2 have "x1 + x2 ∈ H'"
            by (rule vectorspace.add_closed)
          with x1 x2 obtain y y1 y2 a a1 a2 where
                x1x2: "x1 + x2 = y + a · x0" and y: "y ∈ H"
              and x1_rep: "x1 = y1 + a1 · x0" and y1: "y1 ∈ H"
              and x2_rep: "x2 = y2 + a2 · x0" and y2: "y2 ∈ H"
            by (unfold H'_def sum_def lin_def) blast

          have ya: "y1 + y2 = y ∧ a1 + a2 = a" using _ HE _ y x0
          proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
            from HE y1 y2 show "y1 + y2 ∈ H"
              by (rule subspace.add_closed)
            from x0 and HE y y1 y2
            have "x0 ∈ E"  "y ∈ E"  "y1 ∈ E"  "y2 ∈ E" by auto
            with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) · x0 = x1 + x2"
              by (simp add: add_ac add_mult_distrib2)
            also note x1x2
            finally show "(y1 + y2) + (a1 + a2) · x0 = y + a · x0" .
          qed

          from h'_def x1x2 _ HE y x0
          have "h' (x1 + x2) = h y + a * xi"
            by (rule h'_definite)
          also have "… = h (y1 + y2) + (a1 + a2) * xi"
            by (simp only: ya)
          also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
            by simp
          also have "… + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
            by (simp add: left_distrib)
          also from h'_def x1_rep _ HE y1 x0
          have "h y1 + a1 * xi = h' x1"
            by (rule h'_definite [symmetric])
          also from h'_def x2_rep _ HE y2 x0
          have "h y2 + a2 * xi = h' x2"
            by (rule h'_definite [symmetric])
          finally show ?thesis .
        qed
      next
        fix x1 c assume x1: "x1 ∈ H'"
        show "h' (c · x1) = c * (h' x1)"
        proof -
          from H' x1 have ax1: "c · x1 ∈ H'"
            by (rule vectorspace.mult_closed)
          with x1 obtain y a y1 a1 where
                cx1_rep: "c · x1 = y + a · x0" and y: "y ∈ H"
              and x1_rep: "x1 = y1 + a1 · x0" and y1: "y1 ∈ H"
            by (unfold H'_def sum_def lin_def) blast

          have ya: "c · y1 = y ∧ c * a1 = a" using _ HE _ y x0
          proof (rule decomp_H')
            from HE y1 show "c · y1 ∈ H"
              by (rule subspace.mult_closed)
            from x0 and HE y y1
            have "x0 ∈ E"  "y ∈ E"  "y1 ∈ E" by auto
            with x1_rep have "c · y1 + (c * a1) · x0 = c · x1"
              by (simp add: mult_assoc add_mult_distrib1)
            also note cx1_rep
            finally show "c · y1 + (c * a1) · x0 = y + a · x0" .
          qed

          from h'_def cx1_rep _ HE y x0 have "h' (c · x1) = h y + a * xi"
            by (rule h'_definite)
          also have "… = h (c · y1) + (c * a1) * xi"
            by (simp only: ya)
          also from y1 have "h (c · y1) = c * h y1"
            by simp
          also have "… + (c * a1) * xi = c * (h y1 + a1 * xi)"
            by (simp only: right_distrib)
          also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1"
            by (rule h'_definite [symmetric])
          finally show ?thesis .
        qed
      }
    qed

    text {* \medskip The linear extension @{text h'} of @{text h}
      is bounded by the seminorm @{text p}. *}

    lemma h'_norm_pres:
      includes var H + var h + var E
      assumes h'_def: "h' ≡ λx. let (y, a) =
          SOME (y, a). x = y + a · x0 ∧ y ∈ H in h y + a * xi"
        and H'_def: "H' ≡ H + lin x0"
        and x0: "x0 ∉ H"  "x0 ∈ E"  "x0 ≠ 0"
      includes vectorspace E + subspace H E + seminorm E p + linearform H h
      assumes a: "∀y ∈ H. h y ≤ p y"
        and a': "∀y ∈ H. - p (y + x0) - h y ≤ xi ∧ xi ≤ p (y + x0) - h y"
      shows "∀x ∈ H'. h' x ≤ p x"
    proof
      fix x assume x': "x ∈ H'"
      show "h' x ≤ p x"
      proof -
        from a' have a1: "∀ya ∈ H. - p (ya + x0) - h ya ≤ xi"
          and a2: "∀ya ∈ H. xi ≤ p (ya + x0) - h ya" by auto
        from x' obtain y a where
            x_rep: "x = y + a · x0" and y: "y ∈ H"
          by (unfold H'_def sum_def lin_def) blast
        from y have y': "y ∈ E" ..
        from y have ay: "inverse a · y ∈ H" by simp

        from h'_def x_rep _ _ y x0 have "h' x = h y + a * xi"
          by (rule h'_definite)
        also have "… ≤ p (y + a · x0)"
        proof (rule linorder_cases)
          assume z: "a = 0"
          then have "h y + a * xi = h y" by simp
          also from a y have "… ≤ p y" ..
          also from x0 y' z have "p y = p (y + a · x0)" by simp
          finally show ?thesis .
        next
          txt {* In the case @{text "a < 0"}, we use @{text "a1"}
            with @{text ya} taken as @{text "y / a"}: *}
          assume lz: "a < 0" hence nz: "a ≠ 0" by simp
          from a1 ay
          have "- p (inverse a · y + x0) - h (inverse a · y) ≤ xi" ..
          with lz have "a * xi ≤
              a * (- p (inverse a · y + x0) - h (inverse a · y))"
            by (simp add: mult_left_mono_neg order_less_imp_le)

          also have "… =
              - a * (p (inverse a · y + x0)) - a * (h (inverse a · y))"
            by (simp add: right_diff_distrib)
          also from lz x0 y' have "- a * (p (inverse a · y + x0)) =
              p (a · (inverse a · y + x0))"
            by (simp add: abs_homogenous)
          also from nz x0 y' have "… = p (y + a · x0)"
            by (simp add: add_mult_distrib1 mult_assoc [symmetric])
          also from nz y have "a * (h (inverse a · y)) =  h y"
            by simp
          finally have "a * xi ≤ p (y + a · x0) - h y" .
          then show ?thesis by simp
        next
          txt {* In the case @{text "a > 0"}, we use @{text "a2"}
            with @{text ya} taken as @{text "y / a"}: *}
          assume gz: "0 < a" hence nz: "a ≠ 0" by simp
          from a2 ay
          have "xi ≤ p (inverse a · y + x0) - h (inverse a · y)" ..
          with gz have "a * xi ≤
              a * (p (inverse a · y + x0) - h (inverse a · y))"
            by simp
          also have "... = a * p (inverse a · y + x0) - a * h (inverse a · y)"
            by (simp add: right_diff_distrib)
          also from gz x0 y'
          have "a * p (inverse a · y + x0) = p (a · (inverse a · y + x0))"
            by (simp add: abs_homogenous)
          also from nz x0 y' have "… = p (y + a · x0)"
            by (simp add: add_mult_distrib1 mult_assoc [symmetric])
          also from nz y have "a * h (inverse a · y) = h y"
            by simp
          finally have "a * xi ≤ p (y + a · x0) - h y" .
          then show ?thesis by simp
        qed
        also from x_rep have "… = p x" by (simp only:)
        finally show ?thesis .
      qed
    qed

    end

lemma ex_xi:

      [| vectorspace F; !!u v. [| u ∈ F; v ∈ F |] ==> a u ≤ b v |]
      ==> ∃xi. ∀y∈F. a y ≤ xi ∧ xi ≤ b y

lemma h'_lf:

      [| h' == %x. let (y, a) = SOME (y, a). x = y + a · x0.0 ∧ y ∈ H in h y + a * xi;
         H' == H + lin x0.0; subspace H E; linearform H h; x0.0 ∉ H; x0.0 ∈ E;
         x0.0 ≠ (0::'a); vectorspace E |]
      ==> linearform H' h'

lemma h'_norm_pres:

      [| h' == %x. let (y, a) = SOME (y, a). x = y + a · x0.0 ∧ y ∈ H in h y + a * xi;
         H' == H + lin x0.0; x0.0 ∉ H; x0.0 ∈ E; x0.0 ≠ (0::'a); vectorspace E;
         subspace H E; seminorm E p; linearform H h; ∀y∈H. h y ≤ p y;
         ∀y∈H. - p (y + x0.0) - h y ≤ xi ∧ xi ≤ p (y + x0.0) - h y |]
      ==> ∀x∈H'. h' x ≤ p x