Quellcode-Bibliothek Hahn_Banach.thy Interaktion und
PortierbarkeitIsabelle

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

section \<open>The Hahn-Banach Theorem\<close>

theory Hahn_Banach
imports Hahn_Banach_Lemmas
begin

text \<open>
  We present the proof of two different versions of the Hahn-Banach Theorem,
  closely following \<^cite>\<open>\<open>\S36\<close> in "Heuser:1986"\<close>.
\<close>

subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>

paragraph \<open>Hahn-Banach Theorem.\<close>
text \<open>
  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm on
  \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded by
  \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear form \<open>h\<close>
  on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded by \<open>p\<close>.
\<close>

paragraph \<open>Proof Sketch.\<close>
text \<open>
  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces of
  \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.

  \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>.

  \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in \<open>M\<close>.

  \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical
  contradiction:

    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in a
    norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.

    \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
\<close>

theorem Hahn_Banach:
  assumes E: "vectorspace E" and "subspace F E"
    and "seminorm E p" and "linearform F f"
  assumes fp: "\x \ F. f x \ p x"
  shows "\h. linearform E h \ (\x \ F. h x = f x) \ (\x \ E. h x \ p x)"
    \<comment> \<open>Let \<open>E\<close> be a vector space, \<open>F\<close> a subspace of \<open>E\<close>, \<open>p\<close> a seminorm on \<open>E\<close>,\<close>
    \<comment> \<open>and \<open>f\<close> a linear form on \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>,\<close>
    \<comment> \<open>then \<open>f\<close> can be extended to a linear form \<open>h\<close> on \<open>E\<close> in a norm-preserving way. \<^smallskip>\<close>
proof -
  interpret vectorspace E by fact
  interpret subspace F E by fact
  interpret seminorm E p by fact
  interpret linearform F f by fact
  define M where "M = norm_pres_extensions E p F f"
  then have M: "M = \" by (simp only:)
  from E have F: "vectorspace F" ..
  note FE = \<open>F \<unlhd> E\<close>
  have "\c \ M" if cM: "c \ chains M" and ex: "\x. x \ c" for c
    \<comment> \<open>Show that every non-empty chain \<open>c\<close> of \<open>M\<close> has an upper bound in \<open>M\<close>:\<close>
    \<comment> \<open>\<open>\<Union>c\<close> is greater than any element of the chain \<open>c\<close>, so it suffices to show \<open>\<Union>c \<in> M\<close>.\<close>
    unfolding M_def
  proof (rule norm_pres_extensionI)
    let ?H = "domain (\c)"
    let ?h = "funct (\c)"

    have a: "graph ?H ?h = \c"
    proof (rule graph_domain_funct)
      fix x y z assume "(x, y) \ \c" and "(x, z) \ \c"
      with M_def cM show "z = y" by (rule sup_definite)
    qed
    moreover from M cM a have "linearform ?H ?h"
      by (rule sup_lf)
    moreover from a M cM ex FE E have "?H \ E"
      by (rule sup_subE)
    moreover from a M cM ex FE have "F \ ?H"
      by (rule sup_supF)
    moreover from a M cM ex have "graph F f \ graph ?H ?h"
      by (rule sup_ext)
    moreover from a M cM have "\x \ ?H. ?h x \ p x"
      by (rule sup_norm_pres)
    ultimately show "\H h. \c = graph H h
        \<and> linearform H h
        \<and> H \<unlhd> E
        \<and> F \<unlhd> H
        \<and> graph F f \<subseteq> graph H h
        \<and> (\<forall>x \<in> H. h x \<le> p x)" by blast
  qed
  then have "\g \ M. \x \ M. g \ x \ x = g"
  \<comment> \<open>With Zorn's Lemma we can conclude that there is a maximal element in \<open>M\<close>. \<^smallskip>\<close>
  proof (rule Zorn's_Lemma)
      \<comment> \<open>We show that \<open>M\<close> is non-empty:\<close>
    show "graph F f \ M"
      unfolding M_def
    proof (rule norm_pres_extensionI2)
      show "linearform F f" by fact
      show "F \ E" by fact
      from F show "F \ F" by (rule vectorspace.subspace_refl)
      show "graph F f \ graph F f" ..
      show "\x\F. f x \ p x" by fact
    qed
  qed
  then obtain g where gM: "g \ M" and gx: "\x \ M. g \ x \ g = x"
    by blast
  from gM obtain H h where
      g_rep: "g = graph H h"
    and linearform: "linearform H h"
    and HE: "H \ E" and FH: "F \ H"
    and graphs: "graph F f \ graph H h"
    and hp: "\x \ H. h x \ p x" unfolding M_def ..
      \<comment> \<open>\<open>g\<close> is a norm-preserving extension of \<open>f\<close>, in other words:\<close>
      \<comment> \<open>\<open>g\<close> is the graph of some linear form \<open>h\<close> defined on a subspace \<open>H\<close> of \<open>E\<close>,\<close>
      \<comment> \<open>and \<open>h\<close> is an extension of \<open>f\<close> that is again bounded by \<open>p\<close>. \<^smallskip>\<close>
  from HE E have H: "vectorspace H"
    by (rule subspace.vectorspace)

  have HE_eq: "H = E"
    \<comment> \<open>We show that \<open>h\<close> is defined on whole \<open>E\<close> by classical contradiction. \<^smallskip>\<close>
  proof (rule classical)
    assume neq: "H \ E"
      \<comment> \<open>Assume \<open>h\<close> is not defined on whole \<open>E\<close>. Then show that \<open>h\<close> can be extended\<close>
      \<comment> \<open>in a norm-preserving way to a function \<open>h'\<close> with the graph \<open>g'\<close>. \<^smallskip>\<close>
    have "\g' \ M. g \ g' \ g \ g'"
    proof -
      from HE have "H \ E" ..
      with neq obtain x' where x'E: "x' \ E" and "x' \ H" by blast
      obtain x': "x' \<noteq> 0"
      proof
        show "x' \ 0"
        proof
          assume "x' = 0"
          with H have "x' \ H" by (simp only: vectorspace.zero)
          with \<open>x' \<notin> H\<close> show False by contradiction
        qed
      qed

      define H' where "H' = H + lin x'"
        \<comment> \<open>Define \<open>H'\<close> as the direct sum of \<open>H\<close> and the linear closure of \<open>x'\<close>. \<^smallskip>\<close>
      have HH': "H \ H'"
      proof (unfold H'_def)
        from x'E have "vectorspace (lin x')" ..
        with H show "H \ H + lin x'" ..
      qed

      obtain xi where
        xi: "\y \ H. - p (y + x') - h y \ xi
          \<and> xi \<le> p (y + x') - h y"
        \<comment> \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close>
        \<comment> \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>.
           \label{ex-xi-use}\<^smallskip>\<close>
      proof -
        from H have "\xi. \y \ H. - p (y + x') - h y \ xi
            \<and> xi \<le> p (y + x') - h y"
        proof (rule ex_xi)
          fix u v assume u: "u \ H" and v: "v \ H"
          with HE have uE: "u \ E" and vE: "v \ E" by auto
          from H u v linearform have "h v - h u = h (v - u)"
            by (simp add: linearform.diff)
          also from hp and H u v have "\ \ p (v - u)"
            by (simp only: vectorspace.diff_closed)
          also from x'E uE vE have "v - u = x' + - x' + v + - u"
            by (simp add: diff_eq1)
          also from x'E uE vE have "\ = v + x' + - (u + x')"
            by (simp add: add_ac)
          also from x'E uE vE have "\ = (v + x') - (u + x')"
            by (simp add: diff_eq1)
          also from x'E uE vE E have "p \ \ p (v + x') + p (u + x')"
            by (simp add: diff_subadditive)
          finally have "h v - h u \ p (v + x') + p (u + x')" .
          then show "- p (u + x') - h u \ p (v + x') - h v" by simp
        qed
        then show thesis by (blast intro: that)
      qed

      define h' where "h' x = (let (y, a) =
          SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi)" for x
        \<comment> \<open>Define the extension \<open>h'\<close> of \<open>h\<close> to \<open>H'\<close> using \<open>\<xi>\<close>. \<^smallskip>\<close>

      have "g \ graph H' h' \ g \ graph H' h'"
        \<comment> \<open>\<open>h'\<close> is an extension of \<open>h\<close> \dots \<^smallskip>\<close>
      proof
        show "g \ graph H' h'"
        proof -
          have "graph H h \ graph H' h'"
          proof (rule graph_extI)
            fix t assume t: "t \ H"
            from E HE t have "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)"
              using \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> by (rule decomp_H'_H)
            with h'_def show "h t = h' t" by (simp add: Let_def)
          next
            from HH' show "H \ H'" ..
          qed
          with g_rep show ?thesis by (simp only:)
        qed

        show "g \ graph H' h'"
        proof -
          have "graph H h \ graph H' h'"
          proof
            assume eq: "graph H h = graph H' h'"
            have "x' \ H'"
              unfolding H'_def
            proof
              from H show "0 \ H" by (rule vectorspace.zero)
              from x'E show "x' \<in> lin x'" by (rule x_lin_x)
              from x'E show "x' = 0 + x'" by simp
            qed
            then have "(x', h' x') \ graph H' h'" ..
            with eq have "(x', h' x') \ graph H h" by (simp only:)
            then have "x' \ H" ..
            with \<open>x' \<notin> H\<close> show False by contradiction
          qed
          with g_rep show ?thesis by simp
        qed
      qed
      moreover have "graph H' h' \ M"
        \<comment> \<open>and \<open>h'\<close> is norm-preserving. \<^smallskip>\<close>
      proof (unfold M_def)
        show "graph H' h' \ norm_pres_extensions E p F f"
        proof (rule norm_pres_extensionI2)
          show "linearform H' h'"
            using h'_def H'_def HE linearform \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> E
            by (rule h'_lf)
          show "H' \ E"
          unfolding H'_def
          proof
            show "H \ E" by fact
            show "vectorspace E" by fact
            from x'E show "lin x' \<unlhd> E" ..
          qed
          from H \<open>F \<unlhd> H\<close> HH' show FH': "F \<unlhd> H'"
            by (rule vectorspace.subspace_trans)
          show "graph F f \ graph H' h'"
          proof (rule graph_extI)
            fix x assume x: "x \ F"
            with graphs have "f x = h x" ..
            also have "\ = h x + 0 * xi" by simp
            also have "\ = (let (y, a) = (x, 0) in h y + a * xi)"
              by (simp add: Let_def)
            also have "(x, 0) =
                (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
              using E HE
            proof (rule decomp_H'_H [symmetric])
              from FH x show "x \ H" ..
              from x' show "x' \<noteq> 0" .
              show "x' \ H" by fact
              show "x' \ E" by fact
            qed
            also have
              "(let (y, a) = (SOME (y, a). x = y + a \ x' \ y \ H)
              in h y + a * xi) = h' x" by (simp only: h'_def)
            finally show "f x = h' x" .
          next
            from FH' show "F \ H'" ..
          qed
          show "\x \ H'. h' x \ p x"
            using h'_def H'_def \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> E HE
              \<open>seminorm E p\<close> linearform and hp xi
            by (rule h'_norm_pres)
        qed
      qed
      ultimately show ?thesis ..
    qed
    then have "\ (\x \ M. g \ x \ g = x)" by simp
      \<comment> \<open>So the graph \<open>g\<close> of \<open>h\<close> cannot be maximal. Contradiction! \<^smallskip>\<close>
    with gx show "H = E" by contradiction
  qed

  from HE_eq and linearform have "linearform E h"
    by (simp only:)
  moreover have "\x \ F. h x = f x"
  proof
    fix x assume "x \ F"
    with graphs have "f x = h x" ..
    then show "h x = f x" ..
  qed
  moreover from HE_eq and hp have "\x \ E. h x \ p x"
    by (simp only:)
  ultimately show ?thesis by blast
qed

subsection \<open>Alternative formulation\<close>

text \<open>
  The following alternative formulation of the Hahn-Banach
  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form \<open>f\<close>
  and a seminorm \<open>p\<close> the following inequality are equivalent:\footnote{This
  was shown in lemma @{thm [source] abs_ineq_iff} (see page
  \pageref{abs-ineq-iff}).}
  \begin{center}
  \begin{tabular}{lll}
  \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
  \end{tabular}
  \end{center}
\<close>

theorem abs_Hahn_Banach:
  assumes E: "vectorspace E" and FE: "subspace F E"
    and lf: "linearform F f" and sn: "seminorm E p"
  assumes fp: "\x \ F. \f x\ \ p x"
  shows "\g. linearform E g
    \<and> (\<forall>x \<in> F. g x = f x)
    \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
proof -
  interpret vectorspace E by fact
  interpret subspace F E by fact
  interpret linearform F f by fact
  interpret seminorm E p by fact
  have "\g. linearform E g \ (\x \ F. g x = f x) \ (\x \ E. g x \ p x)"
    using E FE sn lf
  proof (rule Hahn_Banach)
    show "\x \ F. f x \ p x"
      using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1])
  qed
  then obtain g where lg: "linearform E g" and *: "\x \ F. g x = f x"
      and **: "\x \ E. g x \ p x" by blast
  have "\x \ E. \g x\ \ p x"
    using _ E sn lg **
  proof (rule abs_ineq_iff [THEN iffD2])
    show "E \ E" ..
  qed
  with lg * show ?thesis by blast
qed

subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>

text \<open>
  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>, can
  be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>.
\<close>

theorem norm_Hahn_Banach:
  fixes V and norm (\<open>\<parallel>_\<parallel>\<close>)
  fixes B defines "\V f. B V f \ {0} \ {\f x\ / \x\ | x. x \ 0 \ x \ V}"
  fixes fn_norm (\<open>\<parallel>_\<parallel>\<hyphen>_\<close> [0, 1000] 999)
  defines "\V f. \f\\V \ \(B V f)"
  assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
    and linearform: "linearform F f" and "continuous F f norm"
  shows "\g. linearform E g
     \<and> continuous E g norm
     \<and> (\<forall>x \<in> F. g x = f x)
     \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
proof -
  interpret normed_vectorspace E norm by fact
  interpret normed_vectorspace_with_fn_norm E norm B fn_norm
    by (auto simp: B_def fn_norm_def) intro_locales
  interpret subspace F E by fact
  interpret linearform F f by fact
  interpret continuous F f norm by fact
  have E: "vectorspace E" by intro_locales
  have F: "vectorspace F" by rule intro_locales
  have F_norm: "normed_vectorspace F norm"
    using FE E_norm by (rule subspace_normed_vs)
  have ge_zero: "0 \ \f\\F"
    by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
      [OF normed_vectorspace_with_fn_norm.intro,
       OF F_norm \<open>continuous F f norm\<close> , folded B_def fn_norm_def])
  txt \<open>We define a function \<open>p\<close> on \<open>E\<close> as follows:
    \<open>p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>\<close>
  define p where "p x = \f\\F * \x\" for x

  txt \<open>\<open>p\<close> is a seminorm on \<open>E\<close>:\<close>
  have q: "seminorm E p"
  proof
    fix x y a assume x: "x \ E" and y: "y \ E"

    txt \<open>\<open>p\<close> is positive definite:\<close>
    have "0 \ \f\\F" by (rule ge_zero)
    moreover from x have "0 \ \x\" ..
    ultimately show "0 \ p x"
      by (simp add: p_def zero_le_mult_iff)

    txt \<open>\<open>p\<close> is absolutely homogeneous:\<close>

    show "p (a \ x) = \a\ * p x"
    proof -
      have "p (a \ x) = \f\\F * \a \ x\" by (simp only: p_def)
      also from x have "\a \ x\ = \a\ * \x\" by (rule abs_homogenous)
      also have "\f\\F * (\a\ * \x\) = \a\ * (\f\\F * \x\)" by simp
      also have "\ = \a\ * p x" by (simp only: p_def)
      finally show ?thesis .
    qed

    txt \<open>Furthermore, \<open>p\<close> is subadditive:\<close>

    show "p (x + y) \ p x + p y"
    proof -
      have "p (x + y) = \f\\F * \x + y\" by (simp only: p_def)
      also have a: "0 \ \f\\F" by (rule ge_zero)
      from x y have "\x + y\ \ \x\ + \y\" ..
      with a have " \f\\F * \x + y\ \ \f\\F * (\x\ + \y\)"
        by (simp add: mult_left_mono)
      also have "\ = \f\\F * \x\ + \f\\F * \y\" by (simp only: distrib_left)
      also have "\ = p x + p y" by (simp only: p_def)
      finally show ?thesis .
    qed
  qed

  txt \<open>\<open>f\<close> is bounded by \<open>p\<close>.\<close>

  have "\x \ F. \f x\ \ p x"
  proof
    fix x assume "x \ F"
    with \<open>continuous F f norm\<close> and linearform
    show "\f x\ \ p x"
      unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
        [OF normed_vectorspace_with_fn_norm.intro,
         OF F_norm, folded B_def fn_norm_def])
  qed

  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we can
    apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
    extended in a norm-preserving way to some function \<open>g\<close> on the whole vector
    space \<open>E\<close>.\<close>

  with E FE linearform q obtain g where
      linearformE: "linearform E g"
    and a: "\x \ F. g x = f x"
    and b: "\x \ E. \g x\ \ p x"
    by (rule abs_Hahn_Banach [elim_format]) iprover

  txt \<open>We furthermore have to show that \<open>g\<close> is also continuous:\<close>

  have g_cont: "continuous E g norm" using linearformE
  proof
    fix x assume "x \ E"
    with b show "\g x\ \ \f\\F * \x\"
      by (simp only: p_def)
  qed

  txt \<open>To complete the proof, we show that \<open>\<parallel>g\<parallel> = \<parallel>f\<parallel>\<close>.\<close>

  have "\g\\E = \f\\F"
  proof (rule order_antisym)
    txt \<open>
      First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>. The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the
      smallest \<open>c \<in> \<real>\<close> such that
      \begin{center}
      \begin{tabular}{l}
      \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
      \end{tabular}
      \end{center}
      \<^noindent> Furthermore holds
      \begin{center}
      \begin{tabular}{l}
      \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
      \end{tabular}
      \end{center}
    \<close>

    from g_cont _ ge_zero
    show "\g\\E \ \f\\F"
    proof
      fix x assume "x \ E"
      with b show "\g x\ \ \f\\F * \x\"
        by (simp only: p_def)
    qed

    txt \<open>The other direction is achieved by a similar argument.\<close>

    show "\f\\F \ \g\\E"
    proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
        [OF normed_vectorspace_with_fn_norm.intro,
         OF F_norm, folded B_def fn_norm_def])
      fix x assume x: "x \ F"
      show "\f x\ \ \g\\E * \x\"
      proof -
        from a x have "g x = f x" ..
        then have "\f x\ = \g x\" by (simp only:)
        also from g_cont have "\ \ \g\\E * \x\"
        proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def])
          from FE x show "x \ E" ..
        qed
        finally show ?thesis .
      qed
    next
      show "0 \ \g\\E"
        using g_cont by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
      show "continuous F f norm" by fact
    qed
  qed
  with linearformE a g_cont show ?thesis by blast
qed

end

quality99%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

Quellcode-Bibliothek Hahn_Banach.thy Interaktion und PortierbarkeitIsabelle

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

Quellcode-Bibliothek Hahn_Banach.thy Interaktion und
PortierbarkeitIsabelle