equal
deleted
inserted
replaced
1197 next |
1197 next |
1198 case False thus ?thesis by (simp add: setsum_def) |
1198 case False thus ?thesis by (simp add: setsum_def) |
1199 qed |
1199 qed |
1200 |
1200 |
1201 lemma setsum_abs[iff]: |
1201 lemma setsum_abs[iff]: |
1202 fixes f :: "'a => ('b::lordered_ab_group_abs)" |
1202 fixes f :: "'a => ('b::pordered_ab_group_add_abs)" |
1203 shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" |
1203 shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" |
1204 proof (cases "finite A") |
1204 proof (cases "finite A") |
1205 case True |
1205 case True |
1206 thus ?thesis |
1206 thus ?thesis |
1207 proof induct |
1207 proof induct |
1213 next |
1213 next |
1214 case False thus ?thesis by (simp add: setsum_def) |
1214 case False thus ?thesis by (simp add: setsum_def) |
1215 qed |
1215 qed |
1216 |
1216 |
1217 lemma setsum_abs_ge_zero[iff]: |
1217 lemma setsum_abs_ge_zero[iff]: |
1218 fixes f :: "'a => ('b::lordered_ab_group_abs)" |
1218 fixes f :: "'a => ('b::pordered_ab_group_add_abs)" |
1219 shows "0 \<le> setsum (%i. abs(f i)) A" |
1219 shows "0 \<le> setsum (%i. abs(f i)) A" |
1220 proof (cases "finite A") |
1220 proof (cases "finite A") |
1221 case True |
1221 case True |
1222 thus ?thesis |
1222 thus ?thesis |
1223 proof induct |
1223 proof induct |
1228 next |
1228 next |
1229 case False thus ?thesis by (simp add: setsum_def) |
1229 case False thus ?thesis by (simp add: setsum_def) |
1230 qed |
1230 qed |
1231 |
1231 |
1232 lemma abs_setsum_abs[simp]: |
1232 lemma abs_setsum_abs[simp]: |
1233 fixes f :: "'a => ('b::lordered_ab_group_abs)" |
1233 fixes f :: "'a => ('b::pordered_ab_group_add_abs)" |
1234 shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))" |
1234 shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))" |
1235 proof (cases "finite A") |
1235 proof (cases "finite A") |
1236 case True |
1236 case True |
1237 thus ?thesis |
1237 thus ?thesis |
1238 proof induct |
1238 proof induct |