1160 fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" |
1161 fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" |
1161 shows "setsum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} = |
1162 shows "setsum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} = |
1162 (if m <= n then f m - f(n + 1) else 0)" |
1163 (if m <= n then f m - f(n + 1) else 0)" |
1163 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) |
1164 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) |
1164 |
1165 |
1165 lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] |
1166 lemma setsum_restrict_set': |
|
1167 "finite A \<Longrightarrow> setsum f {x \<in> A. x \<in> B} = (\<Sum>x\<in>A. if x \<in> B then f x else 0)" |
|
1168 by (simp add: setsum_restrict_set [symmetric] Int_def) |
|
1169 |
|
1170 lemma setsum_restrict_set'': |
|
1171 "finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x then f x else 0)" |
|
1172 by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq]) |
1166 |
1173 |
1167 lemma setsum_setsum_restrict: |
1174 lemma setsum_setsum_restrict: |
1168 "finite S \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T" |
1175 "finite S \<Longrightarrow> finite T \<Longrightarrow> |
1169 by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def) |
1176 setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y \<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T" |
1170 (rule setsum_commute) |
1177 by (simp add: setsum_restrict_set'') (rule setsum_commute) |
1171 |
1178 |
1172 lemma setsum_image_gen: assumes fS: "finite S" |
1179 lemma setsum_image_gen: assumes fS: "finite S" |
1173 shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" |
1180 shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" |
1174 proof- |
1181 proof- |
1175 { fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto } |
1182 { fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto } |