src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
 author wenzelm Mon Apr 25 16:09:26 2016 +0200 (2016-04-25) changeset 63040 eb4ddd18d635 parent 61879 e4f9d8f094fe permissions -rw-r--r--
eliminated old 'def';
     1 (*  Title:      HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy

     2     Author:     Gertrud Bauer, TU Munich

     3 *)

     4

     5 section \<open>Extending non-maximal functions\<close>

     6

     7 theory Hahn_Banach_Ext_Lemmas

     8 imports Function_Norm

     9 begin

    10

    11 text \<open>

    12   In this section the following context is presumed. Let \<open>E\<close> be a real vector

    13   space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> a linear

    14   function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a superspace of

    15   \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> and \<open>x\<^sub>0\<close> is an

    16   element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' = H + lin x\<^sub>0\<close>, so

    17   for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is

    18   unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>.

    19

    20   Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>.

    21

    22   \<^medskip>

    23   This lemma will be used to show the existence of a linear extension of \<open>f\<close>

    24   (see page \pageref{ex-xi-use}). It is a consequence of the completeness of

    25   \<open>\<real>\<close>. To show

    26   \begin{center}

    27   \begin{tabular}{l}

    28   \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close>

    29   \end{tabular}

    30   \end{center}

    31   \<^noindent> it suffices to show that

    32   \begin{center}

    33   \begin{tabular}{l}

    34   \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close>

    35   \end{tabular}

    36   \end{center}

    37 \<close>

    38

    39 lemma ex_xi:

    40   assumes "vectorspace F"

    41   assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"

    42   shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"

    43 proof -

    44   interpret vectorspace F by fact

    45   txt \<open>From the completeness of the reals follows:

    46     The set \<open>S = {a u. u \<in> F}\<close> has a supremum, if it is

    47     non-empty and has an upper bound.\<close>

    48

    49   let ?S = "{a u | u. u \<in> F}"

    50   have "\<exists>xi. lub ?S xi"

    51   proof (rule real_complete)

    52     have "a 0 \<in> ?S" by blast

    53     then show "\<exists>X. X \<in> ?S" ..

    54     have "\<forall>y \<in> ?S. y \<le> b 0"

    55     proof

    56       fix y assume y: "y \<in> ?S"

    57       then obtain u where u: "u \<in> F" and y: "y = a u" by blast

    58       from u and zero have "a u \<le> b 0" by (rule r)

    59       with y show "y \<le> b 0" by (simp only:)

    60     qed

    61     then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..

    62   qed

    63   then obtain xi where xi: "lub ?S xi" ..

    64   {

    65     fix y assume "y \<in> F"

    66     then have "a y \<in> ?S" by blast

    67     with xi have "a y \<le> xi" by (rule lub.upper)

    68   }

    69   moreover {

    70     fix y assume y: "y \<in> F"

    71     from xi have "xi \<le> b y"

    72     proof (rule lub.least)

    73       fix au assume "au \<in> ?S"

    74       then obtain u where u: "u \<in> F" and au: "au = a u" by blast

    75       from u y have "a u \<le> b y" by (rule r)

    76       with au show "au \<le> b y" by (simp only:)

    77     qed

    78   }

    79   ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast

    80 qed

    81

    82 text \<open>

    83   \<^medskip>

    84   The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close>

    85   is a linear extension of \<open>h\<close> to \<open>H'\<close>.

    86 \<close>

    87

    88 lemma h'_lf:

    89   assumes h'_def: "\<And>x. h' x = (let (y, a) =

    90       SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi)"

    91     and H'_def: "H' = H + lin x0"

    92     and HE: "H \<unlhd> E"

    93   assumes "linearform H h"

    94   assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"

    95   assumes E: "vectorspace E"

    96   shows "linearform H' h'"

    97 proof -

    98   interpret linearform H h by fact

    99   interpret vectorspace E by fact

   100   show ?thesis

   101   proof

   102     note E = \<open>vectorspace E\<close>

   103     have H': "vectorspace H'"

   104     proof (unfold H'_def)

   105       from \<open>x0 \<in> E\<close>

   106       have "lin x0 \<unlhd> E" ..

   107       with HE show "vectorspace (H + lin x0)" using E ..

   108     qed

   109     {

   110       fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"

   111       show "h' (x1 + x2) = h' x1 + h' x2"

   112       proof -

   113         from H' x1 x2 have "x1 + x2 \<in> H'"

   114           by (rule vectorspace.add_closed)

   115         with x1 x2 obtain y y1 y2 a a1 a2 where

   116           x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"

   117           and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"

   118           and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"

   119           unfolding H'_def sum_def lin_def by blast

   120

   121         have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0

   122         proof (rule decomp_H') text_raw \<open>\label{decomp-H-use}\<close>

   123           from HE y1 y2 show "y1 + y2 \<in> H"

   124             by (rule subspace.add_closed)

   125           from x0 and HE y y1 y2

   126           have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto

   127           with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"

   128             by (simp add: add_ac add_mult_distrib2)

   129           also note x1x2

   130           finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .

   131         qed

   132

   133         from h'_def x1x2 E HE y x0

   134         have "h' (x1 + x2) = h y + a * xi"

   135           by (rule h'_definite)

   136         also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"

   137           by (simp only: ya)

   138         also from y1 y2 have "h (y1 + y2) = h y1 + h y2"

   139           by simp

   140         also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"

   141           by (simp add: distrib_right)

   142         also from h'_def x1_rep E HE y1 x0

   143         have "h y1 + a1 * xi = h' x1"

   144           by (rule h'_definite [symmetric])

   145         also from h'_def x2_rep E HE y2 x0

   146         have "h y2 + a2 * xi = h' x2"

   147           by (rule h'_definite [symmetric])

   148         finally show ?thesis .

   149       qed

   150     next

   151       fix x1 c assume x1: "x1 \<in> H'"

   152       show "h' (c \<cdot> x1) = c * (h' x1)"

   153       proof -

   154         from H' x1 have ax1: "c \<cdot> x1 \<in> H'"

   155           by (rule vectorspace.mult_closed)

   156         with x1 obtain y a y1 a1 where

   157             cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"

   158           and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"

   159           unfolding H'_def sum_def lin_def by blast

   160

   161         have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0

   162         proof (rule decomp_H')

   163           from HE y1 show "c \<cdot> y1 \<in> H"

   164             by (rule subspace.mult_closed)

   165           from x0 and HE y y1

   166           have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto

   167           with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"

   168             by (simp add: mult_assoc add_mult_distrib1)

   169           also note cx1_rep

   170           finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .

   171         qed

   172

   173         from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"

   174           by (rule h'_definite)

   175         also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"

   176           by (simp only: ya)

   177         also from y1 have "h (c \<cdot> y1) = c * h y1"

   178           by simp

   179         also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"

   180           by (simp only: distrib_left)

   181         also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"

   182           by (rule h'_definite [symmetric])

   183         finally show ?thesis .

   184       qed

   185     }

   186   qed

   187 qed

   188

   189 text \<open>

   190   \<^medskip>

   191   The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>.

   192 \<close>

   193

   194 lemma h'_norm_pres:

   195   assumes h'_def: "\<And>x. h' x = (let (y, a) =

   196       SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi)"

   197     and H'_def: "H' = H + lin x0"

   198     and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"

   199   assumes E: "vectorspace E" and HE: "subspace H E"

   200     and "seminorm E p" and "linearform H h"

   201   assumes a: "\<forall>y \<in> H. h y \<le> p y"

   202     and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"

   203   shows "\<forall>x \<in> H'. h' x \<le> p x"

   204 proof -

   205   interpret vectorspace E by fact

   206   interpret subspace H E by fact

   207   interpret seminorm E p by fact

   208   interpret linearform H h by fact

   209   show ?thesis

   210   proof

   211     fix x assume x': "x \<in> H'"

   212     show "h' x \<le> p x"

   213     proof -

   214       from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"

   215         and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto

   216       from x' obtain y a where

   217           x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"

   218         unfolding H'_def sum_def lin_def by blast

   219       from y have y': "y \<in> E" ..

   220       from y have ay: "inverse a \<cdot> y \<in> H" by simp

   221

   222       from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"

   223         by (rule h'_definite)

   224       also have "\<dots> \<le> p (y + a \<cdot> x0)"

   225       proof (rule linorder_cases)

   226         assume z: "a = 0"

   227         then have "h y + a * xi = h y" by simp

   228         also from a y have "\<dots> \<le> p y" ..

   229         also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp

   230         finally show ?thesis .

   231       next

   232         txt \<open>In the case \<open>a < 0\<close>, we use \<open>a\<^sub>1\<close>

   233           with \<open>ya\<close> taken as \<open>y / a\<close>:\<close>

   234         assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp

   235         from a1 ay

   236         have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..

   237         with lz have "a * xi \<le>

   238           a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"

   239           by (simp add: mult_left_mono_neg order_less_imp_le)

   240

   241         also have "\<dots> =

   242           - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"

   243           by (simp add: right_diff_distrib)

   244         also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =

   245           p (a \<cdot> (inverse a \<cdot> y + x0))"

   246           by (simp add: abs_homogenous)

   247         also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"

   248           by (simp add: add_mult_distrib1 mult_assoc [symmetric])

   249         also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"

   250           by simp

   251         finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .

   252         then show ?thesis by simp

   253       next

   254         txt \<open>In the case \<open>a > 0\<close>, we use \<open>a\<^sub>2\<close>

   255           with \<open>ya\<close> taken as \<open>y / a\<close>:\<close>

   256         assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp

   257         from a2 ay

   258         have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..

   259         with gz have "a * xi \<le>

   260           a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"

   261           by simp

   262         also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"

   263           by (simp add: right_diff_distrib)

   264         also from gz x0 y'

   265         have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"

   266           by (simp add: abs_homogenous)

   267         also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"

   268           by (simp add: add_mult_distrib1 mult_assoc [symmetric])

   269         also from nz y have "a * h (inverse a \<cdot> y) = h y"

   270           by simp

   271         finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .

   272         then show ?thesis by simp

   273       qed

   274       also from x_rep have "\<dots> = p x" by (simp only:)

   275       finally show ?thesis .

   276     qed

   277   qed

   278 qed

   279

   280 end