src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
author wenzelm
Sun Sep 17 22:19:02 2000 +0200 (2000-09-17)
changeset 10007 64bf7da1994a
parent 9906 5c027cca6262
child 10606 e3229a37d53f
permissions -rw-r--r--
isar-strip-terminators;
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
wenzelm@10007
     6
header {* Extending non-maximal functions *}
wenzelm@7917
     7
wenzelm@10007
     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$.
bauerg@9379
    16
$H$ is extended to the direct sum  $H' = H + \idt{lin}\ap x_0$, so for
bauerg@9379
    17
any $x\in H'$ the decomposition of $x = y + a \mult x$ 
bauerg@9379
    18
with $y\in H$ is unique. $h'$ is defined on $H'$ by  
bauerg@9379
    19
$h'\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$.
wenzelm@7917
    20
bauerg@9379
    21
Subsequently we show some properties of this extension $h'$ of $h$.
wenzelm@10007
    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}} 
wenzelm@10007
    35
\end{matharray} *}
wenzelm@7917
    36
wenzelm@7917
    37
lemma ex_xi: 
wenzelm@9503
    38
  "[| is_vectorspace F; !! u v. [| u \<in> F; v \<in> F |] ==> a u <= b v |]
wenzelm@10007
    39
  ==> \<exists>xi::real. \<forall>y \<in> F. a y <= xi \<and> xi <= b y" 
wenzelm@10007
    40
proof -
wenzelm@10007
    41
  assume vs: "is_vectorspace F"
wenzelm@10007
    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
wenzelm@10007
    46
  it is non-empty and has an upper bound. *}
wenzelm@7917
    47
wenzelm@10007
    48
  let ?S = "{a u :: real | u. u \<in> F}"
wenzelm@7917
    49
wenzelm@10007
    50
  have "\<exists>xi. isLub UNIV ?S xi"  
wenzelm@10007
    51
  proof (rule reals_complete)
wenzelm@7917
    52
  
wenzelm@10007
    53
    txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *}
wenzelm@7917
    54
wenzelm@10007
    55
    from vs have "a 0 \<in> ?S" by force
wenzelm@10007
    56
    thus "\<exists>X. X \<in> ?S" ..
wenzelm@7917
    57
wenzelm@10007
    58
    txt {* $b\ap \zero$ is an upper bound of $S$: *}
wenzelm@7917
    59
wenzelm@10007
    60
    show "\<exists>Y. isUb UNIV ?S Y" 
wenzelm@10007
    61
    proof 
wenzelm@10007
    62
      show "isUb UNIV ?S (b 0)"
wenzelm@10007
    63
      proof (intro isUbI setleI ballI)
wenzelm@10007
    64
        show "b 0 \<in> UNIV" ..
wenzelm@10007
    65
      next
wenzelm@7917
    66
wenzelm@10007
    67
        txt {* Every element $y\in S$ is less than $b\ap \zero$: *}
wenzelm@7917
    68
wenzelm@10007
    69
        fix y assume y: "y \<in> ?S" 
wenzelm@10007
    70
        from y have "\<exists>u \<in> F. y = a u" by fast
wenzelm@10007
    71
        thus "y <= b 0" 
wenzelm@10007
    72
        proof
wenzelm@10007
    73
          fix u assume "u \<in> F" 
wenzelm@10007
    74
          assume "y = a u"
wenzelm@10007
    75
          also have "a u <= b 0" by (rule r) (simp!)+
wenzelm@10007
    76
          finally show ?thesis .
wenzelm@10007
    77
        qed
wenzelm@10007
    78
      qed
wenzelm@10007
    79
    qed
wenzelm@10007
    80
  qed
wenzelm@7917
    81
wenzelm@10007
    82
  thus "\<exists>xi. \<forall>y \<in> F. a y <= xi \<and> xi <= b y" 
wenzelm@10007
    83
  proof (elim exE)
wenzelm@10007
    84
    fix xi assume "isLub UNIV ?S xi" 
wenzelm@10007
    85
    show ?thesis
wenzelm@10007
    86
    proof (intro exI conjI ballI) 
wenzelm@7917
    87
   
wenzelm@10007
    88
      txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *}
wenzelm@7917
    89
     
wenzelm@10007
    90
      fix y assume y: "y \<in> F"
wenzelm@10007
    91
      show "a y <= xi"    
wenzelm@10007
    92
      proof (rule isUbD)  
wenzelm@10007
    93
        show "isUb UNIV ?S xi" ..
wenzelm@10007
    94
      qed (force!)
wenzelm@10007
    95
    next
wenzelm@7917
    96
wenzelm@10007
    97
      txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *}
wenzelm@7917
    98
wenzelm@10007
    99
      fix y assume "y \<in> F"
wenzelm@10007
   100
      show "xi <= b y"  
wenzelm@10007
   101
      proof (intro isLub_le_isUb isUbI setleI)
wenzelm@10007
   102
        show "b y \<in> UNIV" ..
wenzelm@10007
   103
        show "\<forall>ya \<in> ?S. ya <= b y" 
wenzelm@10007
   104
        proof
wenzelm@10007
   105
          fix au assume au: "au \<in> ?S "
wenzelm@10007
   106
          hence "\<exists>u \<in> F. au = a u" by fast
wenzelm@10007
   107
          thus "au <= b y"
wenzelm@10007
   108
          proof
wenzelm@10007
   109
            fix u assume "u \<in> F" assume "au = a u"  
wenzelm@10007
   110
            also have "... <= b y" by (rule r)
wenzelm@10007
   111
            finally show ?thesis .
wenzelm@10007
   112
          qed
wenzelm@10007
   113
        qed
wenzelm@10007
   114
      qed 
wenzelm@10007
   115
    qed
wenzelm@10007
   116
  qed
wenzelm@10007
   117
qed
wenzelm@7917
   118
bauerg@9379
   119
text{* \medskip The function $h'$ is defined as a
bauerg@9379
   120
$h'\ap x = h\ap y + a\cdot \xi$ where $x = y + a\mult \xi$
wenzelm@10007
   121
is a linear extension of $h$ to $H'$. *}
wenzelm@7917
   122
bauerg@9374
   123
lemma h'_lf: 
wenzelm@9503
   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);
wenzelm@9503
   126
  H' == H + lin x0; is_subspace H E; is_linearform H h; x0 \<notin> H; 
wenzelm@9503
   127
  x0 \<in> E; x0 \<noteq> 0; is_vectorspace E |]
wenzelm@10007
   128
  ==> is_linearform H' h'"
wenzelm@10007
   129
proof -
bauerg@9374
   130
  assume h'_def: 
wenzelm@9503
   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" 
wenzelm@9503
   134
    and vs: "is_subspace H E" "is_linearform H h" "x0 \<notin> H"
wenzelm@10007
   135
      "x0 \<noteq> 0" "x0 \<in> E" "is_vectorspace E"
wenzelm@7917
   136
wenzelm@10007
   137
  have h': "is_vectorspace H'" 
wenzelm@10007
   138
  proof (unfold H'_def, rule vs_sum_vs)
wenzelm@10007
   139
    show "is_subspace (lin x0) E" ..
wenzelm@10007
   140
  qed 
wenzelm@7917
   141
wenzelm@10007
   142
  show ?thesis
wenzelm@10007
   143
  proof
wenzelm@10007
   144
    fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'" 
wenzelm@7917
   145
bauerg@9379
   146
    txt{* We now have to show that $h'$ is additive, i.~e.\
bauerg@9379
   147
    $h' \ap (x_1\plus x_2) = h'\ap x_1 + h'\ap x_2$
wenzelm@10007
   148
    for $x_1, x_2\in H$. *} 
wenzelm@7917
   149
wenzelm@10007
   150
    have x1x2: "x1 + x2 \<in> H'" 
wenzelm@10007
   151
      by (rule vs_add_closed, rule h') 
wenzelm@10007
   152
    from x1 
wenzelm@10007
   153
    have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0  \<and> y1 \<in> H" 
wenzelm@10007
   154
      by (unfold H'_def vs_sum_def lin_def) fast
wenzelm@10007
   155
    from x2 
wenzelm@10007
   156
    have ex_x2: "\<exists>y2 a2. x2 = y2 + a2 \<cdot> x0 \<and> y2 \<in> H" 
wenzelm@10007
   157
      by (unfold H'_def vs_sum_def lin_def) fast
wenzelm@10007
   158
    from x1x2 
wenzelm@10007
   159
    have ex_x1x2: "\<exists>y a. x1 + x2 = y + a \<cdot> x0 \<and> y \<in> H"
wenzelm@10007
   160
      by (unfold H'_def vs_sum_def lin_def) fast
wenzelm@7917
   161
wenzelm@10007
   162
    from ex_x1 ex_x2 ex_x1x2
wenzelm@10007
   163
    show "h' (x1 + x2) = h' x1 + h' x2"
wenzelm@10007
   164
    proof (elim exE conjE)
wenzelm@10007
   165
      fix y1 y2 y a1 a2 a
wenzelm@9503
   166
      assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
wenzelm@9503
   167
         and y2: "x2 = y2 + a2 \<cdot> x0"     and y2': "y2 \<in> H" 
wenzelm@10007
   168
         and y: "x1 + x2 = y + a \<cdot> x0"   and y':  "y  \<in> H" 
bauerg@9379
   169
      txt {* \label{decomp-H-use}*}
wenzelm@10007
   170
      have ya: "y1 + y2 = y \<and> a1 + a2 = a" 
bauerg@9379
   171
      proof (rule decomp_H')
wenzelm@10007
   172
        show "y1 + y2 + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" 
wenzelm@10007
   173
          by (simp! add: vs_add_mult_distrib2 [of E])
wenzelm@10007
   174
        show "y1 + y2 \<in> H" ..
wenzelm@10007
   175
      qed
wenzelm@7917
   176
wenzelm@10007
   177
      have "h' (x1 + x2) = h y + a * xi"
wenzelm@10007
   178
	by (rule h'_definite)
wenzelm@10007
   179
      also have "... = h (y1 + y2) + (a1 + a2) * xi" 
wenzelm@10007
   180
        by (simp add: ya)
wenzelm@10007
   181
      also from vs y1' y2' 
wenzelm@10007
   182
      have "... = h y1 + h y2 + a1 * xi + a2 * xi" 
wenzelm@7978
   183
	by (simp add: linearform_add [of H] 
wenzelm@10007
   184
                      real_add_mult_distrib)
wenzelm@10007
   185
      also have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)" 
wenzelm@10007
   186
        by simp
wenzelm@10007
   187
      also have "h y1 + a1 * xi = h' x1"
wenzelm@10007
   188
        by (rule h'_definite [symmetric])
wenzelm@10007
   189
      also have "h y2 + a2 * xi = h' x2" 
wenzelm@10007
   190
        by (rule h'_definite [symmetric])
wenzelm@10007
   191
      finally show ?thesis .
wenzelm@10007
   192
    qed
wenzelm@7917
   193
 
bauerg@9379
   194
    txt{* We further have to show that $h'$ is multiplicative, 
bauerg@9379
   195
    i.~e.\ $h'\ap (c \mult x_1) = c \cdot h'\ap x_1$
wenzelm@7978
   196
    for $x\in H$ and $c\in \bbbR$. 
wenzelm@10007
   197
    *} 
wenzelm@7917
   198
wenzelm@10007
   199
  next  
wenzelm@10007
   200
    fix c x1 assume x1: "x1 \<in> H'"    
wenzelm@10007
   201
    have ax1: "c \<cdot> x1 \<in> H'"
wenzelm@10007
   202
      by (rule vs_mult_closed, rule h')
wenzelm@10007
   203
    from x1 
wenzelm@10007
   204
    have ex_x: "!! x. x\<in> H' ==> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
wenzelm@10007
   205
      by (unfold H'_def vs_sum_def lin_def) fast
wenzelm@7917
   206
wenzelm@10007
   207
    from x1 have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H"
wenzelm@10007
   208
      by (unfold H'_def vs_sum_def lin_def) fast
wenzelm@10007
   209
    with ex_x [of "c \<cdot> x1", OF ax1]
wenzelm@10007
   210
    show "h' (c \<cdot> x1) = c * (h' x1)"  
wenzelm@10007
   211
    proof (elim exE conjE)
wenzelm@10007
   212
      fix y1 y a1 a 
wenzelm@9503
   213
      assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
wenzelm@10007
   214
        and y: "c \<cdot> x1 = y  + a \<cdot> x0"    and y': "y \<in> H" 
wenzelm@7917
   215
wenzelm@10007
   216
      have ya: "c \<cdot> y1 = y \<and> c * a1 = a" 
wenzelm@10007
   217
      proof (rule decomp_H') 
wenzelm@10007
   218
	show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" 
wenzelm@10007
   219
          by (simp! add: vs_add_mult_distrib1)
wenzelm@10007
   220
        show "c \<cdot> y1 \<in> H" ..
wenzelm@10007
   221
      qed
wenzelm@7917
   222
wenzelm@10007
   223
      have "h' (c \<cdot> x1) = h y + a * xi" 
wenzelm@10007
   224
	by (rule h'_definite)
wenzelm@10007
   225
      also have "... = h (c \<cdot> y1) + (c * a1) * xi"
wenzelm@10007
   226
        by (simp add: ya)
wenzelm@10007
   227
      also from vs y1' have "... = c * h y1 + c * a1 * xi" 
wenzelm@10007
   228
	by (simp add: linearform_mult [of H])
wenzelm@10007
   229
      also from vs y1' have "... = c * (h y1 + a1 * xi)" 
wenzelm@10007
   230
	by (simp add: real_add_mult_distrib2 real_mult_assoc)
wenzelm@10007
   231
      also have "h y1 + a1 * xi = h' x1" 
wenzelm@10007
   232
        by (rule h'_definite [symmetric])
wenzelm@10007
   233
      finally show ?thesis .
wenzelm@10007
   234
    qed
wenzelm@10007
   235
  qed
wenzelm@10007
   236
qed
wenzelm@7917
   237
bauerg@9379
   238
text{* \medskip The linear extension $h'$ of $h$
wenzelm@10007
   239
is bounded by the seminorm $p$. *}
wenzelm@7917
   240
bauerg@9374
   241
lemma h'_norm_pres:
wenzelm@9503
   242
  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
bauerg@9379
   243
                 in h y + a * xi);
wenzelm@9503
   244
  H' == H + lin x0; x0 \<notin> H; x0 \<in> E; x0 \<noteq> 0; is_vectorspace E; 
bauerg@9379
   245
  is_subspace H E; is_seminorm E p; is_linearform H h; 
wenzelm@9503
   246
  \<forall>y \<in> H. h y <= p y; 
wenzelm@9503
   247
  \<forall>y \<in> H. - p (y + x0) - h y <= xi \<and> xi <= p (y + x0) - h y |]
wenzelm@10007
   248
   ==> \<forall>x \<in> H'. h' x <= p x" 
wenzelm@10007
   249
proof 
bauerg@9374
   250
  assume h'_def: 
wenzelm@9503
   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" 
wenzelm@9503
   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" 
wenzelm@10007
   256
    and a: "\<forall>y \<in> H. h y <= p y"
wenzelm@10007
   257
  presume a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya <= xi"
wenzelm@10007
   258
  presume a2: "\<forall>ya \<in> H. xi <= p (ya + x0) - h ya"
wenzelm@10007
   259
  fix x assume "x \<in> H'" 
wenzelm@7917
   260
  have ex_x: 
wenzelm@10007
   261
    "!! x. x \<in> H' ==> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
wenzelm@10007
   262
    by (unfold H'_def vs_sum_def lin_def) fast
wenzelm@10007
   263
  have "\<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
wenzelm@10007
   264
    by (rule ex_x)
wenzelm@10007
   265
  thus "h' x <= p x"
wenzelm@10007
   266
  proof (elim exE conjE)
wenzelm@10007
   267
    fix y a assume x: "x = y + a \<cdot> x0" and y: "y \<in> H"
wenzelm@10007
   268
    have "h' x = h y + a * xi"
wenzelm@10007
   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)$ 
wenzelm@10007
   273
    by case analysis on $a$. *}
wenzelm@7917
   274
wenzelm@10007
   275
    also have "... <= p (y + a \<cdot> x0)"
wenzelm@10007
   276
    proof (rule linorder_cases)
wenzelm@7917
   277
wenzelm@10007
   278
      assume z: "a = #0" 
wenzelm@10007
   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}$ 
wenzelm@10007
   282
    taken as $y/a$: *}
wenzelm@7917
   283
wenzelm@10007
   284
    next
wenzelm@10007
   285
      assume lz: "a < #0" hence nz: "a \<noteq> #0" by simp
wenzelm@10007
   286
      from a1 
wenzelm@10007
   287
      have "- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y) <= xi"
wenzelm@10007
   288
        by (rule bspec) (simp!)
wenzelm@7917
   289
wenzelm@7978
   290
      txt {* The thesis for this case now follows by a short  
wenzelm@10007
   291
      calculation. *}      
wenzelm@10007
   292
      hence "a * xi <= a * (- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y))"
wenzelm@10007
   293
        by (rule real_mult_less_le_anti [OF lz])
wenzelm@10007
   294
      also 
wenzelm@10007
   295
      have "... = - a * (p (rinv a \<cdot> y + x0)) - a * (h (rinv a \<cdot> y))"
wenzelm@10007
   296
        by (rule real_mult_diff_distrib)
wenzelm@10007
   297
      also from lz vs y 
wenzelm@10007
   298
      have "- a * (p (rinv a \<cdot> y + x0)) = p (a \<cdot> (rinv a \<cdot> y + x0))"
wenzelm@10007
   299
        by (simp add: seminorm_abs_homogenous abs_minus_eqI2)
wenzelm@10007
   300
      also from nz vs y have "... = p (y + a \<cdot> x0)"
wenzelm@10007
   301
        by (simp add: vs_add_mult_distrib1)
wenzelm@10007
   302
      also from nz vs y have "a * (h (rinv a \<cdot> y)) =  h y"
wenzelm@10007
   303
        by (simp add: linearform_mult [symmetric])
wenzelm@10007
   304
      finally have "a * xi <= p (y + a \<cdot> x0) - h y" .
wenzelm@7917
   305
wenzelm@10007
   306
      hence "h y + a * xi <= h y + p (y + a \<cdot> x0) - h y"
wenzelm@10007
   307
        by (simp add: real_add_left_cancel_le)
wenzelm@10007
   308
      thus ?thesis by simp
wenzelm@7917
   309
wenzelm@7978
   310
      txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$ 
wenzelm@10007
   311
      taken as $y/a$: *}
wenzelm@7978
   312
wenzelm@10007
   313
    next 
wenzelm@10007
   314
      assume gz: "#0 < a" hence nz: "a \<noteq> #0" by simp
wenzelm@10007
   315
      from a2 have "xi <= p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y)"
wenzelm@10007
   316
        by (rule bspec) (simp!)
wenzelm@7917
   317
wenzelm@7978
   318
      txt {* The thesis for this case follows by a short
wenzelm@10007
   319
      calculation: *}
wenzelm@7917
   320
wenzelm@10007
   321
      with gz 
wenzelm@10007
   322
      have "a * xi <= a * (p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y))"
wenzelm@10007
   323
        by (rule real_mult_less_le_mono)
wenzelm@10007
   324
      also have "... = a * p (rinv a \<cdot> y + x0) - a * h (rinv a \<cdot> y)"
wenzelm@10007
   325
        by (rule real_mult_diff_distrib2) 
wenzelm@10007
   326
      also from gz vs y 
wenzelm@10007
   327
      have "a * p (rinv a \<cdot> y + x0) = p (a \<cdot> (rinv a \<cdot> y + x0))"
wenzelm@10007
   328
        by (simp add: seminorm_abs_homogenous abs_eqI2)
wenzelm@10007
   329
      also from nz vs y have "... = p (y + a \<cdot> x0)"
wenzelm@10007
   330
        by (simp add: vs_add_mult_distrib1)
wenzelm@10007
   331
      also from nz vs y have "a * h (rinv a \<cdot> y) = h y"
wenzelm@10007
   332
        by (simp add: linearform_mult [symmetric]) 
wenzelm@10007
   333
      finally have "a * xi <= p (y + a \<cdot> x0) - h y" .
wenzelm@7917
   334
 
wenzelm@10007
   335
      hence "h y + a * xi <= h y + (p (y + a \<cdot> x0) - h y)"
wenzelm@10007
   336
        by (simp add: real_add_left_cancel_le)
wenzelm@10007
   337
      thus ?thesis by simp
wenzelm@10007
   338
    qed
wenzelm@10007
   339
    also from x have "... = p x" by simp
wenzelm@10007
   340
    finally show ?thesis .
wenzelm@10007
   341
  qed
wenzelm@10007
   342
qed blast+ 
wenzelm@7917
   343
wenzelm@10007
   344
end