src/HOL/SetInterval.thy
 changeset 35171 28f824c7addc parent 35115 446c5063e4fd child 35216 7641e8d831d2
```     1.1 --- a/src/HOL/SetInterval.thy	Wed Feb 17 09:22:40 2010 -0800
1.2 +++ b/src/HOL/SetInterval.thy	Wed Feb 17 17:57:37 2010 +0100
1.3 @@ -970,6 +970,27 @@
1.4    finally show ?thesis .
1.5  qed
1.6
1.7 +lemma setsum_le_included:
1.9 +  assumes "finite s" "finite t"
1.10 +  and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)"
1.11 +  shows "setsum f s \<le> setsum g t"
1.12 +proof -
1.13 +  have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s"
1.14 +  proof (rule setsum_mono)
1.15 +    fix y assume "y \<in> s"
1.16 +    with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
1.17 +    with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
1.18 +      using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]
1.19 +      by (auto intro!: setsum_mono2)
1.20 +  qed
1.21 +  also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)"
1.22 +    using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)
1.23 +  also have "... \<le> setsum g t"
1.24 +    using assms by (auto simp: setsum_image_gen[symmetric])
1.25 +  finally show ?thesis .
1.26 +qed
1.27 +
1.28  lemma setsum_multicount_gen:
1.29    assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
1.30    shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
```