src/HOL/Analysis/Embed_Measure.thy
changeset 63627 6ddb43c6b711
parent 63626 44ce6b524ff3
child 63886 685fb01256af
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Mon Aug 08 14:13:14 2016 +0200
     1.3 @@ -0,0 +1,398 @@
     1.4 +(*  Title:      HOL/Analysis/Embed_Measure.thy
     1.5 +    Author:     Manuel Eberl, TU M√ľnchen
     1.6 +
     1.7 +    Defines measure embeddings with injective functions, i.e. lifting a measure on some values
     1.8 +    to a measure on "tagged" values (e.g. embed_measure M Inl lifts a measure on values 'a to a
     1.9 +    measure on the left part of the sum type 'a + 'b)
    1.10 +*)
    1.11 +
    1.12 +section \<open>Embed Measure Spaces with a Function\<close>
    1.13 +
    1.14 +theory Embed_Measure
    1.15 +imports Binary_Product_Measure
    1.16 +begin
    1.17 +
    1.18 +definition embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
    1.19 +  "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \<in> sets M}
    1.20 +                           (\<lambda>A. emeasure M (f -` A \<inter> space M))"
    1.21 +
    1.22 +lemma space_embed_measure: "space (embed_measure M f) = f ` space M"
    1.23 +  unfolding embed_measure_def
    1.24 +  by (subst space_measure_of) (auto dest: sets.sets_into_space)
    1.25 +
    1.26 +lemma sets_embed_measure':
    1.27 +  assumes inj: "inj_on f (space M)"
    1.28 +  shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
    1.29 +  unfolding embed_measure_def
    1.30 +proof (intro sigma_algebra.sets_measure_of_eq sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI)
    1.31 +  fix s assume "s \<in> {f ` A |A. A \<in> sets M}"
    1.32 +  then obtain s' where s'_props: "s = f ` s'" "s' \<in> sets M" by auto
    1.33 +  hence "f ` space M - s = f ` (space M - s')" using inj
    1.34 +    by (auto dest: inj_onD sets.sets_into_space)
    1.35 +  also have "... \<in> {f ` A |A. A \<in> sets M}" using s'_props by auto
    1.36 +  finally show "f ` space M - s \<in> {f ` A |A. A \<in> sets M}" .
    1.37 +next
    1.38 +  fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> {f ` A |A. A \<in> sets M}"
    1.39 +  then obtain A' where A': "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
    1.40 +    by (auto simp: subset_eq choice_iff)
    1.41 +  then have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
    1.42 +  with A' show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}"
    1.43 +    by simp blast
    1.44 +qed (auto dest: sets.sets_into_space)
    1.45 +
    1.46 +lemma the_inv_into_vimage:
    1.47 +  "inj_on f X \<Longrightarrow> A \<subseteq> X \<Longrightarrow> the_inv_into X f -` A \<inter> (f`X) = f ` A"
    1.48 +  by (auto simp: the_inv_into_f_f)
    1.49 +
    1.50 +lemma sets_embed_eq_vimage_algebra:
    1.51 +  assumes "inj_on f (space M)"
    1.52 +  shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"
    1.53 +  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 simple_image
    1.54 +           dest: sets.sets_into_space
    1.55 +           intro!: image_cong the_inv_into_vimage[symmetric])
    1.56 +
    1.57 +lemma sets_embed_measure:
    1.58 +  assumes inj: "inj f"
    1.59 +  shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
    1.60 +  using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD)
    1.61 +
    1.62 +lemma in_sets_embed_measure: "A \<in> sets M \<Longrightarrow> f ` A \<in> sets (embed_measure M f)"
    1.63 +  unfolding embed_measure_def
    1.64 +  by (intro in_measure_of) (auto dest: sets.sets_into_space)
    1.65 +
    1.66 +lemma measurable_embed_measure1:
    1.67 +  assumes g: "(\<lambda>x. g (f x)) \<in> measurable M N"
    1.68 +  shows "g \<in> measurable (embed_measure M f) N"
    1.69 +  unfolding measurable_def
    1.70 +proof safe
    1.71 +  fix A assume "A \<in> sets N"
    1.72 +  with g have "(\<lambda>x. g (f x)) -` A \<inter> space M \<in> sets M"
    1.73 +    by (rule measurable_sets)
    1.74 +  then have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) \<in> sets (embed_measure M f)"
    1.75 +    by (rule in_sets_embed_measure)
    1.76 +  also have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) = g -` A \<inter> space (embed_measure M f)"
    1.77 +    by (auto simp: space_embed_measure)
    1.78 +  finally show "g -` A \<inter> space (embed_measure M f) \<in> sets (embed_measure M f)" .
    1.79 +qed (insert measurable_space[OF assms], auto simp: space_embed_measure)
    1.80 +
    1.81 +lemma measurable_embed_measure2':
    1.82 +  assumes "inj_on f (space M)"
    1.83 +  shows "f \<in> measurable M (embed_measure M f)"
    1.84 +proof-
    1.85 +  {
    1.86 +    fix A assume A: "A \<in> sets M"
    1.87 +    also from A have "A = A \<inter> space M" by auto
    1.88 +    also have "... = f -` f ` A \<inter> space M" using A assms
    1.89 +      by (auto dest: inj_onD sets.sets_into_space)
    1.90 +    finally have "f -` f ` A \<inter> space M \<in> sets M" .
    1.91 +  }
    1.92 +  thus ?thesis using assms unfolding embed_measure_def
    1.93 +    by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
    1.94 +qed
    1.95 +
    1.96 +lemma measurable_embed_measure2:
    1.97 +  assumes [simp]: "inj f" shows "f \<in> measurable M (embed_measure M f)"
    1.98 +  by (auto simp: inj_vimage_image_eq embed_measure_def
    1.99 +           intro!: measurable_measure_of dest: sets.sets_into_space)
   1.100 +
   1.101 +lemma embed_measure_eq_distr':
   1.102 +  assumes "inj_on f (space M)"
   1.103 +  shows "embed_measure M f = distr M (embed_measure M f) f"
   1.104 +proof-
   1.105 +  have "distr M (embed_measure M f) f =
   1.106 +            measure_of (f ` space M) {f ` A |A. A \<in> sets M}
   1.107 +                       (\<lambda>A. emeasure M (f -` A \<inter> space M))" unfolding distr_def
   1.108 +      by (simp add: space_embed_measure sets_embed_measure'[OF assms])
   1.109 +  also have "... = embed_measure M f" unfolding embed_measure_def ..
   1.110 +  finally show ?thesis ..
   1.111 +qed
   1.112 +
   1.113 +lemma embed_measure_eq_distr:
   1.114 +    "inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f"
   1.115 +  by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD)
   1.116 +
   1.117 +lemma nn_integral_embed_measure':
   1.118 +  "inj_on f (space M) \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
   1.119 +  nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
   1.120 +  apply (subst embed_measure_eq_distr', simp)
   1.121 +  apply (subst nn_integral_distr)
   1.122 +  apply (simp_all add: measurable_embed_measure2')
   1.123 +  done
   1.124 +
   1.125 +lemma nn_integral_embed_measure:
   1.126 +  "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
   1.127 +  nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
   1.128 +  by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp
   1.129 +
   1.130 +lemma emeasure_embed_measure':
   1.131 +    assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
   1.132 +    shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
   1.133 +  by (subst embed_measure_eq_distr'[OF assms(1)])
   1.134 +     (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)])
   1.135 +
   1.136 +lemma emeasure_embed_measure:
   1.137 +    assumes "inj f" "A \<in> sets (embed_measure M f)"
   1.138 +    shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
   1.139 + using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD)
   1.140 +
   1.141 +lemma embed_measure_comp:
   1.142 +  assumes [simp]: "inj f" "inj g"
   1.143 +  shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)"
   1.144 +proof-
   1.145 +  have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp)
   1.146 +  note measurable_embed_measure2[measurable]
   1.147 +  have "embed_measure (embed_measure M f) g =
   1.148 +            distr M (embed_measure (embed_measure M f) g) (g \<circ> f)"
   1.149 +      by (subst (1 2) embed_measure_eq_distr)
   1.150 +         (simp_all add: distr_distr sets_embed_measure cong: distr_cong)
   1.151 +  also have "... = embed_measure M (g \<circ> f)"
   1.152 +      by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong)
   1.153 +         (auto simp: sets_embed_measure o_def image_image[symmetric]
   1.154 +               intro: inj_comp cong: distr_cong)
   1.155 +  finally show ?thesis .
   1.156 +qed
   1.157 +
   1.158 +lemma sigma_finite_embed_measure:
   1.159 +  assumes "sigma_finite_measure M" and inj: "inj f"
   1.160 +  shows "sigma_finite_measure (embed_measure M f)"
   1.161 +proof -
   1.162 +  from assms(1) interpret sigma_finite_measure M .
   1.163 +  from sigma_finite_countable obtain A where
   1.164 +      A_props: "countable A" "A \<subseteq> sets M" "\<Union>A = space M" "\<And>X. X\<in>A \<Longrightarrow> emeasure M X \<noteq> \<infinity>" by blast
   1.165 +  from A_props have "countable (op ` f`A)" by auto
   1.166 +  moreover
   1.167 +  from inj and A_props have "op ` f`A \<subseteq> sets (embed_measure M f)"
   1.168 +    by (auto simp: sets_embed_measure)
   1.169 +  moreover
   1.170 +  from A_props and inj have "\<Union>(op ` f`A) = space (embed_measure M f)"
   1.171 +    by (auto simp: space_embed_measure intro!: imageI)
   1.172 +  moreover
   1.173 +  from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
   1.174 +    by (intro ballI, subst emeasure_embed_measure)
   1.175 +       (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
   1.176 +  ultimately show ?thesis by - (standard, blast)
   1.177 +qed
   1.178 +
   1.179 +lemma embed_measure_count_space':
   1.180 +    "inj_on f A \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
   1.181 +  apply (subst distr_bij_count_space[of f A "f`A", symmetric])
   1.182 +  apply (simp add: inj_on_def bij_betw_def)
   1.183 +  apply (subst embed_measure_eq_distr')
   1.184 +  apply simp
   1.185 +  apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff)
   1.186 +  apply (subst (1 2) emeasure_distr)
   1.187 +  apply (auto simp: space_embed_measure sets_embed_measure')
   1.188 +  done
   1.189 +
   1.190 +lemma embed_measure_count_space:
   1.191 +    "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
   1.192 +  by(rule embed_measure_count_space')(erule subset_inj_on, simp)
   1.193 +
   1.194 +lemma sets_embed_measure_alt:
   1.195 +    "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
   1.196 +  by (auto simp: sets_embed_measure)
   1.197 +
   1.198 +lemma emeasure_embed_measure_image':
   1.199 +  assumes "inj_on f (space M)" "X \<in> sets M"
   1.200 +  shows "emeasure (embed_measure M f) (f`X) = emeasure M X"
   1.201 +proof-
   1.202 +  from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X \<inter> space M)"
   1.203 +    by (subst emeasure_embed_measure') (auto simp: sets_embed_measure')
   1.204 +  also from assms have "f -` f ` X \<inter> space M = X" by (auto dest: inj_onD sets.sets_into_space)
   1.205 +  finally show ?thesis .
   1.206 +qed
   1.207 +
   1.208 +lemma emeasure_embed_measure_image:
   1.209 +    "inj f \<Longrightarrow> X \<in> sets M \<Longrightarrow> emeasure (embed_measure M f) (f`X) = emeasure M X"
   1.210 +  by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq)
   1.211 +
   1.212 +lemma embed_measure_eq_iff:
   1.213 +  assumes "inj f"
   1.214 +  shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _")
   1.215 +proof
   1.216 +  from assms have I: "inj (op` f)" by (auto intro: injI dest: injD)
   1.217 +  assume asm: "?M = ?N"
   1.218 +  hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp
   1.219 +  with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt)
   1.220 +  moreover {
   1.221 +    fix X assume "X \<in> sets A"
   1.222 +    from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp
   1.223 +    with \<open>X \<in> sets A\<close> and \<open>sets A = sets B\<close> and assms
   1.224 +        have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image)
   1.225 +  }
   1.226 +  ultimately show "A = B" by (rule measure_eqI)
   1.227 +qed simp
   1.228 +
   1.229 +lemma the_inv_into_in_Pi: "inj_on f A \<Longrightarrow> the_inv_into A f \<in> f ` A \<rightarrow> A"
   1.230 +  by (auto simp: the_inv_into_f_f)
   1.231 +
   1.232 +lemma map_prod_image: "map_prod f g ` (A \<times> B) = (f`A) \<times> (g`B)"
   1.233 +  using map_prod_surj_on[OF refl refl] .
   1.234 +
   1.235 +lemma map_prod_vimage: "map_prod f g -` (A \<times> B) = (f-`A) \<times> (g-`B)"
   1.236 +  by auto
   1.237 +
   1.238 +lemma embed_measure_prod:
   1.239 +  assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N"
   1.240 +  shows "embed_measure M f \<Otimes>\<^sub>M embed_measure N g = embed_measure (M \<Otimes>\<^sub>M N) (\<lambda>(x, y). (f x, g y))"
   1.241 +    (is "?L = _")
   1.242 +  unfolding map_prod_def[symmetric]
   1.243 +proof (rule pair_measure_eqI)
   1.244 +  have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A"
   1.245 +    using f g by (auto simp: inj_on_def)
   1.246 +
   1.247 +  note complete_lattice_class.Sup_insert[simp del] ccSup_insert[simp del] SUP_insert[simp del]
   1.248 +     ccSUP_insert[simp del]
   1.249 +  show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))"
   1.250 +    unfolding map_prod_def[symmetric]
   1.251 +    apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra
   1.252 +      cong: vimage_algebra_cong)
   1.253 +    apply (subst sets_vimage_Sup_eq[where Y="space (M \<Otimes>\<^sub>M N)"])
   1.254 +    apply (simp_all add: space_pair_measure[symmetric])
   1.255 +    apply (auto simp add: the_inv_into_f_f
   1.256 +                simp del: map_prod_simp
   1.257 +                del: prod_fun_imageE) []
   1.258 +    apply auto []
   1.259 +    apply (subst image_insert)
   1.260 +    apply simp
   1.261 +    apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
   1.262 +    apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
   1.263 +    apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq
   1.264 +       space_pair_measure[symmetric] map_prod_image[symmetric])
   1.265 +    apply (intro arg_cong[where f=sets] arg_cong[where f=Sup] arg_cong2[where f=insert] vimage_algebra_cong)
   1.266 +    apply (auto simp: map_prod_image the_inv_into_f_f
   1.267 +                simp del: map_prod_simp del: prod_fun_imageE)
   1.268 +    apply (simp_all add: the_inv_into_f_f space_pair_measure)
   1.269 +    done
   1.270 +
   1.271 +  note measurable_embed_measure2[measurable]
   1.272 +  fix A B assume AB: "A \<in> sets (embed_measure M f)" "B \<in> sets (embed_measure N g)"
   1.273 +  moreover have "f -` A \<times> g -` B \<inter> space (M \<Otimes>\<^sub>M N) = (f -` A \<inter> space M) \<times> (g -` B \<inter> space N)"
   1.274 +    by (auto simp: space_pair_measure)
   1.275 +  ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B =
   1.276 +                     emeasure (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> B)"
   1.277 +    by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure
   1.278 +                  sigma_finite_measure.emeasure_pair_measure_Times)
   1.279 +qed (insert assms, simp_all add: sigma_finite_embed_measure)
   1.280 +
   1.281 +lemma mono_embed_measure:
   1.282 +  "space M = space M' \<Longrightarrow> sets M \<subseteq> sets M' \<Longrightarrow> sets (embed_measure M f) \<subseteq> sets (embed_measure M' f)"
   1.283 +  unfolding embed_measure_def
   1.284 +  apply (subst (1 2) sets_measure_of)
   1.285 +  apply (blast dest: sets.sets_into_space)
   1.286 +  apply (blast dest: sets.sets_into_space)
   1.287 +  apply simp
   1.288 +  apply (intro sigma_sets_mono')
   1.289 +  apply safe
   1.290 +  apply (simp add: subset_eq)
   1.291 +  apply metis
   1.292 +  done
   1.293 +
   1.294 +lemma density_embed_measure:
   1.295 +  assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)"
   1.296 +  shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2")
   1.297 +proof (rule measure_eqI)
   1.298 +  fix X assume X: "X \<in> sets ?M1"
   1.299 +  from inj have Mf[measurable]: "f \<in> measurable M (embed_measure M f)"
   1.300 +    by (rule measurable_embed_measure2)
   1.301 +  from Mg and X have "emeasure ?M1 X = \<integral>\<^sup>+ x. g x * indicator X x \<partial>embed_measure M f"
   1.302 +    by (subst emeasure_density) simp_all
   1.303 +  also from X have "... = \<integral>\<^sup>+ x. g (f x) * indicator X (f x) \<partial>M"
   1.304 +    by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr) auto
   1.305 +  also have "... = \<integral>\<^sup>+ x. g (f x) * indicator (f -` X \<inter> space M) x \<partial>M"
   1.306 +    by (intro nn_integral_cong) (auto split: split_indicator)
   1.307 +  also from X have "... = emeasure (density M (g \<circ> f)) (f -` X \<inter> space M)"
   1.308 +    by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf])
   1.309 +  also from X and inj have "... = emeasure ?M2 X"
   1.310 +    by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure)
   1.311 +  finally show "emeasure ?M1 X = emeasure ?M2 X" .
   1.312 +qed (simp_all add: sets_embed_measure inj)
   1.313 +
   1.314 +lemma density_embed_measure':
   1.315 +  assumes inj: "inj f" and inv: "\<And>x. f' (f x) = x" and Mg[measurable]: "g \<in> borel_measurable M"
   1.316 +  shows "density (embed_measure M f) (g \<circ> f') = embed_measure (density M g) f"
   1.317 +proof-
   1.318 +  have "density (embed_measure M f) (g \<circ> f') = embed_measure (density M (g \<circ> f' \<circ> f)) f"
   1.319 +    by (rule density_embed_measure[OF inj])
   1.320 +       (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong,
   1.321 +        rule inv, rule measurable_ident_sets, simp, rule Mg)
   1.322 +  also have "density M (g \<circ> f' \<circ> f) = density M g"
   1.323 +    by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv)
   1.324 +  finally show ?thesis .
   1.325 +qed
   1.326 +
   1.327 +lemma inj_on_image_subset_iff:
   1.328 +  assumes "inj_on f C" "A \<subseteq> C"  "B \<subseteq> C"
   1.329 +  shows "f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"
   1.330 +proof (intro iffI subsetI)
   1.331 +  fix x assume A: "f ` A \<subseteq> f ` B" and B: "x \<in> A"
   1.332 +  from B have "f x \<in> f ` A" by blast
   1.333 +  with A have "f x \<in> f ` B" by blast
   1.334 +  then obtain y where "f x = f y" and "y \<in> B" by blast
   1.335 +  with assms and B have "x = y" by (auto dest: inj_onD)
   1.336 +  with \<open>y \<in> B\<close> show "x \<in> B" by simp
   1.337 +qed auto
   1.338 +
   1.339 +
   1.340 +lemma AE_embed_measure':
   1.341 +  assumes inj: "inj_on f (space M)"
   1.342 +  shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   1.343 +proof
   1.344 +  let ?M = "embed_measure M f"
   1.345 +  assume "AE x in ?M. P x"
   1.346 +  then obtain A where A_props: "A \<in> sets ?M" "emeasure ?M A = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> A"
   1.347 +    by (force elim: AE_E)
   1.348 +  then obtain A' where A'_props: "A = f ` A'" "A' \<in> sets M" by (auto simp: sets_embed_measure' inj)
   1.349 +  moreover have B: "{x\<in>space ?M. \<not>P x} = f ` {x\<in>space M. \<not>P (f x)}"
   1.350 +    by (auto simp: inj space_embed_measure)
   1.351 +  from A_props(3) have "{x\<in>space M. \<not>P (f x)} \<subseteq> A'"
   1.352 +    by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj])
   1.353 +       (insert A'_props, auto dest: sets.sets_into_space)
   1.354 +  moreover from A_props A'_props have "emeasure M A' = 0"
   1.355 +    by (simp add: emeasure_embed_measure_image' inj)
   1.356 +  ultimately show "AE x in M. P (f x)" by (intro AE_I)
   1.357 +next
   1.358 +  let ?M = "embed_measure M f"
   1.359 +  assume "AE x in M. P (f x)"
   1.360 +  then obtain A where A_props: "A \<in> sets M" "emeasure M A = 0" "{x\<in>space M. \<not>P (f x)} \<subseteq> A"
   1.361 +    by (force elim: AE_E)
   1.362 +  hence "f`A \<in> sets ?M" "emeasure ?M (f`A) = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> f`A"
   1.363 +    by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj)
   1.364 +  thus "AE x in ?M. P x" by (intro AE_I)
   1.365 +qed
   1.366 +
   1.367 +lemma AE_embed_measure:
   1.368 +  assumes inj: "inj f"
   1.369 +  shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   1.370 +  using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)
   1.371 +
   1.372 +lemma nn_integral_monotone_convergence_SUP_countable:
   1.373 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ennreal"
   1.374 +  assumes nonempty: "Y \<noteq> {}"
   1.375 +  and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
   1.376 +  and countable: "countable B"
   1.377 +  shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
   1.378 +  (is "?lhs = ?rhs")
   1.379 +proof -
   1.380 +  let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"
   1.381 +  have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
   1.382 +    by(rule nn_integral_cong)(simp add: countable)
   1.383 +  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
   1.384 +    by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
   1.385 +  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV"
   1.386 +    by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty)
   1.387 +  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
   1.388 +  proof(rule nn_integral_monotone_convergence_SUP_nat)
   1.389 +    show "Complete_Partial_Order.chain op \<le> (?f ` Y)"
   1.390 +      by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
   1.391 +  qed fact
   1.392 +  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
   1.393 +    by(simp add: nn_integral_count_space_indicator)
   1.394 +  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
   1.395 +    by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
   1.396 +  also have "\<dots> = ?rhs"
   1.397 +    by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
   1.398 +  finally show ?thesis .
   1.399 +qed
   1.400 +
   1.401 +end