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