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.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.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.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)
```