src/HOL/Multivariate_Analysis/Euclidean_Space.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 40786 0a54cfc9add3
child 41863 e5104b436ea1
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
wenzelm@35253
     1
(*  Title:      Library/Multivariate_Analysis/Euclidean_Space.thy
himmelma@33175
     2
    Author:     Amine Chaieb, University of Cambridge
himmelma@33175
     3
*)
himmelma@33175
     4
himmelma@33175
     5
header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
himmelma@33175
     6
himmelma@33175
     7
theory Euclidean_Space
himmelma@33175
     8
imports
wenzelm@41413
     9
  Complex_Main
wenzelm@41413
    10
  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
wenzelm@41413
    11
  "~~/src/HOL/Library/Infinite_Set"
wenzelm@41413
    12
  "~~/src/HOL/Library/Inner_Product"
wenzelm@41413
    13
  L2_Norm
wenzelm@41413
    14
  "~~/src/HOL/Library/Convex"
wenzelm@38136
    15
uses
wenzelm@38136
    16
  "~~/src/HOL/Library/positivstellensatz.ML"  (* FIXME duplicate use!? *)
wenzelm@38136
    17
  ("normarith.ML")
himmelma@33175
    18
begin
himmelma@33175
    19
hoelzl@37489
    20
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
hoelzl@37489
    21
  by auto
himmelma@33175
    22
haftmann@37606
    23
notation inner (infix "\<bullet>" 70)
himmelma@35542
    24
himmelma@33175
    25
subsection {* A connectedness or intermediate value lemma with several applications. *}
himmelma@33175
    26
himmelma@33175
    27
lemma connected_real_lemma:
himmelma@33175
    28
  fixes f :: "real \<Rightarrow> 'a::metric_space"
himmelma@33175
    29
  assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"
himmelma@33175
    30
  and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e"
himmelma@33175
    31
  and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"
himmelma@33175
    32
  and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"
himmelma@33175
    33
  and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"
himmelma@33175
    34
  shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")
himmelma@33175
    35
proof-
himmelma@33175
    36
  let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"
himmelma@33175
    37
  have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa)
himmelma@33175
    38
  have Sub: "\<exists>y. isUb UNIV ?S y"
himmelma@33175
    39
    apply (rule exI[where x= b])
himmelma@33175
    40
    using ab fb e12 by (auto simp add: isUb_def setle_def)
himmelma@33175
    41
  from reals_complete[OF Se Sub] obtain l where
himmelma@33175
    42
    l: "isLub UNIV ?S l"by blast
himmelma@33175
    43
  have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12
himmelma@33175
    44
    apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
himmelma@33175
    45
    by (metis linorder_linear)
himmelma@33175
    46
  have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l
himmelma@33175
    47
    apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
himmelma@33175
    48
    by (metis linorder_linear not_le)
himmelma@33175
    49
    have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
himmelma@33175
    50
    have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
himmelma@33175
    51
    have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by dlo
himmelma@33175
    52
    {assume le2: "f l \<in> e2"
himmelma@33175
    53
      from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
himmelma@33175
    54
      hence lap: "l - a > 0" using alb by arith
himmelma@33175
    55
      from e2[rule_format, OF le2] obtain e where
himmelma@33175
    56
        e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
himmelma@33175
    57
      from dst[OF alb e(1)] obtain d where
himmelma@33175
    58
        d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
himmelma@33175
    59
      have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" using lap d(1)
himmelma@33175
    60
        apply ferrack by arith
himmelma@33175
    61
      then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
himmelma@33175
    62
      from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
himmelma@33175
    63
      from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
himmelma@33175
    64
      moreover
himmelma@33175
    65
      have "f (l - d') \<in> e1" using ale1[rule_format, of "l -d'"] d' by auto
himmelma@33175
    66
      ultimately have False using e12 alb d' by auto}
himmelma@33175
    67
    moreover
himmelma@33175
    68
    {assume le1: "f l \<in> e1"
himmelma@33175
    69
    from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis
himmelma@33175
    70
      hence blp: "b - l > 0" using alb by arith
himmelma@33175
    71
      from e1[rule_format, OF le1] obtain e where
himmelma@33175
    72
        e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
himmelma@33175
    73
      from dst[OF alb e(1)] obtain d where
himmelma@33175
    74
        d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
himmelma@33175
    75
      have "\<exists>d'. d' < d \<and> d' >0" using d(1) by dlo
himmelma@33175
    76
      then obtain d' where d': "d' > 0" "d' < d" by metis
himmelma@33175
    77
      from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
himmelma@33175
    78
      hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
himmelma@33175
    79
      with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto
himmelma@33175
    80
      with l d' have False
himmelma@33175
    81
        by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }
himmelma@33175
    82
    ultimately show ?thesis using alb by metis
himmelma@33175
    83
qed
himmelma@33175
    84
huffman@36431
    85
text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case *}
himmelma@33175
    86
himmelma@33175
    87
lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
himmelma@33175
    88
proof-
himmelma@33175
    89
  have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith
haftmann@36350
    90
  thus ?thesis by (simp add: field_simps power2_eq_square)
himmelma@33175
    91
qed
himmelma@33175
    92
himmelma@33175
    93
lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> abs(y * y - x * x) < e)"
himmelma@33175
    94
  using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] apply (auto simp add: power2_eq_square)
himmelma@33175
    95
  apply (rule_tac x="s" in exI)
himmelma@33175
    96
  apply auto
himmelma@33175
    97
  apply (erule_tac x=y in allE)
himmelma@33175
    98
  apply auto
himmelma@33175
    99
  done
himmelma@33175
   100
himmelma@33175
   101
lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y"
himmelma@33175
   102
  using real_sqrt_le_iff[of x "y^2"] by simp
himmelma@33175
   103
himmelma@33175
   104
lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y"
himmelma@33175
   105
  using real_sqrt_le_mono[of "x^2" y] by simp
himmelma@33175
   106
himmelma@33175
   107
lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y"
himmelma@33175
   108
  using real_sqrt_less_mono[of "x^2" y] by simp
himmelma@33175
   109
himmelma@33175
   110
lemma sqrt_even_pow2: assumes n: "even n"
himmelma@33175
   111
  shows "sqrt(2 ^ n) = 2 ^ (n div 2)"
himmelma@33175
   112
proof-
huffman@36362
   113
  from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex ..
himmelma@33175
   114
  from m  have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)"
himmelma@33175
   115
    by (simp only: power_mult[symmetric] mult_commute)
himmelma@33175
   116
  then show ?thesis  using m by simp
himmelma@33175
   117
qed
himmelma@33175
   118
himmelma@33175
   119
lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)"
himmelma@33175
   120
  apply (cases "x = 0", simp_all)
himmelma@33175
   121
  using sqrt_divide_self_eq[of x]
huffman@36362
   122
  apply (simp add: inverse_eq_divide field_simps)
himmelma@33175
   123
  done
himmelma@33175
   124
himmelma@33175
   125
text{* Hence derive more interesting properties of the norm. *}
himmelma@33175
   126
hoelzl@37489
   127
(* FIXME: same as norm_scaleR
hoelzl@37489
   128
lemma norm_mul[simp]: "norm(a *\<^sub>R x) = abs(a) * norm x"
huffman@36362
   129
  by (simp add: norm_vector_def setL2_right_distrib abs_mult)
hoelzl@37489
   130
*)
huffman@36362
   131
himmelma@35542
   132
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
hoelzl@37489
   133
  by (simp add: setL2_def power2_eq_square)
himmelma@35542
   134
himmelma@33175
   135
lemma norm_cauchy_schwarz:
himmelma@35542
   136
  shows "inner x y <= norm x * norm y"
himmelma@35542
   137
  using Cauchy_Schwarz_ineq2[of x y] by auto
himmelma@33175
   138
himmelma@33175
   139
lemma norm_cauchy_schwarz_abs:
himmelma@35542
   140
  shows "\<bar>inner x y\<bar> \<le> norm x * norm y"
huffman@36585
   141
  by (rule Cauchy_Schwarz_ineq2)
himmelma@33175
   142
himmelma@33175
   143
lemma norm_triangle_sub:
himmelma@33175
   144
  fixes x y :: "'a::real_normed_vector"
himmelma@33175
   145
  shows "norm x \<le> norm y  + norm (x - y)"
haftmann@36350
   146
  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
himmelma@33175
   147
hoelzl@34291
   148
lemma real_abs_norm: "\<bar>norm x\<bar> = norm x"
himmelma@33175
   149
  by (rule abs_norm_cancel)
huffman@36585
   150
lemma real_abs_sub_norm: "\<bar>norm x - norm y\<bar> <= norm(x - y)"
himmelma@33175
   151
  by (rule norm_triangle_ineq3)
huffman@36585
   152
lemma norm_le: "norm(x) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
himmelma@35542
   153
  by (simp add: norm_eq_sqrt_inner) 
huffman@36585
   154
lemma norm_lt: "norm(x) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
himmelma@35542
   155
  by (simp add: norm_eq_sqrt_inner)
huffman@36585
   156
lemma norm_eq: "norm(x) = norm (y) \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
himmelma@35542
   157
  apply(subst order_eq_iff) unfolding norm_le by auto
huffman@36585
   158
lemma norm_eq_1: "norm(x) = 1 \<longleftrightarrow> x \<bullet> x = 1"
himmelma@35542
   159
  unfolding norm_eq_sqrt_inner by auto
himmelma@33175
   160
himmelma@33175
   161
text{* Squaring equations and inequalities involving norms.  *}
himmelma@33175
   162
himmelma@33175
   163
lemma dot_square_norm: "x \<bullet> x = norm(x)^2"
himmelma@35542
   164
  by (simp add: norm_eq_sqrt_inner)
himmelma@33175
   165
himmelma@33175
   166
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
himmelma@35542
   167
  by (auto simp add: norm_eq_sqrt_inner)
himmelma@33175
   168
himmelma@33175
   169
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
huffman@36362
   170
proof
huffman@36362
   171
  assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
huffman@36362
   172
  then have "\<bar>x\<bar>\<twosuperior> \<le> \<bar>y\<bar>\<twosuperior>" by (rule power_mono, simp)
huffman@36362
   173
  then show "x\<twosuperior> \<le> y\<twosuperior>" by simp
huffman@36362
   174
next
huffman@36362
   175
  assume "x\<twosuperior> \<le> y\<twosuperior>"
huffman@36362
   176
  then have "sqrt (x\<twosuperior>) \<le> sqrt (y\<twosuperior>)" by (rule real_sqrt_le_mono)
huffman@36362
   177
  then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp
himmelma@33175
   178
qed
himmelma@33175
   179
himmelma@33175
   180
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
himmelma@33175
   181
  apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
himmelma@33175
   182
  using norm_ge_zero[of x]
himmelma@33175
   183
  apply arith
himmelma@33175
   184
  done
himmelma@33175
   185
himmelma@33175
   186
lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
himmelma@33175
   187
  apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
himmelma@33175
   188
  using norm_ge_zero[of x]
himmelma@33175
   189
  apply arith
himmelma@33175
   190
  done
himmelma@33175
   191
himmelma@33175
   192
lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a^2"
himmelma@33175
   193
  by (metis not_le norm_ge_square)
himmelma@33175
   194
lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2"
himmelma@33175
   195
  by (metis norm_le_square not_less)
himmelma@33175
   196
himmelma@33175
   197
text{* Dot product in terms of the norm rather than conversely. *}
himmelma@33175
   198
himmelma@35542
   199
lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left 
himmelma@35542
   200
inner.scaleR_left inner.scaleR_right
himmelma@35542
   201
himmelma@33175
   202
lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
himmelma@35542
   203
  unfolding power2_norm_eq_inner inner_simps inner_commute by auto 
himmelma@33175
   204
himmelma@33175
   205
lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2"
haftmann@36350
   206
  unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps)
himmelma@33175
   207
himmelma@33175
   208
text{* Equality of vectors in terms of @{term "op \<bullet>"} products.    *}
himmelma@33175
   209
huffman@36585
   210
lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs")
himmelma@33175
   211
proof
huffman@36585
   212
  assume ?lhs then show ?rhs by simp
himmelma@33175
   213
next
himmelma@33175
   214
  assume ?rhs
himmelma@35542
   215
  then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0" by simp
himmelma@35542
   216
  hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" by (simp add: inner_simps inner_commute)
haftmann@36350
   217
  then have "(x - y) \<bullet> (x - y) = 0" by (simp add: field_simps inner_simps inner_commute)
himmelma@35542
   218
  then show "x = y" by (simp)
himmelma@33175
   219
qed
himmelma@33175
   220
himmelma@33175
   221
subsection{* General linear decision procedure for normed spaces. *}
himmelma@33175
   222
himmelma@33175
   223
lemma norm_cmul_rule_thm:
himmelma@33175
   224
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   225
  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
himmelma@33175
   226
  unfolding norm_scaleR
haftmann@38642
   227
  apply (erule mult_left_mono)
himmelma@33175
   228
  apply simp
himmelma@33175
   229
  done
himmelma@33175
   230
himmelma@33175
   231
  (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
himmelma@33175
   232
lemma norm_add_rule_thm:
himmelma@33175
   233
  fixes x1 x2 :: "'a::real_normed_vector"
himmelma@33175
   234
  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
himmelma@33175
   235
  by (rule order_trans [OF norm_triangle_ineq add_mono])
himmelma@33175
   236
haftmann@35028
   237
lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
haftmann@36350
   238
  by (simp add: field_simps)
himmelma@33175
   239
himmelma@33175
   240
lemma pth_1:
himmelma@33175
   241
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   242
  shows "x == scaleR 1 x" by simp
himmelma@33175
   243
himmelma@33175
   244
lemma pth_2:
himmelma@33175
   245
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   246
  shows "x - y == x + -y" by (atomize (full)) simp
himmelma@33175
   247
himmelma@33175
   248
lemma pth_3:
himmelma@33175
   249
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   250
  shows "- x == scaleR (-1) x" by simp
himmelma@33175
   251
himmelma@33175
   252
lemma pth_4:
himmelma@33175
   253
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   254
  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
himmelma@33175
   255
himmelma@33175
   256
lemma pth_5:
himmelma@33175
   257
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   258
  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
himmelma@33175
   259
himmelma@33175
   260
lemma pth_6:
himmelma@33175
   261
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   262
  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
himmelma@33175
   263
  by (simp add: scaleR_right_distrib)
himmelma@33175
   264
himmelma@33175
   265
lemma pth_7:
himmelma@33175
   266
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   267
  shows "0 + x == x" and "x + 0 == x" by simp_all
himmelma@33175
   268
himmelma@33175
   269
lemma pth_8:
himmelma@33175
   270
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   271
  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
himmelma@33175
   272
  by (simp add: scaleR_left_distrib)
himmelma@33175
   273
himmelma@33175
   274
lemma pth_9:
himmelma@33175
   275
  fixes x :: "'a::real_normed_vector" shows
himmelma@33175
   276
  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
himmelma@33175
   277
  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
himmelma@33175
   278
  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
himmelma@33175
   279
  by (simp_all add: algebra_simps)
himmelma@33175
   280
himmelma@33175
   281
lemma pth_a:
himmelma@33175
   282
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   283
  shows "scaleR 0 x + y == y" by simp
himmelma@33175
   284
himmelma@33175
   285
lemma pth_b:
himmelma@33175
   286
  fixes x :: "'a::real_normed_vector" shows
himmelma@33175
   287
  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
himmelma@33175
   288
  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
himmelma@33175
   289
  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
himmelma@33175
   290
  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
himmelma@33175
   291
  by (simp_all add: algebra_simps)
himmelma@33175
   292
himmelma@33175
   293
lemma pth_c:
himmelma@33175
   294
  fixes x :: "'a::real_normed_vector" shows
himmelma@33175
   295
  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
himmelma@33175
   296
  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
himmelma@33175
   297
  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
himmelma@33175
   298
  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
himmelma@33175
   299
  by (simp_all add: algebra_simps)
himmelma@33175
   300
himmelma@33175
   301
lemma pth_d:
himmelma@33175
   302
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   303
  shows "x + 0 == x" by simp
himmelma@33175
   304
himmelma@33175
   305
lemma norm_imp_pos_and_ge:
himmelma@33175
   306
  fixes x :: "'a::real_normed_vector"
himmelma@33175
   307
  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
himmelma@33175
   308
  by atomize auto
himmelma@33175
   309
himmelma@33175
   310
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
himmelma@33175
   311
himmelma@33175
   312
lemma norm_pths:
himmelma@33175
   313
  fixes x :: "'a::real_normed_vector" shows
himmelma@33175
   314
  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
himmelma@33175
   315
  "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
himmelma@33175
   316
  using norm_ge_zero[of "x - y"] by auto
himmelma@33175
   317
himmelma@33175
   318
use "normarith.ML"
himmelma@33175
   319
himmelma@33175
   320
method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
himmelma@33175
   321
*} "Proves simple linear statements about vector norms"
himmelma@33175
   322
himmelma@33175
   323
himmelma@33175
   324
text{* Hence more metric properties. *}
himmelma@33175
   325
himmelma@33175
   326
lemma dist_triangle_alt:
himmelma@33175
   327
  fixes x y z :: "'a::metric_space"
himmelma@33175
   328
  shows "dist y z <= dist x y + dist x z"
huffman@36585
   329
by (rule dist_triangle3)
himmelma@33175
   330
himmelma@33175
   331
lemma dist_pos_lt:
himmelma@33175
   332
  fixes x y :: "'a::metric_space"
himmelma@33175
   333
  shows "x \<noteq> y ==> 0 < dist x y"
himmelma@33175
   334
by (simp add: zero_less_dist_iff)
himmelma@33175
   335
himmelma@33175
   336
lemma dist_nz:
himmelma@33175
   337
  fixes x y :: "'a::metric_space"
himmelma@33175
   338
  shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
himmelma@33175
   339
by (simp add: zero_less_dist_iff)
himmelma@33175
   340
himmelma@33175
   341
lemma dist_triangle_le:
himmelma@33175
   342
  fixes x y z :: "'a::metric_space"
himmelma@33175
   343
  shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
himmelma@33175
   344
by (rule order_trans [OF dist_triangle2])
himmelma@33175
   345
himmelma@33175
   346
lemma dist_triangle_lt:
himmelma@33175
   347
  fixes x y z :: "'a::metric_space"
himmelma@33175
   348
  shows "dist x z + dist y z < e ==> dist x y < e"
himmelma@33175
   349
by (rule le_less_trans [OF dist_triangle2])
himmelma@33175
   350
himmelma@33175
   351
lemma dist_triangle_half_l:
himmelma@33175
   352
  fixes x1 x2 y :: "'a::metric_space"
himmelma@33175
   353
  shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
himmelma@33175
   354
by (rule dist_triangle_lt [where z=y], simp)
himmelma@33175
   355
himmelma@33175
   356
lemma dist_triangle_half_r:
himmelma@33175
   357
  fixes x1 x2 y :: "'a::metric_space"
himmelma@33175
   358
  shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
himmelma@33175
   359
by (rule dist_triangle_half_l, simp_all add: dist_commute)
himmelma@33175
   360
himmelma@35172
   361
himmelma@35172
   362
lemma norm_triangle_half_r:
himmelma@35172
   363
  shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
huffman@36587
   364
  using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
himmelma@35172
   365
himmelma@35172
   366
lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2" 
himmelma@35172
   367
  shows "norm (x - x') < e"
huffman@36587
   368
  using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]]
huffman@36587
   369
  unfolding dist_norm[THEN sym] .
himmelma@35172
   370
himmelma@35172
   371
lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e"
himmelma@35172
   372
  by (metis order_trans norm_triangle_ineq)
himmelma@35172
   373
himmelma@35172
   374
lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
himmelma@35172
   375
  by (metis basic_trans_rules(21) norm_triangle_ineq)
himmelma@35172
   376
himmelma@33175
   377
lemma dist_triangle_add:
himmelma@33175
   378
  fixes x y x' y' :: "'a::real_normed_vector"
himmelma@33175
   379
  shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
himmelma@33175
   380
  by norm
himmelma@33175
   381
himmelma@33175
   382
lemma dist_triangle_add_half:
himmelma@33175
   383
  fixes x x' y y' :: "'a::real_normed_vector"
himmelma@33175
   384
  shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
himmelma@33175
   385
  by norm
himmelma@33175
   386
himmelma@33175
   387
lemma setsum_clauses:
himmelma@33175
   388
  shows "setsum f {} = 0"
himmelma@33175
   389
  and "finite S \<Longrightarrow> setsum f (insert x S) =
himmelma@33175
   390
                 (if x \<in> S then setsum f S else f x + setsum f S)"
himmelma@33175
   391
  by (auto simp add: insert_absorb)
himmelma@33175
   392
himmelma@33175
   393
lemma setsum_norm:
himmelma@33175
   394
  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
himmelma@33175
   395
  assumes fS: "finite S"
himmelma@33175
   396
  shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
himmelma@33175
   397
proof(induct rule: finite_induct[OF fS])
himmelma@33175
   398
  case 1 thus ?case by simp
himmelma@33175
   399
next
himmelma@33175
   400
  case (2 x S)
himmelma@33175
   401
  from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
himmelma@33175
   402
  also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S"
himmelma@33175
   403
    using "2.hyps" by simp
himmelma@33175
   404
  finally  show ?case  using "2.hyps" by simp
himmelma@33175
   405
qed
himmelma@33175
   406
himmelma@33175
   407
lemma setsum_norm_le:
himmelma@33175
   408
  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
himmelma@33175
   409
  assumes fS: "finite S"
himmelma@33175
   410
  and fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
himmelma@33175
   411
  shows "norm (setsum f S) \<le> setsum g S"
himmelma@33175
   412
proof-
himmelma@33175
   413
  from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S"
himmelma@33175
   414
    by - (rule setsum_mono, simp)
himmelma@33175
   415
  then show ?thesis using setsum_norm[OF fS, of f] fg
himmelma@33175
   416
    by arith
himmelma@33175
   417
qed
himmelma@33175
   418
himmelma@33175
   419
lemma setsum_norm_bound:
himmelma@33175
   420
  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
himmelma@33175
   421
  assumes fS: "finite S"
himmelma@33175
   422
  and K: "\<forall>x \<in> S. norm (f x) \<le> K"
himmelma@33175
   423
  shows "norm (setsum f S) \<le> of_nat (card S) * K"
himmelma@33175
   424
  using setsum_norm_le[OF fS K] setsum_constant[symmetric]
himmelma@33175
   425
  by simp
himmelma@33175
   426
himmelma@33175
   427
lemma setsum_group:
himmelma@33175
   428
  assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
himmelma@33175
   429
  shows "setsum (\<lambda>y. setsum g {x. x\<in> S \<and> f x = y}) T = setsum g S"
hoelzl@37489
   430
  apply (subst setsum_image_gen[OF fS, of g f])
hoelzl@37489
   431
  apply (rule setsum_mono_zero_right[OF fT fST])
hoelzl@37489
   432
  by (auto intro: setsum_0')
himmelma@33175
   433
huffman@36585
   434
lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = setsum (\<lambda>x. f x \<bullet> y) S "
himmelma@35542
   435
  apply(induct rule: finite_induct) by(auto simp add: inner_simps)
himmelma@35542
   436
huffman@36585
   437
lemma dot_rsum: "finite S \<Longrightarrow> y \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
himmelma@35542
   438
  apply(induct rule: finite_induct) by(auto simp add: inner_simps)
himmelma@33175
   439
huffman@36585
   440
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
huffman@36585
   441
proof
huffman@36585
   442
  assume "\<forall>x. x \<bullet> y = x \<bullet> z"
huffman@36585
   443
  hence "\<forall>x. x \<bullet> (y - z) = 0" by (simp add: inner_simps)
huffman@36585
   444
  hence "(y - z) \<bullet> (y - z) = 0" ..
huffman@36585
   445
  thus "y = z" by simp
huffman@36585
   446
qed simp
huffman@36585
   447
huffman@36585
   448
lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"
huffman@36585
   449
proof
huffman@36585
   450
  assume "\<forall>z. x \<bullet> z = y \<bullet> z"
huffman@36585
   451
  hence "\<forall>z. (x - y) \<bullet> z = 0" by (simp add: inner_simps)
huffman@36585
   452
  hence "(x - y) \<bullet> (x - y) = 0" ..
huffman@36585
   453
  thus "x = y" by simp
huffman@36585
   454
qed simp
himmelma@33175
   455
himmelma@33175
   456
subsection{* Orthogonality. *}
himmelma@33175
   457
hoelzl@37489
   458
context real_inner
hoelzl@37489
   459
begin
hoelzl@37489
   460
himmelma@33175
   461
definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)"
himmelma@33175
   462
himmelma@33175
   463
lemma orthogonal_clauses:
huffman@36588
   464
  "orthogonal a 0"
hoelzl@37489
   465
  "orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"
hoelzl@37489
   466
  "orthogonal a x \<Longrightarrow> orthogonal a (-x)"
hoelzl@37489
   467
  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)"
hoelzl@37489
   468
  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x - y)"
himmelma@33175
   469
  "orthogonal 0 a"
hoelzl@37489
   470
  "orthogonal x a \<Longrightarrow> orthogonal (c *\<^sub>R x) a"
hoelzl@37489
   471
  "orthogonal x a \<Longrightarrow> orthogonal (-x) a"
hoelzl@37489
   472
  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
hoelzl@37489
   473
  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
haftmann@37606
   474
  unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto
haftmann@37606
   475
 
hoelzl@37489
   476
end
hoelzl@37489
   477
huffman@36585
   478
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
himmelma@35542
   479
  by (simp add: orthogonal_def inner_commute)
himmelma@33175
   480
himmelma@33175
   481
subsection{* Linear functions. *}
himmelma@33175
   482
huffman@36593
   483
definition
huffman@36593
   484
  linear :: "('a::real_vector \<Rightarrow> 'b::real_vector) \<Rightarrow> bool" where
huffman@36593
   485
  "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *\<^sub>R x) = c *\<^sub>R f x)"
huffman@36593
   486
huffman@36593
   487
lemma linearI: assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
hoelzl@33714
   488
  shows "linear f" using assms unfolding linear_def by auto
hoelzl@33714
   489
huffman@36593
   490
lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. c *\<^sub>R f x)"
huffman@36593
   491
  by (simp add: linear_def algebra_simps)
huffman@36593
   492
huffman@36593
   493
lemma linear_compose_neg: "linear f ==> linear (\<lambda>x. -(f(x)))"
huffman@36593
   494
  by (simp add: linear_def)
huffman@36593
   495
huffman@36593
   496
lemma linear_compose_add: "linear f \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))"
huffman@36593
   497
  by (simp add: linear_def algebra_simps)
huffman@36593
   498
huffman@36593
   499
lemma linear_compose_sub: "linear f \<Longrightarrow> linear g ==> linear (\<lambda>x. f x - g x)"
huffman@36593
   500
  by (simp add: linear_def algebra_simps)
himmelma@33175
   501
himmelma@33175
   502
lemma linear_compose: "linear f \<Longrightarrow> linear g ==> linear (g o f)"
himmelma@33175
   503
  by (simp add: linear_def)
himmelma@33175
   504
himmelma@33175
   505
lemma linear_id: "linear id" by (simp add: linear_def id_def)
himmelma@33175
   506
huffman@36593
   507
lemma linear_zero: "linear (\<lambda>x. 0)" by (simp add: linear_def)
himmelma@33175
   508
himmelma@33175
   509
lemma linear_compose_setsum:
huffman@36593
   510
  assumes fS: "finite S" and lS: "\<forall>a \<in> S. linear (f a)"
huffman@36593
   511
  shows "linear(\<lambda>x. setsum (\<lambda>a. f a x) S)"
himmelma@33175
   512
  using lS
himmelma@33175
   513
  apply (induct rule: finite_induct[OF fS])
himmelma@33175
   514
  by (auto simp add: linear_zero intro: linear_compose_add)
himmelma@33175
   515
hoelzl@37489
   516
lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
himmelma@33175
   517
  unfolding linear_def
himmelma@33175
   518
  apply clarsimp
himmelma@33175
   519
  apply (erule allE[where x="0::'a"])
himmelma@33175
   520
  apply simp
himmelma@33175
   521
  done
himmelma@33175
   522
huffman@36593
   523
lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" by (simp add: linear_def)
huffman@36593
   524
huffman@36593
   525
lemma linear_neg: "linear f ==> f (-x) = - f x"
huffman@36593
   526
  using linear_cmul [where c="-1"] by simp
himmelma@33175
   527
himmelma@33175
   528
lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def)
himmelma@33175
   529
huffman@36593
   530
lemma linear_sub: "linear f ==> f(x - y) = f x - f y"
haftmann@37887
   531
  by (simp add: diff_minus linear_add linear_neg)
himmelma@33175
   532
himmelma@33175
   533
lemma linear_setsum:
himmelma@33175
   534
  assumes lf: "linear f" and fS: "finite S"
himmelma@33175
   535
  shows "f (setsum g S) = setsum (f o g) S"
himmelma@33175
   536
proof (induct rule: finite_induct[OF fS])
himmelma@33175
   537
  case 1 thus ?case by (simp add: linear_0[OF lf])
himmelma@33175
   538
next
himmelma@33175
   539
  case (2 x F)
himmelma@33175
   540
  have "f (setsum g (insert x F)) = f (g x + setsum g F)" using "2.hyps"
himmelma@33175
   541
    by simp
himmelma@33175
   542
  also have "\<dots> = f (g x) + f (setsum g F)" using linear_add[OF lf] by simp
himmelma@33175
   543
  also have "\<dots> = setsum (f o g) (insert x F)" using "2.hyps" by simp
himmelma@33175
   544
  finally show ?case .
himmelma@33175
   545
qed
himmelma@33175
   546
himmelma@33175
   547
lemma linear_setsum_mul:
himmelma@33175
   548
  assumes lf: "linear f" and fS: "finite S"
huffman@36593
   549
  shows "f (setsum (\<lambda>i. c i *\<^sub>R v i) S) = setsum (\<lambda>i. c i *\<^sub>R f (v i)) S"
huffman@36593
   550
  using linear_setsum[OF lf fS, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def]
himmelma@33175
   551
  linear_cmul[OF lf] by simp
himmelma@33175
   552
himmelma@33175
   553
lemma linear_injective_0:
huffman@36593
   554
  assumes lf: "linear f"
himmelma@33175
   555
  shows "inj f \<longleftrightarrow> (\<forall>x. f x = 0 \<longrightarrow> x = 0)"
himmelma@33175
   556
proof-
himmelma@33175
   557
  have "inj f \<longleftrightarrow> (\<forall> x y. f x = f y \<longrightarrow> x = y)" by (simp add: inj_on_def)
himmelma@33175
   558
  also have "\<dots> \<longleftrightarrow> (\<forall> x y. f x - f y = 0 \<longrightarrow> x - y = 0)" by simp
himmelma@33175
   559
  also have "\<dots> \<longleftrightarrow> (\<forall> x y. f (x - y) = 0 \<longrightarrow> x - y = 0)"
himmelma@33175
   560
    by (simp add: linear_sub[OF lf])
himmelma@33175
   561
  also have "\<dots> \<longleftrightarrow> (\<forall> x. f x = 0 \<longrightarrow> x = 0)" by auto
himmelma@33175
   562
  finally show ?thesis .
himmelma@33175
   563
qed
himmelma@33175
   564
himmelma@33175
   565
subsection{* Bilinear functions. *}
himmelma@33175
   566
himmelma@33175
   567
definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))"
himmelma@33175
   568
himmelma@33175
   569
lemma bilinear_ladd: "bilinear h ==> h (x + y) z = (h x z) + (h y z)"
himmelma@33175
   570
  by (simp add: bilinear_def linear_def)
himmelma@33175
   571
lemma bilinear_radd: "bilinear h ==> h x (y + z) = (h x y) + (h x z)"
himmelma@33175
   572
  by (simp add: bilinear_def linear_def)
himmelma@33175
   573
huffman@36593
   574
lemma bilinear_lmul: "bilinear h ==> h (c *\<^sub>R x) y = c *\<^sub>R (h x y)"
himmelma@33175
   575
  by (simp add: bilinear_def linear_def)
himmelma@33175
   576
huffman@36593
   577
lemma bilinear_rmul: "bilinear h ==> h x (c *\<^sub>R y) = c *\<^sub>R (h x y)"
himmelma@33175
   578
  by (simp add: bilinear_def linear_def)
himmelma@33175
   579
huffman@36593
   580
lemma bilinear_lneg: "bilinear h ==> h (- x) y = -(h x y)"
huffman@36593
   581
  by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul)
huffman@36593
   582
huffman@36593
   583
lemma bilinear_rneg: "bilinear h ==> h x (- y) = - h x y"
huffman@36593
   584
  by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul)
himmelma@33175
   585
himmelma@33175
   586
lemma  (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
himmelma@33175
   587
  using add_imp_eq[of x y 0] by auto
himmelma@33175
   588
himmelma@33175
   589
lemma bilinear_lzero:
huffman@36593
   590
  assumes bh: "bilinear h" shows "h 0 x = 0"
himmelma@33175
   591
  using bilinear_ladd[OF bh, of 0 0 x]
haftmann@36350
   592
    by (simp add: eq_add_iff field_simps)
himmelma@33175
   593
himmelma@33175
   594
lemma bilinear_rzero:
huffman@36593
   595
  assumes bh: "bilinear h" shows "h x 0 = 0"
himmelma@33175
   596
  using bilinear_radd[OF bh, of x 0 0 ]
haftmann@36350
   597
    by (simp add: eq_add_iff field_simps)
himmelma@33175
   598
huffman@36593
   599
lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z"
haftmann@37887
   600
  by (simp  add: diff_minus bilinear_ladd bilinear_lneg)
himmelma@33175
   601
huffman@36593
   602
lemma bilinear_rsub: "bilinear h ==> h z (x - y) = h z x - h z y"
haftmann@37887
   603
  by (simp  add: diff_minus bilinear_radd bilinear_rneg)
himmelma@33175
   604
himmelma@33175
   605
lemma bilinear_setsum:
himmelma@33175
   606
  assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T"
himmelma@33175
   607
  shows "h (setsum f S) (setsum g T) = setsum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
himmelma@33175
   608
proof-
himmelma@33175
   609
  have "h (setsum f S) (setsum g T) = setsum (\<lambda>x. h (f x) (setsum g T)) S"
himmelma@33175
   610
    apply (rule linear_setsum[unfolded o_def])
himmelma@33175
   611
    using bh fS by (auto simp add: bilinear_def)
himmelma@33175
   612
  also have "\<dots> = setsum (\<lambda>x. setsum (\<lambda>y. h (f x) (g y)) T) S"
himmelma@33175
   613
    apply (rule setsum_cong, simp)
himmelma@33175
   614
    apply (rule linear_setsum[unfolded o_def])
himmelma@33175
   615
    using bh fT by (auto simp add: bilinear_def)
himmelma@33175
   616
  finally show ?thesis unfolding setsum_cartesian_product .
himmelma@33175
   617
qed
himmelma@33175
   618
himmelma@33175
   619
subsection{* Adjoints. *}
himmelma@33175
   620
himmelma@33175
   621
definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
himmelma@33175
   622
huffman@36596
   623
lemma adjoint_unique:
huffman@36596
   624
  assumes "\<forall>x y. inner (f x) y = inner x (g y)"
huffman@36596
   625
  shows "adjoint f = g"
huffman@36596
   626
unfolding adjoint_def
huffman@36596
   627
proof (rule some_equality)
huffman@36596
   628
  show "\<forall>x y. inner (f x) y = inner x (g y)" using assms .
huffman@36596
   629
next
huffman@36596
   630
  fix h assume "\<forall>x y. inner (f x) y = inner x (h y)"
huffman@36596
   631
  hence "\<forall>x y. inner x (g y) = inner x (h y)" using assms by simp
huffman@36596
   632
  hence "\<forall>x y. inner x (g y - h y) = 0" by (simp add: inner_diff_right)
huffman@36596
   633
  hence "\<forall>y. inner (g y - h y) (g y - h y) = 0" by simp
huffman@36596
   634
  hence "\<forall>y. h y = g y" by simp
huffman@36596
   635
  thus "h = g" by (simp add: ext)
huffman@36596
   636
qed
huffman@36596
   637
himmelma@33175
   638
lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis
himmelma@33175
   639
himmelma@33175
   640
subsection{* Interlude: Some properties of real sets *}
himmelma@33175
   641
himmelma@33175
   642
lemma seq_mono_lemma: assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n" and "\<forall>n \<ge> m. e n <= e m"
himmelma@33175
   643
  shows "\<forall>n \<ge> m. d n < e m"
himmelma@33175
   644
  using prems apply auto
himmelma@33175
   645
  apply (erule_tac x="n" in allE)
himmelma@33175
   646
  apply (erule_tac x="n" in allE)
himmelma@33175
   647
  apply auto
himmelma@33175
   648
  done
himmelma@33175
   649
himmelma@33175
   650
himmelma@33175
   651
lemma infinite_enumerate: assumes fS: "infinite S"
himmelma@33175
   652
  shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
himmelma@33175
   653
unfolding subseq_def
himmelma@33175
   654
using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
himmelma@33175
   655
himmelma@33175
   656
lemma approachable_lt_le: "(\<exists>(d::real)>0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
himmelma@33175
   657
apply auto
himmelma@33175
   658
apply (rule_tac x="d/2" in exI)
himmelma@33175
   659
apply auto
himmelma@33175
   660
done
himmelma@33175
   661
himmelma@33175
   662
himmelma@33175
   663
lemma triangle_lemma:
himmelma@33175
   664
  assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2"
himmelma@33175
   665
  shows "x <= y + z"
himmelma@33175
   666
proof-
huffman@36362
   667
  have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg)
haftmann@36350
   668
  with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps)
himmelma@33175
   669
  from y z have yz: "y + z \<ge> 0" by arith
himmelma@33175
   670
  from power2_le_imp_le[OF th yz] show ?thesis .
himmelma@33175
   671
qed
himmelma@33175
   672
himmelma@33175
   673
text {* TODO: move to NthRoot *}
himmelma@33175
   674
lemma sqrt_add_le_add_sqrt:
himmelma@33175
   675
  assumes x: "0 \<le> x" and y: "0 \<le> y"
himmelma@33175
   676
  shows "sqrt (x + y) \<le> sqrt x + sqrt y"
himmelma@33175
   677
apply (rule power2_le_imp_le)
himmelma@33175
   678
apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y)
himmelma@33175
   679
apply (simp add: mult_nonneg_nonneg x y)
himmelma@33175
   680
apply (simp add: add_nonneg_nonneg x y)
himmelma@33175
   681
done
himmelma@33175
   682
himmelma@33175
   683
subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
himmelma@33175
   684
himmelma@33175
   685
definition hull :: "'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where
himmelma@33175
   686
  "S hull s = Inter {t. t \<in> S \<and> s \<subseteq> t}"
himmelma@33175
   687
himmelma@33175
   688
lemma hull_same: "s \<in> S \<Longrightarrow> S hull s = s"
himmelma@33175
   689
  unfolding hull_def by auto
himmelma@33175
   690
himmelma@33175
   691
lemma hull_in: "(\<And>T. T \<subseteq> S ==> Inter T \<in> S) ==> (S hull s) \<in> S"
himmelma@33175
   692
unfolding hull_def subset_iff by auto
himmelma@33175
   693
himmelma@33175
   694
lemma hull_eq: "(\<And>T. T \<subseteq> S ==> Inter T \<in> S) ==> (S hull s) = s \<longleftrightarrow> s \<in> S"
himmelma@33175
   695
using hull_same[of s S] hull_in[of S s] by metis
himmelma@33175
   696
himmelma@33175
   697
himmelma@33175
   698
lemma hull_hull: "S hull (S hull s) = S hull s"
himmelma@33175
   699
  unfolding hull_def by blast
himmelma@33175
   700
hoelzl@34964
   701
lemma hull_subset[intro]: "s \<subseteq> (S hull s)"
himmelma@33175
   702
  unfolding hull_def by blast
himmelma@33175
   703
himmelma@33175
   704
lemma hull_mono: " s \<subseteq> t ==> (S hull s) \<subseteq> (S hull t)"
himmelma@33175
   705
  unfolding hull_def by blast
himmelma@33175
   706
himmelma@33175
   707
lemma hull_antimono: "S \<subseteq> T ==> (T hull s) \<subseteq> (S hull s)"
himmelma@33175
   708
  unfolding hull_def by blast
himmelma@33175
   709
himmelma@33175
   710
lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> t \<in> S ==> (S hull s) \<subseteq> t"
himmelma@33175
   711
  unfolding hull_def by blast
himmelma@33175
   712
himmelma@33175
   713
lemma subset_hull: "t \<in> S ==> S hull s \<subseteq> t \<longleftrightarrow>  s \<subseteq> t"
himmelma@33175
   714
  unfolding hull_def by blast
himmelma@33175
   715
himmelma@33175
   716
lemma hull_unique: "s \<subseteq> t \<Longrightarrow> t \<in> S \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> t' \<in> S ==> t \<subseteq> t')
himmelma@33175
   717
           ==> (S hull s = t)"
himmelma@33175
   718
unfolding hull_def by auto
himmelma@33175
   719
himmelma@33175
   720
lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"
himmelma@33175
   721
  using hull_minimal[of S "{x. P x}" Q]
himmelma@33175
   722
  by (auto simp add: subset_eq Collect_def mem_def)
himmelma@33175
   723
himmelma@33175
   724
lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S" by (metis hull_subset subset_eq)
himmelma@33175
   725
himmelma@33175
   726
lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
himmelma@33175
   727
unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
himmelma@33175
   728
himmelma@33175
   729
lemma hull_union: assumes T: "\<And>T. T \<subseteq> S ==> Inter T \<in> S"
himmelma@33175
   730
  shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
himmelma@33175
   731
apply rule
himmelma@33175
   732
apply (rule hull_mono)
himmelma@33175
   733
unfolding Un_subset_iff
himmelma@33175
   734
apply (metis hull_subset Un_upper1 Un_upper2 subset_trans)
himmelma@33175
   735
apply (rule hull_minimal)
himmelma@33175
   736
apply (metis hull_union_subset)
himmelma@33175
   737
apply (metis hull_in T)
himmelma@33175
   738
done
himmelma@33175
   739
himmelma@33175
   740
lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> (S hull (insert a s) = S hull s)"
himmelma@33175
   741
  unfolding hull_def by blast
himmelma@33175
   742
himmelma@33175
   743
lemma hull_redundant: "a \<in> (S hull s) ==> (S hull (insert a s) = S hull s)"
himmelma@33175
   744
by (metis hull_redundant_eq)
himmelma@33175
   745
himmelma@33175
   746
text{* Archimedian properties and useful consequences. *}
himmelma@33175
   747
himmelma@33175
   748
lemma real_arch_simple: "\<exists>n. x <= real (n::nat)"
himmelma@33175
   749
  using reals_Archimedean2[of x] apply auto by (rule_tac x="Suc n" in exI, auto)
himmelma@33175
   750
lemmas real_arch_lt = reals_Archimedean2
himmelma@33175
   751
himmelma@33175
   752
lemmas real_arch = reals_Archimedean3
himmelma@33175
   753
himmelma@33175
   754
lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
himmelma@33175
   755
  using reals_Archimedean
huffman@36362
   756
  apply (auto simp add: field_simps)
himmelma@33175
   757
  apply (subgoal_tac "inverse (real n) > 0")
himmelma@33175
   758
  apply arith
himmelma@33175
   759
  apply simp
himmelma@33175
   760
  done
himmelma@33175
   761
himmelma@33175
   762
lemma real_pow_lbound: "0 <= x ==> 1 + real n * x <= (1 + x) ^ n"
himmelma@33175
   763
proof(induct n)
himmelma@33175
   764
  case 0 thus ?case by simp
himmelma@33175
   765
next
himmelma@33175
   766
  case (Suc n)
himmelma@33175
   767
  hence h: "1 + real n * x \<le> (1 + x) ^ n" by simp
himmelma@33175
   768
  from h have p: "1 \<le> (1 + x) ^ n" using Suc.prems by simp
himmelma@33175
   769
  from h have "1 + real n * x + x \<le> (1 + x) ^ n + x" by simp
himmelma@33175
   770
  also have "\<dots> \<le> (1 + x) ^ Suc n" apply (subst diff_le_0_iff_le[symmetric])
haftmann@36350
   771
    apply (simp add: field_simps)
himmelma@33175
   772
    using mult_left_mono[OF p Suc.prems] by simp
haftmann@36350
   773
  finally show ?case  by (simp add: real_of_nat_Suc field_simps)
himmelma@33175
   774
qed
himmelma@33175
   775
himmelma@33175
   776
lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\<exists>n. y < x^n"
himmelma@33175
   777
proof-
himmelma@33175
   778
  from x have x0: "x - 1 > 0" by arith
himmelma@33175
   779
  from real_arch[OF x0, rule_format, of y]
himmelma@33175
   780
  obtain n::nat where n:"y < real n * (x - 1)" by metis
himmelma@33175
   781
  from x0 have x00: "x- 1 \<ge> 0" by arith
himmelma@33175
   782
  from real_pow_lbound[OF x00, of n] n
himmelma@33175
   783
  have "y < x^n" by auto
himmelma@33175
   784
  then show ?thesis by metis
himmelma@33175
   785
qed
himmelma@33175
   786
himmelma@33175
   787
lemma real_arch_pow2: "\<exists>n. (x::real) < 2^ n"
himmelma@33175
   788
  using real_arch_pow[of 2 x] by simp
himmelma@33175
   789
himmelma@33175
   790
lemma real_arch_pow_inv: assumes y: "(y::real) > 0" and x1: "x < 1"
himmelma@33175
   791
  shows "\<exists>n. x^n < y"
himmelma@33175
   792
proof-
himmelma@33175
   793
  {assume x0: "x > 0"
himmelma@33175
   794
    from x0 x1 have ix: "1 < 1/x" by (simp add: field_simps)
himmelma@33175
   795
    from real_arch_pow[OF ix, of "1/y"]
himmelma@33175
   796
    obtain n where n: "1/y < (1/x)^n" by blast
himmelma@33175
   797
    then
himmelma@33175
   798
    have ?thesis using y x0 by (auto simp add: field_simps power_divide) }
himmelma@33175
   799
  moreover
himmelma@33175
   800
  {assume "\<not> x > 0" with y x1 have ?thesis apply auto by (rule exI[where x=1], auto)}
himmelma@33175
   801
  ultimately show ?thesis by metis
himmelma@33175
   802
qed
himmelma@33175
   803
himmelma@33175
   804
lemma forall_pos_mono: "(\<And>d e::real. d < e \<Longrightarrow> P d ==> P e) \<Longrightarrow> (\<And>n::nat. n \<noteq> 0 ==> P(inverse(real n))) \<Longrightarrow> (\<And>e. 0 < e ==> P e)"
himmelma@33175
   805
  by (metis real_arch_inv)
himmelma@33175
   806
himmelma@33175
   807
lemma forall_pos_mono_1: "(\<And>d e::real. d < e \<Longrightarrow> P d ==> P e) \<Longrightarrow> (\<And>n. P(inverse(real (Suc n)))) ==> 0 < e ==> P e"
himmelma@33175
   808
  apply (rule forall_pos_mono)
himmelma@33175
   809
  apply auto
himmelma@33175
   810
  apply (atomize)
himmelma@33175
   811
  apply (erule_tac x="n - 1" in allE)
himmelma@33175
   812
  apply auto
himmelma@33175
   813
  done
himmelma@33175
   814
himmelma@33175
   815
lemma real_archimedian_rdiv_eq_0: assumes x0: "x \<ge> 0" and c: "c \<ge> 0" and xc: "\<forall>(m::nat)>0. real m * x \<le> c"
himmelma@33175
   816
  shows "x = 0"
himmelma@33175
   817
proof-
himmelma@33175
   818
  {assume "x \<noteq> 0" with x0 have xp: "x > 0" by arith
himmelma@33175
   819
    from real_arch[OF xp, rule_format, of c] obtain n::nat where n: "c < real n * x"  by blast
himmelma@33175
   820
    with xc[rule_format, of n] have "n = 0" by arith
himmelma@33175
   821
    with n c have False by simp}
himmelma@33175
   822
  then show ?thesis by blast
himmelma@33175
   823
qed
himmelma@33175
   824
huffman@36666
   825
subsection {* Geometric progression *}
himmelma@33175
   826
himmelma@33175
   827
lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
himmelma@33175
   828
  (is "?lhs = ?rhs")
himmelma@33175
   829
proof-
himmelma@33175
   830
  {assume x1: "x = 1" hence ?thesis by simp}
himmelma@33175
   831
  moreover
himmelma@33175
   832
  {assume x1: "x\<noteq>1"
himmelma@33175
   833
    hence x1': "x - 1 \<noteq> 0" "1 - x \<noteq> 0" "x - 1 = - (1 - x)" "- (1 - x) \<noteq> 0" by auto
himmelma@33175
   834
    from geometric_sum[OF x1, of "Suc n", unfolded x1']
himmelma@33175
   835
    have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
himmelma@33175
   836
      unfolding atLeastLessThanSuc_atLeastAtMost
haftmann@36350
   837
      using x1' apply (auto simp only: field_simps)
haftmann@36350
   838
      apply (simp add: field_simps)
himmelma@33175
   839
      done
haftmann@36350
   840
    then have ?thesis by (simp add: field_simps) }
himmelma@33175
   841
  ultimately show ?thesis by metis
himmelma@33175
   842
qed
himmelma@33175
   843
himmelma@33175
   844
lemma sum_gp_multiplied: assumes mn: "m <= n"
himmelma@33175
   845
  shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
himmelma@33175
   846
  (is "?lhs = ?rhs")
himmelma@33175
   847
proof-
himmelma@33175
   848
  let ?S = "{0..(n - m)}"
himmelma@33175
   849
  from mn have mn': "n - m \<ge> 0" by arith
himmelma@33175
   850
  let ?f = "op + m"
himmelma@33175
   851
  have i: "inj_on ?f ?S" unfolding inj_on_def by auto
himmelma@33175
   852
  have f: "?f ` ?S = {m..n}"
himmelma@33175
   853
    using mn apply (auto simp add: image_iff Bex_def) by arith
himmelma@33175
   854
  have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
himmelma@33175
   855
    by (rule ext, simp add: power_add power_mult)
himmelma@33175
   856
  from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
himmelma@33175
   857
  have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
himmelma@33175
   858
  then show ?thesis unfolding sum_gp_basic using mn
haftmann@36350
   859
    by (simp add: field_simps power_add[symmetric])
himmelma@33175
   860
qed
himmelma@33175
   861
himmelma@33175
   862
lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
himmelma@33175
   863
   (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
himmelma@33175
   864
                    else (x^ m - x^ (Suc n)) / (1 - x))"
himmelma@33175
   865
proof-
himmelma@33175
   866
  {assume nm: "n < m" hence ?thesis by simp}
himmelma@33175
   867
  moreover
himmelma@33175
   868
  {assume "\<not> n < m" hence nm: "m \<le> n" by arith
himmelma@33175
   869
    {assume x: "x = 1"  hence ?thesis by simp}
himmelma@33175
   870
    moreover
himmelma@33175
   871
    {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
haftmann@36350
   872
      from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
himmelma@33175
   873
    ultimately have ?thesis by metis
himmelma@33175
   874
  }
himmelma@33175
   875
  ultimately show ?thesis by metis
himmelma@33175
   876
qed
himmelma@33175
   877
himmelma@33175
   878
lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
himmelma@33175
   879
  (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
himmelma@33175
   880
  unfolding sum_gp[of x m "m + n"] power_Suc
haftmann@36350
   881
  by (simp add: field_simps power_add)
himmelma@33175
   882
himmelma@33175
   883
himmelma@33175
   884
subsection{* A bit of linear algebra. *}
himmelma@33175
   885
hoelzl@37489
   886
definition (in real_vector)
hoelzl@37489
   887
  subspace :: "'a set \<Rightarrow> bool" where
huffman@36593
   888
  "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x\<in> S. \<forall>y \<in>S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in>S. c *\<^sub>R x \<in>S )"
huffman@36593
   889
hoelzl@37489
   890
definition (in real_vector) "span S = (subspace hull S)"
hoelzl@37489
   891
definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span(S - {a}))"
hoelzl@37489
   892
abbreviation (in real_vector) "independent s == ~(dependent s)"
himmelma@33175
   893
huffman@36666
   894
text {* Closure properties of subspaces. *}
himmelma@33175
   895
himmelma@33175
   896
lemma subspace_UNIV[simp]: "subspace(UNIV)" by (simp add: subspace_def)
himmelma@33175
   897
hoelzl@37489
   898
lemma (in real_vector) subspace_0: "subspace S ==> 0 \<in> S" by (metis subspace_def)
hoelzl@37489
   899
hoelzl@37489
   900
lemma (in real_vector) subspace_add: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S ==> x + y \<in> S"
himmelma@33175
   901
  by (metis subspace_def)
himmelma@33175
   902
hoelzl@37489
   903
lemma (in real_vector) subspace_mul: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> c *\<^sub>R x \<in> S"
himmelma@33175
   904
  by (metis subspace_def)
himmelma@33175
   905
huffman@36593
   906
lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> - x \<in> S"
huffman@36593
   907
  by (metis scaleR_minus1_left subspace_mul)
huffman@36593
   908
huffman@36593
   909
lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
haftmann@37887
   910
  by (metis diff_minus subspace_add subspace_neg)
himmelma@33175
   911
hoelzl@37489
   912
lemma (in real_vector) subspace_setsum:
himmelma@33175
   913
  assumes sA: "subspace A" and fB: "finite B"
himmelma@33175
   914
  and f: "\<forall>x\<in> B. f x \<in> A"
himmelma@33175
   915
  shows "setsum f B \<in> A"
himmelma@33175
   916
  using  fB f sA
himmelma@33175
   917
  apply(induct rule: finite_induct[OF fB])
himmelma@33175
   918
  by (simp add: subspace_def sA, auto simp add: sA subspace_add)
himmelma@33175
   919
himmelma@33175
   920
lemma subspace_linear_image:
huffman@36593
   921
  assumes lf: "linear f" and sS: "subspace S"
himmelma@33175
   922
  shows "subspace(f ` S)"
himmelma@33175
   923
  using lf sS linear_0[OF lf]
himmelma@33175
   924
  unfolding linear_def subspace_def
himmelma@33175
   925
  apply (auto simp add: image_iff)
himmelma@33175
   926
  apply (rule_tac x="x + y" in bexI, auto)
huffman@36593
   927
  apply (rule_tac x="c *\<^sub>R x" in bexI, auto)
himmelma@33175
   928
  done
himmelma@33175
   929
huffman@36593
   930
lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \<in> S}"
himmelma@33175
   931
  by (auto simp add: subspace_def linear_def linear_0[of f])
himmelma@33175
   932
huffman@36593
   933
lemma subspace_trivial: "subspace {0}"
himmelma@33175
   934
  by (simp add: subspace_def)
himmelma@33175
   935
hoelzl@37489
   936
lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B ==> subspace (A \<inter> B)"
himmelma@33175
   937
  by (simp add: subspace_def)
himmelma@33175
   938
hoelzl@37489
   939
lemma (in real_vector) span_mono: "A \<subseteq> B ==> span A \<subseteq> span B"
himmelma@33175
   940
  by (metis span_def hull_mono)
himmelma@33175
   941
hoelzl@37489
   942
lemma (in real_vector) subspace_span: "subspace(span S)"
himmelma@33175
   943
  unfolding span_def
himmelma@33175
   944
  apply (rule hull_in[unfolded mem_def])
himmelma@33175
   945
  apply (simp only: subspace_def Inter_iff Int_iff subset_eq)
himmelma@33175
   946
  apply auto
himmelma@33175
   947
  apply (erule_tac x="X" in ballE)
himmelma@33175
   948
  apply (simp add: mem_def)
himmelma@33175
   949
  apply blast
himmelma@33175
   950
  apply (erule_tac x="X" in ballE)
himmelma@33175
   951
  apply (erule_tac x="X" in ballE)
himmelma@33175
   952
  apply (erule_tac x="X" in ballE)
himmelma@33175
   953
  apply (clarsimp simp add: mem_def)
himmelma@33175
   954
  apply simp
himmelma@33175
   955
  apply simp
himmelma@33175
   956
  apply simp
himmelma@33175
   957
  apply (erule_tac x="X" in ballE)
himmelma@33175
   958
  apply (erule_tac x="X" in ballE)
himmelma@33175
   959
  apply (simp add: mem_def)
himmelma@33175
   960
  apply simp
himmelma@33175
   961
  apply simp
himmelma@33175
   962
  done
himmelma@33175
   963
hoelzl@37489
   964
lemma (in real_vector) span_clauses:
himmelma@33175
   965
  "a \<in> S ==> a \<in> span S"
himmelma@33175
   966
  "0 \<in> span S"
himmelma@33175
   967
  "x\<in> span S \<Longrightarrow> y \<in> span S ==> x + y \<in> span S"
huffman@36593
   968
  "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
huffman@36362
   969
  by (metis span_def hull_subset subset_eq)
huffman@36362
   970
     (metis subspace_span subspace_def)+
himmelma@33175
   971
hoelzl@37489
   972
lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> P x"
himmelma@33175
   973
  and P: "subspace P" and x: "x \<in> span S" shows "P x"
himmelma@33175
   974
proof-
himmelma@33175
   975
  from SP have SP': "S \<subseteq> P" by (simp add: mem_def subset_eq)
himmelma@33175
   976
  from P have P': "P \<in> subspace" by (simp add: mem_def)
himmelma@33175
   977
  from x hull_minimal[OF SP' P', unfolded span_def[symmetric]]
himmelma@33175
   978
  show "P x" by (metis mem_def subset_eq)
himmelma@33175
   979
qed
himmelma@33175
   980
hoelzl@37489
   981
lemma span_empty[simp]: "span {} = {0}"
himmelma@33175
   982
  apply (simp add: span_def)
himmelma@33175
   983
  apply (rule hull_unique)
himmelma@33175
   984
  apply (auto simp add: mem_def subspace_def)
huffman@36593
   985
  unfolding mem_def[of "0::'a", symmetric]
himmelma@33175
   986
  apply simp
himmelma@33175
   987
  done
himmelma@33175
   988
hoelzl@37489
   989
lemma (in real_vector) independent_empty[intro]: "independent {}"
himmelma@33175
   990
  by (simp add: dependent_def)
himmelma@33175
   991
hoelzl@37489
   992
lemma dependent_single[simp]:
hoelzl@37489
   993
  "dependent {x} \<longleftrightarrow> x = 0"
hoelzl@37489
   994
  unfolding dependent_def by auto
hoelzl@37489
   995
hoelzl@37489
   996
lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A ==> independent B"
himmelma@33175
   997
  apply (clarsimp simp add: dependent_def span_mono)
himmelma@33175
   998
  apply (subgoal_tac "span (B - {a}) \<le> span (A - {a})")
himmelma@33175
   999
  apply force
himmelma@33175
  1000
  apply (rule span_mono)
himmelma@33175
  1001
  apply auto
himmelma@33175
  1002
  done
himmelma@33175
  1003
hoelzl@37489
  1004
lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow>  subspace B \<Longrightarrow> span A = B"
himmelma@33175
  1005
  by (metis order_antisym span_def hull_minimal mem_def)
himmelma@33175
  1006
hoelzl@37489
  1007
lemma (in real_vector) span_induct': assumes SP: "\<forall>x \<in> S. P x"
himmelma@33175
  1008
  and P: "subspace P" shows "\<forall>x \<in> span S. P x"
himmelma@33175
  1009
  using span_induct SP P by blast
himmelma@33175
  1010
hoelzl@37489
  1011
inductive (in real_vector) span_induct_alt_help for S:: "'a \<Rightarrow> bool"
himmelma@33175
  1012
  where
himmelma@33175
  1013
  span_induct_alt_help_0: "span_induct_alt_help S 0"
huffman@36593
  1014
  | span_induct_alt_help_S: "x \<in> S \<Longrightarrow> span_induct_alt_help S z \<Longrightarrow> span_induct_alt_help S (c *\<^sub>R x + z)"
himmelma@33175
  1015
himmelma@33175
  1016
lemma span_induct_alt':
huffman@36593
  1017
  assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)" shows "\<forall>x \<in> span S. h x"
himmelma@33175
  1018
proof-
huffman@36593
  1019
  {fix x:: "'a" assume x: "span_induct_alt_help S x"
himmelma@33175
  1020
    have "h x"
himmelma@33175
  1021
      apply (rule span_induct_alt_help.induct[OF x])
himmelma@33175
  1022
      apply (rule h0)
himmelma@33175
  1023
      apply (rule hS, assumption, assumption)
himmelma@33175
  1024
      done}
himmelma@33175
  1025
  note th0 = this
himmelma@33175
  1026
  {fix x assume x: "x \<in> span S"
himmelma@33175
  1027
himmelma@33175
  1028
    have "span_induct_alt_help S x"
himmelma@33175
  1029
      proof(rule span_induct[where x=x and S=S])
himmelma@33175
  1030
        show "x \<in> span S" using x .
himmelma@33175
  1031
      next
himmelma@33175
  1032
        fix x assume xS : "x \<in> S"
himmelma@33175
  1033
          from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1]
himmelma@33175
  1034
          show "span_induct_alt_help S x" by simp
himmelma@33175
  1035
        next
himmelma@33175
  1036
        have "span_induct_alt_help S 0" by (rule span_induct_alt_help_0)
himmelma@33175
  1037
        moreover
himmelma@33175
  1038
        {fix x y assume h: "span_induct_alt_help S x" "span_induct_alt_help S y"
himmelma@33175
  1039
          from h
himmelma@33175
  1040
          have "span_induct_alt_help S (x + y)"
himmelma@33175
  1041
            apply (induct rule: span_induct_alt_help.induct)
himmelma@33175
  1042
            apply simp
himmelma@33175
  1043
            unfolding add_assoc
himmelma@33175
  1044
            apply (rule span_induct_alt_help_S)
himmelma@33175
  1045
            apply assumption
himmelma@33175
  1046
            apply simp
himmelma@33175
  1047
            done}
himmelma@33175
  1048
        moreover
himmelma@33175
  1049
        {fix c x assume xt: "span_induct_alt_help S x"
huffman@36593
  1050
          then have "span_induct_alt_help S (c *\<^sub>R x)"
himmelma@33175
  1051
            apply (induct rule: span_induct_alt_help.induct)
himmelma@33175
  1052
            apply (simp add: span_induct_alt_help_0)
huffman@36593
  1053
            apply (simp add: scaleR_right_distrib)
himmelma@33175
  1054
            apply (rule span_induct_alt_help_S)
himmelma@33175
  1055
            apply assumption
himmelma@33175
  1056
            apply simp
himmelma@33175
  1057
            done
himmelma@33175
  1058
        }
himmelma@33175
  1059
        ultimately show "subspace (span_induct_alt_help S)"
himmelma@33175
  1060
          unfolding subspace_def mem_def Ball_def by blast
himmelma@33175
  1061
      qed}
himmelma@33175
  1062
  with th0 show ?thesis by blast
himmelma@33175
  1063
qed
himmelma@33175
  1064
himmelma@33175
  1065
lemma span_induct_alt:
huffman@36593
  1066
  assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)" and x: "x \<in> span S"
himmelma@33175
  1067
  shows "h x"
himmelma@33175
  1068
using span_induct_alt'[of h S] h0 hS x by blast
himmelma@33175
  1069
huffman@36666
  1070
text {* Individual closure properties. *}
himmelma@33175
  1071
hoelzl@40377
  1072
lemma span_span: "span (span A) = span A"
hoelzl@40377
  1073
  unfolding span_def hull_hull ..
hoelzl@40377
  1074
hoelzl@37489
  1075
lemma (in real_vector) span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses(1))
hoelzl@37489
  1076
hoelzl@37489
  1077
lemma (in real_vector) span_0: "0 \<in> span S" by (metis subspace_span subspace_0)
hoelzl@37489
  1078
hoelzl@40377
  1079
lemma span_inc: "S \<subseteq> span S"
hoelzl@40377
  1080
  by (metis subset_eq span_superset)
hoelzl@40377
  1081
hoelzl@37489
  1082
lemma (in real_vector) dependent_0: assumes "0\<in>A" shows "dependent A"
hoelzl@37489
  1083
  unfolding dependent_def apply(rule_tac x=0 in bexI)
hoelzl@37489
  1084
  using assms span_0 by auto
hoelzl@37489
  1085
hoelzl@37489
  1086
lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S ==> x + y \<in> span S"
himmelma@33175
  1087
  by (metis subspace_add subspace_span)
himmelma@33175
  1088
hoelzl@37489
  1089
lemma (in real_vector) span_mul: "x \<in> span S ==> (c *\<^sub>R x) \<in> span S"
himmelma@33175
  1090
  by (metis subspace_span subspace_mul)
himmelma@33175
  1091
huffman@36593
  1092
lemma span_neg: "x \<in> span S ==> - x \<in> span S"
himmelma@33175
  1093
  by (metis subspace_neg subspace_span)
himmelma@33175
  1094
huffman@36593
  1095
lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S ==> x - y \<in> span S"
himmelma@33175
  1096
  by (metis subspace_span subspace_sub)
himmelma@33175
  1097
hoelzl@37489
  1098
lemma (in real_vector) span_setsum: "finite A \<Longrightarrow> \<forall>x \<in> A. f x \<in> span S ==> setsum f A \<in> span S"
huffman@36362
  1099
  by (rule subspace_setsum, rule subspace_span)
himmelma@33175
  1100
huffman@36593
  1101
lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
himmelma@33175
  1102
  apply (auto simp only: span_add span_sub)
himmelma@33175
  1103
  apply (subgoal_tac "(x + y) - x \<in> span S", simp)
himmelma@33175
  1104
  by (simp only: span_add span_sub)
himmelma@33175
  1105
huffman@36666
  1106
text {* Mapping under linear image. *}
himmelma@33175
  1107
huffman@36593
  1108
lemma span_linear_image: assumes lf: "linear f"
himmelma@33175
  1109
  shows "span (f ` S) = f ` (span S)"
himmelma@33175
  1110
proof-
himmelma@33175
  1111
  {fix x
himmelma@33175
  1112
    assume x: "x \<in> span (f ` S)"
himmelma@33175
  1113
    have "x \<in> f ` span S"
himmelma@33175
  1114
      apply (rule span_induct[where x=x and S = "f ` S"])
himmelma@33175
  1115
      apply (clarsimp simp add: image_iff)
himmelma@33175
  1116
      apply (frule span_superset)
himmelma@33175
  1117
      apply blast
himmelma@33175
  1118
      apply (simp only: mem_def)
himmelma@33175
  1119
      apply (rule subspace_linear_image[OF lf])
himmelma@33175
  1120
      apply (rule subspace_span)
himmelma@33175
  1121
      apply (rule x)
himmelma@33175
  1122
      done}
himmelma@33175
  1123
  moreover
himmelma@33175
  1124
  {fix x assume x: "x \<in> span S"
nipkow@39302
  1125
    have th0:"(\<lambda>a. f a \<in> span (f ` S)) = {x. f x \<in> span (f ` S)}" apply (rule set_eqI)
himmelma@33175
  1126
      unfolding mem_def Collect_def ..
himmelma@33175
  1127
    have "f x \<in> span (f ` S)"
himmelma@33175
  1128
      apply (rule span_induct[where S=S])
himmelma@33175
  1129
      apply (rule span_superset)
himmelma@33175
  1130
      apply simp
himmelma@33175
  1131
      apply (subst th0)
himmelma@33175
  1132
      apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"])
himmelma@33175
  1133
      apply (rule x)
himmelma@33175
  1134
      done}
himmelma@33175
  1135
  ultimately show ?thesis by blast
himmelma@33175
  1136
qed
himmelma@33175
  1137
huffman@36666
  1138
text {* The key breakdown property. *}
himmelma@33175
  1139
himmelma@33175
  1140
lemma span_breakdown:
huffman@36593
  1141
  assumes bS: "b \<in> S" and aS: "a \<in> span S"
huffman@36593
  1142
  shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})" (is "?P a")
himmelma@33175
  1143
proof-
himmelma@33175
  1144
  {fix x assume xS: "x \<in> S"
himmelma@33175
  1145
    {assume ab: "x = b"
himmelma@33175
  1146
      then have "?P x"
himmelma@33175
  1147
        apply simp
himmelma@33175
  1148
        apply (rule exI[where x="1"], simp)
himmelma@33175
  1149
        by (rule span_0)}
himmelma@33175
  1150
    moreover
himmelma@33175
  1151
    {assume ab: "x \<noteq> b"
himmelma@33175
  1152
      then have "?P x"  using xS
himmelma@33175
  1153
        apply -
himmelma@33175
  1154
        apply (rule exI[where x=0])
himmelma@33175
  1155
        apply (rule span_superset)
himmelma@33175
  1156
        by simp}
himmelma@33175
  1157
    ultimately have "?P x" by blast}
himmelma@33175
  1158
  moreover have "subspace ?P"
himmelma@33175
  1159
    unfolding subspace_def
himmelma@33175
  1160
    apply auto
himmelma@33175
  1161
    apply (simp add: mem_def)
himmelma@33175
  1162
    apply (rule exI[where x=0])
himmelma@33175
  1163
    using span_0[of "S - {b}"]
himmelma@33175
  1164
    apply (simp add: mem_def)
himmelma@33175
  1165
    apply (clarsimp simp add: mem_def)
himmelma@33175
  1166
    apply (rule_tac x="k + ka" in exI)
huffman@36593
  1167
    apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)")
himmelma@33175
  1168
    apply (simp only: )
himmelma@33175
  1169
    apply (rule span_add[unfolded mem_def])
himmelma@33175
  1170
    apply assumption+
huffman@36593
  1171
    apply (simp add: algebra_simps)
himmelma@33175
  1172
    apply (clarsimp simp add: mem_def)
himmelma@33175
  1173
    apply (rule_tac x= "c*k" in exI)
huffman@36593
  1174
    apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)")
himmelma@33175
  1175
    apply (simp only: )
himmelma@33175
  1176
    apply (rule span_mul[unfolded mem_def])
himmelma@33175
  1177
    apply assumption
huffman@36593
  1178
    by (simp add: algebra_simps)
himmelma@33175
  1179
  ultimately show "?P a" using aS span_induct[where S=S and P= "?P"] by metis
himmelma@33175
  1180
qed
himmelma@33175
  1181
himmelma@33175
  1182
lemma span_breakdown_eq:
huffman@36593
  1183
  "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *\<^sub>R a) \<in> span S)" (is "?lhs \<longleftrightarrow> ?rhs")
himmelma@33175
  1184
proof-
himmelma@33175
  1185
  {assume x: "x \<in> span (insert a S)"
himmelma@33175
  1186
    from x span_breakdown[of "a" "insert a S" "x"]
himmelma@33175
  1187
    have ?rhs apply clarsimp
himmelma@33175
  1188
      apply (rule_tac x= "k" in exI)
himmelma@33175
  1189
      apply (rule set_rev_mp[of _ "span (S - {a})" _])
himmelma@33175
  1190
      apply assumption
himmelma@33175
  1191
      apply (rule span_mono)
himmelma@33175
  1192
      apply blast
himmelma@33175
  1193
      done}
himmelma@33175
  1194
  moreover
huffman@36593
  1195
  { fix k assume k: "x - k *\<^sub>R a \<in> span S"
hoelzl@37489
  1196
    have eq: "x = (x - k *\<^sub>R a) + k *\<^sub>R a" by simp
huffman@36593
  1197
    have "(x - k *\<^sub>R a) + k *\<^sub>R a \<in> span (insert a S)"
himmelma@33175
  1198
      apply (rule span_add)
himmelma@33175
  1199
      apply (rule set_rev_mp[of _ "span S" _])
himmelma@33175
  1200
      apply (rule k)
himmelma@33175
  1201
      apply (rule span_mono)
himmelma@33175
  1202
      apply blast
himmelma@33175
  1203
      apply (rule span_mul)
himmelma@33175
  1204
      apply (rule span_superset)
himmelma@33175
  1205
      apply blast
himmelma@33175
  1206
      done
himmelma@33175
  1207
    then have ?lhs using eq by metis}
himmelma@33175
  1208
  ultimately show ?thesis by blast
himmelma@33175
  1209
qed
himmelma@33175
  1210
huffman@36666
  1211
text {* Hence some "reversal" results. *}
himmelma@33175
  1212
himmelma@33175
  1213
lemma in_span_insert:
huffman@36593
  1214
  assumes a: "a \<in> span (insert b S)" and na: "a \<notin> span S"
himmelma@33175
  1215
  shows "b \<in> span (insert a S)"
himmelma@33175
  1216
proof-
himmelma@33175
  1217
  from span_breakdown[of b "insert b S" a, OF insertI1 a]
huffman@36593
  1218
  obtain k where k: "a - k*\<^sub>R b \<in> span (S - {b})" by auto
himmelma@33175
  1219
  {assume k0: "k = 0"
himmelma@33175
  1220
    with k have "a \<in> span S"
himmelma@33175
  1221
      apply (simp)
himmelma@33175
  1222
      apply (rule set_rev_mp)
himmelma@33175
  1223
      apply assumption
himmelma@33175
  1224
      apply (rule span_mono)
himmelma@33175
  1225
      apply blast
himmelma@33175
  1226
      done
himmelma@33175
  1227
    with na  have ?thesis by blast}
himmelma@33175
  1228
  moreover
himmelma@33175
  1229
  {assume k0: "k \<noteq> 0"
hoelzl@37489
  1230
    have eq: "b = (1/k) *\<^sub>R a - ((1/k) *\<^sub>R a - b)" by simp
huffman@36593
  1231
    from k0 have eq': "(1/k) *\<^sub>R (a - k*\<^sub>R b) = (1/k) *\<^sub>R a - b"
huffman@36593
  1232
      by (simp add: algebra_simps)
huffman@36593
  1233
    from k have "(1/k) *\<^sub>R (a - k*\<^sub>R b) \<in> span (S - {b})"
himmelma@33175
  1234
      by (rule span_mul)
huffman@36593
  1235
    hence th: "(1/k) *\<^sub>R a - b \<in> span (S - {b})"
himmelma@33175
  1236
      unfolding eq' .
himmelma@33175
  1237
himmelma@33175
  1238
    from k
himmelma@33175
  1239
    have ?thesis
himmelma@33175
  1240
      apply (subst eq)
himmelma@33175
  1241
      apply (rule span_sub)
himmelma@33175
  1242
      apply (rule span_mul)
himmelma@33175
  1243
      apply (rule span_superset)
himmelma@33175
  1244
      apply blast
himmelma@33175
  1245
      apply (rule set_rev_mp)
himmelma@33175
  1246
      apply (rule th)
himmelma@33175
  1247
      apply (rule span_mono)
himmelma@33175
  1248
      using na by blast}
himmelma@33175
  1249
  ultimately show ?thesis by blast
himmelma@33175
  1250
qed
himmelma@33175
  1251
himmelma@33175
  1252
lemma in_span_delete:
huffman@36593
  1253
  assumes a: "a \<in> span S"
himmelma@33175
  1254
  and na: "a \<notin> span (S-{b})"
himmelma@33175
  1255
  shows "b \<in> span (insert a (S - {b}))"
himmelma@33175
  1256
  apply (rule in_span_insert)
himmelma@33175
  1257
  apply (rule set_rev_mp)
himmelma@33175
  1258
  apply (rule a)
himmelma@33175
  1259
  apply (rule span_mono)
himmelma@33175
  1260
  apply blast
himmelma@33175
  1261
  apply (rule na)
himmelma@33175
  1262
  done
himmelma@33175
  1263
huffman@36666
  1264
text {* Transitivity property. *}
himmelma@33175
  1265
himmelma@33175
  1266
lemma span_trans:
huffman@36593
  1267
  assumes x: "x \<in> span S" and y: "y \<in> span (insert x S)"
himmelma@33175
  1268
  shows "y \<in> span S"
himmelma@33175
  1269
proof-
himmelma@33175
  1270
  from span_breakdown[of x "insert x S" y, OF insertI1 y]
huffman@36593
  1271
  obtain k where k: "y -k*\<^sub>R x \<in> span (S - {x})" by auto
hoelzl@37489
  1272
  have eq: "y = (y - k *\<^sub>R x) + k *\<^sub>R x" by simp
himmelma@33175
  1273
  show ?thesis
himmelma@33175
  1274
    apply (subst eq)
himmelma@33175
  1275
    apply (rule span_add)
himmelma@33175
  1276
    apply (rule set_rev_mp)
himmelma@33175
  1277
    apply (rule k)
himmelma@33175
  1278
    apply (rule span_mono)
himmelma@33175
  1279
    apply blast
himmelma@33175
  1280
    apply (rule span_mul)
himmelma@33175
  1281
    by (rule x)
himmelma@33175
  1282
qed
himmelma@33175
  1283
hoelzl@37489
  1284
lemma span_insert_0[simp]: "span (insert 0 S) = span S"
hoelzl@37489
  1285
  using span_mono[of S "insert 0 S"] by (auto intro: span_trans span_0)
hoelzl@37489
  1286
huffman@36666
  1287
text {* An explicit expansion is sometimes needed. *}
himmelma@33175
  1288
himmelma@33175
  1289
lemma span_explicit:
huffman@36593
  1290
  "span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
himmelma@33175
  1291
  (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")
himmelma@33175
  1292
proof-
himmelma@33175
  1293
  {fix x assume x: "x \<in> ?E"
huffman@36593
  1294
    then obtain S u where fS: "finite S" and SP: "S\<subseteq>P" and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = x"
himmelma@33175
  1295
      by blast
himmelma@33175
  1296
    have "x \<in> span P"
himmelma@33175
  1297
      unfolding u[symmetric]
himmelma@33175
  1298
      apply (rule span_setsum[OF fS])
himmelma@33175
  1299
      using span_mono[OF SP]
himmelma@33175
  1300
      by (auto intro: span_superset span_mul)}
himmelma@33175
  1301
  moreover
himmelma@33175
  1302
  have "\<forall>x \<in> span P. x \<in> ?E"
himmelma@33175
  1303
    unfolding mem_def Collect_def
himmelma@33175
  1304
  proof(rule span_induct_alt')
himmelma@33175
  1305
    show "?h 0"
himmelma@33175
  1306
      apply (rule exI[where x="{}"]) by simp
himmelma@33175
  1307
  next
himmelma@33175
  1308
    fix c x y
himmelma@33175
  1309
    assume x: "x \<in> P" and hy: "?h y"
himmelma@33175
  1310
    from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
huffman@36593
  1311
      and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y" by blast
himmelma@33175
  1312
    let ?S = "insert x S"
himmelma@33175
  1313
    let ?u = "\<lambda>y. if y = x then (if x \<in> S then u y + c else c)
himmelma@33175
  1314
                  else u y"
himmelma@33175
  1315
    from fS SP x have th0: "finite (insert x S)" "insert x S \<subseteq> P" by blast+
himmelma@33175
  1316
    {assume xS: "x \<in> S"
himmelma@33175
  1317
      have S1: "S = (S - {x}) \<union> {x}"
himmelma@33175
  1318
        and Sss:"finite (S - {x})" "finite {x}" "(S -{x}) \<inter> {x} = {}" using xS fS by auto
huffman@36593
  1319
      have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =(\<Sum>v\<in>S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x"
himmelma@33175
  1320
        using xS
himmelma@33175
  1321
        by (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]]
himmelma@33175
  1322
          setsum_clauses(2)[OF fS] cong del: if_weak_cong)
huffman@36593
  1323
      also have "\<dots> = (\<Sum>v\<in>S. u v *\<^sub>R v) + c *\<^sub>R x"
himmelma@33175
  1324
        apply (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]])
huffman@36593
  1325
        by (simp add: algebra_simps)
huffman@36593
  1326
      also have "\<dots> = c*\<^sub>R x + y"
himmelma@33175
  1327
        by (simp add: add_commute u)
huffman@36593
  1328
      finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" .
huffman@36593
  1329
    then have "?Q ?S ?u (c*\<^sub>R x + y)" using th0 by blast}
himmelma@33175
  1330
  moreover
himmelma@33175
  1331
  {assume xS: "x \<notin> S"
huffman@36593
  1332
    have th00: "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y"
himmelma@33175
  1333
      unfolding u[symmetric]
himmelma@33175
  1334
      apply (rule setsum_cong2)
himmelma@33175
  1335
      using xS by auto
huffman@36593
  1336
    have "?Q ?S ?u (c*\<^sub>R x + y)" using fS xS th0
himmelma@33175
  1337
      by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong)}
huffman@36593
  1338
  ultimately have "?Q ?S ?u (c*\<^sub>R x + y)"
himmelma@33175
  1339
    by (cases "x \<in> S", simp, simp)
huffman@36593
  1340
    then show "?h (c*\<^sub>R x + y)"
himmelma@33175
  1341
      apply -
himmelma@33175
  1342
      apply (rule exI[where x="?S"])
himmelma@33175
  1343
      apply (rule exI[where x="?u"]) by metis
himmelma@33175
  1344
  qed
himmelma@33175
  1345
  ultimately show ?thesis by blast
himmelma@33175
  1346
qed
himmelma@33175
  1347
himmelma@33175
  1348
lemma dependent_explicit:
huffman@36593
  1349
  "dependent P \<longleftrightarrow> (\<exists>S u. finite S \<and> S \<subseteq> P \<and> (\<exists>v\<in>S. u v \<noteq> 0 \<and> setsum (\<lambda>v. u v *\<^sub>R v) S = 0))" (is "?lhs = ?rhs")
himmelma@33175
  1350
proof-
himmelma@33175
  1351
  {assume dP: "dependent P"
himmelma@33175
  1352
    then obtain a S u where aP: "a \<in> P" and fS: "finite S"
huffman@36593
  1353
      and SP: "S \<subseteq> P - {a}" and ua: "setsum (\<lambda>v. u v *\<^sub>R v) S = a"
himmelma@33175
  1354
      unfolding dependent_def span_explicit by blast
himmelma@33175
  1355
    let ?S = "insert a S"
himmelma@33175
  1356
    let ?u = "\<lambda>y. if y = a then - 1 else u y"
himmelma@33175
  1357
    let ?v = a
himmelma@33175
  1358
    from aP SP have aS: "a \<notin> S" by blast
himmelma@33175
  1359
    from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0" by auto
huffman@36593
  1360
    have s0: "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"
himmelma@33175
  1361
      using fS aS
hoelzl@37489
  1362
      apply (simp add: setsum_clauses field_simps)
himmelma@33175
  1363
      apply (subst (2) ua[symmetric])
himmelma@33175
  1364
      apply (rule setsum_cong2)
himmelma@33175
  1365
      by auto
himmelma@33175
  1366
    with th0 have ?rhs
himmelma@33175
  1367
      apply -
himmelma@33175
  1368
      apply (rule exI[where x= "?S"])
himmelma@33175
  1369
      apply (rule exI[where x= "?u"])
himmelma@33175
  1370
      by clarsimp}
himmelma@33175
  1371
  moreover
himmelma@33175
  1372
  {fix S u v assume fS: "finite S"
himmelma@33175
  1373
      and SP: "S \<subseteq> P" and vS: "v \<in> S" and uv: "u v \<noteq> 0"
huffman@36593
  1374
    and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = 0"
himmelma@33175
  1375
    let ?a = v
himmelma@33175
  1376
    let ?S = "S - {v}"
himmelma@33175
  1377
    let ?u = "\<lambda>i. (- u i) / u v"
himmelma@33175
  1378
    have th0: "?a \<in> P" "finite ?S" "?S \<subseteq> P"       using fS SP vS by auto
huffman@36593
  1379
    have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = setsum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
himmelma@33175
  1380
      using fS vS uv
hoelzl@37489
  1381
      by (simp add: setsum_diff1 divide_inverse field_simps)
himmelma@33175
  1382
    also have "\<dots> = ?a"
huffman@36593
  1383
      unfolding scaleR_right.setsum [symmetric] u
huffman@36593
  1384
      using uv by simp
huffman@36593
  1385
    finally  have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
himmelma@33175
  1386
    with th0 have ?lhs
himmelma@33175
  1387
      unfolding dependent_def span_explicit
himmelma@33175
  1388
      apply -
himmelma@33175
  1389
      apply (rule bexI[where x= "?a"])
huffman@36593
  1390
      apply (simp_all del: scaleR_minus_left)
himmelma@33175
  1391
      apply (rule exI[where x= "?S"])
huffman@36593
  1392
      by (auto simp del: scaleR_minus_left)}
himmelma@33175
  1393
  ultimately show ?thesis by blast
himmelma@33175
  1394
qed
himmelma@33175
  1395
himmelma@33175
  1396
himmelma@33175
  1397
lemma span_finite:
himmelma@33175
  1398
  assumes fS: "finite S"
huffman@36593
  1399
  shows "span S = {y. \<exists>u. setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
himmelma@33175
  1400
  (is "_ = ?rhs")
himmelma@33175
  1401
proof-
himmelma@33175
  1402
  {fix y assume y: "y \<in> span S"
himmelma@33175
  1403
    from y obtain S' u where fS': "finite S'" and SS': "S' \<subseteq> S" and
huffman@36593
  1404
      u: "setsum (\<lambda>v. u v *\<^sub>R v) S' = y" unfolding span_explicit by blast
himmelma@33175
  1405
    let ?u = "\<lambda>x. if x \<in> S' then u x else 0"
huffman@36593
  1406
    have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = setsum (\<lambda>v. u v *\<^sub>R v) S'"
hoelzl@37489
  1407
      using SS' fS by (auto intro!: setsum_mono_zero_cong_right)
huffman@36593
  1408
    hence "setsum (\<lambda>v. ?u v *\<^sub>R v) S = y" by (metis u)
himmelma@33175
  1409
    hence "y \<in> ?rhs" by auto}
himmelma@33175
  1410
  moreover
huffman@36593
  1411
  {fix y u assume u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y"
himmelma@33175
  1412
    then have "y \<in> span S" using fS unfolding span_explicit by auto}
himmelma@33175
  1413
  ultimately show ?thesis by blast
himmelma@33175
  1414
qed
himmelma@33175
  1415
hoelzl@37664
  1416
lemma Int_Un_cancel: "(A \<union> B) \<inter> A = A" "(A \<union> B) \<inter> B = B" by auto
hoelzl@37664
  1417
hoelzl@37664
  1418
lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
hoelzl@37664
  1419
proof safe
hoelzl@37664
  1420
  fix x assume "x \<in> span (A \<union> B)"
hoelzl@37664
  1421
  then obtain S u where S: "finite S" "S \<subseteq> A \<union> B" and x: "x = (\<Sum>v\<in>S. u v *\<^sub>R v)"
hoelzl@37664
  1422
    unfolding span_explicit by auto
hoelzl@37664
  1423
hoelzl@37664
  1424
  let ?Sa = "\<Sum>v\<in>S\<inter>A. u v *\<^sub>R v"
hoelzl@37664
  1425
  let ?Sb = "(\<Sum>v\<in>S\<inter>(B - A). u v *\<^sub>R v)"
hoelzl@37664
  1426
  show "x \<in> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
hoelzl@37664
  1427
  proof
hoelzl@37664
  1428
    show "x = (case (?Sa, ?Sb) of (a, b) \<Rightarrow> a + b)"
hoelzl@37664
  1429
      unfolding x using S
hoelzl@37664
  1430
      by (simp, subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
hoelzl@37664
  1431
hoelzl@37664
  1432
    from S have "?Sa \<in> span A" unfolding span_explicit
hoelzl@37664
  1433
      by (auto intro!: exI[of _ "S \<inter> A"])
hoelzl@37664
  1434
    moreover from S have "?Sb \<in> span B" unfolding span_explicit
hoelzl@37664
  1435
      by (auto intro!: exI[of _ "S \<inter> (B - A)"])
hoelzl@37664
  1436
    ultimately show "(?Sa, ?Sb) \<in> span A \<times> span B" by simp
hoelzl@37664
  1437
  qed
hoelzl@37664
  1438
next
hoelzl@37664
  1439
  fix a b assume "a \<in> span A" and "b \<in> span B"
hoelzl@37664
  1440
  then obtain Sa ua Sb ub where span:
hoelzl@37664
  1441
    "finite Sa" "Sa \<subseteq> A" "a = (\<Sum>v\<in>Sa. ua v *\<^sub>R v)"
hoelzl@37664
  1442
    "finite Sb" "Sb \<subseteq> B" "b = (\<Sum>v\<in>Sb. ub v *\<^sub>R v)"
hoelzl@37664
  1443
    unfolding span_explicit by auto
hoelzl@37664
  1444
  let "?u v" = "(if v \<in> Sa then ua v else 0) + (if v \<in> Sb then ub v else 0)"
hoelzl@37664
  1445
  from span have "finite (Sa \<union> Sb)" "Sa \<union> Sb \<subseteq> A \<union> B"
hoelzl@37664
  1446
    and "a + b = (\<Sum>v\<in>(Sa\<union>Sb). ?u v *\<^sub>R v)"
hoelzl@37664
  1447
    unfolding setsum_addf scaleR_left_distrib
hoelzl@37664
  1448
    by (auto simp add: if_distrib cond_application_beta setsum_cases Int_Un_cancel)
hoelzl@37664
  1449
  thus "a + b \<in> span (A \<union> B)"
hoelzl@37664
  1450
    unfolding span_explicit by (auto intro!: exI[of _ ?u])
hoelzl@37664
  1451
qed
himmelma@33175
  1452
huffman@36666
  1453
text {* This is useful for building a basis step-by-step. *}
himmelma@33175
  1454
himmelma@33175
  1455
lemma independent_insert:
huffman@36593
  1456
  "independent(insert a S) \<longleftrightarrow>
himmelma@33175
  1457
      (if a \<in> S then independent S
himmelma@33175
  1458
                else independent S \<and> a \<notin> span S)" (is "?lhs \<longleftrightarrow> ?rhs")
himmelma@33175
  1459
proof-
himmelma@33175
  1460
  {assume aS: "a \<in> S"
himmelma@33175
  1461
    hence ?thesis using insert_absorb[OF aS] by simp}
himmelma@33175
  1462
  moreover
himmelma@33175
  1463
  {assume aS: "a \<notin> S"
himmelma@33175
  1464
    {assume i: ?lhs
himmelma@33175
  1465
      then have ?rhs using aS
himmelma@33175
  1466
        apply simp
himmelma@33175
  1467
        apply (rule conjI)
himmelma@33175
  1468
        apply (rule independent_mono)
himmelma@33175
  1469
        apply assumption
himmelma@33175
  1470
        apply blast
himmelma@33175
  1471
        by (simp add: dependent_def)}
himmelma@33175
  1472
    moreover
himmelma@33175
  1473
    {assume i: ?rhs
himmelma@33175
  1474
      have ?lhs using i aS
himmelma@33175
  1475
        apply simp
himmelma@33175
  1476
        apply (auto simp add: dependent_def)
himmelma@33175
  1477
        apply (case_tac "aa = a", auto)
himmelma@33175
  1478
        apply (subgoal_tac "insert a S - {aa} = insert a (S - {aa})")
himmelma@33175
  1479
        apply simp
himmelma@33175
  1480
        apply (subgoal_tac "a \<in> span (insert aa (S - {aa}))")
himmelma@33175
  1481
        apply (subgoal_tac "insert aa (S - {aa}) = S")
himmelma@33175
  1482
        apply simp
himmelma@33175
  1483
        apply blast
himmelma@33175
  1484
        apply (rule in_span_insert)
himmelma@33175
  1485
        apply assumption
himmelma@33175
  1486
        apply blast
himmelma@33175
  1487
        apply blast
himmelma@33175
  1488
        done}
himmelma@33175
  1489
    ultimately have ?thesis by blast}
himmelma@33175
  1490
  ultimately show ?thesis by blast
himmelma@33175
  1491
qed
himmelma@33175
  1492
huffman@36666
  1493
text {* The degenerate case of the Exchange Lemma. *}
himmelma@33175
  1494
himmelma@33175
  1495
lemma mem_delete: "x \<in> (A - {a}) \<longleftrightarrow> x \<noteq> a \<and> x \<in> A"
himmelma@33175
  1496
  by blast
himmelma@33175
  1497
himmelma@33175
  1498
lemma spanning_subset_independent:
huffman@36593
  1499
  assumes BA: "B \<subseteq> A" and iA: "independent A"
himmelma@33175
  1500
  and AsB: "A \<subseteq> span B"
himmelma@33175
  1501
  shows "A = B"
himmelma@33175
  1502
proof
himmelma@33175
  1503
  from BA show "B \<subseteq> A" .
himmelma@33175
  1504
next
himmelma@33175
  1505
  from span_mono[OF BA] span_mono[OF AsB]
himmelma@33175
  1506
  have sAB: "span A = span B" unfolding span_span by blast
himmelma@33175
  1507
himmelma@33175
  1508
  {fix x assume x: "x \<in> A"
himmelma@33175
  1509
    from iA have th0: "x \<notin> span (A - {x})"
himmelma@33175
  1510
      unfolding dependent_def using x by blast
himmelma@33175
  1511
    from x have xsA: "x \<in> span A" by (blast intro: span_superset)
himmelma@33175
  1512
    have "A - {x} \<subseteq> A" by blast
himmelma@33175
  1513
    hence th1:"span (A - {x}) \<subseteq> span A" by (metis span_mono)
himmelma@33175
  1514
    {assume xB: "x \<notin> B"
himmelma@33175
  1515
      from xB BA have "B \<subseteq> A -{x}" by blast
himmelma@33175
  1516
      hence "span B \<subseteq> span (A - {x})" by (metis span_mono)
himmelma@33175
  1517
      with th1 th0 sAB have "x \<notin> span A" by blast
himmelma@33175
  1518
      with x have False by (metis span_superset)}
himmelma@33175
  1519
    then have "x \<in> B" by blast}
himmelma@33175
  1520
  then show "A \<subseteq> B" by blast
himmelma@33175
  1521
qed
himmelma@33175
  1522
huffman@36666
  1523
text {* The general case of the Exchange Lemma, the key to what follows. *}
himmelma@33175
  1524
himmelma@33175
  1525
lemma exchange_lemma:
huffman@36593
  1526
  assumes f:"finite t" and i: "independent s"
himmelma@33175
  1527
  and sp:"s \<subseteq> span t"
hoelzl@33715
  1528
  shows "\<exists>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
himmelma@33175
  1529
using f i sp
berghofe@34915
  1530
proof(induct "card (t - s)" arbitrary: s t rule: less_induct)
berghofe@34915
  1531
  case less
berghofe@34915
  1532
  note ft = `finite t` and s = `independent s` and sp = `s \<subseteq> span t`
hoelzl@33715
  1533
  let ?P = "\<lambda>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
himmelma@33175
  1534
  let ?ths = "\<exists>t'. ?P t'"
himmelma@33175
  1535
  {assume st: "s \<subseteq> t"
himmelma@33175
  1536
    from st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t])
hoelzl@33715
  1537
      by (auto intro: span_superset)}
himmelma@33175
  1538
  moreover
himmelma@33175
  1539
  {assume st: "t \<subseteq> s"
himmelma@33175
  1540
himmelma@33175
  1541
    from spanning_subset_independent[OF st s sp]
himmelma@33175
  1542
      st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t])
hoelzl@33715
  1543
      by (auto intro: span_superset)}
himmelma@33175
  1544
  moreover
himmelma@33175
  1545
  {assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
himmelma@33175
  1546
    from st(2) obtain b where b: "b \<in> t" "b \<notin> s" by blast
himmelma@33175
  1547
      from b have "t - {b} - s \<subset> t - s" by blast
berghofe@34915
  1548
      then have cardlt: "card (t - {b} - s) < card (t - s)" using ft
himmelma@33175
  1549
        by (auto intro: psubset_card_mono)
himmelma@33175
  1550
      from b ft have ct0: "card t \<noteq> 0" by auto
himmelma@33175
  1551
    {assume stb: "s \<subseteq> span(t -{b})"
himmelma@33175
  1552
      from ft have ftb: "finite (t -{b})" by auto
berghofe@34915
  1553
      from less(1)[OF cardlt ftb s stb]
hoelzl@33715
  1554
      obtain u where u: "card u = card (t-{b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u" and fu: "finite u" by blast
himmelma@33175
  1555
      let ?w = "insert b u"
himmelma@33175
  1556
      have th0: "s \<subseteq> insert b u" using u by blast
himmelma@33175
  1557
      from u(3) b have "u \<subseteq> s \<union> t" by blast
himmelma@33175
  1558
      then have th1: "insert b u \<subseteq> s \<union> t" using u b by blast
himmelma@33175
  1559
      have bu: "b \<notin> u" using b u by blast
hoelzl@33715
  1560
      from u(1) ft b have "card u = (card t - 1)" by auto
himmelma@33175
  1561
      then
hoelzl@33715
  1562
      have th2: "card (insert b u) = card t"
hoelzl@33715
  1563
        using card_insert_disjoint[OF fu bu] ct0 by auto
himmelma@33175
  1564
      from u(4) have "s \<subseteq> span u" .
himmelma@33175
  1565
      also have "\<dots> \<subseteq> span (insert b u)" apply (rule span_mono) by blast
hoelzl@33715
  1566
      finally have th3: "s \<subseteq> span (insert b u)" .
hoelzl@33715
  1567
      from th0 th1 th2 th3 fu have th: "?P ?w"  by blast
himmelma@33175
  1568
      from th have ?ths by blast}
himmelma@33175
  1569
    moreover
himmelma@33175
  1570
    {assume stb: "\<not> s \<subseteq> span(t -{b})"
himmelma@33175
  1571
      from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})" by blast
himmelma@33175
  1572
      have ab: "a \<noteq> b" using a b by blast
himmelma@33175
  1573
      have at: "a \<notin> t" using a ab span_superset[of a "t- {b}"] by auto
berghofe@34915
  1574
      have mlt: "card ((insert a (t - {b})) - s) < card (t - s)"
berghofe@34915
  1575
        using cardlt ft a b by auto
himmelma@33175
  1576
      have ft': "finite (insert a (t - {b}))" using ft by auto
himmelma@33175
  1577
      {fix x assume xs: "x \<in> s"
himmelma@33175
  1578
        have t: "t \<subseteq> (insert b (insert a (t -{b})))" using b by auto
himmelma@33175
  1579
        from b(1) have "b \<in> span t" by (simp add: span_superset)
himmelma@35541
  1580
        have bs: "b \<in> span (insert a (t - {b}))" apply(rule in_span_delete)
himmelma@35541
  1581
          using  a sp unfolding subset_eq by auto
himmelma@33175
  1582
        from xs sp have "x \<in> span t" by blast
himmelma@33175
  1583
        with span_mono[OF t]
himmelma@33175
  1584
        have x: "x \<in> span (insert b (insert a (t - {b})))" ..
himmelma@33175
  1585
        from span_trans[OF bs x] have "x \<in> span (insert a (t - {b}))"  .}
himmelma@33175
  1586
      then have sp': "s \<subseteq> span (insert a (t - {b}))" by blast
himmelma@33175
  1587
berghofe@34915
  1588
      from less(1)[OF mlt ft' s sp'] obtain u where
hoelzl@33715
  1589
        u: "card u = card (insert a (t -{b}))" "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t -{b})"
himmelma@33175
  1590
        "s \<subseteq> span u" by blast
hoelzl@33715
  1591
      from u a b ft at ct0 have "?P u" by auto
himmelma@33175
  1592
      then have ?ths by blast }
himmelma@33175
  1593
    ultimately have ?ths by blast
himmelma@33175
  1594
  }
himmelma@33175
  1595
  ultimately
himmelma@33175
  1596
  show ?ths  by blast
himmelma@33175
  1597
qed
himmelma@33175
  1598
huffman@36666
  1599
text {* This implies corresponding size bounds. *}
himmelma@33175
  1600
himmelma@33175
  1601
lemma independent_span_bound:
huffman@36593
  1602
  assumes f: "finite t" and i: "independent s" and sp:"s \<subseteq> span t"
himmelma@33175
  1603
  shows "finite s \<and> card s \<le> card t"
hoelzl@33715
  1604
  by (metis exchange_lemma[OF f i sp] finite_subset card_mono)
himmelma@33175
  1605
himmelma@33175
  1606
himmelma@33175
  1607
lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
himmelma@33175
  1608
proof-
himmelma@33175
  1609
  have eq: "{f x |x. x\<in> UNIV} = f ` UNIV" by auto
himmelma@33175
  1610
  show ?thesis unfolding eq
himmelma@33175
  1611
    apply (rule finite_imageI)
himmelma@33175
  1612
    apply (rule finite)
himmelma@33175
  1613
    done
himmelma@33175
  1614
qed
himmelma@33175
  1615
hoelzl@37489
  1616
subsection{* Euclidean Spaces as Typeclass*}
hoelzl@37489
  1617
hoelzl@37489
  1618
class real_basis = real_vector +
hoelzl@37489
  1619
  fixes basis :: "nat \<Rightarrow> 'a"
hoelzl@37489
  1620
  assumes span_basis: "span (range basis) = UNIV"
hoelzl@37489
  1621
  assumes dimension_exists: "\<exists>d>0.
hoelzl@37489
  1622
    basis ` {d..} = {0} \<and>
hoelzl@37489
  1623
    independent (basis ` {..<d}) \<and>
hoelzl@37489
  1624
    inj_on basis {..<d}"
hoelzl@37489
  1625
huffman@37646
  1626
definition (in real_basis) dimension :: "'a itself \<Rightarrow> nat" where
hoelzl@37489
  1627
  "dimension x =
hoelzl@37489
  1628
    (THE d. basis ` {d..} = {0} \<and> independent (basis ` {..<d}) \<and> inj_on basis {..<d})"
hoelzl@37489
  1629
hoelzl@37489
  1630
syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
hoelzl@37489
  1631
huffman@37646
  1632
translations "DIM('t)" == "CONST dimension (TYPE('t))"
hoelzl@37489
  1633
hoelzl@37489
  1634
lemma (in real_basis) dimensionI:
hoelzl@37489
  1635
  assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0}; independent (basis ` {..<d});
hoelzl@37489
  1636
    inj_on basis {..<d} \<rbrakk> \<Longrightarrow> P d"
hoelzl@37489
  1637
  shows "P DIM('a)"
hoelzl@37489
  1638
proof -
hoelzl@37489
  1639
  obtain d where "0 < d" and d: "basis ` {d..} = {0} \<and>
hoelzl@37489
  1640
      independent (basis ` {..<d}) \<and> inj_on basis {..<d}" (is "?P d")
hoelzl@37489
  1641
    using dimension_exists by auto
hoelzl@37489
  1642
  show ?thesis unfolding dimension_def
hoelzl@37489
  1643
  proof (rule theI2)
hoelzl@37489
  1644
    fix d' assume "?P d'"
hoelzl@37489
  1645
    with d have "basis d' = 0" "basis d = 0" and
hoelzl@37489
  1646
      "d < d' \<Longrightarrow> basis d \<noteq> 0"
hoelzl@37489
  1647
      "d' < d \<Longrightarrow> basis d' \<noteq> 0"
hoelzl@37489
  1648
      using dependent_0 by auto
hoelzl@37489
  1649
    thus "d' = d" by (cases rule: linorder_cases) auto
hoelzl@37489
  1650
    moreover have "P d" using assms[of d] `0 < d` d by auto
hoelzl@37489
  1651
    ultimately show "P d'" by simp
hoelzl@37489
  1652
  next show "?P d" using `?P d` .
hoelzl@37489
  1653
  qed
hoelzl@37489
  1654
qed
hoelzl@37489
  1655
hoelzl@37489
  1656
lemma (in real_basis) dimension_eq:
hoelzl@37489
  1657
  assumes "\<And>i. i < d \<Longrightarrow> basis i \<noteq> 0"
hoelzl@37489
  1658
  assumes "\<And>i. d \<le> i \<Longrightarrow> basis i = 0"
hoelzl@37489
  1659
  shows "DIM('a) = d"
hoelzl@37489
  1660
proof (rule dimensionI)
hoelzl@37489
  1661
  let ?b = "basis :: nat \<Rightarrow> 'a"
hoelzl@37489
  1662
  fix d' assume *: "?b ` {d'..} = {0}" "independent (?b ` {..<d'})"
hoelzl@37489
  1663
  show "d' = d"
hoelzl@37489
  1664
  proof (cases rule: linorder_cases)
hoelzl@37489
  1665
    assume "d' < d" hence "basis d' \<noteq> 0" using assms by auto
hoelzl@37489
  1666
    with * show ?thesis by auto
hoelzl@37489
  1667
  next
hoelzl@37489
  1668
    assume "d < d'" hence "basis d \<noteq> 0" using * dependent_0 by auto
hoelzl@37489
  1669
    with assms(2) `d < d'` show ?thesis by auto
hoelzl@37489
  1670
  qed
hoelzl@37489
  1671
qed
hoelzl@37489
  1672
hoelzl@37489
  1673
lemma (in real_basis)
hoelzl@37489
  1674
  shows basis_finite: "basis ` {DIM('a)..} = {0}"
hoelzl@37489
  1675
  and independent_basis: "independent (basis ` {..<DIM('a)})"
hoelzl@37489
  1676
  and DIM_positive[intro]: "(DIM('a) :: nat) > 0"
hoelzl@37489
  1677
  and basis_inj[simp, intro]: "inj_on basis {..<DIM('a)}"
hoelzl@37489
  1678
  by (auto intro!: dimensionI)
hoelzl@37489
  1679
hoelzl@37489
  1680
lemma (in real_basis) basis_eq_0_iff: "basis j = 0 \<longleftrightarrow> DIM('a) \<le> j"
hoelzl@37489
  1681
proof
hoelzl@37489
  1682
  show "DIM('a) \<le> j \<Longrightarrow> basis j = 0" using basis_finite by auto
hoelzl@37489
  1683
next
hoelzl@37489
  1684
  have "j < DIM('a) \<Longrightarrow> basis j \<noteq> 0"
hoelzl@37489
  1685
    using independent_basis by (auto intro!: dependent_0)
hoelzl@37489
  1686
  thus "basis j = 0 \<Longrightarrow> DIM('a) \<le> j" unfolding not_le[symmetric] by blast
hoelzl@37489
  1687
qed
hoelzl@37489
  1688
hoelzl@37489
  1689
lemma (in real_basis) range_basis:
hoelzl@37489
  1690
    "range basis = insert 0 (basis ` {..<DIM('a)})"
hoelzl@37489
  1691
proof -
hoelzl@37489
  1692
  have *: "UNIV = {..<DIM('a)} \<union> {DIM('a)..}" by auto
hoelzl@37489
  1693
  show ?thesis unfolding * image_Un basis_finite by auto
hoelzl@37489
  1694
qed
hoelzl@37489
  1695
hoelzl@37489
  1696
lemma (in real_basis) range_basis_finite[intro]:
hoelzl@37489
  1697
    "finite (range basis)"
hoelzl@37489
  1698
  unfolding range_basis by auto
hoelzl@37489
  1699
hoelzl@37489
  1700
lemma (in real_basis) basis_neq_0[intro]:
hoelzl@37489
  1701
  assumes "i<DIM('a)" shows "(basis i) \<noteq> 0"
hoelzl@37489
  1702
proof(rule ccontr) assume "\<not> basis i \<noteq> (0::'a)"
hoelzl@37489
  1703
  hence "(0::'a) \<in> basis ` {..<DIM('a)}" using assms by auto
hoelzl@37489
  1704
  from dependent_0[OF this] show False using independent_basis by auto
hoelzl@37489
  1705
qed
hoelzl@37489
  1706
hoelzl@37489
  1707
lemma (in real_basis) basis_zero[simp]:
hoelzl@37489
  1708
  assumes"i \<ge> DIM('a)" shows "basis i = 0"
hoelzl@37489
  1709
proof-
hoelzl@37489
  1710
  have "(basis i::'a) \<in> basis ` {DIM('a)..}" using assms by auto
hoelzl@37489
  1711
  thus ?thesis unfolding basis_finite by fastsimp
hoelzl@37489
  1712
qed
hoelzl@37489
  1713
hoelzl@37489
  1714
lemma basis_representation:
hoelzl@37489
  1715
  "\<exists>u. x = (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R (v\<Colon>'a\<Colon>real_basis))"
hoelzl@37489
  1716
proof -
hoelzl@37489
  1717
  have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]]
hoelzl@37489
  1718
  have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x"
hoelzl@37489
  1719
    unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto
hoelzl@37489
  1720
  thus ?thesis by fastsimp
hoelzl@37489
  1721
qed
hoelzl@37489
  1722
hoelzl@37664
  1723
lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = UNIV"
hoelzl@37664
  1724
  apply(subst span_basis[symmetric]) unfolding range_basis by auto
hoelzl@37664
  1725
hoelzl@37664
  1726
lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = DIM('a)"
hoelzl@37664
  1727
  apply(subst card_image) using basis_inj by auto
hoelzl@37664
  1728
hoelzl@37664
  1729
lemma in_span_basis: "(x::'a::real_basis) \<in> span (basis ` {..<DIM('a)})"
hoelzl@37664
  1730
  unfolding span_basis' ..
hoelzl@37664
  1731
hoelzl@37664
  1732
lemma independent_eq_inj_on:
hoelzl@37664
  1733
  fixes D :: nat and f :: "nat \<Rightarrow> 'c::real_vector" assumes *: "inj_on f {..<D}"
hoelzl@37664
  1734
  shows "independent (f ` {..<D}) \<longleftrightarrow> (\<forall>a u. a < D \<longrightarrow> (\<Sum>i\<in>{..<D}-{a}. u (f i) *\<^sub>R f i) \<noteq> f a)"
hoelzl@37664
  1735
proof -
hoelzl@37664
  1736
  from * have eq: "\<And>i. i < D \<Longrightarrow> f ` {..<D} - {f i} = f`({..<D} - {i})"
hoelzl@37664
  1737
    and inj: "\<And>i. inj_on f ({..<D} - {i})"
hoelzl@37664
  1738
    by (auto simp: inj_on_def)
hoelzl@37664
  1739
  have *: "\<And>i. finite (f ` {..<D} - {i})" by simp
hoelzl@37664
  1740
  show ?thesis unfolding dependent_def span_finite[OF *]
hoelzl@37664
  1741
    by (auto simp: eq setsum_reindex[OF inj])
hoelzl@37664
  1742
qed
hoelzl@37664
  1743
hoelzl@37489
  1744
class real_basis_with_inner = real_inner + real_basis
hoelzl@37489
  1745
begin
hoelzl@37489
  1746
hoelzl@37489
  1747
definition euclidean_component (infixl "$$" 90) where
hoelzl@37489
  1748
  "x $$ i = inner (basis i) x"
hoelzl@37489
  1749
hoelzl@37489
  1750
definition Chi (binder "\<chi>\<chi> " 10) where
hoelzl@37489
  1751
  "(\<chi>\<chi> i. f i) = (\<Sum>i<DIM('a). f i *\<^sub>R basis i)"
hoelzl@37489
  1752
hoelzl@37489
  1753
lemma basis_at_neq_0[intro]:
hoelzl@37489
  1754
  "i < DIM('a) \<Longrightarrow> basis i $$ i \<noteq> 0"
hoelzl@37489
  1755
  unfolding euclidean_component_def by (auto intro!: basis_neq_0)
hoelzl@37489
  1756
hoelzl@37489
  1757
lemma euclidean_component_ge[simp]:
hoelzl@37489
  1758
  assumes "i \<ge> DIM('a)" shows "x $$ i = 0"
hoelzl@37489
  1759
  unfolding euclidean_component_def basis_zero[OF assms] by auto
hoelzl@37489
  1760
hoelzl@37489
  1761
lemma euclidean_scaleR:
hoelzl@37489
  1762
  shows "(a *\<^sub>R x) $$ i = a * (x$$i)"
hoelzl@37489
  1763
  unfolding euclidean_component_def by auto
hoelzl@37489
  1764
hoelzl@37489
  1765
end
hoelzl@37489
  1766
hoelzl@37489
  1767
interpretation euclidean_component: additive "\<lambda>x. euclidean_component x i"
hoelzl@37489
  1768
proof qed (simp add: euclidean_component_def inner_right.add)
hoelzl@37489
  1769
hoelzl@37489
  1770
subsection{* Euclidean Spaces as Typeclass *}
hoelzl@37489
  1771
hoelzl@37489
  1772
class euclidean_space = real_basis_with_inner +
hoelzl@37489
  1773
  assumes basis_orthonormal: "\<forall>i<DIM('a). \<forall>j<DIM('a).
hoelzl@37489
  1774
    inner (basis i) (basis j) = (if i = j then 1 else 0)"
hoelzl@37489
  1775
hoelzl@37489
  1776
lemma (in euclidean_space) dot_basis:
hoelzl@37489
  1777
  "inner (basis i) (basis j) = (if i = j \<and> i<DIM('a) then 1 else 0)"
hoelzl@37489
  1778
proof (cases "(i < DIM('a) \<and> j < DIM('a))")
hoelzl@37489
  1779
  case False
hoelzl@37489
  1780
  hence "basis i = 0 \<or> basis j = 0"
hoelzl@37489
  1781
    using basis_finite by fastsimp
hoelzl@37489
  1782
  hence "inner (basis i) (basis j) = 0" by (rule disjE) simp_all
hoelzl@37489
  1783
  thus ?thesis using False by auto
hoelzl@37489
  1784
next
hoelzl@37489
  1785
  case True thus ?thesis using basis_orthonormal by auto
hoelzl@37489
  1786
qed
hoelzl@37489
  1787
hoelzl@37489
  1788
lemma (in euclidean_space) basis_component[simp]:
hoelzl@37489
  1789
  "basis i $$ j = (if i = j \<and> i < DIM('a) then 1 else 0)"
hoelzl@37489
  1790
  unfolding euclidean_component_def dot_basis by auto
hoelzl@37489
  1791
hoelzl@37489
  1792
lemmas euclidean_simps =
hoelzl@37489
  1793
  euclidean_component.add
hoelzl@37489
  1794
  euclidean_component.diff
hoelzl@37489
  1795
  euclidean_scaleR
hoelzl@37489
  1796
  euclidean_component.minus
hoelzl@37489
  1797
  euclidean_component.setsum
hoelzl@37489
  1798
  basis_component
hoelzl@37489
  1799
hoelzl@37489
  1800
lemma euclidean_representation:
hoelzl@37489
  1801
  "(x\<Colon>'a\<Colon>euclidean_space) = (\<Sum>i\<in>{..<DIM('a)}. (x$$i) *\<^sub>R basis i)"
hoelzl@37489
  1802
proof-
hoelzl@37489
  1803
  from basis_representation[of x] guess u ..
hoelzl@37489
  1804
  hence *:"x = (\<Sum>i\<in>{..<DIM('a)}. u (basis i) *\<^sub>R (basis i))"
hoelzl@37489
  1805
    by (simp add: setsum_reindex)
hoelzl@37489
  1806
  show ?thesis apply(subst *)
hoelzl@37489
  1807
  proof(safe intro!: setsum_cong2)
hoelzl@37489
  1808
    fix i assume i: "i < DIM('a)"
hoelzl@37489
  1809
    hence "x$$i = (\<Sum>x<DIM('a). (if i = x then u (basis x) else 0))"
hoelzl@37489
  1810
      by (auto simp: euclidean_simps * intro!: setsum_cong)
hoelzl@37489
  1811
    also have "... = u (basis i)" using i by (auto simp: setsum_cases)
hoelzl@37489
  1812
    finally show "u (basis i) *\<^sub>R basis i = x $$ i *\<^sub>R basis i" by simp
hoelzl@37489
  1813
  qed
hoelzl@37489
  1814
qed
hoelzl@37489
  1815
hoelzl@37489
  1816
lemma euclidean_eq:
hoelzl@37489
  1817
  fixes x y :: "'a\<Colon>euclidean_space"
hoelzl@37489
  1818
  shows "x = y \<longleftrightarrow> (\<forall>i<DIM('a). x$$i = y$$i)" (is "?l = ?r")
hoelzl@37489
  1819
proof safe
hoelzl@37489
  1820
  assume "\<forall>i<DIM('a). x $$ i = y $$ i"
hoelzl@37489
  1821
  thus "x = y"
hoelzl@37489
  1822
    by (subst (1 2) euclidean_representation) auto
hoelzl@37489
  1823
qed
hoelzl@37489
  1824
hoelzl@37489
  1825
lemma euclidean_lambda_beta[simp]:
hoelzl@37489
  1826
  "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
hoelzl@37489
  1827
  by (auto simp: euclidean_simps Chi_def if_distrib setsum_cases
hoelzl@37489
  1828
           intro!: setsum_cong)
hoelzl@37489
  1829
hoelzl@37489
  1830
lemma euclidean_lambda_beta':
hoelzl@37489
  1831
  "j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j"
hoelzl@37489
  1832
  by simp
hoelzl@37489
  1833
hoelzl@37489
  1834
lemma euclidean_lambda_beta'':"(\<forall>j < DIM('a::euclidean_space). P j (((\<chi>\<chi> i. f i)::'a) $$ j)) \<longleftrightarrow>
hoelzl@37489
  1835
  (\<forall>j < DIM('a::euclidean_space). P j (f j))" by auto
hoelzl@37489
  1836
hoelzl@37489
  1837
lemma euclidean_beta_reduce[simp]:
hoelzl@37489
  1838
  "(\<chi>\<chi> i. x $$ i) = (x::'a::euclidean_space)"
hoelzl@37489
  1839
  by (subst euclidean_eq) (simp add: euclidean_lambda_beta)
hoelzl@37489
  1840
hoelzl@37489
  1841
lemma euclidean_lambda_beta_0[simp]:
hoelzl@37489
  1842
    "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ 0 = f 0"
hoelzl@37489
  1843
  by (simp add: DIM_positive)
hoelzl@37489
  1844
hoelzl@37489
  1845
lemma euclidean_inner:
hoelzl@37489
  1846
  "x \<bullet> (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) \<bullet> (y $$ i))"
hoelzl@37489
  1847
proof -
hoelzl@37489
  1848
  have "x \<bullet> y = (\<Sum>i<DIM('a). x $$ i *\<^sub>R basis i) \<bullet>
hoelzl@37489
  1849
                (\<Sum>i<DIM('a). y $$ i *\<^sub>R (basis i :: 'a))"
hoelzl@37489
  1850
    by (subst (1 2) euclidean_representation) simp
hoelzl@37489
  1851
  also have "\<dots> = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) \<bullet> (y $$ i))"
hoelzl@37489
  1852
    unfolding inner_left.setsum inner_right.setsum
hoelzl@37489
  1853
    by (auto simp add: dot_basis if_distrib setsum_cases intro!: setsum_cong)
hoelzl@37489
  1854
  finally show ?thesis .
hoelzl@37489
  1855
qed
hoelzl@37489
  1856
hoelzl@37489
  1857
lemma norm_basis[simp]:"norm (basis i::'a::euclidean_space) = (if i<DIM('a) then 1 else 0)"
hoelzl@37489
  1858
  unfolding norm_eq_sqrt_inner dot_basis by auto
hoelzl@37489
  1859
hoelzl@37489
  1860
lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
hoelzl@37489
  1861
  unfolding euclidean_component_def
hoelzl@37489
  1862
  apply(rule order_trans[OF real_inner_class.Cauchy_Schwarz_ineq2]) by auto
hoelzl@37489
  1863
hoelzl@37489
  1864
lemma norm_bound_component_le: "norm (x::'a::euclidean_space) \<le> e \<Longrightarrow> \<bar>x$$i\<bar> <= e"
hoelzl@37489
  1865
  by (metis component_le_norm order_trans)
hoelzl@37489
  1866
hoelzl@37489
  1867
lemma norm_bound_component_lt: "norm (x::'a::euclidean_space) < e \<Longrightarrow> \<bar>x$$i\<bar> < e"
hoelzl@37489
  1868
  by (metis component_le_norm basic_trans_rules(21))
hoelzl@37489
  1869
hoelzl@37489
  1870
lemma norm_le_l1: "norm (x::'a::euclidean_space) \<le> (\<Sum>i<DIM('a). \<bar>x $$ i\<bar>)"
hoelzl@37489
  1871
  apply (subst euclidean_representation[of x])
hoelzl@37489
  1872
  apply (rule order_trans[OF setsum_norm])
hoelzl@37489
  1873
  by (auto intro!: setsum_mono)
hoelzl@37489
  1874
hoelzl@37489
  1875
lemma setsum_norm_allsubsets_bound:
hoelzl@37489
  1876
  fixes f:: "'a \<Rightarrow> 'n::euclidean_space"
hoelzl@37489
  1877
  assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
hoelzl@37489
  1878
  shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real DIM('n) *  e"
hoelzl@37489
  1879
proof-
hoelzl@37489
  1880
  let ?d = "real DIM('n)"
hoelzl@37489
  1881
  let ?nf = "\<lambda>x. norm (f x)"
hoelzl@37489
  1882
  let ?U = "{..<DIM('n)}"
hoelzl@37489
  1883
  have th0: "setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $$ i\<bar>) ?U) P = setsum (\<lambda>i. setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P) ?U"
hoelzl@37489
  1884
    by (rule setsum_commute)
hoelzl@37489
  1885
  have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def)
hoelzl@37489
  1886
  have "setsum ?nf P \<le> setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $$ i\<bar>) ?U) P"
hoelzl@37489
  1887
    apply (rule setsum_mono)    by (rule norm_le_l1)
hoelzl@37489
  1888
  also have "\<dots> \<le> 2 * ?d * e"
hoelzl@37489
  1889
    unfolding th0 th1
hoelzl@37489
  1890
  proof(rule setsum_bounded)
hoelzl@37489
  1891
    fix i assume i: "i \<in> ?U"
hoelzl@37489
  1892
    let ?Pp = "{x. x\<in> P \<and> f x $$ i \<ge> 0}"
hoelzl@37489
  1893
    let ?Pn = "{x. x \<in> P \<and> f x $$ i < 0}"
hoelzl@37489
  1894
    have thp: "P = ?Pp \<union> ?Pn" by auto
hoelzl@37489
  1895
    have thp0: "?Pp \<inter> ?Pn ={}" by auto
hoelzl@37489
  1896
    have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
hoelzl@37489
  1897
    have Ppe:"setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp \<le> e"
hoelzl@37489
  1898
      using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i]  fPs[OF PpP]
hoelzl@37489
  1899
      unfolding euclidean_component.setsum by(auto intro: abs_le_D1)
hoelzl@37489
  1900
    have Pne: "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn \<le> e"
hoelzl@37489
  1901
      using component_le_norm[of "setsum (\<lambda>x. - f x) ?Pn" i]  fPs[OF PnP]
hoelzl@37489
  1902
      unfolding euclidean_component.setsum euclidean_component.minus
hoelzl@37489
  1903
      by(auto simp add: setsum_negf intro: abs_le_D1)
hoelzl@37489
  1904
    have "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn"
hoelzl@37489
  1905
      apply (subst thp)
hoelzl@37489
  1906
      apply (rule setsum_Un_zero)
hoelzl@37489
  1907
      using fP thp0 by auto
hoelzl@37489
  1908
    also have "\<dots> \<le> 2*e" using Pne Ppe by arith
hoelzl@37489
  1909
    finally show "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P \<le> 2*e" .
hoelzl@37489
  1910
  qed
hoelzl@37489
  1911
  finally show ?thesis .
hoelzl@37489
  1912
qed
hoelzl@37489
  1913
hoelzl@37489
  1914
lemma choice_iff': "(\<forall>x<d. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x<d. P x (f x))" by metis
hoelzl@37489
  1915
hoelzl@37489
  1916
lemma lambda_skolem': "(\<forall>i<DIM('a::euclidean_space). \<exists>x. P i x) \<longleftrightarrow>
hoelzl@37489
  1917
   (\<exists>x::'a. \<forall>i<DIM('a). P i (x$$i))" (is "?lhs \<longleftrightarrow> ?rhs")
hoelzl@37489
  1918
proof-
hoelzl@37489
  1919
  let ?S = "{..<DIM('a)}"
hoelzl@37489
  1920
  {assume H: "?rhs"
hoelzl@37489
  1921
    then have ?lhs by auto}
hoelzl@37489
  1922
  moreover
hoelzl@37489
  1923
  {assume H: "?lhs"
hoelzl@37489
  1924
    then obtain f where f:"\<forall>i<DIM('a). P i (f i)" unfolding choice_iff' by metis
hoelzl@37489
  1925
    let ?x = "(\<chi>\<chi> i. (f i)) :: 'a"
hoelzl@37489
  1926
    {fix i assume i:"i<DIM('a)"
hoelzl@37489
  1927
      with f have "P i (f i)" by metis
hoelzl@37489
  1928
      then have "P i (?x$$i)" using i by auto
hoelzl@37489
  1929
    }
hoelzl@37489
  1930
    hence "\<forall>i<DIM('a). P i (?x$$i)" by metis
hoelzl@37489
  1931
    hence ?rhs by metis }
hoelzl@37489
  1932
  ultimately show ?thesis by metis
hoelzl@37489
  1933
qed
hoelzl@37489
  1934
hoelzl@37489
  1935
subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
hoelzl@37489
  1936
hoelzl@37489
  1937
class ordered_euclidean_space = ord + euclidean_space +
hoelzl@37489
  1938
  assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i \<le> y $$ i)"
hoelzl@37489
  1939
  and eucl_less: "x < y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i < y $$ i)"
hoelzl@37489
  1940
hoelzl@38656
  1941
lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
hoelzl@38656
  1942
  unfolding eucl_less[where 'a='a] by auto
hoelzl@38656
  1943
hoelzl@38656
  1944
lemma euclidean_trans[trans]:
hoelzl@38656
  1945
  fixes x y z :: "'a::ordered_euclidean_space"
hoelzl@38656
  1946
  shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
hoelzl@38656
  1947
  and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
hoelzl@38656
  1948
  and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
hoelzl@38656
  1949
  by (force simp: eucl_less[where 'a='a] eucl_le[where 'a='a])+
hoelzl@38656
  1950
hoelzl@37489
  1951
subsection {* Linearity and Bilinearity continued *}
hoelzl@37489
  1952
hoelzl@37489
  1953
lemma linear_bounded:
huffman@37645
  1954
  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
hoelzl@37489
  1955
  assumes lf: "linear f"
hoelzl@37489
  1956
  shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
hoelzl@37489
  1957
proof-
hoelzl@37489
  1958
  let ?S = "{..<DIM('a)}"
hoelzl@37489
  1959
  let ?B = "setsum (\<lambda>i. norm(f(basis i))) ?S"
hoelzl@37489
  1960
  have fS: "finite ?S" by simp
hoelzl@37489
  1961
  {fix x:: "'a"
hoelzl@37489
  1962
    let ?g = "(\<lambda> i. (x$$i) *\<^sub>R (basis i) :: 'a)"
hoelzl@37489
  1963
    have "norm (f x) = norm (f (setsum (\<lambda>i. (x$$i) *\<^sub>R (basis i)) ?S))"
hoelzl@37489
  1964
      apply(subst euclidean_representation[of x]) ..
hoelzl@37489
  1965
    also have "\<dots> = norm (setsum (\<lambda> i. (x$$i) *\<^sub>R f (basis i)) ?S)"
hoelzl@37489
  1966
      using linear_setsum[OF lf fS, of ?g, unfolded o_def] linear_cmul[OF lf] by auto
hoelzl@37489
  1967
    finally have th0: "norm (f x) = norm (setsum (\<lambda>i. (x$$i) *\<^sub>R f (basis i))?S)" .
hoelzl@37489
  1968
    {fix i assume i: "i \<in> ?S"
hoelzl@37489
  1969
      from component_le_norm[of x i]
hoelzl@37489
  1970
      have "norm ((x$$i) *\<^sub>R f (basis i :: 'a)) \<le> norm (f (basis i)) * norm x"
hoelzl@37489
  1971
      unfolding norm_scaleR
hoelzl@37489
  1972
      apply (simp only: mult_commute)
hoelzl@37489
  1973
      apply (rule mult_mono)
hoelzl@37489
  1974
      by (auto simp add: field_simps) }
hoelzl@37489
  1975
    then have th: "\<forall>i\<in> ?S. norm ((x$$i) *\<^sub>R f (basis i :: 'a)) \<le> norm (f (basis i)) * norm x" by metis
hoelzl@37489
  1976
    from setsum_norm_le[OF fS, of "\<lambda>i. (x$$i) *\<^sub>R (f (basis i))", OF th]
hoelzl@37489
  1977
    have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
hoelzl@37489
  1978
  then show ?thesis by blast
hoelzl@37489
  1979
qed
hoelzl@37489
  1980
hoelzl@37489
  1981
lemma linear_bounded_pos:
huffman@37645
  1982
  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
hoelzl@37489
  1983
  assumes lf: "linear f"
hoelzl@37489
  1984
  shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
hoelzl@37489
  1985
proof-
hoelzl@37489
  1986
  from linear_bounded[OF lf] obtain B where
hoelzl@37489
  1987
    B: "\<forall>x. norm (f x) \<le> B * norm x" by blast
hoelzl@37489
  1988
  let ?K = "\<bar>B\<bar> + 1"
hoelzl@37489
  1989
  have Kp: "?K > 0" by arith
hoelzl@37489
  1990
    { assume C: "B < 0"
hoelzl@37489
  1991
      have "((\<chi>\<chi> i. 1)::'a) \<noteq> 0" unfolding euclidean_eq[where 'a='a]
hoelzl@37489
  1992
        by(auto intro!:exI[where x=0] simp add:euclidean_component.zero)
hoelzl@37489
  1993
      hence "norm ((\<chi>\<chi> i. 1)::'a) > 0" by auto
hoelzl@37489
  1994
      with C have "B * norm ((\<chi>\<chi> i. 1)::'a) < 0"
hoelzl@37489
  1995
        by (simp add: mult_less_0_iff)
hoelzl@37489
  1996
      with B[rule_format, of "(\<chi>\<chi> i. 1)::'a"] norm_ge_zero[of "f ((\<chi>\<chi> i. 1)::'a)"] have False by simp
hoelzl@37489
  1997
    }
hoelzl@37489
  1998
    then have Bp: "B \<ge> 0" by ferrack
hoelzl@37489
  1999
    {fix x::"'a"
hoelzl@37489
  2000
      have "norm (f x) \<le> ?K *  norm x"
hoelzl@37489
  2001
      using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
hoelzl@37489
  2002
      apply (auto simp add: field_simps split add: abs_split)
hoelzl@37489
  2003
      apply (erule order_trans, simp)
hoelzl@37489
  2004
      done
hoelzl@37489
  2005
  }
hoelzl@37489
  2006
  then show ?thesis using Kp by blast
hoelzl@37489
  2007
qed
hoelzl@37489
  2008
hoelzl@37489
  2009
lemma linear_conv_bounded_linear:
huffman@37645
  2010
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
hoelzl@37489
  2011
  shows "linear f \<longleftrightarrow> bounded_linear f"
hoelzl@37489
  2012
proof
hoelzl@37489
  2013
  assume "linear f"
hoelzl@37489
  2014
  show "bounded_linear f"
hoelzl@37489
  2015
  proof
hoelzl@37489
  2016
    fix x y show "f (x + y) = f x + f y"
hoelzl@37489
  2017
      using `linear f` unfolding linear_def by simp
hoelzl@37489
  2018
  next
hoelzl@37489
  2019
    fix r x show "f (scaleR r x) = scaleR r (f x)"
hoelzl@37489
  2020
      using `linear f` unfolding linear_def by simp
hoelzl@37489
  2021
  next
hoelzl@37489
  2022
    have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
hoelzl@37489
  2023
      using `linear f` by (rule linear_bounded)
hoelzl@37489
  2024
    thus "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
hoelzl@37489
  2025
      by (simp add: mult_commute)
hoelzl@37489
  2026
  qed
hoelzl@37489
  2027
next
hoelzl@37489
  2028
  assume "bounded_linear f"
hoelzl@37489
  2029
  then interpret f: bounded_linear f .
hoelzl@37489
  2030
  show "linear f"
hoelzl@37489
  2031
    by (simp add: f.add f.scaleR linear_def)
hoelzl@37489
  2032
qed
hoelzl@37489
  2033
huffman@37645
  2034
lemma bounded_linearI': fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
hoelzl@37489
  2035
  assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
hoelzl@37489
  2036
  shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym]
hoelzl@37489
  2037
  by(rule linearI[OF assms])
hoelzl@37489
  2038
hoelzl@37489
  2039
hoelzl@37489
  2040
lemma bilinear_bounded:
huffman@37645
  2041
  fixes h:: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
hoelzl@37489
  2042
  assumes bh: "bilinear h"
hoelzl@37489
  2043
  shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
hoelzl@37489
  2044
proof-
hoelzl@37489
  2045
  let ?M = "{..<DIM('m)}"
hoelzl@37489
  2046
  let ?N = "{..<DIM('n)}"
hoelzl@37489
  2047
  let ?B = "setsum (\<lambda>(i,j). norm (h (basis i) (basis j))) (?M \<times> ?N)"
hoelzl@37489
  2048
  have fM: "finite ?M" and fN: "finite ?N" by simp_all
hoelzl@37489
  2049
  {fix x:: "'m" and  y :: "'n"
hoelzl@37489
  2050
    have "norm (h x y) = norm (h (setsum (\<lambda>i. (x$$i) *\<^sub>R basis i) ?M) (setsum (\<lambda>i. (y$$i) *\<^sub>R basis i) ?N))" 
hoelzl@37489
  2051
      apply(subst euclidean_representation[where 'a='m])
hoelzl@37489
  2052
      apply(subst euclidean_representation[where 'a='n]) ..
hoelzl@37489
  2053
    also have "\<dots> = norm (setsum (\<lambda> (i,j). h ((x$$i) *\<^sub>R basis i) ((y$$j) *\<^sub>R basis j)) (?M \<times> ?N))"  
hoelzl@37489
  2054
      unfolding bilinear_setsum[OF bh fM fN] ..
hoelzl@37489
  2055
    finally have th: "norm (h x y) = \<dots>" .
hoelzl@37489
  2056
    have "norm (h x y) \<le> ?B * norm x * norm y"
hoelzl@37489
  2057
      apply (simp add: setsum_left_distrib th)
hoelzl@37489
  2058
      apply (rule setsum_norm_le)
hoelzl@37489
  2059
      using fN fM
hoelzl@37489
  2060
      apply simp
hoelzl@37489
  2061
      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps simp del: scaleR_scaleR)
hoelzl@37489
  2062
      apply (rule mult_mono)
hoelzl@37489
  2063
      apply (auto simp add: zero_le_mult_iff component_le_norm)
hoelzl@37489
  2064
      apply (rule mult_mono)
hoelzl@37489
  2065
      apply (auto simp add: zero_le_mult_iff component_le_norm)
hoelzl@37489
  2066
      done}
hoelzl@37489
  2067
  then show ?thesis by metis
hoelzl@37489
  2068
qed
hoelzl@37489
  2069
hoelzl@37489
  2070
lemma bilinear_bounded_pos:
huffman@37645
  2071
  fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
hoelzl@37489
  2072
  assumes bh: "bilinear h"
hoelzl@37489
  2073
  shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
hoelzl@37489
  2074
proof-
hoelzl@37489
  2075
  from bilinear_bounded[OF bh] obtain B where
hoelzl@37489
  2076
    B: "\<forall>x y. norm (h x y) \<le> B * norm x * norm y" by blast
hoelzl@37489
  2077
  let ?K = "\<bar>B\<bar> + 1"
hoelzl@37489
  2078
  have Kp: "?K > 0" by arith
hoelzl@37489
  2079
  have KB: "B < ?K" by arith
hoelzl@37489
  2080
  {fix x::'a and y::'b
hoelzl@37489
  2081
    from KB Kp
hoelzl@37489
  2082
    have "B * norm x * norm y \<le> ?K * norm x * norm y"
hoelzl@37489
  2083
      apply -
hoelzl@37489
  2084
      apply (rule mult_right_mono, rule mult_right_mono)
hoelzl@37489
  2085
      by auto
hoelzl@37489
  2086
    then have "norm (h x y) \<le> ?K * norm x * norm y"
hoelzl@37489
  2087
      using B[rule_format, of x y] by simp}
hoelzl@37489
  2088
  with Kp show ?thesis by blast
hoelzl@37489
  2089
qed
hoelzl@37489
  2090
hoelzl@37489
  2091
lemma bilinear_conv_bounded_bilinear:
huffman@37645
  2092
  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
hoelzl@37489
  2093
  shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
hoelzl@37489
  2094
proof
hoelzl@37489
  2095
  assume "bilinear h"
hoelzl@37489
  2096
  show "bounded_bilinear h"
hoelzl@37489
  2097
  proof
hoelzl@37489
  2098
    fix x y z show "h (x + y) z = h x z + h y z"
hoelzl@37489
  2099
      using `bilinear h` unfolding bilinear_def linear_def by simp
hoelzl@37489
  2100
  next
hoelzl@37489
  2101
    fix x y z show "h x (y + z) = h x y + h x z"
hoelzl@37489
  2102
      using `bilinear h` unfolding bilinear_def linear_def by simp
hoelzl@37489
  2103
  next
hoelzl@37489
  2104
    fix r x y show "h (scaleR r x) y = scaleR r (h x y)"
hoelzl@37489
  2105
      using `bilinear h` unfolding bilinear_def linear_def
hoelzl@37489
  2106
      by simp
hoelzl@37489
  2107
  next
hoelzl@37489
  2108
    fix r x y show "h x (scaleR r y) = scaleR r (h x y)"
hoelzl@37489
  2109
      using `bilinear h` unfolding bilinear_def linear_def
hoelzl@37489
  2110
      by simp
hoelzl@37489
  2111
  next
hoelzl@37489
  2112
    have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
hoelzl@37489
  2113
      using `bilinear h` by (rule bilinear_bounded)
hoelzl@37489
  2114
    thus "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
hoelzl@37489
  2115
      by (simp add: mult_ac)
hoelzl@37489
  2116
  qed
hoelzl@37489
  2117
next
hoelzl@37489
  2118
  assume "bounded_bilinear h"
hoelzl@37489
  2119
  then interpret h: bounded_bilinear h .
hoelzl@37489
  2120
  show "bilinear h"
hoelzl@37489
  2121
    unfolding bilinear_def linear_conv_bounded_linear
hoelzl@37489
  2122
    using h.bounded_linear_left h.bounded_linear_right
hoelzl@37489
  2123
    by simp
hoelzl@37489
  2124
qed
hoelzl@37489
  2125
hoelzl@37489
  2126
subsection {* We continue. *}
hoelzl@37489
  2127
himmelma@33175
  2128
lemma independent_bound:
hoelzl@37489
  2129
  fixes S:: "('a::euclidean_space) set"
hoelzl@37489
  2130
  shows "independent S \<Longrightarrow> finite S \<and> card S <= DIM('a::euclidean_space)"
hoelzl@37489
  2131
  using independent_span_bound[of "(basis::nat=>'a) ` {..<DIM('a)}" S] by auto
hoelzl@37489
  2132
hoelzl@37489
  2133
lemma dependent_biggerset: "(finite (S::('a::euclidean_space) set) ==> card S > DIM('a)) ==> dependent S"
himmelma@33175
  2134
  by (metis independent_bound not_less)
himmelma@33175
  2135
huffman@36666
  2136
text {* Hence we can create a maximal independent subset. *}
himmelma@33175
  2137
himmelma@33175
  2138
lemma maximal_independent_subset_extend:
hoelzl@37489
  2139
  assumes sv: "(S::('a::euclidean_space) set) \<subseteq> V" and iS: "independent S"
himmelma@33175
  2140
  shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
himmelma@33175
  2141
  using sv iS
hoelzl@37489
  2142
proof(induct "DIM('a) - card S" arbitrary: S rule: less_induct)
berghofe@34915
  2143
  case less
berghofe@34915
  2144
  note sv = `S \<subseteq> V` and i = `independent S`
himmelma@33175
  2145
  let ?P = "\<lambda>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
himmelma@33175
  2146
  let ?ths = "\<exists>x. ?P x"
hoelzl@37489
  2147
  let ?d = "DIM('a)"
himmelma@33175
  2148
  {assume "V \<subseteq> span S"
himmelma@33175
  2149
    then have ?ths  using sv i by blast }
himmelma@33175
  2150
  moreover
himmelma@33175
  2151
  {assume VS: "\<not> V \<subseteq> span S"
himmelma@33175
  2152
    from VS obtain a where a: "a \<in> V" "a \<notin> span S" by blast
himmelma@33175
  2153
    from a have aS: "a \<notin> S" by (auto simp add: span_superset)
himmelma@33175
  2154
    have th0: "insert a S \<subseteq> V" using a sv by blast
himmelma@33175
  2155
    from independent_insert[of a S]  i a
himmelma@33175
  2156
    have th1: "independent (insert a S)" by auto
berghofe@34915
  2157
    have mlt: "?d - card (insert a S) < ?d - card S"
berghofe@34915
  2158
      using aS a independent_bound[OF th1]
himmelma@33175
  2159
      by auto
himmelma@33175
  2160
berghofe@34915
  2161
    from less(1)[OF mlt th0 th1]
himmelma@33175
  2162
    obtain B where B: "insert a S \<subseteq> B" "B \<subseteq> V" "independent B" " V \<subseteq> span B"
himmelma@33175
  2163
      by blast
himmelma@33175
  2164
    from B have "?P B" by auto
himmelma@33175
  2165
    then have ?ths by blast}
himmelma@33175
  2166
  ultimately show ?ths by blast
himmelma@33175
  2167
qed
himmelma@33175
  2168
himmelma@33175
  2169
lemma maximal_independent_subset:
hoelzl@37489
  2170
  "\<exists>(B:: ('a::euclidean_space) set). B\<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
hoelzl@37489
  2171
  by (metis maximal_independent_subset_extend[of "{}:: ('a::euclidean_space) set"] empty_subsetI independent_empty)
hoelzl@37489
  2172
himmelma@33175
  2173
huffman@36666
  2174
text {* Notion of dimension. *}
himmelma@33175
  2175
hoelzl@33715
  2176
definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = n))"
hoelzl@33715
  2177
hoelzl@37489
  2178
lemma basis_exists:  "\<exists>B. (B :: ('a::euclidean_space) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = dim V)"
hoelzl@33715
  2179
unfolding dim_def some_eq_ex[of "\<lambda>n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = n)"]
himmelma@33175
  2180
using maximal_independent_subset[of V] independent_bound
himmelma@33175
  2181
by auto
himmelma@33175
  2182
huffman@36666
  2183
text {* Consequences of independence or spanning for cardinality. *}
himmelma@33175
  2184
hoelzl@33715
  2185
lemma independent_card_le_dim: 
hoelzl@37489
  2186
  assumes "(B::('a::euclidean_space) set) \<subseteq> V" and "independent B" shows "card B \<le> dim V"
hoelzl@33715
  2187
proof -
hoelzl@33715
  2188
  from basis_exists[of V] `B \<subseteq> V`
hoelzl@33715
  2189
  obtain B' where "independent B'" and "B \<subseteq> span B'" and "card B' = dim V" by blast
hoelzl@33715
  2190
  with independent_span_bound[OF _ `independent B` `B \<subseteq> span B'`] independent_bound[of B']
hoelzl@33715
  2191
  show ?thesis by auto
hoelzl@33715
  2192
qed
himmelma@33175
  2193
hoelzl@37489
  2194
lemma span_card_ge_dim:  "(B::('a::euclidean_space) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> finite B \<Longrightarrow> dim V \<le> card B"
hoelzl@33715
  2195
  by (metis basis_exists[of V] independent_span_bound subset_trans)
himmelma@33175
  2196
himmelma@33175
  2197
lemma basis_card_eq_dim:
hoelzl@37489
  2198
  "B \<subseteq> (V:: ('a::euclidean_space) set) \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B = dim V"
huffman@36362
  2199
  by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_bound)
hoelzl@33715
  2200
hoelzl@37489
  2201
lemma dim_unique: "(B::('a::euclidean_space) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = n \<Longrightarrow> dim V = n"
hoelzl@33715
  2202
  by (metis basis_card_eq_dim)
himmelma@33175
  2203
huffman@36666
  2204
text {* More lemmas about dimension. *}
himmelma@33175
  2205
hoelzl@37489
  2206
lemma dim_UNIV: "dim (UNIV :: ('a::euclidean_space) set) = DIM('a)"
hoelzl@37489
  2207
  apply (rule dim_unique[of "(basis::nat=>'a) ` {..<DIM('a)}"])
hoelzl@37489
  2208
  using independent_basis by auto
himmelma@33175
  2209
himmelma@33175
  2210
lemma dim_subset:
hoelzl@37489
  2211
  "(S:: ('a::euclidean_space) set) \<subseteq> T \<Longrightarrow> dim S \<le> dim T"
himmelma@33175
  2212
  using basis_exists[of T] basis_exists[of S]
hoelzl@33715
  2213
  by (metis independent_card_le_dim subset_trans)
himmelma@33175
  2214
hoelzl@37489
  2215
lemma dim_subset_UNIV: "dim (S:: ('a::euclidean_space) set) \<le> DIM('a)"
hoelzl@37489
  2216
  by (metis dim_subset subset_UNIV dim_UNIV)
himmelma@33175
  2217
huffman@36666
  2218
text {* Converses to those. *}
himmelma@33175
  2219
himmelma@33175
  2220
lemma card_ge_dim_independent:
hoelzl@37489
  2221
  assumes BV:"(B::('a::euclidean_space) set) \<subseteq> V" and iB:"independent B" and dVB:"dim V \<le> card B"
himmelma@33175
  2222
  shows "V \<subseteq> span B"
himmelma@33175
  2223
proof-
himmelma@33175
  2224
  {fix a assume aV: "a \<in> V"
himmelma@33175
  2225
    {assume aB: "a \<notin> span B"
himmelma@33175
  2226
      then have iaB: "independent (insert a B)" using iB aV  BV by (simp add: independent_insert)
himmelma@33175
  2227
      from aV BV have th0: "insert a B \<subseteq> V" by blast
himmelma@33175
  2228
      from aB have "a \<notin>B" by (auto simp add: span_superset)
hoelzl@33715
  2229
      with independent_card_le_dim[OF th0 iaB] dVB independent_bound[OF iB] have False by auto }
himmelma@33175
  2230
    then have "a \<in> span B"  by blast}
himmelma@33175
  2231
  then show ?thesis by blast
himmelma@33175
  2232
qed
himmelma@33175
  2233
himmelma@33175
  2234
lemma card_le_dim_spanning:
hoelzl@37489
  2235
  assumes BV: "(B:: ('a::euclidean_space) set) \<subseteq> V" and VB: "V \<subseteq> span B"
himmelma@33175
  2236
  and fB: "finite B" and dVB: "dim V \<ge> card B"
himmelma@33175
  2237
  shows "independent B"
himmelma@33175
  2238
proof-
himmelma@33175
  2239
  {fix a assume a: "a \<in> B" "a \<in> span (B -{a})"
himmelma@33175
  2240
    from a fB have c0: "card B \<noteq> 0" by auto
himmelma@33175
  2241
    from a fB have cb: "card (B -{a}) = card B - 1" by auto
himmelma@33175
  2242
    from BV a have th0: "B -{a} \<subseteq> V" by blast
himmelma@33175
  2243
    {fix x assume x: "x \<in> V"
himmelma@33175
  2244
      from a have eq: "insert a (B -{a}) = B" by blast
himmelma@33175
  2245
      from x VB have x': "x \<in> span B" by blast
himmelma@33175
  2246
      from span_trans[OF a(2), unfolded eq, OF x']
himmelma@33175
  2247
      have "x \<in> span (B -{a})" . }
himmelma@33175
  2248
    then have th1: "V \<subseteq> span (B -{a})" by blast
himmelma@33175
  2249
    have th2: "finite (B -{a})" using fB by auto
himmelma@33175
  2250
    from span_card_ge_dim[OF th0 th1 th2]
himmelma@33175
  2251
    have c: "dim V \<le> card (B -{a})" .
himmelma@33175
  2252
    from c c0 dVB cb have False by simp}
himmelma@33175
  2253
  then show ?thesis unfolding dependent_def by blast
himmelma@33175
  2254
qed
himmelma@33175
  2255
hoelzl@37489
  2256
lemma card_eq_dim: "(B:: ('a::euclidean_space) set) \<subseteq> V \<Longrightarrow> card B = dim V \<Longrightarrow> finite B \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B"
hoelzl@33715
  2257
  by (metis order_eq_iff card_le_dim_spanning
himmelma@33175
  2258
    card_ge_dim_independent)
him