src/HOL/Analysis/Linear_Algebra.thy
 changeset 68072 493b818e8e10 parent 67982 7643b005b29a child 68073 fad29d2a17a5
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Apr 18 21:12:50 2018 +0100
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed May 02 13:49:38 2018 +0200
1.3 @@ -23,8 +23,8 @@
1.4    show "f (a + b) = f a + f b" by (rule f.add)
1.5    show "f (a - b) = f a - f b" by (rule f.diff)
1.6    show "f 0 = 0" by (rule f.zero)
1.7 -  show "f (- a) = - f a" by (rule f.minus)
1.8 -  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
1.9 +  show "f (- a) = - f a" by (rule f.neg)
1.10 +  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scale)
1.11  qed
1.12
1.13  lemma bounded_linearI:
1.14 @@ -34,1312 +34,6 @@
1.15    shows "bounded_linear f"
1.16    using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
1.17
1.18 -subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
1.19 -
1.20 -definition%important hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
1.21 -  where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
1.22 -
1.23 -lemma hull_same: "S s \<Longrightarrow> S hull s = s"
1.24 -  unfolding hull_def by auto
1.25 -
1.26 -lemma hull_in: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> S (S hull s)"
1.27 -  unfolding hull_def Ball_def by auto
1.28 -
1.29 -lemma hull_eq: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> (S hull s) = s \<longleftrightarrow> S s"
1.30 -  using hull_same[of S s] hull_in[of S s] by metis
1.31 -
1.32 -lemma hull_hull [simp]: "S hull (S hull s) = S hull s"
1.33 -  unfolding hull_def by blast
1.34 -
1.35 -lemma hull_subset[intro]: "s \<subseteq> (S hull s)"
1.36 -  unfolding hull_def by blast
1.37 -
1.38 -lemma hull_mono: "s \<subseteq> t \<Longrightarrow> (S hull s) \<subseteq> (S hull t)"
1.39 -  unfolding hull_def by blast
1.40 -
1.41 -lemma hull_antimono: "\<forall>x. S x \<longrightarrow> T x \<Longrightarrow> (T hull s) \<subseteq> (S hull s)"
1.42 -  unfolding hull_def by blast
1.43 -
1.44 -lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (S hull s) \<subseteq> t"
1.45 -  unfolding hull_def by blast
1.46 -
1.47 -lemma subset_hull: "S t \<Longrightarrow> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
1.48 -  unfolding hull_def by blast
1.49 -
1.50 -lemma hull_UNIV [simp]: "S hull UNIV = UNIV"
1.51 -  unfolding hull_def by auto
1.52 -
1.53 -lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
1.54 -  unfolding hull_def by auto
1.55 -
1.56 -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"
1.57 -  using hull_minimal[of S "{x. P x}" Q]
1.58 -  by (auto simp add: subset_eq)
1.59 -
1.60 -lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S"
1.61 -  by (metis hull_subset subset_eq)
1.62 -
1.63 -lemma hull_Un_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
1.64 -  unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
1.65 -
1.66 -lemma hull_Un:
1.67 -  assumes T: "\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)"
1.68 -  shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
1.69 -  apply (rule equalityI)
1.70 -  apply (meson hull_mono hull_subset sup.mono)
1.71 -  by (metis hull_Un_subset hull_hull hull_mono)
1.72 -
1.73 -lemma hull_Un_left: "P hull (S \<union> T) = P hull (P hull S \<union> T)"
1.74 -  apply (rule equalityI)
1.75 -   apply (simp add: Un_commute hull_mono hull_subset sup.coboundedI2)
1.76 -  by (metis Un_subset_iff hull_hull hull_mono hull_subset)
1.77 -
1.78 -lemma hull_Un_right: "P hull (S \<union> T) = P hull (S \<union> P hull T)"
1.79 -  by (metis hull_Un_left sup.commute)
1.80 -
1.81 -lemma hull_insert:
1.82 -   "P hull (insert a S) = P hull (insert a (P hull S))"
1.83 -  by (metis hull_Un_right insert_is_Un)
1.84 -
1.85 -lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> S hull (insert a s) = S hull s"
1.86 -  unfolding hull_def by blast
1.87 -
1.88 -lemma hull_redundant: "a \<in> (S hull s) \<Longrightarrow> S hull (insert a s) = S hull s"
1.89 -  by (metis hull_redundant_eq)
1.90 -
1.91 -subsection \<open>Linear functions.\<close>
1.92 -
1.93 -lemma%important linear_iff:
1.94 -  "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)"
1.95 -  (is "linear f \<longleftrightarrow> ?rhs")
1.96 -proof%unimportant
1.97 -  assume "linear f"
1.98 -  then interpret f: linear f .
1.100 -next
1.101 -  assume "?rhs"
1.102 -  then show "linear f" by unfold_locales simp_all
1.103 -qed
1.104 -
1.105 -lemma linear_compose_cmul: "linear f \<Longrightarrow> linear (\<lambda>x. c *\<^sub>R f x)"
1.106 -  by (simp add: linear_iff algebra_simps)
1.107 -
1.108 -lemma linear_compose_scaleR: "linear f \<Longrightarrow> linear (\<lambda>x. f x *\<^sub>R c)"
1.110 -
1.111 -lemma linear_compose_neg: "linear f \<Longrightarrow> linear (\<lambda>x. - f x)"
1.112 -  by (simp add: linear_iff)
1.113 -
1.114 -lemma linear_compose_add: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (\<lambda>x. f x + g x)"
1.115 -  by (simp add: linear_iff algebra_simps)
1.116 -
1.117 -lemma linear_compose_sub: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (\<lambda>x. f x - g x)"
1.118 -  by (simp add: linear_iff algebra_simps)
1.119 -
1.120 -lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g \<circ> f)"
1.121 -  by (simp add: linear_iff)
1.122 -
1.123 -lemma linear_id: "linear id"
1.124 -  by (simp add: linear_iff id_def)
1.125 -
1.126 -lemma linear_zero: "linear (\<lambda>x. 0)"
1.127 -  by (simp add: linear_iff)
1.128 -
1.129 -lemma linear_uminus: "linear uminus"
1.131 -
1.132 -lemma linear_compose_sum:
1.133 -  assumes lS: "\<forall>a \<in> S. linear (f a)"
1.134 -  shows "linear (\<lambda>x. sum (\<lambda>a. f a x) S)"
1.135 -proof (cases "finite S")
1.136 -  case True
1.137 -  then show ?thesis
1.139 -next
1.140 -  case False
1.141 -  then show ?thesis
1.142 -    by (simp add: linear_zero)
1.143 -qed
1.144 -
1.145 -lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
1.146 -  unfolding linear_iff
1.147 -  apply clarsimp
1.148 -  apply (erule allE[where x="0::'a"])
1.149 -  apply simp
1.150 -  done
1.151 -
1.152 -lemma linear_cmul: "linear f \<Longrightarrow> f (c *\<^sub>R x) = c *\<^sub>R f x"
1.153 -  by (rule linear.scaleR)
1.154 -
1.155 -lemma linear_neg: "linear f \<Longrightarrow> f (- x) = - f x"
1.156 -  using linear_cmul [where c="-1"] by simp
1.157 -
1.158 -lemma linear_add: "linear f \<Longrightarrow> f (x + y) = f x + f y"
1.159 -  by (metis linear_iff)
1.160 -
1.161 -lemma linear_diff: "linear f \<Longrightarrow> f (x - y) = f x - f y"
1.162 -  using linear_add [of f x "- y"] by (simp add: linear_neg)
1.163 -
1.164 -lemma linear_sum:
1.165 -  assumes f: "linear f"
1.166 -  shows "f (sum g S) = sum (f \<circ> g) S"
1.167 -proof (cases "finite S")
1.168 -  case True
1.169 -  then show ?thesis
1.170 -    by induct (simp_all add: linear_0 [OF f] linear_add [OF f])
1.171 -next
1.172 -  case False
1.173 -  then show ?thesis
1.174 -    by (simp add: linear_0 [OF f])
1.175 -qed
1.176 -
1.177 -lemma linear_sum_mul:
1.178 -  assumes lin: "linear f"
1.179 -  shows "f (sum (\<lambda>i. c i *\<^sub>R v i) S) = sum (\<lambda>i. c i *\<^sub>R f (v i)) S"
1.180 -  using linear_sum[OF lin, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lin]
1.181 -  by simp
1.182 -
1.183 -lemma linear_injective_0:
1.184 -  assumes lin: "linear f"
1.185 -  shows "inj f \<longleftrightarrow> (\<forall>x. f x = 0 \<longrightarrow> x = 0)"
1.186 -proof -
1.187 -  have "inj f \<longleftrightarrow> (\<forall> x y. f x = f y \<longrightarrow> x = y)"
1.188 -    by (simp add: inj_on_def)
1.189 -  also have "\<dots> \<longleftrightarrow> (\<forall> x y. f x - f y = 0 \<longrightarrow> x - y = 0)"
1.190 -    by simp
1.191 -  also have "\<dots> \<longleftrightarrow> (\<forall> x y. f (x - y) = 0 \<longrightarrow> x - y = 0)"
1.192 -    by (simp add: linear_diff[OF lin])
1.193 -  also have "\<dots> \<longleftrightarrow> (\<forall> x. f x = 0 \<longrightarrow> x = 0)"
1.194 -    by auto
1.195 -  finally show ?thesis .
1.196 -qed
1.197 -
1.198 -lemma linear_scaleR  [simp]: "linear (\<lambda>x. scaleR c x)"
1.200 -
1.201 -lemma linear_scaleR_left [simp]: "linear (\<lambda>r. scaleR r x)"
1.203 -
1.204 -lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
1.205 -  by (simp add: inj_on_def)
1.206 -
1.208 -  assumes "linear f"
1.209 -  shows "f (a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x +  b *\<^sub>R f y"
1.210 -  using linear_add[of f] linear_cmul[of f] assms by simp
1.211 -
1.212 -subsection \<open>Subspaces of vector spaces\<close>
1.213 -
1.214 -definition%important (in real_vector) subspace :: "'a set \<Rightarrow> bool"
1.215 -  where "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)"
1.216 -
1.217 -definition%important (in real_vector) "span S = (subspace hull S)"
1.218 -definition%important (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
1.219 -abbreviation (in real_vector) "independent s \<equiv> \<not> dependent s"
1.220 -
1.221 -text \<open>Closure properties of subspaces.\<close>
1.222 -
1.223 -lemma subspace_UNIV[simp]: "subspace UNIV"
1.224 -  by (simp add: subspace_def)
1.225 -
1.226 -lemma (in real_vector) subspace_0: "subspace S \<Longrightarrow> 0 \<in> S"
1.227 -  by (metis subspace_def)
1.228 -
1.229 -lemma (in real_vector) subspace_add: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
1.230 -  by (metis subspace_def)
1.231 -
1.232 -lemma (in real_vector) subspace_mul: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> c *\<^sub>R x \<in> S"
1.233 -  by (metis subspace_def)
1.234 -
1.235 -lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> - x \<in> S"
1.236 -  by (metis scaleR_minus1_left subspace_mul)
1.237 -
1.238 -lemma subspace_diff: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
1.239 -  using subspace_add [of S x "- y"] by (simp add: subspace_neg)
1.240 -
1.241 -lemma (in real_vector) subspace_sum:
1.242 -  assumes sA: "subspace A"
1.243 -    and f: "\<And>x. x \<in> B \<Longrightarrow> f x \<in> A"
1.244 -  shows "sum f B \<in> A"
1.245 -proof (cases "finite B")
1.246 -  case True
1.247 -  then show ?thesis
1.248 -    using f by induct (simp_all add: subspace_0 [OF sA] subspace_add [OF sA])
1.249 -qed (simp add: subspace_0 [OF sA])
1.250 -
1.251 -lemma subspace_trivial [iff]: "subspace {0}"
1.252 -  by (simp add: subspace_def)
1.253 -
1.254 -lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<inter> B)"
1.255 -  by (simp add: subspace_def)
1.256 -
1.257 -lemma subspace_Times: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<times> B)"
1.258 -  unfolding subspace_def zero_prod_def by simp
1.259 -
1.260 -lemma subspace_sums: "\<lbrakk>subspace S; subspace T\<rbrakk> \<Longrightarrow> subspace {x + y|x y. x \<in> S \<and> y \<in> T}"
1.262 -apply (intro conjI impI allI)
1.263 -  using add.right_neutral apply blast
1.264 - apply clarify
1.267 -
1.268 -subsection%unimportant \<open>Properties of span\<close>
1.269 -
1.270 -lemma (in real_vector) span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
1.271 -  by (metis span_def hull_mono)
1.272 -
1.273 -lemma (in real_vector) subspace_span [iff]: "subspace (span S)"
1.274 -  unfolding span_def
1.275 -  apply (rule hull_in)
1.276 -  apply (simp only: subspace_def Inter_iff Int_iff subset_eq)
1.277 -  apply auto
1.278 -  done
1.279 -
1.280 -lemma (in real_vector) span_clauses:
1.281 -  "a \<in> S \<Longrightarrow> a \<in> span S"
1.282 -  "0 \<in> span S"
1.283 -  "x\<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
1.284 -  "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
1.285 -  by (metis span_def hull_subset subset_eq) (metis subspace_span subspace_def)+
1.286 -
1.287 -lemma span_unique:
1.288 -  "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> (\<And>T'. S \<subseteq> T' \<Longrightarrow> subspace T' \<Longrightarrow> T \<subseteq> T') \<Longrightarrow> span S = T"
1.289 -  unfolding span_def by (rule hull_unique)
1.290 -
1.291 -lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
1.292 -  unfolding span_def by (rule hull_minimal)
1.293 -
1.294 -lemma span_UNIV [simp]: "span UNIV = UNIV"
1.295 -  by (intro span_unique) auto
1.296 -
1.297 -lemma (in real_vector) span_induct:
1.298 -  assumes x: "x \<in> span S"
1.299 -    and P: "subspace (Collect P)"
1.300 -    and SP: "\<And>x. x \<in> S \<Longrightarrow> P x"
1.301 -  shows "P x"
1.302 -proof -
1.303 -  from SP have SP': "S \<subseteq> Collect P"
1.304 -    by (simp add: subset_eq)
1.305 -  from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
1.306 -  show ?thesis
1.307 -    using subset_eq by force
1.308 -qed
1.309 -
1.310 -lemma span_empty[simp]: "span {} = {0}"
1.311 -  apply (simp add: span_def)
1.312 -  apply (rule hull_unique)
1.313 -  apply (auto simp add: subspace_def)
1.314 -  done
1.315 -
1.316 -lemma (in real_vector) independent_empty [iff]: "independent {}"
1.317 -  by (simp add: dependent_def)
1.318 -
1.319 -lemma dependent_single[simp]: "dependent {x} \<longleftrightarrow> x = 0"
1.320 -  unfolding dependent_def by auto
1.321 -
1.322 -lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> independent B"
1.323 -  apply (clarsimp simp add: dependent_def span_mono)
1.324 -  apply (subgoal_tac "span (B - {a}) \<le> span (A - {a})")
1.325 -  apply force
1.326 -  apply (rule span_mono)
1.327 -  apply auto
1.328 -  done
1.329 -
1.330 -lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow>  subspace B \<Longrightarrow> span A = B"
1.331 -  by (metis order_antisym span_def hull_minimal)
1.332 -
1.333 -lemma (in real_vector) span_induct':
1.334 -  "\<forall>x \<in> S. P x \<Longrightarrow> subspace {x. P x} \<Longrightarrow> \<forall>x \<in> span S. P x"
1.335 -  unfolding span_def by (rule hull_induct) auto
1.336 -
1.337 -inductive_set (in real_vector) span_induct_alt_help for S :: "'a set"
1.338 -where
1.339 -  span_induct_alt_help_0: "0 \<in> span_induct_alt_help S"
1.340 -| span_induct_alt_help_S:
1.341 -    "x \<in> S \<Longrightarrow> z \<in> span_induct_alt_help S \<Longrightarrow>
1.342 -      (c *\<^sub>R x + z) \<in> span_induct_alt_help S"
1.343 -
1.344 -lemma span_induct_alt':
1.345 -  assumes h0: "h 0"
1.346 -    and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)"
1.347 -  shows "\<forall>x \<in> span S. h x"
1.348 -proof -
1.349 -  {
1.350 -    fix x :: 'a
1.351 -    assume x: "x \<in> span_induct_alt_help S"
1.352 -    have "h x"
1.353 -      apply (rule span_induct_alt_help.induct[OF x])
1.354 -      apply (rule h0)
1.355 -      apply (rule hS)
1.356 -      apply assumption
1.357 -      apply assumption
1.358 -      done
1.359 -  }
1.360 -  note th0 = this
1.361 -  {
1.362 -    fix x
1.363 -    assume x: "x \<in> span S"
1.364 -    have "x \<in> span_induct_alt_help S"
1.365 -    proof (rule span_induct[where x=x and S=S])
1.366 -      show "x \<in> span S" by (rule x)
1.367 -    next
1.368 -      fix x
1.369 -      assume xS: "x \<in> S"
1.370 -      from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1]
1.371 -      show "x \<in> span_induct_alt_help S"
1.372 -        by simp
1.373 -    next
1.374 -      have "0 \<in> span_induct_alt_help S" by (rule span_induct_alt_help_0)
1.375 -      moreover
1.376 -      {
1.377 -        fix x y
1.378 -        assume h: "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S"
1.379 -        from h have "(x + y) \<in> span_induct_alt_help S"
1.380 -          apply (induct rule: span_induct_alt_help.induct)
1.381 -          apply simp
1.383 -          apply (rule span_induct_alt_help_S)
1.384 -          apply assumption
1.385 -          apply simp
1.386 -          done
1.387 -      }
1.388 -      moreover
1.389 -      {
1.390 -        fix c x
1.391 -        assume xt: "x \<in> span_induct_alt_help S"
1.392 -        then have "(c *\<^sub>R x) \<in> span_induct_alt_help S"
1.393 -          apply (induct rule: span_induct_alt_help.induct)
1.394 -          apply (simp add: span_induct_alt_help_0)
1.395 -          apply (simp add: scaleR_right_distrib)
1.396 -          apply (rule span_induct_alt_help_S)
1.397 -          apply assumption
1.398 -          apply simp
1.399 -          done }
1.400 -      ultimately show "subspace {a. a \<in> span_induct_alt_help S}"
1.401 -        unfolding subspace_def Ball_def by blast
1.402 -    qed
1.403 -  }
1.404 -  with th0 show ?thesis by blast
1.405 -qed
1.406 -
1.407 -lemma span_induct_alt:
1.408 -  assumes h0: "h 0"
1.409 -    and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)"
1.410 -    and x: "x \<in> span S"
1.411 -  shows "h x"
1.412 -  using span_induct_alt'[of h S] h0 hS x by blast
1.413 -
1.414 -text \<open>Individual closure properties.\<close>
1.415 -
1.416 -lemma span_span: "span (span A) = span A"
1.417 -  unfolding span_def hull_hull ..
1.418 -
1.419 -lemma (in real_vector) span_superset: "x \<in> S \<Longrightarrow> x \<in> span S"
1.420 -  by (metis span_clauses(1))
1.421 -
1.422 -lemma (in real_vector) span_0 [simp]: "0 \<in> span S"
1.423 -  by (metis subspace_span subspace_0)
1.424 -
1.425 -lemma span_inc: "S \<subseteq> span S"
1.426 -  by (metis subset_eq span_superset)
1.427 -
1.428 -lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
1.429 -  using span_inc[unfolded subset_eq] using span_mono[of T "span S"] span_mono[of S "span T"]
1.430 -  by (auto simp add: span_span)
1.431 -
1.432 -lemma (in real_vector) dependent_0:
1.433 -  assumes "0 \<in> A"
1.434 -  shows "dependent A"
1.435 -  unfolding dependent_def
1.436 -  using assms span_0
1.437 -  by blast
1.438 -
1.439 -lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
1.440 -  by (metis subspace_add subspace_span)
1.441 -
1.442 -lemma (in real_vector) span_mul: "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
1.443 -  by (metis subspace_span subspace_mul)
1.444 -
1.445 -lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S"
1.446 -  by (metis subspace_neg subspace_span)
1.447 -
1.448 -lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
1.449 -  by (metis subspace_span subspace_diff)
1.450 -
1.451 -lemma (in real_vector) span_sum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> sum f A \<in> span S"
1.452 -  by (rule subspace_sum [OF subspace_span])
1.453 -
1.454 -lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
1.455 -  by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
1.456 -
1.457 -text \<open>The key breakdown property.\<close>
1.458 -
1.459 -lemma span_singleton: "span {x} = range (\<lambda>k. k *\<^sub>R x)"
1.460 -proof (rule span_unique)
1.461 -  show "{x} \<subseteq> range (\<lambda>k. k *\<^sub>R x)"
1.462 -    by (fast intro: scaleR_one [symmetric])
1.463 -  show "subspace (range (\<lambda>k. k *\<^sub>R x))"
1.464 -    unfolding subspace_def
1.465 -    by (auto intro: scaleR_add_left [symmetric])
1.466 -next
1.467 -  fix T
1.468 -  assume "{x} \<subseteq> T" and "subspace T"
1.469 -  then show "range (\<lambda>k. k *\<^sub>R x) \<subseteq> T"
1.470 -    unfolding subspace_def by auto
1.471 -qed
1.472 -
1.473 -text \<open>Mapping under linear image.\<close>
1.474 -
1.475 -lemma subspace_linear_image:
1.476 -  assumes lf: "linear f"
1.477 -    and sS: "subspace S"
1.478 -  shows "subspace (f ` S)"
1.479 -  using lf sS linear_0[OF lf]
1.480 -  unfolding linear_iff subspace_def
1.481 -  apply (auto simp add: image_iff)
1.482 -  apply (rule_tac x="x + y" in bexI)
1.483 -  apply auto
1.484 -  apply (rule_tac x="c *\<^sub>R x" in bexI)
1.485 -  apply auto
1.486 -  done
1.487 -
1.488 -lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f -` S)"
1.489 -  by (auto simp add: subspace_def linear_iff linear_0[of f])
1.490 -
1.491 -lemma subspace_linear_preimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace {x. f x \<in> S}"
1.492 -  by (auto simp add: subspace_def linear_iff linear_0[of f])
1.493 -
1.494 -lemma span_linear_image:
1.495 -  assumes lf: "linear f"
1.496 -  shows "span (f ` S) = f ` span S"
1.497 -proof (rule span_unique)
1.498 -  show "f ` S \<subseteq> f ` span S"
1.499 -    by (intro image_mono span_inc)
1.500 -  show "subspace (f ` span S)"
1.501 -    using lf subspace_span by (rule subspace_linear_image)
1.502 -next
1.503 -  fix T
1.504 -  assume "f ` S \<subseteq> T" and "subspace T"
1.505 -  then show "f ` span S \<subseteq> T"
1.506 -    unfolding image_subset_iff_subset_vimage
1.507 -    by (intro span_minimal subspace_linear_vimage lf)
1.508 -qed
1.509 -
1.510 -lemma spans_image:
1.511 -  assumes lf: "linear f"
1.512 -    and VB: "V \<subseteq> span B"
1.513 -  shows "f ` V \<subseteq> span (f ` B)"
1.514 -  unfolding span_linear_image[OF lf] by (metis VB image_mono)
1.515 -
1.516 -lemma span_Un: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
1.517 -proof (rule span_unique)
1.518 -  show "A \<union> B \<subseteq> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
1.519 -    by safe (force intro: span_clauses)+
1.520 -next
1.521 -  have "linear (\<lambda>(a, b). a + b)"
1.523 -  moreover have "subspace (span A \<times> span B)"
1.524 -    by (intro subspace_Times subspace_span)
1.525 -  ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
1.526 -    by (rule subspace_linear_image)
1.527 -next
1.528 -  fix T
1.529 -  assume "A \<union> B \<subseteq> T" and "subspace T"
1.530 -  then show "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T"
1.531 -    by (auto intro!: subspace_add elim: span_induct)
1.532 -qed
1.533 -
1.534 -lemma span_insert: "span (insert a S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
1.535 -proof -
1.536 -  have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
1.537 -    unfolding span_Un span_singleton
1.538 -    apply safe
1.539 -    apply (rule_tac x=k in exI, simp)
1.540 -    apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
1.541 -    apply auto
1.542 -    done
1.543 -  then show ?thesis by simp
1.544 -qed
1.545 -
1.546 -lemma span_breakdown:
1.547 -  assumes bS: "b \<in> S"
1.548 -    and aS: "a \<in> span S"
1.549 -  shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})"
1.550 -  using assms span_insert [of b "S - {b}"]
1.551 -  by (simp add: insert_absorb)
1.552 -
1.553 -lemma span_breakdown_eq: "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. x - k *\<^sub>R a \<in> span S)"
1.554 -  by (simp add: span_insert)
1.555 -
1.556 -text \<open>Hence some "reversal" results.\<close>
1.557 -
1.558 -lemma in_span_insert:
1.559 -  assumes a: "a \<in> span (insert b S)"
1.560 -    and na: "a \<notin> span S"
1.561 -  shows "b \<in> span (insert a S)"
1.562 -proof -
1.563 -  from a obtain k where k: "a - k *\<^sub>R b \<in> span S"
1.564 -    unfolding span_insert by fast
1.565 -  show ?thesis
1.566 -  proof (cases "k = 0")
1.567 -    case True
1.568 -    with k have "a \<in> span S" by simp
1.569 -    with na show ?thesis by simp
1.570 -  next
1.571 -    case False
1.572 -    from k have "(- inverse k) *\<^sub>R (a - k *\<^sub>R b) \<in> span S"
1.573 -      by (rule span_mul)
1.574 -    then have "b - inverse k *\<^sub>R a \<in> span S"
1.575 -      using \<open>k \<noteq> 0\<close> by (simp add: scaleR_diff_right)
1.576 -    then show ?thesis
1.577 -      unfolding span_insert by fast
1.578 -  qed
1.579 -qed
1.580 -
1.581 -lemma in_span_delete:
1.582 -  assumes a: "a \<in> span S"
1.583 -    and na: "a \<notin> span (S - {b})"
1.584 -  shows "b \<in> span (insert a (S - {b}))"
1.585 -  apply (rule in_span_insert)
1.586 -  apply (rule set_rev_mp)
1.587 -  apply (rule a)
1.588 -  apply (rule span_mono)
1.589 -  apply blast
1.590 -  apply (rule na)
1.591 -  done
1.592 -
1.593 -text \<open>Transitivity property.\<close>
1.594 -
1.595 -lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S"
1.596 -  unfolding span_def by (rule hull_redundant)
1.597 -
1.598 -lemma span_trans:
1.599 -  assumes x: "x \<in> span S"
1.600 -    and y: "y \<in> span (insert x S)"
1.601 -  shows "y \<in> span S"
1.602 -  using assms by (simp only: span_redundant)
1.603 -
1.604 -lemma span_insert_0[simp]: "span (insert 0 S) = span S"
1.605 -  by (simp only: span_redundant span_0)
1.606 -
1.607 -text \<open>An explicit expansion is sometimes needed.\<close>
1.608 -
1.609 -lemma span_explicit:
1.610 -  "span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
1.611 -  (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")
1.612 -proof -
1.613 -  {
1.614 -    fix x
1.615 -    assume "?h x"
1.616 -    then obtain S u where "finite S" and "S \<subseteq> P" and "sum (\<lambda>v. u v *\<^sub>R v) S = x"
1.617 -      by blast
1.618 -    then have "x \<in> span P"
1.619 -      by (auto intro: span_sum span_mul span_superset)
1.620 -  }
1.621 -  moreover
1.622 -  have "\<forall>x \<in> span P. ?h x"
1.623 -  proof (rule span_induct_alt')
1.624 -    show "?h 0"
1.625 -      by (rule exI[where x="{}"], simp)
1.626 -  next
1.627 -    fix c x y
1.628 -    assume x: "x \<in> P"
1.629 -    assume hy: "?h y"
1.630 -    from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
1.631 -      and u: "sum (\<lambda>v. u v *\<^sub>R v) S = y" by blast
1.632 -    let ?S = "insert x S"
1.633 -    let ?u = "\<lambda>y. if y = x then (if x \<in> S then u y + c else c) else u y"
1.634 -    from fS SP x have th0: "finite (insert x S)" "insert x S \<subseteq> P"
1.635 -      by blast+
1.636 -    have "?Q ?S ?u (c*\<^sub>R x + y)"
1.637 -    proof cases
1.638 -      assume xS: "x \<in> S"
1.639 -      have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = (\<Sum>v\<in>S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x"
1.640 -        using xS by (simp add: sum.remove [OF fS xS] insert_absorb)
1.641 -      also have "\<dots> = (\<Sum>v\<in>S. u v *\<^sub>R v) + c *\<^sub>R x"
1.642 -        by (simp add: sum.remove [OF fS xS] algebra_simps)
1.643 -      also have "\<dots> = c*\<^sub>R x + y"
1.645 -      finally have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" .
1.646 -      then show ?thesis using th0 by blast
1.647 -    next
1.648 -      assume xS: "x \<notin> S"
1.649 -      have th00: "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y"
1.650 -        unfolding u[symmetric]
1.651 -        apply (rule sum.cong)
1.652 -        using xS
1.653 -        apply auto
1.654 -        done
1.655 -      show ?thesis using fS xS th0
1.657 -    qed
1.658 -    then show "?h (c*\<^sub>R x + y)"
1.659 -      by fast
1.660 -  qed
1.661 -  ultimately show ?thesis by blast
1.662 -qed
1.663 -
1.664 -lemma dependent_explicit:
1.665 -  "dependent P \<longleftrightarrow> (\<exists>S u. finite S \<and> S \<subseteq> P \<and> (\<exists>v\<in>S. u v \<noteq> 0 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0))"
1.666 -  (is "?lhs = ?rhs")
1.667 -proof -
1.668 -  {
1.669 -    assume dP: "dependent P"
1.670 -    then obtain a S u where aP: "a \<in> P" and fS: "finite S"
1.671 -      and SP: "S \<subseteq> P - {a}" and ua: "sum (\<lambda>v. u v *\<^sub>R v) S = a"
1.672 -      unfolding dependent_def span_explicit by blast
1.673 -    let ?S = "insert a S"
1.674 -    let ?u = "\<lambda>y. if y = a then - 1 else u y"
1.675 -    let ?v = a
1.676 -    from aP SP have aS: "a \<notin> S"
1.677 -      by blast
1.678 -    from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0"
1.679 -      by auto
1.680 -    have s0: "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"
1.681 -      using fS aS
1.682 -      apply simp
1.683 -      apply (subst (2) ua[symmetric])
1.684 -      apply (rule sum.cong)
1.685 -      apply auto
1.686 -      done
1.687 -    with th0 have ?rhs by fast
1.688 -  }
1.689 -  moreover
1.690 -  {
1.691 -    fix S u v
1.692 -    assume fS: "finite S"
1.693 -      and SP: "S \<subseteq> P"
1.694 -      and vS: "v \<in> S"
1.695 -      and uv: "u v \<noteq> 0"
1.696 -      and u: "sum (\<lambda>v. u v *\<^sub>R v) S = 0"
1.697 -    let ?a = v
1.698 -    let ?S = "S - {v}"
1.699 -    let ?u = "\<lambda>i. (- u i) / u v"
1.700 -    have th0: "?a \<in> P" "finite ?S" "?S \<subseteq> P"
1.701 -      using fS SP vS by auto
1.702 -    have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S =
1.703 -      sum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
1.704 -      using fS vS uv by (simp add: sum_diff1 field_simps)
1.705 -    also have "\<dots> = ?a"
1.706 -      unfolding scaleR_right.sum [symmetric] u using uv by simp
1.707 -    finally have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
1.708 -    with th0 have ?lhs
1.709 -      unfolding dependent_def span_explicit
1.710 -      apply -
1.711 -      apply (rule bexI[where x= "?a"])
1.712 -      apply (simp_all del: scaleR_minus_left)
1.713 -      apply (rule exI[where x= "?S"])
1.714 -      apply (auto simp del: scaleR_minus_left)
1.715 -      done
1.716 -  }
1.717 -  ultimately show ?thesis by blast
1.718 -qed
1.719 -
1.720 -lemma dependent_finite:
1.721 -  assumes "finite S"
1.722 -    shows "dependent S \<longleftrightarrow> (\<exists>u. (\<exists>v \<in> S. u v \<noteq> 0) \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = 0)"
1.723 -           (is "?lhs = ?rhs")
1.724 -proof
1.725 -  assume ?lhs
1.726 -  then obtain T u v
1.727 -         where "finite T" "T \<subseteq> S" "v\<in>T" "u v \<noteq> 0" "(\<Sum>v\<in>T. u v *\<^sub>R v) = 0"
1.728 -    by (force simp: dependent_explicit)
1.729 -  with assms show ?rhs
1.730 -    apply (rule_tac x="\<lambda>v. if v \<in> T then u v else 0" in exI)
1.731 -    apply (auto simp: sum.mono_neutral_right)
1.732 -    done
1.733 -next
1.734 -  assume ?rhs  with assms show ?lhs
1.735 -    by (fastforce simp add: dependent_explicit)
1.736 -qed
1.737 -
1.738 -lemma span_alt:
1.739 -  "span B = {(\<Sum>x | f x \<noteq> 0. f x *\<^sub>R x) | f. {x. f x \<noteq> 0} \<subseteq> B \<and> finite {x. f x \<noteq> 0}}"
1.740 -  unfolding span_explicit
1.741 -  apply safe
1.742 -  subgoal for x S u
1.743 -    by (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
1.744 -        (auto intro!: sum.mono_neutral_cong_right)
1.745 -  apply auto
1.746 -  done
1.747 -
1.748 -lemma dependent_alt:
1.749 -  "dependent B \<longleftrightarrow>
1.750 -    (\<exists>X. finite {x. X x \<noteq> 0} \<and> {x. X x \<noteq> 0} \<subseteq> B \<and> (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x) = 0 \<and> (\<exists>x. X x \<noteq> 0))"
1.751 -  unfolding dependent_explicit
1.752 -  apply safe
1.753 -  subgoal for S u v
1.754 -    apply (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
1.755 -    apply (subst sum.mono_neutral_cong_left[where T=S])
1.756 -    apply (auto intro!: sum.mono_neutral_cong_right cong: rev_conj_cong)
1.757 -    done
1.758 -  apply auto
1.759 -  done
1.760 -
1.761 -lemma independent_alt:
1.762 -  "independent B \<longleftrightarrow>
1.763 -    (\<forall>X. finite {x. X x \<noteq> 0} \<longrightarrow> {x. X x \<noteq> 0} \<subseteq> B \<longrightarrow> (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x) = 0 \<longrightarrow> (\<forall>x. X x = 0))"
1.764 -  unfolding dependent_alt by auto
1.765 -
1.766 -lemma independentD_alt:
1.767 -  "independent B \<Longrightarrow> finite {x. X x \<noteq> 0} \<Longrightarrow> {x. X x \<noteq> 0} \<subseteq> B \<Longrightarrow> (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x) = 0 \<Longrightarrow> X x = 0"
1.768 -  unfolding independent_alt by blast
1.769 -
1.770 -lemma independentD_unique:
1.771 -  assumes B: "independent B"
1.772 -    and X: "finite {x. X x \<noteq> 0}" "{x. X x \<noteq> 0} \<subseteq> B"
1.773 -    and Y: "finite {x. Y x \<noteq> 0}" "{x. Y x \<noteq> 0} \<subseteq> B"
1.774 -    and "(\<Sum>x | X x \<noteq> 0. X x *\<^sub>R x) = (\<Sum>x| Y x \<noteq> 0. Y x *\<^sub>R x)"
1.775 -  shows "X = Y"
1.776 -proof -
1.777 -  have "X x - Y x = 0" for x
1.778 -    using B
1.779 -  proof (rule independentD_alt)
1.780 -    have "{x. X x - Y x \<noteq> 0} \<subseteq> {x. X x \<noteq> 0} \<union> {x. Y x \<noteq> 0}"
1.781 -      by auto
1.782 -    then show "finite {x. X x - Y x \<noteq> 0}" "{x. X x - Y x \<noteq> 0} \<subseteq> B"
1.783 -      using X Y by (auto dest: finite_subset)
1.784 -    then have "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *\<^sub>R x) = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. (X v - Y v) *\<^sub>R v)"
1.785 -      using X Y by (intro sum.mono_neutral_cong_left) auto
1.786 -    also have "\<dots> = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *\<^sub>R v) - (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *\<^sub>R v)"
1.787 -      by (simp add: scaleR_diff_left sum_subtractf assms)
1.788 -    also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *\<^sub>R v) = (\<Sum>v\<in>{S. X S \<noteq> 0}. X v *\<^sub>R v)"
1.789 -      using X Y by (intro sum.mono_neutral_cong_right) auto
1.790 -    also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *\<^sub>R v) = (\<Sum>v\<in>{S. Y S \<noteq> 0}. Y v *\<^sub>R v)"
1.791 -      using X Y by (intro sum.mono_neutral_cong_right) auto
1.792 -    finally show "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *\<^sub>R x) = 0"
1.793 -      using assms by simp
1.794 -  qed
1.795 -  then show ?thesis
1.796 -    by auto
1.797 -qed
1.798 -
1.799 -text \<open>This is useful for building a basis step-by-step.\<close>
1.800 -
1.801 -lemma independent_insert:
1.802 -  "independent (insert a S) \<longleftrightarrow>
1.803 -    (if a \<in> S then independent S else independent S \<and> a \<notin> span S)"
1.804 -  (is "?lhs \<longleftrightarrow> ?rhs")
1.805 -proof (cases "a \<in> S")
1.806 -  case True
1.807 -  then show ?thesis
1.808 -    using insert_absorb[OF True] by simp
1.809 -next
1.810 -  case False
1.811 -  show ?thesis
1.812 -  proof
1.813 -    assume i: ?lhs
1.814 -    then show ?rhs
1.815 -      using False
1.816 -      apply simp
1.817 -      apply (rule conjI)
1.818 -      apply (rule independent_mono)
1.819 -      apply assumption
1.820 -      apply blast
1.821 -      apply (simp add: dependent_def)
1.822 -      done
1.823 -  next
1.824 -    assume i: ?rhs
1.825 -    show ?lhs
1.826 -      using i False
1.827 -      apply (auto simp add: dependent_def)
1.828 -      by (metis in_span_insert insert_Diff_if insert_Diff_single insert_absorb)
1.829 -  qed
1.830 -qed
1.831 -
1.832 -lemma independent_Union_directed:
1.833 -  assumes directed: "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c"
1.834 -  assumes indep: "\<And>c. c \<in> C \<Longrightarrow> independent c"
1.835 -  shows "independent (\<Union>C)"
1.836 -proof
1.837 -  assume "dependent (\<Union>C)"
1.838 -  then obtain u v S where S: "finite S" "S \<subseteq> \<Union>C" "v \<in> S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0"
1.839 -    by (auto simp: dependent_explicit)
1.840 -
1.841 -  have "S \<noteq> {}"
1.842 -    using \<open>v \<in> S\<close> by auto
1.843 -  have "\<exists>c\<in>C. S \<subseteq> c"
1.844 -    using \<open>finite S\<close> \<open>S \<noteq> {}\<close> \<open>S \<subseteq> \<Union>C\<close>
1.845 -  proof (induction rule: finite_ne_induct)
1.846 -    case (insert i I)
1.847 -    then obtain c d where cd: "c \<in> C" "d \<in> C" and iI: "I \<subseteq> c" "i \<in> d"
1.848 -      by blast
1.849 -    from directed[OF cd] cd have "c \<union> d \<in> C"
1.850 -      by (auto simp: sup.absorb1 sup.absorb2)
1.851 -    with iI show ?case
1.852 -      by (intro bexI[of _ "c \<union> d"]) auto
1.853 -  qed auto
1.854 -  then obtain c where "c \<in> C" "S \<subseteq> c"
1.855 -    by auto
1.856 -  have "dependent c"
1.857 -    unfolding dependent_explicit
1.858 -    by (intro exI[of _ S] exI[of _ u] bexI[of _ v] conjI) fact+
1.859 -  with indep[OF \<open>c \<in> C\<close>] show False
1.860 -    by auto
1.861 -qed
1.862 -
1.863 -text \<open>Hence we can create a maximal independent subset.\<close>
1.864 -
1.865 -lemma maximal_independent_subset_extend:
1.866 -  assumes "S \<subseteq> V" "independent S"
1.867 -  shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
1.868 -proof -
1.869 -  let ?C = "{B. S \<subseteq> B \<and> independent B \<and> B \<subseteq> V}"
1.870 -  have "\<exists>M\<in>?C. \<forall>X\<in>?C. M \<subseteq> X \<longrightarrow> X = M"
1.871 -  proof (rule subset_Zorn)
1.872 -    fix C :: "'a set set" assume "subset.chain ?C C"
1.873 -    then have C: "\<And>c. c \<in> C \<Longrightarrow> c \<subseteq> V" "\<And>c. c \<in> C \<Longrightarrow> S \<subseteq> c" "\<And>c. c \<in> C \<Longrightarrow> independent c"
1.874 -      "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c"
1.875 -      unfolding subset.chain_def by blast+
1.876 -
1.877 -    show "\<exists>U\<in>?C. \<forall>X\<in>C. X \<subseteq> U"
1.878 -    proof cases
1.879 -      assume "C = {}" with assms show ?thesis
1.880 -        by (auto intro!: exI[of _ S])
1.881 -    next
1.882 -      assume "C \<noteq> {}"
1.883 -      with C(2) have "S \<subseteq> \<Union>C"
1.884 -        by auto
1.885 -      moreover have "independent (\<Union>C)"
1.886 -        by (intro independent_Union_directed C)
1.887 -      moreover have "\<Union>C \<subseteq> V"
1.888 -        using C by auto
1.889 -      ultimately show ?thesis
1.890 -        by auto
1.891 -    qed
1.892 -  qed
1.893 -  then obtain B where B: "independent B" "B \<subseteq> V" "S \<subseteq> B"
1.894 -    and max: "\<And>S. independent S \<Longrightarrow> S \<subseteq> V \<Longrightarrow> B \<subseteq> S \<Longrightarrow> S = B"
1.895 -    by auto
1.896 -  moreover
1.897 -  { assume "\<not> V \<subseteq> span B"
1.898 -    then obtain v where "v \<in> V" "v \<notin> span B"
1.899 -      by auto
1.900 -    with B have "independent (insert v B)"
1.901 -      unfolding independent_insert by auto
1.902 -    from max[OF this] \<open>v \<in> V\<close> \<open>B \<subseteq> V\<close>
1.903 -    have "v \<in> B"
1.904 -      by auto
1.905 -    with \<open>v \<notin> span B\<close> have False
1.906 -      by (auto intro: span_superset) }
1.907 -  ultimately show ?thesis
1.908 -    by (auto intro!: exI[of _ B])
1.909 -qed
1.910 -
1.911 -
1.912 -lemma maximal_independent_subset:
1.913 -  "\<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
1.914 -  by (metis maximal_independent_subset_extend[of "{}"] empty_subsetI independent_empty)
1.915 -
1.916 -lemma span_finite:
1.917 -  assumes fS: "finite S"
1.918 -  shows "span S = {y. \<exists>u. sum (\<lambda>v. u v *\<^sub>R v) S = y}"
1.919 -  (is "_ = ?rhs")
1.920 -proof -
1.921 -  {
1.922 -    fix y
1.923 -    assume y: "y \<in> span S"
1.924 -    from y obtain S' u where fS': "finite S'"
1.925 -      and SS': "S' \<subseteq> S"
1.926 -      and u: "sum (\<lambda>v. u v *\<^sub>R v) S' = y"
1.927 -      unfolding span_explicit by blast
1.928 -    let ?u = "\<lambda>x. if x \<in> S' then u x else 0"
1.929 -    have "sum (\<lambda>v. ?u v *\<^sub>R v) S = sum (\<lambda>v. u v *\<^sub>R v) S'"
1.930 -      using SS' fS by (auto intro!: sum.mono_neutral_cong_right)
1.931 -    then have "sum (\<lambda>v. ?u v *\<^sub>R v) S = y" by (metis u)
1.932 -    then have "y \<in> ?rhs" by auto
1.933 -  }
1.934 -  moreover
1.935 -  {
1.936 -    fix y u
1.937 -    assume u: "sum (\<lambda>v. u v *\<^sub>R v) S = y"
1.938 -    then have "y \<in> span S" using fS unfolding span_explicit by auto
1.939 -  }
1.940 -  ultimately show ?thesis by blast
1.941 -qed
1.942 -
1.943 -lemma linear_independent_extend_subspace:
1.944 -  assumes "independent B"
1.945 -  shows "\<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x) \<and> range g = span (f`B)"
1.946 -proof -
1.947 -  from maximal_independent_subset_extend[OF _ \<open>independent B\<close>, of UNIV]
1.948 -  obtain B' where "B \<subseteq> B'" "independent B'" "span B' = UNIV"
1.949 -    by (auto simp: top_unique)
1.950 -  have "\<forall>y. \<exists>X. {x. X x \<noteq> 0} \<subseteq> B' \<and> finite {x. X x \<noteq> 0} \<and> y = (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x)"
1.951 -    using \<open>span B' = UNIV\<close> unfolding span_alt by auto
1.952 -  then obtain X where X: "\<And>y. {x. X y x \<noteq> 0} \<subseteq> B'" "\<And>y. finite {x. X y x \<noteq> 0}"
1.953 -    "\<And>y. y = (\<Sum>x|X y x \<noteq> 0. X y x *\<^sub>R x)"
1.954 -    unfolding choice_iff by auto
1.955 -
1.956 -  have X_add: "X (x + y) = (\<lambda>z. X x z + X y z)" for x y
1.957 -    using \<open>independent B'\<close>
1.958 -  proof (rule independentD_unique)
1.959 -    have "(\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R z)
1.960 -      = (\<Sum>z\<in>{z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}. (X x z + X y z) *\<^sub>R z)"
1.961 -      by (intro sum.mono_neutral_cong_left) (auto intro: X)
1.962 -    also have "\<dots> = (\<Sum>z\<in>{z. X x z \<noteq> 0}. X x z *\<^sub>R z) + (\<Sum>z\<in>{z. X y z \<noteq> 0}. X y z *\<^sub>R z)"
1.964 -               intro!: arg_cong2[where f="(+)"]  sum.mono_neutral_cong_right X)
1.965 -    also have "\<dots> = x + y"
1.966 -      by (simp add: X(3)[symmetric])
1.967 -    also have "\<dots> = (\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z)"
1.968 -      by (rule X(3))
1.969 -    finally show "(\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z) = (\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R z)"
1.970 -      ..
1.971 -    have "{z. X x z + X y z \<noteq> 0} \<subseteq> {z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}"
1.972 -      by auto
1.973 -    then show "finite {z. X x z + X y z \<noteq> 0}" "{xa. X x xa + X y xa \<noteq> 0} \<subseteq> B'"
1.974 -        "finite {xa. X (x + y) xa \<noteq> 0}" "{xa. X (x + y) xa \<noteq> 0} \<subseteq> B'"
1.975 -      using X(1) by (auto dest: finite_subset intro: X)
1.976 -  qed
1.977 -
1.978 -  have X_cmult: "X (c *\<^sub>R x) = (\<lambda>z. c * X x z)" for x c
1.979 -    using \<open>independent B'\<close>
1.980 -  proof (rule independentD_unique)
1.981 -    show "finite {z. X (c *\<^sub>R x) z \<noteq> 0}" "{z. X (c *\<^sub>R x) z \<noteq> 0} \<subseteq> B'"
1.982 -      "finite {z. c * X x z \<noteq> 0}" "{z. c * X x z \<noteq> 0} \<subseteq> B' "
1.983 -      using X(1,2) by auto
1.984 -    show "(\<Sum>z | X (c *\<^sub>R x) z \<noteq> 0. X (c *\<^sub>R x) z *\<^sub>R z) = (\<Sum>z | c * X x z \<noteq> 0. (c * X x z) *\<^sub>R z)"
1.985 -      unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric]
1.986 -      by (cases "c = 0") (auto simp: X(3)[symmetric])
1.987 -  qed
1.988 -
1.989 -  have X_B': "x \<in> B' \<Longrightarrow> X x = (\<lambda>z. if z = x then 1 else 0)" for x
1.990 -    using \<open>independent B'\<close>
1.991 -    by (rule independentD_unique[OF _ X(2) X(1)]) (auto intro: X simp: X(3)[symmetric])
1.992 -
1.993 -  define f' where "f' y = (if y \<in> B then f y else 0)" for y
1.994 -  define g where "g y = (\<Sum>x|X y x \<noteq> 0. X y x *\<^sub>R f' x)" for y
1.995 -
1.996 -  have g_f': "x \<in> B' \<Longrightarrow> g x = f' x" for x
1.997 -    by (auto simp: g_def X_B')
1.998 -
1.999 -  have "linear g"
1.1000 -  proof
1.1001 -    fix x y
1.1002 -    have *: "(\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R f' z)
1.1003 -      = (\<Sum>z\<in>{z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}. (X x z + X y z) *\<^sub>R f' z)"
1.1004 -      by (intro sum.mono_neutral_cong_left) (auto intro: X)
1.1005 -    show "g (x + y) = g x + g y"
1.1006 -      unfolding g_def X_add *
1.1008 -               intro!: arg_cong2[where f="(+)"]  sum.mono_neutral_cong_right X)
1.1009 -  next
1.1010 -    show "g (r *\<^sub>R x) = r *\<^sub>R g x" for r x
1.1011 -      by (auto simp add: g_def X_cmult scaleR_sum_right intro!: sum.mono_neutral_cong_left X)
1.1012 -  qed
1.1013 -  moreover have "\<forall>x\<in>B. g x = f x"
1.1014 -    using \<open>B \<subseteq> B'\<close> by (auto simp: g_f' f'_def)
1.1015 -  moreover have "range g = span (f`B)"
1.1016 -    unfolding \<open>span B' = UNIV\<close>[symmetric] span_linear_image[OF \<open>linear g\<close>, symmetric]
1.1017 -  proof (rule span_subspace)
1.1018 -    have "g ` B' \<subseteq> f`B \<union> {0}"
1.1019 -      by (auto simp: g_f' f'_def)
1.1020 -    also have "\<dots> \<subseteq> span (f`B)"
1.1021 -      by (auto intro: span_superset span_0)
1.1022 -    finally show "g ` B' \<subseteq> span (f`B)"
1.1023 -      by auto
1.1024 -    have "x \<in> B \<Longrightarrow> f x = g x" for x
1.1025 -      using \<open>B \<subseteq> B'\<close> by (auto simp add: g_f' f'_def)
1.1026 -    then show "span (f ` B) \<subseteq> span (g ` B')"
1.1027 -      using \<open>B \<subseteq> B'\<close> by (intro span_mono) auto
1.1028 -  qed (rule subspace_span)
1.1029 -  ultimately show ?thesis
1.1030 -    by auto
1.1031 -qed
1.1032 -
1.1033 -lemma linear_independent_extend:
1.1034 -  "independent B \<Longrightarrow> \<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x)"
1.1035 -  using linear_independent_extend_subspace[of B f] by auto
1.1036 -
1.1037 -text \<open>Linear functions are equal on a subspace if they are on a spanning set.\<close>
1.1038 -
1.1039 -lemma subspace_kernel:
1.1040 -  assumes lf: "linear f"
1.1041 -  shows "subspace {x. f x = 0}"
1.1042 -  apply (simp add: subspace_def)
1.1044 -  done
1.1045 -
1.1046 -lemma linear_eq_0_span:
1.1047 -  assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
1.1048 -  shows "\<forall>x \<in> span B. f x = 0"
1.1049 -  using f0 subspace_kernel[OF lf]
1.1050 -  by (rule span_induct')
1.1051 -
1.1052 -lemma linear_eq_0: "linear f \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = 0 \<Longrightarrow> \<forall>x\<in>S. f x = 0"
1.1053 -  using linear_eq_0_span[of f B] by auto
1.1054 -
1.1055 -lemma linear_eq_span:  "linear f \<Longrightarrow> linear g \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x \<in> span B. f x = g x"
1.1056 -  using linear_eq_0_span[of "\<lambda>x. f x - g x" B] by (auto simp: linear_compose_sub)
1.1057 -
1.1058 -lemma linear_eq: "linear f \<Longrightarrow> linear g \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x\<in>S. f x = g x"
1.1059 -  using linear_eq_span[of f g B] by auto
1.1060 -
1.1061 -text \<open>The degenerate case of the Exchange Lemma.\<close>
1.1062 -
1.1063 -lemma spanning_subset_independent:
1.1064 -  assumes BA: "B \<subseteq> A"
1.1065 -    and iA: "independent A"
1.1066 -    and AsB: "A \<subseteq> span B"
1.1067 -  shows "A = B"
1.1068 -proof
1.1069 -  show "B \<subseteq> A" by (rule BA)
1.1070 -
1.1071 -  from span_mono[OF BA] span_mono[OF AsB]
1.1072 -  have sAB: "span A = span B" unfolding span_span by blast
1.1073 -
1.1074 -  {
1.1075 -    fix x
1.1076 -    assume x: "x \<in> A"
1.1077 -    from iA have th0: "x \<notin> span (A - {x})"
1.1078 -      unfolding dependent_def using x by blast
1.1079 -    from x have xsA: "x \<in> span A"
1.1080 -      by (blast intro: span_superset)
1.1081 -    have "A - {x} \<subseteq> A" by blast
1.1082 -    then have th1: "span (A - {x}) \<subseteq> span A"
1.1083 -      by (metis span_mono)
1.1084 -    {
1.1085 -      assume xB: "x \<notin> B"
1.1086 -      from xB BA have "B \<subseteq> A - {x}"
1.1087 -        by blast
1.1088 -      then have "span B \<subseteq> span (A - {x})"
1.1089 -        by (metis span_mono)
1.1090 -      with th1 th0 sAB have "x \<notin> span A"
1.1091 -        by blast
1.1092 -      with x have False
1.1093 -        by (metis span_superset)
1.1094 -    }
1.1095 -    then have "x \<in> B" by blast
1.1096 -  }
1.1097 -  then show "A \<subseteq> B" by blast
1.1098 -qed
1.1099 -
1.1100 -text \<open>Relation between bases and injectivity/surjectivity of map.\<close>
1.1101 -
1.1102 -lemma spanning_surjective_image:
1.1103 -  assumes us: "UNIV \<subseteq> span S"
1.1104 -    and lf: "linear f"
1.1105 -    and sf: "surj f"
1.1106 -  shows "UNIV \<subseteq> span (f ` S)"
1.1107 -proof -
1.1108 -  have "UNIV \<subseteq> f ` UNIV"
1.1109 -    using sf by (auto simp add: surj_def)
1.1110 -  also have " \<dots> \<subseteq> span (f ` S)"
1.1111 -    using spans_image[OF lf us] .
1.1112 -  finally show ?thesis .
1.1113 -qed
1.1114 -
1.1115 -lemma independent_inj_on_image:
1.1116 -  assumes iS: "independent S"
1.1117 -    and lf: "linear f"
1.1118 -    and fi: "inj_on f (span S)"
1.1119 -  shows "independent (f ` S)"
1.1120 -proof -
1.1121 -  {
1.1122 -    fix a
1.1123 -    assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
1.1124 -    have eq: "f ` S - {f a} = f ` (S - {a})"
1.1125 -      using fi \<open>a\<in>S\<close> by (auto simp add: inj_on_def span_superset)
1.1126 -    from a have "f a \<in> f ` span (S - {a})"
1.1127 -      unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
1.1128 -    then have "a \<in> span (S - {a})"
1.1129 -      by (rule inj_on_image_mem_iff_alt[OF fi, rotated])
1.1130 -         (insert span_mono[of "S - {a}" S], auto intro: span_superset \<open>a\<in>S\<close>)
1.1131 -    with a(1) iS have False
1.1132 -      by (simp add: dependent_def)
1.1133 -  }
1.1134 -  then show ?thesis
1.1135 -    unfolding dependent_def by blast
1.1136 -qed
1.1137 -
1.1138 -lemma independent_injective_image:
1.1139 -  "independent S \<Longrightarrow> linear f \<Longrightarrow> inj f \<Longrightarrow> independent (f ` S)"
1.1140 -  using independent_inj_on_image[of S f] by (auto simp: subset_inj_on)
1.1141 -
1.1142 -text \<open>Detailed theorems about left and right invertibility in general case.\<close>
1.1143 -
1.1144 -lemma linear_inj_on_left_inverse:
1.1145 -  assumes lf: "linear f" and fi: "inj_on f (span S)"
1.1146 -  shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span S. g (f x) = x)"
1.1147 -proof -
1.1148 -  obtain B where "independent B" "B \<subseteq> S" "S \<subseteq> span B"
1.1149 -    using maximal_independent_subset[of S] by auto
1.1150 -  then have "span S = span B"
1.1151 -    unfolding span_eq by (auto simp: span_superset)
1.1152 -  with linear_independent_extend_subspace[OF independent_inj_on_image, OF \<open>independent B\<close> lf] fi
1.1153 -  obtain g where g: "linear g" "\<forall>x\<in>f ` B. g x = inv_into B f x" "range g = span (inv_into B f ` f ` B)"
1.1154 -    by fastforce
1.1155 -  have fB: "inj_on f B"
1.1156 -    using fi by (auto simp: \<open>span S = span B\<close> intro: subset_inj_on span_superset)
1.1157 -
1.1158 -  have "\<forall>x\<in>span B. g (f x) = x"
1.1159 -  proof (intro linear_eq_span)
1.1160 -    show "linear (\<lambda>x. x)" "linear (\<lambda>x. g (f x))"
1.1161 -      using linear_id linear_compose[OF \<open>linear f\<close> \<open>linear g\<close>] by (auto simp: id_def comp_def)
1.1162 -    show "\<forall>x \<in> B. g (f x) = x"
1.1163 -      using g fi \<open>span S = span B\<close> by (auto simp: fB)
1.1164 -  qed
1.1165 -  moreover
1.1166 -  have "inv_into B f ` f ` B \<subseteq> B"
1.1167 -    by (auto simp: fB)
1.1168 -  then have "range g \<subseteq> span S"
1.1169 -    unfolding g \<open>span S = span B\<close> by (intro span_mono)
1.1170 -  ultimately show ?thesis
1.1171 -    using \<open>span S = span B\<close> \<open>linear g\<close> by auto
1.1172 -qed
1.1173 -
1.1174 -lemma linear_injective_left_inverse: "linear f \<Longrightarrow> inj f \<Longrightarrow> \<exists>g. linear g \<and> g \<circ> f = id"
1.1175 -  using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff span_UNIV)
1.1176 -
1.1177 -lemma linear_surj_right_inverse:
1.1178 -  assumes lf: "linear f" and sf: "span T \<subseteq> f`span S"
1.1179 -  shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span T. f (g x) = x)"
1.1180 -proof -
1.1181 -  obtain B where "independent B" "B \<subseteq> T" "T \<subseteq> span B"
1.1182 -    using maximal_independent_subset[of T] by auto
1.1183 -  then have "span T = span B"
1.1184 -    unfolding span_eq by (auto simp: span_superset)
1.1185 -
1.1186 -  from linear_independent_extend_subspace[OF \<open>independent B\<close>, of "inv_into (span S) f"]
1.1187 -  obtain g where g: "linear g" "\<forall>x\<in>B. g x = inv_into (span S) f x" "range g = span (inv_into (span S) f`B)"
1.1188 -    by auto
1.1189 -  moreover have "x \<in> B \<Longrightarrow> f (inv_into (span S) f x) = x" for x
1.1190 -    using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (intro f_inv_into_f) (auto intro: span_superset)
1.1191 -  ultimately have "\<forall>x\<in>B. f (g x) = x"
1.1192 -    by auto
1.1193 -  then have "\<forall>x\<in>span B. f (g x) = x"
1.1194 -    using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>]
1.1195 -    by (intro linear_eq_span) (auto simp: id_def comp_def)
1.1196 -  moreover have "inv_into (span S) f ` B \<subseteq> span S"
1.1197 -    using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (auto intro: inv_into_into span_superset)
1.1198 -  then have "range g \<subseteq> span S"
1.1199 -    unfolding g by (intro span_minimal subspace_span) auto
1.1200 -  ultimately show ?thesis
1.1201 -    using \<open>linear g\<close> \<open>span T = span B\<close> by auto
1.1202 -qed
1.1203 -
1.1204 -lemma linear_surjective_right_inverse: "linear f \<Longrightarrow> surj f \<Longrightarrow> \<exists>g. linear g \<and> f \<circ> g = id"
1.1205 -  using linear_surj_right_inverse[of f UNIV UNIV]
1.1206 -  by (auto simp: span_UNIV fun_eq_iff)
1.1207 -
1.1208 -text \<open>The general case of the Exchange Lemma, the key to what follows.\<close>
1.1209 -
1.1210 -lemma exchange_lemma:
1.1211 -  assumes f:"finite t"
1.1212 -    and i: "independent s"
1.1213 -    and sp: "s \<subseteq> span t"
1.1214 -  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'"
1.1215 -  using f i sp
1.1216 -proof (induct "card (t - s)" arbitrary: s t rule: less_induct)
1.1217 -  case less
1.1218 -  note ft = \<open>finite t\<close> and s = \<open>independent s\<close> and sp = \<open>s \<subseteq> span t\<close>
1.1219 -  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'"
1.1220 -  let ?ths = "\<exists>t'. ?P t'"
1.1221 -  {
1.1222 -    assume "s \<subseteq> t"
1.1223 -    then have ?ths
1.1224 -      by (metis ft Un_commute sp sup_ge1)
1.1225 -  }
1.1226 -  moreover
1.1227 -  {
1.1228 -    assume st: "t \<subseteq> s"
1.1229 -    from spanning_subset_independent[OF st s sp] st ft span_mono[OF st]
1.1230 -    have ?ths
1.1231 -      by (metis Un_absorb sp)
1.1232 -  }
1.1233 -  moreover
1.1234 -  {
1.1235 -    assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
1.1236 -    from st(2) obtain b where b: "b \<in> t" "b \<notin> s"
1.1237 -      by blast
1.1238 -    from b have "t - {b} - s \<subset> t - s"
1.1239 -      by blast
1.1240 -    then have cardlt: "card (t - {b} - s) < card (t - s)"
1.1241 -      using ft by (auto intro: psubset_card_mono)
1.1242 -    from b ft have ct0: "card t \<noteq> 0"
1.1243 -      by auto
1.1244 -    have ?ths
1.1245 -    proof cases
1.1246 -      assume stb: "s \<subseteq> span (t - {b})"
1.1247 -      from ft have ftb: "finite (t - {b})"
1.1248 -        by auto
1.1249 -      from less(1)[OF cardlt ftb s stb]
1.1250 -      obtain u where u: "card u = card (t - {b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u"
1.1251 -        and fu: "finite u" by blast
1.1252 -      let ?w = "insert b u"
1.1253 -      have th0: "s \<subseteq> insert b u"
1.1254 -        using u by blast
1.1255 -      from u(3) b have "u \<subseteq> s \<union> t"
1.1256 -        by blast
1.1257 -      then have th1: "insert b u \<subseteq> s \<union> t"
1.1258 -        using u b by blast
1.1259 -      have bu: "b \<notin> u"
1.1260 -        using b u by blast
1.1261 -      from u(1) ft b have "card u = (card t - 1)"
1.1262 -        by auto
1.1263 -      then have th2: "card (insert b u) = card t"
1.1264 -        using card_insert_disjoint[OF fu bu] ct0 by auto
1.1265 -      from u(4) have "s \<subseteq> span u" .
1.1266 -      also have "\<dots> \<subseteq> span (insert b u)"
1.1267 -        by (rule span_mono) blast
1.1268 -      finally have th3: "s \<subseteq> span (insert b u)" .
1.1269 -      from th0 th1 th2 th3 fu have th: "?P ?w"
1.1270 -        by blast
1.1271 -      from th show ?thesis by blast
1.1272 -    next
1.1273 -      assume stb: "\<not> s \<subseteq> span (t - {b})"
1.1274 -      from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})"
1.1275 -        by blast
1.1276 -      have ab: "a \<noteq> b"
1.1277 -        using a b by blast
1.1278 -      have at: "a \<notin> t"
1.1279 -        using a ab span_superset[of a "t- {b}"] by auto
1.1280 -      have mlt: "card ((insert a (t - {b})) - s) < card (t - s)"
1.1281 -        using cardlt ft a b by auto
1.1282 -      have ft': "finite (insert a (t - {b}))"
1.1283 -        using ft by auto
1.1284 -      {
1.1285 -        fix x
1.1286 -        assume xs: "x \<in> s"
1.1287 -        have t: "t \<subseteq> insert b (insert a (t - {b}))"
1.1288 -          using b by auto
1.1289 -        from b(1) have "b \<in> span t"
1.1290 -          by (simp add: span_superset)
1.1291 -        have bs: "b \<in> span (insert a (t - {b}))"
1.1292 -          apply (rule in_span_delete)
1.1293 -          using a sp unfolding subset_eq
1.1294 -          apply auto
1.1295 -          done
1.1296 -        from xs sp have "x \<in> span t"
1.1297 -          by blast
1.1298 -        with span_mono[OF t] have x: "x \<in> span (insert b (insert a (t - {b})))" ..
1.1299 -        from span_trans[OF bs x] have "x \<in> span (insert a (t - {b}))" .
1.1300 -      }
1.1301 -      then have sp': "s \<subseteq> span (insert a (t - {b}))"
1.1302 -        by blast
1.1303 -      from less(1)[OF mlt ft' s sp'] obtain u where u:
1.1304 -        "card u = card (insert a (t - {b}))"
1.1305 -        "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t - {b})"
1.1306 -        "s \<subseteq> span u" by blast
1.1307 -      from u a b ft at ct0 have "?P u"
1.1308 -        by auto
1.1309 -      then show ?thesis by blast
1.1310 -    qed
1.1311 -  }
1.1312 -  ultimately show ?ths by blast
1.1313 -qed
1.1314 -
1.1315 -text \<open>This implies corresponding size bounds.\<close>
1.1316 -
1.1317 -lemma independent_span_bound:
1.1318 -  assumes f: "finite t"
1.1319 -    and i: "independent s"
1.1320 -    and sp: "s \<subseteq> span t"
1.1321 -  shows "finite s \<and> card s \<le> card t"
1.1322 -  by (metis exchange_lemma[OF f i sp] finite_subset card_mono)
1.1323 -
1.1324  lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
1.1325  proof -
1.1326    have eq: "{f x |x. x\<in> UNIV} = f ` UNIV"
1.1327 @@ -1353,51 +47,8 @@
1.1328
1.1329  subsection%unimportant \<open>More interesting properties of the norm.\<close>
1.1330
1.1331 -lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
1.1332 -  by auto
1.1333 -
1.1334  notation inner (infix "\<bullet>" 70)
1.1335
1.1336 -lemma square_bound_lemma:
1.1337 -  fixes x :: real
1.1338 -  shows "x < (1 + x) * (1 + x)"
1.1339 -proof -
1.1340 -  have "(x + 1/2)\<^sup>2 + 3/4 > 0"
1.1341 -    using zero_le_power2[of "x+1/2"] by arith
1.1342 -  then show ?thesis
1.1343 -    by (simp add: field_simps power2_eq_square)
1.1344 -qed
1.1345 -
1.1346 -lemma square_continuous:
1.1347 -  fixes e :: real
1.1348 -  shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)"
1.1349 -  using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
1.1350 -  by (force simp add: power2_eq_square)
1.1351 -
1.1352 -
1.1353 -lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
1.1354 -  by simp (* TODO: delete *)
1.1355 -
1.1356 -lemma norm_triangle_sub:
1.1357 -  fixes x y :: "'a::real_normed_vector"
1.1358 -  shows "norm x \<le> norm y + norm (x - y)"
1.1359 -  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
1.1360 -
1.1361 -lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> x \<bullet> x \<le> y \<bullet> y"
1.1362 -  by (simp add: norm_eq_sqrt_inner)
1.1363 -
1.1364 -lemma norm_lt: "norm x < norm y \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
1.1365 -  by (simp add: norm_eq_sqrt_inner)
1.1366 -
1.1367 -lemma norm_eq: "norm x = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
1.1368 -  apply (subst order_eq_iff)
1.1369 -  apply (auto simp: norm_le)
1.1370 -  done
1.1371 -
1.1372 -lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> x \<bullet> x = 1"
1.1373 -  by (simp add: norm_eq_sqrt_inner)
1.1374 -
1.1375 -
1.1376  text\<open>Equality of vectors in terms of @{term "(\<bullet>)"} products.\<close>
1.1377
1.1378  lemma linear_componentwise:
1.1379 @@ -1405,11 +56,11 @@
1.1380    assumes lf: "linear f"
1.1381    shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
1.1382  proof -
1.1383 +  interpret linear f by fact
1.1384    have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
1.1386    then show ?thesis
1.1387 -    unfolding linear_sum_mul[OF lf, symmetric]
1.1388 -    unfolding euclidean_representation ..
1.1389 +    by (simp add: euclidean_representation sum[symmetric] scale[symmetric])
1.1390  qed
1.1391
1.1392  lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x"
1.1393 @@ -1607,22 +258,15 @@
1.1394    using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)
1.1395
1.1396  lemma bilinear_sum:
1.1397 -  assumes bh: "bilinear h"
1.1398 -    and fS: "finite S"
1.1399 -    and fT: "finite T"
1.1400 +  assumes "bilinear h"
1.1401    shows "h (sum f S) (sum g T) = sum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
1.1402  proof -
1.1403 +  interpret l: linear "\<lambda>x. h x y" for y using assms by (simp add: bilinear_def)
1.1404 +  interpret r: linear "\<lambda>y. h x y" for x using assms by (simp add: bilinear_def)
1.1405    have "h (sum f S) (sum g T) = sum (\<lambda>x. h (f x) (sum g T)) S"
1.1406 -    apply (rule linear_sum[unfolded o_def])
1.1407 -    using bh fS
1.1408 -    apply (auto simp add: bilinear_def)
1.1409 -    done
1.1410 +    by (simp add: l.sum)
1.1411    also have "\<dots> = sum (\<lambda>x. sum (\<lambda>y. h (f x) (g y)) T) S"
1.1412 -    apply (rule sum.cong, simp)
1.1413 -    apply (rule linear_sum[unfolded o_def])
1.1414 -    using bh fT
1.1415 -    apply (auto simp add: bilinear_def)
1.1416 -    done
1.1417 +    by (rule sum.cong) (simp_all add: r.sum)
1.1418    finally show ?thesis
1.1419      unfolding sum.cartesian_product .
1.1420  qed
1.1421 @@ -1663,6 +307,7 @@
1.1422    assumes lf: "linear f"
1.1423    shows "x \<bullet> adjoint f y = f x \<bullet> y"
1.1424  proof -
1.1425 +  interpret linear f by fact
1.1426    have "\<forall>y. \<exists>w. \<forall>x. f x \<bullet> y = x \<bullet> w"
1.1427    proof (intro allI exI)
1.1428      fix y :: "'m" and x
1.1429 @@ -1670,8 +315,7 @@
1.1430      have "f x \<bullet> y = f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i) \<bullet> y"
1.1432      also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<bullet> y"
1.1433 -      unfolding linear_sum[OF lf]
1.1434 -      by (simp add: linear_cmul[OF lf])
1.1435 +      by (simp add: sum scale)
1.1436      finally show "f x \<bullet> y = x \<bullet> ?w"
1.1437        by (simp add: inner_sum_left inner_sum_right mult.commute)
1.1438    qed
1.1439 @@ -1847,63 +491,14 @@
1.1440  subsection%unimportant \<open>Euclidean Spaces as Typeclass\<close>
1.1441
1.1442  lemma independent_Basis: "independent Basis"
1.1443 -  unfolding dependent_def
1.1444 -  apply (subst span_finite)
1.1445 -  apply simp
1.1446 -  apply clarify
1.1447 -  apply (drule_tac f="inner a" in arg_cong)
1.1448 -  apply (simp add: inner_Basis inner_sum_right eq_commute)
1.1449 -  done
1.1450 +  by (rule independent_Basis)
1.1451
1.1452  lemma span_Basis [simp]: "span Basis = UNIV"
1.1453 -  unfolding span_finite [OF finite_Basis]
1.1454 -  by (fast intro: euclidean_representation)
1.1455 +  by (rule span_Basis)
1.1456
1.1457  lemma in_span_Basis: "x \<in> span Basis"
1.1458    unfolding span_Basis ..
1.1459
1.1460 -lemma Basis_le_norm: "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> norm x"
1.1461 -  by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
1.1462 -
1.1463 -lemma norm_bound_Basis_le: "b \<in> Basis \<Longrightarrow> norm x \<le> e \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> e"
1.1464 -  by (metis Basis_le_norm order_trans)
1.1465 -
1.1466 -lemma norm_bound_Basis_lt: "b \<in> Basis \<Longrightarrow> norm x < e \<Longrightarrow> \<bar>x \<bullet> b\<bar> < e"
1.1467 -  by (metis Basis_le_norm le_less_trans)
1.1468 -
1.1469 -lemma norm_le_l1: "norm x \<le> (\<Sum>b\<in>Basis. \<bar>x \<bullet> b\<bar>)"
1.1470 -  apply (subst euclidean_representation[of x, symmetric])
1.1471 -  apply (rule order_trans[OF norm_sum])
1.1472 -  apply (auto intro!: sum_mono)
1.1473 -  done
1.1474 -
1.1475 -lemma sum_norm_allsubsets_bound:
1.1476 -  fixes f :: "'a \<Rightarrow> 'n::euclidean_space"
1.1477 -  assumes fP: "finite P"
1.1478 -    and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (sum f Q) \<le> e"
1.1479 -  shows "(\<Sum>x\<in>P. norm (f x)) \<le> 2 * real DIM('n) * e"
1.1480 -proof -
1.1481 -  have "(\<Sum>x\<in>P. norm (f x)) \<le> (\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>)"
1.1482 -    by (rule sum_mono) (rule norm_le_l1)
1.1483 -  also have "(\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>) = (\<Sum>b\<in>Basis. \<Sum>x\<in>P. \<bar>f x \<bullet> b\<bar>)"
1.1484 -    by (rule sum.swap)
1.1485 -  also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
1.1486 -  proof (rule sum_bounded_above)
1.1487 -    fix i :: 'n
1.1488 -    assume i: "i \<in> Basis"
1.1489 -    have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
1.1490 -      norm ((\<Sum>x\<in>P \<inter> - {x. f x \<bullet> i < 0}. f x) \<bullet> i) + norm ((\<Sum>x\<in>P \<inter> {x. f x \<bullet> i < 0}. f x) \<bullet> i)"
1.1491 -      by (simp add: abs_real_def sum.If_cases[OF fP] sum_negf norm_triangle_ineq4 inner_sum_left
1.1492 -        del: real_norm_def)
1.1493 -    also have "\<dots> \<le> e + e"
1.1494 -      unfolding real_norm_def
1.1495 -      by (intro add_mono norm_bound_Basis_le i fPs) auto
1.1496 -    finally show "(\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le> 2*e" by simp
1.1497 -  qed
1.1498 -  also have "\<dots> = 2 * real DIM('n) * e" by simp
1.1499 -  finally show ?thesis .
1.1500 -qed
1.1501 -
1.1502
1.1503  subsection%unimportant \<open>Linearity and Bilinearity continued\<close>
1.1504
1.1505 @@ -1912,6 +507,7 @@
1.1506    assumes lf: "linear f"
1.1507    shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
1.1508  proof
1.1509 +  interpret linear f by fact
1.1510    let ?B = "\<Sum>b\<in>Basis. norm (f b)"
1.1511    show "\<forall>x. norm (f x) \<le> ?B * norm x"
1.1512    proof
1.1513 @@ -1920,7 +516,7 @@
1.1514      have "norm (f x) = norm (f (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b))"
1.1515        unfolding euclidean_representation ..
1.1516      also have "\<dots> = norm (sum ?g Basis)"
1.1517 -      by (simp add: linear_sum [OF lf] linear_cmul [OF lf])
1.1518 +      by (simp add: sum scale)
1.1519      finally have th0: "norm (f x) = norm (sum ?g Basis)" .
1.1520      have th: "norm (?g i) \<le> norm (f i) * norm x" if "i \<in> Basis" for i
1.1521      proof -
1.1522 @@ -1997,15 +593,15 @@
1.1523    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
1.1524    assumes "linear f" "inj f"
1.1525    obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
1.1526 -  using linear_injective_left_inverse [OF assms] linear_invertible_bounded_below_pos assms by blast
1.1527 +  using linear_injective_left_inverse [OF assms]
1.1528 +    linear_invertible_bounded_below_pos assms by blast
1.1529
1.1530  lemma bounded_linearI':
1.1531    fixes f ::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1.1532    assumes "\<And>x y. f (x + y) = f x + f y"
1.1533      and "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
1.1534    shows "bounded_linear f"
1.1535 -  unfolding linear_conv_bounded_linear[symmetric]
1.1536 -  by (rule linearI[OF assms])
1.1537 +  using assms linearI linear_conv_bounded_linear by blast
1.1538
1.1539  lemma bilinear_bounded:
1.1540    fixes h :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
1.1541 @@ -2020,7 +616,7 @@
1.1542      apply rule
1.1543      done
1.1544    also have "\<dots> = norm (sum (\<lambda> (i,j). h ((x \<bullet> i) *\<^sub>R i) ((y \<bullet> j) *\<^sub>R j)) (Basis \<times> Basis))"
1.1545 -    unfolding bilinear_sum[OF bh finite_Basis finite_Basis] ..
1.1546 +    unfolding bilinear_sum[OF bh] ..
1.1547    finally have th: "norm (h x y) = \<dots>" .
1.1548    show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
1.1549      apply (auto simp add: sum_distrib_right th sum.cartesian_product)
1.1550 @@ -2084,14 +680,14 @@
1.1551      by (simp only: ac_simps)
1.1552  qed
1.1553
1.1554 -lemma bounded_linear_imp_has_derivative:
1.1555 -     "bounded_linear f \<Longrightarrow> (f has_derivative f) net"
1.1556 -  by (simp add: has_derivative_def bounded_linear.linear linear_diff)
1.1557 +lemma bounded_linear_imp_has_derivative: "bounded_linear f \<Longrightarrow> (f has_derivative f) net"
1.1558 +  by (auto simp add: has_derivative_def linear_diff linear_linear linear_def
1.1559 +      dest: bounded_linear.linear)
1.1560
1.1561  lemma linear_imp_has_derivative:
1.1562    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1.1563    shows "linear f \<Longrightarrow> (f has_derivative f) net"
1.1564 -by (simp add: has_derivative_def linear_conv_bounded_linear linear_diff)
1.1565 +  by (simp add: bounded_linear_imp_has_derivative linear_conv_bounded_linear)
1.1566
1.1567  lemma bounded_linear_imp_differentiable: "bounded_linear f \<Longrightarrow> f differentiable net"
1.1568    using bounded_linear_imp_has_derivative differentiable_def by blast
1.1569 @@ -2099,7 +695,7 @@
1.1570  lemma linear_imp_differentiable:
1.1571    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1.1572    shows "linear f \<Longrightarrow> f differentiable net"
1.1573 -by (metis linear_imp_has_derivative differentiable_def)
1.1574 +  by (metis linear_imp_has_derivative differentiable_def)
1.1575
1.1576
1.1577  subsection%unimportant \<open>We continue.\<close>
1.1578 @@ -2107,221 +703,21 @@
1.1579  lemma independent_bound:
1.1580    fixes S :: "'a::euclidean_space set"
1.1581    shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a)"
1.1582 -  using independent_span_bound[OF finite_Basis, of S] by auto
1.1583 +  by (metis dim_subset_UNIV finiteI_independent dim_span_eq_card_independent)
1.1584 +
1.1585 +lemmas independent_imp_finite = finiteI_independent
1.1586
1.1587  corollary
1.1588    fixes S :: "'a::euclidean_space set"
1.1589    assumes "independent S"
1.1590 -  shows independent_imp_finite: "finite S" and independent_card_le:"card S \<le> DIM('a)"
1.1591 -using assms independent_bound by auto
1.1592 -
1.1593 -lemma independent_explicit:
1.1594 -  fixes B :: "'a::euclidean_space set"
1.1595 -  shows "independent B \<longleftrightarrow>
1.1596 -         finite B \<and> (\<forall>c. (\<Sum>v\<in>B. c v *\<^sub>R v) = 0 \<longrightarrow> (\<forall>v \<in> B. c v = 0))"
1.1597 -apply (cases "finite B")
1.1598 - apply (force simp: dependent_finite)
1.1599 -using independent_bound
1.1600 -apply auto
1.1601 -done
1.1602 +  shows independent_card_le:"card S \<le> DIM('a)"
1.1603 +  using assms independent_bound by auto
1.1604
1.1605  lemma dependent_biggerset:
1.1606    fixes S :: "'a::euclidean_space set"
1.1607    shows "(finite S \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
1.1608    by (metis independent_bound not_less)
1.1609
1.1610 -text \<open>Notion of dimension.\<close>
1.1611 -
1.1612 -definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> card B = n)"
1.1613 -
1.1614 -lemma basis_exists:
1.1615 -  "\<exists>B. (B :: ('a::euclidean_space) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = dim V)"
1.1616 -  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)"]
1.1617 -  using maximal_independent_subset[of V] independent_bound
1.1618 -  by auto
1.1619 -
1.1620 -corollary dim_le_card:
1.1621 -  fixes s :: "'a::euclidean_space set"
1.1622 -  shows "finite s \<Longrightarrow> dim s \<le> card s"
1.1623 -by (metis basis_exists card_mono)
1.1624 -
1.1625 -text \<open>Consequences of independence or spanning for cardinality.\<close>
1.1626 -
1.1627 -lemma independent_card_le_dim:
1.1628 -  fixes B :: "'a::euclidean_space set"
1.1629 -  assumes "B \<subseteq> V"
1.1630 -    and "independent B"
1.1631 -  shows "card B \<le> dim V"
1.1632 -proof -
1.1633 -  from basis_exists[of V] \<open>B \<subseteq> V\<close>
1.1634 -  obtain B' where "independent B'"
1.1635 -    and "B \<subseteq> span B'"
1.1636 -    and "card B' = dim V"
1.1637 -    by blast
1.1638 -  with independent_span_bound[OF _ \<open>independent B\<close> \<open>B \<subseteq> span B'\<close>] independent_bound[of B']
1.1639 -  show ?thesis by auto
1.1640 -qed
1.1641 -
1.1642 -lemma span_card_ge_dim:
1.1643 -  fixes B :: "'a::euclidean_space set"
1.1644 -  shows "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> finite B \<Longrightarrow> dim V \<le> card B"
1.1645 -  by (metis basis_exists[of V] independent_span_bound subset_trans)
1.1646 -
1.1647 -lemma basis_card_eq_dim:
1.1648 -  fixes V :: "'a::euclidean_space set"
1.1649 -  shows "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B = dim V"
1.1650 -  by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_bound)
1.1651 -
1.1652 -lemma dim_unique:
1.1653 -  fixes B :: "'a::euclidean_space set"
1.1654 -  shows "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = n \<Longrightarrow> dim V = n"
1.1655 -  by (metis basis_card_eq_dim)
1.1656 -
1.1657 -text \<open>More lemmas about dimension.\<close>
1.1658 -
1.1659 -lemma dim_UNIV [simp]: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
1.1660 -  using independent_Basis
1.1661 -  by (intro dim_unique[of Basis]) auto
1.1662 -
1.1663 -lemma dim_subset:
1.1664 -  fixes S :: "'a::euclidean_space set"
1.1665 -  shows "S \<subseteq> T \<Longrightarrow> dim S \<le> dim T"
1.1666 -  using basis_exists[of T] basis_exists[of S]
1.1667 -  by (metis independent_card_le_dim subset_trans)
1.1668 -
1.1669 -lemma dim_subset_UNIV:
1.1670 -  fixes S :: "'a::euclidean_space set"
1.1671 -  shows "dim S \<le> DIM('a)"
1.1672 -  by (metis dim_subset subset_UNIV dim_UNIV)
1.1673 -
1.1674 -text \<open>Converses to those.\<close>
1.1675 -
1.1676 -lemma card_ge_dim_independent:
1.1677 -  fixes B :: "'a::euclidean_space set"
1.1678 -  assumes BV: "B \<subseteq> V"
1.1679 -    and iB: "independent B"
1.1680 -    and dVB: "dim V \<le> card B"
1.1681 -  shows "V \<subseteq> span B"
1.1682 -proof
1.1683 -  fix a
1.1684 -  assume aV: "a \<in> V"
1.1685 -  {
1.1686 -    assume aB: "a \<notin> span B"
1.1687 -    then have iaB: "independent (insert a B)"
1.1688 -      using iB aV BV by (simp add: independent_insert)
1.1689 -    from aV BV have th0: "insert a B \<subseteq> V"
1.1690 -      by blast
1.1691 -    from aB have "a \<notin>B"
1.1692 -      by (auto simp add: span_superset)
1.1693 -    with independent_card_le_dim[OF th0 iaB] dVB independent_bound[OF iB]
1.1694 -    have False by auto
1.1695 -  }
1.1696 -  then show "a \<in> span B" by blast
1.1697 -qed
1.1698 -
1.1699 -lemma card_le_dim_spanning:
1.1700 -  assumes BV: "(B:: ('a::euclidean_space) set) \<subseteq> V"
1.1701 -    and VB: "V \<subseteq> span B"
1.1702 -    and fB: "finite B"
1.1703 -    and dVB: "dim V \<ge> card B"
1.1704 -  shows "independent B"
1.1705 -proof -
1.1706 -  {
1.1707 -    fix a
1.1708 -    assume a: "a \<in> B" "a \<in> span (B - {a})"
1.1709 -    from a fB have c0: "card B \<noteq> 0"
1.1710 -      by auto
1.1711 -    from a fB have cb: "card (B - {a}) = card B - 1"
1.1712 -      by auto
1.1713 -    from BV a have th0: "B - {a} \<subseteq> V"
1.1714 -      by blast
1.1715 -    {
1.1716 -      fix x
1.1717 -      assume x: "x \<in> V"
1.1718 -      from a have eq: "insert a (B - {a}) = B"
1.1719 -        by blast
1.1720 -      from x VB have x': "x \<in> span B"
1.1721 -        by blast
1.1722 -      from span_trans[OF a(2), unfolded eq, OF x']
1.1723 -      have "x \<in> span (B - {a})" .
1.1724 -    }
1.1725 -    then have th1: "V \<subseteq> span (B - {a})"
1.1726 -      by blast
1.1727 -    have th2: "finite (B - {a})"
1.1728 -      using fB by auto
1.1729 -    from span_card_ge_dim[OF th0 th1 th2]
1.1730 -    have c: "dim V \<le> card (B - {a})" .
1.1731 -    from c c0 dVB cb have False by simp
1.1732 -  }
1.1733 -  then show ?thesis
1.1734 -    unfolding dependent_def by blast
1.1735 -qed
1.1736 -
1.1737 -lemma card_eq_dim:
1.1738 -  fixes B :: "'a::euclidean_space set"
1.1739 -  shows "B \<subseteq> V \<Longrightarrow> card B = dim V \<Longrightarrow> finite B \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B"
1.1740 -  by (metis order_eq_iff card_le_dim_spanning card_ge_dim_independent)
1.1741 -
1.1742 -text \<open>More general size bound lemmas.\<close>
1.1743 -
1.1744 -lemma independent_bound_general:
1.1745 -  fixes S :: "'a::euclidean_space set"
1.1746 -  shows "independent S \<Longrightarrow> finite S \<and> card S \<le> dim S"
1.1747 -  by (metis independent_card_le_dim independent_bound subset_refl)
1.1748 -
1.1749 -lemma dependent_biggerset_general:
1.1750 -  fixes S :: "'a::euclidean_space set"
1.1751 -  shows "(finite S \<Longrightarrow> card S > dim S) \<Longrightarrow> dependent S"
1.1752 -  using independent_bound_general[of S] by (metis linorder_not_le)
1.1753 -
1.1754 -lemma dim_span [simp]:
1.1755 -  fixes S :: "'a::euclidean_space set"
1.1756 -  shows "dim (span S) = dim S"
1.1757 -proof -
1.1758 -  have th0: "dim S \<le> dim (span S)"
1.1759 -    by (auto simp add: subset_eq intro: dim_subset span_superset)
1.1760 -  from basis_exists[of S]
1.1761 -  obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
1.1762 -    by blast
1.1763 -  from B have fB: "finite B" "card B = dim S"
1.1764 -    using independent_bound by blast+
1.1765 -  have bSS: "B \<subseteq> span S"
1.1766 -    using B(1) by (metis subset_eq span_inc)
1.1767 -  have sssB: "span S \<subseteq> span B"
1.1768 -    using span_mono[OF B(3)] by (simp add: span_span)
1.1769 -  from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis
1.1770 -    using fB(2) by arith
1.1771 -qed
1.1772 -
1.1773 -lemma subset_le_dim:
1.1774 -  fixes S :: "'a::euclidean_space set"
1.1775 -  shows "S \<subseteq> span T \<Longrightarrow> dim S \<le> dim T"
1.1776 -  by (metis dim_span dim_subset)
1.1777 -
1.1778 -lemma span_eq_dim:
1.1779 -  fixes S :: "'a::euclidean_space set"
1.1780 -  shows "span S = span T \<Longrightarrow> dim S = dim T"
1.1781 -  by (metis dim_span)
1.1782 -
1.1783 -lemma dim_image_le:
1.1784 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.1785 -  assumes lf: "linear f"
1.1786 -  shows "dim (f ` S) \<le> dim (S)"
1.1787 -proof -
1.1788 -  from basis_exists[of S] obtain B where
1.1789 -    B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" by blast
1.1790 -  from B have fB: "finite B" "card B = dim S"
1.1791 -    using independent_bound by blast+
1.1792 -  have "dim (f ` S) \<le> card (f ` B)"
1.1793 -    apply (rule span_card_ge_dim)
1.1794 -    using lf B fB
1.1795 -    apply (auto simp add: span_linear_image spans_image subset_image_iff)
1.1796 -    done
1.1797 -  also have "\<dots> \<le> dim S"
1.1798 -    using card_image_le[OF fB(1)] fB by simp
1.1799 -  finally show ?thesis .
1.1800 -qed
1.1801 -
1.1802  text \<open>Picking an orthogonal replacement for a spanning set.\<close>
1.1803
1.1804  lemma vector_sub_project_orthogonal:
1.1805 @@ -2367,10 +763,10 @@
1.1806      have "x - k *\<^sub>R (a - (\<Sum>x\<in>C. (x \<bullet> a / (x \<bullet> x)) *\<^sub>R x)) \<in> span C \<longleftrightarrow> x - k *\<^sub>R a \<in> span C"
1.1807        apply (simp only: scaleR_right_diff_distrib th0)
1.1809 -      apply (rule span_mul)
1.1810 +      apply (rule span_scale)
1.1811        apply (rule span_sum)
1.1812 -      apply (rule span_mul)
1.1813 -      apply (rule span_superset)
1.1814 +      apply (rule span_scale)
1.1815 +      apply (rule span_base)
1.1816        apply assumption
1.1817        done
1.1818    }
1.1819 @@ -2402,7 +798,8 @@
1.1820
1.1821  lemma orthogonal_basis_exists:
1.1822    fixes V :: "('a::euclidean_space) set"
1.1823 -  shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and> (card B = dim V) \<and> pairwise orthogonal B"
1.1824 +  shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and>
1.1825 +  (card B = dim V) \<and> pairwise orthogonal B"
1.1826  proof -
1.1827    from basis_exists[of V] obtain B where
1.1828      B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V"
1.1829 @@ -2413,7 +810,7 @@
1.1830      C: "finite C" "card C \<le> card B" "span C = span B" "pairwise orthogonal C"
1.1831      by blast
1.1832    from C B have CSV: "C \<subseteq> span V"
1.1833 -    by (metis span_inc span_mono subset_trans)
1.1834 +    by (metis span_superset span_mono subset_trans)
1.1835    from span_mono[OF B(3)] C have SVC: "span V \<subseteq> span C"
1.1837    from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB
1.1838 @@ -2423,7 +820,7 @@
1.1839      by simp
1.1840    moreover have "dim V \<le> card C"
1.1841      using span_card_ge_dim[OF CSV SVC C(1)]
1.1842 -    by (simp add: dim_span)
1.1843 +    by simp
1.1844    ultimately have CdV: "card C = dim V"
1.1845      using C(1) by simp
1.1846    from C B CSV CdV iC show ?thesis
1.1847 @@ -2440,7 +837,8 @@
1.1848    from sU obtain a where a: "a \<notin> span S"
1.1849      by blast
1.1850    from orthogonal_basis_exists obtain B where
1.1851 -    B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B" "card B = dim S" "pairwise orthogonal B"
1.1852 +    B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B"
1.1853 +    "card B = dim S" "pairwise orthogonal B"
1.1854      by blast
1.1855    from B have fB: "finite B" "card B = dim S"
1.1856      using independent_bound by auto
1.1857 @@ -2451,8 +849,8 @@
1.1858    have "sum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> span S"
1.1859      unfolding sSB
1.1860      apply (rule span_sum)
1.1861 -    apply (rule span_mul)
1.1862 -    apply (rule span_superset)
1.1863 +    apply (rule span_scale)
1.1864 +    apply (rule span_base)
1.1865      apply assumption
1.1866      done
1.1867    with a have a0:"?a  \<noteq> 0"
1.1868 @@ -2504,7 +902,7 @@
1.1869      then have "dim (span S) = dim (UNIV :: ('a) set)"
1.1870        by simp
1.1871      then have "dim S = DIM('a)"
1.1872 -      by (simp add: dim_span dim_UNIV)
1.1873 +      by (metis Euclidean_Space.dim_UNIV dim_span)
1.1874      with d have False by arith
1.1875    }
1.1876    then have th: "span S \<noteq> UNIV"
1.1877 @@ -2512,132 +910,15 @@
1.1878    from span_not_univ_subset_hyperplane[OF th] show ?thesis .
1.1879  qed
1.1880
1.1881 -text \<open>We can extend a linear basis-basis injection to the whole set.\<close>
1.1882 -
1.1883 -lemma linear_indep_image_lemma:
1.1884 -  assumes lf: "linear f"
1.1885 -    and fB: "finite B"
1.1886 -    and ifB: "independent (f ` B)"
1.1887 -    and fi: "inj_on f B"
1.1888 -    and xsB: "x \<in> span B"
1.1889 -    and fx: "f x = 0"
1.1890 -  shows "x = 0"
1.1891 -  using fB ifB fi xsB fx
1.1892 -proof (induct arbitrary: x rule: finite_induct[OF fB])
1.1893 -  case 1
1.1894 -  then show ?case by auto
1.1895 -next
1.1896 -  case (2 a b x)
1.1897 -  have fb: "finite b" using "2.prems" by simp
1.1898 -  have th0: "f ` b \<subseteq> f ` (insert a b)"
1.1899 -    apply (rule image_mono)
1.1900 -    apply blast
1.1901 -    done
1.1902 -  from independent_mono[ OF "2.prems"(2) th0]
1.1903 -  have ifb: "independent (f ` b)"  .
1.1904 -  have fib: "inj_on f b"
1.1905 -    apply (rule subset_inj_on [OF "2.prems"(3)])
1.1906 -    apply blast
1.1907 -    done
1.1908 -  from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)]
1.1909 -  obtain k where k: "x - k*\<^sub>R a \<in> span (b - {a})"
1.1910 -    by blast
1.1911 -  have "f (x - k*\<^sub>R a) \<in> span (f ` b)"
1.1912 -    unfolding span_linear_image[OF lf]
1.1913 -    apply (rule imageI)
1.1914 -    using k span_mono[of "b - {a}" b]
1.1915 -    apply blast
1.1916 -    done
1.1917 -  then have "f x - k*\<^sub>R f a \<in> span (f ` b)"
1.1918 -    by (simp add: linear_diff[OF lf] linear_cmul[OF lf])
1.1919 -  then have th: "-k *\<^sub>R f a \<in> span (f ` b)"
1.1920 -    using "2.prems"(5) by simp
1.1921 -  have xsb: "x \<in> span b"
1.1922 -  proof (cases "k = 0")
1.1923 -    case True
1.1924 -    with k have "x \<in> span (b - {a})" by simp
1.1925 -    then show ?thesis using span_mono[of "b - {a}" b]
1.1926 -      by blast
1.1927 -  next
1.1928 -    case False
1.1929 -    with span_mul[OF th, of "- 1/ k"]
1.1930 -    have th1: "f a \<in> span (f ` b)"
1.1931 -      by auto
1.1932 -    from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
1.1933 -    have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
1.1934 -    from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
1.1935 -    have "f a \<notin> span (f ` b)" using tha
1.1936 -      using "2.hyps"(2)
1.1937 -      "2.prems"(3) by auto
1.1938 -    with th1 have False by blast
1.1939 -    then show ?thesis by blast
1.1940 -  qed
1.1941 -  from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] show "x = 0" .
1.1942 -qed
1.1943 -
1.1944 -text \<open>Can construct an isomorphism between spaces of same dimension.\<close>
1.1945 -
1.1946 -lemma subspace_isomorphism:
1.1947 -  fixes S :: "'a::euclidean_space set"
1.1948 -    and T :: "'b::euclidean_space set"
1.1949 -  assumes s: "subspace S"
1.1950 -    and t: "subspace T"
1.1951 -    and d: "dim S = dim T"
1.1952 -  shows "\<exists>f. linear f \<and> f ` S = T \<and> inj_on f S"
1.1953 -proof -
1.1954 -  from basis_exists[of S] independent_bound
1.1955 -  obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" and fB: "finite B"
1.1956 -    by blast
1.1957 -  from basis_exists[of T] independent_bound
1.1958 -  obtain C where C: "C \<subseteq> T" "independent C" "T \<subseteq> span C" "card C = dim T" and fC: "finite C"
1.1959 -    by blast
1.1960 -  from B(4) C(4) card_le_inj[of B C] d
1.1961 -  obtain f where f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close>
1.1962 -    by auto
1.1963 -  from linear_independent_extend[OF B(2)]
1.1964 -  obtain g where g: "linear g" "\<forall>x\<in> B. g x = f x"
1.1965 -    by blast
1.1966 -  from inj_on_iff_eq_card[OF fB, of f] f(2) have "card (f ` B) = card B"
1.1967 -    by simp
1.1968 -  with B(4) C(4) have ceq: "card (f ` B) = card C"
1.1969 -    using d by simp
1.1970 -  have "g ` B = f ` B"
1.1971 -    using g(2) by (auto simp add: image_iff)
1.1972 -  also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] .
1.1973 -  finally have gBC: "g ` B = C" .
1.1974 -  have gi: "inj_on g B"
1.1975 -    using f(2) g(2) by (auto simp add: inj_on_def)
1.1976 -  note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
1.1977 -  {
1.1978 -    fix x y
1.1979 -    assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y"
1.1980 -    from B(3) x y have x': "x \<in> span B" and y': "y \<in> span B"
1.1981 -      by blast+
1.1982 -    from gxy have th0: "g (x - y) = 0"
1.1983 -      by (simp add: linear_diff[OF g(1)])
1.1984 -    have th1: "x - y \<in> span B"
1.1985 -      using x' y' by (metis span_diff)
1.1986 -    have "x = y"
1.1987 -      using g0[OF th1 th0] by simp
1.1988 -  }
1.1989 -  then have giS: "inj_on g S"
1.1990 -    unfolding inj_on_def by blast
1.1991 -  from span_subspace[OF B(1,3) s] have "g ` S = span (g ` B)"
1.1992 -    by (simp add: span_linear_image[OF g(1)])
1.1993 -  also have "\<dots> = span C" unfolding gBC ..
1.1994 -  also have "\<dots> = T" using span_subspace[OF C(1,3) t] .
1.1995 -  finally have gS: "g ` S = T" .
1.1996 -  from g(1) gS giS show ?thesis
1.1997 -    by blast
1.1998 -qed
1.1999 -
1.2000  lemma linear_eq_stdbasis:
1.2001    fixes f :: "'a::euclidean_space \<Rightarrow> _"
1.2002    assumes lf: "linear f"
1.2003      and lg: "linear g"
1.2004 -    and fg: "\<forall>b\<in>Basis. f b = g b"
1.2005 +    and fg: "\<And>b. b \<in> Basis \<Longrightarrow> f b = g b"
1.2006    shows "f = g"
1.2007 -  using linear_eq[OF lf lg, of _ Basis] fg by auto
1.2008 +  using linear_eq_on_span[OF lf lg, of Basis] fg
1.2009 +  by auto
1.2010 +
1.2011
1.2012  text \<open>Similar results for bilinear functions.\<close>
1.2013
1.2014 @@ -2652,7 +933,8 @@
1.2015    let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
1.2016    from bf bg have sp: "subspace ?P"
1.2017      unfolding bilinear_def linear_iff subspace_def bf bg
1.2018 -    by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
1.2019 +    by (auto simp add: span_zero bilinear_lzero[OF bf] bilinear_lzero[OF bg]
1.2022
1.2023    have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
1.2024 @@ -2662,7 +944,8 @@
1.2026      apply (auto simp add: subspace_def)
1.2027      using bf bg unfolding bilinear_def linear_iff
1.2028 -    apply (auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def
1.2029 +      apply (auto simp add: span_zero bilinear_rzero[OF bf] bilinear_rzero[OF bg]
1.2032      done
1.2033    then show ?thesis
1.2034 @@ -2677,234 +960,6 @@
1.2035    shows "f = g"
1.2036    using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
1.2037
1.2038 -text \<open>An injective map @{typ "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"} is also surjective.\<close>
1.2039 -
1.2040 -lemma linear_injective_imp_surjective:
1.2041 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.2042 -  assumes lf: "linear f"
1.2043 -    and fi: "inj f"
1.2044 -  shows "surj f"
1.2045 -proof -
1.2046 -  let ?U = "UNIV :: 'a set"
1.2047 -  from basis_exists[of ?U] obtain B
1.2048 -    where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" "card B = dim ?U"
1.2049 -    by blast
1.2050 -  from B(4) have d: "dim ?U = card B"
1.2051 -    by simp
1.2052 -  have th: "?U \<subseteq> span (f ` B)"
1.2053 -    apply (rule card_ge_dim_independent)
1.2054 -    apply blast
1.2055 -    apply (rule independent_injective_image[OF B(2) lf fi])
1.2056 -    apply (rule order_eq_refl)
1.2057 -    apply (rule sym)
1.2058 -    unfolding d
1.2059 -    apply (rule card_image)
1.2060 -    apply (rule subset_inj_on[OF fi])
1.2061 -    apply blast
1.2062 -    done
1.2063 -  from th show ?thesis
1.2064 -    unfolding span_linear_image[OF lf] surj_def
1.2065 -    using B(3) by blast
1.2066 -qed
1.2067 -
1.2068 -text \<open>And vice versa.\<close>
1.2069 -
1.2070 -lemma surjective_iff_injective_gen:
1.2071 -  assumes fS: "finite S"
1.2072 -    and fT: "finite T"
1.2073 -    and c: "card S = card T"
1.2074 -    and ST: "f ` S \<subseteq> T"
1.2075 -  shows "(\<forall>y \<in> T. \<exists>x \<in> S. f x = y) \<longleftrightarrow> inj_on f S"
1.2076 -  (is "?lhs \<longleftrightarrow> ?rhs")
1.2077 -proof
1.2078 -  assume h: "?lhs"
1.2079 -  {
1.2080 -    fix x y
1.2081 -    assume x: "x \<in> S"
1.2082 -    assume y: "y \<in> S"
1.2083 -    assume f: "f x = f y"
1.2084 -    from x fS have S0: "card S \<noteq> 0"
1.2085 -      by auto
1.2086 -    have "x = y"
1.2087 -    proof (rule ccontr)
1.2088 -      assume xy: "\<not> ?thesis"
1.2089 -      have th: "card S \<le> card (f ` (S - {y}))"
1.2090 -        unfolding c
1.2091 -        apply (rule card_mono)
1.2092 -        apply (rule finite_imageI)
1.2093 -        using fS apply simp
1.2094 -        using h xy x y f unfolding subset_eq image_iff
1.2095 -        apply auto
1.2096 -        apply (case_tac "xa = f x")
1.2097 -        apply (rule bexI[where x=x])
1.2098 -        apply auto
1.2099 -        done
1.2100 -      also have " \<dots> \<le> card (S - {y})"
1.2101 -        apply (rule card_image_le)
1.2102 -        using fS by simp
1.2103 -      also have "\<dots> \<le> card S - 1" using y fS by simp
1.2104 -      finally show False using S0 by arith
1.2105 -    qed
1.2106 -  }
1.2107 -  then show ?rhs
1.2108 -    unfolding inj_on_def by blast
1.2109 -next
1.2110 -  assume h: ?rhs
1.2111 -  have "f ` S = T"
1.2112 -    apply (rule card_subset_eq[OF fT ST])
1.2113 -    unfolding card_image[OF h]
1.2114 -    apply (rule c)
1.2115 -    done
1.2116 -  then show ?lhs by blast
1.2117 -qed
1.2118 -
1.2119 -lemma linear_surjective_imp_injective:
1.2120 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.2121 -  assumes lf: "linear f"
1.2122 -    and sf: "surj f"
1.2123 -  shows "inj f"
1.2124 -proof -
1.2125 -  let ?U = "UNIV :: 'a set"
1.2126 -  from basis_exists[of ?U] obtain B
1.2127 -    where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" and d: "card B = dim ?U"
1.2128 -    by blast
1.2129 -  {
1.2130 -    fix x
1.2131 -    assume x: "x \<in> span B"
1.2132 -    assume fx: "f x = 0"
1.2133 -    from B(2) have fB: "finite B"
1.2134 -      using independent_bound by auto
1.2135 -    have fBi: "independent (f ` B)"
1.2136 -      apply (rule card_le_dim_spanning[of "f ` B" ?U])
1.2137 -      apply blast
1.2138 -      using sf B(3)
1.2139 -      unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
1.2140 -      apply blast
1.2141 -      using fB apply blast
1.2142 -      unfolding d[symmetric]
1.2143 -      apply (rule card_image_le)
1.2144 -      apply (rule fB)
1.2145 -      done
1.2146 -    have th0: "dim ?U \<le> card (f ` B)"
1.2147 -      apply (rule span_card_ge_dim)
1.2148 -      apply blast
1.2149 -      unfolding span_linear_image[OF lf]
1.2150 -      apply (rule subset_trans[where B = "f ` UNIV"])
1.2151 -      using sf unfolding surj_def
1.2152 -      apply blast
1.2153 -      apply (rule image_mono)
1.2154 -      apply (rule B(3))
1.2155 -      apply (metis finite_imageI fB)
1.2156 -      done
1.2157 -    moreover have "card (f ` B) \<le> card B"
1.2158 -      by (rule card_image_le, rule fB)
1.2159 -    ultimately have th1: "card B = card (f ` B)"
1.2160 -      unfolding d by arith
1.2161 -    have fiB: "inj_on f B"
1.2162 -      unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric]
1.2163 -      by blast
1.2164 -    from linear_indep_image_lemma[OF lf fB fBi fiB x] fx
1.2165 -    have "x = 0" by blast
1.2166 -  }
1.2167 -  then show ?thesis
1.2168 -    unfolding linear_injective_0[OF lf]
1.2169 -    using B(3)
1.2170 -    by blast
1.2171 -qed
1.2172 -
1.2173 -text \<open>Hence either is enough for isomorphism.\<close>
1.2174 -
1.2175 -lemma left_right_inverse_eq:
1.2176 -  assumes fg: "f \<circ> g = id"
1.2177 -    and gh: "g \<circ> h = id"
1.2178 -  shows "f = h"
1.2179 -proof -
1.2180 -  have "f = f \<circ> (g \<circ> h)"
1.2181 -    unfolding gh by simp
1.2182 -  also have "\<dots> = (f \<circ> g) \<circ> h"
1.2183 -    by (simp add: o_assoc)
1.2184 -  finally show "f = h"
1.2185 -    unfolding fg by simp
1.2186 -qed
1.2187 -
1.2188 -lemma isomorphism_expand:
1.2189 -  "f \<circ> g = id \<and> g \<circ> f = id \<longleftrightarrow> (\<forall>x. f (g x) = x) \<and> (\<forall>x. g (f x) = x)"
1.2190 -  by (simp add: fun_eq_iff o_def id_def)
1.2191 -
1.2192 -lemma linear_injective_isomorphism:
1.2193 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.2194 -  assumes lf: "linear f"
1.2195 -    and fi: "inj f"
1.2196 -  shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
1.2197 -  unfolding isomorphism_expand[symmetric]
1.2198 -  using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]]
1.2199 -    linear_injective_left_inverse[OF lf fi]
1.2200 -  by (metis left_right_inverse_eq)
1.2201 -
1.2202 -lemma linear_surjective_isomorphism:
1.2203 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.2204 -  assumes lf: "linear f"
1.2205 -    and sf: "surj f"
1.2206 -  shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
1.2207 -  unfolding isomorphism_expand[symmetric]
1.2208 -  using linear_surjective_right_inverse[OF lf sf]
1.2209 -    linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]]
1.2210 -  by (metis left_right_inverse_eq)
1.2211 -
1.2212 -text \<open>Left and right inverses are the same for
1.2213 -  @{typ "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"}.\<close>
1.2214 -
1.2215 -lemma linear_inverse_left:
1.2216 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.2217 -  assumes lf: "linear f"
1.2218 -    and lf': "linear f'"
1.2219 -  shows "f \<circ> f' = id \<longleftrightarrow> f' \<circ> f = id"
1.2220 -proof -
1.2221 -  {
1.2222 -    fix f f':: "'a \<Rightarrow> 'a"
1.2223 -    assume lf: "linear f" "linear f'"
1.2224 -    assume f: "f \<circ> f' = id"
1.2225 -    from f have sf: "surj f"
1.2226 -      apply (auto simp add: o_def id_def surj_def)
1.2227 -      apply metis
1.2228 -      done
1.2229 -    from linear_surjective_isomorphism[OF lf(1) sf] lf f
1.2230 -    have "f' \<circ> f = id"
1.2231 -      unfolding fun_eq_iff o_def id_def by metis
1.2232 -  }
1.2233 -  then show ?thesis
1.2234 -    using lf lf' by metis
1.2235 -qed
1.2236 -
1.2237 -text \<open>Moreover, a one-sided inverse is automatically linear.\<close>
1.2238 -
1.2239 -lemma left_inverse_linear:
1.2240 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.2241 -  assumes lf: "linear f"
1.2242 -    and gf: "g \<circ> f = id"
1.2243 -  shows "linear g"
1.2244 -proof -
1.2245 -  from gf have fi: "inj f"
1.2246 -    apply (auto simp add: inj_on_def o_def id_def fun_eq_iff)
1.2247 -    apply metis
1.2248 -    done
1.2249 -  from linear_injective_isomorphism[OF lf fi]
1.2250 -  obtain h :: "'a \<Rightarrow> 'a" where h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
1.2251 -    by blast
1.2252 -  have "h = g"
1.2253 -    apply (rule ext) using gf h(2,3)
1.2254 -    apply (simp add: o_def id_def fun_eq_iff)
1.2255 -    apply metis
1.2256 -    done
1.2257 -  with h(1) show ?thesis by blast
1.2258 -qed
1.2259 -
1.2260 -lemma inj_linear_imp_inv_linear:
1.2261 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.2262 -  assumes "linear f" "inj f" shows "linear (inv f)"
1.2263 -using assms inj_iff left_inverse_linear by blast
1.2264 -
1.2265 -
1.2266  subsection \<open>Infinity norm\<close>
1.2267
1.2268  definition%important "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
1.2269 @@ -3181,7 +1236,7 @@
1.2270    qed
1.2271    then show ?thesis
1.2272      apply (clarsimp simp: collinear_def)
1.2273 -    by (metis real_vector.scale_zero_right vector_fraction_eq_iff)
1.2274 +    by (metis scaleR_zero_right vector_fraction_eq_iff)
1.2275  qed
1.2276
1.2277  lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S"
```