7 theory Hahn_Banach_Ext_Lemmas |
7 theory Hahn_Banach_Ext_Lemmas |
8 imports Function_Norm |
8 imports Function_Norm |
9 begin |
9 begin |
10 |
10 |
11 text \<open> |
11 text \<open> |
12 In this section the following context is presumed. Let \<open>E\<close> be a real |
12 In this section the following context is presumed. Let \<open>E\<close> be a real vector |
13 vector 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> |
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 a linear function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a |
14 function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a superspace of |
15 superspace of \<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> |
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 and \<open>x\<^sub>0\<close> is an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' |
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 = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> |
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 with \<open>y \<in> H\<close> is unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> |
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 for a certain \<open>\<xi>\<close>. |
|
20 |
19 |
21 Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>. |
20 Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>. |
22 |
21 |
23 \<^medskip> |
22 \<^medskip> |
24 This lemma will be used to show the existence of a linear extension of \<open>f\<close> |
23 This lemma will be used to show the existence of a linear extension of \<open>f\<close> |
80 ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast |
79 ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast |
81 qed |
80 qed |
82 |
81 |
83 text \<open> |
82 text \<open> |
84 \<^medskip> |
83 \<^medskip> |
85 The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where |
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> |
86 \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>. |
85 is a linear extension of \<open>h\<close> to \<open>H'\<close>. |
87 \<close> |
86 \<close> |
88 |
87 |
89 lemma h'_lf: |
88 lemma h'_lf: |
90 assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) = |
89 assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) = |
91 SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi" |
90 SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi" |