integral over setprod
authorhoelzl
Wed Dec 08 16:15:14 2010 +0100 (2010-12-08)
changeset 41096843c40bbc379
parent 41095 c335d880ff82
child 41097 a1abfa4e2b44
integral over setprod
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Positive_Extended_Real.thy
src/HOL/Probability/Product_Measure.thy
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 16:15:14 2010 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 16:15:14 2010 +0100
     1.3 @@ -1347,6 +1347,16 @@
     1.4      by (auto intro!: measurable_If)
     1.5  qed
     1.6  
     1.7 +lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
     1.8 +  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
     1.9 +  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
    1.10 +  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
    1.11 +proof cases
    1.12 +  assume "finite S"
    1.13 +  thus ?thesis using assms
    1.14 +    by induct auto
    1.15 +qed (simp add: borel_measurable_const)
    1.16 +
    1.17  lemma (in sigma_algebra) borel_measurable_pextreal_times[intro, simp]:
    1.18    fixes f :: "'a \<Rightarrow> pextreal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
    1.19    shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
    1.20 @@ -1359,15 +1369,14 @@
    1.21      by (auto intro!: measurable_If)
    1.22  qed
    1.23  
    1.24 -lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
    1.25 +lemma (in sigma_algebra) borel_measurable_pextreal_setprod[simp, intro]:
    1.26    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
    1.27    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
    1.28 -  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
    1.29 +  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
    1.30  proof cases
    1.31    assume "finite S"
    1.32 -  thus ?thesis using assms
    1.33 -    by induct auto
    1.34 -qed (simp add: borel_measurable_const)
    1.35 +  thus ?thesis using assms by induct auto
    1.36 +qed simp
    1.37  
    1.38  lemma (in sigma_algebra) borel_measurable_pextreal_min[simp, intro]:
    1.39    fixes f g :: "'a \<Rightarrow> pextreal"
     2.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 08 16:15:14 2010 +0100
     2.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 08 16:15:14 2010 +0100
     2.3 @@ -1283,6 +1283,11 @@
     2.4    shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f"
     2.5    using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto
     2.6  
     2.7 +lemma (in measure_space) positive_integral_multc:
     2.8 +  assumes "f \<in> borel_measurable M"
     2.9 +  shows "positive_integral (\<lambda>x. f x * c) = positive_integral f * c"
    2.10 +  unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
    2.11 +
    2.12  lemma (in measure_space) positive_integral_indicator[simp]:
    2.13    "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A"
    2.14  by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
    2.15 @@ -1763,6 +1768,11 @@
    2.16    thus ?P ?I by auto
    2.17  qed
    2.18  
    2.19 +lemma (in measure_space) integral_multc:
    2.20 +  assumes "integrable f"
    2.21 +  shows "integral (\<lambda>x. f x * c) = integral f * c"
    2.22 +  unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
    2.23 +
    2.24  lemma (in measure_space) integral_mono_AE:
    2.25    assumes fg: "integrable f" "integrable g"
    2.26    and mono: "AE t. f t \<le> g t"
     3.1 --- a/src/HOL/Probability/Positive_Extended_Real.thy	Wed Dec 08 16:15:14 2010 +0100
     3.2 +++ b/src/HOL/Probability/Positive_Extended_Real.thy	Wed Dec 08 16:15:14 2010 +0100
     3.3 @@ -260,6 +260,9 @@
     3.4  qed
     3.5  end
     3.6  
     3.7 +lemma Real_minus_abs[simp]: "Real (- \<bar>x\<bar>) = 0"
     3.8 +  by simp
     3.9 +
    3.10  lemma pextreal_plus_eq_\<omega>[simp]: "(a :: pextreal) + b = \<omega> \<longleftrightarrow> a = \<omega> \<or> b = \<omega>"
    3.11    by (cases a, cases b) auto
    3.12  
     4.1 --- a/src/HOL/Probability/Product_Measure.thy	Wed Dec 08 16:15:14 2010 +0100
     4.2 +++ b/src/HOL/Probability/Product_Measure.thy	Wed Dec 08 16:15:14 2010 +0100
     4.3 @@ -1638,6 +1638,17 @@
     4.4    "product_integral I \<equiv>
     4.5      measure_space.integral (sigma (product_algebra M I)) (product_measure I)"
     4.6  
     4.7 +abbreviation (in product_sigma_finite)
     4.8 +  "product_integrable I \<equiv>
     4.9 +    measure_space.integrable (sigma (product_algebra M I)) (product_measure I)"
    4.10 +
    4.11 +lemma (in product_sigma_finite) product_measure_empty[simp]:
    4.12 +  "product_measure {} {\<lambda>x. undefined} = 1"
    4.13 +proof -
    4.14 +  interpret finite_product_sigma_finite M \<mu> "{}" by default auto
    4.15 +  from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
    4.16 +qed
    4.17 +
    4.18  lemma (in product_sigma_finite) positive_integral_empty:
    4.19    "product_positive_integral {} f = f (\<lambda>k. undefined)"
    4.20  proof -
    4.21 @@ -1776,6 +1787,59 @@
    4.22    qed simp
    4.23  qed
    4.24  
    4.25 +lemma (in product_sigma_finite) product_positive_integral_insert:
    4.26 +  assumes [simp]: "finite I" "i \<notin> I"
    4.27 +    and f: "f \<in> borel_measurable (sigma (product_algebra M (insert i I)))"
    4.28 +  shows "product_positive_integral (insert i I) f
    4.29 +    = product_positive_integral I (\<lambda>x. M.positive_integral i (\<lambda>y. f (x(i:=y))))"
    4.30 +proof -
    4.31 +  interpret I: finite_product_sigma_finite M \<mu> I by default auto
    4.32 +  interpret i: finite_product_sigma_finite M \<mu> "{i}" by default auto
    4.33 +  interpret P: pair_sigma_algebra I.P i.P ..
    4.34 +  have IJ: "I \<inter> {i} = {}" by auto
    4.35 +  show ?thesis
    4.36 +    unfolding product_positive_integral_fold[OF IJ, simplified, OF f]
    4.37 +  proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
    4.38 +    fix x assume x: "x \<in> space I.P"
    4.39 +    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
    4.40 +    have f'_eq: "\<And>y. ?f y = f (x(i := y))"
    4.41 +      using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
    4.42 +    note fP = f[unfolded measurable_merge_iff[OF IJ, simplified]]
    4.43 +    show "?f \<in> borel_measurable (M i)"
    4.44 +      using P.measurable_pair_image_snd[OF fP x]
    4.45 +      unfolding measurable_singleton f'_eq by (simp add: f'_eq)
    4.46 +    show "M.positive_integral i ?f = M.positive_integral i (\<lambda>y. f (x(i := y)))"
    4.47 +      unfolding f'_eq by simp
    4.48 +  qed
    4.49 +qed
    4.50 +
    4.51 +lemma (in product_sigma_finite) product_positive_integral_setprod:
    4.52 +  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> pextreal"
    4.53 +  assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
    4.54 +  shows "product_positive_integral I (\<lambda>x. (\<Prod>i\<in>I. f i (x i))) =
    4.55 +    (\<Prod>i\<in>I. M.positive_integral i (f i))"
    4.56 +using assms proof induct
    4.57 +  case empty
    4.58 +  interpret finite_product_sigma_finite M \<mu> "{}" by default auto
    4.59 +  then show ?case by simp
    4.60 +next
    4.61 +  case (insert i I)
    4.62 +  note `finite I`[intro, simp]
    4.63 +  interpret I: finite_product_sigma_finite M \<mu> I by default auto
    4.64 +  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))"
    4.65 +    using insert by (auto intro!: setprod_cong)
    4.66 +  have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
    4.67 +    (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (sigma (product_algebra M J))"
    4.68 +    using sets_into_space insert
    4.69 +    by (intro sigma_algebra.borel_measurable_pextreal_setprod
    4.70 +              sigma_algebra_sigma product_algebra_sets_into_space
    4.71 +              measurable_component)
    4.72 +       auto
    4.73 +  show ?case
    4.74 +    by (simp add: product_positive_integral_insert[OF insert(1,2) prod])
    4.75 +       (simp add: insert I.positive_integral_cmult M.positive_integral_multc * prod subset_insertI)
    4.76 +qed
    4.77 +
    4.78  lemma (in product_sigma_finite) product_integral_singleton:
    4.79    assumes f: "f \<in> borel_measurable (M i)"
    4.80    shows "product_integral {i} (\<lambda>x. f (x i)) = M.integral i f"
    4.81 @@ -1829,6 +1893,84 @@
    4.82      unfolding PI by simp
    4.83  qed
    4.84  
    4.85 +lemma (in product_sigma_finite) product_integral_insert:
    4.86 +  assumes [simp]: "finite I" "i \<notin> I"
    4.87 +    and f: "measure_space.integrable (sigma (product_algebra M (insert i I))) (product_measure (insert i I)) f"
    4.88 +  shows "product_integral (insert i I) f
    4.89 +    = product_integral I (\<lambda>x. M.integral i (\<lambda>y. f (x(i:=y))))"
    4.90 +proof -
    4.91 +  interpret I: finite_product_sigma_finite M \<mu> I by default auto
    4.92 +  interpret I': finite_product_sigma_finite M \<mu> "insert i I" by default auto
    4.93 +  interpret i: finite_product_sigma_finite M \<mu> "{i}" by default auto
    4.94 +  interpret P: pair_sigma_algebra I.P i.P ..
    4.95 +  have IJ: "I \<inter> {i} = {}" by auto
    4.96 +  show ?thesis
    4.97 +    unfolding product_integral_fold[OF IJ, simplified, OF f]
    4.98 +  proof (rule I.integral_cong, subst product_integral_singleton)
    4.99 +    fix x assume x: "x \<in> space I.P"
   4.100 +    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
   4.101 +    have f'_eq: "\<And>y. ?f y = f (x(i := y))"
   4.102 +      using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
   4.103 +    have "f \<in> borel_measurable I'.P" using f unfolding I'.integrable_def by auto
   4.104 +    note fP = this[unfolded measurable_merge_iff[OF IJ, simplified]]
   4.105 +    show "?f \<in> borel_measurable (M i)"
   4.106 +      using P.measurable_pair_image_snd[OF fP x]
   4.107 +      unfolding measurable_singleton f'_eq by (simp add: f'_eq)
   4.108 +    show "M.integral i ?f = M.integral i (\<lambda>y. f (x(i := y)))"
   4.109 +      unfolding f'_eq by simp
   4.110 +  qed
   4.111 +qed
   4.112 +
   4.113 +lemma (in product_sigma_finite) product_integrable_setprod:
   4.114 +  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   4.115 +  assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> M.integrable i (f i)"
   4.116 +  shows "product_integrable I (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "product_integrable I ?f")
   4.117 +proof -
   4.118 +  interpret finite_product_sigma_finite M \<mu> I by default fact
   4.119 +  have f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
   4.120 +    using integrable unfolding M.integrable_def by auto
   4.121 +  then have borel: "?f \<in> borel_measurable P"
   4.122 +    by (intro borel_measurable_setprod measurable_component) auto
   4.123 +  moreover have "integrable (\<lambda>x. \<bar>\<Prod>i\<in>I. f i (x i)\<bar>)"
   4.124 +  proof (unfold integrable_def, intro conjI)
   4.125 +    show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
   4.126 +      using borel by auto
   4.127 +    have "positive_integral (\<lambda>x. Real (abs (?f x))) =
   4.128 +      positive_integral (\<lambda>x. \<Prod>i\<in>I. Real (abs (f i (x i))))"
   4.129 +      by (simp add: Real_setprod abs_setprod)
   4.130 +    also have "\<dots> = (\<Prod>i\<in>I. M.positive_integral i (\<lambda>x. Real (abs (f i x))))"
   4.131 +      using f by (subst product_positive_integral_setprod) auto
   4.132 +    also have "\<dots> < \<omega>"
   4.133 +      using integrable[THEN M.integrable_abs]
   4.134 +      unfolding pextreal_less_\<omega> setprod_\<omega> M.integrable_def by simp
   4.135 +    finally show "positive_integral (\<lambda>x. Real (abs (?f x))) \<noteq> \<omega>" by auto
   4.136 +    show "positive_integral (\<lambda>x. Real (- abs (?f x))) \<noteq> \<omega>" by simp
   4.137 +  qed
   4.138 +  ultimately show ?thesis
   4.139 +    by (rule integrable_abs_iff[THEN iffD1])
   4.140 +qed
   4.141 +
   4.142 +lemma (in product_sigma_finite) product_integral_setprod:
   4.143 +  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   4.144 +  assumes "finite I" "I \<noteq> {}" and integrable: "\<And>i. i \<in> I \<Longrightarrow> M.integrable i (f i)"
   4.145 +  shows "product_integral I (\<lambda>x. (\<Prod>i\<in>I. f i (x i))) = (\<Prod>i\<in>I. M.integral i (f i))"
   4.146 +using assms proof (induct rule: finite_ne_induct)
   4.147 +  case (singleton i)
   4.148 +  then show ?case by (simp add: product_integral_singleton integrable_def)
   4.149 +next
   4.150 +  case (insert i I)
   4.151 +  then have iI: "finite (insert i I)" by auto
   4.152 +  then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
   4.153 +    product_integrable J (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
   4.154 +    by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset)
   4.155 +  interpret I: finite_product_sigma_finite M \<mu> I by default fact
   4.156 +  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))"
   4.157 +    using `i \<notin> I` by (auto intro!: setprod_cong)
   4.158 +  show ?case
   4.159 +    unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
   4.160 +    by (simp add: * insert integral_multc I.integral_cmult[OF prod] subset_insertI)
   4.161 +qed
   4.162 +
   4.163  section "Products on finite spaces"
   4.164  
   4.165  lemma sigma_sets_pair_algebra_finite: