src/HOL/Probability/Infinite_Product_Measure.thy
changeset 49780 92a58f80b20c
parent 49776 199d1d5bb17e
child 49784 5e5b2da42a69
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:20 2012 +0200
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:21 2012 +0200
     1.3 @@ -14,10 +14,10 @@
     1.4  lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
     1.5    unfolding restrict_def by (simp add: fun_eq_iff)
     1.6  
     1.7 -lemma split_merge: "P (merge I x J y i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
     1.8 +lemma split_merge: "P (merge I J (x,y) i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
     1.9    unfolding merge_def by auto
    1.10  
    1.11 -lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I x J y \<in> extensional K"
    1.12 +lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I J (x, y) \<in> extensional K"
    1.13    unfolding merge_def extensional_def by auto
    1.14  
    1.15  lemma injective_vimage_restrict:
    1.16 @@ -32,7 +32,7 @@
    1.17    show "x \<in> A \<longleftrightarrow> x \<in> B"
    1.18    proof cases
    1.19      assume x: "x \<in> (\<Pi>\<^isub>E i\<in>J. S i)"
    1.20 -    have "x \<in> A \<longleftrightarrow> merge J x (I - J) y \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
    1.21 +    have "x \<in> A \<longleftrightarrow> merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
    1.22        using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub split: split_merge)
    1.23      then show "x \<in> A \<longleftrightarrow> x \<in> B"
    1.24        using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub eq split: split_merge)
    1.25 @@ -131,7 +131,7 @@
    1.26    show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
    1.27      using sets[THEN sets_into_space] by (auto simp: space_PiM)
    1.28    have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
    1.29 -    using M.not_empty by auto
    1.30 +      using M.not_empty by auto
    1.31    from bchoice[OF this]
    1.32    show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
    1.33    show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))"
    1.34 @@ -230,23 +230,19 @@
    1.35  qed
    1.36  
    1.37  lemma (in product_prob_space) merge_sets:
    1.38 -  assumes "finite J" "finite K" "J \<inter> K = {}" and A: "A \<in> sets (Pi\<^isub>M (J \<union> K) M)" and x: "x \<in> space (Pi\<^isub>M J M)"
    1.39 -  shows "merge J x K -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
    1.40 -proof -
    1.41 -  from sets_Pair1[OF
    1.42 -    measurable_merge[THEN measurable_sets, OF `J \<inter> K = {}`], OF A, of x] x
    1.43 -  show ?thesis
    1.44 -      by (simp add: space_pair_measure comp_def vimage_compose[symmetric])
    1.45 -qed
    1.46 +  assumes "J \<inter> K = {}" and A: "A \<in> sets (Pi\<^isub>M (J \<union> K) M)" and x: "x \<in> space (Pi\<^isub>M J M)"
    1.47 +  shows "(\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
    1.48 +  by (rule measurable_sets[OF _ A] measurable_compose[OF measurable_Pair measurable_merge]  
    1.49 +           measurable_const x measurable_ident)+
    1.50  
    1.51  lemma (in product_prob_space) merge_emb:
    1.52    assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M J M)"
    1.53 -  shows "(merge J y (I - J) -` emb I K X \<inter> space (Pi\<^isub>M I M)) =
    1.54 -    emb I (K - J) (merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M))"
    1.55 +  shows "((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) =
    1.56 +    emb I (K - J) ((\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M))"
    1.57  proof -
    1.58 -  have [simp]: "\<And>x J K L. merge J y K (restrict x L) = merge J y (K \<inter> L) x"
    1.59 +  have [simp]: "\<And>x J K L. merge J K (y, restrict x L) = merge J (K \<inter> L) (y, x)"
    1.60      by (auto simp: restrict_def merge_def)
    1.61 -  have [simp]: "\<And>x J K L. restrict (merge J y K x) L = merge (J \<inter> L) y (K \<inter> L) x"
    1.62 +  have [simp]: "\<And>x J K L. restrict (merge J K (y, x)) L = merge (J \<inter> L) (K \<inter> L) (y, x)"
    1.63      by (auto simp: restrict_def merge_def)
    1.64    have [simp]: "(I - J) \<inter> K = K - J" using `K \<subseteq> I` `J \<subseteq> I` by auto
    1.65    have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
    1.66 @@ -331,16 +327,16 @@
    1.67        "K - J \<noteq> {}" "K - J \<subseteq> I" "\<mu>G Z = emeasure (Pi\<^isub>M K M) X"
    1.68        by (auto simp: subset_insertI)
    1.69  
    1.70 -    let ?M = "\<lambda>y. merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
    1.71 +    let ?M = "\<lambda>y. (\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
    1.72      { fix y assume y: "y \<in> space (Pi\<^isub>M J M)"
    1.73        note * = merge_emb[OF `K \<subseteq> I` `J \<subseteq> I` y, of X]
    1.74        moreover
    1.75        have **: "?M y \<in> sets (Pi\<^isub>M (K - J) M)"
    1.76          using J K y by (intro merge_sets) auto
    1.77        ultimately
    1.78 -      have ***: "(merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M)) \<in> ?G"
    1.79 +      have ***: "((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)) \<in> ?G"
    1.80          using J K by (intro generatorI) auto
    1.81 -      have "\<mu>G (merge J y (I - J) -` emb I K X \<inter> space (Pi\<^isub>M I M)) = emeasure (Pi\<^isub>M (K - J) M) (?M y)"
    1.82 +      have "\<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) = emeasure (Pi\<^isub>M (K - J) M) (?M y)"
    1.83          unfolding * using K J by (subst \<mu>G_eq[OF _ _ _ **]) auto
    1.84        note * ** *** this }
    1.85      note merge_in_G = this
    1.86 @@ -354,7 +350,7 @@
    1.87        using K J by simp
    1.88      also have "\<dots> = (\<integral>\<^isup>+ x. emeasure (Pi\<^isub>M (K - J) M) (?M x) \<partial>Pi\<^isub>M J M)"
    1.89        using K J by (subst emeasure_fold_integral) auto
    1.90 -    also have "\<dots> = (\<integral>\<^isup>+ y. \<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M)) \<partial>Pi\<^isub>M J M)"
    1.91 +    also have "\<dots> = (\<integral>\<^isup>+ y. \<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)) \<partial>Pi\<^isub>M J M)"
    1.92        (is "_ = (\<integral>\<^isup>+x. \<mu>G (?MZ x) \<partial>Pi\<^isub>M J M)")
    1.93      proof (intro positive_integral_cong)
    1.94        fix x assume x: "x \<in> space (Pi\<^isub>M J M)"
    1.95 @@ -370,7 +366,7 @@
    1.96          by (intro KmJ.measure_le_1 merge_in_G(2)[OF x]) }
    1.97      note le_1 = this
    1.98  
    1.99 -    let ?q = "\<lambda>y. \<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M))"
   1.100 +    let ?q = "\<lambda>y. \<mu>G ((\<lambda>x. merge J (I - J) (y,x)) -` Z \<inter> space (Pi\<^isub>M I M))"
   1.101      have "?q \<in> borel_measurable (Pi\<^isub>M J M)"
   1.102        unfolding `Z = emb I K X` using J K merge_in_G(3)
   1.103        by (simp add: merge_in_G  \<mu>G_eq emeasure_fold_measurable cong: measurable_cong)
   1.104 @@ -416,7 +412,7 @@
   1.105          using \<mu>G_spec[of "J 0" "A 0" "X 0"] J A_eq
   1.106          by (auto intro!: INF_lower2[of 0] J.measure_le_1)
   1.107  
   1.108 -      let ?M = "\<lambda>K Z y. merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
   1.109 +      let ?M = "\<lambda>K Z y. (\<lambda>x. merge K (I - K) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)"
   1.110  
   1.111        { fix Z k assume Z: "range Z \<subseteq> ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
   1.112          then have Z_sets: "\<And>n. Z n \<in> ?G" by auto
   1.113 @@ -524,9 +520,9 @@
   1.114              from Ex_w[OF this `?D \<noteq> {}`] J[of "Suc k"]
   1.115              obtain w' where w': "w' \<in> space (Pi\<^isub>M ?D M)"
   1.116                "\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> \<mu>G (?M ?D (?M (J k) (A n) (w k)) w')" by auto
   1.117 -            let ?w = "merge (J k) (w k) ?D w'"
   1.118 -            have [simp]: "\<And>x. merge (J k) (w k) (I - J k) (merge ?D w' (I - ?D) x) =
   1.119 -              merge (J (Suc k)) ?w (I - (J (Suc k))) x"
   1.120 +            let ?w = "merge (J k) ?D (w k, w')"
   1.121 +            have [simp]: "\<And>x. merge (J k) (I - J k) (w k, merge ?D (I - ?D) (w', x)) =
   1.122 +              merge (J (Suc k)) (I - (J (Suc k))) (?w, x)"
   1.123                using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"]
   1.124                by (auto intro!: ext split: split_merge)
   1.125              have *: "\<And>n. ?M ?D (?M (J k) (A n) (w k)) w' = ?M (J (Suc k)) (A n) ?w"
   1.126 @@ -552,7 +548,7 @@
   1.127            using positive_\<mu>G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1`
   1.128            by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq)
   1.129          then obtain x where "x \<in> ?M (J k) (A k) (w k)" by auto
   1.130 -        then have "merge (J k) (w k) (I - J k) x \<in> A k" by auto
   1.131 +        then have "merge (J k) (I - J k) (w k, x) \<in> A k" by auto
   1.132          then have "\<exists>x\<in>A k. restrict x (J k) = w k"
   1.133            using `w k \<in> space (Pi\<^isub>M (J k) M)`
   1.134            by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM)