src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
author wenzelm
Fri Oct 22 20:14:31 1999 +0200 (1999-10-22)
changeset 7917 5e5b9813cce7
child 7927 b50446a33c16
permissions -rw-r--r--
HahnBanach update by Gertrud Bauer;
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@7917
     6
header {* Extending a non-ma\-xi\-mal function *};
wenzelm@7917
     7
wenzelm@7917
     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@7917
    12
quasinorm $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@7917
    14
superspace of $F$ and a linearform $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@7917
    19
$h_0 x = h y + a \cdot \xi$ for some $\xi$.
wenzelm@7917
    20
wenzelm@7917
    21
Subsequently we show some properties of this extension $h_0$ of $h$.
wenzelm@7917
    22
*}; 
wenzelm@7917
    23
wenzelm@7917
    24
wenzelm@7917
    25
text {* This lemma will be used to show the existence of a linear 
wenzelm@7917
    26
extension of $f$. It is a conclusion of the completenesss of the 
wenzelm@7917
    27
reals. To show 
wenzelm@7917
    28
\begin{matharray}{l}
wenzelm@7917
    29
\exists \xi. \ap (\forall y\in F.\ap a\ap y \leq \xi) \land (\forall y\in F.\ap xi \leq b\ap y)
wenzelm@7917
    30
\end{matharray}
wenzelm@7917
    31
it suffices to show that 
wenzelm@7917
    32
\begin{matharray}{l}
wenzelm@7917
    33
\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v.
wenzelm@7917
    34
\end{matharray}
wenzelm@7917
    35
*};
wenzelm@7917
    36
wenzelm@7917
    37
lemma ex_xi: 
wenzelm@7917
    38
  "[| is_vectorspace F; !! u v. [| u:F; v:F |] ==> a u <= b v |]
wenzelm@7917
    39
  ==> EX (xi::real). (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)"; 
wenzelm@7917
    40
proof -;
wenzelm@7917
    41
  assume vs: "is_vectorspace F";
wenzelm@7917
    42
  assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
wenzelm@7917
    43
wenzelm@7917
    44
  txt {* From the completeness of the reals follows:
wenzelm@7917
    45
  The set $S = \{a\ap u.\ap u\in F\}$ has a supremum, if
wenzelm@7917
    46
  it is non-empty and if it has an upperbound. *};
wenzelm@7917
    47
wenzelm@7917
    48
  let ?S = "{s::real. EX u:F. s = a u}";
wenzelm@7917
    49
wenzelm@7917
    50
  have "EX xi. isLub UNIV ?S xi";  
wenzelm@7917
    51
  proof (rule reals_complete);
wenzelm@7917
    52
  
wenzelm@7917
    53
    txt {* The set $S$ is non-empty, since $a\ap\zero \in S$ *};
wenzelm@7917
    54
wenzelm@7917
    55
    from vs; have "a <0> : ?S"; by force;
wenzelm@7917
    56
    thus "EX X. X : ?S"; ..;
wenzelm@7917
    57
wenzelm@7917
    58
    txt {* $b\ap \zero$ is an upperboud of $S$. *};
wenzelm@7917
    59
wenzelm@7917
    60
    show "EX Y. isUb UNIV ?S Y"; 
wenzelm@7917
    61
    proof; 
wenzelm@7917
    62
      show "isUb UNIV ?S (b <0>)";
wenzelm@7917
    63
      proof (intro isUbI setleI ballI);
wenzelm@7917
    64
wenzelm@7917
    65
        txt {* Every element $y\in S$ is less than $b\ap \zero$ *};  
wenzelm@7917
    66
wenzelm@7917
    67
        fix y; assume y: "y : ?S"; 
wenzelm@7917
    68
        from y; have "EX u:F. y = a u"; ..;
wenzelm@7917
    69
        thus "y <= b <0>"; 
wenzelm@7917
    70
        proof;
wenzelm@7917
    71
          fix u; assume "u:F"; assume "y = a u";
wenzelm@7917
    72
          also; have "a u <= b <0>"; by (rule r) (simp!)+;
wenzelm@7917
    73
          finally; show ?thesis; .;
wenzelm@7917
    74
        qed;
wenzelm@7917
    75
      next;
wenzelm@7917
    76
        show "b <0> : UNIV"; by simp;
wenzelm@7917
    77
      qed;
wenzelm@7917
    78
    qed;
wenzelm@7917
    79
  qed;
wenzelm@7917
    80
wenzelm@7917
    81
  thus "EX xi. (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)"; 
wenzelm@7917
    82
  proof (elim exE);
wenzelm@7917
    83
    fix xi; assume "isLub UNIV ?S xi"; 
wenzelm@7917
    84
    show ?thesis;
wenzelm@7917
    85
    proof (intro exI conjI ballI); 
wenzelm@7917
    86
   
wenzelm@7917
    87
      txt {* For all $y\in F$ is $a\ap y \leq \xi$. *};
wenzelm@7917
    88
     
wenzelm@7917
    89
      fix y; assume y: "y:F";
wenzelm@7917
    90
      show "a y <= xi";    
wenzelm@7917
    91
      proof (rule isUbD);  
wenzelm@7917
    92
        show "isUb UNIV ?S xi"; ..;
wenzelm@7917
    93
      qed (force!);
wenzelm@7917
    94
    next;
wenzelm@7917
    95
wenzelm@7917
    96
      txt {* For all $y\in F$ is $\xi\leq b\ap y$. *};
wenzelm@7917
    97
wenzelm@7917
    98
      fix y; assume "y:F";
wenzelm@7917
    99
      show "xi <= b y";  
wenzelm@7917
   100
      proof (intro isLub_le_isUb isUbI setleI);
wenzelm@7917
   101
        show "b y : UNIV"; by simp;
wenzelm@7917
   102
        show "ALL ya : ?S. ya <= b y"; 
wenzelm@7917
   103
        proof;
wenzelm@7917
   104
          fix au; assume au: "au : ?S ";
wenzelm@7917
   105
          hence "EX u:F. au = a u"; ..;
wenzelm@7917
   106
          thus "au <= b y";
wenzelm@7917
   107
          proof;
wenzelm@7917
   108
            fix u; assume "u:F"; assume "au = a u";  
wenzelm@7917
   109
            also; have "... <= b y"; by (rule r);
wenzelm@7917
   110
            finally; show ?thesis; .;
wenzelm@7917
   111
          qed;
wenzelm@7917
   112
        qed;
wenzelm@7917
   113
      qed; 
wenzelm@7917
   114
    qed;
wenzelm@7917
   115
  qed;
wenzelm@7917
   116
qed;
wenzelm@7917
   117
wenzelm@7917
   118
text{* The function $h_0$ is defined as a linear extension of $h$
wenzelm@7917
   119
to $H_0$. $h_0$ is linear. *};
wenzelm@7917
   120
wenzelm@7917
   121
lemma h0_lf: 
wenzelm@7917
   122
  "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
wenzelm@7917
   123
                in h y + a * xi);
wenzelm@7917
   124
  H0 = H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; 
wenzelm@7917
   125
  x0 : E; x0 ~= <0>; is_vectorspace E |]
wenzelm@7917
   126
  ==> is_linearform H0 h0";
wenzelm@7917
   127
proof -;
wenzelm@7917
   128
  assume h0_def: 
wenzelm@7917
   129
    "h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
wenzelm@7917
   130
               in h y + a * xi)"
wenzelm@7917
   131
      and H0_def: "H0 = H + lin x0" 
wenzelm@7917
   132
      and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
wenzelm@7917
   133
        "x0 ~= <0>" "x0 : E" "is_vectorspace E";
wenzelm@7917
   134
wenzelm@7917
   135
  have h0: "is_vectorspace H0"; 
wenzelm@7917
   136
  proof (simp only: H0_def, rule vs_sum_vs);
wenzelm@7917
   137
    show "is_subspace (lin x0) E"; ..;
wenzelm@7917
   138
  qed; 
wenzelm@7917
   139
wenzelm@7917
   140
  show ?thesis;
wenzelm@7917
   141
  proof;
wenzelm@7917
   142
    fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0"; 
wenzelm@7917
   143
wenzelm@7917
   144
    txt{* We now have to show that $h_0$ is linear 
wenzelm@7917
   145
    w.~r.~t.~addition, i.~e.~
wenzelm@7917
   146
    $h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
wenzelm@7917
   147
    for $x_1, x_2\in H$. *}; 
wenzelm@7917
   148
wenzelm@7917
   149
    have x1x2: "x1 + x2 : H0"; 
wenzelm@7917
   150
      by (rule vs_add_closed, rule h0); 
wenzelm@7917
   151
    from x1; 
wenzelm@7917
   152
    have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0  & y1 : H"; 
wenzelm@7917
   153
      by (simp add: H0_def vs_sum_def lin_def) blast;
wenzelm@7917
   154
    from x2; 
wenzelm@7917
   155
    have ex_x2: "EX y2 a2. x2 = y2 + a2 <*> x0 & y2 : H"; 
wenzelm@7917
   156
      by (simp add: H0_def vs_sum_def lin_def) blast;
wenzelm@7917
   157
    from x1x2; 
wenzelm@7917
   158
    have ex_x1x2: "EX y a. x1 + x2 = y + a <*> x0 & y : H";
wenzelm@7917
   159
      by (simp add: H0_def vs_sum_def lin_def) force;
wenzelm@7917
   160
wenzelm@7917
   161
    from ex_x1 ex_x2 ex_x1x2;
wenzelm@7917
   162
    show "h0 (x1 + x2) = h0 x1 + h0 x2";
wenzelm@7917
   163
    proof (elim exE conjE);
wenzelm@7917
   164
      fix y1 y2 y a1 a2 a;
wenzelm@7917
   165
      assume y1: "x1 = y1 + a1 <*> x0"     and y1': "y1 : H"
wenzelm@7917
   166
         and y2: "x2 = y2 + a2 <*> x0"     and y2': "y2 : H" 
wenzelm@7917
   167
         and y: "x1 + x2 = y + a <*> x0"   and y':  "y  : H"; 
wenzelm@7917
   168
wenzelm@7917
   169
      have ya: "y1 + y2 = y & a1 + a2 = a"; 
wenzelm@7917
   170
      proof (rule decomp_H0); 
wenzelm@7917
   171
        show "y1 + y2 + (a1 + a2) <*> x0 = y + a <*> x0"; 
wenzelm@7917
   172
          by (simp! add: vs_add_mult_distrib2 [of E]);
wenzelm@7917
   173
        show "y1 + y2 : H"; ..;
wenzelm@7917
   174
      qed;
wenzelm@7917
   175
wenzelm@7917
   176
      have "h0 (x1 + x2) = h y + a * xi";
wenzelm@7917
   177
	by (rule h0_definite);
wenzelm@7917
   178
      also; have "... = h (y1 + y2) + (a1 + a2) * xi"; 
wenzelm@7917
   179
        by (simp add: ya);
wenzelm@7917
   180
      also; from vs y1' y2'; 
wenzelm@7917
   181
      have "... = h y1 + h y2 + a1 * xi + a2 * xi"; 
wenzelm@7917
   182
	by (simp add: linearform_add_linear [of H] 
wenzelm@7917
   183
                      real_add_mult_distrib);
wenzelm@7917
   184
      also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; 
wenzelm@7917
   185
        by simp;
wenzelm@7917
   186
      also; have "h y1 + a1 * xi = h0 x1"; 
wenzelm@7917
   187
        by (rule h0_definite [RS sym]);
wenzelm@7917
   188
      also; have "h y2 + a2 * xi = h0 x2"; 
wenzelm@7917
   189
        by (rule h0_definite [RS sym]);
wenzelm@7917
   190
      finally; show ?thesis; .;
wenzelm@7917
   191
    qed;
wenzelm@7917
   192
 
wenzelm@7917
   193
    txt{* We further have to show that $h_0$ is linear 
wenzelm@7917
   194
    w.~r.~t.~scalar multiplication, 
wenzelm@7917
   195
    i.~e.~ $c\in real$ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
wenzelm@7917
   196
    for $x\in H$ and real $c$. 
wenzelm@7917
   197
    *}; 
wenzelm@7917
   198
wenzelm@7917
   199
  next;  
wenzelm@7917
   200
    fix c x1; assume x1: "x1 : H0";    
wenzelm@7917
   201
    have ax1: "c <*> x1 : H0";
wenzelm@7917
   202
      by (rule vs_mult_closed, rule h0);
wenzelm@7917
   203
    from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
wenzelm@7917
   204
      by (simp add: H0_def vs_sum_def lin_def) fast;
wenzelm@7917
   205
    from x1; have ex_x: "!! x. x: H0 
wenzelm@7917
   206
                        ==> EX y a. x = y + a <*> x0 & y : H";
wenzelm@7917
   207
      by (simp add: H0_def vs_sum_def lin_def) fast;
wenzelm@7917
   208
    note ex_ax1 = ex_x [of "c <*> x1", OF ax1];
wenzelm@7917
   209
wenzelm@7917
   210
    with ex_x1; show "h0 (c <*> x1) = c * (h0 x1)";  
wenzelm@7917
   211
    proof (elim exE conjE);
wenzelm@7917
   212
      fix y1 y a1 a; 
wenzelm@7917
   213
      assume y1: "x1 = y1 + a1 <*> x0"       and y1': "y1 : H"
wenzelm@7917
   214
        and y: "c <*> x1 = y  + a  <*> x0"   and y':  "y  : H"; 
wenzelm@7917
   215
wenzelm@7917
   216
      have ya: "c <*> y1 = y & c * a1 = a"; 
wenzelm@7917
   217
      proof (rule decomp_H0); 
wenzelm@7917
   218
	show "c <*> y1 + (c * a1) <*> x0 = y + a <*> x0"; 
wenzelm@7917
   219
          by (simp! add: add: vs_add_mult_distrib1);
wenzelm@7917
   220
        show "c <*> y1 : H"; ..;
wenzelm@7917
   221
      qed;
wenzelm@7917
   222
wenzelm@7917
   223
      have "h0 (c <*> x1) = h y + a * xi"; 
wenzelm@7917
   224
	by (rule h0_definite);
wenzelm@7917
   225
      also; have "... = h (c <*> y1) + (c * a1) * xi";
wenzelm@7917
   226
        by (simp add: ya);
wenzelm@7917
   227
      also; from vs y1'; have "... = c * h y1 + c * a1 * xi"; 
wenzelm@7917
   228
	by (simp add: linearform_mult_linear [of H]);
wenzelm@7917
   229
      also; from vs y1'; have "... = c * (h y1 + a1 * xi)"; 
wenzelm@7917
   230
	by (simp add: real_add_mult_distrib2 real_mult_assoc);
wenzelm@7917
   231
      also; have "h y1 + a1 * xi = h0 x1"; 
wenzelm@7917
   232
        by (rule h0_definite [RS sym]);
wenzelm@7917
   233
      finally; show ?thesis; .;
wenzelm@7917
   234
    qed;
wenzelm@7917
   235
  qed;
wenzelm@7917
   236
qed;
wenzelm@7917
   237
wenzelm@7917
   238
text{* $h_0$ is bounded by the quasinorm $p$. *};
wenzelm@7917
   239
wenzelm@7917
   240
lemma h0_norm_pres:
wenzelm@7917
   241
  "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
wenzelm@7917
   242
                in h y + a * xi);
wenzelm@7917
   243
  H0 = H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E; 
wenzelm@7917
   244
  is_subspace H E; is_quasinorm E p; is_linearform H h; 
wenzelm@7917
   245
  ALL y:H. h y <= p y; (ALL y:H. - p (y + x0) - h y <= xi) 
wenzelm@7917
   246
  & (ALL y:H. xi <= p (y + x0) - h y) |]
wenzelm@7917
   247
   ==> ALL x:H0. h0 x <= p x"; 
wenzelm@7917
   248
proof; 
wenzelm@7917
   249
  assume h0_def: 
wenzelm@7917
   250
    "h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
wenzelm@7917
   251
               in (h y) + a * xi)"
wenzelm@7917
   252
    and H0_def: "H0 = H + lin x0" 
wenzelm@7917
   253
    and vs: "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E" 
wenzelm@7917
   254
            "is_subspace H E" "is_quasinorm E p" "is_linearform H h" 
wenzelm@7917
   255
    and a:      " ALL y:H. h y <= p y";
wenzelm@7917
   256
  presume a1: "ALL y:H. - p (y + x0) - h y <= xi";
wenzelm@7917
   257
  presume a2: "ALL y:H. xi <= p (y + x0) - h y";
wenzelm@7917
   258
  fix x; assume "x : H0"; 
wenzelm@7917
   259
  have ex_x: 
wenzelm@7917
   260
    "!! x. x : H0 ==> EX y a. x = y + a <*> x0 & y : H";
wenzelm@7917
   261
    by (simp add: H0_def vs_sum_def lin_def) fast;
wenzelm@7917
   262
  have "EX y a. x = y + a <*> x0 & y : H";
wenzelm@7917
   263
    by (rule ex_x);
wenzelm@7917
   264
  thus "h0 x <= p x";
wenzelm@7917
   265
  proof (elim exE conjE);
wenzelm@7917
   266
    fix y a; assume x: "x = y + a <*> x0" and y: "y : H";
wenzelm@7917
   267
    have "h0 x = h y + a * xi";
wenzelm@7917
   268
      by (rule h0_definite);
wenzelm@7917
   269
wenzelm@7917
   270
    txt{* Now we show  
wenzelm@7917
   271
    $h\ap y + a * xi\leq  p\ap (y\plus a \mult x_0)$ 
wenzelm@7917
   272
    by case analysis on $a$. *};
wenzelm@7917
   273
wenzelm@7917
   274
    also; have "... <= p (y + a <*> x0)";
wenzelm@7917
   275
    proof (rule linorder_linear_split); 
wenzelm@7917
   276
wenzelm@7917
   277
      assume z: "a = 0r"; 
wenzelm@7917
   278
      with vs y a; show ?thesis; by simp;
wenzelm@7917
   279
wenzelm@7917
   280
    txt {* In the case $a < 0$ we use $a_1$ with $y$ taken as
wenzelm@7917
   281
    $\frac{y}{a}$. *};
wenzelm@7917
   282
wenzelm@7917
   283
    next;
wenzelm@7917
   284
      assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
wenzelm@7917
   285
      from a1; 
wenzelm@7917
   286
      have "- p (rinv a <*> y + x0) - h (rinv a <*> y) <= xi";
wenzelm@7917
   287
        by (rule bspec)(simp!);
wenzelm@7917
   288
 
wenzelm@7917
   289
      txt {* The thesis now follows by a short calculation. *};      
wenzelm@7917
   290
wenzelm@7917
   291
      hence "a * xi 
wenzelm@7917
   292
            <= a * (- p (rinv a <*> y + x0) - h (rinv a <*> y))";
wenzelm@7917
   293
        by (rule real_mult_less_le_anti [OF lz]);
wenzelm@7917
   294
      also; have "... = - a * (p (rinv a <*> y + x0)) 
wenzelm@7917
   295
                        - a * (h (rinv a <*> y))";
wenzelm@7917
   296
        by (rule real_mult_diff_distrib);
wenzelm@7917
   297
      also; from lz vs y; have "- a * (p (rinv a <*> y + x0)) 
wenzelm@7917
   298
                               = p (a <*> (rinv a <*> y + x0))";
wenzelm@7917
   299
        by (simp add: quasinorm_mult_distrib rabs_minus_eqI2);
wenzelm@7917
   300
      also; from nz vs y; have "... = p (y + a <*> x0)";
wenzelm@7917
   301
        by (simp add: vs_add_mult_distrib1);
wenzelm@7917
   302
      also; from nz vs y; have "a * (h (rinv a <*> y)) =  h y";
wenzelm@7917
   303
        by (simp add: linearform_mult_linear [RS sym]);
wenzelm@7917
   304
      finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
wenzelm@7917
   305
wenzelm@7917
   306
      hence "h y + a * xi <= h y + p (y + a <*> x0) - h y";
wenzelm@7917
   307
        by (simp add: real_add_left_cancel_le);
wenzelm@7917
   308
      thus ?thesis; by simp;
wenzelm@7917
   309
wenzelm@7917
   310
      txt {* In the case $a > 0$ we use $a_2$ with $y$ taken
wenzelm@7917
   311
      as $\frac{y}{a}$. *};
wenzelm@7917
   312
    next; 
wenzelm@7917
   313
      assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
wenzelm@7917
   314
      have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
wenzelm@7917
   315
        by (rule bspec [OF a2]) (simp!);
wenzelm@7917
   316
wenzelm@7917
   317
      txt {* The thesis follows by a short calculation. *};
wenzelm@7917
   318
wenzelm@7917
   319
      with gz; have "a * xi 
wenzelm@7917
   320
            <= a * (p (rinv a <*> y + x0) - h (rinv a <*> y))";
wenzelm@7917
   321
        by (rule real_mult_less_le_mono);
wenzelm@7917
   322
      also; have "... = a * p (rinv a <*> y + x0) 
wenzelm@7917
   323
                        - a * h (rinv a <*> y)";
wenzelm@7917
   324
        by (rule real_mult_diff_distrib2); 
wenzelm@7917
   325
      also; from gz vs y; 
wenzelm@7917
   326
      have "a * p (rinv a <*> y + x0) 
wenzelm@7917
   327
           = p (a <*> (rinv a <*> y + x0))";
wenzelm@7917
   328
        by (simp add: quasinorm_mult_distrib rabs_eqI2);
wenzelm@7917
   329
      also; from nz vs y; 
wenzelm@7917
   330
      have "... = p (y + a <*> x0)";
wenzelm@7917
   331
        by (simp add: vs_add_mult_distrib1);
wenzelm@7917
   332
      also; from nz vs y; have "a * h (rinv a <*> y) = h y";
wenzelm@7917
   333
        by (simp add: linearform_mult_linear [RS sym]); 
wenzelm@7917
   334
      finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
wenzelm@7917
   335
 
wenzelm@7917
   336
      hence "h y + a * xi <= h y + (p (y + a <*> x0) - h y)";
wenzelm@7917
   337
        by (simp add: real_add_left_cancel_le);
wenzelm@7917
   338
      thus ?thesis; by simp;
wenzelm@7917
   339
    qed;
wenzelm@7917
   340
    also; from x; have "... = p x"; by simp;
wenzelm@7917
   341
    finally; show ?thesis; .;
wenzelm@7917
   342
  qed;
wenzelm@7917
   343
qed blast+; 
wenzelm@7917
   344
wenzelm@7917
   345
wenzelm@7917
   346
end;