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.52 -lemma measurable_add_dim:
    1.53 +lemma measurable_add_dim[measurable]:
    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.115 -qed (simp add: emeasure_PiM_empty)
   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 @@
   1.153      by (simp add: P_closed)
   1.154    show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
   1.155      using `finite I`
   1.156 -    by (auto intro!: sigma_sets_subset simp: E_generates P_def)
   1.157 +    by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
   1.158  qed
   1.159  
   1.160  end