equal
deleted
inserted
replaced
694 qed |
694 qed |
695 |
695 |
696 lemma setsum_subtractf: |
696 lemma setsum_subtractf: |
697 "setsum (%x. ((f x)::'a::ab_group_add) - g x) A = |
697 "setsum (%x. ((f x)::'a::ab_group_add) - g x) A = |
698 setsum f A - setsum g A" |
698 setsum f A - setsum g A" |
699 proof (cases "finite A") |
699 using setsum_addf [of f "- g" A] by (simp add: setsum_negf) |
700 case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf) |
|
701 next |
|
702 case False thus ?thesis by simp |
|
703 qed |
|
704 |
700 |
705 lemma setsum_nonneg: |
701 lemma setsum_nonneg: |
706 assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x" |
702 assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x" |
707 shows "0 \<le> setsum f A" |
703 shows "0 \<le> setsum f A" |
708 proof (cases "finite A") |
704 proof (cases "finite A") |