src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
author bauerg
Mon Jul 17 13:58:18 2000 +0200 (2000-07-17)
changeset 9374 153853af318b
parent 9256 f9a6670427fb
child 9379 21cfeae6659d
permissions -rw-r--r--
- xsymbols for
\<noteq> \<notin> \<in> \<exists> \<forall>
\<and> \<inter> \<union> \<Union>
- vector space type of {plus, minus, zero}, overload 0 in vector space
- syntax |.| and ||.||
wenzelm@7917
     1
(*  Title:      HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
wenzelm@7917
     2
    ID:         $Id$
wenzelm@7917
     3
    Author:     Gertrud Bauer, TU Munich
wenzelm@7917
     4
*)
wenzelm@7917
     5
bauerg@9256
     6
header {* Extending non-maximal functions *};
wenzelm@7917
     7
bauerg@9256
     8
theory HahnBanachExtLemmas = FunctionNorm:;
wenzelm@7917
     9
wenzelm@7917
    10
text{* In this section the following context is presumed.
wenzelm@7917
    11
Let $E$ be a real vector space with a 
wenzelm@7978
    12
seminorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear 
wenzelm@7917
    13
function on $F$. We consider a subspace $H$ of $E$ that is a 
wenzelm@7978
    14
superspace of $F$ and a linear form $h$ on $H$. $H$ is a not equal 
wenzelm@7917
    15
to $E$ and $x_0$ is an element in $E \backslash H$.
wenzelm@7917
    16
$H$ is extended to the direct sum  $H_0 = H + \idt{lin}\ap x_0$, so for
wenzelm@7917
    17
any $x\in H_0$ the decomposition of $x = y + a \mult x$ 
wenzelm@7917
    18
with $y\in H$ is unique. $h_0$ is defined on $H_0$ by  
wenzelm@7978
    19
$h_0\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$.
wenzelm@7917
    20
wenzelm@7917
    21
Subsequently we show some properties of this extension $h_0$ of $h$.
bauerg@9256
    22
*}; 
wenzelm@7917
    23
wenzelm@7917
    24
wenzelm@7978
    25
text {* This lemma will be used to show the existence of a linear
wenzelm@7978
    26
extension of $f$ (see page \pageref{ex-xi-use}). 
wenzelm@7978
    27
It is a consequence
wenzelm@7978
    28
of the completeness of $\bbbR$. To show 
wenzelm@7917
    29
\begin{matharray}{l}
wenzelm@7978
    30
\Ex{\xi}{\All {y\in F}{a\ap y \leq \xi \land \xi \leq b\ap y}}
wenzelm@7978
    31
\end{matharray} 
wenzelm@7917
    32
it suffices to show that 
wenzelm@7978
    33
\begin{matharray}{l} \All
wenzelm@7978
    34
{u\in F}{\All {v\in F}{a\ap u \leq b \ap v}} 
bauerg@9256
    35
\end{matharray} *};
wenzelm@7917
    36
wenzelm@7917
    37
lemma ex_xi: 
bauerg@9374
    38
  "[| is_vectorspace F; !! u v. [| u \<in> F; v \<in> F |] ==> a u <= b v |]
bauerg@9374
    39
  ==> \<exists>xi::real. \<forall>y \<in> F. a y <= xi \<and> xi <= b y"; 
bauerg@9256
    40
proof -;
bauerg@9256
    41
  assume vs: "is_vectorspace F";
bauerg@9374
    42
  assume r: "(!! u v. [| u \<in> F; v \<in> F |] ==> a u <= (b v::real))";
wenzelm@7917
    43
wenzelm@7917
    44
  txt {* From the completeness of the reals follows:
bauerg@8084
    45
  The set $S = \{a\: u\dt\: u\in F\}$ has a supremum, if
bauerg@9256
    46
  it is non-empty and has an upper bound. *};
wenzelm@7917
    47
bauerg@9374
    48
  let ?S = "{a u :: real | u. u \<in> F}";
wenzelm@7917
    49
bauerg@9374
    50
  have "\<exists>xi. isLub UNIV ?S xi";  
bauerg@9256
    51
  proof (rule reals_complete);
wenzelm@7917
    52
  
bauerg@9256
    53
    txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
wenzelm@7917
    54
bauerg@9374
    55
    from vs; have "a 0 \<in> ?S"; by force;
bauerg@9374
    56
    thus "\<exists>X. X \<in> ?S"; ..;
wenzelm@7917
    57
bauerg@9256
    58
    txt {* $b\ap \zero$ is an upper bound of $S$: *};
wenzelm@7917
    59
bauerg@9374
    60
    show "\<exists>Y. isUb UNIV ?S Y"; 
bauerg@9256
    61
    proof; 
bauerg@9374
    62
      show "isUb UNIV ?S (b 0)";
bauerg@9256
    63
      proof (intro isUbI setleI ballI);
bauerg@9374
    64
        show "b 0 \<in> UNIV"; ..;
bauerg@9256
    65
      next;
wenzelm@7917
    66
bauerg@9256
    67
        txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
wenzelm@7917
    68
bauerg@9374
    69
        fix y; assume y: "y \<in> ?S"; 
bauerg@9374
    70
        from y; have "\<exists>u \<in> F. y = a u"; by fast;
bauerg@9374
    71
        thus "y <= b 0"; 
bauerg@9256
    72
        proof;
bauerg@9374
    73
          fix u; assume "u \<in> F"; 
bauerg@9256
    74
          assume "y = a u";
bauerg@9374
    75
          also; have "a u <= b 0"; by (rule r) (simp!)+;
bauerg@9256
    76
          finally; show ?thesis; .;
bauerg@9256
    77
        qed;
bauerg@9256
    78
      qed;
bauerg@9256
    79
    qed;
bauerg@9256
    80
  qed;
wenzelm@7917
    81
bauerg@9374
    82
  thus "\<exists>xi. \<forall>y \<in> F. a y <= xi \<and> xi <= b y"; 
bauerg@9256
    83
  proof (elim exE);
bauerg@9256
    84
    fix xi; assume "isLub UNIV ?S xi"; 
bauerg@9256
    85
    show ?thesis;
bauerg@9256
    86
    proof (intro exI conjI ballI); 
wenzelm@7917
    87
   
bauerg@9256
    88
      txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *};
wenzelm@7917
    89
     
bauerg@9374
    90
      fix y; assume y: "y \<in> F";
bauerg@9256
    91
      show "a y <= xi";    
bauerg@9256
    92
      proof (rule isUbD);  
bauerg@9256
    93
        show "isUb UNIV ?S xi"; ..;
bauerg@9256
    94
      qed (force!);
bauerg@9256
    95
    next;
wenzelm@7917
    96
bauerg@9256
    97
      txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *};
wenzelm@7917
    98
bauerg@9374
    99
      fix y; assume "y \<in> F";
bauerg@9256
   100
      show "xi <= b y";  
bauerg@9256
   101
      proof (intro isLub_le_isUb isUbI setleI);
bauerg@9374
   102
        show "b y \<in> UNIV"; ..;
bauerg@9374
   103
        show "\<forall>ya \<in> ?S. ya <= b y"; 
bauerg@9256
   104
        proof;
bauerg@9374
   105
          fix au; assume au: "au \<in> ?S ";
bauerg@9374
   106
          hence "\<exists>u \<in> F. au = a u"; by fast;
bauerg@9256
   107
          thus "au <= b y";
bauerg@9256
   108
          proof;
bauerg@9374
   109
            fix u; assume "u \<in> F"; assume "au = a u";  
bauerg@9256
   110
            also; have "... <= b y"; by (rule r);
bauerg@9256
   111
            finally; show ?thesis; .;
bauerg@9256
   112
          qed;
bauerg@9256
   113
        qed;
bauerg@9256
   114
      qed; 
bauerg@9256
   115
    qed;
bauerg@9256
   116
  qed;
bauerg@9256
   117
qed;
wenzelm@7917
   118
bauerg@8084
   119
text{* \medskip The function $h_0$ is defined as a
bauerg@8084
   120
$h_0\ap x = h\ap y + a\cdot \xi$ where $x = y + a\mult \xi$
bauerg@9256
   121
is a linear extension of $h$ to $H_0$. *};
wenzelm@7917
   122
bauerg@9374
   123
lemma h'_lf: 
bauerg@9374
   124
  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
wenzelm@7917
   125
                in h y + a * xi);
bauerg@9374
   126
  H' == H + lin x0; is_subspace H E; is_linearform H h; x0 \<notin> H; 
bauerg@9374
   127
  x0 \<in> E; x0 \<noteq> 0; is_vectorspace E |]
bauerg@9374
   128
  ==> is_linearform H' h'";
bauerg@9256
   129
proof -;
bauerg@9374
   130
  assume h'_def: 
bauerg@9374
   131
    "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
wenzelm@7917
   132
               in h y + a * xi)"
bauerg@9374
   133
    and H'_def: "H' == H + lin x0" 
bauerg@9374
   134
    and vs: "is_subspace H E" "is_linearform H h" "x0 \<notin> H"
bauerg@9374
   135
      "x0 \<noteq> 0" "x0 \<in> E" "is_vectorspace E";
wenzelm@7917
   136
bauerg@9374
   137
  have h': "is_vectorspace H'"; 
bauerg@9374
   138
  proof (unfold H'_def, rule vs_sum_vs);
bauerg@9256
   139
    show "is_subspace (lin x0) E"; ..;
bauerg@9256
   140
  qed; 
wenzelm@7917
   141
bauerg@9256
   142
  show ?thesis;
bauerg@9256
   143
  proof;
bauerg@9374
   144
    fix x1 x2; assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"; 
wenzelm@7917
   145
wenzelm@7978
   146
    txt{* We now have to show that $h_0$ is additive, i.~e.\
wenzelm@7917
   147
    $h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
bauerg@9256
   148
    for $x_1, x_2\in H$. *}; 
wenzelm@7917
   149
bauerg@9374
   150
    have x1x2: "x1 + x2 \<in> H'"; 
bauerg@9374
   151
      by (rule vs_add_closed, rule h'); 
bauerg@9256
   152
    from x1; 
bauerg@9374
   153
    have ex_x1: "\<exists> y1 a1. x1 = y1 + a1 \<cdot> x0  \<and> y1 \<in> H"; 
bauerg@9374
   154
      by (unfold H'_def vs_sum_def lin_def) fast;
bauerg@9256
   155
    from x2; 
bauerg@9374
   156
    have ex_x2: "\<exists> y2 a2. x2 = y2 + a2 \<cdot> x0 \<and> y2 \<in> H"; 
bauerg@9374
   157
      by (unfold H'_def vs_sum_def lin_def) fast;
bauerg@9256
   158
    from x1x2; 
bauerg@9374
   159
    have ex_x1x2: "\<exists> y a. x1 + x2 = y + a \<cdot> x0 \<and> y \<in> H";
bauerg@9374
   160
      by (unfold H'_def vs_sum_def lin_def) fast;
wenzelm@7917
   161
bauerg@9256
   162
    from ex_x1 ex_x2 ex_x1x2;
bauerg@9374
   163
    show "h' (x1 + x2) = h' x1 + h' x2";
bauerg@9256
   164
    proof (elim exE conjE);
bauerg@9256
   165
      fix y1 y2 y a1 a2 a;
bauerg@9374
   166
      assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
bauerg@9374
   167
         and y2: "x2 = y2 + a2 \<cdot> x0"     and y2': "y2 \<in> H" 
bauerg@9374
   168
         and y: "x1 + x2 = y + a \<cdot> x0"   and y':  "y  \<in> H"; 
wenzelm@7917
   169
bauerg@9374
   170
      have ya: "y1 + y2 = y \<and> a1 + a2 = a"; 
bauerg@9374
   171
      proof (rule decomp_H');;
bauerg@9374
   172
	txt_raw {* \label{decomp-H-use} *};;
bauerg@9374
   173
        show "y1 + y2 + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0"; 
bauerg@9256
   174
          by (simp! add: vs_add_mult_distrib2 [of E]);
bauerg@9374
   175
        show "y1 + y2 \<in> H"; ..;
bauerg@9256
   176
      qed;
wenzelm@7917
   177
bauerg@9374
   178
      have "h' (x1 + x2) = h y + a * xi";
bauerg@9374
   179
	by (rule h'_definite);
bauerg@9256
   180
      also; have "... = h (y1 + y2) + (a1 + a2) * xi"; 
bauerg@9256
   181
        by (simp add: ya);
bauerg@9256
   182
      also; from vs y1' y2'; 
bauerg@9256
   183
      have "... = h y1 + h y2 + a1 * xi + a2 * xi"; 
wenzelm@7978
   184
	by (simp add: linearform_add [of H] 
bauerg@9256
   185
                      real_add_mult_distrib);
bauerg@9256
   186
      also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; 
bauerg@9256
   187
        by simp;
bauerg@9374
   188
      also; have "h y1 + a1 * xi = h' x1"; 
bauerg@9374
   189
        by (rule h'_definite [RS sym]);
bauerg@9374
   190
      also; have "h y2 + a2 * xi = h' x2"; 
bauerg@9374
   191
        by (rule h'_definite [RS sym]);
bauerg@9256
   192
      finally; show ?thesis; .;
bauerg@9256
   193
    qed;
wenzelm@7917
   194
 
wenzelm@7978
   195
    txt{* We further have to show that $h_0$ is multiplicative, 
wenzelm@7927
   196
    i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
wenzelm@7978
   197
    for $x\in H$ and $c\in \bbbR$. 
bauerg@9256
   198
    *}; 
wenzelm@7917
   199
bauerg@9256
   200
  next;  
bauerg@9374
   201
    fix c x1; assume x1: "x1 \<in> H'";    
bauerg@9374
   202
    have ax1: "c \<cdot> x1 \<in> H'";
bauerg@9374
   203
      by (rule vs_mult_closed, rule h');
bauerg@9374
   204
    from x1; have ex_x: "!! x. x\<in> H' 
bauerg@9374
   205
                        ==> \<exists> y a. x = y + a \<cdot> x0 \<and> y \<in> H";
bauerg@9374
   206
      by (unfold H'_def vs_sum_def lin_def) fast;
wenzelm@7917
   207
bauerg@9374
   208
    from x1; have ex_x1: "\<exists> y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H";
bauerg@9374
   209
      by (unfold H'_def vs_sum_def lin_def) fast;
bauerg@9374
   210
    with ex_x [of "c \<cdot> x1", OF ax1];
bauerg@9374
   211
    show "h' (c \<cdot> x1) = c * (h' x1)";  
bauerg@9256
   212
    proof (elim exE conjE);
bauerg@9256
   213
      fix y1 y a1 a; 
bauerg@9374
   214
      assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
bauerg@9374
   215
        and y: "c \<cdot> x1 = y  + a \<cdot> x0"    and y': "y \<in> H"; 
wenzelm@7917
   216
bauerg@9374
   217
      have ya: "c \<cdot> y1 = y \<and> c * a1 = a"; 
bauerg@9374
   218
      proof (rule decomp_H'); 
bauerg@9374
   219
	show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0"; 
bauerg@9374
   220
          by (simp! add: vs_add_mult_distrib1);
bauerg@9374
   221
        show "c \<cdot> y1 \<in> H"; ..;
bauerg@9256
   222
      qed;
wenzelm@7917
   223
bauerg@9374
   224
      have "h' (c \<cdot> x1) = h y + a * xi"; 
bauerg@9374
   225
	by (rule h'_definite);
bauerg@9374
   226
      also; have "... = h (c \<cdot> y1) + (c * a1) * xi";
bauerg@9256
   227
        by (simp add: ya);
bauerg@9256
   228
      also; from vs y1'; have "... = c * h y1 + c * a1 * xi"; 
bauerg@9256
   229
	by (simp add: linearform_mult [of H]);
bauerg@9256
   230
      also; from vs y1'; have "... = c * (h y1 + a1 * xi)"; 
bauerg@9256
   231
	by (simp add: real_add_mult_distrib2 real_mult_assoc);
bauerg@9374
   232
      also; have "h y1 + a1 * xi = h' x1"; 
bauerg@9374
   233
        by (rule h'_definite [RS sym]);
bauerg@9256
   234
      finally; show ?thesis; .;
bauerg@9256
   235
    qed;
bauerg@9256
   236
  qed;
bauerg@9256
   237
qed;
wenzelm@7917
   238
bauerg@8084
   239
text{* \medskip The linear extension $h_0$ of $h$
bauerg@9256
   240
is bounded by the seminorm $p$. *};
wenzelm@7917
   241
bauerg@9374
   242
lemma h'_norm_pres:
bauerg@9374
   243
  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
wenzelm@7917
   244
                in h y + a * xi);
bauerg@9374
   245
  H' == H + lin x0; x0 \<notin> H; x0 \<in> E; x0 \<noteq> 0; is_vectorspace E; 
bauerg@9374
   246
  is_subspace H E; is_seminorm E p; is_linearform H h; \<forall>y \<in> H. h y <= p y; 
bauerg@9374
   247
  \<forall>y \<in> H. - p (y + x0) - h y <= xi \<and> xi <= p (y + x0) - h y |]
bauerg@9374
   248
   ==> \<forall> x \<in> H'. h' x <= p x"; 
bauerg@9256
   249
proof; 
bauerg@9374
   250
  assume h'_def: 
bauerg@9374
   251
    "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
wenzelm@7917
   252
               in (h y) + a * xi)"
bauerg@9374
   253
    and H'_def: "H' == H + lin x0" 
bauerg@9374
   254
    and vs: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" "is_vectorspace E" 
wenzelm@7978
   255
            "is_subspace H E" "is_seminorm E p" "is_linearform H h" 
bauerg@9374
   256
    and a: "\<forall>y \<in> H. h y <= p y";
bauerg@9374
   257
  presume a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya <= xi";
bauerg@9374
   258
  presume a2: "\<forall>ya \<in> H. xi <= p (ya + x0) - h ya";
bauerg@9374
   259
  fix x; assume "x \<in> H'"; 
wenzelm@7917
   260
  have ex_x: 
bauerg@9374
   261
    "!! x. x \<in> H' ==> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H";
bauerg@9374
   262
    by (unfold H'_def vs_sum_def lin_def) fast;
bauerg@9374
   263
  have "\<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H";
bauerg@9256
   264
    by (rule ex_x);
bauerg@9374
   265
  thus "h' x <= p x";
bauerg@9256
   266
  proof (elim exE conjE);
bauerg@9374
   267
    fix y a; assume x: "x = y + a \<cdot> x0" and y: "y \<in> H";
bauerg@9374
   268
    have "h' x = h y + a * xi";
bauerg@9374
   269
      by (rule h'_definite);
wenzelm@7917
   270
wenzelm@7917
   271
    txt{* Now we show  
wenzelm@7978
   272
    $h\ap y + a \cdot \xi\leq  p\ap (y\plus a \mult x_0)$ 
bauerg@9256
   273
    by case analysis on $a$. \label{linorder_linear_split}*};
wenzelm@7917
   274
bauerg@9374
   275
    also; have "... <= p (y + a \<cdot> x0)";
bauerg@9256
   276
    proof (rule linorder_linear_split); 
wenzelm@7917
   277
bauerg@9256
   278
      assume z: "a = #0"; 
bauerg@9256
   279
      with vs y a; show ?thesis; by simp;
wenzelm@7917
   280
wenzelm@7978
   281
    txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$ 
bauerg@9256
   282
    taken as $y/a$: *};
wenzelm@7917
   283
bauerg@9256
   284
    next;
bauerg@9374
   285
      assume lz: "a < #0"; hence nz: "a \<noteq> #0"; by simp;
bauerg@9256
   286
      from a1; 
bauerg@9374
   287
      have "- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y) <= xi";
bauerg@9256
   288
        by (rule bspec) (simp!);
wenzelm@7917
   289
wenzelm@7978
   290
      txt {* The thesis for this case now follows by a short  
bauerg@9256
   291
      calculation. *};      
wenzelm@7917
   292
      hence "a * xi 
bauerg@9374
   293
            <= a * (- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y))";
bauerg@9256
   294
        by (rule real_mult_less_le_anti [OF lz]);
bauerg@9374
   295
      also; have "... = - a * (p (rinv a \<cdot> y + x0)) 
bauerg@9374
   296
                        - a * (h (rinv a \<cdot> y))";
bauerg@9256
   297
        by (rule real_mult_diff_distrib);
bauerg@9374
   298
      also; from lz vs y; have "- a * (p (rinv a \<cdot> y + x0)) 
bauerg@9374
   299
                               = p (a \<cdot> (rinv a \<cdot> y + x0))";
bauerg@9256
   300
        by (simp add: seminorm_abs_homogenous abs_minus_eqI2);
bauerg@9374
   301
      also; from nz vs y; have "... = p (y + a \<cdot> x0)";
bauerg@9256
   302
        by (simp add: vs_add_mult_distrib1);
bauerg@9374
   303
      also; from nz vs y; have "a * (h (rinv a \<cdot> y)) =  h y";
bauerg@9256
   304
        by (simp add: linearform_mult [RS sym]);
bauerg@9374
   305
      finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
wenzelm@7917
   306
bauerg@9374
   307
      hence "h y + a * xi <= h y + p (y + a \<cdot> x0) - h y";
bauerg@9256
   308
        by (simp add: real_add_left_cancel_le);
bauerg@9256
   309
      thus ?thesis; by simp;
wenzelm@7917
   310
wenzelm@7978
   311
      txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$ 
bauerg@9256
   312
      taken as $y/a$: *};
wenzelm@7978
   313
bauerg@9256
   314
    next; 
bauerg@9374
   315
      assume gz: "#0 < a"; hence nz: "a \<noteq> #0"; by simp;
bauerg@9256
   316
      from a2;
bauerg@9374
   317
      have "xi <= p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y)";
bauerg@9256
   318
        by (rule bspec) (simp!);
wenzelm@7917
   319
wenzelm@7978
   320
      txt {* The thesis for this case follows by a short
bauerg@9256
   321
      calculation: *};
wenzelm@7917
   322
bauerg@9256
   323
      with gz; have "a * xi 
bauerg@9374
   324
            <= a * (p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y))";
bauerg@9256
   325
        by (rule real_mult_less_le_mono);
bauerg@9374
   326
      also; have "... = a * p (rinv a \<cdot> y + x0) 
bauerg@9374
   327
                        - a * h (rinv a \<cdot> y)";
bauerg@9256
   328
        by (rule real_mult_diff_distrib2); 
bauerg@9256
   329
      also; from gz vs y; 
bauerg@9374
   330
      have "a * p (rinv a \<cdot> y + x0) 
bauerg@9374
   331
           = p (a \<cdot> (rinv a \<cdot> y + x0))";
bauerg@9256
   332
        by (simp add: seminorm_abs_homogenous abs_eqI2);
bauerg@9256
   333
      also; from nz vs y; 
bauerg@9374
   334
      have "... = p (y + a \<cdot> x0)";
bauerg@9256
   335
        by (simp add: vs_add_mult_distrib1);
bauerg@9374
   336
      also; from nz vs y; have "a * h (rinv a \<cdot> y) = h y";
bauerg@9256
   337
        by (simp add: linearform_mult [RS sym]); 
bauerg@9374
   338
      finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
wenzelm@7917
   339
 
bauerg@9374
   340
      hence "h y + a * xi <= h y + (p (y + a \<cdot> x0) - h y)";
bauerg@9256
   341
        by (simp add: real_add_left_cancel_le);
bauerg@9256
   342
      thus ?thesis; by simp;
bauerg@9256
   343
    qed;
bauerg@9256
   344
    also; from x; have "... = p x"; by simp;
bauerg@9256
   345
    finally; show ?thesis; .;
bauerg@9256
   346
  qed;
bauerg@9256
   347
qed blast+; 
wenzelm@7917
   348
bauerg@9374
   349
end;