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