prefer p2e before e2p; use measure_unique_Int_stable_vimage;
authorhoelzl
Fri Feb 04 14:16:55 2011 +0100 (2011-02-04)
changeset 41706a207a858d1f6
parent 41705 1100512e16d8
child 41707 a10f0a1cae41
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure.thy
src/HOL/Probability/Product_Measure.thy
     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Feb 04 14:16:55 2011 +0100
     1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Feb 04 14:16:55 2011 +0100
     1.3 @@ -48,6 +48,8 @@
     1.4  lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
     1.5    unfolding Pi_def by auto
     1.6  
     1.7 +subsection {* Lebesgue measure *}
     1.8 +
     1.9  definition lebesgue :: "'a::ordered_euclidean_space measure_space" where
    1.10    "lebesgue = \<lparr> space = UNIV,
    1.11      sets = {A. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n},
    1.12 @@ -498,6 +500,8 @@
    1.13    then show ?thesis by auto
    1.14  qed auto
    1.15  
    1.16 +subsection {* Lebesgue-Borel measure *}
    1.17 +
    1.18  definition "lborel = lebesgue \<lparr> sets := sets borel \<rparr>"
    1.19  
    1.20  lemma
    1.21 @@ -544,6 +548,8 @@
    1.22      by auto
    1.23  qed
    1.24  
    1.25 +subsection {* Lebesgue integrable implies Gauge integrable *}
    1.26 +
    1.27  lemma simple_function_has_integral:
    1.28    fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal"
    1.29    assumes f:"simple_function lebesgue f"
    1.30 @@ -734,13 +740,7 @@
    1.31    apply(rule borel.borel_measurableI)
    1.32    using continuous_open_preimage[OF assms] unfolding vimage_def by auto
    1.33  
    1.34 -lemma (in measure_space) integral_monotone_convergence_pos':
    1.35 -  assumes i: "\<And>i. integrable M (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)"
    1.36 -  and pos: "\<And>x i. 0 \<le> f i x"
    1.37 -  and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
    1.38 -  and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x"
    1.39 -  shows "integrable M u \<and> integral\<^isup>L M u = x"
    1.40 -  using integral_monotone_convergence_pos[OF assms] by auto
    1.41 +subsection {* Equivalence between product spaces and euclidean spaces *}
    1.42  
    1.43  definition e2p :: "'a::ordered_euclidean_space \<Rightarrow> (nat \<Rightarrow> real)" where
    1.44    "e2p x = (\<lambda>i\<in>{..<DIM('a)}. x$$i)"
    1.45 @@ -756,21 +756,6 @@
    1.46    "p2e (e2p x) = (x::'a::ordered_euclidean_space)"
    1.47    by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def)
    1.48  
    1.49 -declare restrict_extensional[intro]
    1.50 -
    1.51 -lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \<in> extensional {..<DIM('a)}"
    1.52 -  unfolding e2p_def by auto
    1.53 -
    1.54 -lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
    1.55 -  shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
    1.56 -proof(rule set_eqI,rule)
    1.57 -  fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
    1.58 -  show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
    1.59 -    apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
    1.60 -next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
    1.61 -  thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
    1.62 -qed
    1.63 -
    1.64  interpretation lborel_product: product_sigma_finite "\<lambda>x. lborel::real measure_space"
    1.65    by default
    1.66  
    1.67 @@ -843,107 +828,65 @@
    1.68    then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto
    1.69  qed simp
    1.70  
    1.71 -lemma inj_e2p[intro, simp]: "inj e2p"
    1.72 -proof (intro inj_onI conjI allI impI euclidean_eq[where 'a='a, THEN iffD2])
    1.73 -  fix x y ::'a and i assume "e2p x = e2p y" "i < DIM('a)"
    1.74 -  then show "x $$ i= y $$ i"
    1.75 -    by (auto simp: e2p_def restrict_def fun_eq_iff elim!: allE[where x=i])
    1.76 -qed
    1.77 -
    1.78 -lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
    1.79 -  by (auto simp: image_Int[THEN sym])
    1.80 +lemma Int_stable_cuboids:
    1.81 +  fixes x::"'a::ordered_euclidean_space"
    1.82 +  shows "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a, b::'a). {a..b})\<rparr>"
    1.83 +  by (auto simp: inter_interval Int_stable_def)
    1.84  
    1.85 -lemma Int_stable_cuboids: fixes x::"'a::ordered_euclidean_space"
    1.86 -  shows "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a, b::'a). e2p ` {a..b})\<rparr>"
    1.87 -  unfolding Int_stable_def algebra.select_convs
    1.88 -proof safe fix a b x y::'a
    1.89 -  have *:"e2p ` {a..b} \<inter> e2p ` {x..y} =
    1.90 -    (\<lambda>(a, b). e2p ` {a..b}) (\<chi>\<chi> i. max (a $$ i) (x $$ i), \<chi>\<chi> i. min (b $$ i) (y $$ i)::'a)"
    1.91 -    unfolding e2p_Int inter_interval by auto
    1.92 -  show "e2p ` {a..b} \<inter> e2p ` {x..y} \<in> range (\<lambda>(a, b). e2p ` {a..b::'a})" unfolding *
    1.93 -    apply(rule range_eqI) ..
    1.94 -qed
    1.95 -
    1.96 -lemma Int_stable_cuboids': fixes x::"'a::ordered_euclidean_space"
    1.97 -  shows "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a, b::'a). {a..b})\<rparr>"
    1.98 -  unfolding Int_stable_def algebra.select_convs
    1.99 -  apply safe unfolding inter_interval by auto
   1.100 -
   1.101 -lemma lmeasure_measure_eq_borel_prod:
   1.102 +lemma lborel_eq_lborel_space:
   1.103    fixes A :: "('a::ordered_euclidean_space) set"
   1.104    assumes "A \<in> sets borel"
   1.105 -  shows "lebesgue.\<mu> A = lborel_space.\<mu> TYPE('a) (e2p ` A)" (is "_ = ?m A")
   1.106 -proof (rule measure_unique_Int_stable[where X=A and A=cube])
   1.107 -  show "Int_stable \<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
   1.108 -    (is "Int_stable ?E" ) using Int_stable_cuboids' .
   1.109 -  have [simp]: "sigma ?E = borel" using borel_eq_atLeastAtMost ..
   1.110 -  show "\<And>i. lebesgue.\<mu> (cube i) \<noteq> \<omega>" unfolding cube_def by auto
   1.111 -  show "\<And>X. X \<in> sets ?E \<Longrightarrow> lebesgue.\<mu> X = ?m X"
   1.112 -  proof- case goal1 then obtain a b where X:"X = {a..b}" by auto
   1.113 -    { presume *:"X \<noteq> {} \<Longrightarrow> ?case"
   1.114 -      show ?case apply(cases,rule *,assumption) by auto }
   1.115 -    def XX \<equiv> "\<lambda>i. {a $$ i .. b $$ i}" assume  "X \<noteq> {}"  note X' = this[unfolded X interval_ne_empty]
   1.116 -    have *:"Pi\<^isub>E {..<DIM('a)} XX = e2p ` X" apply(rule set_eqI)
   1.117 -    proof fix x assume "x \<in> Pi\<^isub>E {..<DIM('a)} XX"
   1.118 -      thus "x \<in> e2p ` X" unfolding image_iff apply(rule_tac x="\<chi>\<chi> i. x i" in bexI)
   1.119 -        unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by rule auto
   1.120 -    next fix x assume "x \<in> e2p ` X" then guess y unfolding image_iff .. note y = this
   1.121 -      show "x \<in> Pi\<^isub>E {..<DIM('a)} XX" unfolding y using y(1)
   1.122 -        unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by auto
   1.123 -    qed
   1.124 -    have "lebesgue.\<mu> X = (\<Prod>x<DIM('a). Real (b $$ x - a $$ x))"  using X' apply- unfolding X
   1.125 -      unfolding lmeasure_atLeastAtMost content_closed_interval apply(subst Real_setprod) by auto
   1.126 -    also have "... = (\<Prod>i<DIM('a). lebesgue.\<mu> (XX i))" apply(rule setprod_cong2)
   1.127 -      unfolding XX_def lmeasure_atLeastAtMost apply(subst content_real) using X' by auto
   1.128 -    also have "... = ?m X" unfolding *[THEN sym]
   1.129 -      apply(rule lborel_space.measure_times[symmetric]) unfolding XX_def by auto
   1.130 -    finally show ?case .
   1.131 -  qed
   1.132 +  shows "lborel.\<mu> A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> (space (lborel_space.P TYPE('a))))"
   1.133 +    (is "_ = measure ?P (?T A)")
   1.134 +proof (rule measure_unique_Int_stable_vimage)
   1.135 +  show "measure_space ?P" by default
   1.136 +  show "measure_space lborel" by default
   1.137 +
   1.138 +  let ?E = "\<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
   1.139 +  show "Int_stable ?E" using Int_stable_cuboids .
   1.140 +  show "range cube \<subseteq> sets ?E" unfolding cube_def_raw by auto
   1.141 +  { fix x have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastsimp }
   1.142 +  then show "cube \<up> space ?E" by (intro isotoneI cube_subset_Suc) auto
   1.143 +  { fix i show "lborel.\<mu> (cube i) \<noteq> \<omega>" unfolding cube_def by auto }
   1.144 +  show "A \<in> sets (sigma ?E)" "sets (sigma ?E) = sets lborel" "space ?E = space lborel"
   1.145 +    using assms by (simp_all add: borel_eq_atLeastAtMost)
   1.146  
   1.147 -  show "range cube \<subseteq> sets \<lparr>space = UNIV, sets = range (\<lambda>(a, b). {a..b})\<rparr>"
   1.148 -    unfolding cube_def_raw by auto
   1.149 -  have "\<And>x. \<exists>xa. x \<in> cube xa" apply(rule_tac x=x in mem_big_cube) by fastsimp
   1.150 -  thus "cube \<up> space \<lparr>space = UNIV, sets = range (\<lambda>(a, b). {a..b})\<rparr>"
   1.151 -    apply-apply(rule isotoneI) apply(rule cube_subset_Suc) by auto
   1.152 -  show "A \<in> sets (sigma ?E)" using assms by simp
   1.153 -  have "measure_space lborel" by default
   1.154 -  then show "measure_space \<lparr> space = space ?E, sets = sets (sigma ?E), measure = measure lebesgue\<rparr>"
   1.155 -    unfolding lebesgue_def lborel_def by simp
   1.156 -  let ?M = "\<lparr> space = space ?E, sets = sets (sigma ?E), measure = ?m \<rparr>"
   1.157 -  show "measure_space ?M"
   1.158 -  proof (rule lborel_space.measure_space_vimage)
   1.159 -    show "sigma_algebra ?M" by (rule lborel.sigma_algebra_cong) auto
   1.160 -    show "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel) ?M"
   1.161 -      using measurable_p2e unfolding measurable_def by auto
   1.162 -    fix A :: "'a set" assume "A \<in> sets ?M"
   1.163 -    show "measure ?M A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> space (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel))"
   1.164 -      by (simp add: e2p_image_vimage)
   1.165 -  qed
   1.166 -qed simp
   1.167 +  show "p2e \<in> measurable ?P (lborel :: 'a measure_space)"
   1.168 +    using measurable_p2e unfolding measurable_def by simp
   1.169 +  { fix X assume "X \<in> sets ?E"
   1.170 +    then obtain a b where X[simp]: "X = {a .. b}" by auto
   1.171 +    have *: "?T X = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {a $$ i .. b $$ i})"
   1.172 +      by (auto simp: Pi_iff eucl_le[where 'a='a] p2e_def)
   1.173 +    show "lborel.\<mu> X = measure ?P (?T X)"
   1.174 +    proof cases
   1.175 +      assume "X \<noteq> {}"
   1.176 +      then have "a \<le> b"
   1.177 +        by (simp add: interval_ne_empty eucl_le[where 'a='a])
   1.178 +      then have "lborel.\<mu> X = (\<Prod>x<DIM('a). lborel.\<mu> {a $$ x .. b $$ x})"
   1.179 +        by (auto simp: content_closed_interval eucl_le[where 'a='a]
   1.180 +                 intro!: Real_setprod )
   1.181 +      also have "\<dots> = measure ?P (?T X)"
   1.182 +        unfolding * by (subst lborel_space.measure_times) auto
   1.183 +      finally show ?thesis .
   1.184 +    qed simp }
   1.185 +qed
   1.186  
   1.187 -lemma range_e2p:"range (e2p::'a::ordered_euclidean_space \<Rightarrow> _) = extensional {..<DIM('a)}"
   1.188 -  unfolding e2p_def_raw
   1.189 -  apply auto
   1.190 -  by (rule_tac x="\<chi>\<chi> i. x i" in image_eqI) (auto simp: fun_eq_iff extensional_def)
   1.191 +lemma lebesgue_eq_lborel_space_in_borel:
   1.192 +  fixes A :: "('a::ordered_euclidean_space) set"
   1.193 +  assumes A: "A \<in> sets borel"
   1.194 +  shows "lebesgue.\<mu> A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> (space (lborel_space.P TYPE('a))))"
   1.195 +  using lborel_eq_lborel_space[OF A] by simp
   1.196  
   1.197  lemma borel_fubini_positiv_integral:
   1.198    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal"
   1.199    assumes f: "f \<in> borel_measurable borel"
   1.200    shows "integral\<^isup>P lborel f = \<integral>\<^isup>+x. f (p2e x) \<partial>(lborel_space.P TYPE('a))"
   1.201 -proof (rule lborel.positive_integral_vimage[symmetric, of _ "e2p :: 'a \<Rightarrow> _" "(\<lambda>x. f (p2e x))", unfolded p2e_e2p])
   1.202 -  show "(e2p :: 'a \<Rightarrow> _) \<in> measurable borel (lborel_space.P TYPE('a))" by (rule measurable_e2p)
   1.203 -  show "sigma_algebra (lborel_space.P TYPE('a))" by default
   1.204 -  from measurable_comp[OF measurable_p2e f]
   1.205 -  show "(\<lambda>x. f (p2e x)) \<in> borel_measurable (lborel_space.P TYPE('a))" by (simp add: comp_def)
   1.206 -  let "?L A" = "lebesgue.\<mu> ((e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> UNIV)"
   1.207 -  fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> sets (lborel_space.P TYPE('a))"
   1.208 -  then have A: "(e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel \<in> sets borel"
   1.209 -    by (rule measurable_sets[OF measurable_e2p])
   1.210 -  have [simp]: "A \<inter> extensional {..<DIM('a)} = A"
   1.211 -    using `A \<in> sets (lborel_space.P TYPE('a))`[THEN lborel_space.sets_into_space] by auto
   1.212 -  show "lborel_space.\<mu> TYPE('a) A = ?L A"
   1.213 -    using lmeasure_measure_eq_borel_prod[OF A] by (simp add: range_e2p)
   1.214 -qed
   1.215 +proof (rule lborel_space.positive_integral_vimage[OF _ _ _ lborel_eq_lborel_space])
   1.216 +  show "sigma_algebra lborel" by default
   1.217 +  show "p2e \<in> measurable (lborel_space.P TYPE('a)) (lborel :: 'a measure_space)"
   1.218 +       "f \<in> borel_measurable lborel"
   1.219 +    using measurable_p2e f by (simp_all add: measurable_def)
   1.220 +qed simp
   1.221  
   1.222  lemma borel_fubini_integrable:
   1.223    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
   1.224 @@ -967,19 +910,13 @@
   1.225    then have "f \<in> borel_measurable borel"
   1.226      by (simp cong: measurable_cong)
   1.227    ultimately show "integrable lborel f"
   1.228 -    by (simp add: comp_def borel_fubini_positiv_integral integrable_def)
   1.229 +    by (simp add: borel_fubini_positiv_integral integrable_def)
   1.230  qed
   1.231  
   1.232  lemma borel_fubini:
   1.233    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
   1.234    assumes f: "f \<in> borel_measurable borel"
   1.235    shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>(lborel_space.P TYPE('a))"
   1.236 -proof -
   1.237 -  have 1:"(\<lambda>x. Real (f x)) \<in> borel_measurable borel" using f by auto
   1.238 -  have 2:"(\<lambda>x. Real (- f x)) \<in> borel_measurable borel" using f by auto
   1.239 -  show ?thesis unfolding lebesgue_integral_def
   1.240 -    unfolding borel_fubini_positiv_integral[OF 1] borel_fubini_positiv_integral[OF 2]
   1.241 -    unfolding o_def ..
   1.242 -qed
   1.243 +  using f by (simp add: borel_fubini_positiv_integral lebesgue_integral_def)
   1.244  
   1.245  end
     2.1 --- a/src/HOL/Probability/Measure.thy	Fri Feb 04 14:16:55 2011 +0100
     2.2 +++ b/src/HOL/Probability/Measure.thy	Fri Feb 04 14:16:55 2011 +0100
     2.3 @@ -624,6 +624,59 @@
     2.4    ultimately show ?thesis by (simp add: isoton_def)
     2.5  qed
     2.6  
     2.7 +lemma (in measure_space) measure_space_vimage:
     2.8 +  fixes M' :: "('c, 'd) measure_space_scheme"
     2.9 +  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
    2.10 +    and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
    2.11 +  shows "measure_space M'"
    2.12 +proof -
    2.13 +  interpret M': sigma_algebra M' by fact
    2.14 +  show ?thesis
    2.15 +  proof
    2.16 +    show "measure M' {} = 0" using \<nu>[of "{}"] by simp
    2.17 +
    2.18 +    show "countably_additive M' (measure M')"
    2.19 +    proof (intro countably_additiveI)
    2.20 +      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
    2.21 +      then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
    2.22 +      then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
    2.23 +        using `T \<in> measurable M M'` by (auto simp: measurable_def)
    2.24 +      moreover have "(\<Union>i. T -`  A i \<inter> space M) \<in> sets M"
    2.25 +        using * by blast
    2.26 +      moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
    2.27 +        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
    2.28 +      ultimately show "(\<Sum>\<^isub>\<infinity> i. measure M' (A i)) = measure M' (\<Union>i. A i)"
    2.29 +        using measure_countably_additive[OF _ **] A
    2.30 +        by (auto simp: comp_def vimage_UN \<nu>)
    2.31 +    qed
    2.32 +  qed
    2.33 +qed
    2.34 +
    2.35 +lemma measure_unique_Int_stable_vimage:
    2.36 +  fixes A :: "nat \<Rightarrow> 'a set"
    2.37 +  assumes E: "Int_stable E"
    2.38 +  and A: "range A \<subseteq> sets E" "A \<up> space E" "\<And>i. measure M (A i) \<noteq> \<omega>"
    2.39 +  and N: "measure_space N" "T \<in> measurable N M"
    2.40 +  and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M"
    2.41 +  and eq: "\<And>X. X \<in> sets E \<Longrightarrow> measure M X = measure N (T -` X \<inter> space N)"
    2.42 +  assumes X: "X \<in> sets (sigma E)"
    2.43 +  shows "measure M X = measure N (T -` X \<inter> space N)"
    2.44 +proof (rule measure_unique_Int_stable[OF E A(1,2) _ _ eq _ X])
    2.45 +  interpret M: measure_space M by fact
    2.46 +  interpret N: measure_space N by fact
    2.47 +  let "?T X" = "T -` X \<inter> space N"
    2.48 +  show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
    2.49 +    by (rule M.measure_space_cong) (auto simp: M)
    2.50 +  show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
    2.51 +  proof (rule N.measure_space_vimage)
    2.52 +    show "sigma_algebra ?E"
    2.53 +      by (rule M.sigma_algebra_cong) (auto simp: M)
    2.54 +    show "T \<in> measurable N ?E"
    2.55 +      using `T \<in> measurable N M` by (auto simp: M measurable_def)
    2.56 +  qed simp
    2.57 +  show "\<And>i. M.\<mu> (A i) \<noteq> \<omega>" by fact
    2.58 +qed
    2.59 +
    2.60  section "@{text \<mu>}-null sets"
    2.61  
    2.62  abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
    2.63 @@ -836,34 +889,6 @@
    2.64    qed
    2.65  qed
    2.66  
    2.67 -lemma (in measure_space) measure_space_vimage:
    2.68 -  fixes M' :: "('c, 'd) measure_space_scheme"
    2.69 -  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
    2.70 -    and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
    2.71 -  shows "measure_space M'"
    2.72 -proof -
    2.73 -  interpret M': sigma_algebra M' by fact
    2.74 -  show ?thesis
    2.75 -  proof
    2.76 -    show "measure M' {} = 0" using \<nu>[of "{}"] by simp
    2.77 -
    2.78 -    show "countably_additive M' (measure M')"
    2.79 -    proof (intro countably_additiveI)
    2.80 -      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
    2.81 -      then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
    2.82 -      then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
    2.83 -        using `T \<in> measurable M M'` by (auto simp: measurable_def)
    2.84 -      moreover have "(\<Union>i. T -`  A i \<inter> space M) \<in> sets M"
    2.85 -        using * by blast
    2.86 -      moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
    2.87 -        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
    2.88 -      ultimately show "(\<Sum>\<^isub>\<infinity> i. measure M' (A i)) = measure M' (\<Union>i. A i)"
    2.89 -        using measure_countably_additive[OF _ **] A
    2.90 -        by (auto simp: comp_def vimage_UN \<nu>)
    2.91 -    qed
    2.92 -  qed
    2.93 -qed
    2.94 -
    2.95  lemma (in measure_space) measure_space_subalgebra:
    2.96    assumes "sigma_algebra N" and [simp]: "sets N \<subseteq> sets M" "space N = space M"
    2.97    and measure[simp]: "\<And>X. X \<in> sets N \<Longrightarrow> measure N X = measure M X"
     3.1 --- a/src/HOL/Probability/Product_Measure.thy	Fri Feb 04 14:16:55 2011 +0100
     3.2 +++ b/src/HOL/Probability/Product_Measure.thy	Fri Feb 04 14:16:55 2011 +0100
     3.3 @@ -734,48 +734,37 @@
     3.4  qed
     3.5  
     3.6  lemma (in pair_sigma_finite) pair_measure_alt2:
     3.7 -  assumes "A \<in> sets P"
     3.8 +  assumes A: "A \<in> sets P"
     3.9    shows "\<mu> A = (\<integral>\<^isup>+y. M1.\<mu> ((\<lambda>x. (x, y)) -` A) \<partial>M2)"
    3.10      (is "_ = ?\<nu> A")
    3.11  proof -
    3.12 +  interpret Q: pair_sigma_finite M2 M1 by default
    3.13    from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
    3.14    have [simp]: "\<And>m. \<lparr> space = space E, sets = sets (sigma E), measure = m \<rparr> = P\<lparr> measure := m \<rparr>"
    3.15      unfolding pair_measure_def by simp
    3.16 -  show ?thesis
    3.17 -  proof (rule measure_unique_Int_stable[where \<nu>="?\<nu>", OF Int_stable_pair_measure_generator], simp_all)
    3.18 -    show "range F \<subseteq> sets E" "F \<up> space E" "\<And>i. \<mu> (F i) \<noteq> \<omega>" "A \<in> sets (sigma E)"
    3.19 +
    3.20 +  have "\<mu> A = Q.\<mu> ((\<lambda>(y, x). (x, y)) -` A \<inter> space Q.P)"
    3.21 +  proof (rule measure_unique_Int_stable_vimage[OF Int_stable_pair_measure_generator])
    3.22 +    show "measure_space P" "measure_space Q.P" by default
    3.23 +    show "(\<lambda>(y, x). (x, y)) \<in> measurable Q.P P" by (rule Q.pair_sigma_algebra_swap_measurable)
    3.24 +    show "sets (sigma E) = sets P" "space E = space P" "A \<in> sets (sigma E)"
    3.25 +      using assms unfolding pair_measure_def by auto
    3.26 +    show "range F \<subseteq> sets E" "F \<up> space E" "\<And>i. \<mu> (F i) \<noteq> \<omega>"
    3.27        using F `A \<in> sets P` by (auto simp: pair_measure_def)
    3.28 -    show "measure_space P" by default
    3.29 -    interpret Q: pair_sigma_finite M2 M1 by default
    3.30 -    have P: "sigma_algebra (P\<lparr> measure := ?\<nu>\<rparr>)"
    3.31 -      by (intro sigma_algebra_cong) auto
    3.32 -    show "measure_space (P\<lparr> measure := ?\<nu>\<rparr>)"
    3.33 -      apply (rule Q.measure_space_vimage[OF P])
    3.34 -      apply (simp_all)
    3.35 -      apply (rule Q.pair_sigma_algebra_swap_measurable)
    3.36 -    proof -
    3.37 -      fix A assume "A \<in> sets P"
    3.38 -      from sets_swap[OF this]
    3.39 -      show "(\<integral>\<^isup>+ y. M1.\<mu> ((\<lambda>x. (x, y)) -` A) \<partial>M2) = Q.\<mu> ((\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^isub>M M1))"
    3.40 -        using sets_into_space[OF `A \<in> sets P`]
    3.41 -        by (auto simp add: Q.pair_measure_alt space_pair_measure
    3.42 -                 intro!: M2.positive_integral_cong arg_cong[where f="M1.\<mu>"])
    3.43 -    qed
    3.44      fix X assume "X \<in> sets E"
    3.45 -    then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
    3.46 +    then obtain A B where X[simp]: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
    3.47        unfolding pair_measure_def pair_measure_generator_def by auto
    3.48 -    show "\<mu> X = ?\<nu> X"
    3.49 -    proof -
    3.50 -      from AB have "?\<nu> (A \<times> B) = (\<integral>\<^isup>+y. M1.\<mu> A * indicator B y \<partial>M2)"
    3.51 -        by (auto intro!: M2.positive_integral_cong)
    3.52 -      with AB show ?thesis
    3.53 -        unfolding pair_measure_times[OF AB] X
    3.54 -        by (simp add: M2.positive_integral_cmult_indicator ac_simps)
    3.55 -    qed
    3.56 +    then have "(\<lambda>(y, x). (x, y)) -` X \<inter> space Q.P = B \<times> A"
    3.57 +      using M1.sets_into_space M2.sets_into_space by (auto simp: space_pair_measure)
    3.58 +    then show "\<mu> X = Q.\<mu> ((\<lambda>(y, x). (x, y)) -` X \<inter> space Q.P)"
    3.59 +      using AB by (simp add: pair_measure_times Q.pair_measure_times ac_simps)
    3.60    qed
    3.61 +  then show ?thesis
    3.62 +    using sets_into_space[OF A] Q.pair_measure_alt[OF sets_swap[OF A]]
    3.63 +    by (auto simp add: Q.pair_measure_alt space_pair_measure
    3.64 +             intro!: M2.positive_integral_cong arg_cong[where f="M1.\<mu>"])
    3.65  qed
    3.66  
    3.67 -
    3.68  lemma pair_sigma_algebra_sigma:
    3.69    assumes 1: "S1 \<up> (space E1)" "range S1 \<subseteq> sets E1" and E1: "sets E1 \<subseteq> Pow (space E1)"
    3.70    assumes 2: "S2 \<up> (space E2)" "range S2 \<subseteq> sets E2" and E2: "sets E2 \<subseteq> Pow (space E2)"
    3.71 @@ -1559,8 +1548,8 @@
    3.72  lemma (in product_sigma_finite) measure_fold:
    3.73    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
    3.74    assumes A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
    3.75 -  shows "measure (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)) =
    3.76 -   measure (Pi\<^isub>M (I \<union> J) M) A"
    3.77 +  shows "measure (Pi\<^isub>M (I \<union> J) M) A =
    3.78 +    measure (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M))"
    3.79  proof -
    3.80    interpret I: finite_product_sigma_finite M I by default fact
    3.81    interpret J: finite_product_sigma_finite M J by default fact
    3.82 @@ -1575,10 +1564,12 @@
    3.83         "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
    3.84      by auto
    3.85    let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
    3.86 -  show "P.\<mu> (?X A) = IJ.\<mu> A"
    3.87 -  proof (rule measure_unique_Int_stable[where X=A])
    3.88 -    show "A \<in> sets (sigma IJ.G)"
    3.89 +  show "IJ.\<mu> A = P.\<mu> (?X A)"
    3.90 +  proof (rule measure_unique_Int_stable_vimage)
    3.91 +    show "measure_space IJ.P" "measure_space P.P" by default
    3.92 +    show "sets (sigma IJ.G) = sets IJ.P" "space IJ.G = space IJ.P" "A \<in> sets (sigma IJ.G)"
    3.93        using A unfolding product_algebra_def by auto
    3.94 +  next
    3.95      show "Int_stable IJ.G"
    3.96        by (simp add: PiE_Int Int_stable_def product_algebra_def
    3.97                      product_algebra_generator_def)
    3.98 @@ -1587,25 +1578,17 @@
    3.99        by (simp add: image_subset_iff product_algebra_def
   3.100                      product_algebra_generator_def)
   3.101      show "?F \<up> space IJ.G " using F(2) by simp
   3.102 -    have "measure_space IJ.P" by fact
   3.103 -    also have "IJ.P = \<lparr> space = space IJ.G, sets = sets (sigma IJ.G), measure = IJ.\<mu> \<rparr>"
   3.104 -      by (simp add: product_algebra_def)
   3.105 -    finally show "measure_space \<dots>" .
   3.106 -    let ?P = "\<lparr> space = space IJ.G, sets = sets (sigma IJ.G),
   3.107 -                measure = \<lambda>A. P.\<mu> (?X A)\<rparr>"
   3.108 -    have *: "?P = (sigma IJ.G \<lparr> measure := \<lambda>A. P.\<mu> (?X A) \<rparr>)"
   3.109 -      by auto
   3.110 -    have "sigma_algebra (sigma IJ.G \<lparr> measure := \<lambda>A. P.\<mu> (?X A) \<rparr>)"
   3.111 -      by (rule IJ.sigma_algebra_cong) (auto simp: product_algebra_def)
   3.112 -    then show "measure_space ?P" unfolding *
   3.113 -      using measurable_merge[OF `I \<inter> J = {}`]
   3.114 -      by (auto intro!: P.measure_space_vimage simp add: product_algebra_def)
   3.115 +    show "\<And>k. IJ.\<mu> (?F k) \<noteq> \<omega>"
   3.116 +      using `finite I` F
   3.117 +      by (subst IJ.measure_times) (auto simp add: setprod_\<omega>)
   3.118 +    show "?g \<in> measurable P.P IJ.P"
   3.119 +      using IJ by (rule measurable_merge)
   3.120    next
   3.121      fix A assume "A \<in> sets IJ.G"
   3.122 -    then obtain F where A[simp]: "A = Pi\<^isub>E (I \<union> J) F"
   3.123 +    then obtain F where A: "A = Pi\<^isub>E (I \<union> J) F"
   3.124        and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
   3.125        by (auto simp: product_algebra_generator_def)
   3.126 -    then have "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
   3.127 +    then have X: "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
   3.128        using sets_into_space by (auto simp: space_pair_measure) blast+
   3.129      then have "P.\<mu> (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
   3.130        using `finite J` `finite I` F
   3.131 @@ -1615,16 +1598,7 @@
   3.132      also have "\<dots> = IJ.\<mu> A"
   3.133        using `finite J` `finite I` F unfolding A
   3.134        by (intro IJ.measure_times[symmetric]) auto
   3.135 -    finally show "P.\<mu> (?X A) = IJ.\<mu> A" .
   3.136 -  next
   3.137 -    fix k
   3.138 -    have k: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
   3.139 -    then have "?X (?F k) = (\<Pi>\<^isub>E i\<in>I. F i k) \<times> (\<Pi>\<^isub>E i\<in>J. F i k)"
   3.140 -      using sets_into_space by (auto simp: space_pair_measure) blast+
   3.141 -    with k have "P.\<mu> (?X (?F k)) = (\<Prod>i\<in>I. \<mu> i (F i k)) * (\<Prod>i\<in>J. \<mu> i (F i k))"
   3.142 -     by (simp add: P.pair_measure_times I.measure_times J.measure_times)
   3.143 -    then show "P.\<mu> (?X (?F k)) \<noteq> \<omega>"
   3.144 -      using `finite I` F by (simp add: setprod_\<omega>)
   3.145 +    finally show "IJ.\<mu> A = P.\<mu> (?X A)" by (rule sym)
   3.146    qed
   3.147  qed
   3.148  
   3.149 @@ -1751,7 +1725,7 @@
   3.150      have 1: "sigma_algebra IJ.P" by default
   3.151      have 2: "?M \<in> measurable P.P IJ.P" using measurable_merge[OF IJ] .
   3.152      have 3: "\<And>A. A \<in> sets IJ.P \<Longrightarrow> IJ.\<mu> A = P.\<mu> (?M -` A \<inter> space P.P)"
   3.153 -      by (rule measure_fold[OF IJ fin, symmetric])
   3.154 +      by (rule measure_fold[OF IJ fin])
   3.155      have 4: "integrable (Pi\<^isub>M (I \<union> J) M) f" by fact
   3.156      show "integrable P.P ?f"
   3.157        by (rule P.integral_vimage[where f=f, OF 1 2 3 4])