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.8 +  fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,ordered_ab_semigroup_add_imp_le}"
     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")