src/HOL/Probability/Finite_Product_Measure.thy
 changeset 50003 8c213922ed49 parent 49999 dfb63b9b8908 child 50021 d96a3f468203
```     1.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
1.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
1.3 @@ -56,7 +56,7 @@
1.4
1.5  lemma merge_commute:
1.6    "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)"
1.7 -  by (auto simp: merge_def intro!: ext)
1.8 +  by (force simp: merge_def)
1.9
1.10  lemma Pi_cancel_merge_range[simp]:
1.11    "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
1.12 @@ -430,7 +430,7 @@
1.13      by (auto simp add: sets_PiM intro!: sigma_sets_top)
1.14  next
1.15    assume "J \<noteq> {}" with assms show ?thesis
1.16 -    by (auto simp add: sets_PiM prod_algebra_def intro!: sigma_sets.Basic)
1.17 +    by (force simp add: sets_PiM prod_algebra_def)
1.18  qed
1.19
1.20  lemma measurable_PiM:
1.21 @@ -475,24 +475,12 @@
1.22    finally show "f -` A \<inter> space N \<in> sets N" .
1.23  qed (auto simp: space)
1.24
1.25 -lemma sets_PiM_I_finite[simp, intro]:
1.26 +lemma sets_PiM_I_finite[measurable]:
1.27    assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
1.28    shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
1.29    using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto
1.30
1.31 -lemma measurable_component_update:
1.32 -  assumes "x \<in> space (Pi\<^isub>M I M)" and "i \<notin> I"
1.33 -  shows "(\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \<in> _")
1.34 -proof (intro measurable_PiM_single)
1.35 -  fix j A assume "j \<in> insert i I" "A \<in> sets (M j)"
1.36 -  moreover have "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} =
1.37 -    (if i = j then space (M i) \<inter> A else if x j \<in> A then space (M i) else {})"
1.38 -    by auto
1.39 -  ultimately show "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} \<in> sets (M i)"
1.40 -    by auto
1.41 -qed (insert sets_into_space assms, auto simp: space_PiM)
1.42 -
1.43 -lemma measurable_component_singleton:
1.44 +lemma measurable_component_singleton[measurable (raw)]:
1.45    assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
1.46  proof (unfold measurable_def, intro CollectI conjI ballI)
1.47    fix A assume "A \<in> sets (M i)"
1.48 @@ -503,7 +491,7 @@
1.49      using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
1.50  qed (insert `i \<in> I`, auto simp: space_PiM)
1.51
1.54    "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
1.55      (is "?f \<in> measurable ?P ?I")
1.56  proof (rule measurable_PiM_single)
1.57 @@ -517,7 +505,11 @@
1.58    finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
1.59  qed (auto simp: space_pair_measure space_PiM)
1.60
1.61 -lemma measurable_merge:
1.62 +lemma measurable_component_update:
1.63 +  "x \<in> space (Pi\<^isub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)"
1.64 +  by simp
1.65 +
1.66 +lemma measurable_merge[measurable]:
1.67    "merge I J \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
1.68      (is "?f \<in> measurable ?P ?U")
1.69  proof (rule measurable_PiM_single)
1.70 @@ -531,7 +523,7 @@
1.71    finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
1.72  qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
1.73
1.74 -lemma measurable_restrict:
1.75 +lemma measurable_restrict[measurable (raw)]:
1.76    assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
1.77    shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^isub>M I M)"
1.78  proof (rule measurable_PiM_single)
1.79 @@ -542,6 +534,31 @@
1.80      using A X by (auto intro!: measurable_sets)
1.81  qed (insert X, auto dest: measurable_space)
1.82
1.83 +lemma sets_in_Pi_aux:
1.84 +  "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
1.85 +  {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
1.86 +  by (simp add: subset_eq Pi_iff)
1.87 +
1.88 +lemma sets_in_Pi[measurable (raw)]:
1.89 +  "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
1.90 +  (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
1.91 +  Sigma_Algebra.pred N (\<lambda>x. f x \<in> Pi I F)"
1.92 +  unfolding pred_def
1.93 +  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
1.94 +
1.95 +lemma sets_in_extensional_aux:
1.96 +  "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
1.97 +proof -
1.98 +  have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
1.99 +    by (auto simp add: extensional_def space_PiM)
1.100 +  then show ?thesis by simp
1.101 +qed
1.102 +
1.103 +lemma sets_in_extensional[measurable (raw)]:
1.104 +  "f \<in> measurable N (PiM I M) \<Longrightarrow> Sigma_Algebra.pred N (\<lambda>x. f x \<in> extensional I)"
1.105 +  unfolding pred_def
1.106 +  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
1.107 +
1.108  locale product_sigma_finite =
1.109    fixes M :: "'i \<Rightarrow> 'a measure"
1.110    assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
1.111 @@ -665,7 +682,7 @@
1.112    qed (auto intro!: setprod_cong)
1.113    with insert show ?case
1.114      by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
1.116 +qed simp
1.117
1.118  lemma (in product_sigma_finite) sigma_finite:
1.119    assumes "finite I"
1.120 @@ -759,18 +776,18 @@
1.121      show "emeasure ?P (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
1.122    next
1.123      fix A assume A: "A \<in> prod_algebra (I \<union> J) M"
1.124 -    with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>I \<union> J. F i \<in> sets (M i)"
1.125 +    with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>J. F i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
1.126        by (auto simp add: prod_algebra_eq_finite)
1.127      let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M"
1.128      let ?X = "?g -` A \<inter> space ?B"
1.129      have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)"
1.130 -      using F[rule_format, THEN sets_into_space] by (auto simp: space_PiM)
1.131 +      using F[rule_format, THEN sets_into_space] by (force simp: space_PiM)+
1.132      then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
1.133        unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
1.134      have "emeasure ?D A = emeasure ?B ?X"
1.135        using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
1.136      also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
1.137 -      using `finite J` `finite I` F X
1.138 +      using `finite J` `finite I` F unfolding X
1.139        by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
1.140      also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
1.141        using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
1.142 @@ -1013,8 +1030,7 @@
1.143
1.144  lemma sets_Collect_single:
1.145    "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^isub>M I M). x i \<in> A } \<in> sets (Pi\<^isub>M I M)"
1.146 -  unfolding sets_PiM_single
1.147 -  by (auto intro!: sigma_sets.Basic exI[of _ i] exI[of _ A]) (auto simp: space_PiM)
1.148 +  by simp
1.149
1.150  lemma sigma_prod_algebra_sigma_eq_infinite:
1.151    fixes E :: "'i \<Rightarrow> 'a set set"
1.152 @@ -1127,7 +1143,7 @@