src/HOL/Probability/Lebesgue_Measure.thy
changeset 41095 c335d880ff82
parent 41023 9118eb4eb8dc
child 41097 a1abfa4e2b44
     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 08 18:07:04 2010 +0100
     1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 08 16:15:14 2010 +0100
     1.3 @@ -647,44 +647,20 @@
     1.4  definition p2e :: "(nat \<Rightarrow> real) \<Rightarrow> 'a::ordered_euclidean_space" where
     1.5    "p2e x = (\<chi>\<chi> i. x i)"
     1.6  
     1.7 -lemma bij_euclidean_component:
     1.8 -  "bij_betw (e2p::'a::ordered_euclidean_space \<Rightarrow> _) (UNIV :: 'a set)
     1.9 -  ({..<DIM('a)} \<rightarrow>\<^isub>E (UNIV :: real set))"
    1.10 -  unfolding bij_betw_def e2p_def_raw
    1.11 -proof let ?e = "\<lambda>x.\<lambda>i\<in>{..<DIM('a::ordered_euclidean_space)}. (x::'a)$$i"
    1.12 -  show "inj ?e" unfolding inj_on_def restrict_def apply(subst euclidean_eq) apply safe
    1.13 -    apply(drule_tac x=i in fun_cong) by auto
    1.14 -  { fix x::"nat \<Rightarrow> real" assume x:"\<forall>i. i \<notin> {..<DIM('a)} \<longrightarrow> x i = undefined"
    1.15 -    hence "x = ?e (\<chi>\<chi> i. x i)" apply-apply(rule,case_tac "xa<DIM('a)") by auto
    1.16 -    hence "x \<in> range ?e" by fastsimp
    1.17 -  } thus "range ?e = ({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}"
    1.18 -    unfolding extensional_def using DIM_positive by auto
    1.19 -qed
    1.20 +lemma e2p_p2e[simp]:
    1.21 +  "x \<in> extensional {..<DIM('a)} \<Longrightarrow> e2p (p2e x::'a::ordered_euclidean_space) = x"
    1.22 +  by (auto simp: fun_eq_iff extensional_def p2e_def e2p_def)
    1.23  
    1.24 -lemma bij_p2e:
    1.25 -  "bij_betw (p2e::_ \<Rightarrow> 'a::ordered_euclidean_space) ({..<DIM('a)} \<rightarrow>\<^isub>E (UNIV :: real set))
    1.26 -  (UNIV :: 'a set)" (is "bij_betw ?p ?U _")
    1.27 -  unfolding bij_betw_def
    1.28 -proof show "inj_on ?p ?U" unfolding inj_on_def p2e_def
    1.29 -    apply(subst euclidean_eq) apply(safe,rule) unfolding extensional_def
    1.30 -    apply(case_tac "xa<DIM('a)") by auto
    1.31 -  { fix x::'a have "x \<in> ?p ` extensional {..<DIM('a)}"
    1.32 -      unfolding image_iff apply(rule_tac x="\<lambda>i. if i<DIM('a) then x$$i else undefined" in bexI)
    1.33 -      apply(subst euclidean_eq,safe) unfolding p2e_def extensional_def by auto
    1.34 -  } thus "?p ` ?U = UNIV" by auto
    1.35 -qed
    1.36 +lemma p2e_e2p[simp]:
    1.37 +  "p2e (e2p x) = (x::'a::ordered_euclidean_space)"
    1.38 +  by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def)
    1.39  
    1.40 -lemma e2p_p2e[simp]: fixes z::"'a::ordered_euclidean_space"
    1.41 -  assumes "x \<in> extensional {..<DIM('a)}"
    1.42 -  shows "e2p (p2e x::'a) = x"
    1.43 -proof fix i::nat
    1.44 -  show "e2p (p2e x::'a) i = x i" unfolding e2p_def p2e_def restrict_def
    1.45 -    using assms unfolding extensional_def by auto
    1.46 -qed
    1.47 -
    1.48 -lemma p2e_e2p[simp]: fixes x::"'a::ordered_euclidean_space"
    1.49 -  shows "p2e (e2p x) = x"
    1.50 -  apply(subst euclidean_eq) unfolding e2p_def p2e_def restrict_def by auto
    1.51 +lemma bij_inv_p2e_e2p:
    1.52 +  shows "bij_inv ({..<DIM('a)} \<rightarrow>\<^isub>E UNIV) (UNIV :: 'a::ordered_euclidean_space set)
    1.53 +     p2e e2p" (is "bij_inv ?P ?U _ _")
    1.54 +proof (rule bij_invI)
    1.55 +  show "p2e \<in> ?P \<rightarrow> ?U" "e2p \<in> ?U \<rightarrow> ?P" by (auto simp: e2p_def)
    1.56 +qed auto
    1.57  
    1.58  interpretation borel_product: product_sigma_finite "\<lambda>x. borel::real algebra" "\<lambda>x. lmeasure"
    1.59    by default
    1.60 @@ -692,71 +668,80 @@
    1.61  lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
    1.62    unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
    1.63  
    1.64 -lemma borel_vimage_algebra_eq:
    1.65 -  "sigma_algebra.vimage_algebra
    1.66 -         (borel :: ('a::ordered_euclidean_space) algebra) ({..<DIM('a)} \<rightarrow>\<^isub>E UNIV) p2e =
    1.67 -  sigma (product_algebra (\<lambda>x. \<lparr> space = UNIV::real set, sets = range (\<lambda>a. {..<a}) \<rparr>) {..<DIM('a)} )"
    1.68 -proof- note bor = borel_eq_lessThan
    1.69 -  def F \<equiv> "product_algebra (\<lambda>x. \<lparr> space = UNIV::real set, sets = range (\<lambda>a. {..<a}) \<rparr>) {..<DIM('a)}"
    1.70 -  def E \<equiv> "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
    1.71 -  have *:"(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}) = space F" unfolding F_def by auto
    1.72 -  show ?thesis unfolding F_def[symmetric] * bor
    1.73 -  proof(rule vimage_algebra_sigma,unfold E_def[symmetric])
    1.74 -    show "sets E \<subseteq> Pow (space E)" "p2e \<in> space F \<rightarrow> space E" unfolding E_def by auto
    1.75 -  next fix A assume "A \<in> sets F"
    1.76 -    hence A:"A \<in> (Pi\<^isub>E {..<DIM('a)}) ` ({..<DIM('a)} \<rightarrow> range lessThan)"
    1.77 -      unfolding F_def product_algebra_def algebra.simps .
    1.78 -    then guess B unfolding image_iff .. note B=this
    1.79 -    hence "\<forall>x<DIM('a). B x \<in> range lessThan" by auto
    1.80 -    hence "\<forall>x. \<exists>xa. x<DIM('a) \<longrightarrow> B x = {..<xa}" unfolding image_iff by auto
    1.81 -    from choice[OF this] guess b .. note b=this
    1.82 -    hence b':"\<forall>i<DIM('a). Sup (B i) = b i" using Sup_lessThan by auto
    1.83 +lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
    1.84 +  unfolding Pi_def by auto
    1.85  
    1.86 -    show "A \<in> (\<lambda>X. p2e -` X \<inter> space F) ` sets E" unfolding image_iff B
    1.87 -    proof(rule_tac x="{..< \<chi>\<chi> i. Sup (B i)}" in bexI)
    1.88 -      show "Pi\<^isub>E {..<DIM('a)} B = p2e -` {..<(\<chi>\<chi> i. Sup (B i))::'a} \<inter> space F"
    1.89 -        unfolding F_def E_def product_algebra_def algebra.simps
    1.90 -      proof(rule,unfold subset_eq,rule_tac[!] ballI)
    1.91 -        fix x assume "x \<in> Pi\<^isub>E {..<DIM('a)} B"
    1.92 -        hence *:"\<forall>i<DIM('a). x i < b i" "\<forall>i\<ge>DIM('a). x i = undefined"
    1.93 -          unfolding Pi_def extensional_def using b by auto
    1.94 -        have "(p2e x::'a) < (\<chi>\<chi> i. Sup (B i))" unfolding less_prod_def eucl_less[of "p2e x"]
    1.95 -          apply safe unfolding euclidean_lambda_beta b'[rule_format] p2e_def using * by auto
    1.96 -        moreover have "x \<in> extensional {..<DIM('a)}"
    1.97 -          using *(2) unfolding extensional_def by auto
    1.98 -        ultimately show "x \<in> p2e -` {..<(\<chi>\<chi> i. Sup (B i)) ::'a} \<inter>
    1.99 -          (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})" by auto
   1.100 -      next fix x assume as:"x \<in> p2e -` {..<(\<chi>\<chi> i. Sup (B i))::'a} \<inter>
   1.101 -          (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
   1.102 -        hence "p2e x < ((\<chi>\<chi> i. Sup (B i))::'a)" by auto
   1.103 -        hence "\<forall>i<DIM('a). x i \<in> B i" apply-apply(subst(asm) eucl_less)
   1.104 -          unfolding p2e_def using b b' by auto
   1.105 -        thus "x \<in> Pi\<^isub>E {..<DIM('a)} B" using as unfolding Pi_def extensional_def by auto
   1.106 -      qed
   1.107 -      show "{..<(\<chi>\<chi> i. Sup (B i))::'a} \<in> sets E" unfolding E_def algebra.simps by auto
   1.108 -    qed
   1.109 -  next fix A assume "A \<in> sets E"
   1.110 -    then guess a unfolding E_def algebra.simps image_iff .. note a = this(2)
   1.111 -    def B \<equiv> "\<lambda>i. {..<a $$ i}"
   1.112 -    show "p2e -` A \<inter> space F \<in> sets F" unfolding F_def
   1.113 -      unfolding product_algebra_def algebra.simps image_iff
   1.114 -      apply(rule_tac x=B in bexI) apply rule unfolding subset_eq apply(rule_tac[1-2] ballI)
   1.115 -    proof- show "B \<in> {..<DIM('a)} \<rightarrow> range lessThan" unfolding B_def by auto
   1.116 -      fix x assume as:"x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
   1.117 -      hence "p2e x \<in> A" by auto
   1.118 -      hence "\<forall>i<DIM('a). x i \<in> B i" unfolding B_def a lessThan_iff
   1.119 -        apply-apply(subst (asm) eucl_less) unfolding p2e_def by auto
   1.120 -      thus "x \<in> Pi\<^isub>E {..<DIM('a)} B" using as unfolding Pi_def extensional_def by auto
   1.121 -    next fix x assume x:"x \<in> Pi\<^isub>E {..<DIM('a)} B"
   1.122 -      moreover have "p2e x \<in> A" unfolding a lessThan_iff p2e_def apply(subst eucl_less)
   1.123 -        using x unfolding Pi_def extensional_def B_def by auto
   1.124 -      ultimately show "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})" by auto
   1.125 -    qed
   1.126 -  qed
   1.127 +lemma measurable_e2p_on_generator:
   1.128 +  "e2p \<in> measurable \<lparr> space = UNIV::'a set, sets = range lessThan \<rparr>
   1.129 +  (product_algebra
   1.130 +    (\<lambda>x. \<lparr> space = UNIV::real set, sets = range lessThan \<rparr>)
   1.131 +    {..<DIM('a::ordered_euclidean_space)})"
   1.132 +  (is "e2p \<in> measurable ?E ?P")
   1.133 +proof (unfold measurable_def, intro CollectI conjI ballI)
   1.134 +  show "e2p \<in> space ?E \<rightarrow> space ?P" by (auto simp: e2p_def)
   1.135 +  fix A assume "A \<in> sets ?P"
   1.136 +  then obtain E where A: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. E i)"
   1.137 +    and "E \<in> {..<DIM('a)} \<rightarrow> (range lessThan)"
   1.138 +    by (auto elim!: product_algebraE)
   1.139 +  then have "\<forall>i\<in>{..<DIM('a)}. \<exists>xs. E i = {..< xs}" by auto
   1.140 +  from this[THEN bchoice] guess xs ..
   1.141 +  then have A_eq: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< xs i})"
   1.142 +    using A by auto
   1.143 +  have "e2p -` A = {..< (\<chi>\<chi> i. xs i) :: 'a}"
   1.144 +    using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def A_eq
   1.145 +      euclidean_eq[where 'a='a] eucl_less[where 'a='a])
   1.146 +  then show "e2p -` A \<inter> space ?E \<in> sets ?E" by simp
   1.147  qed
   1.148  
   1.149 +lemma measurable_p2e_on_generator:
   1.150 +  "p2e \<in> measurable
   1.151 +    (product_algebra
   1.152 +      (\<lambda>x. \<lparr> space = UNIV::real set, sets = range lessThan \<rparr>)
   1.153 +      {..<DIM('a::ordered_euclidean_space)})
   1.154 +    \<lparr> space = UNIV::'a set, sets = range lessThan \<rparr>"
   1.155 +  (is "p2e \<in> measurable ?P ?E")
   1.156 +proof (unfold measurable_def, intro CollectI conjI ballI)
   1.157 +  show "p2e \<in> space ?P \<rightarrow> space ?E" by simp
   1.158 +  fix A assume "A \<in> sets ?E"
   1.159 +  then obtain x where "A = {..<x}" by auto
   1.160 +  then have "p2e -` A \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< x $$ i})"
   1.161 +    using DIM_positive
   1.162 +    by (auto simp: Pi_iff set_eq_iff p2e_def
   1.163 +                   euclidean_eq[where 'a='a] eucl_less[where 'a='a])
   1.164 +  then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto
   1.165 +qed
   1.166 +
   1.167 +lemma borel_vimage_algebra_eq:
   1.168 +  defines "F \<equiv> product_algebra (\<lambda>x. \<lparr> space = (UNIV::real set), sets = range lessThan \<rparr>) {..<DIM('a::ordered_euclidean_space)}"
   1.169 +  shows "sigma_algebra.vimage_algebra (borel::'a::ordered_euclidean_space algebra) (space (sigma F)) p2e = sigma F"
   1.170 +  unfolding borel_eq_lessThan
   1.171 +proof (intro vimage_algebra_sigma)
   1.172 +  let ?E = "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
   1.173 +  show "bij_inv (space (sigma F)) (space (sigma ?E)) p2e e2p"
   1.174 +    using bij_inv_p2e_e2p unfolding F_def by simp
   1.175 +  show "sets F \<subseteq> Pow (space F)" "sets ?E \<subseteq> Pow (space ?E)" unfolding F_def
   1.176 +    by (intro product_algebra_sets_into_space) auto
   1.177 +  show "p2e \<in> measurable F ?E"
   1.178 +    "e2p \<in> measurable ?E F"
   1.179 +    unfolding F_def using measurable_p2e_on_generator measurable_e2p_on_generator by auto
   1.180 +qed
   1.181 +
   1.182 +lemma product_borel_eq_vimage:
   1.183 +  "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
   1.184 +  sigma_algebra.vimage_algebra borel (extensional {..<DIM('a)})
   1.185 +  (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
   1.186 +  unfolding borel_vimage_algebra_eq[simplified]
   1.187 +  unfolding borel_eq_lessThan
   1.188 +  apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
   1.189 +  unfolding lessThan_iff
   1.190 +proof- fix i assume i:"i<DIM('a)"
   1.191 +  show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
   1.192 +    by(auto intro!:real_arch_lt isotoneI)
   1.193 +qed auto
   1.194 +
   1.195  lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
   1.196 -  apply(rule image_Int[THEN sym]) using bij_euclidean_component
   1.197 +  apply(rule image_Int[THEN sym])
   1.198 +  using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)]
   1.199    unfolding bij_betw_def by auto
   1.200  
   1.201  lemma Int_stable_cuboids: fixes x::"'a::ordered_euclidean_space"
   1.202 @@ -775,18 +760,6 @@
   1.203    unfolding Int_stable_def algebra.select_convs
   1.204    apply safe unfolding inter_interval by auto
   1.205  
   1.206 -lemma product_borel_eq_vimage:
   1.207 -  "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
   1.208 -  sigma_algebra.vimage_algebra borel (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})
   1.209 -  (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
   1.210 -  unfolding borel_vimage_algebra_eq unfolding borel_eq_lessThan
   1.211 -  apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
   1.212 -  unfolding lessThan_iff
   1.213 -proof- fix i assume i:"i<DIM('a)"
   1.214 -  show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
   1.215 -    by(auto intro!:real_arch_lt isotoneI)
   1.216 -qed auto
   1.217 -
   1.218  lemma inj_on_disjoint_family_on: assumes "disjoint_family_on A S" "inj f"
   1.219    shows "disjoint_family_on (\<lambda>x. f ` A x) S"
   1.220    unfolding disjoint_family_on_def
   1.221 @@ -808,12 +781,12 @@
   1.222    unfolding e2p_def by auto
   1.223  
   1.224  lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
   1.225 -  shows "e2p ` A = p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
   1.226 +  shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
   1.227  proof(rule set_eqI,rule)
   1.228    fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
   1.229 -  show "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
   1.230 +  show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
   1.231      apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
   1.232 -next fix x assume "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
   1.233 +next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
   1.234    thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
   1.235  qed
   1.236  
   1.237 @@ -879,17 +852,15 @@
   1.238        qed
   1.239  
   1.240        show "disjoint_family (\<lambda>n. e2p ` A n)" apply(rule inj_on_disjoint_family_on)
   1.241 -        using bij_euclidean_component using A(2) unfolding bij_betw_def by auto
   1.242 +        using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)] using A(2) unfolding bij_betw_def by auto
   1.243        show "(\<Union>n. e2p ` A n) \<in> sets (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
   1.244          unfolding product_borel_eq_vimage borel.in_vimage_algebra
   1.245        proof(rule bexI[OF _ A(3)],rule set_eqI,rule)
   1.246          fix x assume x:"x \<in> (\<Union>n. e2p ` A n)" hence "p2e x \<in> (\<Union>i. A i)" by auto
   1.247          moreover have "x \<in> extensional {..<DIM('a)}"
   1.248            using x unfolding extensional_def e2p_def_raw by auto
   1.249 -        ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter>
   1.250 -          extensional {..<DIM('a)})" by auto
   1.251 -      next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter>
   1.252 -          extensional {..<DIM('a)})"
   1.253 +        ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}" by auto
   1.254 +      next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}"
   1.255          hence "p2e x \<in> (\<Union>i. A i)" by auto
   1.256          hence "\<exists>n. x \<in> e2p ` A n" apply safe apply(rule_tac x=i in exI)
   1.257            unfolding image_iff apply(rule_tac x="p2e x" in bexI)
   1.258 @@ -925,23 +896,20 @@
   1.259    assumes f: "f \<in> borel_measurable borel"
   1.260    shows "borel.positive_integral f =
   1.261            borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)"
   1.262 -proof- def U \<equiv> "(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}):: (nat \<Rightarrow> real) set"
   1.263 +proof- def U \<equiv> "extensional {..<DIM('a)} :: (nat \<Rightarrow> real) set"
   1.264    interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
   1.265 -  have "\<And>x. \<exists>i::nat. x < real i" by (metis real_arch_lt)
   1.266 -  hence "(\<lambda>n::nat. {..<real n}) \<up> UNIV" apply-apply(rule isotoneI) by auto
   1.267 -  hence *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
   1.268 +  have *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
   1.269      = sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)})"
   1.270 -    unfolding U_def apply-apply(subst borel_vimage_algebra_eq)
   1.271 -    apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>x. \<lambda>n. {..<(\<chi>\<chi> i. real n)}", THEN sym])
   1.272 -    unfolding borel_eq_lessThan[THEN sym] by auto
   1.273 -  show ?thesis unfolding borel.positive_integral_vimage[unfolded space_borel,OF bij_p2e]
   1.274 +    unfolding U_def product_borel_eq_vimage[symmetric] ..
   1.275 +  show ?thesis
   1.276 +    unfolding borel.positive_integral_vimage[unfolded space_borel, OF bij_inv_p2e_e2p[THEN bij_inv_bij_betw(1)]]
   1.277      apply(subst fprod.positive_integral_cong_measure[THEN sym, of "\<lambda>A. lmeasure (p2e ` A)"])
   1.278      unfolding U_def[symmetric] *[THEN sym] o_def
   1.279    proof- fix A assume A:"A \<in> sets (sigma_algebra.vimage_algebra borel U (p2e ::_ \<Rightarrow> 'a))"
   1.280      hence *:"A \<subseteq> extensional {..<DIM('a)}" unfolding U_def by auto
   1.281 -    from A guess B unfolding borel.in_vimage_algebra U_def .. note B=this
   1.282 -    have "(p2e ` A::'a set) \<in> sets borel" unfolding B apply(subst Int_left_commute)
   1.283 -      apply(subst Int_absorb1) unfolding p2e_inv_extensional[of B,THEN sym] using B(1) by auto
   1.284 +    from A guess B unfolding borel.in_vimage_algebra U_def ..
   1.285 +    then have "(p2e ` A::'a set) \<in> sets borel"
   1.286 +      by (simp add: p2e_inv_extensional[of B, symmetric])
   1.287      from lmeasure_measure_eq_borel_prod[OF this] show "lmeasure (p2e ` A::'a set) =
   1.288        finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} A"
   1.289        unfolding e2p_p2e'[OF *] .