src/HOL/Analysis/Linear_Algebra.thy
 author wenzelm Fri Aug 12 17:53:55 2016 +0200 (2016-08-12) changeset 63680 6e1e8b5abbfa parent 63627 6ddb43c6b711 child 63881 b746b19197bd permissions -rw-r--r--
more symbols;
1 (*  Title:      HOL/Analysis/Linear_Algebra.thy
2     Author:     Amine Chaieb, University of Cambridge
3 *)
5 section \<open>Elementary linear algebra on Euclidean spaces\<close>
7 theory Linear_Algebra
8 imports
9   Euclidean_Space
10   "~~/src/HOL/Library/Infinite_Set"
11 begin
13 subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
15 definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
16   where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
18 lemma hull_same: "S s \<Longrightarrow> S hull s = s"
19   unfolding hull_def by auto
21 lemma hull_in: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> S (S hull s)"
22   unfolding hull_def Ball_def by auto
24 lemma hull_eq: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> (S hull s) = s \<longleftrightarrow> S s"
25   using hull_same[of S s] hull_in[of S s] by metis
27 lemma hull_hull [simp]: "S hull (S hull s) = S hull s"
28   unfolding hull_def by blast
30 lemma hull_subset[intro]: "s \<subseteq> (S hull s)"
31   unfolding hull_def by blast
33 lemma hull_mono: "s \<subseteq> t \<Longrightarrow> (S hull s) \<subseteq> (S hull t)"
34   unfolding hull_def by blast
36 lemma hull_antimono: "\<forall>x. S x \<longrightarrow> T x \<Longrightarrow> (T hull s) \<subseteq> (S hull s)"
37   unfolding hull_def by blast
39 lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (S hull s) \<subseteq> t"
40   unfolding hull_def by blast
42 lemma subset_hull: "S t \<Longrightarrow> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
43   unfolding hull_def by blast
45 lemma hull_UNIV [simp]: "S hull UNIV = UNIV"
46   unfolding hull_def by auto
48 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)"
49   unfolding hull_def by auto
51 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"
52   using hull_minimal[of S "{x. P x}" Q]
53   by (auto simp add: subset_eq)
55 lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S"
56   by (metis hull_subset subset_eq)
58 lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
59   unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
61 lemma hull_union:
62   assumes T: "\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)"
63   shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
64   apply rule
65   apply (rule hull_mono)
66   unfolding Un_subset_iff
67   apply (metis hull_subset Un_upper1 Un_upper2 subset_trans)
68   apply (rule hull_minimal)
69   apply (metis hull_union_subset)
70   apply (metis hull_in T)
71   done
73 lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> S hull (insert a s) = S hull s"
74   unfolding hull_def by blast
76 lemma hull_redundant: "a \<in> (S hull s) \<Longrightarrow> S hull (insert a s) = S hull s"
77   by (metis hull_redundant_eq)
79 subsection \<open>Linear functions.\<close>
81 lemma linear_iff:
82   "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)"
83   (is "linear f \<longleftrightarrow> ?rhs")
84 proof
85   assume "linear f"
86   then interpret f: linear f .
88 next
89   assume "?rhs"
90   then show "linear f" by unfold_locales simp_all
91 qed
93 lemma linear_compose_cmul: "linear f \<Longrightarrow> linear (\<lambda>x. c *\<^sub>R f x)"
94   by (simp add: linear_iff algebra_simps)
96 lemma linear_compose_scaleR: "linear f \<Longrightarrow> linear (\<lambda>x. f x *\<^sub>R c)"
99 lemma linear_compose_neg: "linear f \<Longrightarrow> linear (\<lambda>x. - f x)"
102 lemma linear_compose_add: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (\<lambda>x. f x + g x)"
103   by (simp add: linear_iff algebra_simps)
105 lemma linear_compose_sub: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (\<lambda>x. f x - g x)"
106   by (simp add: linear_iff algebra_simps)
108 lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g \<circ> f)"
111 lemma linear_id: "linear id"
112   by (simp add: linear_iff id_def)
114 lemma linear_zero: "linear (\<lambda>x. 0)"
117 lemma linear_uminus: "linear uminus"
120 lemma linear_compose_setsum:
121   assumes lS: "\<forall>a \<in> S. linear (f a)"
122   shows "linear (\<lambda>x. setsum (\<lambda>a. f a x) S)"
123 proof (cases "finite S")
124   case True
125   then show ?thesis
127 next
128   case False
129   then show ?thesis
131 qed
133 lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
134   unfolding linear_iff
135   apply clarsimp
136   apply (erule allE[where x="0::'a"])
137   apply simp
138   done
140 lemma linear_cmul: "linear f \<Longrightarrow> f (c *\<^sub>R x) = c *\<^sub>R f x"
141   by (rule linear.scaleR)
143 lemma linear_neg: "linear f \<Longrightarrow> f (- x) = - f x"
144   using linear_cmul [where c="-1"] by simp
146 lemma linear_add: "linear f \<Longrightarrow> f (x + y) = f x + f y"
147   by (metis linear_iff)
149 lemma linear_diff: "linear f \<Longrightarrow> f (x - y) = f x - f y"
150   using linear_add [of f x "- y"] by (simp add: linear_neg)
152 lemma linear_setsum:
153   assumes f: "linear f"
154   shows "f (setsum g S) = setsum (f \<circ> g) S"
155 proof (cases "finite S")
156   case True
157   then show ?thesis
159 next
160   case False
161   then show ?thesis
162     by (simp add: linear_0 [OF f])
163 qed
165 lemma linear_setsum_mul:
166   assumes lin: "linear f"
167   shows "f (setsum (\<lambda>i. c i *\<^sub>R v i) S) = setsum (\<lambda>i. c i *\<^sub>R f (v i)) S"
168   using linear_setsum[OF lin, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lin]
169   by simp
171 lemma linear_injective_0:
172   assumes lin: "linear f"
173   shows "inj f \<longleftrightarrow> (\<forall>x. f x = 0 \<longrightarrow> x = 0)"
174 proof -
175   have "inj f \<longleftrightarrow> (\<forall> x y. f x = f y \<longrightarrow> x = y)"
177   also have "\<dots> \<longleftrightarrow> (\<forall> x y. f x - f y = 0 \<longrightarrow> x - y = 0)"
178     by simp
179   also have "\<dots> \<longleftrightarrow> (\<forall> x y. f (x - y) = 0 \<longrightarrow> x - y = 0)"
180     by (simp add: linear_diff[OF lin])
181   also have "\<dots> \<longleftrightarrow> (\<forall> x. f x = 0 \<longrightarrow> x = 0)"
182     by auto
183   finally show ?thesis .
184 qed
186 lemma linear_scaleR  [simp]: "linear (\<lambda>x. scaleR c x)"
189 lemma linear_scaleR_left [simp]: "linear (\<lambda>r. scaleR r x)"
192 lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
196   assumes "linear f"
197   shows "f (a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x +  b *\<^sub>R f y"
198   using linear_add[of f] linear_cmul[of f] assms by simp
200 subsection \<open>Subspaces of vector spaces\<close>
202 definition (in real_vector) subspace :: "'a set \<Rightarrow> bool"
203   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)"
205 definition (in real_vector) "span S = (subspace hull S)"
206 definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
207 abbreviation (in real_vector) "independent s \<equiv> \<not> dependent s"
209 text \<open>Closure properties of subspaces.\<close>
211 lemma subspace_UNIV[simp]: "subspace UNIV"
214 lemma (in real_vector) subspace_0: "subspace S \<Longrightarrow> 0 \<in> S"
215   by (metis subspace_def)
217 lemma (in real_vector) subspace_add: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
218   by (metis subspace_def)
220 lemma (in real_vector) subspace_mul: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> c *\<^sub>R x \<in> S"
221   by (metis subspace_def)
223 lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> - x \<in> S"
224   by (metis scaleR_minus1_left subspace_mul)
226 lemma subspace_diff: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
227   using subspace_add [of S x "- y"] by (simp add: subspace_neg)
229 lemma (in real_vector) subspace_setsum:
230   assumes sA: "subspace A"
231     and f: "\<And>x. x \<in> B \<Longrightarrow> f x \<in> A"
232   shows "setsum f B \<in> A"
233 proof (cases "finite B")
234   case True
235   then show ?thesis
236     using f by induct (simp_all add: subspace_0 [OF sA] subspace_add [OF sA])
237 qed (simp add: subspace_0 [OF sA])
239 lemma subspace_trivial [iff]: "subspace {0}"
242 lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<inter> B)"
245 lemma subspace_Times: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<times> B)"
246   unfolding subspace_def zero_prod_def by simp
248 lemma subspace_sums: "\<lbrakk>subspace S; subspace T\<rbrakk> \<Longrightarrow> subspace {x + y|x y. x \<in> S \<and> y \<in> T}"
250 apply (intro conjI impI allI)
252  apply clarify
256 subsection \<open>Properties of span\<close>
258 lemma (in real_vector) span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
259   by (metis span_def hull_mono)
261 lemma (in real_vector) subspace_span [iff]: "subspace (span S)"
262   unfolding span_def
263   apply (rule hull_in)
264   apply (simp only: subspace_def Inter_iff Int_iff subset_eq)
265   apply auto
266   done
268 lemma (in real_vector) span_clauses:
269   "a \<in> S \<Longrightarrow> a \<in> span S"
270   "0 \<in> span S"
271   "x\<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
272   "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
273   by (metis span_def hull_subset subset_eq) (metis subspace_span subspace_def)+
275 lemma span_unique:
276   "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> (\<And>T'. S \<subseteq> T' \<Longrightarrow> subspace T' \<Longrightarrow> T \<subseteq> T') \<Longrightarrow> span S = T"
277   unfolding span_def by (rule hull_unique)
279 lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
280   unfolding span_def by (rule hull_minimal)
282 lemma span_UNIV: "span UNIV = UNIV"
283   by (intro span_unique) auto
285 lemma (in real_vector) span_induct:
286   assumes x: "x \<in> span S"
287     and P: "subspace (Collect P)"
288     and SP: "\<And>x. x \<in> S \<Longrightarrow> P x"
289   shows "P x"
290 proof -
291   from SP have SP': "S \<subseteq> Collect P"
293   from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
294   show ?thesis
295     using subset_eq by force
296 qed
298 lemma span_empty[simp]: "span {} = {0}"
300   apply (rule hull_unique)
301   apply (auto simp add: subspace_def)
302   done
304 lemma (in real_vector) independent_empty [iff]: "independent {}"
307 lemma dependent_single[simp]: "dependent {x} \<longleftrightarrow> x = 0"
308   unfolding dependent_def by auto
310 lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> independent B"
311   apply (clarsimp simp add: dependent_def span_mono)
312   apply (subgoal_tac "span (B - {a}) \<le> span (A - {a})")
313   apply force
314   apply (rule span_mono)
315   apply auto
316   done
318 lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow>  subspace B \<Longrightarrow> span A = B"
319   by (metis order_antisym span_def hull_minimal)
321 lemma (in real_vector) span_induct':
322   "\<forall>x \<in> S. P x \<Longrightarrow> subspace {x. P x} \<Longrightarrow> \<forall>x \<in> span S. P x"
323   unfolding span_def by (rule hull_induct) auto
325 inductive_set (in real_vector) span_induct_alt_help for S :: "'a set"
326 where
327   span_induct_alt_help_0: "0 \<in> span_induct_alt_help S"
328 | span_induct_alt_help_S:
329     "x \<in> S \<Longrightarrow> z \<in> span_induct_alt_help S \<Longrightarrow>
330       (c *\<^sub>R x + z) \<in> span_induct_alt_help S"
332 lemma span_induct_alt':
333   assumes h0: "h 0"
334     and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)"
335   shows "\<forall>x \<in> span S. h x"
336 proof -
337   {
338     fix x :: 'a
339     assume x: "x \<in> span_induct_alt_help S"
340     have "h x"
341       apply (rule span_induct_alt_help.induct[OF x])
342       apply (rule h0)
343       apply (rule hS)
344       apply assumption
345       apply assumption
346       done
347   }
348   note th0 = this
349   {
350     fix x
351     assume x: "x \<in> span S"
352     have "x \<in> span_induct_alt_help S"
353     proof (rule span_induct[where x=x and S=S])
354       show "x \<in> span S" by (rule x)
355     next
356       fix x
357       assume xS: "x \<in> S"
358       from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1]
359       show "x \<in> span_induct_alt_help S"
360         by simp
361     next
362       have "0 \<in> span_induct_alt_help S" by (rule span_induct_alt_help_0)
363       moreover
364       {
365         fix x y
366         assume h: "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S"
367         from h have "(x + y) \<in> span_induct_alt_help S"
368           apply (induct rule: span_induct_alt_help.induct)
369           apply simp
371           apply (rule span_induct_alt_help_S)
372           apply assumption
373           apply simp
374           done
375       }
376       moreover
377       {
378         fix c x
379         assume xt: "x \<in> span_induct_alt_help S"
380         then have "(c *\<^sub>R x) \<in> span_induct_alt_help S"
381           apply (induct rule: span_induct_alt_help.induct)
384           apply (rule span_induct_alt_help_S)
385           apply assumption
386           apply simp
387           done }
388       ultimately show "subspace {a. a \<in> span_induct_alt_help S}"
389         unfolding subspace_def Ball_def by blast
390     qed
391   }
392   with th0 show ?thesis by blast
393 qed
395 lemma span_induct_alt:
396   assumes h0: "h 0"
397     and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)"
398     and x: "x \<in> span S"
399   shows "h x"
400   using span_induct_alt'[of h S] h0 hS x by blast
402 text \<open>Individual closure properties.\<close>
404 lemma span_span: "span (span A) = span A"
405   unfolding span_def hull_hull ..
407 lemma (in real_vector) span_superset: "x \<in> S \<Longrightarrow> x \<in> span S"
408   by (metis span_clauses(1))
410 lemma (in real_vector) span_0 [simp]: "0 \<in> span S"
411   by (metis subspace_span subspace_0)
413 lemma span_inc: "S \<subseteq> span S"
414   by (metis subset_eq span_superset)
416 lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
417   using span_inc[unfolded subset_eq] using span_mono[of T "span S"] span_mono[of S "span T"]
418   by (auto simp add: span_span)
420 lemma (in real_vector) dependent_0:
421   assumes "0 \<in> A"
422   shows "dependent A"
423   unfolding dependent_def
424   using assms span_0
425   by blast
427 lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
430 lemma (in real_vector) span_mul: "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
431   by (metis subspace_span subspace_mul)
433 lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S"
434   by (metis subspace_neg subspace_span)
436 lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
437   by (metis subspace_span subspace_diff)
439 lemma (in real_vector) span_setsum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> setsum f A \<in> span S"
440   by (rule subspace_setsum [OF subspace_span])
442 lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
443   by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
445 text \<open>The key breakdown property.\<close>
447 lemma span_singleton: "span {x} = range (\<lambda>k. k *\<^sub>R x)"
448 proof (rule span_unique)
449   show "{x} \<subseteq> range (\<lambda>k. k *\<^sub>R x)"
450     by (fast intro: scaleR_one [symmetric])
451   show "subspace (range (\<lambda>k. k *\<^sub>R x))"
452     unfolding subspace_def
453     by (auto intro: scaleR_add_left [symmetric])
454 next
455   fix T
456   assume "{x} \<subseteq> T" and "subspace T"
457   then show "range (\<lambda>k. k *\<^sub>R x) \<subseteq> T"
458     unfolding subspace_def by auto
459 qed
461 text \<open>Mapping under linear image.\<close>
463 lemma subspace_linear_image:
464   assumes lf: "linear f"
465     and sS: "subspace S"
466   shows "subspace (f ` S)"
467   using lf sS linear_0[OF lf]
468   unfolding linear_iff subspace_def
469   apply (auto simp add: image_iff)
470   apply (rule_tac x="x + y" in bexI)
471   apply auto
472   apply (rule_tac x="c *\<^sub>R x" in bexI)
473   apply auto
474   done
476 lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f -` S)"
477   by (auto simp add: subspace_def linear_iff linear_0[of f])
479 lemma subspace_linear_preimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace {x. f x \<in> S}"
480   by (auto simp add: subspace_def linear_iff linear_0[of f])
482 lemma span_linear_image:
483   assumes lf: "linear f"
484   shows "span (f ` S) = f ` span S"
485 proof (rule span_unique)
486   show "f ` S \<subseteq> f ` span S"
487     by (intro image_mono span_inc)
488   show "subspace (f ` span S)"
489     using lf subspace_span by (rule subspace_linear_image)
490 next
491   fix T
492   assume "f ` S \<subseteq> T" and "subspace T"
493   then show "f ` span S \<subseteq> T"
494     unfolding image_subset_iff_subset_vimage
495     by (intro span_minimal subspace_linear_vimage lf)
496 qed
498 lemma spans_image:
499   assumes lf: "linear f"
500     and VB: "V \<subseteq> span B"
501   shows "f ` V \<subseteq> span (f ` B)"
502   unfolding span_linear_image[OF lf] by (metis VB image_mono)
504 lemma span_Un: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
505 proof (rule span_unique)
506   show "A \<union> B \<subseteq> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
507     by safe (force intro: span_clauses)+
508 next
509   have "linear (\<lambda>(a, b). a + b)"
511   moreover have "subspace (span A \<times> span B)"
512     by (intro subspace_Times subspace_span)
513   ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
514     by (rule subspace_linear_image)
515 next
516   fix T
517   assume "A \<union> B \<subseteq> T" and "subspace T"
518   then show "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T"
519     by (auto intro!: subspace_add elim: span_induct)
520 qed
522 lemma span_insert: "span (insert a S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
523 proof -
524   have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
525     unfolding span_Un span_singleton
526     apply safe
527     apply (rule_tac x=k in exI, simp)
528     apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
529     apply auto
530     done
531   then show ?thesis by simp
532 qed
534 lemma span_breakdown:
535   assumes bS: "b \<in> S"
536     and aS: "a \<in> span S"
537   shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})"
538   using assms span_insert [of b "S - {b}"]
541 lemma span_breakdown_eq: "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. x - k *\<^sub>R a \<in> span S)"
544 text \<open>Hence some "reversal" results.\<close>
546 lemma in_span_insert:
547   assumes a: "a \<in> span (insert b S)"
548     and na: "a \<notin> span S"
549   shows "b \<in> span (insert a S)"
550 proof -
551   from a obtain k where k: "a - k *\<^sub>R b \<in> span S"
552     unfolding span_insert by fast
553   show ?thesis
554   proof (cases "k = 0")
555     case True
556     with k have "a \<in> span S" by simp
557     with na show ?thesis by simp
558   next
559     case False
560     from k have "(- inverse k) *\<^sub>R (a - k *\<^sub>R b) \<in> span S"
561       by (rule span_mul)
562     then have "b - inverse k *\<^sub>R a \<in> span S"
563       using \<open>k \<noteq> 0\<close> by (simp add: scaleR_diff_right)
564     then show ?thesis
565       unfolding span_insert by fast
566   qed
567 qed
569 lemma in_span_delete:
570   assumes a: "a \<in> span S"
571     and na: "a \<notin> span (S - {b})"
572   shows "b \<in> span (insert a (S - {b}))"
573   apply (rule in_span_insert)
574   apply (rule set_rev_mp)
575   apply (rule a)
576   apply (rule span_mono)
577   apply blast
578   apply (rule na)
579   done
581 text \<open>Transitivity property.\<close>
583 lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S"
584   unfolding span_def by (rule hull_redundant)
586 lemma span_trans:
587   assumes x: "x \<in> span S"
588     and y: "y \<in> span (insert x S)"
589   shows "y \<in> span S"
590   using assms by (simp only: span_redundant)
592 lemma span_insert_0[simp]: "span (insert 0 S) = span S"
593   by (simp only: span_redundant span_0)
595 text \<open>An explicit expansion is sometimes needed.\<close>
597 lemma span_explicit:
598   "span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
599   (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")
600 proof -
601   {
602     fix x
603     assume "?h x"
604     then obtain S u where "finite S" and "S \<subseteq> P" and "setsum (\<lambda>v. u v *\<^sub>R v) S = x"
605       by blast
606     then have "x \<in> span P"
607       by (auto intro: span_setsum span_mul span_superset)
608   }
609   moreover
610   have "\<forall>x \<in> span P. ?h x"
611   proof (rule span_induct_alt')
612     show "?h 0"
613       by (rule exI[where x="{}"], simp)
614   next
615     fix c x y
616     assume x: "x \<in> P"
617     assume hy: "?h y"
618     from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
619       and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y" by blast
620     let ?S = "insert x S"
621     let ?u = "\<lambda>y. if y = x then (if x \<in> S then u y + c else c) else u y"
622     from fS SP x have th0: "finite (insert x S)" "insert x S \<subseteq> P"
623       by blast+
624     have "?Q ?S ?u (c*\<^sub>R x + y)"
625     proof cases
626       assume xS: "x \<in> S"
627       have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = (\<Sum>v\<in>S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x"
628         using xS by (simp add: setsum.remove [OF fS xS] insert_absorb)
629       also have "\<dots> = (\<Sum>v\<in>S. u v *\<^sub>R v) + c *\<^sub>R x"
630         by (simp add: setsum.remove [OF fS xS] algebra_simps)
631       also have "\<dots> = c*\<^sub>R x + y"
633       finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" .
634       then show ?thesis using th0 by blast
635     next
636       assume xS: "x \<notin> S"
637       have th00: "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y"
638         unfolding u[symmetric]
639         apply (rule setsum.cong)
640         using xS
641         apply auto
642         done
643       show ?thesis using fS xS th0
645     qed
646     then show "?h (c*\<^sub>R x + y)"
647       by fast
648   qed
649   ultimately show ?thesis by blast
650 qed
652 lemma dependent_explicit:
653   "dependent P \<longleftrightarrow> (\<exists>S u. finite S \<and> S \<subseteq> P \<and> (\<exists>v\<in>S. u v \<noteq> 0 \<and> setsum (\<lambda>v. u v *\<^sub>R v) S = 0))"
654   (is "?lhs = ?rhs")
655 proof -
656   {
657     assume dP: "dependent P"
658     then obtain a S u where aP: "a \<in> P" and fS: "finite S"
659       and SP: "S \<subseteq> P - {a}" and ua: "setsum (\<lambda>v. u v *\<^sub>R v) S = a"
660       unfolding dependent_def span_explicit by blast
661     let ?S = "insert a S"
662     let ?u = "\<lambda>y. if y = a then - 1 else u y"
663     let ?v = a
664     from aP SP have aS: "a \<notin> S"
665       by blast
666     from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0"
667       by auto
668     have s0: "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"
669       using fS aS
670       apply simp
671       apply (subst (2) ua[symmetric])
672       apply (rule setsum.cong)
673       apply auto
674       done
675     with th0 have ?rhs by fast
676   }
677   moreover
678   {
679     fix S u v
680     assume fS: "finite S"
681       and SP: "S \<subseteq> P"
682       and vS: "v \<in> S"
683       and uv: "u v \<noteq> 0"
684       and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = 0"
685     let ?a = v
686     let ?S = "S - {v}"
687     let ?u = "\<lambda>i. (- u i) / u v"
688     have th0: "?a \<in> P" "finite ?S" "?S \<subseteq> P"
689       using fS SP vS by auto
690     have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =
691       setsum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
692       using fS vS uv by (simp add: setsum_diff1 field_simps)
693     also have "\<dots> = ?a"
694       unfolding scaleR_right.setsum [symmetric] u using uv by simp
695     finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
696     with th0 have ?lhs
697       unfolding dependent_def span_explicit
698       apply -
699       apply (rule bexI[where x= "?a"])
700       apply (simp_all del: scaleR_minus_left)
701       apply (rule exI[where x= "?S"])
702       apply (auto simp del: scaleR_minus_left)
703       done
704   }
705   ultimately show ?thesis by blast
706 qed
708 lemma dependent_finite:
709   assumes "finite S"
710     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)"
711            (is "?lhs = ?rhs")
712 proof
713   assume ?lhs
714   then obtain T u v
715          where "finite T" "T \<subseteq> S" "v\<in>T" "u v \<noteq> 0" "(\<Sum>v\<in>T. u v *\<^sub>R v) = 0"
716     by (force simp: dependent_explicit)
717   with assms show ?rhs
718     apply (rule_tac x="\<lambda>v. if v \<in> T then u v else 0" in exI)
719     apply (auto simp: setsum.mono_neutral_right)
720     done
721 next
722   assume ?rhs  with assms show ?lhs
723     by (fastforce simp add: dependent_explicit)
724 qed
726 lemma span_alt:
727   "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}}"
728   unfolding span_explicit
729   apply safe
730   subgoal for x S u
731     by (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
732         (auto intro!: setsum.mono_neutral_cong_right)
733   apply auto
734   done
736 lemma dependent_alt:
737   "dependent B \<longleftrightarrow>
738     (\<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))"
739   unfolding dependent_explicit
740   apply safe
741   subgoal for S u v
742     apply (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
743     apply (subst setsum.mono_neutral_cong_left[where T=S])
744     apply (auto intro!: setsum.mono_neutral_cong_right cong: rev_conj_cong)
745     done
746   apply auto
747   done
749 lemma independent_alt:
750   "independent B \<longleftrightarrow>
751     (\<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))"
752   unfolding dependent_alt by auto
754 lemma independentD_alt:
755   "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"
756   unfolding independent_alt by blast
758 lemma independentD_unique:
759   assumes B: "independent B"
760     and X: "finite {x. X x \<noteq> 0}" "{x. X x \<noteq> 0} \<subseteq> B"
761     and Y: "finite {x. Y x \<noteq> 0}" "{x. Y x \<noteq> 0} \<subseteq> B"
762     and "(\<Sum>x | X x \<noteq> 0. X x *\<^sub>R x) = (\<Sum>x| Y x \<noteq> 0. Y x *\<^sub>R x)"
763   shows "X = Y"
764 proof -
765   have "X x - Y x = 0" for x
766     using B
767   proof (rule independentD_alt)
768     have "{x. X x - Y x \<noteq> 0} \<subseteq> {x. X x \<noteq> 0} \<union> {x. Y x \<noteq> 0}"
769       by auto
770     then show "finite {x. X x - Y x \<noteq> 0}" "{x. X x - Y x \<noteq> 0} \<subseteq> B"
771       using X Y by (auto dest: finite_subset)
772     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)"
773       using X Y by (intro setsum.mono_neutral_cong_left) auto
774     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)"
775       by (simp add: scaleR_diff_left setsum_subtractf assms)
776     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)"
777       using X Y by (intro setsum.mono_neutral_cong_right) auto
778     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)"
779       using X Y by (intro setsum.mono_neutral_cong_right) auto
780     finally show "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *\<^sub>R x) = 0"
781       using assms by simp
782   qed
783   then show ?thesis
784     by auto
785 qed
787 text \<open>This is useful for building a basis step-by-step.\<close>
789 lemma independent_insert:
790   "independent (insert a S) \<longleftrightarrow>
791     (if a \<in> S then independent S else independent S \<and> a \<notin> span S)"
792   (is "?lhs \<longleftrightarrow> ?rhs")
793 proof (cases "a \<in> S")
794   case True
795   then show ?thesis
796     using insert_absorb[OF True] by simp
797 next
798   case False
799   show ?thesis
800   proof
801     assume i: ?lhs
802     then show ?rhs
803       using False
804       apply simp
805       apply (rule conjI)
806       apply (rule independent_mono)
807       apply assumption
808       apply blast
810       done
811   next
812     assume i: ?rhs
813     show ?lhs
814       using i False
815       apply (auto simp add: dependent_def)
816       by (metis in_span_insert insert_Diff_if insert_Diff_single insert_absorb)
817   qed
818 qed
820 lemma independent_Union_directed:
821   assumes directed: "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c"
822   assumes indep: "\<And>c. c \<in> C \<Longrightarrow> independent c"
823   shows "independent (\<Union>C)"
824 proof
825   assume "dependent (\<Union>C)"
826   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"
827     by (auto simp: dependent_explicit)
829   have "S \<noteq> {}"
830     using \<open>v \<in> S\<close> by auto
831   have "\<exists>c\<in>C. S \<subseteq> c"
832     using \<open>finite S\<close> \<open>S \<noteq> {}\<close> \<open>S \<subseteq> \<Union>C\<close>
833   proof (induction rule: finite_ne_induct)
834     case (insert i I)
835     then obtain c d where cd: "c \<in> C" "d \<in> C" and iI: "I \<subseteq> c" "i \<in> d"
836       by blast
837     from directed[OF cd] cd have "c \<union> d \<in> C"
838       by (auto simp: sup.absorb1 sup.absorb2)
839     with iI show ?case
840       by (intro bexI[of _ "c \<union> d"]) auto
841   qed auto
842   then obtain c where "c \<in> C" "S \<subseteq> c"
843     by auto
844   have "dependent c"
845     unfolding dependent_explicit
846     by (intro exI[of _ S] exI[of _ u] bexI[of _ v] conjI) fact+
847   with indep[OF \<open>c \<in> C\<close>] show False
848     by auto
849 qed
851 text \<open>Hence we can create a maximal independent subset.\<close>
853 lemma maximal_independent_subset_extend:
854   assumes "S \<subseteq> V" "independent S"
855   shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
856 proof -
857   let ?C = "{B. S \<subseteq> B \<and> independent B \<and> B \<subseteq> V}"
858   have "\<exists>M\<in>?C. \<forall>X\<in>?C. M \<subseteq> X \<longrightarrow> X = M"
859   proof (rule subset_Zorn)
860     fix C :: "'a set set" assume "subset.chain ?C C"
861     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"
862       "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c"
863       unfolding subset.chain_def by blast+
865     show "\<exists>U\<in>?C. \<forall>X\<in>C. X \<subseteq> U"
866     proof cases
867       assume "C = {}" with assms show ?thesis
868         by (auto intro!: exI[of _ S])
869     next
870       assume "C \<noteq> {}"
871       with C(2) have "S \<subseteq> \<Union>C"
872         by auto
873       moreover have "independent (\<Union>C)"
874         by (intro independent_Union_directed C)
875       moreover have "\<Union>C \<subseteq> V"
876         using C by auto
877       ultimately show ?thesis
878         by auto
879     qed
880   qed
881   then obtain B where B: "independent B" "B \<subseteq> V" "S \<subseteq> B"
882     and max: "\<And>S. independent S \<Longrightarrow> S \<subseteq> V \<Longrightarrow> B \<subseteq> S \<Longrightarrow> S = B"
883     by auto
884   moreover
885   { assume "\<not> V \<subseteq> span B"
886     then obtain v where "v \<in> V" "v \<notin> span B"
887       by auto
888     with B have "independent (insert v B)"
889       unfolding independent_insert by auto
890     from max[OF this] \<open>v \<in> V\<close> \<open>B \<subseteq> V\<close>
891     have "v \<in> B"
892       by auto
893     with \<open>v \<notin> span B\<close> have False
894       by (auto intro: span_superset) }
895   ultimately show ?thesis
896     by (auto intro!: exI[of _ B])
897 qed
900 lemma maximal_independent_subset:
901   "\<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
902   by (metis maximal_independent_subset_extend[of "{}"] empty_subsetI independent_empty)
904 lemma span_finite:
905   assumes fS: "finite S"
906   shows "span S = {y. \<exists>u. setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
907   (is "_ = ?rhs")
908 proof -
909   {
910     fix y
911     assume y: "y \<in> span S"
912     from y obtain S' u where fS': "finite S'"
913       and SS': "S' \<subseteq> S"
914       and u: "setsum (\<lambda>v. u v *\<^sub>R v) S' = y"
915       unfolding span_explicit by blast
916     let ?u = "\<lambda>x. if x \<in> S' then u x else 0"
917     have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = setsum (\<lambda>v. u v *\<^sub>R v) S'"
918       using SS' fS by (auto intro!: setsum.mono_neutral_cong_right)
919     then have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = y" by (metis u)
920     then have "y \<in> ?rhs" by auto
921   }
922   moreover
923   {
924     fix y u
925     assume u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y"
926     then have "y \<in> span S" using fS unfolding span_explicit by auto
927   }
928   ultimately show ?thesis by blast
929 qed
931 lemma linear_independent_extend_subspace:
932   assumes "independent B"
933   shows "\<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x) \<and> range g = span (f`B)"
934 proof -
935   from maximal_independent_subset_extend[OF _ \<open>independent B\<close>, of UNIV]
936   obtain B' where "B \<subseteq> B'" "independent B'" "span B' = UNIV"
937     by (auto simp: top_unique)
938   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)"
939     using \<open>span B' = UNIV\<close> unfolding span_alt by auto
940   then obtain X where X: "\<And>y. {x. X y x \<noteq> 0} \<subseteq> B'" "\<And>y. finite {x. X y x \<noteq> 0}"
941     "\<And>y. y = (\<Sum>x|X y x \<noteq> 0. X y x *\<^sub>R x)"
942     unfolding choice_iff by auto
944   have X_add: "X (x + y) = (\<lambda>z. X x z + X y z)" for x y
945     using \<open>independent B'\<close>
946   proof (rule independentD_unique)
947     have "(\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R z)
948       = (\<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)"
949       by (intro setsum.mono_neutral_cong_left) (auto intro: X)
950     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)"
952                intro!: arg_cong2[where f="op +"]  setsum.mono_neutral_cong_right X)
953     also have "\<dots> = x + y"
955     also have "\<dots> = (\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z)"
956       by (rule X(3))
957     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)"
958       ..
959     have "{z. X x z + X y z \<noteq> 0} \<subseteq> {z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}"
960       by auto
961     then show "finite {z. X x z + X y z \<noteq> 0}" "{xa. X x xa + X y xa \<noteq> 0} \<subseteq> B'"
962         "finite {xa. X (x + y) xa \<noteq> 0}" "{xa. X (x + y) xa \<noteq> 0} \<subseteq> B'"
963       using X(1) by (auto dest: finite_subset intro: X)
964   qed
966   have X_cmult: "X (c *\<^sub>R x) = (\<lambda>z. c * X x z)" for x c
967     using \<open>independent B'\<close>
968   proof (rule independentD_unique)
969     show "finite {z. X (c *\<^sub>R x) z \<noteq> 0}" "{z. X (c *\<^sub>R x) z \<noteq> 0} \<subseteq> B'"
970       "finite {z. c * X x z \<noteq> 0}" "{z. c * X x z \<noteq> 0} \<subseteq> B' "
971       using X(1,2) by auto
972     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)"
973       unfolding scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric]
974       by (cases "c = 0") (auto simp: X(3)[symmetric])
975   qed
977   have X_B': "x \<in> B' \<Longrightarrow> X x = (\<lambda>z. if z = x then 1 else 0)" for x
978     using \<open>independent B'\<close>
979     by (rule independentD_unique[OF _ X(2) X(1)]) (auto intro: X simp: X(3)[symmetric])
981   define f' where "f' y = (if y \<in> B then f y else 0)" for y
982   define g where "g y = (\<Sum>x|X y x \<noteq> 0. X y x *\<^sub>R f' x)" for y
984   have g_f': "x \<in> B' \<Longrightarrow> g x = f' x" for x
985     by (auto simp: g_def X_B')
987   have "linear g"
988   proof
989     fix x y
990     have *: "(\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R f' z)
991       = (\<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)"
992       by (intro setsum.mono_neutral_cong_left) (auto intro: X)
993     show "g (x + y) = g x + g y"
996                intro!: arg_cong2[where f="op +"]  setsum.mono_neutral_cong_right X)
997   next
998     show "g (r *\<^sub>R x) = r *\<^sub>R g x" for r x
999       by (auto simp add: g_def X_cmult scaleR_setsum_right intro!: setsum.mono_neutral_cong_left X)
1000   qed
1001   moreover have "\<forall>x\<in>B. g x = f x"
1002     using \<open>B \<subseteq> B'\<close> by (auto simp: g_f' f'_def)
1003   moreover have "range g = span (f`B)"
1004     unfolding \<open>span B' = UNIV\<close>[symmetric] span_linear_image[OF \<open>linear g\<close>, symmetric]
1005   proof (rule span_subspace)
1006     have "g ` B' \<subseteq> f`B \<union> {0}"
1007       by (auto simp: g_f' f'_def)
1008     also have "\<dots> \<subseteq> span (f`B)"
1009       by (auto intro: span_superset span_0)
1010     finally show "g ` B' \<subseteq> span (f`B)"
1011       by auto
1012     have "x \<in> B \<Longrightarrow> f x = g x" for x
1013       using \<open>B \<subseteq> B'\<close> by (auto simp add: g_f' f'_def)
1014     then show "span (f ` B) \<subseteq> span (g ` B')"
1015       using \<open>B \<subseteq> B'\<close> by (intro span_mono) auto
1016   qed (rule subspace_span)
1017   ultimately show ?thesis
1018     by auto
1019 qed
1021 lemma linear_independent_extend:
1022   "independent B \<Longrightarrow> \<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x)"
1023   using linear_independent_extend_subspace[of B f] by auto
1025 text \<open>Linear functions are equal on a subspace if they are on a spanning set.\<close>
1027 lemma subspace_kernel:
1028   assumes lf: "linear f"
1029   shows "subspace {x. f x = 0}"
1032   done
1034 lemma linear_eq_0_span:
1035   assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
1036   shows "\<forall>x \<in> span B. f x = 0"
1037   using f0 subspace_kernel[OF lf]
1038   by (rule span_induct')
1040 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"
1041   using linear_eq_0_span[of f B] by auto
1043 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"
1044   using linear_eq_0_span[of "\<lambda>x. f x - g x" B] by (auto simp: linear_compose_sub)
1046 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"
1047   using linear_eq_span[of f g B] by auto
1049 text \<open>The degenerate case of the Exchange Lemma.\<close>
1051 lemma spanning_subset_independent:
1052   assumes BA: "B \<subseteq> A"
1053     and iA: "independent A"
1054     and AsB: "A \<subseteq> span B"
1055   shows "A = B"
1056 proof
1057   show "B \<subseteq> A" by (rule BA)
1059   from span_mono[OF BA] span_mono[OF AsB]
1060   have sAB: "span A = span B" unfolding span_span by blast
1062   {
1063     fix x
1064     assume x: "x \<in> A"
1065     from iA have th0: "x \<notin> span (A - {x})"
1066       unfolding dependent_def using x by blast
1067     from x have xsA: "x \<in> span A"
1068       by (blast intro: span_superset)
1069     have "A - {x} \<subseteq> A" by blast
1070     then have th1: "span (A - {x}) \<subseteq> span A"
1071       by (metis span_mono)
1072     {
1073       assume xB: "x \<notin> B"
1074       from xB BA have "B \<subseteq> A - {x}"
1075         by blast
1076       then have "span B \<subseteq> span (A - {x})"
1077         by (metis span_mono)
1078       with th1 th0 sAB have "x \<notin> span A"
1079         by blast
1080       with x have False
1081         by (metis span_superset)
1082     }
1083     then have "x \<in> B" by blast
1084   }
1085   then show "A \<subseteq> B" by blast
1086 qed
1088 text \<open>Relation between bases and injectivity/surjectivity of map.\<close>
1090 lemma spanning_surjective_image:
1091   assumes us: "UNIV \<subseteq> span S"
1092     and lf: "linear f"
1093     and sf: "surj f"
1094   shows "UNIV \<subseteq> span (f ` S)"
1095 proof -
1096   have "UNIV \<subseteq> f ` UNIV"
1097     using sf by (auto simp add: surj_def)
1098   also have " \<dots> \<subseteq> span (f ` S)"
1099     using spans_image[OF lf us] .
1100   finally show ?thesis .
1101 qed
1103 lemma independent_inj_on_image:
1104   assumes iS: "independent S"
1105     and lf: "linear f"
1106     and fi: "inj_on f (span S)"
1107   shows "independent (f ` S)"
1108 proof -
1109   {
1110     fix a
1111     assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
1112     have eq: "f ` S - {f a} = f ` (S - {a})"
1113       using fi \<open>a\<in>S\<close> by (auto simp add: inj_on_def span_superset)
1114     from a have "f a \<in> f ` span (S - {a})"
1115       unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
1116     then have "a \<in> span (S - {a})"
1117       by (rule inj_on_image_mem_iff_alt[OF fi, rotated])
1118          (insert span_mono[of "S - {a}" S], auto intro: span_superset \<open>a\<in>S\<close>)
1119     with a(1) iS have False
1121   }
1122   then show ?thesis
1123     unfolding dependent_def by blast
1124 qed
1126 lemma independent_injective_image:
1127   "independent S \<Longrightarrow> linear f \<Longrightarrow> inj f \<Longrightarrow> independent (f ` S)"
1128   using independent_inj_on_image[of S f] by (auto simp: subset_inj_on)
1130 text \<open>Detailed theorems about left and right invertibility in general case.\<close>
1132 lemma linear_inj_on_left_inverse:
1133   assumes lf: "linear f" and fi: "inj_on f (span S)"
1134   shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span S. g (f x) = x)"
1135 proof -
1136   obtain B where "independent B" "B \<subseteq> S" "S \<subseteq> span B"
1137     using maximal_independent_subset[of S] by auto
1138   then have "span S = span B"
1139     unfolding span_eq by (auto simp: span_superset)
1140   with linear_independent_extend_subspace[OF independent_inj_on_image, OF \<open>independent B\<close> lf] fi
1141   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)"
1142     by fastforce
1143   have fB: "inj_on f B"
1144     using fi by (auto simp: \<open>span S = span B\<close> intro: subset_inj_on span_superset)
1146   have "\<forall>x\<in>span B. g (f x) = x"
1147   proof (intro linear_eq_span)
1148     show "linear (\<lambda>x. x)" "linear (\<lambda>x. g (f x))"
1149       using linear_id linear_compose[OF \<open>linear f\<close> \<open>linear g\<close>] by (auto simp: id_def comp_def)
1150     show "\<forall>x \<in> B. g (f x) = x"
1151       using g fi \<open>span S = span B\<close> by (auto simp: fB)
1152   qed
1153   moreover
1154   have "inv_into B f ` f ` B \<subseteq> B"
1155     by (auto simp: fB)
1156   then have "range g \<subseteq> span S"
1157     unfolding g \<open>span S = span B\<close> by (intro span_mono)
1158   ultimately show ?thesis
1159     using \<open>span S = span B\<close> \<open>linear g\<close> by auto
1160 qed
1162 lemma linear_injective_left_inverse: "linear f \<Longrightarrow> inj f \<Longrightarrow> \<exists>g. linear g \<and> g \<circ> f = id"
1163   using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff span_UNIV)
1165 lemma linear_surj_right_inverse:
1166   assumes lf: "linear f" and sf: "span T \<subseteq> f`span S"
1167   shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span T. f (g x) = x)"
1168 proof -
1169   obtain B where "independent B" "B \<subseteq> T" "T \<subseteq> span B"
1170     using maximal_independent_subset[of T] by auto
1171   then have "span T = span B"
1172     unfolding span_eq by (auto simp: span_superset)
1174   from linear_independent_extend_subspace[OF \<open>independent B\<close>, of "inv_into (span S) f"]
1175   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)"
1176     by auto
1177   moreover have "x \<in> B \<Longrightarrow> f (inv_into (span S) f x) = x" for x
1178     using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (intro f_inv_into_f) (auto intro: span_superset)
1179   ultimately have "\<forall>x\<in>B. f (g x) = x"
1180     by auto
1181   then have "\<forall>x\<in>span B. f (g x) = x"
1182     using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>]
1183     by (intro linear_eq_span) (auto simp: id_def comp_def)
1184   moreover have "inv_into (span S) f ` B \<subseteq> span S"
1185     using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (auto intro: inv_into_into span_superset)
1186   then have "range g \<subseteq> span S"
1187     unfolding g by (intro span_minimal subspace_span) auto
1188   ultimately show ?thesis
1189     using \<open>linear g\<close> \<open>span T = span B\<close> by auto
1190 qed
1192 lemma linear_surjective_right_inverse: "linear f \<Longrightarrow> surj f \<Longrightarrow> \<exists>g. linear g \<and> f \<circ> g = id"
1193   using linear_surj_right_inverse[of f UNIV UNIV]
1194   by (auto simp: span_UNIV fun_eq_iff)
1196 text \<open>The general case of the Exchange Lemma, the key to what follows.\<close>
1198 lemma exchange_lemma:
1199   assumes f:"finite t"
1200     and i: "independent s"
1201     and sp: "s \<subseteq> span t"
1202   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'"
1203   using f i sp
1204 proof (induct "card (t - s)" arbitrary: s t rule: less_induct)
1205   case less
1206   note ft = \<open>finite t\<close> and s = \<open>independent s\<close> and sp = \<open>s \<subseteq> span t\<close>
1207   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'"
1208   let ?ths = "\<exists>t'. ?P t'"
1209   {
1210     assume "s \<subseteq> t"
1211     then have ?ths
1212       by (metis ft Un_commute sp sup_ge1)
1213   }
1214   moreover
1215   {
1216     assume st: "t \<subseteq> s"
1217     from spanning_subset_independent[OF st s sp] st ft span_mono[OF st]
1218     have ?ths
1219       by (metis Un_absorb sp)
1220   }
1221   moreover
1222   {
1223     assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
1224     from st(2) obtain b where b: "b \<in> t" "b \<notin> s"
1225       by blast
1226     from b have "t - {b} - s \<subset> t - s"
1227       by blast
1228     then have cardlt: "card (t - {b} - s) < card (t - s)"
1229       using ft by (auto intro: psubset_card_mono)
1230     from b ft have ct0: "card t \<noteq> 0"
1231       by auto
1232     have ?ths
1233     proof cases
1234       assume stb: "s \<subseteq> span (t - {b})"
1235       from ft have ftb: "finite (t - {b})"
1236         by auto
1237       from less(1)[OF cardlt ftb s stb]
1238       obtain u where u: "card u = card (t - {b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u"
1239         and fu: "finite u" by blast
1240       let ?w = "insert b u"
1241       have th0: "s \<subseteq> insert b u"
1242         using u by blast
1243       from u(3) b have "u \<subseteq> s \<union> t"
1244         by blast
1245       then have th1: "insert b u \<subseteq> s \<union> t"
1246         using u b by blast
1247       have bu: "b \<notin> u"
1248         using b u by blast
1249       from u(1) ft b have "card u = (card t - 1)"
1250         by auto
1251       then have th2: "card (insert b u) = card t"
1252         using card_insert_disjoint[OF fu bu] ct0 by auto
1253       from u(4) have "s \<subseteq> span u" .
1254       also have "\<dots> \<subseteq> span (insert b u)"
1255         by (rule span_mono) blast
1256       finally have th3: "s \<subseteq> span (insert b u)" .
1257       from th0 th1 th2 th3 fu have th: "?P ?w"
1258         by blast
1259       from th show ?thesis by blast
1260     next
1261       assume stb: "\<not> s \<subseteq> span (t - {b})"
1262       from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})"
1263         by blast
1264       have ab: "a \<noteq> b"
1265         using a b by blast
1266       have at: "a \<notin> t"
1267         using a ab span_superset[of a "t- {b}"] by auto
1268       have mlt: "card ((insert a (t - {b})) - s) < card (t - s)"
1269         using cardlt ft a b by auto
1270       have ft': "finite (insert a (t - {b}))"
1271         using ft by auto
1272       {
1273         fix x
1274         assume xs: "x \<in> s"
1275         have t: "t \<subseteq> insert b (insert a (t - {b}))"
1276           using b by auto
1277         from b(1) have "b \<in> span t"
1279         have bs: "b \<in> span (insert a (t - {b}))"
1280           apply (rule in_span_delete)
1281           using a sp unfolding subset_eq
1282           apply auto
1283           done
1284         from xs sp have "x \<in> span t"
1285           by blast
1286         with span_mono[OF t] have x: "x \<in> span (insert b (insert a (t - {b})))" ..
1287         from span_trans[OF bs x] have "x \<in> span (insert a (t - {b}))" .
1288       }
1289       then have sp': "s \<subseteq> span (insert a (t - {b}))"
1290         by blast
1291       from less(1)[OF mlt ft' s sp'] obtain u where u:
1292         "card u = card (insert a (t - {b}))"
1293         "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t - {b})"
1294         "s \<subseteq> span u" by blast
1295       from u a b ft at ct0 have "?P u"
1296         by auto
1297       then show ?thesis by blast
1298     qed
1299   }
1300   ultimately show ?ths by blast
1301 qed
1303 text \<open>This implies corresponding size bounds.\<close>
1305 lemma independent_span_bound:
1306   assumes f: "finite t"
1307     and i: "independent s"
1308     and sp: "s \<subseteq> span t"
1309   shows "finite s \<and> card s \<le> card t"
1310   by (metis exchange_lemma[OF f i sp] finite_subset card_mono)
1312 lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
1313 proof -
1314   have eq: "{f x |x. x\<in> UNIV} = f ` UNIV"
1315     by auto
1316   show ?thesis unfolding eq
1317     apply (rule finite_imageI)
1318     apply (rule finite)
1319     done
1320 qed
1323 subsection \<open>More interesting properties of the norm.\<close>
1325 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
1326   by auto
1328 notation inner (infix "\<bullet>" 70)
1330 lemma square_bound_lemma:
1331   fixes x :: real
1332   shows "x < (1 + x) * (1 + x)"
1333 proof -
1334   have "(x + 1/2)\<^sup>2 + 3/4 > 0"
1335     using zero_le_power2[of "x+1/2"] by arith
1336   then show ?thesis
1337     by (simp add: field_simps power2_eq_square)
1338 qed
1340 lemma square_continuous:
1341   fixes e :: real
1342   shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)"
1343   using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
1344   by (force simp add: power2_eq_square)
1347 lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
1348   by simp (* TODO: delete *)
1350 lemma norm_triangle_sub:
1351   fixes x y :: "'a::real_normed_vector"
1352   shows "norm x \<le> norm y + norm (x - y)"
1353   using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
1355 lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> x \<bullet> x \<le> y \<bullet> y"
1358 lemma norm_lt: "norm x < norm y \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
1361 lemma norm_eq: "norm x = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
1362   apply (subst order_eq_iff)
1363   apply (auto simp: norm_le)
1364   done
1366 lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> x \<bullet> x = 1"
1369 text\<open>Squaring equations and inequalities involving norms.\<close>
1371 lemma dot_square_norm: "x \<bullet> x = (norm x)\<^sup>2"
1372   by (simp only: power2_norm_eq_inner) (* TODO: move? *)
1374 lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x = a\<^sup>2"
1375   by (auto simp add: norm_eq_sqrt_inner)
1377 lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x \<le> a\<^sup>2"
1378   apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
1379   using norm_ge_zero[of x]
1380   apply arith
1381   done
1383 lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> x \<bullet> x \<ge> a\<^sup>2"
1384   apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
1385   using norm_ge_zero[of x]
1386   apply arith
1387   done
1389 lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
1390   by (metis not_le norm_ge_square)
1392 lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
1393   by (metis norm_le_square not_less)
1395 text\<open>Dot product in terms of the norm rather than conversely.\<close>
1398   inner_scaleR_left inner_scaleR_right
1400 lemma dot_norm: "x \<bullet> y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
1401   by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
1403 lemma dot_norm_neg: "x \<bullet> y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
1404   by (simp only: power2_norm_eq_inner inner_simps inner_commute)
1407 text\<open>Equality of vectors in terms of @{term "op \<bullet>"} products.\<close>
1409 lemma linear_componentwise:
1410   fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
1411   assumes lf: "linear f"
1412   shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
1413 proof -
1414   have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
1416   then show ?thesis
1417     unfolding linear_setsum_mul[OF lf, symmetric]
1418     unfolding euclidean_representation ..
1419 qed
1421 lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x"
1422   (is "?lhs \<longleftrightarrow> ?rhs")
1423 proof
1424   assume ?lhs
1425   then show ?rhs by simp
1426 next
1427   assume ?rhs
1428   then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0"
1429     by simp
1430   then have "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0"
1431     by (simp add: inner_diff inner_commute)
1432   then have "(x - y) \<bullet> (x - y) = 0"
1433     by (simp add: field_simps inner_diff inner_commute)
1434   then show "x = y" by simp
1435 qed
1437 lemma norm_triangle_half_r:
1438   "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
1439   using dist_triangle_half_r unfolding dist_norm[symmetric] by auto
1441 lemma norm_triangle_half_l:
1442   assumes "norm (x - y) < e / 2"
1443     and "norm (x' - y) < e / 2"
1444   shows "norm (x - x') < e"
1445   using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
1446   unfolding dist_norm[symmetric] .
1448 lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
1449   by (rule norm_triangle_ineq [THEN order_trans])
1451 lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
1452   by (rule norm_triangle_ineq [THEN le_less_trans])
1454 lemma setsum_clauses:
1455   shows "setsum f {} = 0"
1456     and "finite S \<Longrightarrow> setsum f (insert x S) = (if x \<in> S then setsum f S else f x + setsum f S)"
1457   by (auto simp add: insert_absorb)
1459 lemma setsum_norm_le:
1460   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1461   assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
1462   shows "norm (setsum f S) \<le> setsum g S"
1463   by (rule order_trans [OF norm_setsum setsum_mono]) (simp add: fg)
1465 lemma setsum_norm_bound:
1466   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1467   assumes K: "\<forall>x \<in> S. norm (f x) \<le> K"
1468   shows "norm (setsum f S) \<le> of_nat (card S) * K"
1469   using setsum_norm_le[OF K] setsum_constant[symmetric]
1470   by simp
1472 lemma setsum_group:
1473   assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
1474   shows "setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) T = setsum g S"
1475   apply (subst setsum_image_gen[OF fS, of g f])
1476   apply (rule setsum.mono_neutral_right[OF fT fST])
1477   apply (auto intro: setsum.neutral)
1478   done
1480 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
1481 proof
1482   assume "\<forall>x. x \<bullet> y = x \<bullet> z"
1483   then have "\<forall>x. x \<bullet> (y - z) = 0"
1485   then have "(y - z) \<bullet> (y - z) = 0" ..
1486   then show "y = z" by simp
1487 qed simp
1489 lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"
1490 proof
1491   assume "\<forall>z. x \<bullet> z = y \<bullet> z"
1492   then have "\<forall>z. (x - y) \<bullet> z = 0"
1494   then have "(x - y) \<bullet> (x - y) = 0" ..
1495   then show "x = y" by simp
1496 qed simp
1499 subsection \<open>Orthogonality.\<close>
1501 context real_inner
1502 begin
1504 definition "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
1506 lemma orthogonal_self: "orthogonal x x \<longleftrightarrow> x = 0"
1509 lemma orthogonal_clauses:
1510   "orthogonal a 0"
1511   "orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"
1512   "orthogonal a x \<Longrightarrow> orthogonal a (- x)"
1513   "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)"
1514   "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x - y)"
1515   "orthogonal 0 a"
1516   "orthogonal x a \<Longrightarrow> orthogonal (c *\<^sub>R x) a"
1517   "orthogonal x a \<Longrightarrow> orthogonal (- x) a"
1518   "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
1519   "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
1520   unfolding orthogonal_def inner_add inner_diff by auto
1522 end
1524 lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
1525   by (simp add: orthogonal_def inner_commute)
1527 lemma orthogonal_scaleR [simp]: "c \<noteq> 0 \<Longrightarrow> orthogonal (c *\<^sub>R x) = orthogonal x"
1528   by (rule ext) (simp add: orthogonal_def)
1530 lemma pairwise_ortho_scaleR:
1531     "pairwise (\<lambda>i j. orthogonal (f i) (g j)) B
1532     \<Longrightarrow> pairwise (\<lambda>i j. orthogonal (a i *\<^sub>R f i) (a j *\<^sub>R g j)) B"
1533   by (auto simp: pairwise_def orthogonal_clauses)
1535 lemma orthogonal_rvsum:
1536     "\<lbrakk>finite s; \<And>y. y \<in> s \<Longrightarrow> orthogonal x (f y)\<rbrakk> \<Longrightarrow> orthogonal x (setsum f s)"
1537   by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
1539 lemma orthogonal_lvsum:
1540     "\<lbrakk>finite s; \<And>x. x \<in> s \<Longrightarrow> orthogonal (f x) y\<rbrakk> \<Longrightarrow> orthogonal (setsum f s) y"
1541   by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
1544   assumes "orthogonal a b"
1545     shows "norm(a + b) ^ 2 = norm a ^ 2 + norm b ^ 2"
1546 proof -
1547   from assms have "(a - (0 - b)) \<bullet> (a - (0 - b)) = a \<bullet> a - (0 - b \<bullet> b)"
1548     by (simp add: algebra_simps orthogonal_def inner_commute)
1549   then show ?thesis
1551 qed
1553 lemma norm_setsum_Pythagorean:
1554   assumes "finite I" "pairwise (\<lambda>i j. orthogonal (f i) (f j)) I"
1555     shows "(norm (setsum f I))\<^sup>2 = (\<Sum>i\<in>I. (norm (f i))\<^sup>2)"
1556 using assms
1557 proof (induction I rule: finite_induct)
1558   case empty then show ?case by simp
1559 next
1560   case (insert x I)
1561   then have "orthogonal (f x) (setsum f I)"
1562     by (metis pairwise_insert orthogonal_rvsum)
1563   with insert show ?case
1565 qed
1568 subsection \<open>Bilinear functions.\<close>
1570 definition "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
1572 lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
1573   by (simp add: bilinear_def linear_iff)
1575 lemma bilinear_radd: "bilinear h \<Longrightarrow> h x (y + z) = h x y + h x z"
1576   by (simp add: bilinear_def linear_iff)
1578 lemma bilinear_lmul: "bilinear h \<Longrightarrow> h (c *\<^sub>R x) y = c *\<^sub>R h x y"
1579   by (simp add: bilinear_def linear_iff)
1581 lemma bilinear_rmul: "bilinear h \<Longrightarrow> h x (c *\<^sub>R y) = c *\<^sub>R h x y"
1582   by (simp add: bilinear_def linear_iff)
1584 lemma bilinear_lneg: "bilinear h \<Longrightarrow> h (- x) y = - h x y"
1585   by (drule bilinear_lmul [of _ "- 1"]) simp
1587 lemma bilinear_rneg: "bilinear h \<Longrightarrow> h x (- y) = - h x y"
1588   by (drule bilinear_rmul [of _ _ "- 1"]) simp
1590 lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
1591   using add_left_imp_eq[of x y 0] by auto
1593 lemma bilinear_lzero:
1594   assumes "bilinear h"
1595   shows "h 0 x = 0"
1598 lemma bilinear_rzero:
1599   assumes "bilinear h"
1600   shows "h x 0 = 0"
1603 lemma bilinear_lsub: "bilinear h \<Longrightarrow> h (x - y) z = h x z - h y z"
1604   using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg)
1606 lemma bilinear_rsub: "bilinear h \<Longrightarrow> h z (x - y) = h z x - h z y"
1607   using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)
1609 lemma bilinear_setsum:
1610   assumes bh: "bilinear h"
1611     and fS: "finite S"
1612     and fT: "finite T"
1613   shows "h (setsum f S) (setsum g T) = setsum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
1614 proof -
1615   have "h (setsum f S) (setsum g T) = setsum (\<lambda>x. h (f x) (setsum g T)) S"
1616     apply (rule linear_setsum[unfolded o_def])
1617     using bh fS
1618     apply (auto simp add: bilinear_def)
1619     done
1620   also have "\<dots> = setsum (\<lambda>x. setsum (\<lambda>y. h (f x) (g y)) T) S"
1621     apply (rule setsum.cong, simp)
1622     apply (rule linear_setsum[unfolded o_def])
1623     using bh fT
1624     apply (auto simp add: bilinear_def)
1625     done
1626   finally show ?thesis
1627     unfolding setsum.cartesian_product .
1628 qed
1633 definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
1636   assumes "\<forall>x y. inner (f x) y = inner x (g y)"
1637   shows "adjoint f = g"
1639 proof (rule some_equality)
1640   show "\<forall>x y. inner (f x) y = inner x (g y)"
1641     by (rule assms)
1642 next
1643   fix h
1644   assume "\<forall>x y. inner (f x) y = inner x (h y)"
1645   then have "\<forall>x y. inner x (g y) = inner x (h y)"
1646     using assms by simp
1647   then have "\<forall>x y. inner x (g y - h y) = 0"
1649   then have "\<forall>y. inner (g y - h y) (g y - h y) = 0"
1650     by simp
1651   then have "\<forall>y. h y = g y"
1652     by simp
1653   then show "h = g" by (simp add: ext)
1654 qed
1656 text \<open>TODO: The following lemmas about adjoints should hold for any
1657   Hilbert space (i.e. complete inner product space).
1659 \<close>
1662   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
1663   assumes lf: "linear f"
1664   shows "x \<bullet> adjoint f y = f x \<bullet> y"
1665 proof -
1666   have "\<forall>y. \<exists>w. \<forall>x. f x \<bullet> y = x \<bullet> w"
1667   proof (intro allI exI)
1668     fix y :: "'m" and x
1669     let ?w = "(\<Sum>i\<in>Basis. (f i \<bullet> y) *\<^sub>R i) :: 'n"
1670     have "f x \<bullet> y = f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i) \<bullet> y"
1672     also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<bullet> y"
1673       unfolding linear_setsum[OF lf]
1674       by (simp add: linear_cmul[OF lf])
1675     finally show "f x \<bullet> y = x \<bullet> ?w"
1676       by (simp add: inner_setsum_left inner_setsum_right mult.commute)
1677   qed
1678   then show ?thesis
1680     by (intro someI2_ex[where Q="\<lambda>f'. x \<bullet> f' y = f x \<bullet> y"]) auto
1681 qed
1684   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
1685   assumes lf: "linear f"
1686   shows "x \<bullet> adjoint f y = f x \<bullet> y"
1687     and "adjoint f y \<bullet> x = y \<bullet> f x"
1691   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
1692   assumes lf: "linear f"
1694   by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
1698   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
1699   assumes lf: "linear f"
1704 subsection \<open>Interlude: Some properties of real sets\<close>
1706 lemma seq_mono_lemma:
1707   assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
1708     and "\<forall>n \<ge> m. e n \<le> e m"
1709   shows "\<forall>n \<ge> m. d n < e m"
1710   using assms
1711   apply auto
1712   apply (erule_tac x="n" in allE)
1713   apply (erule_tac x="n" in allE)
1714   apply auto
1715   done
1717 lemma infinite_enumerate:
1718   assumes fS: "infinite S"
1719   shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
1720   unfolding subseq_def
1721   using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
1723 lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
1724   apply auto
1725   apply (rule_tac x="d/2" in exI)
1726   apply auto
1727   done
1729 lemma approachable_lt_le2:  \<comment>\<open>like the above, but pushes aside an extra formula\<close>
1730     "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
1731   apply auto
1732   apply (rule_tac x="d/2" in exI, auto)
1733   done
1735 lemma triangle_lemma:
1736   fixes x y z :: real
1737   assumes x: "0 \<le> x"
1738     and y: "0 \<le> y"
1739     and z: "0 \<le> z"
1740     and xy: "x\<^sup>2 \<le> y\<^sup>2 + z\<^sup>2"
1741   shows "x \<le> y + z"
1742 proof -
1743   have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
1744     using z y by simp
1745   with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
1746     by (simp add: power2_eq_square field_simps)
1747   from y z have yz: "y + z \<ge> 0"
1748     by arith
1749   from power2_le_imp_le[OF th yz] show ?thesis .
1750 qed
1754 subsection \<open>Archimedean properties and useful consequences\<close>
1756 text\<open>Bernoulli's inequality\<close>
1757 proposition Bernoulli_inequality:
1758   fixes x :: real
1759   assumes "-1 \<le> x"
1760     shows "1 + n * x \<le> (1 + x) ^ n"
1761 proof (induct n)
1762   case 0
1763   then show ?case by simp
1764 next
1765   case (Suc n)
1766   have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
1768   also have "... = (1 + x) * (1 + n*x)"
1769     by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
1770   also have "... \<le> (1 + x) ^ Suc n"
1771     using Suc.hyps assms mult_left_mono by fastforce
1772   finally show ?case .
1773 qed
1775 corollary Bernoulli_inequality_even:
1776   fixes x :: real
1777   assumes "even n"
1778     shows "1 + n * x \<le> (1 + x) ^ n"
1779 proof (cases "-1 \<le> x \<or> n=0")
1780   case True
1781   then show ?thesis
1782     by (auto simp: Bernoulli_inequality)
1783 next
1784   case False
1785   then have "real n \<ge> 1"
1786     by simp
1787   with False have "n * x \<le> -1"
1788     by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
1789   then have "1 + n * x \<le> 0"
1790     by auto
1791   also have "... \<le> (1 + x) ^ n"
1792     using assms
1793     using zero_le_even_power by blast
1794   finally show ?thesis .
1795 qed
1797 corollary real_arch_pow:
1798   fixes x :: real
1799   assumes x: "1 < x"
1800   shows "\<exists>n. y < x^n"
1801 proof -
1802   from x have x0: "x - 1 > 0"
1803     by arith
1804   from reals_Archimedean3[OF x0, rule_format, of y]
1805   obtain n :: nat where n: "y < real n * (x - 1)" by metis
1806   from x0 have x00: "x- 1 \<ge> -1" by arith
1807   from Bernoulli_inequality[OF x00, of n] n
1808   have "y < x^n" by auto
1809   then show ?thesis by metis
1810 qed
1812 corollary real_arch_pow_inv:
1813   fixes x y :: real
1814   assumes y: "y > 0"
1815     and x1: "x < 1"
1816   shows "\<exists>n. x^n < y"
1817 proof (cases "x > 0")
1818   case True
1819   with x1 have ix: "1 < 1/x" by (simp add: field_simps)
1820   from real_arch_pow[OF ix, of "1/y"]
1821   obtain n where n: "1/y < (1/x)^n" by blast
1822   then show ?thesis using y \<open>x > 0\<close>
1823     by (auto simp add: field_simps)
1824 next
1825   case False
1826   with y x1 show ?thesis
1827     apply auto
1828     apply (rule exI[where x=1])
1829     apply auto
1830     done
1831 qed
1833 lemma forall_pos_mono:
1834   "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
1835     (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
1836   by (metis real_arch_inverse)
1838 lemma forall_pos_mono_1:
1839   "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
1840     (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
1841   apply (rule forall_pos_mono)
1842   apply auto
1843   apply (metis Suc_pred of_nat_Suc)
1844   done
1847 subsection \<open>Euclidean Spaces as Typeclass\<close>
1849 lemma independent_Basis: "independent Basis"
1850   unfolding dependent_def
1851   apply (subst span_finite)
1852   apply simp
1853   apply clarify
1854   apply (drule_tac f="inner a" in arg_cong)
1855   apply (simp add: inner_Basis inner_setsum_right eq_commute)
1856   done
1858 lemma span_Basis [simp]: "span Basis = UNIV"
1859   unfolding span_finite [OF finite_Basis]
1860   by (fast intro: euclidean_representation)
1862 lemma in_span_Basis: "x \<in> span Basis"
1863   unfolding span_Basis ..
1865 lemma Basis_le_norm: "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> norm x"
1866   by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
1868 lemma norm_bound_Basis_le: "b \<in> Basis \<Longrightarrow> norm x \<le> e \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> e"
1869   by (metis Basis_le_norm order_trans)
1871 lemma norm_bound_Basis_lt: "b \<in> Basis \<Longrightarrow> norm x < e \<Longrightarrow> \<bar>x \<bullet> b\<bar> < e"
1872   by (metis Basis_le_norm le_less_trans)
1874 lemma norm_le_l1: "norm x \<le> (\<Sum>b\<in>Basis. \<bar>x \<bullet> b\<bar>)"
1875   apply (subst euclidean_representation[of x, symmetric])
1876   apply (rule order_trans[OF norm_setsum])
1877   apply (auto intro!: setsum_mono)
1878   done
1880 lemma setsum_norm_allsubsets_bound:
1881   fixes f :: "'a \<Rightarrow> 'n::euclidean_space"
1882   assumes fP: "finite P"
1883     and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
1884   shows "(\<Sum>x\<in>P. norm (f x)) \<le> 2 * real DIM('n) * e"
1885 proof -
1886   have "(\<Sum>x\<in>P. norm (f x)) \<le> (\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>)"
1887     by (rule setsum_mono) (rule norm_le_l1)
1888   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>)"
1889     by (rule setsum.commute)
1890   also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
1891   proof (rule setsum_bounded_above)
1892     fix i :: 'n
1893     assume i: "i \<in> Basis"
1894     have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
1895       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)"
1896       by (simp add: abs_real_def setsum.If_cases[OF fP] setsum_negf norm_triangle_ineq4 inner_setsum_left
1897         del: real_norm_def)
1898     also have "\<dots> \<le> e + e"
1899       unfolding real_norm_def
1900       by (intro add_mono norm_bound_Basis_le i fPs) auto
1901     finally show "(\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le> 2*e" by simp
1902   qed
1903   also have "\<dots> = 2 * real DIM('n) * e" by simp
1904   finally show ?thesis .
1905 qed
1908 subsection \<open>Linearity and Bilinearity continued\<close>
1910 lemma linear_bounded:
1911   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1912   assumes lf: "linear f"
1913   shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
1914 proof
1915   let ?B = "\<Sum>b\<in>Basis. norm (f b)"
1916   show "\<forall>x. norm (f x) \<le> ?B * norm x"
1917   proof
1918     fix x :: 'a
1919     let ?g = "\<lambda>b. (x \<bullet> b) *\<^sub>R f b"
1920     have "norm (f x) = norm (f (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b))"
1921       unfolding euclidean_representation ..
1922     also have "\<dots> = norm (setsum ?g Basis)"
1923       by (simp add: linear_setsum [OF lf] linear_cmul [OF lf])
1924     finally have th0: "norm (f x) = norm (setsum ?g Basis)" .
1925     have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x"
1926     proof
1927       fix i :: 'a
1928       assume i: "i \<in> Basis"
1929       from Basis_le_norm[OF i, of x]
1930       show "norm (?g i) \<le> norm (f i) * norm x"
1931         unfolding norm_scaleR
1932         apply (subst mult.commute)
1933         apply (rule mult_mono)
1934         apply (auto simp add: field_simps)
1935         done
1936     qed
1937     from setsum_norm_le[of _ ?g, OF th]
1938     show "norm (f x) \<le> ?B * norm x"
1939       unfolding th0 setsum_left_distrib by metis
1940   qed
1941 qed
1943 lemma linear_conv_bounded_linear:
1944   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1945   shows "linear f \<longleftrightarrow> bounded_linear f"
1946 proof
1947   assume "linear f"
1948   then interpret f: linear f .
1949   show "bounded_linear f"
1950   proof
1951     have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
1952       using \<open>linear f\<close> by (rule linear_bounded)
1953     then show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
1955   qed
1956 next
1957   assume "bounded_linear f"
1958   then interpret f: bounded_linear f .
1959   show "linear f" ..
1960 qed
1962 lemmas linear_linear = linear_conv_bounded_linear[symmetric]
1964 lemma linear_bounded_pos:
1965   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1966   assumes lf: "linear f"
1967   shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
1968 proof -
1969   have "\<exists>B > 0. \<forall>x. norm (f x) \<le> norm x * B"
1970     using lf unfolding linear_conv_bounded_linear
1971     by (rule bounded_linear.pos_bounded)
1972   then show ?thesis
1973     by (simp only: mult.commute)
1974 qed
1976 lemma bounded_linearI':
1977   fixes f ::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1978   assumes "\<And>x y. f (x + y) = f x + f y"
1979     and "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
1980   shows "bounded_linear f"
1981   unfolding linear_conv_bounded_linear[symmetric]
1982   by (rule linearI[OF assms])
1984 lemma bilinear_bounded:
1985   fixes h :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
1986   assumes bh: "bilinear h"
1987   shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
1988 proof (clarify intro!: exI[of _ "\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)"])
1989   fix x :: 'm
1990   fix y :: 'n
1991   have "norm (h x y) = norm (h (setsum (\<lambda>i. (x \<bullet> i) *\<^sub>R i) Basis) (setsum (\<lambda>i. (y \<bullet> i) *\<^sub>R i) Basis))"
1992     apply (subst euclidean_representation[where 'a='m])
1993     apply (subst euclidean_representation[where 'a='n])
1994     apply rule
1995     done
1996   also have "\<dots> = norm (setsum (\<lambda> (i,j). h ((x \<bullet> i) *\<^sub>R i) ((y \<bullet> j) *\<^sub>R j)) (Basis \<times> Basis))"
1997     unfolding bilinear_setsum[OF bh finite_Basis finite_Basis] ..
1998   finally have th: "norm (h x y) = \<dots>" .
1999   show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
2000     apply (auto simp add: setsum_left_distrib th setsum.cartesian_product)
2001     apply (rule setsum_norm_le)
2002     apply simp
2003     apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
2004       field_simps simp del: scaleR_scaleR)
2005     apply (rule mult_mono)
2006     apply (auto simp add: zero_le_mult_iff Basis_le_norm)
2007     apply (rule mult_mono)
2008     apply (auto simp add: zero_le_mult_iff Basis_le_norm)
2009     done
2010 qed
2012 lemma bilinear_conv_bounded_bilinear:
2013   fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
2014   shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
2015 proof
2016   assume "bilinear h"
2017   show "bounded_bilinear h"
2018   proof
2019     fix x y z
2020     show "h (x + y) z = h x z + h y z"
2021       using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
2022   next
2023     fix x y z
2024     show "h x (y + z) = h x y + h x z"
2025       using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
2026   next
2027     fix r x y
2028     show "h (scaleR r x) y = scaleR r (h x y)"
2029       using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
2030       by simp
2031   next
2032     fix r x y
2033     show "h x (scaleR r y) = scaleR r (h x y)"
2034       using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
2035       by simp
2036   next
2037     have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
2038       using \<open>bilinear h\<close> by (rule bilinear_bounded)
2039     then show "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
2041   qed
2042 next
2043   assume "bounded_bilinear h"
2044   then interpret h: bounded_bilinear h .
2045   show "bilinear h"
2046     unfolding bilinear_def linear_conv_bounded_linear
2047     using h.bounded_linear_left h.bounded_linear_right by simp
2048 qed
2050 lemma bilinear_bounded_pos:
2051   fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
2052   assumes bh: "bilinear h"
2053   shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
2054 proof -
2055   have "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> norm x * norm y * B"
2056     using bh [unfolded bilinear_conv_bounded_bilinear]
2057     by (rule bounded_bilinear.pos_bounded)
2058   then show ?thesis
2059     by (simp only: ac_simps)
2060 qed
2062 lemma bounded_linear_imp_has_derivative:
2063      "bounded_linear f \<Longrightarrow> (f has_derivative f) net"
2064   by (simp add: has_derivative_def bounded_linear.linear linear_diff)
2066 lemma linear_imp_has_derivative:
2067   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
2068   shows "linear f \<Longrightarrow> (f has_derivative f) net"
2069 by (simp add: has_derivative_def linear_conv_bounded_linear linear_diff)
2071 lemma bounded_linear_imp_differentiable: "bounded_linear f \<Longrightarrow> f differentiable net"
2072   using bounded_linear_imp_has_derivative differentiable_def by blast
2074 lemma linear_imp_differentiable:
2075   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
2076   shows "linear f \<Longrightarrow> f differentiable net"
2077 by (metis linear_imp_has_derivative differentiable_def)
2080 subsection \<open>We continue.\<close>
2082 lemma independent_bound:
2083   fixes S :: "'a::euclidean_space set"
2084   shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a)"
2085   using independent_span_bound[OF finite_Basis, of S] by auto
2087 corollary
2088   fixes S :: "'a::euclidean_space set"
2089   assumes "independent S"
2090   shows independent_imp_finite: "finite S" and independent_card_le:"card S \<le> DIM('a)"
2091 using assms independent_bound by auto
2093 lemma independent_explicit:
2094   fixes B :: "'a::euclidean_space set"
2095   shows "independent B \<longleftrightarrow>
2096          finite B \<and> (\<forall>c. (\<Sum>v\<in>B. c v *\<^sub>R v) = 0 \<longrightarrow> (\<forall>v \<in> B. c v = 0))"
2097 apply (cases "finite B")
2098  apply (force simp: dependent_finite)
2099 using independent_bound
2100 apply auto
2101 done
2103 lemma dependent_biggerset:
2104   fixes S :: "'a::euclidean_space set"
2105   shows "(finite S \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
2106   by (metis independent_bound not_less)
2108 text \<open>Notion of dimension.\<close>
2110 definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> card B = n)"
2112 lemma basis_exists:
2113   "\<exists>B. (B :: ('a::euclidean_space) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = dim V)"
2114   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)"]
2115   using maximal_independent_subset[of V] independent_bound
2116   by auto
2118 corollary dim_le_card:
2119   fixes s :: "'a::euclidean_space set"
2120   shows "finite s \<Longrightarrow> dim s \<le> card s"
2121 by (metis basis_exists card_mono)
2123 text \<open>Consequences of independence or spanning for cardinality.\<close>
2125 lemma independent_card_le_dim:
2126   fixes B :: "'a::euclidean_space set"
2127   assumes "B \<subseteq> V"
2128     and "independent B"
2129   shows "card B \<le> dim V"
2130 proof -
2131   from basis_exists[of V] \<open>B \<subseteq> V\<close>
2132   obtain B' where "independent B'"
2133     and "B \<subseteq> span B'"
2134     and "card B' = dim V"
2135     by blast
2136   with independent_span_bound[OF _ \<open>independent B\<close> \<open>B \<subseteq> span B'\<close>] independent_bound[of B']
2137   show ?thesis by auto
2138 qed
2140 lemma span_card_ge_dim:
2141   fixes B :: "'a::euclidean_space set"
2142   shows "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> finite B \<Longrightarrow> dim V \<le> card B"
2143   by (metis basis_exists[of V] independent_span_bound subset_trans)
2145 lemma basis_card_eq_dim:
2146   fixes V :: "'a::euclidean_space set"
2147   shows "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B = dim V"
2148   by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_bound)
2150 lemma dim_unique:
2151   fixes B :: "'a::euclidean_space set"
2152   shows "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = n \<Longrightarrow> dim V = n"
2153   by (metis basis_card_eq_dim)
2155 text \<open>More lemmas about dimension.\<close>
2157 lemma dim_UNIV: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
2158   using independent_Basis
2159   by (intro dim_unique[of Basis]) auto
2161 lemma dim_subset:
2162   fixes S :: "'a::euclidean_space set"
2163   shows "S \<subseteq> T \<Longrightarrow> dim S \<le> dim T"
2164   using basis_exists[of T] basis_exists[of S]
2165   by (metis independent_card_le_dim subset_trans)
2167 lemma dim_subset_UNIV:
2168   fixes S :: "'a::euclidean_space set"
2169   shows "dim S \<le> DIM('a)"
2170   by (metis dim_subset subset_UNIV dim_UNIV)
2172 text \<open>Converses to those.\<close>
2174 lemma card_ge_dim_independent:
2175   fixes B :: "'a::euclidean_space set"
2176   assumes BV: "B \<subseteq> V"
2177     and iB: "independent B"
2178     and dVB: "dim V \<le> card B"
2179   shows "V \<subseteq> span B"
2180 proof
2181   fix a
2182   assume aV: "a \<in> V"
2183   {
2184     assume aB: "a \<notin> span B"
2185     then have iaB: "independent (insert a B)"
2186       using iB aV BV by (simp add: independent_insert)
2187     from aV BV have th0: "insert a B \<subseteq> V"
2188       by blast
2189     from aB have "a \<notin>B"
2190       by (auto simp add: span_superset)
2191     with independent_card_le_dim[OF th0 iaB] dVB independent_bound[OF iB]
2192     have False by auto
2193   }
2194   then show "a \<in> span B" by blast
2195 qed
2197 lemma card_le_dim_spanning:
2198   assumes BV: "(B:: ('a::euclidean_space) set) \<subseteq> V"
2199     and VB: "V \<subseteq> span B"
2200     and fB: "finite B"
2201     and dVB: "dim V \<ge> card B"
2202   shows "independent B"
2203 proof -
2204   {
2205     fix a
2206     assume a: "a \<in> B" "a \<in> span (B - {a})"
2207     from a fB have c0: "card B \<noteq> 0"
2208       by auto
2209     from a fB have cb: "card (B - {a}) = card B - 1"
2210       by auto
2211     from BV a have th0: "B - {a} \<subseteq> V"
2212       by blast
2213     {
2214       fix x
2215       assume x: "x \<in> V"
2216       from a have eq: "insert a (B - {a}) = B"
2217         by blast
2218       from x VB have x': "x \<in> span B"
2219         by blast
2220       from span_trans[OF a(2), unfolded eq, OF x']
2221       have "x \<in> span (B - {a})" .
2222     }
2223     then have th1: "V \<subseteq> span (B - {a})"
2224       by blast
2225     have th2: "finite (B - {a})"
2226       using fB by auto
2227     from span_card_ge_dim[OF th0 th1 th2]
2228     have c: "dim V \<le> card (B - {a})" .
2229     from c c0 dVB cb have False by simp
2230   }
2231   then show ?thesis
2232     unfolding dependent_def by blast
2233 qed
2235 lemma card_eq_dim:
2236   fixes B :: "'a::euclidean_space set"
2237   shows "B \<subseteq> V \<Longrightarrow> card B = dim V \<Longrightarrow> finite B \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B"
2238   by (metis order_eq_iff card_le_dim_spanning card_ge_dim_independent)
2240 text \<open>More general size bound lemmas.\<close>
2242 lemma independent_bound_general:
2243   fixes S :: "'a::euclidean_space set"
2244   shows "independent S \<Longrightarrow> finite S \<and> card S \<le> dim S"
2245   by (metis independent_card_le_dim independent_bound subset_refl)
2247 lemma dependent_biggerset_general:
2248   fixes S :: "'a::euclidean_space set"
2249   shows "(finite S \<Longrightarrow> card S > dim S) \<Longrightarrow> dependent S"
2250   using independent_bound_general[of S] by (metis linorder_not_le)
2252 lemma dim_span [simp]:
2253   fixes S :: "'a::euclidean_space set"
2254   shows "dim (span S) = dim S"
2255 proof -
2256   have th0: "dim S \<le> dim (span S)"
2257     by (auto simp add: subset_eq intro: dim_subset span_superset)
2258   from basis_exists[of S]
2259   obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
2260     by blast
2261   from B have fB: "finite B" "card B = dim S"
2262     using independent_bound by blast+
2263   have bSS: "B \<subseteq> span S"
2264     using B(1) by (metis subset_eq span_inc)
2265   have sssB: "span S \<subseteq> span B"
2266     using span_mono[OF B(3)] by (simp add: span_span)
2267   from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis
2268     using fB(2) by arith
2269 qed
2271 lemma subset_le_dim:
2272   fixes S :: "'a::euclidean_space set"
2273   shows "S \<subseteq> span T \<Longrightarrow> dim S \<le> dim T"
2274   by (metis dim_span dim_subset)
2276 lemma span_eq_dim:
2277   fixes S :: "'a::euclidean_space set"
2278   shows "span S = span T \<Longrightarrow> dim S = dim T"
2279   by (metis dim_span)
2281 lemma dim_image_le:
2282   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
2283   assumes lf: "linear f"
2284   shows "dim (f ` S) \<le> dim (S)"
2285 proof -
2286   from basis_exists[of S] obtain B where
2287     B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" by blast
2288   from B have fB: "finite B" "card B = dim S"
2289     using independent_bound by blast+
2290   have "dim (f ` S) \<le> card (f ` B)"
2291     apply (rule span_card_ge_dim)
2292     using lf B fB
2293     apply (auto simp add: span_linear_image spans_image subset_image_iff)
2294     done
2295   also have "\<dots> \<le> dim S"
2296     using card_image_le[OF fB(1)] fB by simp
2297   finally show ?thesis .
2298 qed
2300 text \<open>Picking an orthogonal replacement for a spanning set.\<close>
2302 lemma vector_sub_project_orthogonal:
2303   fixes b x :: "'a::euclidean_space"
2304   shows "b \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *\<^sub>R b) = 0"
2305   unfolding inner_simps by auto
2307 lemma pairwise_orthogonal_insert:
2308   assumes "pairwise orthogonal S"
2309     and "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
2310   shows "pairwise orthogonal (insert x S)"
2311   using assms unfolding pairwise_def
2312   by (auto simp add: orthogonal_commute)
2314 lemma basis_orthogonal:
2315   fixes B :: "'a::real_inner set"
2316   assumes fB: "finite B"
2317   shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"
2318   (is " \<exists>C. ?P B C")
2319   using fB
2320 proof (induct rule: finite_induct)
2321   case empty
2322   then show ?case
2323     apply (rule exI[where x="{}"])
2324     apply (auto simp add: pairwise_def)
2325     done
2326 next
2327   case (insert a B)
2328   note fB = \<open>finite B\<close> and aB = \<open>a \<notin> B\<close>
2329   from \<open>\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C\<close>
2330   obtain C where C: "finite C" "card C \<le> card B"
2331     "span C = span B" "pairwise orthogonal C" by blast
2332   let ?a = "a - setsum (\<lambda>x. (x \<bullet> a / (x \<bullet> x)) *\<^sub>R x) C"
2333   let ?C = "insert ?a C"
2334   from C(1) have fC: "finite ?C"
2335     by simp
2336   from fB aB C(1,2) have cC: "card ?C \<le> card (insert a B)"
2338   {
2339     fix x k
2340     have th0: "\<And>(a::'a) b c. a - (b - c) = c + (a - b)"
2342     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"
2343       apply (simp only: scaleR_right_diff_distrib th0)
2345       apply (rule span_mul)
2346       apply (rule span_setsum)
2347       apply (rule span_mul)
2348       apply (rule span_superset)
2349       apply assumption
2350       done
2351   }
2352   then have SC: "span ?C = span (insert a B)"
2353     unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto
2354   {
2355     fix y
2356     assume yC: "y \<in> C"
2357     then have Cy: "C = insert y (C - {y})"
2358       by blast
2359     have fth: "finite (C - {y})"
2360       using C by simp
2361     have "orthogonal ?a y"
2362       unfolding orthogonal_def
2363       unfolding inner_diff inner_setsum_left right_minus_eq
2364       unfolding setsum.remove [OF \<open>finite C\<close> \<open>y \<in> C\<close>]
2365       apply (clarsimp simp add: inner_commute[of y a])
2366       apply (rule setsum.neutral)
2367       apply clarsimp
2368       apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
2369       using \<open>y \<in> C\<close> by auto
2370   }
2371   with \<open>pairwise orthogonal C\<close> have CPO: "pairwise orthogonal ?C"
2372     by (rule pairwise_orthogonal_insert)
2373   from fC cC SC CPO have "?P (insert a B) ?C"
2374     by blast
2375   then show ?case by blast
2376 qed
2378 lemma orthogonal_basis_exists:
2379   fixes V :: "('a::euclidean_space) set"
2380   shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and> (card B = dim V) \<and> pairwise orthogonal B"
2381 proof -
2382   from basis_exists[of V] obtain B where
2383     B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V"
2384     by blast
2385   from B have fB: "finite B" "card B = dim V"
2386     using independent_bound by auto
2387   from basis_orthogonal[OF fB(1)] obtain C where
2388     C: "finite C" "card C \<le> card B" "span C = span B" "pairwise orthogonal C"
2389     by blast
2390   from C B have CSV: "C \<subseteq> span V"
2391     by (metis span_inc span_mono subset_trans)
2392   from span_mono[OF B(3)] C have SVC: "span V \<subseteq> span C"
2394   from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB
2395   have iC: "independent C"
2397   from C fB have "card C \<le> dim V"
2398     by simp
2399   moreover have "dim V \<le> card C"
2400     using span_card_ge_dim[OF CSV SVC C(1)]
2402   ultimately have CdV: "card C = dim V"
2403     using C(1) by simp
2404   from C B CSV CdV iC show ?thesis
2405     by auto
2406 qed
2408 text \<open>Low-dimensional subset is in a hyperplane (weak orthogonal complement).\<close>
2410 lemma span_not_univ_orthogonal:
2411   fixes S :: "'a::euclidean_space set"
2412   assumes sU: "span S \<noteq> UNIV"
2413   shows "\<exists>a::'a. a \<noteq> 0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"
2414 proof -
2415   from sU obtain a where a: "a \<notin> span S"
2416     by blast
2417   from orthogonal_basis_exists obtain B where
2418     B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B" "card B = dim S" "pairwise orthogonal B"
2419     by blast
2420   from B have fB: "finite B" "card B = dim S"
2421     using independent_bound by auto
2422   from span_mono[OF B(2)] span_mono[OF B(3)]
2423   have sSB: "span S = span B"
2425   let ?a = "a - setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B"
2426   have "setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> span S"
2427     unfolding sSB
2428     apply (rule span_setsum)
2429     apply (rule span_mul)
2430     apply (rule span_superset)
2431     apply assumption
2432     done
2433   with a have a0:"?a  \<noteq> 0"
2434     by auto
2435   have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
2436   proof (rule span_induct')
2437     show "subspace {x. ?a \<bullet> x = 0}"
2439   next
2440     {
2441       fix x
2442       assume x: "x \<in> B"
2443       from x have B': "B = insert x (B - {x})"
2444         by blast
2445       have fth: "finite (B - {x})"
2446         using fB by simp
2447       have "?a \<bullet> x = 0"
2448         apply (subst B')
2449         using fB fth
2450         unfolding setsum_clauses(2)[OF fth]
2451         apply simp unfolding inner_simps
2453         apply (rule setsum.neutral, rule ballI)
2454         apply (simp only: inner_commute)
2455         apply (auto simp add: x field_simps
2456           intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
2457         done
2458     }
2459     then show "\<forall>x \<in> B. ?a \<bullet> x = 0"
2460       by blast
2461   qed
2462   with a0 show ?thesis
2463     unfolding sSB by (auto intro: exI[where x="?a"])
2464 qed
2466 lemma span_not_univ_subset_hyperplane:
2467   fixes S :: "'a::euclidean_space set"
2468   assumes SU: "span S \<noteq> UNIV"
2469   shows "\<exists> a. a \<noteq>0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
2470   using span_not_univ_orthogonal[OF SU] by auto
2472 lemma lowdim_subset_hyperplane:
2473   fixes S :: "'a::euclidean_space set"
2474   assumes d: "dim S < DIM('a)"
2475   shows "\<exists>a::'a. a \<noteq> 0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
2476 proof -
2477   {
2478     assume "span S = UNIV"
2479     then have "dim (span S) = dim (UNIV :: ('a) set)"
2480       by simp
2481     then have "dim S = DIM('a)"
2482       by (simp add: dim_span dim_UNIV)
2483     with d have False by arith
2484   }
2485   then have th: "span S \<noteq> UNIV"
2486     by blast
2487   from span_not_univ_subset_hyperplane[OF th] show ?thesis .
2488 qed
2490 text \<open>We can extend a linear basis-basis injection to the whole set.\<close>
2492 lemma linear_indep_image_lemma:
2493   assumes lf: "linear f"
2494     and fB: "finite B"
2495     and ifB: "independent (f ` B)"
2496     and fi: "inj_on f B"
2497     and xsB: "x \<in> span B"
2498     and fx: "f x = 0"
2499   shows "x = 0"
2500   using fB ifB fi xsB fx
2501 proof (induct arbitrary: x rule: finite_induct[OF fB])
2502   case 1
2503   then show ?case by auto
2504 next
2505   case (2 a b x)
2506   have fb: "finite b" using "2.prems" by simp
2507   have th0: "f ` b \<subseteq> f ` (insert a b)"
2508     apply (rule image_mono)
2509     apply blast
2510     done
2511   from independent_mono[ OF "2.prems"(2) th0]
2512   have ifb: "independent (f ` b)"  .
2513   have fib: "inj_on f b"
2514     apply (rule subset_inj_on [OF "2.prems"(3)])
2515     apply blast
2516     done
2517   from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)]
2518   obtain k where k: "x - k*\<^sub>R a \<in> span (b - {a})"
2519     by blast
2520   have "f (x - k*\<^sub>R a) \<in> span (f ` b)"
2521     unfolding span_linear_image[OF lf]
2522     apply (rule imageI)
2523     using k span_mono[of "b - {a}" b]
2524     apply blast
2525     done
2526   then have "f x - k*\<^sub>R f a \<in> span (f ` b)"
2527     by (simp add: linear_diff[OF lf] linear_cmul[OF lf])
2528   then have th: "-k *\<^sub>R f a \<in> span (f ` b)"
2529     using "2.prems"(5) by simp
2530   have xsb: "x \<in> span b"
2531   proof (cases "k = 0")
2532     case True
2533     with k have "x \<in> span (b - {a})" by simp
2534     then show ?thesis using span_mono[of "b - {a}" b]
2535       by blast
2536   next
2537     case False
2538     with span_mul[OF th, of "- 1/ k"]
2539     have th1: "f a \<in> span (f ` b)"
2540       by auto
2541     from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
2542     have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
2543     from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
2544     have "f a \<notin> span (f ` b)" using tha
2545       using "2.hyps"(2)
2546       "2.prems"(3) by auto
2547     with th1 have False by blast
2548     then show ?thesis by blast
2549   qed
2550   from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] show "x = 0" .
2551 qed
2553 text \<open>Can construct an isomorphism between spaces of same dimension.\<close>
2555 lemma subspace_isomorphism:
2556   fixes S :: "'a::euclidean_space set"
2557     and T :: "'b::euclidean_space set"
2558   assumes s: "subspace S"
2559     and t: "subspace T"
2560     and d: "dim S = dim T"
2561   shows "\<exists>f. linear f \<and> f ` S = T \<and> inj_on f S"
2562 proof -
2563   from basis_exists[of S] independent_bound
2564   obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" and fB: "finite B"
2565     by blast
2566   from basis_exists[of T] independent_bound
2567   obtain C where C: "C \<subseteq> T" "independent C" "T \<subseteq> span C" "card C = dim T" and fC: "finite C"
2568     by blast
2569   from B(4) C(4) card_le_inj[of B C] d
2570   obtain f where f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close>
2571     by auto
2572   from linear_independent_extend[OF B(2)]
2573   obtain g where g: "linear g" "\<forall>x\<in> B. g x = f x"
2574     by blast
2575   from inj_on_iff_eq_card[OF fB, of f] f(2) have "card (f ` B) = card B"
2576     by simp
2577   with B(4) C(4) have ceq: "card (f ` B) = card C"
2578     using d by simp
2579   have "g ` B = f ` B"
2580     using g(2) by (auto simp add: image_iff)
2581   also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] .
2582   finally have gBC: "g ` B = C" .
2583   have gi: "inj_on g B"
2584     using f(2) g(2) by (auto simp add: inj_on_def)
2585   note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
2586   {
2587     fix x y
2588     assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y"
2589     from B(3) x y have x': "x \<in> span B" and y': "y \<in> span B"
2590       by blast+
2591     from gxy have th0: "g (x - y) = 0"
2592       by (simp add: linear_diff[OF g(1)])
2593     have th1: "x - y \<in> span B"
2594       using x' y' by (metis span_sub)
2595     have "x = y"
2596       using g0[OF th1 th0] by simp
2597   }
2598   then have giS: "inj_on g S"
2599     unfolding inj_on_def by blast
2600   from span_subspace[OF B(1,3) s] have "g ` S = span (g ` B)"
2601     by (simp add: span_linear_image[OF g(1)])
2602   also have "\<dots> = span C" unfolding gBC ..
2603   also have "\<dots> = T" using span_subspace[OF C(1,3) t] .
2604   finally have gS: "g ` S = T" .
2605   from g(1) gS giS show ?thesis
2606     by blast
2607 qed
2609 lemma linear_eq_stdbasis:
2610   fixes f :: "'a::euclidean_space \<Rightarrow> _"
2611   assumes lf: "linear f"
2612     and lg: "linear g"
2613     and fg: "\<forall>b\<in>Basis. f b = g b"
2614   shows "f = g"
2615   using linear_eq[OF lf lg, of _ Basis] fg by auto
2617 text \<open>Similar results for bilinear functions.\<close>
2619 lemma bilinear_eq:
2620   assumes bf: "bilinear f"
2621     and bg: "bilinear g"
2622     and SB: "S \<subseteq> span B"
2623     and TC: "T \<subseteq> span C"
2624     and fg: "\<forall>x\<in> B. \<forall>y\<in> C. f x y = g x y"
2625   shows "\<forall>x\<in>S. \<forall>y\<in>T. f x y = g x y "
2626 proof -
2627   let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
2628   from bf bg have sp: "subspace ?P"
2629     unfolding bilinear_def linear_iff subspace_def bf bg
2630     by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
2633   have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
2634     apply (rule span_induct' [OF _ sp])
2635     apply (rule ballI)
2636     apply (rule span_induct')
2638     apply (auto simp add: subspace_def)
2639     using bf bg unfolding bilinear_def linear_iff
2640     apply (auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def
2642     done
2643   then show ?thesis
2644     using SB TC by auto
2645 qed
2647 lemma bilinear_eq_stdbasis:
2648   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> _"
2649   assumes bf: "bilinear f"
2650     and bg: "bilinear g"
2651     and fg: "\<forall>i\<in>Basis. \<forall>j\<in>Basis. f i j = g i j"
2652   shows "f = g"
2653   using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
2655 text \<open>An injective map @{typ "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"} is also surjective.\<close>
2657 lemma linear_injective_imp_surjective:
2658   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
2659   assumes lf: "linear f"
2660     and fi: "inj f"
2661   shows "surj f"
2662 proof -
2663   let ?U = "UNIV :: 'a set"
2664   from basis_exists[of ?U] obtain B
2665     where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" "card B = dim ?U"
2666     by blast
2667   from B(4) have d: "dim ?U = card B"
2668     by simp
2669   have th: "?U \<subseteq> span (f ` B)"
2670     apply (rule card_ge_dim_independent)
2671     apply blast
2672     apply (rule independent_injective_image[OF B(2) lf fi])
2673     apply (rule order_eq_refl)
2674     apply (rule sym)
2675     unfolding d
2676     apply (rule card_image)
2677     apply (rule subset_inj_on[OF fi])
2678     apply blast
2679     done
2680   from th show ?thesis
2681     unfolding span_linear_image[OF lf] surj_def
2682     using B(3) by blast
2683 qed
2685 text \<open>And vice versa.\<close>
2687 lemma surjective_iff_injective_gen:
2688   assumes fS: "finite S"
2689     and fT: "finite T"
2690     and c: "card S = card T"
2691     and ST: "f ` S \<subseteq> T"
2692   shows "(\<forall>y \<in> T. \<exists>x \<in> S. f x = y) \<longleftrightarrow> inj_on f S"
2693   (is "?lhs \<longleftrightarrow> ?rhs")
2694 proof
2695   assume h: "?lhs"
2696   {
2697     fix x y
2698     assume x: "x \<in> S"
2699     assume y: "y \<in> S"
2700     assume f: "f x = f y"
2701     from x fS have S0: "card S \<noteq> 0"
2702       by auto
2703     have "x = y"
2704     proof (rule ccontr)
2705       assume xy: "\<not> ?thesis"
2706       have th: "card S \<le> card (f ` (S - {y}))"
2707         unfolding c
2708         apply (rule card_mono)
2709         apply (rule finite_imageI)
2710         using fS apply simp
2711         using h xy x y f unfolding subset_eq image_iff
2712         apply auto
2713         apply (case_tac "xa = f x")
2714         apply (rule bexI[where x=x])
2715         apply auto
2716         done
2717       also have " \<dots> \<le> card (S - {y})"
2718         apply (rule card_image_le)
2719         using fS by simp
2720       also have "\<dots> \<le> card S - 1" using y fS by simp
2721       finally show False using S0 by arith
2722     qed
2723   }
2724   then show ?rhs
2725     unfolding inj_on_def by blast
2726 next
2727   assume h: ?rhs
2728   have "f ` S = T"
2729     apply (rule card_subset_eq[OF fT ST])
2730     unfolding card_image[OF h]
2731     apply (rule c)
2732     done
2733   then show ?lhs by blast
2734 qed
2736 lemma linear_surjective_imp_injective:
2737   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
2738   assumes lf: "linear f"
2739     and sf: "surj f"
2740   shows "inj f"
2741 proof -
2742   let ?U = "UNIV :: 'a set"
2743   from basis_exists[of ?U] obtain B
2744     where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" and d: "card B = dim ?U"
2745     by blast
2746   {
2747     fix x
2748     assume x: "x \<in> span B"
2749     assume fx: "f x = 0"
2750     from B(2) have fB: "finite B"
2751       using independent_bound by auto
2752     have fBi: "independent (f ` B)"
2753       apply (rule card_le_dim_spanning[of "f ` B" ?U])
2754       apply blast
2755       using sf B(3)
2756       unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
2757       apply blast
2758       using fB apply blast
2759       unfolding d[symmetric]
2760       apply (rule card_image_le)
2761       apply (rule fB)
2762       done
2763     have th0: "dim ?U \<le> card (f ` B)"
2764       apply (rule span_card_ge_dim)
2765       apply blast
2766       unfolding span_linear_image[OF lf]
2767       apply (rule subset_trans[where B = "f ` UNIV"])
2768       using sf unfolding surj_def
2769       apply blast
2770       apply (rule image_mono)
2771       apply (rule B(3))
2772       apply (metis finite_imageI fB)
2773       done
2774     moreover have "card (f ` B) \<le> card B"
2775       by (rule card_image_le, rule fB)
2776     ultimately have th1: "card B = card (f ` B)"
2777       unfolding d by arith
2778     have fiB: "inj_on f B"
2779       unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric]
2780       by blast
2781     from linear_indep_image_lemma[OF lf fB fBi fiB x] fx
2782     have "x = 0" by blast
2783   }
2784   then show ?thesis
2785     unfolding linear_injective_0[OF lf]
2786     using B(3)
2787     by blast
2788 qed
2790 text \<open>Hence either is enough for isomorphism.\<close>
2792 lemma left_right_inverse_eq:
2793   assumes fg: "f \<circ> g = id"
2794     and gh: "g \<circ> h = id"
2795   shows "f = h"
2796 proof -
2797   have "f = f \<circ> (g \<circ> h)"
2798     unfolding gh by simp
2799   also have "\<dots> = (f \<circ> g) \<circ> h"
2801   finally show "f = h"
2802     unfolding fg by simp
2803 qed
2805 lemma isomorphism_expand:
2806   "f \<circ> g = id \<and> g \<circ> f = id \<longleftrightarrow> (\<forall>x. f (g x) = x) \<and> (\<forall>x. g (f x) = x)"
2807   by (simp add: fun_eq_iff o_def id_def)
2809 lemma linear_injective_isomorphism:
2810   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
2811   assumes lf: "linear f"
2812     and fi: "inj f"
2813   shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
2814   unfolding isomorphism_expand[symmetric]
2815   using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]]
2816     linear_injective_left_inverse[OF lf fi]
2817   by (metis left_right_inverse_eq)
2819 lemma linear_surjective_isomorphism:
2820   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
2821   assumes lf: "linear f"
2822     and sf: "surj f"
2823   shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
2824   unfolding isomorphism_expand[symmetric]
2825   using linear_surjective_right_inverse[OF lf sf]
2826     linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]]
2827   by (metis left_right_inverse_eq)
2829 text \<open>Left and right inverses are the same for
2830   @{typ "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"}.\<close>
2832 lemma linear_inverse_left:
2833   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
2834   assumes lf: "linear f"
2835     and lf': "linear f'"
2836   shows "f \<circ> f' = id \<longleftrightarrow> f' \<circ> f = id"
2837 proof -
2838   {
2839     fix f f':: "'a \<Rightarrow> 'a"
2840     assume lf: "linear f" "linear f'"
2841     assume f: "f \<circ> f' = id"
2842     from f have sf: "surj f"
2843       apply (auto simp add: o_def id_def surj_def)
2844       apply metis
2845       done
2846     from linear_surjective_isomorphism[OF lf(1) sf] lf f
2847     have "f' \<circ> f = id"
2848       unfolding fun_eq_iff o_def id_def by metis
2849   }
2850   then show ?thesis
2851     using lf lf' by metis
2852 qed
2854 text \<open>Moreover, a one-sided inverse is automatically linear.\<close>
2856 lemma left_inverse_linear:
2857   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
2858   assumes lf: "linear f"
2859     and gf: "g \<circ> f = id"
2860   shows "linear g"
2861 proof -
2862   from gf have fi: "inj f"
2863     apply (auto simp add: inj_on_def o_def id_def fun_eq_iff)
2864     apply metis
2865     done
2866   from linear_injective_isomorphism[OF lf fi]
2867   obtain h :: "'a \<Rightarrow> 'a" where h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
2868     by blast
2869   have "h = g"
2870     apply (rule ext) using gf h(2,3)
2871     apply (simp add: o_def id_def fun_eq_iff)
2872     apply metis
2873     done
2874   with h(1) show ?thesis by blast
2875 qed
2877 lemma inj_linear_imp_inv_linear:
2878   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
2879   assumes "linear f" "inj f" shows "linear (inv f)"
2880 using assms inj_iff left_inverse_linear by blast
2883 subsection \<open>Infinity norm\<close>
2885 definition "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
2887 lemma infnorm_set_image:
2888   fixes x :: "'a::euclidean_space"
2889   shows "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis} = (\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
2890   by blast
2892 lemma infnorm_Max:
2893   fixes x :: "'a::euclidean_space"
2894   shows "infnorm x = Max ((\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis)"
2895   by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
2897 lemma infnorm_set_lemma:
2898   fixes x :: "'a::euclidean_space"
2899   shows "finite {\<bar>x \<bullet> i\<bar> |i. i \<in> Basis}"
2900     and "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis} \<noteq> {}"
2901   unfolding infnorm_set_image
2902   by auto
2904 lemma infnorm_pos_le:
2905   fixes x :: "'a::euclidean_space"
2906   shows "0 \<le> infnorm x"
2907   by (simp add: infnorm_Max Max_ge_iff ex_in_conv)
2909 lemma infnorm_triangle:
2910   fixes x :: "'a::euclidean_space"
2911   shows "infnorm (x + y) \<le> infnorm x + infnorm y"
2912 proof -
2913   have *: "\<And>a b c d :: real. \<bar>a\<bar> \<le> c \<Longrightarrow> \<bar>b\<bar> \<le> d \<Longrightarrow> \<bar>a + b\<bar> \<le> c + d"
2914     by simp
2915   show ?thesis
2916     by (auto simp: infnorm_Max inner_add_left intro!: *)
2917 qed
2919 lemma infnorm_eq_0:
2920   fixes x :: "'a::euclidean_space"
2921   shows "infnorm x = 0 \<longleftrightarrow> x = 0"
2922 proof -
2923   have "infnorm x \<le> 0 \<longleftrightarrow> x = 0"
2924     unfolding infnorm_Max by (simp add: euclidean_all_zero_iff)
2925   then show ?thesis
2926     using infnorm_pos_le[of x] by simp
2927 qed
2929 lemma infnorm_0: "infnorm 0 = 0"
2932 lemma infnorm_neg: "infnorm (- x) = infnorm x"
2933   unfolding infnorm_def
2934   apply (rule cong[of "Sup" "Sup"])
2935   apply blast
2936   apply auto
2937   done
2939 lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
2940 proof -
2941   have "y - x = - (x - y)" by simp
2942   then show ?thesis
2943     by (metis infnorm_neg)
2944 qed
2946 lemma real_abs_sub_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
2947 proof -
2948   have th: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
2949     by arith
2950   from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
2951   have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
2952     "infnorm y \<le> infnorm (x - y) + infnorm x"
2953     by (simp_all add: field_simps infnorm_neg)
2954   from th[OF ths] show ?thesis .
2955 qed
2957 lemma real_abs_infnorm: "\<bar>infnorm x\<bar> = infnorm x"
2958   using infnorm_pos_le[of x] by arith
2960 lemma Basis_le_infnorm:
2961   fixes x :: "'a::euclidean_space"
2962   shows "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> infnorm x"
2965 lemma infnorm_mul: "infnorm (a *\<^sub>R x) = \<bar>a\<bar> * infnorm x"
2966   unfolding infnorm_Max
2967 proof (safe intro!: Max_eqI)
2968   let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
2969   {
2970     fix b :: 'a
2971     assume "b \<in> Basis"
2972     then show "\<bar>a *\<^sub>R x \<bullet> b\<bar> \<le> \<bar>a\<bar> * Max ?B"
2973       by (simp add: abs_mult mult_left_mono)
2974   next
2975     from Max_in[of ?B] obtain b where "b \<in> Basis" "Max ?B = \<bar>x \<bullet> b\<bar>"
2976       by (auto simp del: Max_in)
2977     then show "\<bar>a\<bar> * Max ((\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis) \<in> (\<lambda>i. \<bar>a *\<^sub>R x \<bullet> i\<bar>) ` Basis"
2978       by (intro image_eqI[where x=b]) (auto simp: abs_mult)
2979   }
2980 qed simp
2982 lemma infnorm_mul_lemma: "infnorm (a *\<^sub>R x) \<le> \<bar>a\<bar> * infnorm x"
2983   unfolding infnorm_mul ..
2985 lemma infnorm_pos_lt: "infnorm x > 0 \<longleftrightarrow> x \<noteq> 0"
2986   using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith
2988 text \<open>Prove that it differs only up to a bound from Euclidean norm.\<close>
2990 lemma infnorm_le_norm: "infnorm x \<le> norm x"
2991   by (simp add: Basis_le_norm infnorm_Max)
2993 lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
2994   by (subst (1 2) euclidean_representation [symmetric])
2995     (simp add: inner_setsum_right inner_Basis ac_simps)
2997 lemma norm_le_infnorm:
2998   fixes x :: "'a::euclidean_space"
2999   shows "norm x \<le> sqrt DIM('a) * infnorm x"
3000 proof -
3001   let ?d = "DIM('a)"
3002   have "real ?d \<ge> 0"
3003     by simp
3004   then have d2: "(sqrt (real ?d))\<^sup>2 = real ?d"
3005     by (auto intro: real_sqrt_pow2)
3006   have th: "sqrt (real ?d) * infnorm x \<ge> 0"
3007     by (simp add: zero_le_mult_iff infnorm_pos_le)
3008   have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
3009     unfolding power_mult_distrib d2
3010     apply (subst euclidean_inner)
3011     apply (subst power2_abs[symmetric])
3012     apply (rule order_trans[OF setsum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
3013     apply (auto simp add: power2_eq_square[symmetric])
3014     apply (subst power2_abs[symmetric])
3015     apply (rule power_mono)
3016     apply (auto simp: infnorm_Max)
3017     done
3018   from real_le_lsqrt[OF inner_ge_zero th th1]
3019   show ?thesis
3020     unfolding norm_eq_sqrt_inner id_def .
3021 qed
3023 lemma tendsto_infnorm [tendsto_intros]:
3024   assumes "(f \<longlongrightarrow> a) F"
3025   shows "((\<lambda>x. infnorm (f x)) \<longlongrightarrow> infnorm a) F"
3026 proof (rule tendsto_compose [OF LIM_I assms])
3027   fix r :: real
3028   assume "r > 0"
3029   then show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (infnorm x - infnorm a) < r"
3030     by (metis real_norm_def le_less_trans real_abs_sub_infnorm infnorm_le_norm)
3031 qed
3033 text \<open>Equality in Cauchy-Schwarz and triangle inequalities.\<close>
3035 lemma norm_cauchy_schwarz_eq: "x \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
3036   (is "?lhs \<longleftrightarrow> ?rhs")
3037 proof -
3038   {
3039     assume h: "x = 0"
3040     then have ?thesis by simp
3041   }
3042   moreover
3043   {
3044     assume h: "y = 0"
3045     then have ?thesis by simp
3046   }
3047   moreover
3048   {
3049     assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
3050     from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
3051     have "?rhs \<longleftrightarrow>
3052       (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) -
3053         norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) =  0)"
3054       using x y
3055       unfolding inner_simps
3056       unfolding power2_norm_eq_inner[symmetric] power2_eq_square right_minus_eq
3059       apply metis
3060       done
3061     also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
3062       by (simp add: field_simps inner_commute)
3063     also have "\<dots> \<longleftrightarrow> ?lhs" using x y
3064       apply simp
3065       apply metis
3066       done
3067     finally have ?thesis by blast
3068   }
3069   ultimately show ?thesis by blast
3070 qed
3072 lemma norm_cauchy_schwarz_abs_eq:
3073   "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow>
3074     norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm x *\<^sub>R y = - norm y *\<^sub>R x"
3075   (is "?lhs \<longleftrightarrow> ?rhs")
3076 proof -
3077   have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> \<bar>x\<bar> = a \<longleftrightarrow> x = a \<or> x = - a"
3078     by arith
3079   have "?rhs \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)"
3080     by simp
3081   also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
3082     unfolding norm_cauchy_schwarz_eq[symmetric]
3083     unfolding norm_minus_cancel norm_scaleR ..
3084   also have "\<dots> \<longleftrightarrow> ?lhs"
3085     unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps
3086     by auto
3087   finally show ?thesis ..
3088 qed
3090 lemma norm_triangle_eq:
3091   fixes x y :: "'a::real_inner"
3092   shows "norm (x + y) = norm x + norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
3093 proof -
3094   {
3095     assume x: "x = 0 \<or> y = 0"
3096     then have ?thesis
3097       by (cases "x = 0") simp_all
3098   }
3099   moreover
3100   {
3101     assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
3102     then have "norm x \<noteq> 0" "norm y \<noteq> 0"
3103       by simp_all
3104     then have n: "norm x > 0" "norm y > 0"
3105       using norm_ge_zero[of x] norm_ge_zero[of y] by arith+
3106     have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 \<Longrightarrow> a = b + c \<longleftrightarrow> a\<^sup>2 = (b + c)\<^sup>2"
3107       by algebra
3108     have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
3109       apply (rule th)
3110       using n norm_ge_zero[of "x + y"]
3111       apply arith
3112       done
3113     also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
3114       unfolding norm_cauchy_schwarz_eq[symmetric]
3115       unfolding power2_norm_eq_inner inner_simps
3116       by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
3117     finally have ?thesis .
3118   }
3119   ultimately show ?thesis by blast
3120 qed
3123 subsection \<open>Collinearity\<close>
3125 definition collinear :: "'a::real_vector set \<Rightarrow> bool"
3126   where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
3128 lemma collinear_empty [iff]: "collinear {}"
3131 lemma collinear_sing [iff]: "collinear {x}"
3134 lemma collinear_2 [iff]: "collinear {x, y}"
3136   apply (rule exI[where x="x - y"])
3137   apply auto
3138   apply (rule exI[where x=1], simp)
3139   apply (rule exI[where x="- 1"], simp)
3140   done
3142 lemma collinear_lemma: "collinear {0, x, y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *\<^sub>R x)"
3143   (is "?lhs \<longleftrightarrow> ?rhs")
3144 proof -
3145   {
3146     assume "x = 0 \<or> y = 0"
3147     then have ?thesis
3148       by (cases "x = 0") (simp_all add: collinear_2 insert_commute)
3149   }
3150   moreover
3151   {
3152     assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
3153     have ?thesis
3154     proof
3155       assume h: "?lhs"
3156       then obtain u where u: "\<forall> x\<in> {0,x,y}. \<forall>y\<in> {0,x,y}. \<exists>c. x - y = c *\<^sub>R u"
3157         unfolding collinear_def by blast
3158       from u[rule_format, of x 0] u[rule_format, of y 0]
3159       obtain cx and cy where
3160         cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
3161         by auto
3162       from cx x have cx0: "cx \<noteq> 0" by auto
3163       from cy y have cy0: "cy \<noteq> 0" by auto
3164       let ?d = "cy / cx"
3165       from cx cy cx0 have "y = ?d *\<^sub>R x"
3166         by simp
3167       then show ?rhs using x y by blast
3168     next
3169       assume h: "?rhs"
3170       then obtain c where c: "y = c *\<^sub>R x"
3171         using x y by blast
3172       show ?lhs
3173         unfolding collinear_def c
3174         apply (rule exI[where x=x])
3175         apply auto
3176         apply (rule exI[where x="- 1"], simp)
3177         apply (rule exI[where x= "-c"], simp)
3178         apply (rule exI[where x=1], simp)
3179         apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
3180         apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
3181         done
3182     qed
3183   }
3184   ultimately show ?thesis by blast
3185 qed
3187 lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
3188   unfolding norm_cauchy_schwarz_abs_eq
3189   apply (cases "x=0", simp_all)
3190   apply (cases "y=0", simp_all add: insert_commute)
3191   unfolding collinear_lemma
3192   apply simp
3193   apply (subgoal_tac "norm x \<noteq> 0")
3194   apply (subgoal_tac "norm y \<noteq> 0")
3195   apply (rule iffI)
3196   apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x")
3197   apply (rule exI[where x="(1/norm x) * norm y"])
3198   apply (drule sym)
3199   unfolding scaleR_scaleR[symmetric]