521 case singleton thus ?case by simp |
521 case singleton thus ?case by simp |
522 next |
522 next |
523 case insert thus ?case by (auto simp: add_strict_mono) |
523 case insert thus ?case by (auto simp: add_strict_mono) |
524 qed |
524 qed |
525 |
525 |
|
526 lemma setsum_strict_mono_ex1: |
|
527 fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}" |
|
528 assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a" |
|
529 shows "setsum f A < setsum g A" |
|
530 proof- |
|
531 from assms(3) obtain a where a: "a:A" "f a < g a" by blast |
|
532 have "setsum f A = setsum f ((A-{a}) \<union> {a})" |
|
533 by(simp add:insert_absorb[OF `a:A`]) |
|
534 also have "\<dots> = setsum f (A-{a}) + setsum f {a}" |
|
535 using `finite A` by(subst setsum_Un_disjoint) auto |
|
536 also have "setsum f (A-{a}) \<le> setsum g (A-{a})" |
|
537 by(rule setsum_mono)(simp add: assms(2)) |
|
538 also have "setsum f {a} < setsum g {a}" using a by simp |
|
539 also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})" |
|
540 using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto |
|
541 also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`]) |
|
542 finally show ?thesis by (metis add_right_mono add_strict_left_mono) |
|
543 qed |
|
544 |
526 lemma setsum_negf: |
545 lemma setsum_negf: |
527 "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A" |
546 "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A" |
528 proof (cases "finite A") |
547 proof (cases "finite A") |
529 case True thus ?thesis by (induct set: finite) auto |
548 case True thus ?thesis by (induct set: finite) auto |
530 next |
549 next |