# HG changeset patch
# User hoelzl
# Date 1291821314 -3600
# Node ID 843c40bbc37903bfce15fbc5534655e2c19d840e
# Parent  c335d880ff8230c075d93c709f6c79f19eff8602
integral over setprod

diff -r c335d880ff82 -r 843c40bbc379 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 16:15:14 2010 +0100
@@ -1347,6 +1347,16 @@
     by (auto intro!: measurable_If)
 qed
 
+lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
+  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
+  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
+  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
+proof cases
+  assume "finite S"
+  thus ?thesis using assms
+    by induct auto
+qed (simp add: borel_measurable_const)
+
 lemma (in sigma_algebra) borel_measurable_pextreal_times[intro, simp]:
   fixes f :: "'a \<Rightarrow> pextreal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
@@ -1359,15 +1369,14 @@
     by (auto intro!: measurable_If)
 qed
 
-lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
+lemma (in sigma_algebra) borel_measurable_pextreal_setprod[simp, intro]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
-  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
+  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
 proof cases
   assume "finite S"
-  thus ?thesis using assms
-    by induct auto
-qed (simp add: borel_measurable_const)
+  thus ?thesis using assms by induct auto
+qed simp
 
 lemma (in sigma_algebra) borel_measurable_pextreal_min[simp, intro]:
   fixes f g :: "'a \<Rightarrow> pextreal"
diff -r c335d880ff82 -r 843c40bbc379 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 08 16:15:14 2010 +0100
@@ -1283,6 +1283,11 @@
   shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f"
   using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto
 
+lemma (in measure_space) positive_integral_multc:
+  assumes "f \<in> borel_measurable M"
+  shows "positive_integral (\<lambda>x. f x * c) = positive_integral f * c"
+  unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
+
 lemma (in measure_space) positive_integral_indicator[simp]:
   "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A"
 by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
@@ -1763,6 +1768,11 @@
   thus ?P ?I by auto
 qed
 
+lemma (in measure_space) integral_multc:
+  assumes "integrable f"
+  shows "integral (\<lambda>x. f x * c) = integral f * c"
+  unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
+
 lemma (in measure_space) integral_mono_AE:
   assumes fg: "integrable f" "integrable g"
   and mono: "AE t. f t \<le> g t"
diff -r c335d880ff82 -r 843c40bbc379 src/HOL/Probability/Positive_Extended_Real.thy
--- a/src/HOL/Probability/Positive_Extended_Real.thy	Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Positive_Extended_Real.thy	Wed Dec 08 16:15:14 2010 +0100
@@ -260,6 +260,9 @@
 qed
 end
 
+lemma Real_minus_abs[simp]: "Real (- \<bar>x\<bar>) = 0"
+  by simp
+
 lemma pextreal_plus_eq_\<omega>[simp]: "(a :: pextreal) + b = \<omega> \<longleftrightarrow> a = \<omega> \<or> b = \<omega>"
   by (cases a, cases b) auto
 
diff -r c335d880ff82 -r 843c40bbc379 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Wed Dec 08 16:15:14 2010 +0100
@@ -1638,6 +1638,17 @@
   "product_integral I \<equiv>
     measure_space.integral (sigma (product_algebra M I)) (product_measure I)"
 
+abbreviation (in product_sigma_finite)
+  "product_integrable I \<equiv>
+    measure_space.integrable (sigma (product_algebra M I)) (product_measure I)"
+
+lemma (in product_sigma_finite) product_measure_empty[simp]:
+  "product_measure {} {\<lambda>x. undefined} = 1"
+proof -
+  interpret finite_product_sigma_finite M \<mu> "{}" by default auto
+  from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
+qed
+
 lemma (in product_sigma_finite) positive_integral_empty:
   "product_positive_integral {} f = f (\<lambda>k. undefined)"
 proof -
@@ -1776,6 +1787,59 @@
   qed simp
 qed
 
+lemma (in product_sigma_finite) product_positive_integral_insert:
+  assumes [simp]: "finite I" "i \<notin> I"
+    and f: "f \<in> borel_measurable (sigma (product_algebra M (insert i I)))"
+  shows "product_positive_integral (insert i I) f
+    = product_positive_integral I (\<lambda>x. M.positive_integral i (\<lambda>y. f (x(i:=y))))"
+proof -
+  interpret I: finite_product_sigma_finite M \<mu> I by default auto
+  interpret i: finite_product_sigma_finite M \<mu> "{i}" by default auto
+  interpret P: pair_sigma_algebra I.P i.P ..
+  have IJ: "I \<inter> {i} = {}" by auto
+  show ?thesis
+    unfolding product_positive_integral_fold[OF IJ, simplified, OF f]
+  proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
+    fix x assume x: "x \<in> space I.P"
+    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
+    have f'_eq: "\<And>y. ?f y = f (x(i := y))"
+      using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
+    note fP = f[unfolded measurable_merge_iff[OF IJ, simplified]]
+    show "?f \<in> borel_measurable (M i)"
+      using P.measurable_pair_image_snd[OF fP x]
+      unfolding measurable_singleton f'_eq by (simp add: f'_eq)
+    show "M.positive_integral i ?f = M.positive_integral i (\<lambda>y. f (x(i := y)))"
+      unfolding f'_eq by simp
+  qed
+qed
+
+lemma (in product_sigma_finite) product_positive_integral_setprod:
+  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> pextreal"
+  assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
+  shows "product_positive_integral I (\<lambda>x. (\<Prod>i\<in>I. f i (x i))) =
+    (\<Prod>i\<in>I. M.positive_integral i (f i))"
+using assms proof induct
+  case empty
+  interpret finite_product_sigma_finite M \<mu> "{}" by default auto
+  then show ?case by simp
+next
+  case (insert i I)
+  note `finite I`[intro, simp]
+  interpret I: finite_product_sigma_finite M \<mu> I by default auto
+  have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
+    using insert by (auto intro!: setprod_cong)
+  have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
+    (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (sigma (product_algebra M J))"
+    using sets_into_space insert
+    by (intro sigma_algebra.borel_measurable_pextreal_setprod
+              sigma_algebra_sigma product_algebra_sets_into_space
+              measurable_component)
+       auto
+  show ?case
+    by (simp add: product_positive_integral_insert[OF insert(1,2) prod])
+       (simp add: insert I.positive_integral_cmult M.positive_integral_multc * prod subset_insertI)
+qed
+
 lemma (in product_sigma_finite) product_integral_singleton:
   assumes f: "f \<in> borel_measurable (M i)"
   shows "product_integral {i} (\<lambda>x. f (x i)) = M.integral i f"
@@ -1829,6 +1893,84 @@
     unfolding PI by simp
 qed
 
+lemma (in product_sigma_finite) product_integral_insert:
+  assumes [simp]: "finite I" "i \<notin> I"
+    and f: "measure_space.integrable (sigma (product_algebra M (insert i I))) (product_measure (insert i I)) f"
+  shows "product_integral (insert i I) f
+    = product_integral I (\<lambda>x. M.integral i (\<lambda>y. f (x(i:=y))))"
+proof -
+  interpret I: finite_product_sigma_finite M \<mu> I by default auto
+  interpret I': finite_product_sigma_finite M \<mu> "insert i I" by default auto
+  interpret i: finite_product_sigma_finite M \<mu> "{i}" by default auto
+  interpret P: pair_sigma_algebra I.P i.P ..
+  have IJ: "I \<inter> {i} = {}" by auto
+  show ?thesis
+    unfolding product_integral_fold[OF IJ, simplified, OF f]
+  proof (rule I.integral_cong, subst product_integral_singleton)
+    fix x assume x: "x \<in> space I.P"
+    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
+    have f'_eq: "\<And>y. ?f y = f (x(i := y))"
+      using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
+    have "f \<in> borel_measurable I'.P" using f unfolding I'.integrable_def by auto
+    note fP = this[unfolded measurable_merge_iff[OF IJ, simplified]]
+    show "?f \<in> borel_measurable (M i)"
+      using P.measurable_pair_image_snd[OF fP x]
+      unfolding measurable_singleton f'_eq by (simp add: f'_eq)
+    show "M.integral i ?f = M.integral i (\<lambda>y. f (x(i := y)))"
+      unfolding f'_eq by simp
+  qed
+qed
+
+lemma (in product_sigma_finite) product_integrable_setprod:
+  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
+  assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> M.integrable i (f i)"
+  shows "product_integrable I (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "product_integrable I ?f")
+proof -
+  interpret finite_product_sigma_finite M \<mu> I by default fact
+  have f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
+    using integrable unfolding M.integrable_def by auto
+  then have borel: "?f \<in> borel_measurable P"
+    by (intro borel_measurable_setprod measurable_component) auto
+  moreover have "integrable (\<lambda>x. \<bar>\<Prod>i\<in>I. f i (x i)\<bar>)"
+  proof (unfold integrable_def, intro conjI)
+    show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
+      using borel by auto
+    have "positive_integral (\<lambda>x. Real (abs (?f x))) =
+      positive_integral (\<lambda>x. \<Prod>i\<in>I. Real (abs (f i (x i))))"
+      by (simp add: Real_setprod abs_setprod)
+    also have "\<dots> = (\<Prod>i\<in>I. M.positive_integral i (\<lambda>x. Real (abs (f i x))))"
+      using f by (subst product_positive_integral_setprod) auto
+    also have "\<dots> < \<omega>"
+      using integrable[THEN M.integrable_abs]
+      unfolding pextreal_less_\<omega> setprod_\<omega> M.integrable_def by simp
+    finally show "positive_integral (\<lambda>x. Real (abs (?f x))) \<noteq> \<omega>" by auto
+    show "positive_integral (\<lambda>x. Real (- abs (?f x))) \<noteq> \<omega>" by simp
+  qed
+  ultimately show ?thesis
+    by (rule integrable_abs_iff[THEN iffD1])
+qed
+
+lemma (in product_sigma_finite) product_integral_setprod:
+  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
+  assumes "finite I" "I \<noteq> {}" and integrable: "\<And>i. i \<in> I \<Longrightarrow> M.integrable i (f i)"
+  shows "product_integral I (\<lambda>x. (\<Prod>i\<in>I. f i (x i))) = (\<Prod>i\<in>I. M.integral i (f i))"
+using assms proof (induct rule: finite_ne_induct)
+  case (singleton i)
+  then show ?case by (simp add: product_integral_singleton integrable_def)
+next
+  case (insert i I)
+  then have iI: "finite (insert i I)" by auto
+  then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
+    product_integrable J (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
+    by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset)
+  interpret I: finite_product_sigma_finite M \<mu> I by default fact
+  have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
+    using `i \<notin> I` by (auto intro!: setprod_cong)
+  show ?case
+    unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
+    by (simp add: * insert integral_multc I.integral_cmult[OF prod] subset_insertI)
+qed
+
 section "Products on finite spaces"
 
 lemma sigma_sets_pair_algebra_finite: