Quelle  Hahn_Banach_Ext_Lemmas.thy

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

section ‹Extending non-maximal functions›

theory Hahn_Banach_Ext_Lemmas
imports Function_Norm
begin

text ‹
  In this section the following context is presumed. Let ‹E› be a real vector
  space with a seminorm ‹q› on ‹E›. ‹F› is a subspace of ‹E› and ‹f› a linear
  function on ‹F›. We consider a subspace ‹H› of ‹E› that is a superspace of
  ‹F› and a linear form ‹h› on ‹H›. ‹H› is a not equal to ‹E› and ‹x🪙0› is an
  element in ‹E - H›. ‹H› is extended to the direct sum ‹H' = H + lin x🪙0›, so
  for any ‹x ∈ H'› the decomposition of ‹x = y + a ⋅ x› with ‹y ∈ H› is
  unique. ‹h'› is defined on ‹H'› by ‹h' x = h y + a ⋅ ξ› for a certain ‹ξ›.
 
  Subsequently we show some properties of this extension ‹h'› of ‹h›.
 
  🪙
  This lemma will be used to show the existence of a linear extension of ‹f›
  (see page \pageref{ex-xi-use}). It is a consequence of the completeness of
  ‹ℝ›. To show
  \begin{center}
  \begin{tabular}{l}
  ‹∃ξ. ∀y ∈ F. a y ≤ ξ ∧ ξ ≤ b y›
  \end{tabular}
  \end{center}
  🪙 it suffices to show that
  \begin{center}
  \begin{tabular}{l}
  ‹∀u ∈ F. ∀v ∈ F. a u ≤ b v›
  \end{tabular}
  \end{center}
 ›

lemma ex_xi:
  assumes "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 -
  interpret vectorspace F by fact
  txt ‹From the completeness of the reals follows:
  The set ‹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" ..
  have "a y ≤ xi" if "y ∈ F" for y
  proof -
    from that have "a y ∈ ?S" by blast
    with xi show ?thesis by (rule lub.upper)
  qed
  moreover have "xi ≤ b y" if y: "y ∈ F" for y
  proof -
    from xi
    show ?thesis
    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
  qed
  ultimately show "∃xi. ∀y ∈ F. a y ≤ xi ∧ xi ≤ b y" by blast
qed

text ‹
  🪙
  The function ‹h'› is defined as a ‹h' x = h y + a ⋅ ξ› where ‹x = y + a ⋅ ξ›
  is a linear extension of ‹h› to ‹H'›.
 ›

lemma h'_lf:
  assumes h'_def: "∧x. 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 ⊴ E"
  assumes "linearform H h"
  assumes x0: "x0 ∉ H"  "x0 ∈ E"  "x0 ≠ 0"
  assumes E: "vectorspace E"
  shows "linearform H' h'"
proof -
  interpret linearform H h by fact
  interpret vectorspace E by fact
  show ?thesis
  proof
    note E = ‹vectorspace E›
    have H': "vectorspace H'"
    proof (unfold H'_def)
      from ‹x0 ∈ E›
      have "lin x0 ⊴ E" ..
      with HE show "vectorspace (H + lin x0)" using E ..
    qed
    show "h' (x1 + x2) = h' x1 + h' x2" if x1: "x1 ∈ H'" and x2: "x2 ∈ H'" for x1 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"
        unfolding H'_def sum_def lin_def by blast

      have ya: "y1 + y2 = y ∧ a1 + a2 = a" using E HE _ y x0
      proof (rule decomp_H') text_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 E 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: distrib_right)
      also from h'_def x1_rep E HE y1 x0
      have "h y1 + a1 * xi = h' x1"
        by (rule h'_definite [symmetric])
      also from h'_def x2_rep E HE y2 x0
      have "h y2 + a2 * xi = h' x2"
        by (rule h'_definite [symmetric])
      finally show ?thesis .
    qed
    show "h' (c ⋅ x1) = c * (h' x1)" if x1: "x1 ∈ H'" for x1 c
    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"
        unfolding H'_def sum_def lin_def by blast

      have ya: "c ⋅ y1 = y ∧ c * a1 = a" using E 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 E 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: distrib_left)
      also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
        by (rule h'_definite [symmetric])
      finally show ?thesis .
    qed
  qed
qed

text ‹
  🪙
  The linear extension ‹h'› of ‹h› is bounded by the seminorm ‹p›.
 ›

lemma h'_norm_pres:
  assumes h'_def: "∧x. 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"
  assumes E: "vectorspace E" and HE: "subspace H E"
    and "seminorm E p" and "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 -
  interpret vectorspace E by fact
  interpret subspace H E by fact
  interpret seminorm E p by fact
  interpret linearform H h by fact
  show ?thesis
  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"
        unfolding H'_def sum_def lin_def by blast
      from y have y': "y ∈ E" ..
      from y have ay: "inverse a ⋅ y ∈ H" by simp

      from h'_def x_rep E HE 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 ‹a 🚫›, we use ‹a🪙1›
  with ‹ya› taken as ‹y / a›:›
        assume lz: "a < 0" then have 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 ‹a > 0›, we use ‹a🪙2›
  with ‹ya› taken as ‹y / a›:›
        assume gz: "0 < a" then have 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
qed

end