piecewise measurability using restrict_space; cleanup Borel_Space
authorhoelzl
Thu Jan 15 15:04:51 2015 +0100 (2015-01-15)
changeset 59361fd5da2434be4
parent 59360 b1e5d552e8cc
child 59373 6162878e3e53
piecewise measurability using restrict_space; cleanup Borel_Space
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Measurable.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Jan 14 17:04:19 2015 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Thu Jan 15 15:04:51 2015 +0100
     1.3 @@ -202,21 +202,28 @@
     1.4    qed auto
     1.5  qed (auto simp: eq intro: generate_topology.Basis)
     1.6  
     1.7 -lemma borel_measurable_continuous_on_if:
     1.8 -  assumes A: "A \<in> sets borel" and f: "continuous_on A f" and g: "continuous_on (- A) g"
     1.9 -  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> borel_measurable borel"
    1.10 +lemma borel_measurable_continuous_on_restrict:
    1.11 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
    1.12 +  assumes f: "continuous_on A f"
    1.13 +  shows "f \<in> borel_measurable (restrict_space borel A)"
    1.14  proof (rule borel_measurableI)
    1.15    fix S :: "'b set" assume "open S"
    1.16 -  have "(\<lambda>x. if x \<in> A then f x else g x) -` S \<inter> space borel = (f -` S \<inter> A) \<union> (g -` S \<inter> -A)"
    1.17 -    by (auto split: split_if_asm)
    1.18 -  moreover obtain A' where "f -` S \<inter> A = A' \<inter> A" "open A'"
    1.19 -    using continuous_on_open_invariant[THEN iffD1, rule_format, OF f `open S`] by metis
    1.20 -  moreover obtain B' where "g -` S \<inter> -A = B' \<inter> -A" "open B'"
    1.21 -    using continuous_on_open_invariant[THEN iffD1, rule_format, OF g `open S`] by metis
    1.22 -  ultimately show "(\<lambda>x. if x \<in> A then f x else g x) -` S \<inter> space borel \<in> sets borel"
    1.23 -    using A by auto
    1.24 +  with f obtain T where "f -` S \<inter> A = T \<inter> A" "open T"
    1.25 +    by (metis continuous_on_open_invariant)
    1.26 +  then show "f -` S \<inter> space (restrict_space borel A) \<in> sets (restrict_space borel A)"
    1.27 +    by (force simp add: sets_restrict_space space_restrict_space)
    1.28  qed
    1.29  
    1.30 +lemma borel_measurable_continuous_on1: "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
    1.31 +  by (drule borel_measurable_continuous_on_restrict) simp
    1.32 +
    1.33 +lemma borel_measurable_continuous_on_if:
    1.34 +  assumes [measurable]: "A \<in> sets borel" and f: "continuous_on A f" and g: "continuous_on (- A) g"
    1.35 +  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> borel_measurable borel"
    1.36 +  by (rule measurable_piecewise_restrict[where
    1.37 +       X="\<lambda>b. if b then A else - A" and I=UNIV and f="\<lambda>b x. if b then f x else g x"])
    1.38 +     (auto intro: f g borel_measurable_continuous_on_restrict)
    1.39 +
    1.40  lemma borel_measurable_continuous_countable_exceptions:
    1.41    fixes f :: "'a::t1_space \<Rightarrow> 'b::topological_space"
    1.42    assumes X: "countable X"
    1.43 @@ -229,11 +236,6 @@
    1.44      by (intro borel_measurable_continuous_on_if assms continuous_intros)
    1.45  qed auto
    1.46  
    1.47 -lemma borel_measurable_continuous_on1:
    1.48 -  "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
    1.49 -  using borel_measurable_continuous_on_if[of UNIV f "\<lambda>_. undefined"]
    1.50 -  by (auto intro: continuous_on_const)
    1.51 -
    1.52  lemma borel_measurable_continuous_on:
    1.53    assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
    1.54    shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
    1.55 @@ -636,7 +638,7 @@
    1.56      fix x :: 'a assume "a < x \<bullet> i"
    1.57      with reals_Archimedean[of "x \<bullet> i - a"]
    1.58      obtain n where "a + 1 / real (Suc n) < x \<bullet> i"
    1.59 -      by (auto simp: inverse_eq_divide field_simps)
    1.60 +      by (auto simp: field_simps)
    1.61      then show "\<exists>n. a + 1 / real (Suc n) \<le> x \<bullet> i"
    1.62        by (blast intro: less_imp_le)
    1.63    next
    1.64 @@ -673,7 +675,7 @@
    1.65      fix x::'a assume *: "x\<bullet>i < a"
    1.66      with reals_Archimedean[of "a - x\<bullet>i"]
    1.67      obtain n where "x \<bullet> i < a - 1 / (real (Suc n))"
    1.68 -      by (auto simp: field_simps inverse_eq_divide)
    1.69 +      by (auto simp: field_simps)
    1.70      then show "\<exists>n. x \<bullet> i \<le> a - 1 / (real (Suc n))"
    1.71        by (blast intro: less_imp_le)
    1.72    next
    1.73 @@ -683,7 +685,7 @@
    1.74      finally show "x\<bullet>i < a" .
    1.75    qed
    1.76    show "{x. x\<bullet>i < a} \<in> ?SIGMA" unfolding *
    1.77 -    by (safe intro!: sets.countable_UN) (auto intro: i)
    1.78 +    by (intro sets.countable_UN) (auto intro: i)
    1.79  qed auto
    1.80  
    1.81  lemma borel_eq_halfspace_ge:
    1.82 @@ -693,7 +695,7 @@
    1.83    fix a :: real and i :: 'a assume i: "(a, i) \<in> UNIV \<times> Basis"
    1.84    have *: "{x::'a. x\<bullet>i < a} = space ?SIGMA - {x::'a. a \<le> x\<bullet>i}" by auto
    1.85    show "{x. x\<bullet>i < a} \<in> ?SIGMA" unfolding *
    1.86 -    using i by (safe intro!: sets.compl_sets) auto
    1.87 +    using i by (intro sets.compl_sets) auto
    1.88  qed auto
    1.89  
    1.90  lemma borel_eq_halfspace_greater:
    1.91 @@ -704,7 +706,7 @@
    1.92    then have i: "i \<in> Basis" by auto
    1.93    have *: "{x::'a. x\<bullet>i \<le> a} = space ?SIGMA - {x::'a. a < x\<bullet>i}" by auto
    1.94    show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA" unfolding *
    1.95 -    by (safe intro!: sets.compl_sets) (auto intro: i)
    1.96 +    by (intro sets.compl_sets) (auto intro: i)
    1.97  qed auto
    1.98  
    1.99  lemma borel_eq_atMost:
   1.100 @@ -723,7 +725,7 @@
   1.101        by (auto intro!: exI[of _ k])
   1.102    qed
   1.103    show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA" unfolding *
   1.104 -    by (safe intro!: sets.countable_UN) auto
   1.105 +    by (intro sets.countable_UN) auto
   1.106  qed auto
   1.107  
   1.108  lemma borel_eq_greaterThan:
   1.109 @@ -748,7 +750,7 @@
   1.110    qed
   1.111    finally show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA"
   1.112      apply (simp only:)
   1.113 -    apply (safe intro!: sets.countable_UN sets.Diff)
   1.114 +    apply (intro sets.countable_UN sets.Diff)
   1.115      apply (auto intro: sigma_sets_top)
   1.116      done
   1.117  qed auto
   1.118 @@ -774,7 +776,7 @@
   1.119    qed
   1.120    finally show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA"
   1.121      apply (simp only:)
   1.122 -    apply (safe intro!: sets.countable_UN sets.Diff)
   1.123 +    apply (intro sets.countable_UN sets.Diff)
   1.124      apply (auto intro: sigma_sets_top )
   1.125      done
   1.126  qed auto
   1.127 @@ -797,7 +799,7 @@
   1.128        by (auto intro!: exI[of _ k])
   1.129    qed
   1.130    show "{..a} \<in> ?SIGMA" unfolding *
   1.131 -    by (safe intro!: sets.countable_UN)
   1.132 +    by (intro sets.countable_UN)
   1.133         (auto intro!: sigma_sets_top)
   1.134  qed auto
   1.135  
   1.136 @@ -822,7 +824,7 @@
   1.137    have "{..<x} = (\<Union>i::nat. {-real i ..< x})"
   1.138      by (auto simp: move_uminus real_arch_simple)
   1.139    then show "{y. y <e x} \<in> ?SIGMA"
   1.140 -    by (auto intro: sigma_sets.intros simp: eucl_lessThan)
   1.141 +    by (auto intro: sigma_sets.intros(2-) simp: eucl_lessThan)
   1.142  qed auto
   1.143  
   1.144  lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
   1.145 @@ -831,15 +833,13 @@
   1.146    fix x :: "'a set" assume "open x"
   1.147    hence "x = UNIV - (UNIV - x)" by auto
   1.148    also have "\<dots> \<in> sigma_sets UNIV (Collect closed)"
   1.149 -    by (rule sigma_sets.Compl)
   1.150 -       (auto intro!: sigma_sets.Basic simp: `open x`)
   1.151 +    by (force intro: sigma_sets.Compl simp: `open x`)
   1.152    finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp
   1.153  next
   1.154    fix x :: "'a set" assume "closed x"
   1.155    hence "x = UNIV - (UNIV - x)" by auto
   1.156    also have "\<dots> \<in> sigma_sets UNIV (Collect open)"
   1.157 -    by (rule sigma_sets.Compl)
   1.158 -       (auto intro!: sigma_sets.Basic simp: `closed x`)
   1.159 +    by (force intro: sigma_sets.Compl simp: `closed x`)
   1.160    finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
   1.161  qed simp_all
   1.162  
   1.163 @@ -1151,14 +1151,10 @@
   1.164    fixes f :: "'a \<Rightarrow> ereal" 
   1.165    assumes f: "f \<in> borel_measurable M"
   1.166    shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
   1.167 -proof -
   1.168 -  have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) \<in> borel_measurable M"
   1.169 -    using continuous_on_real
   1.170 -    by (rule borel_measurable_continuous_on_open[OF _ _ f]) auto
   1.171 -  also have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) = (\<lambda>x. real (f x))"
   1.172 -    by auto
   1.173 -  finally show ?thesis .
   1.174 -qed
   1.175 +  apply (rule measurable_compose[OF f])
   1.176 +  apply (rule borel_measurable_continuous_countable_exceptions[of "{\<infinity>, -\<infinity> }"])
   1.177 +  apply (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV)
   1.178 +  done
   1.179  
   1.180  lemma borel_measurable_ereal_cases:
   1.181    fixes f :: "'a \<Rightarrow> ereal" 
   1.182 @@ -1229,83 +1225,31 @@
   1.183    finally show "f \<in> borel_measurable M" .
   1.184  qed simp_all
   1.185  
   1.186 -lemma borel_measurable_eq_atMost_ereal:
   1.187 -  fixes f :: "'a \<Rightarrow> ereal"
   1.188 -  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
   1.189 -proof (intro iffI allI)
   1.190 -  assume pos[rule_format]: "\<forall>a. f -` {..a} \<inter> space M \<in> sets M"
   1.191 -  show "f \<in> borel_measurable M"
   1.192 -    unfolding borel_measurable_ereal_iff_real borel_measurable_iff_le
   1.193 -  proof (intro conjI allI)
   1.194 -    fix a :: real
   1.195 -    { fix x :: ereal assume *: "\<forall>i::nat. real i < x"
   1.196 -      have "x = \<infinity>"
   1.197 -      proof (rule ereal_top)
   1.198 -        fix B from reals_Archimedean2[of B] guess n ..
   1.199 -        then have "ereal B < real n" by auto
   1.200 -        with * show "B \<le> x" by (metis less_trans less_imp_le)
   1.201 -      qed }
   1.202 -    then have "f -` {\<infinity>} \<inter> space M = space M - (\<Union>i::nat. f -` {.. real i} \<inter> space M)"
   1.203 -      by (auto simp: not_le)
   1.204 -    then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos
   1.205 -      by (auto simp del: UN_simps)
   1.206 -    moreover
   1.207 -    have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto
   1.208 -    then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
   1.209 -    moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"
   1.210 -      using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute)
   1.211 -    moreover have "{w \<in> space M. real (f w) \<le> a} =
   1.212 -      (if a < 0 then {w \<in> space M. f w \<le> ereal a} - f -` {-\<infinity>} \<inter> space M
   1.213 -      else {w \<in> space M. f w \<le> ereal a} \<union> (f -` {\<infinity>} \<inter> space M) \<union> (f -` {-\<infinity>} \<inter> space M))" (is "?l = ?r")
   1.214 -      proof (intro set_eqI) fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases "f x") auto qed
   1.215 -    ultimately show "{w \<in> space M. real (f w) \<le> a} \<in> sets M" by auto
   1.216 -  qed
   1.217 -qed (simp add: measurable_sets)
   1.218 +lemma borel_measurable_ereal_iff_Iio:
   1.219 +  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)"
   1.220 +  by (auto simp: borel_Iio measurable_iff_measure_of)
   1.221 +
   1.222 +lemma borel_measurable_ereal_iff_Ioi:
   1.223 +  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)"
   1.224 +  by (auto simp: borel_Ioi measurable_iff_measure_of)
   1.225  
   1.226 -lemma borel_measurable_eq_atLeast_ereal:
   1.227 -  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)"
   1.228 -proof
   1.229 -  assume pos: "\<forall>a. f -` {a..} \<inter> space M \<in> sets M"
   1.230 -  moreover have "\<And>a. (\<lambda>x. - f x) -` {..a} = f -` {-a ..}"
   1.231 -    by (auto simp: ereal_uminus_le_reorder)
   1.232 -  ultimately have "(\<lambda>x. - f x) \<in> borel_measurable M"
   1.233 -    unfolding borel_measurable_eq_atMost_ereal by auto
   1.234 -  then show "f \<in> borel_measurable M" by simp
   1.235 -qed (simp add: measurable_sets)
   1.236 -
   1.237 -lemma greater_eq_le_measurable:
   1.238 -  fixes f :: "'a \<Rightarrow> 'c::linorder"
   1.239 -  shows "f -` {..< a} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {a ..} \<inter> space M \<in> sets M"
   1.240 -proof
   1.241 -  assume "f -` {a ..} \<inter> space M \<in> sets M"
   1.242 -  moreover have "f -` {..< a} \<inter> space M = space M - f -` {a ..} \<inter> space M" by auto
   1.243 -  ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
   1.244 -next
   1.245 -  assume "f -` {..< a} \<inter> space M \<in> sets M"
   1.246 -  moreover have "f -` {a ..} \<inter> space M = space M - f -` {..< a} \<inter> space M" by auto
   1.247 -  ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
   1.248 +lemma vimage_sets_compl_iff:
   1.249 +  "f -` A \<inter> space M \<in> sets M \<longleftrightarrow> f -` (- A) \<inter> space M \<in> sets M"
   1.250 +proof -
   1.251 +  { fix A assume "f -` A \<inter> space M \<in> sets M"
   1.252 +    moreover have "f -` (- A) \<inter> space M = space M - f -` A \<inter> space M" by auto
   1.253 +    ultimately have "f -` (- A) \<inter> space M \<in> sets M" by auto }
   1.254 +  from this[of A] this[of "-A"] show ?thesis
   1.255 +    by (metis double_complement)
   1.256  qed
   1.257  
   1.258 -lemma borel_measurable_ereal_iff_less:
   1.259 -  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)"
   1.260 -  unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable ..
   1.261 +lemma borel_measurable_iff_Iic_ereal:
   1.262 +  "(f::'a\<Rightarrow>ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
   1.263 +  unfolding borel_measurable_ereal_iff_Ioi vimage_sets_compl_iff[where A="{a <..}" for a] by simp
   1.264  
   1.265 -lemma less_eq_ge_measurable:
   1.266 -  fixes f :: "'a \<Rightarrow> 'c::linorder"
   1.267 -  shows "f -` {a <..} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {..a} \<inter> space M \<in> sets M"
   1.268 -proof
   1.269 -  assume "f -` {a <..} \<inter> space M \<in> sets M"
   1.270 -  moreover have "f -` {..a} \<inter> space M = space M - f -` {a <..} \<inter> space M" by auto
   1.271 -  ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
   1.272 -next
   1.273 -  assume "f -` {..a} \<inter> space M \<in> sets M"
   1.274 -  moreover have "f -` {a <..} \<inter> space M = space M - f -` {..a} \<inter> space M" by auto
   1.275 -  ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
   1.276 -qed
   1.277 -
   1.278 -lemma borel_measurable_ereal_iff_ge:
   1.279 -  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)"
   1.280 -  unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable ..
   1.281 +lemma borel_measurable_iff_Ici_ereal:
   1.282 +  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)"
   1.283 +  unfolding borel_measurable_ereal_iff_Iio vimage_sets_compl_iff[where A="{..< a}" for a] by simp
   1.284  
   1.285  lemma borel_measurable_ereal2:
   1.286    fixes f g :: "'a \<Rightarrow> ereal" 
   1.287 @@ -1352,20 +1296,13 @@
   1.288    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   1.289    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   1.290    shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
   1.291 -proof cases
   1.292 -  assume "finite S"
   1.293 -  thus ?thesis using assms
   1.294 -    by induct auto
   1.295 -qed simp
   1.296 +  using assms by (induction S rule: infinite_finite_induct) auto
   1.297  
   1.298  lemma borel_measurable_ereal_setprod[measurable (raw)]:
   1.299    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   1.300    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   1.301    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
   1.302 -proof cases
   1.303 -  assume "finite S"
   1.304 -  thus ?thesis using assms by induct auto
   1.305 -qed simp
   1.306 +  using assms by (induction S rule: infinite_finite_induct) auto
   1.307  
   1.308  lemma [measurable (raw)]:
   1.309    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
     2.1 --- a/src/HOL/Probability/Measurable.thy	Wed Jan 14 17:04:19 2015 +0100
     2.2 +++ b/src/HOL/Probability/Measurable.thy	Thu Jan 15 15:04:51 2015 +0100
     2.3 @@ -97,6 +97,7 @@
     2.4  
     2.5  declare measurable_cong_sets[measurable_cong]
     2.6  declare sets_restrict_space_cong[measurable_cong]
     2.7 +declare sets_restrict_UNIV[measurable_cong]
     2.8  
     2.9  lemma predE[measurable (raw)]: 
    2.10    "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
     3.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Jan 14 17:04:19 2015 +0100
     3.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Jan 15 15:04:51 2015 +0100
     3.3 @@ -2440,6 +2440,9 @@
     3.4      by simp
     3.5  qed
     3.6  
     3.7 +lemma sets_restrict_UNIV[simp]: "sets (restrict_space M UNIV) = sets M"
     3.8 +  by (auto simp add: sets_restrict_space)
     3.9 +
    3.10  lemma sets_restrict_space_iff:
    3.11    "\<Omega> \<inter> space M \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
    3.12  proof (subst sets_restrict_space, safe)
    3.13 @@ -2525,5 +2528,40 @@
    3.14      by (auto simp add: sets_restrict_space_iff space_restrict_space)
    3.15  qed
    3.16  
    3.17 +lemma measurableI:
    3.18 +  "(\<And>x. x \<in> space M \<Longrightarrow> f x \<in> space N) \<Longrightarrow>
    3.19 +    (\<And>A. A \<in> sets N \<Longrightarrow> f -` A \<inter> space M \<in> sets M) \<Longrightarrow>
    3.20 +    f \<in> measurable M N"
    3.21 +  by (auto simp: measurable_def)
    3.22 +
    3.23 +lemma measurable_piecewise_restrict:
    3.24 +  assumes I: "countable I" and X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" "(\<Union>i\<in>I. X i) = space M"
    3.25 +    and meas: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> measurable (restrict_space M (X i)) N"
    3.26 +    and eq: "\<And>i x. i \<in> I \<Longrightarrow> x \<in> X i \<Longrightarrow> f i x = f' x"
    3.27 +  shows "f' \<in> measurable M N"
    3.28 +proof (rule measurableI)
    3.29 +  fix x assume "x \<in> space M"
    3.30 +  then obtain i where "i \<in> I" "x \<in> X i"
    3.31 +    using X by auto
    3.32 +  then show "f' x \<in> space N"
    3.33 +    using eq[of i x] meas[THEN measurable_space, of i x] `x \<in> space M`
    3.34 +    by (auto simp: space_restrict_space)
    3.35 +next
    3.36 +  fix A assume A: "A \<in> sets N"
    3.37 +  have "f' -` A \<inter> space M = {x \<in> space M. \<forall>i\<in>I. x \<in> X i \<longrightarrow> f i x \<in> A}"
    3.38 +    by (auto simp: eq X(2)[symmetric])
    3.39 +  also have "\<dots> \<in> sets M"
    3.40 +  proof (intro sets.sets_Collect_countable_All'[OF _ I])
    3.41 +    fix i assume "i \<in> I"
    3.42 +    then have "(f i -` A \<inter> X i) \<union> (space M - X i) \<in> sets M"
    3.43 +      using meas[THEN measurable_sets, OF `i \<in> I` A] X(1)
    3.44 +      by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
    3.45 +    also have "(f i -` A \<inter> X i) \<union> (space M - X i) = {x \<in> space M. x \<in> X i \<longrightarrow> f i x \<in> A}"
    3.46 +      using `i \<in> I` by (auto simp: X(2)[symmetric])
    3.47 +    finally show "{x \<in> space M. x \<in> X i \<longrightarrow> f i x \<in> A} \<in> sets M" .
    3.48 +  qed
    3.49 +  finally show "f' -` A \<inter> space M \<in> sets M" .
    3.50 +qed
    3.51 +
    3.52  end
    3.53