src/HOL/Analysis/Linear_Algebra.thy
changeset 64267 b9a1486e79be
parent 64122 74fde524799e
child 64773 223b2ebdda79
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -141,9 +141,9 @@
     1.4  lemma linear_uminus: "linear uminus"
     1.5  by (simp add: linear_iff)
     1.6  
     1.7 -lemma linear_compose_setsum:
     1.8 +lemma linear_compose_sum:
     1.9    assumes lS: "\<forall>a \<in> S. linear (f a)"
    1.10 -  shows "linear (\<lambda>x. setsum (\<lambda>a. f a x) S)"
    1.11 +  shows "linear (\<lambda>x. sum (\<lambda>a. f a x) S)"
    1.12  proof (cases "finite S")
    1.13    case True
    1.14    then show ?thesis
    1.15 @@ -173,9 +173,9 @@
    1.16  lemma linear_diff: "linear f \<Longrightarrow> f (x - y) = f x - f y"
    1.17    using linear_add [of f x "- y"] by (simp add: linear_neg)
    1.18  
    1.19 -lemma linear_setsum:
    1.20 +lemma linear_sum:
    1.21    assumes f: "linear f"
    1.22 -  shows "f (setsum g S) = setsum (f \<circ> g) S"
    1.23 +  shows "f (sum g S) = sum (f \<circ> g) S"
    1.24  proof (cases "finite S")
    1.25    case True
    1.26    then show ?thesis
    1.27 @@ -186,10 +186,10 @@
    1.28      by (simp add: linear_0 [OF f])
    1.29  qed
    1.30  
    1.31 -lemma linear_setsum_mul:
    1.32 +lemma linear_sum_mul:
    1.33    assumes lin: "linear f"
    1.34 -  shows "f (setsum (\<lambda>i. c i *\<^sub>R v i) S) = setsum (\<lambda>i. c i *\<^sub>R f (v i)) S"
    1.35 -  using linear_setsum[OF lin, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lin]
    1.36 +  shows "f (sum (\<lambda>i. c i *\<^sub>R v i) S) = sum (\<lambda>i. c i *\<^sub>R f (v i)) S"
    1.37 +  using linear_sum[OF lin, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lin]
    1.38    by simp
    1.39  
    1.40  lemma linear_injective_0:
    1.41 @@ -250,10 +250,10 @@
    1.42  lemma subspace_diff: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
    1.43    using subspace_add [of S x "- y"] by (simp add: subspace_neg)
    1.44  
    1.45 -lemma (in real_vector) subspace_setsum:
    1.46 +lemma (in real_vector) subspace_sum:
    1.47    assumes sA: "subspace A"
    1.48      and f: "\<And>x. x \<in> B \<Longrightarrow> f x \<in> A"
    1.49 -  shows "setsum f B \<in> A"
    1.50 +  shows "sum f B \<in> A"
    1.51  proof (cases "finite B")
    1.52    case True
    1.53    then show ?thesis
    1.54 @@ -460,8 +460,8 @@
    1.55  lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
    1.56    by (metis subspace_span subspace_diff)
    1.57  
    1.58 -lemma (in real_vector) span_setsum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> setsum f A \<in> span S"
    1.59 -  by (rule subspace_setsum [OF subspace_span])
    1.60 +lemma (in real_vector) span_sum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> sum f A \<in> span S"
    1.61 +  by (rule subspace_sum [OF subspace_span])
    1.62  
    1.63  lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
    1.64    by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
    1.65 @@ -619,16 +619,16 @@
    1.66  text \<open>An explicit expansion is sometimes needed.\<close>
    1.67  
    1.68  lemma span_explicit:
    1.69 -  "span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
    1.70 +  "span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
    1.71    (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")
    1.72  proof -
    1.73    {
    1.74      fix x
    1.75      assume "?h x"
    1.76 -    then obtain S u where "finite S" and "S \<subseteq> P" and "setsum (\<lambda>v. u v *\<^sub>R v) S = x"
    1.77 +    then obtain S u where "finite S" and "S \<subseteq> P" and "sum (\<lambda>v. u v *\<^sub>R v) S = x"
    1.78        by blast
    1.79      then have "x \<in> span P"
    1.80 -      by (auto intro: span_setsum span_mul span_superset)
    1.81 +      by (auto intro: span_sum span_mul span_superset)
    1.82    }
    1.83    moreover
    1.84    have "\<forall>x \<in> span P. ?h x"
    1.85 @@ -640,7 +640,7 @@
    1.86      assume x: "x \<in> P"
    1.87      assume hy: "?h y"
    1.88      from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
    1.89 -      and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y" by blast
    1.90 +      and u: "sum (\<lambda>v. u v *\<^sub>R v) S = y" by blast
    1.91      let ?S = "insert x S"
    1.92      let ?u = "\<lambda>y. if y = x then (if x \<in> S then u y + c else c) else u y"
    1.93      from fS SP x have th0: "finite (insert x S)" "insert x S \<subseteq> P"
    1.94 @@ -648,19 +648,19 @@
    1.95      have "?Q ?S ?u (c*\<^sub>R x + y)"
    1.96      proof cases
    1.97        assume xS: "x \<in> S"
    1.98 -      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"
    1.99 -        using xS by (simp add: setsum.remove [OF fS xS] insert_absorb)
   1.100 +      have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = (\<Sum>v\<in>S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x"
   1.101 +        using xS by (simp add: sum.remove [OF fS xS] insert_absorb)
   1.102        also have "\<dots> = (\<Sum>v\<in>S. u v *\<^sub>R v) + c *\<^sub>R x"
   1.103 -        by (simp add: setsum.remove [OF fS xS] algebra_simps)
   1.104 +        by (simp add: sum.remove [OF fS xS] algebra_simps)
   1.105        also have "\<dots> = c*\<^sub>R x + y"
   1.106          by (simp add: add.commute u)
   1.107 -      finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" .
   1.108 +      finally have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" .
   1.109        then show ?thesis using th0 by blast
   1.110      next
   1.111        assume xS: "x \<notin> S"
   1.112        have th00: "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y"
   1.113          unfolding u[symmetric]
   1.114 -        apply (rule setsum.cong)
   1.115 +        apply (rule sum.cong)
   1.116          using xS
   1.117          apply auto
   1.118          done
   1.119 @@ -674,13 +674,13 @@
   1.120  qed
   1.121  
   1.122  lemma dependent_explicit:
   1.123 -  "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))"
   1.124 +  "dependent P \<longleftrightarrow> (\<exists>S u. finite S \<and> S \<subseteq> P \<and> (\<exists>v\<in>S. u v \<noteq> 0 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0))"
   1.125    (is "?lhs = ?rhs")
   1.126  proof -
   1.127    {
   1.128      assume dP: "dependent P"
   1.129      then obtain a S u where aP: "a \<in> P" and fS: "finite S"
   1.130 -      and SP: "S \<subseteq> P - {a}" and ua: "setsum (\<lambda>v. u v *\<^sub>R v) S = a"
   1.131 +      and SP: "S \<subseteq> P - {a}" and ua: "sum (\<lambda>v. u v *\<^sub>R v) S = a"
   1.132        unfolding dependent_def span_explicit by blast
   1.133      let ?S = "insert a S"
   1.134      let ?u = "\<lambda>y. if y = a then - 1 else u y"
   1.135 @@ -689,11 +689,11 @@
   1.136        by blast
   1.137      from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0"
   1.138        by auto
   1.139 -    have s0: "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"
   1.140 +    have s0: "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"
   1.141        using fS aS
   1.142        apply simp
   1.143        apply (subst (2) ua[symmetric])
   1.144 -      apply (rule setsum.cong)
   1.145 +      apply (rule sum.cong)
   1.146        apply auto
   1.147        done
   1.148      with th0 have ?rhs by fast
   1.149 @@ -705,18 +705,18 @@
   1.150        and SP: "S \<subseteq> P"
   1.151        and vS: "v \<in> S"
   1.152        and uv: "u v \<noteq> 0"
   1.153 -      and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = 0"
   1.154 +      and u: "sum (\<lambda>v. u v *\<^sub>R v) S = 0"
   1.155      let ?a = v
   1.156      let ?S = "S - {v}"
   1.157      let ?u = "\<lambda>i. (- u i) / u v"
   1.158      have th0: "?a \<in> P" "finite ?S" "?S \<subseteq> P"
   1.159        using fS SP vS by auto
   1.160 -    have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =
   1.161 -      setsum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
   1.162 -      using fS vS uv by (simp add: setsum_diff1 field_simps)
   1.163 +    have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S =
   1.164 +      sum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
   1.165 +      using fS vS uv by (simp add: sum_diff1 field_simps)
   1.166      also have "\<dots> = ?a"
   1.167 -      unfolding scaleR_right.setsum [symmetric] u using uv by simp
   1.168 -    finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
   1.169 +      unfolding scaleR_right.sum [symmetric] u using uv by simp
   1.170 +    finally have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
   1.171      with th0 have ?lhs
   1.172        unfolding dependent_def span_explicit
   1.173        apply -
   1.174 @@ -740,7 +740,7 @@
   1.175      by (force simp: dependent_explicit)
   1.176    with assms show ?rhs
   1.177      apply (rule_tac x="\<lambda>v. if v \<in> T then u v else 0" in exI)
   1.178 -    apply (auto simp: setsum.mono_neutral_right)
   1.179 +    apply (auto simp: sum.mono_neutral_right)
   1.180      done
   1.181  next
   1.182    assume ?rhs  with assms show ?lhs
   1.183 @@ -753,7 +753,7 @@
   1.184    apply safe
   1.185    subgoal for x S u
   1.186      by (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
   1.187 -        (auto intro!: setsum.mono_neutral_cong_right)
   1.188 +        (auto intro!: sum.mono_neutral_cong_right)
   1.189    apply auto
   1.190    done
   1.191  
   1.192 @@ -764,8 +764,8 @@
   1.193    apply safe
   1.194    subgoal for S u v
   1.195      apply (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
   1.196 -    apply (subst setsum.mono_neutral_cong_left[where T=S])
   1.197 -    apply (auto intro!: setsum.mono_neutral_cong_right cong: rev_conj_cong)
   1.198 +    apply (subst sum.mono_neutral_cong_left[where T=S])
   1.199 +    apply (auto intro!: sum.mono_neutral_cong_right cong: rev_conj_cong)
   1.200      done
   1.201    apply auto
   1.202    done
   1.203 @@ -794,13 +794,13 @@
   1.204      then show "finite {x. X x - Y x \<noteq> 0}" "{x. X x - Y x \<noteq> 0} \<subseteq> B"
   1.205        using X Y by (auto dest: finite_subset)
   1.206      then have "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *\<^sub>R x) = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. (X v - Y v) *\<^sub>R v)"
   1.207 -      using X Y by (intro setsum.mono_neutral_cong_left) auto
   1.208 +      using X Y by (intro sum.mono_neutral_cong_left) auto
   1.209      also have "\<dots> = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *\<^sub>R v) - (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *\<^sub>R v)"
   1.210 -      by (simp add: scaleR_diff_left setsum_subtractf assms)
   1.211 +      by (simp add: scaleR_diff_left sum_subtractf assms)
   1.212      also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *\<^sub>R v) = (\<Sum>v\<in>{S. X S \<noteq> 0}. X v *\<^sub>R v)"
   1.213 -      using X Y by (intro setsum.mono_neutral_cong_right) auto
   1.214 +      using X Y by (intro sum.mono_neutral_cong_right) auto
   1.215      also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *\<^sub>R v) = (\<Sum>v\<in>{S. Y S \<noteq> 0}. Y v *\<^sub>R v)"
   1.216 -      using X Y by (intro setsum.mono_neutral_cong_right) auto
   1.217 +      using X Y by (intro sum.mono_neutral_cong_right) auto
   1.218      finally show "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *\<^sub>R x) = 0"
   1.219        using assms by simp
   1.220    qed
   1.221 @@ -927,7 +927,7 @@
   1.222  
   1.223  lemma span_finite:
   1.224    assumes fS: "finite S"
   1.225 -  shows "span S = {y. \<exists>u. setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
   1.226 +  shows "span S = {y. \<exists>u. sum (\<lambda>v. u v *\<^sub>R v) S = y}"
   1.227    (is "_ = ?rhs")
   1.228  proof -
   1.229    {
   1.230 @@ -935,18 +935,18 @@
   1.231      assume y: "y \<in> span S"
   1.232      from y obtain S' u where fS': "finite S'"
   1.233        and SS': "S' \<subseteq> S"
   1.234 -      and u: "setsum (\<lambda>v. u v *\<^sub>R v) S' = y"
   1.235 +      and u: "sum (\<lambda>v. u v *\<^sub>R v) S' = y"
   1.236        unfolding span_explicit by blast
   1.237      let ?u = "\<lambda>x. if x \<in> S' then u x else 0"
   1.238 -    have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = setsum (\<lambda>v. u v *\<^sub>R v) S'"
   1.239 -      using SS' fS by (auto intro!: setsum.mono_neutral_cong_right)
   1.240 -    then have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = y" by (metis u)
   1.241 +    have "sum (\<lambda>v. ?u v *\<^sub>R v) S = sum (\<lambda>v. u v *\<^sub>R v) S'"
   1.242 +      using SS' fS by (auto intro!: sum.mono_neutral_cong_right)
   1.243 +    then have "sum (\<lambda>v. ?u v *\<^sub>R v) S = y" by (metis u)
   1.244      then have "y \<in> ?rhs" by auto
   1.245    }
   1.246    moreover
   1.247    {
   1.248      fix y u
   1.249 -    assume u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y"
   1.250 +    assume u: "sum (\<lambda>v. u v *\<^sub>R v) S = y"
   1.251      then have "y \<in> span S" using fS unfolding span_explicit by auto
   1.252    }
   1.253    ultimately show ?thesis by blast
   1.254 @@ -970,10 +970,10 @@
   1.255    proof (rule independentD_unique)
   1.256      have "(\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R z)
   1.257        = (\<Sum>z\<in>{z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}. (X x z + X y z) *\<^sub>R z)"
   1.258 -      by (intro setsum.mono_neutral_cong_left) (auto intro: X)
   1.259 +      by (intro sum.mono_neutral_cong_left) (auto intro: X)
   1.260      also have "\<dots> = (\<Sum>z\<in>{z. X x z \<noteq> 0}. X x z *\<^sub>R z) + (\<Sum>z\<in>{z. X y z \<noteq> 0}. X y z *\<^sub>R z)"
   1.261 -      by (auto simp add: scaleR_add_left setsum.distrib
   1.262 -               intro!: arg_cong2[where f="op +"]  setsum.mono_neutral_cong_right X)
   1.263 +      by (auto simp add: scaleR_add_left sum.distrib
   1.264 +               intro!: arg_cong2[where f="op +"]  sum.mono_neutral_cong_right X)
   1.265      also have "\<dots> = x + y"
   1.266        by (simp add: X(3)[symmetric])
   1.267      also have "\<dots> = (\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z)"
   1.268 @@ -994,7 +994,7 @@
   1.269        "finite {z. c * X x z \<noteq> 0}" "{z. c * X x z \<noteq> 0} \<subseteq> B' "
   1.270        using X(1,2) by auto
   1.271      show "(\<Sum>z | X (c *\<^sub>R x) z \<noteq> 0. X (c *\<^sub>R x) z *\<^sub>R z) = (\<Sum>z | c * X x z \<noteq> 0. (c * X x z) *\<^sub>R z)"
   1.272 -      unfolding scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric]
   1.273 +      unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric]
   1.274        by (cases "c = 0") (auto simp: X(3)[symmetric])
   1.275    qed
   1.276  
   1.277 @@ -1013,14 +1013,14 @@
   1.278      fix x y
   1.279      have *: "(\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R f' z)
   1.280        = (\<Sum>z\<in>{z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}. (X x z + X y z) *\<^sub>R f' z)"
   1.281 -      by (intro setsum.mono_neutral_cong_left) (auto intro: X)
   1.282 +      by (intro sum.mono_neutral_cong_left) (auto intro: X)
   1.283      show "g (x + y) = g x + g y"
   1.284        unfolding g_def X_add *
   1.285 -      by (auto simp add: scaleR_add_left setsum.distrib
   1.286 -               intro!: arg_cong2[where f="op +"]  setsum.mono_neutral_cong_right X)
   1.287 +      by (auto simp add: scaleR_add_left sum.distrib
   1.288 +               intro!: arg_cong2[where f="op +"]  sum.mono_neutral_cong_right X)
   1.289    next
   1.290      show "g (r *\<^sub>R x) = r *\<^sub>R g x" for r x
   1.291 -      by (auto simp add: g_def X_cmult scaleR_setsum_right intro!: setsum.mono_neutral_cong_left X)
   1.292 +      by (auto simp add: g_def X_cmult scaleR_sum_right intro!: sum.mono_neutral_cong_left X)
   1.293    qed
   1.294    moreover have "\<forall>x\<in>B. g x = f x"
   1.295      using \<open>B \<subseteq> B'\<close> by (auto simp: g_f' f'_def)
   1.296 @@ -1436,9 +1436,9 @@
   1.297    shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
   1.298  proof -
   1.299    have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
   1.300 -    by (simp add: inner_setsum_left)
   1.301 +    by (simp add: inner_sum_left)
   1.302    then show ?thesis
   1.303 -    unfolding linear_setsum_mul[OF lf, symmetric]
   1.304 +    unfolding linear_sum_mul[OF lf, symmetric]
   1.305      unfolding euclidean_representation ..
   1.306  qed
   1.307  
   1.308 @@ -1475,30 +1475,30 @@
   1.309  lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
   1.310    by (rule norm_triangle_ineq [THEN le_less_trans])
   1.311  
   1.312 -lemma setsum_clauses:
   1.313 -  shows "setsum f {} = 0"
   1.314 -    and "finite S \<Longrightarrow> setsum f (insert x S) = (if x \<in> S then setsum f S else f x + setsum f S)"
   1.315 +lemma sum_clauses:
   1.316 +  shows "sum f {} = 0"
   1.317 +    and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
   1.318    by (auto simp add: insert_absorb)
   1.319  
   1.320 -lemma setsum_norm_le:
   1.321 +lemma sum_norm_le:
   1.322    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   1.323    assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
   1.324 -  shows "norm (setsum f S) \<le> setsum g S"
   1.325 -  by (rule order_trans [OF norm_setsum setsum_mono]) (simp add: fg)
   1.326 -
   1.327 -lemma setsum_norm_bound:
   1.328 +  shows "norm (sum f S) \<le> sum g S"
   1.329 +  by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
   1.330 +
   1.331 +lemma sum_norm_bound:
   1.332    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   1.333    assumes K: "\<forall>x \<in> S. norm (f x) \<le> K"
   1.334 -  shows "norm (setsum f S) \<le> of_nat (card S) * K"
   1.335 -  using setsum_norm_le[OF K] setsum_constant[symmetric]
   1.336 +  shows "norm (sum f S) \<le> of_nat (card S) * K"
   1.337 +  using sum_norm_le[OF K] sum_constant[symmetric]
   1.338    by simp
   1.339  
   1.340 -lemma setsum_group:
   1.341 +lemma sum_group:
   1.342    assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
   1.343 -  shows "setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) T = setsum g S"
   1.344 -  apply (subst setsum_image_gen[OF fS, of g f])
   1.345 -  apply (rule setsum.mono_neutral_right[OF fT fST])
   1.346 -  apply (auto intro: setsum.neutral)
   1.347 +  shows "sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) T = sum g S"
   1.348 +  apply (subst sum_image_gen[OF fS, of g f])
   1.349 +  apply (rule sum.mono_neutral_right[OF fT fST])
   1.350 +  apply (auto intro: sum.neutral)
   1.351    done
   1.352  
   1.353  lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
   1.354 @@ -1557,11 +1557,11 @@
   1.355    by (auto simp: pairwise_def orthogonal_clauses)
   1.356  
   1.357  lemma orthogonal_rvsum:
   1.358 -    "\<lbrakk>finite s; \<And>y. y \<in> s \<Longrightarrow> orthogonal x (f y)\<rbrakk> \<Longrightarrow> orthogonal x (setsum f s)"
   1.359 +    "\<lbrakk>finite s; \<And>y. y \<in> s \<Longrightarrow> orthogonal x (f y)\<rbrakk> \<Longrightarrow> orthogonal x (sum f s)"
   1.360    by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
   1.361  
   1.362  lemma orthogonal_lvsum:
   1.363 -    "\<lbrakk>finite s; \<And>x. x \<in> s \<Longrightarrow> orthogonal (f x) y\<rbrakk> \<Longrightarrow> orthogonal (setsum f s) y"
   1.364 +    "\<lbrakk>finite s; \<And>x. x \<in> s \<Longrightarrow> orthogonal (f x) y\<rbrakk> \<Longrightarrow> orthogonal (sum f s) y"
   1.365    by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
   1.366  
   1.367  lemma norm_add_Pythagorean:
   1.368 @@ -1574,15 +1574,15 @@
   1.369      by (simp add: power2_norm_eq_inner)
   1.370  qed
   1.371  
   1.372 -lemma norm_setsum_Pythagorean:
   1.373 +lemma norm_sum_Pythagorean:
   1.374    assumes "finite I" "pairwise (\<lambda>i j. orthogonal (f i) (f j)) I"
   1.375 -    shows "(norm (setsum f I))\<^sup>2 = (\<Sum>i\<in>I. (norm (f i))\<^sup>2)"
   1.376 +    shows "(norm (sum f I))\<^sup>2 = (\<Sum>i\<in>I. (norm (f i))\<^sup>2)"
   1.377  using assms
   1.378  proof (induction I rule: finite_induct)
   1.379    case empty then show ?case by simp
   1.380  next
   1.381    case (insert x I)
   1.382 -  then have "orthogonal (f x) (setsum f I)"
   1.383 +  then have "orthogonal (f x) (sum f I)"
   1.384      by (metis pairwise_insert orthogonal_rvsum)
   1.385    with insert show ?case
   1.386      by (simp add: pairwise_insert norm_add_Pythagorean)
   1.387 @@ -1630,25 +1630,25 @@
   1.388  lemma bilinear_rsub: "bilinear h \<Longrightarrow> h z (x - y) = h z x - h z y"
   1.389    using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)
   1.390  
   1.391 -lemma bilinear_setsum:
   1.392 +lemma bilinear_sum:
   1.393    assumes bh: "bilinear h"
   1.394      and fS: "finite S"
   1.395      and fT: "finite T"
   1.396 -  shows "h (setsum f S) (setsum g T) = setsum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
   1.397 +  shows "h (sum f S) (sum g T) = sum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
   1.398  proof -
   1.399 -  have "h (setsum f S) (setsum g T) = setsum (\<lambda>x. h (f x) (setsum g T)) S"
   1.400 -    apply (rule linear_setsum[unfolded o_def])
   1.401 +  have "h (sum f S) (sum g T) = sum (\<lambda>x. h (f x) (sum g T)) S"
   1.402 +    apply (rule linear_sum[unfolded o_def])
   1.403      using bh fS
   1.404      apply (auto simp add: bilinear_def)
   1.405      done
   1.406 -  also have "\<dots> = setsum (\<lambda>x. setsum (\<lambda>y. h (f x) (g y)) T) S"
   1.407 -    apply (rule setsum.cong, simp)
   1.408 -    apply (rule linear_setsum[unfolded o_def])
   1.409 +  also have "\<dots> = sum (\<lambda>x. sum (\<lambda>y. h (f x) (g y)) T) S"
   1.410 +    apply (rule sum.cong, simp)
   1.411 +    apply (rule linear_sum[unfolded o_def])
   1.412      using bh fT
   1.413      apply (auto simp add: bilinear_def)
   1.414      done
   1.415    finally show ?thesis
   1.416 -    unfolding setsum.cartesian_product .
   1.417 +    unfolding sum.cartesian_product .
   1.418  qed
   1.419  
   1.420  
   1.421 @@ -1694,10 +1694,10 @@
   1.422      have "f x \<bullet> y = f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i) \<bullet> y"
   1.423        by (simp add: euclidean_representation)
   1.424      also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<bullet> y"
   1.425 -      unfolding linear_setsum[OF lf]
   1.426 +      unfolding linear_sum[OF lf]
   1.427        by (simp add: linear_cmul[OF lf])
   1.428      finally show "f x \<bullet> y = x \<bullet> ?w"
   1.429 -      by (simp add: inner_setsum_left inner_setsum_right mult.commute)
   1.430 +      by (simp add: inner_sum_left inner_sum_right mult.commute)
   1.431    qed
   1.432    then show ?thesis
   1.433      unfolding adjoint_def choice_iff
   1.434 @@ -1876,7 +1876,7 @@
   1.435    apply simp
   1.436    apply clarify
   1.437    apply (drule_tac f="inner a" in arg_cong)
   1.438 -  apply (simp add: inner_Basis inner_setsum_right eq_commute)
   1.439 +  apply (simp add: inner_Basis inner_sum_right eq_commute)
   1.440    done
   1.441  
   1.442  lemma span_Basis [simp]: "span Basis = UNIV"
   1.443 @@ -1897,27 +1897,27 @@
   1.444  
   1.445  lemma norm_le_l1: "norm x \<le> (\<Sum>b\<in>Basis. \<bar>x \<bullet> b\<bar>)"
   1.446    apply (subst euclidean_representation[of x, symmetric])
   1.447 -  apply (rule order_trans[OF norm_setsum])
   1.448 -  apply (auto intro!: setsum_mono)
   1.449 +  apply (rule order_trans[OF norm_sum])
   1.450 +  apply (auto intro!: sum_mono)
   1.451    done
   1.452  
   1.453 -lemma setsum_norm_allsubsets_bound:
   1.454 +lemma sum_norm_allsubsets_bound:
   1.455    fixes f :: "'a \<Rightarrow> 'n::euclidean_space"
   1.456    assumes fP: "finite P"
   1.457 -    and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
   1.458 +    and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (sum f Q) \<le> e"
   1.459    shows "(\<Sum>x\<in>P. norm (f x)) \<le> 2 * real DIM('n) * e"
   1.460  proof -
   1.461    have "(\<Sum>x\<in>P. norm (f x)) \<le> (\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>)"
   1.462 -    by (rule setsum_mono) (rule norm_le_l1)
   1.463 +    by (rule sum_mono) (rule norm_le_l1)
   1.464    also have "(\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>) = (\<Sum>b\<in>Basis. \<Sum>x\<in>P. \<bar>f x \<bullet> b\<bar>)"
   1.465 -    by (rule setsum.commute)
   1.466 +    by (rule sum.commute)
   1.467    also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
   1.468 -  proof (rule setsum_bounded_above)
   1.469 +  proof (rule sum_bounded_above)
   1.470      fix i :: 'n
   1.471      assume i: "i \<in> Basis"
   1.472      have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
   1.473        norm ((\<Sum>x\<in>P \<inter> - {x. f x \<bullet> i < 0}. f x) \<bullet> i) + norm ((\<Sum>x\<in>P \<inter> {x. f x \<bullet> i < 0}. f x) \<bullet> i)"
   1.474 -      by (simp add: abs_real_def setsum.If_cases[OF fP] setsum_negf norm_triangle_ineq4 inner_setsum_left
   1.475 +      by (simp add: abs_real_def sum.If_cases[OF fP] sum_negf norm_triangle_ineq4 inner_sum_left
   1.476          del: real_norm_def)
   1.477      also have "\<dots> \<le> e + e"
   1.478        unfolding real_norm_def
   1.479 @@ -1943,9 +1943,9 @@
   1.480      let ?g = "\<lambda>b. (x \<bullet> b) *\<^sub>R f b"
   1.481      have "norm (f x) = norm (f (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b))"
   1.482        unfolding euclidean_representation ..
   1.483 -    also have "\<dots> = norm (setsum ?g Basis)"
   1.484 -      by (simp add: linear_setsum [OF lf] linear_cmul [OF lf])
   1.485 -    finally have th0: "norm (f x) = norm (setsum ?g Basis)" .
   1.486 +    also have "\<dots> = norm (sum ?g Basis)"
   1.487 +      by (simp add: linear_sum [OF lf] linear_cmul [OF lf])
   1.488 +    finally have th0: "norm (f x) = norm (sum ?g Basis)" .
   1.489      have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x"
   1.490      proof
   1.491        fix i :: 'a
   1.492 @@ -1958,9 +1958,9 @@
   1.493          apply (auto simp add: field_simps)
   1.494          done
   1.495      qed
   1.496 -    from setsum_norm_le[of _ ?g, OF th]
   1.497 +    from sum_norm_le[of _ ?g, OF th]
   1.498      show "norm (f x) \<le> ?B * norm x"
   1.499 -      unfolding th0 setsum_distrib_right by metis
   1.500 +      unfolding th0 sum_distrib_right by metis
   1.501    qed
   1.502  qed
   1.503  
   1.504 @@ -2012,17 +2012,17 @@
   1.505  proof (clarify intro!: exI[of _ "\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)"])
   1.506    fix x :: 'm
   1.507    fix y :: 'n
   1.508 -  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))"
   1.509 +  have "norm (h x y) = norm (h (sum (\<lambda>i. (x \<bullet> i) *\<^sub>R i) Basis) (sum (\<lambda>i. (y \<bullet> i) *\<^sub>R i) Basis))"
   1.510      apply (subst euclidean_representation[where 'a='m])
   1.511      apply (subst euclidean_representation[where 'a='n])
   1.512      apply rule
   1.513      done
   1.514 -  also have "\<dots> = norm (setsum (\<lambda> (i,j). h ((x \<bullet> i) *\<^sub>R i) ((y \<bullet> j) *\<^sub>R j)) (Basis \<times> Basis))"
   1.515 -    unfolding bilinear_setsum[OF bh finite_Basis finite_Basis] ..
   1.516 +  also have "\<dots> = norm (sum (\<lambda> (i,j). h ((x \<bullet> i) *\<^sub>R i) ((y \<bullet> j) *\<^sub>R j)) (Basis \<times> Basis))"
   1.517 +    unfolding bilinear_sum[OF bh finite_Basis finite_Basis] ..
   1.518    finally have th: "norm (h x y) = \<dots>" .
   1.519    show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
   1.520 -    apply (auto simp add: setsum_distrib_right th setsum.cartesian_product)
   1.521 -    apply (rule setsum_norm_le)
   1.522 +    apply (auto simp add: sum_distrib_right th sum.cartesian_product)
   1.523 +    apply (rule sum_norm_le)
   1.524      apply simp
   1.525      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
   1.526        field_simps simp del: scaleR_scaleR)
   1.527 @@ -2353,7 +2353,7 @@
   1.528    from \<open>\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C\<close>
   1.529    obtain C where C: "finite C" "card C \<le> card B"
   1.530      "span C = span B" "pairwise orthogonal C" by blast
   1.531 -  let ?a = "a - setsum (\<lambda>x. (x \<bullet> a / (x \<bullet> x)) *\<^sub>R x) C"
   1.532 +  let ?a = "a - sum (\<lambda>x. (x \<bullet> a / (x \<bullet> x)) *\<^sub>R x) C"
   1.533    let ?C = "insert ?a C"
   1.534    from C(1) have fC: "finite ?C"
   1.535      by simp
   1.536 @@ -2367,7 +2367,7 @@
   1.537        apply (simp only: scaleR_right_diff_distrib th0)
   1.538        apply (rule span_add_eq)
   1.539        apply (rule span_mul)
   1.540 -      apply (rule span_setsum)
   1.541 +      apply (rule span_sum)
   1.542        apply (rule span_mul)
   1.543        apply (rule span_superset)
   1.544        apply assumption
   1.545 @@ -2384,10 +2384,10 @@
   1.546        using C by simp
   1.547      have "orthogonal ?a y"
   1.548        unfolding orthogonal_def
   1.549 -      unfolding inner_diff inner_setsum_left right_minus_eq
   1.550 -      unfolding setsum.remove [OF \<open>finite C\<close> \<open>y \<in> C\<close>]
   1.551 +      unfolding inner_diff inner_sum_left right_minus_eq
   1.552 +      unfolding sum.remove [OF \<open>finite C\<close> \<open>y \<in> C\<close>]
   1.553        apply (clarsimp simp add: inner_commute[of y a])
   1.554 -      apply (rule setsum.neutral)
   1.555 +      apply (rule sum.neutral)
   1.556        apply clarsimp
   1.557        apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
   1.558        using \<open>y \<in> C\<close> by auto
   1.559 @@ -2446,10 +2446,10 @@
   1.560    from span_mono[OF B(2)] span_mono[OF B(3)]
   1.561    have sSB: "span S = span B"
   1.562      by (simp add: span_span)
   1.563 -  let ?a = "a - setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B"
   1.564 -  have "setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> span S"
   1.565 +  let ?a = "a - sum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B"
   1.566 +  have "sum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> span S"
   1.567      unfolding sSB
   1.568 -    apply (rule span_setsum)
   1.569 +    apply (rule span_sum)
   1.570      apply (rule span_mul)
   1.571      apply (rule span_superset)
   1.572      apply assumption
   1.573 @@ -2471,10 +2471,10 @@
   1.574        have "?a \<bullet> x = 0"
   1.575          apply (subst B')
   1.576          using fB fth
   1.577 -        unfolding setsum_clauses(2)[OF fth]
   1.578 +        unfolding sum_clauses(2)[OF fth]
   1.579          apply simp unfolding inner_simps
   1.580 -        apply (clarsimp simp add: inner_add inner_setsum_left)
   1.581 -        apply (rule setsum.neutral, rule ballI)
   1.582 +        apply (clarsimp simp add: inner_add inner_sum_left)
   1.583 +        apply (rule sum.neutral, rule ballI)
   1.584          apply (simp only: inner_commute)
   1.585          apply (auto simp add: x field_simps
   1.586            intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
   1.587 @@ -3016,7 +3016,7 @@
   1.588  
   1.589  lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
   1.590    by (subst (1 2) euclidean_representation [symmetric])
   1.591 -    (simp add: inner_setsum_right inner_Basis ac_simps)
   1.592 +    (simp add: inner_sum_right inner_Basis ac_simps)
   1.593  
   1.594  lemma norm_le_infnorm:
   1.595    fixes x :: "'a::euclidean_space"
   1.596 @@ -3033,7 +3033,7 @@
   1.597      unfolding power_mult_distrib d2
   1.598      apply (subst euclidean_inner)
   1.599      apply (subst power2_abs[symmetric])
   1.600 -    apply (rule order_trans[OF setsum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
   1.601 +    apply (rule order_trans[OF sum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
   1.602      apply (auto simp add: power2_eq_square[symmetric])
   1.603      apply (subst power2_abs[symmetric])
   1.604      apply (rule power_mono)