src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
author wenzelm
Tue, 15 Jul 2008 19:39:37 +0200
changeset 27612 d3eb431db035
parent 27611 2c01c0bdb385
child 29234 60f7fb56f8cd
permissions -rw-r--r--
modernized specifications and proofs; tuned document;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     3
    Author:     Gertrud Bauer, TU Munich
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     4
*)
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     5
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
     6
header {* Extending non-maximal functions *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     7
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
     8
theory HahnBanachExtLemmas
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
     9
imports FunctionNorm
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    10
begin
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    11
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    12
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    13
  In this section the following context is presumed.  Let @{text E} be
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    14
  a real vector space with a seminorm @{text q} on @{text E}. @{text
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    15
  F} is a subspace of @{text E} and @{text f} a linear function on
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    16
  @{text F}. We consider a subspace @{text H} of @{text E} that is a
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    17
  superspace of @{text F} and a linear form @{text h} on @{text
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    18
  H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    19
  an element in @{text "E - H"}.  @{text H} is extended to the direct
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    20
  sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    21
  the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    22
  unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    23
  a \<cdot> \<xi>"} for a certain @{text \<xi>}.
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    24
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    25
  Subsequently we show some properties of this extension @{text h'} of
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    26
  @{text h}.
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    27
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    28
  \medskip This lemma will be used to show the existence of a linear
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    29
  extension of @{text f} (see page \pageref{ex-xi-use}). It is a
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    30
  consequence of the completeness of @{text \<real>}. To show
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    31
  \begin{center}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    32
  \begin{tabular}{l}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    33
  @{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    34
  \end{tabular}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    35
  \end{center}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    36
  \noindent it suffices to show that
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    37
  \begin{center}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    38
  \begin{tabular}{l}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    39
  @{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    40
  \end{tabular}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    41
  \end{center}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    42
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    43
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    44
lemma ex_xi:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
    45
  assumes "vectorspace F"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    46
  assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    47
  shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
    48
proof -
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
    49
  interpret vectorspace [F] by fact
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    50
  txt {* From the completeness of the reals follows:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    51
    The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    52
    non-empty and has an upper bound. *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    53
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    54
  let ?S = "{a u | u. u \<in> F}"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    55
  have "\<exists>xi. lub ?S xi"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    56
  proof (rule real_complete)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    57
    have "a 0 \<in> ?S" by blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    58
    then show "\<exists>X. X \<in> ?S" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    59
    have "\<forall>y \<in> ?S. y \<le> b 0"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    60
    proof
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    61
      fix y assume y: "y \<in> ?S"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    62
      then obtain u where u: "u \<in> F" and y: "y = a u" by blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    63
      from u and zero have "a u \<le> b 0" by (rule r)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    64
      with y show "y \<le> b 0" by (simp only:)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
    65
    qed
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    66
    then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
    67
  qed
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    68
  then obtain xi where xi: "lub ?S xi" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    69
  {
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    70
    fix y assume "y \<in> F"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    71
    then have "a y \<in> ?S" by blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    72
    with xi have "a y \<le> xi" by (rule lub.upper)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    73
  } moreover {
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    74
    fix y assume y: "y \<in> F"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    75
    from xi have "xi \<le> b y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    76
    proof (rule lub.least)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    77
      fix au assume "au \<in> ?S"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    78
      then obtain u where u: "u \<in> F" and au: "au = a u" by blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    79
      from u y have "a u \<le> b y" by (rule r)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    80
      with au show "au \<le> b y" by (simp only:)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
    81
    qed
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    82
  } ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
    83
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    84
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    85
text {*
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    86
  \medskip The function @{text h'} is defined as a @{text "h' x = h y
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    87
  + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    88
  @{text h} to @{text H'}.
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    89
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    90
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    91
lemma h'_lf:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    92
  assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    93
      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    94
    and H'_def: "H' \<equiv> H + lin x0"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    95
    and HE: "H \<unlhd> E"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
    96
  assumes "linearform H h"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    97
  assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
    98
  assumes E: "vectorspace E"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    99
  shows "linearform H' h'"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   100
proof -
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   101
  interpret linearform [H h] by fact
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   102
  interpret vectorspace [E] by fact
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   103
  show ?thesis
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   104
  proof
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   105
    note E = `vectorspace E`
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   106
    have H': "vectorspace H'"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   107
    proof (unfold H'_def)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   108
      from `x0 \<in> E`
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   109
      have "lin x0 \<unlhd> E" ..
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   110
      with HE show "vectorspace (H + lin x0)" using E ..
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   111
    qed
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   112
    {
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   113
      fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   114
      show "h' (x1 + x2) = h' x1 + h' x2"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   115
      proof -
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   116
	from H' x1 x2 have "x1 + x2 \<in> H'"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   117
          by (rule vectorspace.add_closed)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   118
	with x1 x2 obtain y y1 y2 a a1 a2 where
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   119
          x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   120
          and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   121
          and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   122
          unfolding H'_def sum_def lin_def by blast
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   123
	
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   124
	have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   125
	proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   126
          from HE y1 y2 show "y1 + y2 \<in> H"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   127
            by (rule subspace.add_closed)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   128
          from x0 and HE y y1 y2
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   129
          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   130
          with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   131
            by (simp add: add_ac add_mult_distrib2)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   132
          also note x1x2
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   133
          finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   134
	qed
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   135
	
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   136
	from h'_def x1x2 E HE y x0
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   137
	have "h' (x1 + x2) = h y + a * xi"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   138
          by (rule h'_definite)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   139
	also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   140
          by (simp only: ya)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   141
	also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   142
          by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   143
	also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   144
          by (simp add: left_distrib)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   145
	also from h'_def x1_rep E HE y1 x0
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   146
	have "h y1 + a1 * xi = h' x1"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   147
          by (rule h'_definite [symmetric])
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   148
	also from h'_def x2_rep E HE y2 x0
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   149
	have "h y2 + a2 * xi = h' x2"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   150
          by (rule h'_definite [symmetric])
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   151
	finally show ?thesis .
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
   152
      qed
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   153
    next
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   154
      fix x1 c assume x1: "x1 \<in> H'"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   155
      show "h' (c \<cdot> x1) = c * (h' x1)"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   156
      proof -
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   157
	from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   158
          by (rule vectorspace.mult_closed)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   159
	with x1 obtain y a y1 a1 where
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   160
            cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   161
          and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   162
          unfolding H'_def sum_def lin_def by blast
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   163
	
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   164
	have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   165
	proof (rule decomp_H')
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   166
          from HE y1 show "c \<cdot> y1 \<in> H"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   167
            by (rule subspace.mult_closed)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   168
          from x0 and HE y y1
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   169
          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   170
          with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   171
            by (simp add: mult_assoc add_mult_distrib1)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   172
          also note cx1_rep
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   173
          finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   174
	qed
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   175
	
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   176
	from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   177
          by (rule h'_definite)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   178
	also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   179
          by (simp only: ya)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   180
	also from y1 have "h (c \<cdot> y1) = c * h y1"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   181
          by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   182
	also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   183
          by (simp only: right_distrib)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   184
	also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   185
          by (rule h'_definite [symmetric])
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   186
	finally show ?thesis .
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
   187
      qed
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   188
    }
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   189
  qed
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
   190
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   191
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   192
text {* \medskip The linear extension @{text h'} of @{text h}
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   193
  is bounded by the seminorm @{text p}. *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   194
9374
153853af318b - xsymbols for
bauerg
parents: 9256
diff changeset
   195
lemma h'_norm_pres:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   196
  assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   197
      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   198
    and H'_def: "H' \<equiv> H + lin x0"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   199
    and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   200
  assumes E: "vectorspace E" and HE: "subspace H E"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   201
    and "seminorm E p" and "linearform H h"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   202
  assumes a: "\<forall>y \<in> H. h y \<le> p y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   203
    and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   204
  shows "\<forall>x \<in> H'. h' x \<le> p x"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   205
proof -
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   206
  interpret vectorspace [E] by fact
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   207
  interpret subspace [H E] by fact
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   208
  interpret seminorm [E p] by fact
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   209
  interpret linearform [H h] by fact
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   210
  show ?thesis
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   211
  proof
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   212
    fix x assume x': "x \<in> H'"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   213
    show "h' x \<le> p x"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   214
    proof -
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   215
      from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   216
	and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   217
      from x' obtain y a where
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   218
          x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   219
	unfolding H'_def sum_def lin_def by blast
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   220
      from y have y': "y \<in> E" ..
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   221
      from y have ay: "inverse a \<cdot> y \<in> H" by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   222
      
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   223
      from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   224
	by (rule h'_definite)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   225
      also have "\<dots> \<le> p (y + a \<cdot> x0)"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   226
      proof (rule linorder_cases)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   227
	assume z: "a = 0"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   228
	then have "h y + a * xi = h y" by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   229
	also from a y have "\<dots> \<le> p y" ..
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   230
	also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   231
	finally show ?thesis .
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   232
      next
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   233
	txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   234
          with @{text ya} taken as @{text "y / a"}: *}
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   235
	assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   236
	from a1 ay
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   237
	have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   238
	with lz have "a * xi \<le>
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   239
          a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   240
          by (simp add: mult_left_mono_neg order_less_imp_le)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   241
	
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   242
	also have "\<dots> =
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   243
          - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   244
	  by (simp add: right_diff_distrib)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   245
	also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   246
          p (a \<cdot> (inverse a \<cdot> y + x0))"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   247
          by (simp add: abs_homogenous)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   248
	also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   249
          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   250
	also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   251
          by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   252
	finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   253
	then show ?thesis by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   254
      next
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   255
	txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   256
          with @{text ya} taken as @{text "y / a"}: *}
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   257
	assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   258
	from a2 ay
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   259
	have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   260
	with gz have "a * xi \<le>
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   261
          a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   262
          by simp
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   263
	also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   264
	  by (simp add: right_diff_distrib)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   265
	also from gz x0 y'
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   266
	have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   267
          by (simp add: abs_homogenous)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   268
	also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   269
          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   270
	also from nz y have "a * h (inverse a \<cdot> y) = h y"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   271
          by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   272
	finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   273
	then show ?thesis by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   274
      qed
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   275
      also from x_rep have "\<dots> = p x" by (simp only:)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   276
      finally show ?thesis .
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
   277
    qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
   278
  qed
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   279
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   280
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9906
diff changeset
   281
end