author hoelzl Wed Dec 08 16:15:14 2010 +0100 (2010-12-08) changeset 41096 843c40bbc379 parent 41095 c335d880ff82 child 41097 a1abfa4e2b44
integral over setprod
```     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.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.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:
```