# HG changeset patch
# User hoelzl
# Date 1266425857 -3600
# Node ID 28f824c7addc92ef5adae7822bb79fd9b9b8e6f4
# Parent  bb1d1c6a10bb642d3694194f39f620f1470796c9
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.

diff -r bb1d1c6a10bb -r 28f824c7addc src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Feb 17 09:22:40 2010 -0800
+++ b/src/HOL/Finite_Set.thy	Wed Feb 17 17:57:37 2010 +0100
@@ -2034,6 +2034,31 @@
   apply auto
 done
 
+lemma setprod_mono:
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
+  assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
+  shows "setprod f A \<le> setprod g A"
+proof (cases "finite A")
+  case True
+  hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
+  proof (induct A rule: finite_subset_induct)
+    case (insert a F)
+    thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
+      unfolding setprod_insert[OF insert(1,3)]
+      using assms[rule_format,OF insert(2)] insert
+      by (auto intro: mult_mono mult_nonneg_nonneg)
+  qed auto
+  thus ?thesis by simp
+qed auto
+
+lemma abs_setprod:
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
+  shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
+proof (cases "finite A")
+  case True thus ?thesis
+    by induct (auto simp add: field_simps setprod_insert abs_mult)
+qed auto
+
 
 subsection {* Finite cardinality *}
 
diff -r bb1d1c6a10bb -r 28f824c7addc src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Feb 17 09:22:40 2010 -0800
+++ b/src/HOL/SetInterval.thy	Wed Feb 17 17:57:37 2010 +0100
@@ -970,6 +970,27 @@
   finally show ?thesis .
 qed
 
+lemma setsum_le_included:
+  fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,ordered_ab_semigroup_add_imp_le}"
+  assumes "finite s" "finite t"
+  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)"
+  shows "setsum f s \<le> setsum g t"
+proof -
+  have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s"
+  proof (rule setsum_mono)
+    fix y assume "y \<in> s"
+    with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
+    with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
+      using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]
+      by (auto intro!: setsum_mono2)
+  qed
+  also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)"
+    using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)
+  also have "... \<le> setsum g t"
+    using assms by (auto simp: setsum_image_gen[symmetric])
+  finally show ?thesis .
+qed
+
 lemma setsum_multicount_gen:
   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
   shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")