src/HOL/Multivariate_Analysis/PolyRoots.thy
author paulson <lp15@cam.ac.uk>
Tue Nov 10 14:18:41 2015 +0000 (2015-11-10)
changeset 61609 77b453bd616f
parent 60420 884f54e01427
child 61610 4f54d2759a0b
permissions -rw-r--r--
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
wenzelm@60420
     1
section \<open>polynomial functions: extremal behaviour and root counts\<close>
lp15@56215
     2
lp15@56215
     3
(*  Author: John Harrison and Valentina Bruno
lp15@56215
     4
    Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
lp15@56215
     5
*)
lp15@56215
     6
lp15@56215
     7
theory PolyRoots
lp15@56215
     8
imports Complex_Main
lp15@56215
     9
lp15@56215
    10
begin
lp15@56215
    11
wenzelm@60420
    12
subsection\<open>Geometric progressions\<close>
lp15@56215
    13
lp15@56215
    14
lemma setsum_gp_basic:
lp15@56215
    15
  fixes x :: "'a::{comm_ring,monoid_mult}"
lp15@56215
    16
  shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
lp15@56215
    17
  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
lp15@56215
    18
lp15@56215
    19
lemma setsum_gp0:
haftmann@59867
    20
  fixes x :: "'a::{comm_ring,division_ring}"
lp15@59615
    21
  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
lp15@59615
    22
  using setsum_gp_basic[of x n]
lp15@61609
    23
  by (simp add: mult.commute divide_simps)
lp15@59615
    24
lp15@59615
    25
lemma setsum_power_add:
lp15@59615
    26
  fixes x :: "'a::{comm_ring,monoid_mult}"
lp15@59615
    27
  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
lp15@59615
    28
  by (simp add: setsum_right_distrib power_add)
lp15@56215
    29
lp15@56215
    30
lemma setsum_power_shift:
lp15@56215
    31
  fixes x :: "'a::{comm_ring,monoid_mult}"
lp15@56215
    32
  assumes "m \<le> n"
lp15@56215
    33
  shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
lp15@56215
    34
proof -
lp15@56215
    35
  have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
lp15@56215
    36
    by (simp add: setsum_right_distrib power_add [symmetric])
hoelzl@57129
    37
  also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
wenzelm@60420
    38
    using \<open>m \<le> n\<close> by (intro setsum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
lp15@56215
    39
  finally show ?thesis .
lp15@56215
    40
qed
lp15@56215
    41
lp15@56215
    42
lemma setsum_gp_multiplied:
lp15@56215
    43
  fixes x :: "'a::{comm_ring,monoid_mult}"
lp15@56215
    44
  assumes "m \<le> n"
lp15@56215
    45
  shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
lp15@56215
    46
proof -
lp15@56215
    47
  have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
haftmann@57514
    48
    by (metis mult.assoc mult.commute assms setsum_power_shift)
lp15@56215
    49
  also have "... =x^m * (1 - x^Suc(n-m))"
haftmann@57514
    50
    by (metis mult.assoc setsum_gp_basic)
lp15@56215
    51
  also have "... = x^m - x^Suc n"
lp15@56215
    52
    using assms
lp15@56215
    53
    by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
lp15@56215
    54
  finally show ?thesis .
lp15@56215
    55
qed
lp15@56215
    56
lp15@56215
    57
lemma setsum_gp:
haftmann@59867
    58
  fixes x :: "'a::{comm_ring,division_ring}"
lp15@56215
    59
  shows   "(\<Sum>i=m..n. x^i) =
lp15@56215
    60
               (if n < m then 0
lp15@56215
    61
                else if x = 1 then of_nat((n + 1) - m)
lp15@56215
    62
                else (x^m - x^Suc n) / (1 - x))"
lp15@61609
    63
using setsum_gp_multiplied [of m n x]
lp15@61609
    64
apply auto
haftmann@57512
    65
by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
lp15@56215
    66
lp15@56215
    67
lemma setsum_gp_offset:
haftmann@59867
    68
  fixes x :: "'a::{comm_ring,division_ring}"
lp15@56215
    69
  shows   "(\<Sum>i=m..m+n. x^i) =
lp15@56215
    70
       (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
lp15@56215
    71
  using setsum_gp [of x m "m+n"]
lp15@56215
    72
  by (auto simp: power_add algebra_simps)
lp15@56215
    73
lp15@59615
    74
lemma setsum_gp_strict:
haftmann@59867
    75
  fixes x :: "'a::{comm_ring,division_ring}"
lp15@59615
    76
  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
lp15@59615
    77
  by (induct n) (auto simp: algebra_simps divide_simps)
lp15@61609
    78
wenzelm@60420
    79
subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
lp15@56215
    80
lp15@56215
    81
lemma sub_polyfun:
lp15@56215
    82
  fixes x :: "'a::{comm_ring,monoid_mult}"
lp15@61609
    83
  shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
lp15@56215
    84
           (x - y) * (\<Sum>j<n. \<Sum>k= Suc j..n. a k * y^(k - Suc j) * x^j)"
lp15@56215
    85
proof -
lp15@61609
    86
  have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
lp15@56215
    87
        (\<Sum>i\<le>n. a i * (x^i - y^i))"
lp15@56215
    88
    by (simp add: algebra_simps setsum_subtractf [symmetric])
lp15@56215
    89
  also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
haftmann@57514
    90
    by (simp add: power_diff_sumr2 ac_simps)
lp15@56215
    91
  also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))"
haftmann@57514
    92
    by (simp add: setsum_right_distrib ac_simps)
lp15@56215
    93
  also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
lp15@56215
    94
    by (simp add: nested_setsum_swap')
lp15@56215
    95
  finally show ?thesis .
lp15@56215
    96
qed
lp15@56215
    97
lp15@56215
    98
lemma sub_polyfun_alt:
lp15@56215
    99
  fixes x :: "'a::{comm_ring,monoid_mult}"
lp15@61609
   100
  shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
lp15@56215
   101
           (x - y) * (\<Sum>j<n. \<Sum>k<n-j. a (j+k+1) * y^k * x^j)"
lp15@56215
   102
proof -
lp15@56215
   103
  { fix j
lp15@56215
   104
    have "(\<Sum>k = Suc j..n. a k * y^(k - Suc j) * x^j) =
lp15@56215
   105
          (\<Sum>k <n - j. a (Suc (j + k)) * y^k * x^j)"
hoelzl@57129
   106
      by (rule setsum.reindex_bij_witness[where i="\<lambda>i. i + Suc j" and j="\<lambda>i. i - Suc j"]) auto }
lp15@56215
   107
  then show ?thesis
lp15@56215
   108
    by (simp add: sub_polyfun)
lp15@56215
   109
qed
lp15@56215
   110
lp15@56215
   111
lemma polyfun_linear_factor:
lp15@56215
   112
  fixes a :: "'a::{comm_ring,monoid_mult}"
lp15@61609
   113
  shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) =
lp15@56215
   114
                  (z-a) * (\<Sum>i<n. b i * z^i) + (\<Sum>i\<le>n. c i * a^i)"
lp15@56215
   115
proof -
lp15@56215
   116
  { fix z
lp15@61609
   117
    have "(\<Sum>i\<le>n. c i * z^i) - (\<Sum>i\<le>n. c i * a^i) =
lp15@56215
   118
          (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)"
lp15@56215
   119
      by (simp add: sub_polyfun setsum_left_distrib)
lp15@61609
   120
    then have "(\<Sum>i\<le>n. c i * z^i) =
lp15@56215
   121
          (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)
lp15@56215
   122
          + (\<Sum>i\<le>n. c i * a^i)"
lp15@56215
   123
      by (simp add: algebra_simps) }
lp15@56215
   124
  then show ?thesis
lp15@61609
   125
    by (intro exI allI)
lp15@56215
   126
qed
lp15@56215
   127
lp15@56215
   128
lemma polyfun_linear_factor_root:
lp15@56215
   129
  fixes a :: "'a::{comm_ring,monoid_mult}"
lp15@56215
   130
  assumes "(\<Sum>i\<le>n. c i * a^i) = 0"
lp15@56215
   131
  shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) = (z-a) * (\<Sum>i<n. b i * z^i)"
lp15@56215
   132
  using polyfun_linear_factor [of c n a] assms
lp15@56215
   133
  by simp
lp15@56215
   134
lp15@56215
   135
lemma adhoc_norm_triangle: "a + norm(y) \<le> b ==> norm(x) \<le> a ==> norm(x + y) \<le> b"
lp15@56215
   136
  by (metis norm_triangle_mono order.trans order_refl)
lp15@56215
   137
lp15@56215
   138
lemma polyfun_extremal_lemma:
lp15@56215
   139
  fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
lp15@56215
   140
  assumes "e > 0"
lp15@56215
   141
    shows "\<exists>M. \<forall>z. M \<le> norm z \<longrightarrow> norm(\<Sum>i\<le>n. c i * z^i) \<le> e * norm(z) ^ Suc n"
lp15@56215
   142
proof (induction n)
lp15@56215
   143
  case 0
lp15@61609
   144
  show ?case
haftmann@57512
   145
    by (rule exI [where x="norm (c 0) / e"]) (auto simp: mult.commute pos_divide_le_eq assms)
lp15@56215
   146
next
lp15@56215
   147
  case (Suc n)
lp15@56215
   148
  then obtain M where M: "\<forall>z. M \<le> norm z \<longrightarrow> norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n" ..
lp15@56215
   149
  show ?case
lp15@56215
   150
  proof (rule exI [where x="max 1 (max M ((e + norm(c(Suc n))) / e))"], clarify)
lp15@56215
   151
    fix z::'a
lp15@56215
   152
    assume "max 1 (max M ((e + norm (c (Suc n))) / e)) \<le> norm z"
lp15@56215
   153
    then have norm1: "0 < norm z" "M \<le> norm z" "(e + norm (c (Suc n))) / e \<le> norm z"
lp15@56215
   154
      by auto
lp15@56215
   155
    then have norm2: "(e + norm (c (Suc n))) \<le> e * norm z"  "(norm z * norm z ^ n) > 0"
lp15@61609
   156
      apply (metis assms less_divide_eq mult.commute not_le)
lp15@56215
   157
      using norm1 apply (metis mult_pos_pos zero_less_power)
lp15@56215
   158
      done
lp15@56215
   159
    have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n)) =
lp15@56215
   160
          (e + norm (c (Suc n))) * (norm z * norm z ^ n)"
lp15@56215
   161
      by (simp add: norm_mult norm_power algebra_simps)
lp15@56215
   162
    also have "... \<le> (e * norm z) * (norm z * norm z ^ n)"
lp15@61609
   163
      using norm2 by (metis real_mult_le_cancel_iff1)
lp15@56215
   164
    also have "... = e * (norm z * (norm z * norm z ^ n))"
lp15@56215
   165
      by (simp add: algebra_simps)
lp15@56215
   166
    finally have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n))
lp15@56215
   167
                  \<le> e * (norm z * (norm z * norm z ^ n))" .
lp15@56215
   168
    then show "norm (\<Sum>i\<le>Suc n. c i * z^i) \<le> e * norm z ^ Suc (Suc n)" using M norm1
lp15@56215
   169
      by (drule_tac x=z in spec) (auto simp: intro!: adhoc_norm_triangle)
lp15@56215
   170
    qed
lp15@56215
   171
qed
lp15@56215
   172
lp15@56215
   173
lemma norm_lemma_xy: "\<lbrakk>abs b + 1 \<le> norm(y) - a; norm(x) \<le> a\<rbrakk> \<Longrightarrow> b \<le> norm(x + y)"
lp15@61609
   174
  by (metis abs_add_one_not_less_self add.commute diff_le_eq dual_order.trans le_less_linear
lp15@56215
   175
         norm_diff_ineq)
lp15@56215
   176
lp15@56215
   177
lemma polyfun_extremal:
lp15@56215
   178
  fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
lp15@56215
   179
  assumes "\<exists>k. k \<noteq> 0 \<and> k \<le> n \<and> c k \<noteq> 0"
lp15@56215
   180
    shows "eventually (\<lambda>z. norm(\<Sum>i\<le>n. c i * z^i) \<ge> B) at_infinity"
lp15@56215
   181
using assms
lp15@56215
   182
proof (induction n)
lp15@56215
   183
  case 0 then show ?case
lp15@56215
   184
    by simp
lp15@56215
   185
next
lp15@56215
   186
  case (Suc n)
lp15@56215
   187
  show ?case
lp15@56215
   188
  proof (cases "c (Suc n) = 0")
lp15@56215
   189
    case True
lp15@56215
   190
    with Suc show ?thesis
lp15@56215
   191
      by auto (metis diff_is_0_eq diffs0_imp_equal less_Suc_eq_le not_less_eq)
lp15@56215
   192
  next
lp15@56215
   193
    case False
lp15@56215
   194
    with polyfun_extremal_lemma [of "norm(c (Suc n)) / 2" c n]
lp15@61609
   195
    obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow>
lp15@56215
   196
               norm (\<Sum>i\<le>n. c i * z^i) \<le> norm (c (Suc n)) / 2 * norm z ^ Suc n"
lp15@56215
   197
      by auto
lp15@56215
   198
    show ?thesis
lp15@56215
   199
    unfolding eventually_at_infinity
lp15@56215
   200
    proof (rule exI [where x="max M (max 1 ((abs B + 1) / (norm (c (Suc n)) / 2)))"], clarsimp)
lp15@56215
   201
      fix z::'a
lp15@56215
   202
      assume les: "M \<le> norm z"  "1 \<le> norm z"  "(\<bar>B\<bar> * 2 + 2) / norm (c (Suc n)) \<le> norm z"
lp15@56215
   203
      then have "\<bar>B\<bar> * 2 + 2 \<le> norm z * norm (c (Suc n))"
lp15@56215
   204
        by (metis False pos_divide_le_eq zero_less_norm_iff)
lp15@61609
   205
      then have "\<bar>B\<bar> * 2 + 2 \<le> norm z ^ (Suc n) * norm (c (Suc n))"
wenzelm@60420
   206
        by (metis \<open>1 \<le> norm z\<close> order.trans mult_right_mono norm_ge_zero self_le_power zero_less_Suc)
lp15@56215
   207
      then show "B \<le> norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * (z * z ^ n))" using M les
lp15@56215
   208
        apply auto
lp15@56215
   209
        apply (rule norm_lemma_xy [where a = "norm (c (Suc n)) * norm z ^ (Suc n) / 2"])
lp15@56215
   210
        apply (simp_all add: norm_mult norm_power)
lp15@56215
   211
        done
lp15@56215
   212
    qed
lp15@56215
   213
  qed
lp15@56215
   214
qed
lp15@56215
   215
lp15@56215
   216
lemma polyfun_rootbound:
lp15@56215
   217
 fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
lp15@56215
   218
 assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
lp15@56215
   219
   shows "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<and> card {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<le> n"
lp15@56215
   220
using assms
lp15@56215
   221
proof (induction n arbitrary: c)
lp15@56215
   222
 case (Suc n) show ?case
lp15@56215
   223
 proof (cases "{z. (\<Sum>i\<le>Suc n. c i * z^i) = 0} = {}")
lp15@56215
   224
   case False
lp15@56215
   225
   then obtain a where a: "(\<Sum>i\<le>Suc n. c i * a^i) = 0"
lp15@56215
   226
     by auto
lp15@56215
   227
   from polyfun_linear_factor_root [OF this]
lp15@56215
   228
   obtain b where "\<And>z. (\<Sum>i\<le>Suc n. c i * z^i) = (z - a) * (\<Sum>i< Suc n. b i * z^i)"
lp15@56215
   229
     by auto
lp15@56215
   230
   then have b: "\<And>z. (\<Sum>i\<le>Suc n. c i * z^i) = (z - a) * (\<Sum>i\<le>n. b i * z^i)"
lp15@56215
   231
     by (metis lessThan_Suc_atMost)
lp15@56215
   232
   then have ins_ab: "{z. (\<Sum>i\<le>Suc n. c i * z^i) = 0} = insert a {z. (\<Sum>i\<le>n. b i * z^i) = 0}"
lp15@56215
   233
     by auto
lp15@56215
   234
   have c0: "c 0 = - (a * b 0)" using  b [of 0]
lp15@56215
   235
     by simp
lp15@56215
   236
   then have extr_prem: "~ (\<exists>k\<le>n. b k \<noteq> 0) \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> k \<le> Suc n \<and> c k \<noteq> 0"
lp15@56215
   237
     by (metis Suc.prems le0 minus_zero mult_zero_right)
lp15@61609
   238
   have "\<exists>k\<le>n. b k \<noteq> 0"
lp15@56215
   239
     apply (rule ccontr)
lp15@56215
   240
     using polyfun_extremal [OF extr_prem, of 1]
lp15@56215
   241
     apply (auto simp: eventually_at_infinity b simp del: setsum_atMost_Suc)
lp15@56215
   242
     apply (drule_tac x="of_real ba" in spec, simp)
lp15@56215
   243
     done
lp15@56215
   244
   then show ?thesis using Suc.IH [of b] ins_ab
lp15@56215
   245
     by (auto simp: card_insert_if)
lp15@56215
   246
   qed simp
lp15@56215
   247
qed simp
lp15@56215
   248
lp15@56215
   249
corollary
lp15@56215
   250
  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
lp15@56215
   251
  assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
lp15@56215
   252
    shows polyfun_rootbound_finite: "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
lp15@56215
   253
      and polyfun_rootbound_card:   "card {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<le> n"
lp15@56215
   254
using polyfun_rootbound [OF assms] by auto
lp15@56215
   255
lp15@56215
   256
lemma polyfun_finite_roots:
lp15@56215
   257
  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
lp15@56215
   258
    shows  "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<longleftrightarrow> (\<exists>k. k \<le> n \<and> c k \<noteq> 0)"
lp15@56215
   259
proof (cases " \<exists>k\<le>n. c k \<noteq> 0")
lp15@61609
   260
  case True then show ?thesis
lp15@56215
   261
    by (blast intro: polyfun_rootbound_finite)
lp15@56215
   262
next
lp15@61609
   263
  case False then show ?thesis
lp15@56215
   264
    by (auto simp: infinite_UNIV_char_0)
lp15@56215
   265
qed
lp15@56215
   266
lp15@56215
   267
lemma polyfun_eq_0:
lp15@56215
   268
  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
lp15@56215
   269
    shows  "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0) \<longleftrightarrow> (\<forall>k. k \<le> n \<longrightarrow> c k = 0)"
lp15@56215
   270
proof (cases "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0)")
lp15@56215
   271
  case True
lp15@56215
   272
  then have "~ finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
lp15@56215
   273
    by (simp add: infinite_UNIV_char_0)
lp15@56215
   274
  with True show ?thesis
lp15@56215
   275
    by (metis (poly_guards_query) polyfun_rootbound_finite)
lp15@56215
   276
next
lp15@56215
   277
  case False
lp15@56215
   278
  then show ?thesis
lp15@56215
   279
    by auto
lp15@56215
   280
qed
lp15@56215
   281
lp15@56215
   282
lemma polyfun_eq_const:
lp15@56215
   283
  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
lp15@56215
   284
    shows  "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = k) \<longleftrightarrow> c 0 = k \<and> (\<forall>k. k \<noteq> 0 \<and> k \<le> n \<longrightarrow> c k = 0)"
lp15@56215
   285
proof -
lp15@56215
   286
  {fix z
lp15@56215
   287
    have "(\<Sum>i\<le>n. c i * z^i) = (\<Sum>i\<le>n. (if i = 0 then c 0 - k else c i) * z^i) + k"
lp15@56215
   288
      by (induct n) auto
lp15@56215
   289
  } then
lp15@56215
   290
  have "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = k) \<longleftrightarrow> (\<forall>z. (\<Sum>i\<le>n. (if i = 0 then c 0 - k else c i) * z^i) = 0)"
lp15@56215
   291
    by auto
lp15@56215
   292
  also have "... \<longleftrightarrow>  c 0 = k \<and> (\<forall>k. k \<noteq> 0 \<and> k \<le> n \<longrightarrow> c k = 0)"
lp15@56215
   293
    by (auto simp: polyfun_eq_0)
lp15@56215
   294
  finally show ?thesis .
lp15@56215
   295
qed
lp15@56215
   296
lp15@56215
   297
end
lp15@56215
   298