src/HOL/Probability/Projective_Family.thy
changeset 50095 94d7dfa9f404
parent 50087 635d73673b5e
child 50101 a3bede207a04
     1.1 --- a/src/HOL/Probability/Projective_Family.thy	Fri Nov 16 11:22:22 2012 +0100
     1.2 +++ b/src/HOL/Probability/Projective_Family.thy	Fri Nov 16 11:34:34 2012 +0100
     1.3 @@ -57,22 +57,24 @@
     1.4       (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
     1.5  
     1.6  definition
     1.7 -  PiP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
     1.8 -  "PiP I M P = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
     1.9 +  limP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
    1.10 +  "limP I M P = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
    1.11      {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
    1.12      (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^isub>E j\<in>J. X j))
    1.13      (\<lambda>(J, X). emeasure (P J) (Pi\<^isub>E J X))"
    1.14  
    1.15 -lemma space_PiP[simp]: "space (PiP I M P) = space (PiM I M)"
    1.16 -  by (auto simp add: PiP_def space_PiM prod_emb_def intro!: space_extend_measure)
    1.17 +abbreviation "lim\<^isub>P \<equiv> limP"
    1.18 +
    1.19 +lemma space_limP[simp]: "space (limP I M P) = space (PiM I M)"
    1.20 +  by (auto simp add: limP_def space_PiM prod_emb_def intro!: space_extend_measure)
    1.21  
    1.22 -lemma sets_PiP[simp]: "sets (PiP I M P) = sets (PiM I M)"
    1.23 -  by (auto simp add: PiP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure)
    1.24 +lemma sets_limP[simp]: "sets (limP I M P) = sets (PiM I M)"
    1.25 +  by (auto simp add: limP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure)
    1.26  
    1.27 -lemma measurable_PiP1[simp]: "measurable (PiP I M P) M' = measurable (\<Pi>\<^isub>M i\<in>I. M i) M'"
    1.28 +lemma measurable_limP1[simp]: "measurable (limP I M P) M' = measurable (\<Pi>\<^isub>M i\<in>I. M i) M'"
    1.29    unfolding measurable_def by auto
    1.30  
    1.31 -lemma measurable_PiP2[simp]: "measurable M' (PiP I M P) = measurable M' (\<Pi>\<^isub>M i\<in>I. M i)"
    1.32 +lemma measurable_limP2[simp]: "measurable M' (limP I M P) = measurable M' (\<Pi>\<^isub>M i\<in>I. M i)"
    1.33    unfolding measurable_def by auto
    1.34  
    1.35  locale projective_family =
    1.36 @@ -84,11 +86,11 @@
    1.37    assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
    1.38  begin
    1.39  
    1.40 -lemma emeasure_PiP:
    1.41 +lemma emeasure_limP:
    1.42    assumes "finite J"
    1.43    assumes "J \<subseteq> I"
    1.44    assumes A: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> sets (M i)"
    1.45 -  shows "emeasure (PiP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
    1.46 +  shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
    1.47  proof -
    1.48    have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
    1.49    proof safe
    1.50 @@ -97,13 +99,13 @@
    1.51      also have "\<dots> \<subseteq> space (M j)" using sets_into_space A `j \<in> J` by auto
    1.52      finally show "x j \<in> space (M j)" .
    1.53    qed
    1.54 -  hence "emeasure (PiP J M P) (Pi\<^isub>E J A) =
    1.55 -    emeasure (PiP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
    1.56 +  hence "emeasure (limP J M P) (Pi\<^isub>E J A) =
    1.57 +    emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
    1.58      using assms(1-3) sets_into_space by (auto simp add: prod_emb_id Pi_def)
    1.59    also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
    1.60 -  proof (rule emeasure_extend_measure_Pair[OF PiP_def])
    1.61 -    show "positive (sets (PiP J M P)) (P J)" unfolding positive_def by auto
    1.62 -    show "countably_additive (sets (PiP J M P)) (P J)" unfolding countably_additive_def
    1.63 +  proof (rule emeasure_extend_measure_Pair[OF limP_def])
    1.64 +    show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
    1.65 +    show "countably_additive (sets (limP J M P)) (P J)" unfolding countably_additive_def
    1.66        by (auto simp: suminf_emeasure proj_sets[OF `finite J`])
    1.67      show "(J \<noteq> {} \<or> J = {}) \<and> finite J \<and> J \<subseteq> J \<and> A \<in> (\<Pi> j\<in>J. sets (M j))"
    1.68        using assms by auto
    1.69 @@ -121,10 +123,10 @@
    1.70    finally show ?thesis .
    1.71  qed
    1.72  
    1.73 -lemma PiP_finite:
    1.74 +lemma limP_finite:
    1.75    assumes "finite J"
    1.76    assumes "J \<subseteq> I"
    1.77 -  shows "PiP J M P = P J" (is "?P = _")
    1.78 +  shows "limP J M P = P J" (is "?P = _")
    1.79  proof (rule measure_eqI_generator_eq)
    1.80    let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
    1.81    let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
    1.82 @@ -132,26 +134,26 @@
    1.83    show "Int_stable ?J"
    1.84      by (rule Int_stable_PiE)
    1.85    interpret prob_space "P J" using prob_space `finite J` by simp
    1.86 -  show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_PiP)
    1.87 +  show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
    1.88    show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
    1.89 -  show "sets (PiP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
    1.90 +  show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
    1.91      using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
    1.92    fix X assume "X \<in> ?J"
    1.93    then obtain E where X: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
    1.94 -  with `finite J` have "X \<in> sets (PiP J M P)" by simp
    1.95 +  with `finite J` have "X \<in> sets (limP J M P)" by simp
    1.96    have emb_self: "prod_emb J M J (Pi\<^isub>E J E) = Pi\<^isub>E J E"
    1.97      using E sets_into_space
    1.98      by (auto intro!: prod_emb_PiE_same_index)
    1.99 -  show "emeasure (PiP J M P) X = emeasure (P J) X"
   1.100 +  show "emeasure (limP J M P) X = emeasure (P J) X"
   1.101      unfolding X using E
   1.102 -    by (intro emeasure_PiP assms) simp
   1.103 +    by (intro emeasure_limP assms) simp
   1.104  qed (insert `finite J`, auto intro!: prod_algebraI_finite)
   1.105  
   1.106  lemma emeasure_fun_emb[simp]:
   1.107    assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
   1.108 -  shows "emeasure (PiP L M P) (prod_emb L M J X) = emeasure (PiP J M P) X"
   1.109 +  shows "emeasure (limP L M P) (prod_emb L M J X) = emeasure (limP J M P) X"
   1.110    using assms
   1.111 -  by (subst PiP_finite) (auto simp: PiP_finite finite_subset projective)
   1.112 +  by (subst limP_finite) (auto simp: limP_finite finite_subset projective)
   1.113  
   1.114  lemma prod_emb_injective:
   1.115    assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
   1.116 @@ -235,30 +237,30 @@
   1.117  
   1.118  definition
   1.119    "\<mu>G A =
   1.120 -    (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = emeasure (PiP J M P) X))"
   1.121 +    (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = emeasure (limP J M P) X))"
   1.122  
   1.123  lemma \<mu>G_spec:
   1.124    assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
   1.125 -  shows "\<mu>G A = emeasure (PiP J M P) X"
   1.126 +  shows "\<mu>G A = emeasure (limP J M P) X"
   1.127    unfolding \<mu>G_def
   1.128  proof (intro the_equality allI impI ballI)
   1.129    fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^isub>M K M)"
   1.130 -  have "emeasure (PiP K M P) Y = emeasure (PiP (K \<union> J) M P) (emb (K \<union> J) K Y)"
   1.131 +  have "emeasure (limP K M P) Y = emeasure (limP (K \<union> J) M P) (emb (K \<union> J) K Y)"
   1.132      using K J by simp
   1.133    also have "emb (K \<union> J) K Y = emb (K \<union> J) J X"
   1.134      using K J by (simp add: prod_emb_injective[of "K \<union> J" I])
   1.135 -  also have "emeasure (PiP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (PiP J M P) X"
   1.136 +  also have "emeasure (limP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (limP J M P) X"
   1.137      using K J by simp
   1.138 -  finally show "emeasure (PiP J M P) X = emeasure (PiP K M P) Y" ..
   1.139 +  finally show "emeasure (limP J M P) X = emeasure (limP K M P) Y" ..
   1.140  qed (insert J, force)
   1.141  
   1.142  lemma \<mu>G_eq:
   1.143 -  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (PiP J M P) X"
   1.144 +  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (limP J M P) X"
   1.145    by (intro \<mu>G_spec) auto
   1.146  
   1.147  lemma generator_Ex:
   1.148    assumes *: "A \<in> generator"
   1.149 -  shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (PiP J M P) X"
   1.150 +  shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (limP J M P) X"
   1.151  proof -
   1.152    from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
   1.153      unfolding generator_def by auto
   1.154 @@ -267,10 +269,10 @@
   1.155  
   1.156  lemma generatorE:
   1.157    assumes A: "A \<in> generator"
   1.158 -  obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (PiP J M P) X"
   1.159 +  obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (limP J M P) X"
   1.160  proof -
   1.161    from generator_Ex[OF A] obtain X J where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A"
   1.162 -    "\<mu>G A = emeasure (PiP J M P) X" by auto
   1.163 +    "\<mu>G A = emeasure (limP J M P) X" by auto
   1.164    then show thesis by (intro that) auto
   1.165  qed
   1.166  
   1.167 @@ -334,7 +336,7 @@
   1.168        using J K by simp_all
   1.169      then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
   1.170        by simp
   1.171 -    also have "\<dots> = emeasure (PiP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
   1.172 +    also have "\<dots> = emeasure (limP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
   1.173        using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un)
   1.174      also have "\<dots> = \<mu>G A + \<mu>G B"
   1.175        using J K JK_disj by (simp add: plus_emeasure[symmetric])
   1.176 @@ -356,8 +358,8 @@
   1.177    show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1)
   1.178  qed simp_all
   1.179  
   1.180 -lemma (in product_prob_space) PiP_PiM_finite[simp]:
   1.181 -  assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "PiP J M (\<lambda>J. PiM J M) = PiM J M"
   1.182 -  using assms by (simp add: PiP_finite)
   1.183 +lemma (in product_prob_space) limP_PiM_finite[simp]:
   1.184 +  assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "limP J M (\<lambda>J. PiM J M) = PiM J M"
   1.185 +  using assms by (simp add: limP_finite)
   1.186  
   1.187  end