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