author hoelzl Fri Nov 02 14:23:54 2012 +0100 (2012-11-02) changeset 50003 8c213922ed49 parent 50002 ce0d316b5b44 child 50004 c96e8e40d789
use measurability prover
```     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
1.3 @@ -50,7 +50,7 @@
1.4    "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
1.5    unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
1.6
1.7 -lemma pair_measureI[intro, simp]:
1.8 +lemma pair_measureI[intro, simp, measurable]:
1.9    "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^isub>M B)"
1.10    by (auto simp: sets_pair_measure)
1.11
1.12 @@ -61,7 +61,11 @@
1.13    unfolding pair_measure_def using 1 2
1.14    by (intro measurable_measure_of) (auto dest: sets_into_space)
1.15
1.16 -lemma measurable_Pair:
1.17 +lemma measurable_split_replace[measurable (raw)]:
1.18 +  "(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. split (f x) (g x)) \<in> measurable M N"
1.19 +  unfolding split_beta' .
1.20 +
1.21 +lemma measurable_Pair[measurable (raw)]:
1.22    assumes f: "f \<in> measurable M M1" and g: "g \<in> measurable M M2"
1.23    shows "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
1.24  proof (rule measurable_pair_measureI)
1.25 @@ -75,34 +79,38 @@
1.26    finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" .
1.27  qed
1.28
1.29 +lemma measurable_Pair_compose_split[measurable_dest]:
1.30 +  assumes f: "split f \<in> measurable (M1 \<Otimes>\<^isub>M M2) N"
1.31 +  assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2"
1.32 +  shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N"
1.33 +  using measurable_compose[OF measurable_Pair f, OF g h] by simp
1.34 +
1.35  lemma measurable_pair:
1.36    assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
1.37    shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
1.38    using measurable_Pair[OF assms] by simp
1.39
1.40 -lemma measurable_fst[intro!, simp]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
1.41 +lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
1.42    by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
1.43
1.44 -lemma measurable_snd[intro!, simp]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
1.45 +lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
1.46    by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
1.47
1.48 -lemma measurable_fst': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. fst (f x)) \<in> measurable M N"
1.49 -  using measurable_comp[OF _ measurable_fst] by (auto simp: comp_def)
1.50 -
1.51 -lemma measurable_snd': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. snd (f x)) \<in> measurable M P"
1.52 -    using measurable_comp[OF _ measurable_snd] by (auto simp: comp_def)
1.53 +lemma
1.54 +  assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^isub>M P)"
1.55 +  shows measurable_fst': "(\<lambda>x. fst (f x)) \<in> measurable M N"
1.56 +    and measurable_snd': "(\<lambda>x. snd (f x)) \<in> measurable M P"
1.57 +  by simp_all
1.58
1.59 -lemma measurable_fst'': "f \<in> measurable M N \<Longrightarrow> (\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^isub>M P) N"
1.60 -  using measurable_comp[OF measurable_fst _] by (auto simp: comp_def)
1.61 -
1.62 -lemma measurable_snd'': "f \<in> measurable M N \<Longrightarrow> (\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^isub>M M) N"
1.63 -  using measurable_comp[OF measurable_snd _] by (auto simp: comp_def)
1.64 +lemma
1.65 +  assumes f[measurable]: "f \<in> measurable M N"
1.66 +  shows measurable_fst'': "(\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^isub>M P) N"
1.67 +    and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^isub>M M) N"
1.68 +  by simp_all
1.69
1.70  lemma measurable_pair_iff:
1.71    "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
1.72 -  using measurable_pair[of f M M1 M2]
1.73 -  using [[simproc del: measurable]] (* the measurable method is nonterminating when using measurable_pair *)
1.74 -  by auto
1.75 +  by (auto intro: measurable_pair[of f M M1 M2])
1.76
1.77  lemma measurable_split_conv:
1.78    "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"
1.79 @@ -117,16 +125,13 @@
1.80
1.81  lemma measurable_pair_swap_iff:
1.82    "f \<in> measurable (M2 \<Otimes>\<^isub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) M"
1.83 -  using measurable_pair_swap[of "\<lambda>(x,y). f (y, x)"]
1.84 -  by (auto intro!: measurable_pair_swap)
1.85 -
1.86 -lemma measurable_ident[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
1.87 -  unfolding measurable_def by auto
1.88 +  by (auto dest: measurable_pair_swap)
1.89
1.90  lemma measurable_Pair1': "x \<in> space M1 \<Longrightarrow> Pair x \<in> measurable M2 (M1 \<Otimes>\<^isub>M M2)"
1.91 -  by (auto intro!: measurable_Pair)
1.92 +  by simp
1.93
1.94 -lemma sets_Pair1: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
1.95 +lemma sets_Pair1[measurable (raw)]:
1.96 +  assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
1.97  proof -
1.98    have "Pair x -` A = (if x \<in> space M1 then Pair x -` A \<inter> space M2 else {})"
1.99      using A[THEN sets_into_space] by (auto simp: space_pair_measure)
1.100 @@ -163,8 +168,11 @@
1.101    unfolding Int_stable_def
1.102    by safe (auto simp add: times_Int_times)
1.103
1.104 +lemma disjoint_family_vimageI: "disjoint_family F \<Longrightarrow> disjoint_family (\<lambda>i. f -` F i)"
1.105 +  by (auto simp: disjoint_family_on_def)
1.106 +
1.107  lemma (in finite_measure) finite_measure_cut_measurable:
1.108 -  assumes "Q \<in> sets (N \<Otimes>\<^isub>M M)"
1.109 +  assumes [measurable]: "Q \<in> sets (N \<Otimes>\<^isub>M M)"
1.110    shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N"
1.111      (is "?s Q \<in> _")
1.112    using Int_stable_pair_measure_generator pair_measure_closed assms
1.113 @@ -179,11 +187,10 @@
1.114      by (auto intro!: measurable_If simp: space_pair_measure)
1.115  next
1.116    case (union F)
1.117 -  moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
1.118 -    unfolding sets_pair_measure[symmetric]
1.119 -    by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
1.120 +  moreover then have *: "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
1.121 +    by (simp add: suminf_emeasure disjoint_family_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])
1.122    ultimately show ?case
1.123 -    by (auto simp: vimage_UN)
1.124 +    unfolding sets_pair_measure[symmetric] by simp
1.125  qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
1.126
1.127  lemma (in sigma_finite_measure) measurable_emeasure_Pair:
1.128 @@ -226,6 +233,17 @@
1.129      by auto
1.130  qed
1.131
1.132 +lemma (in sigma_finite_measure) measurable_emeasure[measurable (raw)]:
1.133 +  assumes space: "\<And>x. x \<in> space N \<Longrightarrow> A x \<subseteq> space M"
1.134 +  assumes A: "{x\<in>space (N \<Otimes>\<^isub>M M). snd x \<in> A (fst x)} \<in> sets (N \<Otimes>\<^isub>M M)"
1.135 +  shows "(\<lambda>x. emeasure M (A x)) \<in> borel_measurable N"
1.136 +proof -
1.137 +  from space have "\<And>x. x \<in> space N \<Longrightarrow> Pair x -` {x \<in> space (N \<Otimes>\<^isub>M M). snd x \<in> A (fst x)} = A x"
1.138 +    by (auto simp: space_pair_measure)
1.139 +  with measurable_emeasure_Pair[OF A] show ?thesis
1.140 +    by (auto cong: measurable_cong)
1.141 +qed
1.142 +
1.143  lemma (in sigma_finite_measure) emeasure_pair_measure:
1.144    assumes "X \<in> sets (N \<Otimes>\<^isub>M M)"
1.145    shows "emeasure (N \<Otimes>\<^isub>M M) X = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator X (x, y) \<partial>M \<partial>N)" (is "_ = ?\<mu> X")
1.146 @@ -476,7 +494,7 @@
1.147
1.148  lemma measurable_compose_Pair1:
1.149    "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^isub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
1.150 -  by (rule measurable_compose[OF measurable_Pair]) auto
1.151 +  by simp
1.152
1.153  lemma (in sigma_finite_measure) borel_measurable_positive_integral_fst':
1.154    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M)" "\<And>x. 0 \<le> f x"
1.155 @@ -527,9 +545,13 @@
1.156      positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
1.157    unfolding positive_integral_max_0 by auto
1.158
1.159 -lemma (in sigma_finite_measure) borel_measurable_positive_integral:
1.160 -  "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M) \<in> borel_measurable M1"
1.161 -  using positive_integral_fst_measurable(1)[of "split f" M1] by simp
1.162 +lemma (in sigma_finite_measure) borel_measurable_positive_integral[measurable (raw)]:
1.163 +  "split f \<in> borel_measurable (N \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M) \<in> borel_measurable N"
1.164 +  using positive_integral_fst_measurable(1)[of "split f" N] by simp
1.165 +
1.166 +lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
1.167 +  "split f \<in> borel_measurable (N \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral> y. f x y \<partial>M) \<in> borel_measurable N"
1.168 +  by (simp add: lebesgue_integral_def)
1.169
1.170  lemma (in pair_sigma_finite) positive_integral_snd_measurable:
1.171    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
1.172 @@ -650,29 +672,6 @@
1.173      by simp
1.174  qed
1.175
1.176 -lemma (in pair_sigma_finite) positive_integral_fst_measurable':
1.177 -  assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
1.178 -  shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
1.179 -  using M2.positive_integral_fst_measurable(1)[OF f] by simp
1.180 -
1.181 -lemma (in pair_sigma_finite) integral_fst_measurable:
1.182 -  "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral> y. f x y \<partial>M2) \<in> borel_measurable M1"
1.183 -  by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_fst_measurable')
1.184 -
1.185 -lemma (in pair_sigma_finite) positive_integral_snd_measurable':
1.186 -  assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
1.187 -  shows "(\<lambda>y. \<integral>\<^isup>+ x. f x y \<partial>M1) \<in> borel_measurable M2"
1.188 -proof -
1.189 -  interpret Q: pair_sigma_finite M2 M1 ..
1.190 -  show ?thesis
1.191 -    using measurable_pair_swap[OF f]
1.192 -    by (intro Q.positive_integral_fst_measurable') (simp add: split_beta')
1.193 -qed
1.194 -
1.195 -lemma (in pair_sigma_finite) integral_snd_measurable:
1.196 -  "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>y. \<integral> x. f x y \<partial>M1) \<in> borel_measurable M2"
1.197 -  by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_snd_measurable')
1.198 -
1.199  lemma (in pair_sigma_finite) Fubini_integral:
1.200    assumes f: "integrable (M1 \<Otimes>\<^isub>M M2) f"
1.201    shows "(\<integral>y. (\<integral>x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1)"
1.202 @@ -739,48 +738,21 @@
1.203  lemma pair_measure_density:
1.204    assumes f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x"
1.205    assumes g: "g \<in> borel_measurable M2" "AE x in M2. 0 \<le> g x"
1.206 -  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
1.207 -  assumes "sigma_finite_measure (density M1 f)" "sigma_finite_measure (density M2 g)"
1.208 +  assumes "sigma_finite_measure M2" "sigma_finite_measure (density M2 g)"
1.209    shows "density M1 f \<Otimes>\<^isub>M density M2 g = density (M1 \<Otimes>\<^isub>M M2) (\<lambda>(x,y). f x * g y)" (is "?L = ?R")
1.210  proof (rule measure_eqI)
1.211 -  interpret M1: sigma_finite_measure M1 by fact
1.212    interpret M2: sigma_finite_measure M2 by fact
1.213 -  interpret D1: sigma_finite_measure "density M1 f" by fact
1.214    interpret D2: sigma_finite_measure "density M2 g" by fact
1.215 -  interpret L: pair_sigma_finite "density M1 f" "density M2 g" ..
1.216 -  interpret R: pair_sigma_finite M1 M2 ..
1.217
1.218    fix A assume A: "A \<in> sets ?L"
1.219 -  then have indicator_eq: "\<And>x y. indicator A (x, y) = indicator (Pair x -` A) y"
1.220 -   and Pair_A: "\<And>x. Pair x -` A \<in> sets M2"
1.221 -    by (auto simp: indicator_def sets_Pair1)
1.222 -  have f_fst: "(\<lambda>p. f (fst p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
1.223 -    using measurable_comp[OF measurable_fst f(1)] by (simp add: comp_def)
1.224 -  have g_snd: "(\<lambda>p. g (snd p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
1.225 -    using measurable_comp[OF measurable_snd g(1)] by (simp add: comp_def)
1.226 -  have "(\<lambda>x. \<integral>\<^isup>+ y. g (snd (x, y)) * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1"
1.227 -    using g_snd Pair_A A by (intro M2.positive_integral_fst_measurable) auto
1.228 -  then have int_g: "(\<lambda>x. \<integral>\<^isup>+ y. g y * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1"
1.229 -    by simp
1.230 -
1.231 -  show "emeasure ?L A = emeasure ?R A"
1.232 -    apply (subst D2.emeasure_pair_measure[OF A])
1.233 -    apply (subst emeasure_density)
1.234 -        using f_fst g_snd apply (simp add: split_beta')
1.235 -      using A apply simp
1.236 -    apply (subst positive_integral_density[OF g])
1.237 -      apply (simp add: indicator_eq Pair_A)
1.238 -    apply (subst positive_integral_density[OF f])
1.239 -      apply (rule int_g)
1.240 -    apply (subst M2.positive_integral_fst_measurable(2)[symmetric])
1.241 -      using f g A Pair_A f_fst g_snd
1.242 -      apply (auto intro!: positive_integral_cong_AE R.measurable_emeasure_Pair1
1.243 -                  simp: positive_integral_cmult indicator_eq split_beta')
1.244 -    apply (intro AE_I2 impI)
1.245 -    apply (subst mult_assoc)
1.246 -    apply (subst positive_integral_cmult)
1.247 -          apply auto
1.248 -    done
1.249 +  with f g have "(\<integral>\<^isup>+ x. f x * \<integral>\<^isup>+ y. g y * indicator A (x, y) \<partial>M2 \<partial>M1) =
1.250 +    (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. f x * g y * indicator A (x, y) \<partial>M2 \<partial>M1)"
1.251 +    by (intro positive_integral_cong_AE)
1.252 +       (auto simp add: positive_integral_cmult[symmetric] ac_simps)
1.253 +  with A f g show "emeasure ?L A = emeasure ?R A"
1.254 +    by (simp add: D2.emeasure_pair_measure emeasure_density positive_integral_density
1.255 +                  M2.positive_integral_fst_measurable(2)[symmetric]
1.256 +             cong: positive_integral_cong)
1.257  qed simp
1.258
1.259  lemma sigma_finite_measure_distr:
1.260 @@ -792,7 +764,7 @@
1.261    show ?thesis
1.262    proof (unfold_locales, intro conjI exI allI)
1.263      show "range (\<lambda>i. f -` A i \<inter> space M) \<subseteq> sets M"
1.264 -      using A f by (auto intro!: measurable_sets)
1.265 +      using A f by auto
1.266      show "(\<Union>i. f -` A i \<inter> space M) = space M"
1.267        using A(1) A(2)[symmetric] f by (auto simp: measurable_def Pi_def)
1.268      fix i show "emeasure M (f -` A i \<inter> space M) \<noteq> \<infinity>"
1.269 @@ -800,47 +772,19 @@
1.270    qed
1.271  qed
1.272
1.273 -lemma measurable_cong':
1.274 -  assumes sets: "sets M = sets M'" "sets N = sets N'"
1.275 -  shows "measurable M N = measurable M' N'"
1.276 -  using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def)
1.277 -
1.278  lemma pair_measure_distr:
1.279    assumes f: "f \<in> measurable M S" and g: "g \<in> measurable N T"
1.280 -  assumes "sigma_finite_measure (distr M S f)" "sigma_finite_measure (distr N T g)"
1.281 +  assumes "sigma_finite_measure (distr N T g)"
1.282    shows "distr M S f \<Otimes>\<^isub>M distr N T g = distr (M \<Otimes>\<^isub>M N) (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). (f x, g y))" (is "?P = ?D")
1.283  proof (rule measure_eqI)
1.284 -  show "sets ?P = sets ?D"
1.285 -    by simp
1.286 -  interpret S: sigma_finite_measure "distr M S f" by fact
1.287    interpret T: sigma_finite_measure "distr N T g" by fact
1.288 -  interpret ST: pair_sigma_finite "distr M S f"  "distr N T g" ..
1.289 -  interpret M: sigma_finite_measure M by (rule sigma_finite_measure_distr) fact+
1.290    interpret N: sigma_finite_measure N by (rule sigma_finite_measure_distr) fact+
1.291 -  interpret MN: pair_sigma_finite M N ..
1.292 -  interpret SN: pair_sigma_finite "distr M S f" N ..
1.293 -  have [simp]:
1.294 -    "\<And>f g. fst \<circ> (\<lambda>(x, y). (f x, g y)) = f \<circ> fst" "\<And>f g. snd \<circ> (\<lambda>(x, y). (f x, g y)) = g \<circ> snd"
1.295 -    by auto
1.296 -  then have fg: "(\<lambda>(x, y). (f x, g y)) \<in> measurable (M \<Otimes>\<^isub>M N) (S \<Otimes>\<^isub>M T)"
1.297 -    using measurable_comp[OF measurable_fst f] measurable_comp[OF measurable_snd g]
1.298 -    by (auto simp: measurable_pair_iff)
1.299 +
1.300    fix A assume A: "A \<in> sets ?P"
1.301 -  then have "emeasure ?P A = (\<integral>\<^isup>+x. emeasure (distr N T g) (Pair x -` A) \<partial>distr M S f)"
1.302 -    by (rule T.emeasure_pair_measure_alt)
1.303 -  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair x -` A) \<inter> space N) \<partial>distr M S f)"
1.304 -    using g A by (simp add: sets_Pair1 emeasure_distr)
1.305 -  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair (f x) -` A) \<inter> space N) \<partial>M)"
1.306 -    using f g A ST.measurable_emeasure_Pair1[OF A]
1.307 -    by (intro positive_integral_distr) (auto simp add: sets_Pair1 emeasure_distr)
1.308 -  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (Pair x -` ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))) \<partial>M)"
1.309 -    by (intro positive_integral_cong arg_cong2[where f=emeasure]) (auto simp: space_pair_measure)
1.310 -  also have "\<dots> = emeasure (M \<Otimes>\<^isub>M N) ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))"
1.311 -    using fg by (intro N.emeasure_pair_measure_alt[symmetric] measurable_sets[OF _ A])
1.312 -                (auto cong: measurable_cong')
1.313 -  also have "\<dots> = emeasure ?D A"
1.314 -    using fg A by (subst emeasure_distr) auto
1.315 -  finally show "emeasure ?P A = emeasure ?D A" .
1.316 -qed
1.317 +  with f g show "emeasure ?P A = emeasure ?D A"
1.318 +    by (auto simp add: N.emeasure_pair_measure_alt space_pair_measure emeasure_distr
1.319 +                       T.emeasure_pair_measure_alt positive_integral_distr
1.320 +             intro!: positive_integral_cong arg_cong[where f="emeasure N"])
1.321 +qed simp
1.322
1.323  end
1.324 \ No newline at end of file
```
```     2.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:23:40 2012 +0100
2.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:23:54 2012 +0100
2.3 @@ -36,14 +36,14 @@
2.4  lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
2.5    unfolding borel_def pred_def by auto
2.6
2.7 -lemma borel_open[simp, measurable (raw generic)]:
2.8 +lemma borel_open[measurable (raw generic)]:
2.9    assumes "open A" shows "A \<in> sets borel"
2.10  proof -
2.11    have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
2.12    thus ?thesis unfolding borel_def by auto
2.13  qed
2.14
2.15 -lemma borel_closed[simp, measurable (raw generic)]:
2.16 +lemma borel_closed[measurable (raw generic)]:
2.17    assumes "closed A" shows "A \<in> sets borel"
2.18  proof -
2.19    have "space borel - (- A) \<in> sets borel"
2.20 @@ -51,11 +51,11 @@
2.21    thus ?thesis by simp
2.22  qed
2.23
2.24 -lemma borel_insert[measurable]:
2.25 -  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t2_space measure)"
2.26 +lemma borel_singleton[measurable]:
2.27 +  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
2.28    unfolding insert_def by (rule Un) auto
2.29
2.30 -lemma borel_comp[intro, simp, measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
2.31 +lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
2.32    unfolding Compl_eq_Diff_UNIV by simp
2.33
2.34  lemma borel_measurable_vimage:
2.35 @@ -74,19 +74,11 @@
2.36      using assms[of S] by simp
2.37  qed
2.38
2.39 -lemma borel_singleton[simp, intro]:
2.40 -  fixes x :: "'a::t1_space"
2.41 -  shows "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets borel"
2.42 -  proof (rule insert_in_sets)
2.43 -    show "{x} \<in> sets borel"
2.44 -      using closed_singleton[of x] by (rule borel_closed)
2.45 -  qed simp
2.46 -
2.47 -lemma borel_measurable_const[simp, intro, measurable (raw)]:
2.48 +lemma borel_measurable_const[measurable (raw)]:
2.49    "(\<lambda>x. c) \<in> borel_measurable M"
2.50    by auto
2.51
2.52 -lemma borel_measurable_indicator[simp, intro!]:
2.53 +lemma borel_measurable_indicator:
2.54    assumes A: "A \<in> sets M"
2.55    shows "indicator A \<in> borel_measurable M"
2.56    unfolding indicator_def [abs_def] using A
2.57 @@ -137,7 +129,7 @@
2.58    "(f :: 'a \<Rightarrow> 'b::euclidean_space) \<in> borel_measurable M \<Longrightarrow>(\<lambda>x. f x \$\$ i) \<in> borel_measurable M"
2.59    by simp
2.60
2.61 -lemma [simp, intro, measurable]:
2.62 +lemma [measurable]:
2.63    fixes a b :: "'a\<Colon>ordered_euclidean_space"
2.64    shows lessThan_borel: "{..< a} \<in> sets borel"
2.65      and greaterThan_borel: "{a <..} \<in> sets borel"
2.66 @@ -151,13 +143,13 @@
2.67    by (blast intro: borel_open borel_closed)+
2.68
2.69  lemma
2.70 -  shows hafspace_less_borel[simp, intro]: "{x::'a::euclidean_space. a < x \$\$ i} \<in> sets borel"
2.71 -    and hafspace_greater_borel[simp, intro]: "{x::'a::euclidean_space. x \$\$ i < a} \<in> sets borel"
2.72 -    and hafspace_less_eq_borel[simp, intro]: "{x::'a::euclidean_space. a \<le> x \$\$ i} \<in> sets borel"
2.73 -    and hafspace_greater_eq_borel[simp, intro]: "{x::'a::euclidean_space. x \$\$ i \<le> a} \<in> sets borel"
2.74 +  shows hafspace_less_borel: "{x::'a::euclidean_space. a < x \$\$ i} \<in> sets borel"
2.75 +    and hafspace_greater_borel: "{x::'a::euclidean_space. x \$\$ i < a} \<in> sets borel"
2.76 +    and hafspace_less_eq_borel: "{x::'a::euclidean_space. a \<le> x \$\$ i} \<in> sets borel"
2.77 +    and hafspace_greater_eq_borel: "{x::'a::euclidean_space. x \$\$ i \<le> a} \<in> sets borel"
2.78    by simp_all
2.79
2.80 -lemma borel_measurable_less[simp, intro, measurable]:
2.81 +lemma borel_measurable_less[measurable]:
2.82    fixes f :: "'a \<Rightarrow> real"
2.83    assumes f: "f \<in> borel_measurable M"
2.84    assumes g: "g \<in> borel_measurable M"
2.85 @@ -169,7 +161,7 @@
2.86      by simp
2.87  qed
2.88
2.89 -lemma [simp, intro]:
2.90 +lemma
2.91    fixes f :: "'a \<Rightarrow> real"
2.92    assumes f[measurable]: "f \<in> borel_measurable M"
2.93    assumes g[measurable]: "g \<in> borel_measurable M"
2.94 @@ -633,7 +625,7 @@
2.95    using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
2.97
2.98 -lemma borel_measurable_uminus[simp, intro, measurable (raw)]:
2.99 +lemma borel_measurable_uminus[measurable (raw)]:
2.100    fixes g :: "'a \<Rightarrow> real"
2.101    assumes g: "g \<in> borel_measurable M"
2.102    shows "(\<lambda>x. - g x) \<in> borel_measurable M"
2.103 @@ -644,7 +636,7 @@
2.104    shows "x \$\$ i = (if i < DIM('a) then fst x \$\$ i else snd x \$\$ (i - DIM('a)))"
2.105    unfolding euclidean_component_def basis_prod_def inner_prod_def by auto
2.106
2.107 -lemma borel_measurable_Pair[simp, intro, measurable (raw)]:
2.108 +lemma borel_measurable_Pair[measurable (raw)]:
2.109    fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
2.110    assumes f: "f \<in> borel_measurable M"
2.111    assumes g: "g \<in> borel_measurable M"
2.112 @@ -675,8 +667,8 @@
2.113
2.114  lemma borel_measurable_continuous_Pair:
2.115    fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
2.116 -  assumes [simp]: "f \<in> borel_measurable M"
2.117 -  assumes [simp]: "g \<in> borel_measurable M"
2.118 +  assumes [measurable]: "f \<in> borel_measurable M"
2.119 +  assumes [measurable]: "g \<in> borel_measurable M"
2.120    assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
2.121    shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
2.122  proof -
2.123 @@ -685,7 +677,7 @@
2.124      unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
2.125  qed
2.126
2.127 -lemma borel_measurable_add[simp, intro, measurable (raw)]:
2.129    fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
2.130    assumes f: "f \<in> borel_measurable M"
2.131    assumes g: "g \<in> borel_measurable M"
2.132 @@ -694,7 +686,7 @@
2.133    by (rule borel_measurable_continuous_Pair)
2.134       (auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
2.135
2.136 -lemma borel_measurable_setsum[simp, intro, measurable (raw)]:
2.137 +lemma borel_measurable_setsum[measurable (raw)]:
2.138    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
2.139    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
2.140    shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
2.141 @@ -703,14 +695,14 @@
2.142    thus ?thesis using assms by induct auto
2.143  qed simp
2.144
2.145 -lemma borel_measurable_diff[simp, intro, measurable (raw)]:
2.146 +lemma borel_measurable_diff[measurable (raw)]:
2.147    fixes f :: "'a \<Rightarrow> real"
2.148    assumes f: "f \<in> borel_measurable M"
2.149    assumes g: "g \<in> borel_measurable M"
2.150    shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
2.151 -  unfolding diff_minus using assms by fast
2.152 +  unfolding diff_minus using assms by simp
2.153
2.154 -lemma borel_measurable_times[simp, intro, measurable (raw)]:
2.155 +lemma borel_measurable_times[measurable (raw)]:
2.156    fixes f :: "'a \<Rightarrow> real"
2.157    assumes f: "f \<in> borel_measurable M"
2.158    assumes g: "g \<in> borel_measurable M"
2.159 @@ -724,7 +716,7 @@
2.160    shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
2.161    unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
2.162
2.163 -lemma borel_measurable_dist[simp, intro, measurable (raw)]:
2.164 +lemma borel_measurable_dist[measurable (raw)]:
2.165    fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
2.166    assumes f: "f \<in> borel_measurable M"
2.167    assumes g: "g \<in> borel_measurable M"
2.168 @@ -769,7 +761,7 @@
2.169    "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M"
2.170    using affine_borel_measurable_vector[of f M a 1] by simp
2.171
2.172 -lemma borel_measurable_setprod[simp, intro, measurable (raw)]:
2.173 +lemma borel_measurable_setprod[measurable (raw)]:
2.174    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
2.175    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
2.176    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
2.177 @@ -778,53 +770,36 @@
2.178    thus ?thesis using assms by induct auto
2.179  qed simp
2.180
2.181 -lemma borel_measurable_inverse[simp, intro, measurable (raw)]:
2.182 +lemma borel_measurable_inverse[measurable (raw)]:
2.183    fixes f :: "'a \<Rightarrow> real"
2.184    assumes f: "f \<in> borel_measurable M"
2.185    shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
2.186  proof -
2.187 -  have *: "\<And>x::real. inverse x = (if x \<in> UNIV - {0} then inverse x else 0)" by auto
2.188 -  show ?thesis
2.189 -    apply (subst *)
2.190 -    apply (rule borel_measurable_continuous_on_open)
2.191 -    apply (auto intro!: f continuous_on_inverse continuous_on_id)
2.192 -    done
2.193 +  have "(\<lambda>x::real. if x \<in> UNIV - {0} then inverse x else 0) \<in> borel_measurable borel"
2.194 +    by (intro borel_measurable_continuous_on_open' continuous_on_inverse continuous_on_id) auto
2.195 +  also have "(\<lambda>x::real. if x \<in> UNIV - {0} then inverse x else 0) = inverse" by (intro ext) auto
2.196 +  finally show ?thesis using f by simp
2.197  qed
2.198
2.199 -lemma borel_measurable_divide[simp, intro, measurable (raw)]:
2.200 -  fixes f :: "'a \<Rightarrow> real"
2.201 -  assumes "f \<in> borel_measurable M"
2.202 -  and "g \<in> borel_measurable M"
2.203 -  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
2.204 -  unfolding field_divide_inverse
2.205 -  by (rule borel_measurable_inverse borel_measurable_times assms)+
2.206 +lemma borel_measurable_divide[measurable (raw)]:
2.207 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. f x / g x::real) \<in> borel_measurable M"
2.208 +  by (simp add: field_divide_inverse)
2.209
2.210 -lemma borel_measurable_max[intro, simp, measurable (raw)]:
2.211 -  fixes f g :: "'a \<Rightarrow> real"
2.212 -  assumes "f \<in> borel_measurable M"
2.213 -  assumes "g \<in> borel_measurable M"
2.214 -  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
2.215 -  unfolding max_def by (auto intro!: assms measurable_If)
2.216 +lemma borel_measurable_max[measurable (raw)]:
2.217 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: real) \<in> borel_measurable M"
2.218 +  by (simp add: max_def)
2.219
2.220 -lemma borel_measurable_min[intro, simp, measurable (raw)]:
2.221 -  fixes f g :: "'a \<Rightarrow> real"
2.222 -  assumes "f \<in> borel_measurable M"
2.223 -  assumes "g \<in> borel_measurable M"
2.224 -  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
2.225 -  unfolding min_def by (auto intro!: assms measurable_If)
2.226 +lemma borel_measurable_min[measurable (raw)]:
2.227 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: real) \<in> borel_measurable M"
2.228 +  by (simp add: min_def)
2.229
2.230 -lemma borel_measurable_abs[simp, intro, measurable (raw)]:
2.231 -  assumes "f \<in> borel_measurable M"
2.232 -  shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
2.233 -proof -
2.234 -  have *: "\<And>x. \<bar>f x\<bar> = max 0 (f x) + max 0 (- f x)" by (simp add: max_def)
2.235 -  show ?thesis unfolding * using assms by auto
2.236 -qed
2.237 +lemma borel_measurable_abs[measurable (raw)]:
2.238 +  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
2.239 +  unfolding abs_real_def by simp
2.240
2.241 -lemma borel_measurable_nth[simp, intro, measurable (raw)]:
2.242 +lemma borel_measurable_nth[measurable (raw)]:
2.243    "(\<lambda>x::real^'n. x \$ i) \<in> borel_measurable borel"
2.244 -  using borel_measurable_euclidean_component'
2.245 -  unfolding nth_conv_component by auto
2.246 +  by (simp add: nth_conv_component)
2.247
2.248  lemma convex_measurable:
2.249    fixes a b :: real
2.250 @@ -843,7 +818,7 @@
2.251    finally show ?thesis .
2.252  qed
2.253
2.254 -lemma borel_measurable_ln[simp, intro, measurable (raw)]:
2.255 +lemma borel_measurable_ln[measurable (raw)]:
2.256    assumes f: "f \<in> borel_measurable M"
2.257    shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
2.258  proof -
2.259 @@ -864,7 +839,7 @@
2.260    finally show ?thesis .
2.261  qed
2.262
2.263 -lemma borel_measurable_log[simp, intro, measurable (raw)]:
2.264 +lemma borel_measurable_log[measurable (raw)]:
2.265    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
2.266    unfolding log_def by auto
2.267
2.268 @@ -902,17 +877,17 @@
2.269  lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
2.270    by simp
2.271
2.272 -lemma borel_measurable_real_natfloor[intro, simp]:
2.273 +lemma borel_measurable_real_natfloor:
2.274    "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
2.275    by simp
2.276
2.277  subsection "Borel space on the extended reals"
2.278
2.279 -lemma borel_measurable_ereal[simp, intro, measurable (raw)]:
2.280 +lemma borel_measurable_ereal[measurable (raw)]:
2.281    assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
2.282    using continuous_on_ereal f by (rule borel_measurable_continuous_on)
2.283
2.284 -lemma borel_measurable_real_of_ereal[simp, intro, measurable (raw)]:
2.285 +lemma borel_measurable_real_of_ereal[measurable (raw)]:
2.286    fixes f :: "'a \<Rightarrow> ereal"
2.287    assumes f: "f \<in> borel_measurable M"
2.288    shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
2.289 @@ -937,10 +912,10 @@
2.290  qed
2.291
2.292  lemma
2.293 -  fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M"
2.294 -  shows borel_measurable_ereal_abs[intro, simp, measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
2.295 -    and borel_measurable_ereal_inverse[simp, intro, measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
2.296 -    and borel_measurable_uminus_ereal[intro, measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
2.297 +  fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M"
2.298 +  shows borel_measurable_ereal_abs[measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
2.299 +    and borel_measurable_ereal_inverse[measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
2.300 +    and borel_measurable_uminus_ereal[measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
2.301    by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
2.302
2.303  lemma borel_measurable_uminus_eq_ereal[simp]:
2.304 @@ -968,15 +943,18 @@
2.305      by (subst *) (simp del: space_borel split del: split_if)
2.306  qed
2.307
2.308 -lemma
2.309 +lemma [measurable]:
2.310    fixes f g :: "'a \<Rightarrow> ereal"
2.311    assumes f: "f \<in> borel_measurable M"
2.312    assumes g: "g \<in> borel_measurable M"
2.313 -  shows borel_measurable_ereal_le[intro,simp,measurable(raw)]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
2.314 -    and borel_measurable_ereal_less[intro,simp,measurable(raw)]: "{x \<in> space M. f x < g x} \<in> sets M"
2.315 -    and borel_measurable_ereal_eq[intro,simp,measurable(raw)]: "{w \<in> space M. f w = g w} \<in> sets M"
2.316 -    and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
2.317 -  using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg)
2.318 +  shows borel_measurable_ereal_le: "{x \<in> space M. f x \<le> g x} \<in> sets M"
2.319 +    and borel_measurable_ereal_less: "{x \<in> space M. f x < g x} \<in> sets M"
2.320 +    and borel_measurable_ereal_eq: "{w \<in> space M. f w = g w} \<in> sets M"
2.321 +  using f g by (simp_all add: set_Collect_ereal2)
2.322 +
2.323 +lemma borel_measurable_ereal_neq:
2.324 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> {w \<in> space M. f w \<noteq> (g w :: ereal)} \<in> sets M"
2.325 +  by simp
2.326
2.327  lemma borel_measurable_ereal_iff:
2.328    shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
2.329 @@ -1102,24 +1080,24 @@
2.330      and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
2.331    using f by auto
2.332
2.333 -lemma [intro, simp, measurable(raw)]:
2.334 +lemma [measurable(raw)]:
2.335    fixes f :: "'a \<Rightarrow> ereal"
2.336 -  assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
2.337 +  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
2.338    shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
2.339      and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
2.340      and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
2.341      and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
2.342 -  by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def)
2.343 +  by (simp_all add: borel_measurable_ereal2 min_def max_def)
2.344
2.345 -lemma [simp, intro, measurable(raw)]:
2.346 +lemma [measurable(raw)]:
2.347    fixes f g :: "'a \<Rightarrow> ereal"
2.348    assumes "f \<in> borel_measurable M"
2.349    assumes "g \<in> borel_measurable M"
2.350    shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
2.351      and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
2.352 -  unfolding minus_ereal_def divide_ereal_def using assms by auto
2.353 +  using assms by (simp_all add: minus_ereal_def divide_ereal_def)
2.354
2.355 -lemma borel_measurable_ereal_setsum[simp, intro,measurable (raw)]:
2.356 +lemma borel_measurable_ereal_setsum[measurable (raw)]:
2.357    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
2.358    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
2.359    shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
2.360 @@ -1129,7 +1107,7 @@
2.361      by induct auto
2.362  qed simp
2.363
2.364 -lemma borel_measurable_ereal_setprod[simp, intro,measurable (raw)]:
2.365 +lemma borel_measurable_ereal_setprod[measurable (raw)]:
2.366    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
2.367    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
2.368    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
2.369 @@ -1138,7 +1116,7 @@
2.370    thus ?thesis using assms by induct auto
2.371  qed simp
2.372
2.373 -lemma borel_measurable_SUP[simp, intro,measurable (raw)]:
2.374 +lemma borel_measurable_SUP[measurable (raw)]:
2.375    fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
2.376    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
2.377    shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
2.378 @@ -1151,7 +1129,7 @@
2.379      using assms by auto
2.380  qed
2.381
2.382 -lemma borel_measurable_INF[simp, intro,measurable (raw)]:
2.383 +lemma borel_measurable_INF[measurable (raw)]:
2.384    fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
2.385    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
2.386    shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
2.387 @@ -1164,13 +1142,45 @@
2.388      using assms by auto
2.389  qed
2.390
2.391 -lemma [simp, intro, measurable (raw)]:
2.392 +lemma [measurable (raw)]:
2.393    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
2.394    assumes "\<And>i. f i \<in> borel_measurable M"
2.395    shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
2.396      and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
2.397    unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
2.398
2.399 +lemma sets_Collect_eventually_sequientially[measurable]:
2.400 +  "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
2.401 +  unfolding eventually_sequentially by simp
2.402 +
2.403 +lemma convergent_ereal:
2.404 +  fixes X :: "nat \<Rightarrow> ereal"
2.405 +  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
2.406 +  using ereal_Liminf_eq_Limsup_iff[of sequentially]
2.407 +  by (auto simp: convergent_def)
2.408 +
2.409 +lemma convergent_ereal_limsup:
2.410 +  fixes X :: "nat \<Rightarrow> ereal"
2.411 +  shows "convergent X \<Longrightarrow> limsup X = lim X"
2.412 +  by (auto simp: convergent_def limI lim_imp_Limsup)
2.413 +
2.414 +lemma sets_Collect_ereal_convergent[measurable]:
2.415 +  fixes f :: "nat \<Rightarrow> 'a => ereal"
2.416 +  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
2.417 +  shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
2.418 +  unfolding convergent_ereal by auto
2.419 +
2.420 +lemma borel_measurable_extreal_lim[measurable (raw)]:
2.421 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
2.422 +  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
2.423 +  shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
2.424 +proof -
2.425 +  have "\<And>x. lim (\<lambda>i. f i x) = (if convergent (\<lambda>i. f i x) then limsup (\<lambda>i. f i x) else (THE i. False))"
2.426 +    using convergent_ereal_limsup by (simp add: lim_def convergent_def)
2.427 +  then show ?thesis
2.428 +    by simp
2.429 +qed
2.430 +
2.431  lemma borel_measurable_ereal_LIMSEQ:
2.432    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
2.433    assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
2.434 @@ -1179,17 +1189,14 @@
2.435  proof -
2.436    have "\<And>x. x \<in> space M \<Longrightarrow> u' x = liminf (\<lambda>n. u n x)"
2.437      using u' by (simp add: lim_imp_Liminf[symmetric])
2.438 -  then show ?thesis by (simp add: u cong: measurable_cong)
2.439 +  with u show ?thesis by (simp cong: measurable_cong)
2.440  qed
2.441
2.442 -lemma borel_measurable_psuminf[simp, intro, measurable (raw)]:
2.443 +lemma borel_measurable_extreal_suminf[measurable (raw)]:
2.444    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
2.445 -  assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x"
2.446 +  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
2.447    shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
2.448 -  apply (subst measurable_cong)
2.449 -  apply (subst suminf_ereal_eq_SUPR)
2.450 -  apply (rule pos)
2.451 -  using assms by auto
2.452 +  unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
2.453
2.454  section "LIMSEQ is borel measurable"
2.455
```
```     3.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
3.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
3.3 @@ -56,7 +56,7 @@
3.4
3.5  lemma merge_commute:
3.6    "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)"
3.7 -  by (auto simp: merge_def intro!: ext)
3.8 +  by (force simp: merge_def)
3.9
3.10  lemma Pi_cancel_merge_range[simp]:
3.11    "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
3.12 @@ -430,7 +430,7 @@
3.13      by (auto simp add: sets_PiM intro!: sigma_sets_top)
3.14  next
3.15    assume "J \<noteq> {}" with assms show ?thesis
3.16 -    by (auto simp add: sets_PiM prod_algebra_def intro!: sigma_sets.Basic)
3.17 +    by (force simp add: sets_PiM prod_algebra_def)
3.18  qed
3.19
3.20  lemma measurable_PiM:
3.21 @@ -475,24 +475,12 @@
3.22    finally show "f -` A \<inter> space N \<in> sets N" .
3.23  qed (auto simp: space)
3.24
3.25 -lemma sets_PiM_I_finite[simp, intro]:
3.26 +lemma sets_PiM_I_finite[measurable]:
3.27    assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
3.28    shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
3.29    using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto
3.30
3.31 -lemma measurable_component_update:
3.32 -  assumes "x \<in> space (Pi\<^isub>M I M)" and "i \<notin> I"
3.33 -  shows "(\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \<in> _")
3.34 -proof (intro measurable_PiM_single)
3.35 -  fix j A assume "j \<in> insert i I" "A \<in> sets (M j)"
3.36 -  moreover have "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} =
3.37 -    (if i = j then space (M i) \<inter> A else if x j \<in> A then space (M i) else {})"
3.38 -    by auto
3.39 -  ultimately show "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} \<in> sets (M i)"
3.40 -    by auto
3.41 -qed (insert sets_into_space assms, auto simp: space_PiM)
3.42 -
3.43 -lemma measurable_component_singleton:
3.44 +lemma measurable_component_singleton[measurable (raw)]:
3.45    assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
3.46  proof (unfold measurable_def, intro CollectI conjI ballI)
3.47    fix A assume "A \<in> sets (M i)"
3.48 @@ -503,7 +491,7 @@
3.49      using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
3.50  qed (insert `i \<in> I`, auto simp: space_PiM)
3.51
3.54    "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
3.55      (is "?f \<in> measurable ?P ?I")
3.56  proof (rule measurable_PiM_single)
3.57 @@ -517,7 +505,11 @@
3.58    finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
3.59  qed (auto simp: space_pair_measure space_PiM)
3.60
3.61 -lemma measurable_merge:
3.62 +lemma measurable_component_update:
3.63 +  "x \<in> space (Pi\<^isub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)"
3.64 +  by simp
3.65 +
3.66 +lemma measurable_merge[measurable]:
3.67    "merge I J \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
3.68      (is "?f \<in> measurable ?P ?U")
3.69  proof (rule measurable_PiM_single)
3.70 @@ -531,7 +523,7 @@
3.71    finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
3.72  qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
3.73
3.74 -lemma measurable_restrict:
3.75 +lemma measurable_restrict[measurable (raw)]:
3.76    assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
3.77    shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^isub>M I M)"
3.78  proof (rule measurable_PiM_single)
3.79 @@ -542,6 +534,31 @@
3.80      using A X by (auto intro!: measurable_sets)
3.81  qed (insert X, auto dest: measurable_space)
3.82
3.83 +lemma sets_in_Pi_aux:
3.84 +  "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
3.85 +  {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
3.86 +  by (simp add: subset_eq Pi_iff)
3.87 +
3.88 +lemma sets_in_Pi[measurable (raw)]:
3.89 +  "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
3.90 +  (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
3.91 +  Sigma_Algebra.pred N (\<lambda>x. f x \<in> Pi I F)"
3.92 +  unfolding pred_def
3.93 +  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
3.94 +
3.95 +lemma sets_in_extensional_aux:
3.96 +  "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
3.97 +proof -
3.98 +  have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
3.99 +    by (auto simp add: extensional_def space_PiM)
3.100 +  then show ?thesis by simp
3.101 +qed
3.102 +
3.103 +lemma sets_in_extensional[measurable (raw)]:
3.104 +  "f \<in> measurable N (PiM I M) \<Longrightarrow> Sigma_Algebra.pred N (\<lambda>x. f x \<in> extensional I)"
3.105 +  unfolding pred_def
3.106 +  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
3.107 +
3.108  locale product_sigma_finite =
3.109    fixes M :: "'i \<Rightarrow> 'a measure"
3.110    assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
3.111 @@ -665,7 +682,7 @@
3.112    qed (auto intro!: setprod_cong)
3.113    with insert show ?case
3.114      by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
3.116 +qed simp
3.117
3.118  lemma (in product_sigma_finite) sigma_finite:
3.119    assumes "finite I"
3.120 @@ -759,18 +776,18 @@
3.121      show "emeasure ?P (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
3.122    next
3.123      fix A assume A: "A \<in> prod_algebra (I \<union> J) M"
3.124 -    with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>I \<union> J. F i \<in> sets (M i)"
3.125 +    with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>J. F i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
3.126        by (auto simp add: prod_algebra_eq_finite)
3.127      let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M"
3.128      let ?X = "?g -` A \<inter> space ?B"
3.129      have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)"
3.130 -      using F[rule_format, THEN sets_into_space] by (auto simp: space_PiM)
3.131 +      using F[rule_format, THEN sets_into_space] by (force simp: space_PiM)+
3.132      then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
3.133        unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
3.134      have "emeasure ?D A = emeasure ?B ?X"
3.135        using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
3.136      also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
3.137 -      using `finite J` `finite I` F X
3.138 +      using `finite J` `finite I` F unfolding X
3.139        by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
3.140      also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
3.141        using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
3.142 @@ -1013,8 +1030,7 @@
3.143
3.144  lemma sets_Collect_single:
3.145    "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^isub>M I M). x i \<in> A } \<in> sets (Pi\<^isub>M I M)"
3.146 -  unfolding sets_PiM_single
3.147 -  by (auto intro!: sigma_sets.Basic exI[of _ i] exI[of _ A]) (auto simp: space_PiM)
3.148 +  by simp
3.149
3.150  lemma sigma_prod_algebra_sigma_eq_infinite:
3.151    fixes E :: "'i \<Rightarrow> 'a set set"
3.152 @@ -1127,7 +1143,7 @@
3.154    show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
3.155      using `finite I`
3.156 -    by (auto intro!: sigma_sets_subset simp: E_generates P_def)
3.157 +    by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
3.158  qed
3.159
3.160  end
```
```     4.1 --- a/src/HOL/Probability/Independent_Family.thy	Fri Nov 02 14:23:40 2012 +0100
4.2 +++ b/src/HOL/Probability/Independent_Family.thy	Fri Nov 02 14:23:54 2012 +0100
4.3 @@ -1004,6 +1004,9 @@
4.4    "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
4.5    using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def)
4.6
4.7 +lemma measurable_id_prod[measurable (raw)]: "i = j \<Longrightarrow> (\<lambda>x. x) \<in> measurable (M i) (M j)"
4.8 +  by simp
4.9 +
4.10  lemma (in product_sigma_finite) distr_component:
4.11    "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
4.12  proof (intro measure_eqI[symmetric])
4.13 @@ -1015,15 +1018,10 @@
4.14    fix A assume A: "A \<in> sets ?P"
4.15    then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)"
4.16      by simp
4.17 -  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) x \<partial>M i)"
4.18 -    apply (subst product_positive_integral_singleton[symmetric])
4.19 -    apply (force intro!: measurable_restrict measurable_sets A)
4.20 -    apply (auto intro!: positive_integral_cong simp: space_PiM indicator_def simp: eq)
4.21 -    done
4.22 -  also have "\<dots> = emeasure (M i) ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i))"
4.23 -    by (force intro!: measurable_restrict measurable_sets A positive_integral_indicator)
4.24 +  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)"
4.25 +    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
4.26    also have "\<dots> = emeasure ?D A"
4.27 -    using A by (auto intro!: emeasure_distr[symmetric] measurable_restrict)
4.28 +    using A by (simp add: product_positive_integral_singleton emeasure_distr)
4.29    finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
4.30  qed simp
4.31
```
```     5.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
5.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
5.3 @@ -99,7 +99,8 @@
5.4
5.5    fix X assume "X \<in> ?J"
5.6    then obtain E where [simp]: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
5.7 -  with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)" by auto
5.8 +  with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)"
5.9 +    by simp
5.10
5.11    have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
5.12      using E by (simp add: J.measure_times)
5.13 @@ -190,7 +191,7 @@
5.14        unfolding sets_PiM
5.15      proof (safe intro!: sigma_sets_subseteq)
5.16        fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
5.17 -        by (auto intro!: generatorI' elim!: prod_algebraE)
5.18 +        by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
5.19      qed
5.20    qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
5.21  qed
5.22 @@ -242,10 +243,8 @@
5.23  qed
5.24
5.25  lemma (in product_prob_space) merge_sets:
5.26 -  assumes "J \<inter> K = {}" and A: "A \<in> sets (Pi\<^isub>M (J \<union> K) M)" and x: "x \<in> space (Pi\<^isub>M J M)"
5.27 -  shows "(\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
5.28 -  by (rule measurable_sets[OF _ A] measurable_compose[OF measurable_Pair measurable_merge]
5.29 -           measurable_const x measurable_ident)+
5.30 +  "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
5.31 +  by simp
5.32
5.33  lemma (in product_prob_space) merge_emb:
5.34    assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M J M)"
5.35 @@ -622,7 +621,7 @@
5.36      then show "emb I J (Pi\<^isub>E J X) \<in> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
5.37        by (auto simp: Pi_iff prod_emb_def dest: sets_into_space)
5.38      have "emb I J (Pi\<^isub>E J X) \<in> generator"
5.39 -      using J `I \<noteq> {}` by (intro generatorI') auto
5.40 +      using J `I \<noteq> {}` by (intro generatorI') (auto simp: Pi_iff)
5.41      then have "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))"
5.42        using \<mu> by simp
5.43      also have "\<dots> = (\<Prod> j\<in>J. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
```
```     6.1 --- a/src/HOL/Probability/Information.thy	Fri Nov 02 14:23:40 2012 +0100
6.2 +++ b/src/HOL/Probability/Information.thy	Fri Nov 02 14:23:54 2012 +0100
6.3 @@ -84,10 +84,14 @@
6.4    shows "entropy_density b M N \<in> borel_measurable M"
6.5  proof -
6.6    from borel_measurable_RN_deriv[OF ac] b_gt_1 show ?thesis
6.7 -    unfolding entropy_density_def
6.8 -    by (intro measurable_comp) auto
6.9 +    unfolding entropy_density_def by auto
6.10  qed
6.11
6.12 +lemma borel_measurable_RN_deriv_density[measurable (raw)]:
6.13 +  "f \<in> borel_measurable M \<Longrightarrow> RN_deriv M (density M f) \<in> borel_measurable M"
6.14 +  using borel_measurable_RN_deriv_density[of "\<lambda>x. max 0 (f x )" M]
6.15 +  by (simp add: density_max_0[symmetric])
6.16 +
6.17  lemma (in sigma_finite_measure) KL_density:
6.18    fixes f :: "'a \<Rightarrow> real"
6.19    assumes "1 < b"
6.20 @@ -97,7 +101,7 @@
6.21  proof (subst integral_density)
6.22    show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
6.23      using f
6.24 -    by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density)
6.25 +    by (auto simp: comp_def entropy_density_def)
6.26    have "density M (RN_deriv M (density M f)) = density M f"
6.27      using f by (intro density_RN_deriv_density) auto
6.28    then have eq: "AE x in M. RN_deriv M (density M f) x = f x"
6.29 @@ -366,7 +370,7 @@
6.30    shows "AE x in P. 0 \<le> g (T x)"
6.31    using g
6.32    apply (subst AE_distr_iff[symmetric, OF T(1)])
6.33 -  apply (simp add: distributed_borel_measurable)
6.34 +  apply simp
6.35    apply (rule absolutely_continuous_AE[OF _ T(2)])
6.36    apply simp
6.38 @@ -409,7 +413,7 @@
6.39  lemma distributed_integrable:
6.40    "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
6.41      integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
6.42 -  by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
6.43 +  by (auto simp: distributed_real_AE
6.44                      distributed_distr_eq_density[symmetric] integral_density[symmetric] integrable_distr_eq)
6.45
6.46  lemma distributed_transform_integrable:
6.47 @@ -446,7 +450,7 @@
6.48    shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))"
6.49    using assms unfolding finite_entropy_def
6.50    using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"]
6.51 -  by (auto dest!: distributed_real_measurable)
6.52 +  by auto
6.53
6.54  subsection {* Mutual Information *}
6.55
6.56 @@ -464,7 +468,7 @@
6.57        mutual_information b S T X Y = 0)"
6.58    unfolding indep_var_distribution_eq
6.59  proof safe
6.60 -  assume rv: "random_variable S X" "random_variable T Y"
6.61 +  assume rv[measurable]: "random_variable S X" "random_variable T Y"
6.62
6.63    interpret X: prob_space "distr M S X"
6.64      by (rule prob_space_distr) fact
6.65 @@ -474,7 +478,7 @@
6.66    interpret P: information_space P b unfolding P_def by default (rule b_gt_1)
6.67
6.68    interpret Q: prob_space Q unfolding Q_def
6.69 -    by (rule prob_space_distr) (simp add: comp_def measurable_pair_iff rv)
6.70 +    by (rule prob_space_distr) simp
6.71
6.72    { assume "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
6.73      then have [simp]: "Q = P"  unfolding Q_def P_def by simp
6.74 @@ -536,9 +540,9 @@
6.75      using Fxy by (auto simp: finite_entropy_def)
6.76
6.77    have X: "random_variable S X"
6.78 -    using Px by (auto simp: distributed_def finite_entropy_def)
6.79 +    using Px by auto
6.80    have Y: "random_variable T Y"
6.81 -    using Py by (auto simp: distributed_def finite_entropy_def)
6.82 +    using Py by auto
6.83    interpret S: sigma_finite_measure S by fact
6.84    interpret T: sigma_finite_measure T by fact
6.85    interpret ST: pair_sigma_finite S T ..
6.86 @@ -568,7 +572,6 @@
6.87      show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
6.88        "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
6.89        using Px Py by (auto simp: distributed_def)
6.90 -    show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
6.91      show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
6.92    qed (fact | simp)+
6.93
6.94 @@ -675,7 +678,6 @@
6.95      show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
6.96        "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
6.97        using Px Py by (auto simp: distributed_def)
6.98 -    show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
6.99      show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
6.100    qed (fact | simp)+
6.101
6.102 @@ -1009,11 +1011,11 @@
6.103
6.104  lemma (in information_space)
6.105    assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
6.106 -  assumes Px: "distributed M S X Px"
6.107 -  assumes Pz: "distributed M P Z Pz"
6.108 -  assumes Pyz: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
6.109 -  assumes Pxz: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
6.110 -  assumes Pxyz: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
6.111 +  assumes Px[measurable]: "distributed M S X Px"
6.112 +  assumes Pz[measurable]: "distributed M P Z Pz"
6.113 +  assumes Pyz[measurable]: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
6.114 +  assumes Pxz[measurable]: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
6.115 +  assumes Pxyz[measurable]: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
6.116    assumes I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
6.117    assumes I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
6.118    shows conditional_mutual_information_generic_eq: "conditional_mutual_information b S T P X Y Z
6.119 @@ -1033,56 +1035,38 @@
6.120    have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
6.121    have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
6.122      using Pyz by (simp add: distributed_measurable)
6.123 -
6.124 -  have Pxyz_f: "\<And>M f. f \<in> measurable M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. Pxyz (f x)) \<in> borel_measurable M"
6.125 -    using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
6.126 -
6.127 -  { fix f g h M
6.128 -    assume f: "f \<in> measurable M S" and g: "g \<in> measurable M P" and h: "h \<in> measurable M (S \<Otimes>\<^isub>M P)"
6.129 -    from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
6.130 -         measurable_comp[OF f Px[THEN distributed_real_measurable]]
6.131 -         measurable_comp[OF g Pz[THEN distributed_real_measurable]]
6.132 -    have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
6.133 -      by (simp add: comp_def b_gt_1) }
6.134 -  note borel_log = this
6.135 -
6.136 -  have measurable_cut: "(\<lambda>(x, y, z). (x, z)) \<in> measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (S \<Otimes>\<^isub>M P)"
6.137 -    by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
6.138
6.139    from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
6.140      distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"
6.141 -    by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
6.142 +    by (simp add: comp_def distr_distr)
6.143
6.144    have "mutual_information b S P X Z =
6.145      (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
6.146      by (rule mutual_information_distr[OF S P Px Pz Pxz])
6.147    also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
6.148      using b_gt_1 Pxz Px Pz
6.149 -    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
6.150 -       (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
6.151 -             dest!: distributed_real_measurable)
6.152 +    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"]) (auto simp: split_beta')
6.153    finally have mi_eq:
6.154      "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .
6.155
6.156    have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
6.157      by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
6.158    moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
6.159 -    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
6.160 +    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) auto
6.161    moreover have ae3: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
6.162 -    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
6.163 +    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) auto
6.164    moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
6.165 -    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
6.166 +    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) auto
6.167    moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
6.168 -    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
6.169 +    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
6.170    moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
6.171 -    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
6.172 +    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
6.173    moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
6.174 -    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: measurable_snd'' TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
6.175 +    using Pz Pz[THEN distributed_real_measurable]
6.176 +    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
6.177    moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
6.178      using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
6.179 -    using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
6.180 -    using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
6.181 -    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
6.182 +    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure)
6.183    moreover note Pxyz[THEN distributed_real_AE]
6.184    ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
6.185      Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
6.186 @@ -1110,52 +1094,36 @@
6.187    let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
6.188    interpret P: prob_space ?P
6.189      unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
6.190 -    using distributed_measurable[OF Pxyz] by (rule prob_space_distr)
6.191 +    by (rule prob_space_distr) simp
6.192
6.193    let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
6.194    interpret Q: prob_space ?Q
6.195      unfolding distributed_distr_eq_density[OF Pyz, symmetric]
6.196 -    using distributed_measurable[OF Pyz] by (rule prob_space_distr)
6.197 +    by (rule prob_space_distr) simp
6.198
6.199    let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
6.200
6.201    from subdensity_real[of snd, OF _ Pyz Pz]
6.202    have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
6.203    have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
6.204 -    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
6.205 +    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
6.206
6.207    have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
6.208      using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
6.209 -    apply (intro TP.AE_pair_measure)
6.210 -    apply (auto simp: comp_def measurable_split_conv
6.211 -                intro!: measurable_snd'' measurable_fst'' borel_measurable_ereal_eq borel_measurable_ereal
6.212 -                        S.borel_measurable_positive_integral measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
6.213 -                        measurable_Pair
6.214 -                dest: distributed_real_AE distributed_real_measurable)
6.215 -    done
6.216 +    by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
6.217
6.218 -  note M = borel_measurable_divide borel_measurable_diff borel_measurable_times borel_measurable_ereal
6.219 -           measurable_compose[OF _ measurable_snd]
6.220 -           measurable_Pair
6.221 -           measurable_compose[OF _ Pxyz[THEN distributed_real_measurable]]
6.222 -           measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
6.223 -           measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
6.224 -           measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
6.225 -           measurable_compose[OF _ Px[THEN distributed_real_measurable]]
6.226 -           TP.borel_measurable_positive_integral
6.227    have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
6.228      apply (subst positive_integral_density)
6.229 -    apply (rule distributed_borel_measurable[OF Pxyz])
6.230 +    apply simp
6.231      apply (rule distributed_AE[OF Pxyz])
6.232 -    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
6.233 +    apply auto []
6.234      apply (rule positive_integral_mono_AE)
6.235      using ae5 ae6 ae7 ae8
6.236      apply eventually_elim
6.237      apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
6.238      done
6.239    also have "\<dots> = (\<integral>\<^isup>+(y, z). \<integral>\<^isup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^isub>M P)"
6.240 -    by (subst STP.positive_integral_snd_measurable[symmetric])
6.241 -       (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M)
6.242 +    by (subst STP.positive_integral_snd_measurable[symmetric]) (auto simp add: split_beta')
6.243    also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
6.244      apply (rule positive_integral_cong_AE)
6.245      using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
6.246 @@ -1164,44 +1132,41 @@
6.247      fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
6.248        "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)"
6.249      then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
6.250 -      apply (subst positive_integral_multc)
6.251 -      apply (auto intro!: borel_measurable_ereal divide_nonneg_nonneg
6.252 -                          measurable_compose[OF _ Pxz[THEN distributed_real_measurable]] measurable_Pair
6.253 -                  split: prod.split)
6.254 -      done
6.255 +      by (subst positive_integral_multc)
6.256 +         (auto intro!: divide_nonneg_nonneg split: prod.split)
6.257    qed
6.258    also have "\<dots> = 1"
6.259      using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
6.260 -    by (subst positive_integral_density[symmetric]) (auto intro!: M)
6.261 +    by (subst positive_integral_density[symmetric]) auto
6.262    finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
6.263    also have "\<dots> < \<infinity>" by simp
6.264    finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
6.265
6.266    have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
6.267      apply (subst positive_integral_density)
6.268 -    apply (rule distributed_borel_measurable[OF Pxyz])
6.269 +    apply simp
6.270      apply (rule distributed_AE[OF Pxyz])
6.271 -    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
6.272 +    apply auto []
6.274    proof
6.275      let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
6.276      assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
6.277      then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
6.278 -      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: M borel_measurable_ereal measurable_If)
6.279 +      by (intro positive_integral_0_iff_AE[THEN iffD1]) auto
6.280      then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
6.281        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
6.282        by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
6.283      then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
6.284        by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
6.285      with P.emeasure_space_1 show False
6.286 -      by (subst (asm) emeasure_density) (auto intro!: M cong: positive_integral_cong)
6.287 +      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
6.288    qed
6.289
6.290    have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
6.291      apply (rule positive_integral_0_iff_AE[THEN iffD2])
6.292 -    apply (auto intro!: M simp: split_beta') []
6.293 +    apply simp
6.294      apply (subst AE_density)
6.295 -    apply (auto intro!: M simp: split_beta') []
6.296 +    apply simp
6.297      using ae5 ae6 ae7 ae8
6.298      apply eventually_elim
6.299      apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
6.300 @@ -1210,7 +1175,7 @@
6.301    have I3: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
6.302      apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
6.303      using ae
6.304 -    apply (auto intro!: M simp: split_beta')
6.305 +    apply (auto simp: split_beta')
6.306      done
6.307
6.308    have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
6.309 @@ -1230,15 +1195,15 @@
6.310        by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
6.311      show "integrable ?P ?f"
6.312        unfolding integrable_def
6.313 -      using fin neg by (auto intro!: M simp: split_beta')
6.314 +      using fin neg by (auto simp: split_beta')
6.315      show "integrable ?P (\<lambda>x. - log b (?f x))"
6.316        apply (subst integral_density)
6.317 -      apply (auto intro!: M) []
6.318 -      apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
6.319 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
6.320 +      apply simp
6.321 +      apply (auto intro!: distributed_real_AE[OF Pxyz]) []
6.322 +      apply simp
6.323        apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
6.324 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
6.325 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
6.326 +      apply simp
6.327 +      apply simp
6.328        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
6.329        apply eventually_elim
6.330        apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
6.331 @@ -1247,9 +1212,9 @@
6.332    also have "\<dots> = conditional_mutual_information b S T P X Y Z"
6.333      unfolding `?eq`
6.334      apply (subst integral_density)
6.335 -    apply (auto intro!: M) []
6.336 -    apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
6.337 -    apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
6.338 +    apply simp
6.339 +    apply (auto intro!: distributed_real_AE[OF Pxyz]) []
6.340 +    apply simp
6.341      apply (intro integral_cong_AE)
6.342      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
6.343      apply eventually_elim
6.344 @@ -1271,11 +1236,11 @@
6.345      = (\<integral>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" (is "?eq")
6.346      and conditional_mutual_information_generic_nonneg': "0 \<le> conditional_mutual_information b S T P X Y Z" (is "?nonneg")
6.347  proof -
6.348 -  note Px = Fx[THEN finite_entropy_distributed]
6.349 -  note Pz = Fz[THEN finite_entropy_distributed]
6.350 -  note Pyz = Fyz[THEN finite_entropy_distributed]
6.351 -  note Pxz = Fxz[THEN finite_entropy_distributed]
6.352 -  note Pxyz = Fxyz[THEN finite_entropy_distributed]
6.353 +  note Px = Fx[THEN finite_entropy_distributed, measurable]
6.354 +  note Pz = Fz[THEN finite_entropy_distributed, measurable]
6.355 +  note Pyz = Fyz[THEN finite_entropy_distributed, measurable]
6.356 +  note Pxz = Fxz[THEN finite_entropy_distributed, measurable]
6.357 +  note Pxyz = Fxyz[THEN finite_entropy_distributed, measurable]
6.358
6.359    interpret S: sigma_finite_measure S by fact
6.360    interpret T: sigma_finite_measure T by fact
6.361 @@ -1288,27 +1253,10 @@
6.362    interpret TPS: pair_sigma_finite "T \<Otimes>\<^isub>M P" S ..
6.363    have TP: "sigma_finite_measure (T \<Otimes>\<^isub>M P)" ..
6.364    have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
6.365 -  have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
6.366 -    using Pyz by (simp add: distributed_measurable)
6.367
6.368 -  have Pxyz_f: "\<And>M f. f \<in> measurable M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. Pxyz (f x)) \<in> borel_measurable M"
6.369 -    using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
6.370 -
6.371 -  { fix f g h M
6.372 -    assume f: "f \<in> measurable M S" and g: "g \<in> measurable M P" and h: "h \<in> measurable M (S \<Otimes>\<^isub>M P)"
6.373 -    from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
6.374 -         measurable_comp[OF f Px[THEN distributed_real_measurable]]
6.375 -         measurable_comp[OF g Pz[THEN distributed_real_measurable]]
6.376 -    have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
6.377 -      by (simp add: comp_def b_gt_1) }
6.378 -  note borel_log = this
6.379 -
6.380 -  have measurable_cut: "(\<lambda>(x, y, z). (x, z)) \<in> measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (S \<Otimes>\<^isub>M P)"
6.381 -    by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
6.382 -
6.383    from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
6.384      distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"
6.385 -    by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
6.386 +    by (simp add: distr_distr comp_def)
6.387
6.388    have "mutual_information b S P X Z =
6.389      (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
6.390 @@ -1316,29 +1264,26 @@
6.391    also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
6.392      using b_gt_1 Pxz Px Pz
6.393      by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
6.394 -       (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
6.395 -             dest!: distributed_real_measurable)
6.396 +       (auto simp: split_beta')
6.397    finally have mi_eq:
6.398      "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .
6.399
6.400    have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
6.401      by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
6.402    moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
6.403 -    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
6.404 +    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) auto
6.405    moreover have ae3: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
6.406 -    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
6.407 +    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) auto
6.408    moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
6.409 -    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
6.410 +    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) auto
6.411    moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
6.412 -    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
6.413 +    using Px by (intro STP.AE_pair_measure) (auto dest: distributed_real_AE)
6.414    moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
6.415 -    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
6.416 +    using Pyz by (intro STP.AE_pair_measure) (auto dest: distributed_real_AE)
6.417    moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
6.418 -    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: measurable_snd'' TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
6.419 +    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
6.420    moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
6.421      using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
6.422 -    using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
6.423 -    using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
6.424      by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
6.425    moreover note ae9 = Pxyz[THEN distributed_real_AE]
6.426    ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
6.427 @@ -1364,8 +1309,7 @@
6.428      using finite_entropy_integrable_transform[OF Fyz Pxyz, of snd]
6.429      by simp
6.430    moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z)))) \<in> borel_measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)"
6.431 -    using Pxyz Px Pyz
6.432 -    by (auto intro!: borel_measurable_times measurable_fst'' measurable_snd'' dest!: distributed_real_measurable simp: split_beta')
6.433 +    using Pxyz Px Pyz by simp
6.434    ultimately have I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
6.435      apply (rule integrable_cong_AE_imp)
6.436      using ae1 ae4 ae5 ae6 ae9
6.437 @@ -1377,12 +1321,10 @@
6.438      using finite_entropy_integrable_transform[OF Fxz Pxyz, of "\<lambda>x. (fst x, snd (snd x))"]
6.439      using finite_entropy_integrable_transform[OF Fx Pxyz, of fst]
6.440      using finite_entropy_integrable_transform[OF Fz Pxyz, of "snd \<circ> snd"]
6.441 -    by (simp add: measurable_Pair measurable_snd'' comp_def)
6.442 +    by simp
6.443    moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z))) \<in> borel_measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)"
6.444      using Pxyz Px Pz
6.445 -    by (auto intro!: measurable_compose[OF _ distributed_real_measurable[OF Pxz]]
6.446 -                     measurable_Pair borel_measurable_times measurable_fst'' measurable_snd''
6.447 -             dest!: distributed_real_measurable simp: split_beta')
6.448 +    by auto
6.449    ultimately have I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
6.450      apply (rule integrable_cong_AE_imp)
6.451      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 ae9
6.452 @@ -1399,45 +1341,27 @@
6.453
6.454    let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
6.455    interpret P: prob_space ?P
6.456 -    unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
6.457 -    using distributed_measurable[OF Pxyz] by (rule prob_space_distr)
6.458 +    unfolding distributed_distr_eq_density[OF Pxyz, symmetric] by (rule prob_space_distr) simp
6.459
6.460    let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
6.461    interpret Q: prob_space ?Q
6.462 -    unfolding distributed_distr_eq_density[OF Pyz, symmetric]
6.463 -    using distributed_measurable[OF Pyz] by (rule prob_space_distr)
6.464 +    unfolding distributed_distr_eq_density[OF Pyz, symmetric] by (rule prob_space_distr) simp
6.465
6.466    let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
6.467
6.468    from subdensity_real[of snd, OF _ Pyz Pz]
6.469    have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
6.470    have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
6.471 -    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
6.472 +    using Pz by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
6.473
6.474    have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
6.475      using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
6.476 -    apply (intro TP.AE_pair_measure)
6.477 -    apply (auto simp: comp_def measurable_split_conv
6.478 -                intro!: measurable_snd'' measurable_fst'' borel_measurable_ereal_eq borel_measurable_ereal
6.479 -                        S.borel_measurable_positive_integral measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
6.480 -                        measurable_Pair
6.481 -                dest: distributed_real_AE distributed_real_measurable)
6.482 -    done
6.483 -
6.484 -  note M = borel_measurable_divide borel_measurable_diff borel_measurable_times borel_measurable_ereal
6.485 -           measurable_compose[OF _ measurable_snd]
6.486 -           measurable_Pair
6.487 -           measurable_compose[OF _ Pxyz[THEN distributed_real_measurable]]
6.488 -           measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
6.489 -           measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
6.490 -           measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
6.491 -           measurable_compose[OF _ Px[THEN distributed_real_measurable]]
6.492 -           TP.borel_measurable_positive_integral
6.493 +    by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
6.494    have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
6.495      apply (subst positive_integral_density)
6.496      apply (rule distributed_borel_measurable[OF Pxyz])
6.497      apply (rule distributed_AE[OF Pxyz])
6.498 -    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
6.499 +    apply simp
6.500      apply (rule positive_integral_mono_AE)
6.501      using ae5 ae6 ae7 ae8
6.502      apply eventually_elim
6.503 @@ -1445,7 +1369,7 @@
6.504      done
6.505    also have "\<dots> = (\<integral>\<^isup>+(y, z). \<integral>\<^isup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^isub>M P)"
6.506      by (subst STP.positive_integral_snd_measurable[symmetric])
6.507 -       (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M)
6.508 +       (auto simp add: split_beta')
6.509    also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
6.510      apply (rule positive_integral_cong_AE)
6.511      using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
6.512 @@ -1454,44 +1378,40 @@
6.513      fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
6.514        "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)"
6.515      then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
6.516 -      apply (subst positive_integral_multc)
6.517 -      apply (auto intro!: borel_measurable_ereal divide_nonneg_nonneg
6.518 -                          measurable_compose[OF _ Pxz[THEN distributed_real_measurable]] measurable_Pair
6.519 -                  split: prod.split)
6.520 -      done
6.521 +      by (subst positive_integral_multc) (auto intro!: divide_nonneg_nonneg)
6.522    qed
6.523    also have "\<dots> = 1"
6.524      using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
6.525 -    by (subst positive_integral_density[symmetric]) (auto intro!: M)
6.526 +    by (subst positive_integral_density[symmetric]) auto
6.527    finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
6.528    also have "\<dots> < \<infinity>" by simp
6.529    finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
6.530
6.531    have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
6.532      apply (subst positive_integral_density)
6.533 -    apply (rule distributed_borel_measurable[OF Pxyz])
6.534 +    apply simp
6.535      apply (rule distributed_AE[OF Pxyz])
6.536 -    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
6.537 +    apply simp
6.539    proof
6.540      let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
6.541      assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
6.542      then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
6.543 -      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: M borel_measurable_ereal measurable_If)
6.544 +      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
6.545      then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
6.546        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
6.547        by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
6.548      then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
6.549        by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
6.550      with P.emeasure_space_1 show False
6.551 -      by (subst (asm) emeasure_density) (auto intro!: M cong: positive_integral_cong)
6.552 +      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
6.553    qed
6.554
6.555    have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
6.556      apply (rule positive_integral_0_iff_AE[THEN iffD2])
6.557 -    apply (auto intro!: M simp: split_beta') []
6.558 +    apply (auto simp: split_beta') []
6.559      apply (subst AE_density)
6.560 -    apply (auto intro!: M simp: split_beta') []
6.561 +    apply (auto simp: split_beta') []
6.562      using ae5 ae6 ae7 ae8
6.563      apply eventually_elim
6.564      apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
6.565 @@ -1500,7 +1420,7 @@
6.566    have I3: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
6.567      apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
6.568      using ae
6.569 -    apply (auto intro!: M simp: split_beta')
6.570 +    apply (auto simp: split_beta')
6.571      done
6.572
6.573    have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
6.574 @@ -1520,15 +1440,15 @@
6.575        by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
6.576      show "integrable ?P ?f"
6.577        unfolding integrable_def
6.578 -      using fin neg by (auto intro!: M simp: split_beta')
6.579 +      using fin neg by (auto simp: split_beta')
6.580      show "integrable ?P (\<lambda>x. - log b (?f x))"
6.581        apply (subst integral_density)
6.582 -      apply (auto intro!: M) []
6.583 -      apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
6.584 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
6.585 +      apply simp
6.586 +      apply (auto intro!: distributed_real_AE[OF Pxyz]) []
6.587 +      apply simp
6.588        apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
6.589 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
6.590 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
6.591 +      apply simp
6.592 +      apply simp
6.593        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
6.594        apply eventually_elim
6.595        apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
6.596 @@ -1537,9 +1457,9 @@
6.597    also have "\<dots> = conditional_mutual_information b S T P X Y Z"
6.598      unfolding `?eq`
6.599      apply (subst integral_density)
6.600 -    apply (auto intro!: M) []
6.601 -    apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
6.602 -    apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
6.603 +    apply simp
6.604 +    apply (auto intro!: distributed_real_AE[OF Pxyz]) []
6.605 +    apply simp
6.606      apply (intro integral_cong_AE)
6.607      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
6.608      apply eventually_elim
6.609 @@ -1633,8 +1553,8 @@
6.610  lemma (in information_space) conditional_entropy_generic_eq:
6.611    fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
6.612    assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
6.613 -  assumes Py: "distributed M T Y Py"
6.614 -  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
6.615 +  assumes Py[measurable]: "distributed M T Y Py"
6.616 +  assumes Pxy[measurable]: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
6.617    shows "conditional_entropy b S T X Y = - (\<integral>(x, y). Pxy (x, y) * log b (Pxy (x, y) / Py y) \<partial>(S \<Otimes>\<^isub>M T))"
6.618  proof -
6.619    interpret S: sigma_finite_measure S by fact
```
```     7.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:23:40 2012 +0100
7.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:23:54 2012 +0100
7.3 @@ -121,7 +121,7 @@
7.4    shows "simple_function M f \<longleftrightarrow> simple_function N f"
7.5    unfolding simple_function_def assms ..
7.6
7.7 -lemma borel_measurable_simple_function:
7.8 +lemma borel_measurable_simple_function[measurable_dest]:
7.9    assumes "simple_function M f"
7.10    shows "f \<in> borel_measurable M"
7.11  proof (rule borel_measurableI)
7.12 @@ -918,7 +918,7 @@
7.13    hence "a \<noteq> 0" by auto
7.14    let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}"
7.15    have B: "\<And>i. ?B i \<in> sets M"
7.16 -    using f `simple_function M u` by (auto simp: borel_measurable_simple_function)
7.17 +    using f `simple_function M u` by auto
7.18
7.19    let ?uB = "\<lambda>i x. u x * indicator (?B i) x"
7.20
7.21 @@ -1436,6 +1436,10 @@
7.22    "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and>
7.23      (\<integral>\<^isup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity> \<and> (\<integral>\<^isup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
7.24
7.25 +lemma borel_measurable_integrable[measurable_dest]:
7.26 +  "integrable M f \<Longrightarrow> f \<in> borel_measurable M"
7.27 +  by (auto simp: integrable_def)
7.28 +
7.29  lemma integrableD[dest]:
7.30    assumes "integrable M f"
7.31    shows "f \<in> borel_measurable M" "(\<integral>\<^isup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^isup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
7.32 @@ -1776,7 +1780,7 @@
7.33  qed
7.34
7.35  lemma integrable_abs:
7.36 -  assumes f: "integrable M f"
7.37 +  assumes f[measurable]: "integrable M f"
7.38    shows "integrable M (\<lambda> x. \<bar>f x\<bar>)"
7.39  proof -
7.40    from assms have *: "(\<integral>\<^isup>+x. ereal (- \<bar>f x\<bar>)\<partial>M) = 0"
7.41 @@ -1871,7 +1875,7 @@
7.42      from mono pos show "AE x in M. ereal (f i x) \<le> ereal (f (Suc i) x) \<and> 0 \<le> ereal (f i x)"
7.43        by eventually_elim (auto simp: mono_def)
7.44      show "(\<lambda>x. ereal (f i x)) \<in> borel_measurable M"
7.45 -      using i by (auto simp: integrable_def)
7.46 +      using i by auto
7.47    next
7.48      show "(\<integral>\<^isup>+ x. ereal (u x) \<partial>M) = \<integral>\<^isup>+ x. (SUP i. ereal (f i x)) \<partial>M"
7.49        apply (rule positive_integral_cong_AE)
7.50 @@ -2045,10 +2049,10 @@
7.51    using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
7.52
7.53  lemma integral_dominated_convergence:
7.54 -  assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>j. AE x in M. \<bar>u j x\<bar> \<le> w x"
7.55 -  and w: "integrable M w"
7.56 +  assumes u[measurable]: "\<And>i. integrable M (u i)" and bound: "\<And>j. AE x in M. \<bar>u j x\<bar> \<le> w x"
7.57 +  and w[measurable]: "integrable M w"
7.58    and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
7.59 -  and borel: "u' \<in> borel_measurable M"
7.60 +  and [measurable]: "u' \<in> borel_measurable M"
7.61    shows "integrable M u'"
7.62    and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar> \<partial>M)) ----> 0" (is "?lim_diff")
7.63    and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim)
7.64 @@ -2120,7 +2124,7 @@
7.65        qed (rule trivial_limit_sequentially)
7.66      qed
7.67      also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^isup>+ x. max 0 (ereal (?diff n x)) \<partial>M)"
7.68 -      using borel w u unfolding integrable_def
7.69 +      using w u unfolding integrable_def
7.70        by (intro positive_integral_lim_INF) (auto intro!: positive_integral_lim_INF)
7.71      also have "\<dots> = (\<integral>\<^isup>+ x. ereal (2 * w x) \<partial>M) -
7.72          limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
7.73 @@ -2171,7 +2175,7 @@
7.74  qed
7.75
7.76  lemma integral_sums:
7.77 -  assumes borel: "\<And>i. integrable M (f i)"
7.78 +  assumes integrable[measurable]: "\<And>i. integrable M (f i)"
7.79    and summable: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>f i x\<bar>)"
7.80    and sums: "summable (\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
7.81    shows "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
7.82 @@ -2182,7 +2186,7 @@
7.83    from bchoice[OF this]
7.84    obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto
7.85    then have w_borel: "w \<in> borel_measurable M" unfolding sums_def
7.86 -    by (rule borel_measurable_LIMSEQ) (auto simp: borel[THEN integrableD(1)])
7.87 +    by (rule borel_measurable_LIMSEQ) auto
7.88
7.89    let ?w = "\<lambda>y. if y \<in> space M then w y else 0"
7.90
7.91 @@ -2190,7 +2194,7 @@
7.92      using sums unfolding summable_def ..
7.93
7.94    have 1: "\<And>n. integrable M (\<lambda>x. \<Sum>i = 0..<n. f i x)"
7.95 -    using borel by auto
7.96 +    using integrable by auto
7.97
7.98    have 2: "\<And>j. AE x in M. \<bar>\<Sum>i = 0..<j. f i x\<bar> \<le> ?w x"
7.99      using AE_space
7.100 @@ -2206,14 +2210,14 @@
7.101      let ?F = "\<lambda>n y. (\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
7.102      let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
7.103      have "\<And>n. integrable M (?F n)"
7.104 -      using borel by (auto intro!: integrable_abs)
7.105 +      using integrable by (auto intro!: integrable_abs)
7.106      thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
7.107      show "AE x in M. mono (\<lambda>n. ?w' n x)"
7.108        by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
7.109      show "AE x in M. (\<lambda>n. ?w' n x) ----> ?w x"
7.110          using w by (simp_all add: tendsto_const sums_def)
7.111      have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
7.112 -      using borel by (simp add: integrable_abs cong: integral_cong)
7.113 +      using integrable by (simp add: integrable_abs cong: integral_cong)
7.114      from abs_sum
7.115      show "(\<lambda>i. integral\<^isup>L M (?w' i)) ----> x" unfolding * sums_def .
7.116    qed (simp add: w_borel measurable_If_set)
7.117 @@ -2223,11 +2227,11 @@
7.118      by (auto intro: summable_sumr_LIMSEQ_suminf)
7.119
7.120    note int = integral_dominated_convergence(1,3)[OF 1 2 3 4
7.121 -    borel_measurable_suminf[OF integrableD(1)[OF borel]]]
7.122 +    borel_measurable_suminf[OF integrableD(1)[OF integrable]]]
7.123
7.124    from int show "integrable M ?S" by simp
7.125
7.126 -  show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF borel]
7.127 +  show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF integrable]
7.128      using int(2) by simp
7.129  qed
7.130
7.131 @@ -2317,13 +2321,9 @@
7.132                     positive_integral_monotone_convergence_SUP le_fun_def incseq_def)
7.133
7.134  lemma positive_integral_distr:
7.135 -  assumes T: "T \<in> measurable M M'"
7.136 -  and f: "f \<in> borel_measurable M'"
7.137 -  shows "integral\<^isup>P (distr M M' T) f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
7.138 -  apply (subst (1 2) positive_integral_max_0[symmetric])
7.139 -  apply (rule positive_integral_distr')
7.140 -  apply (auto simp: f T)
7.141 -  done
7.142 +  "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^isup>P (distr M M' T) f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
7.143 +  by (subst (1 2) positive_integral_max_0[symmetric])
7.145
7.146  lemma integral_distr:
7.147    "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^isup>L (distr M M' T) f = (\<integral> x. f (T x) \<partial>M)"
7.148 @@ -2331,15 +2331,13 @@
7.149    by (subst (1 2) positive_integral_distr) auto
7.150
7.151  lemma integrable_distr_eq:
7.152 -  assumes T: "T \<in> measurable M M'" "f \<in> borel_measurable M'"
7.153 -  shows "integrable (distr M M' T) f \<longleftrightarrow> integrable M (\<lambda>x. f (T x))"
7.154 -  using T measurable_comp[OF T]
7.155 +  "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integrable (distr M M' T) f \<longleftrightarrow> integrable M (\<lambda>x. f (T x))"
7.156    unfolding integrable_def
7.157    by (subst (1 2) positive_integral_distr) (auto simp: comp_def)
7.158
7.159  lemma integrable_distr:
7.160 -  assumes T: "T \<in> measurable M M'" shows "integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
7.161 -  by (subst integrable_distr_eq[symmetric, OF T]) auto
7.162 +  "T \<in> measurable M M' \<Longrightarrow> integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
7.163 +  by (subst integrable_distr_eq[symmetric]) auto
7.164
7.165  section {* Lebesgue integration on @{const count_space} *}
7.166
7.167 @@ -2414,6 +2412,10 @@
7.168      and space_density[simp]: "space (density M f) = space M"
7.169    by (auto simp: density_def)
7.170
7.171 +(* FIXME: add conversion to simplify space, sets and measurable *)
7.172 +lemma space_density_imp[measurable_dest]:
7.173 +  "\<And>x M f. x \<in> space (density M f) \<Longrightarrow> x \<in> space M" by auto
7.174 +
7.175  lemma
7.176    shows measurable_density_eq1[simp]: "g \<in> measurable (density Mg f) Mg' \<longleftrightarrow> g \<in> measurable Mg Mg'"
7.177      and measurable_density_eq2[simp]: "h \<in> measurable Mh (density Mh' f) \<longleftrightarrow> h \<in> measurable Mh Mh'"
7.178 @@ -2533,7 +2535,7 @@
7.179    case (mult u c)
7.180    moreover have "\<And>x. f x * (c * u x) = c * (f x * u x)" by (simp add: field_simps)
7.181    ultimately show ?case
7.182 -    by (simp add: f positive_integral_cmult)
7.183 +    using f by (simp add: positive_integral_cmult)
7.184  next
7.186    moreover then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
```
```     8.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
8.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
8.3 @@ -695,66 +695,6 @@
8.4    qed
8.5  qed
8.6
8.7 -lemma borel_measurable_real_induct[consumes 2, case_names cong set mult add seq, induct set: borel_measurable]:
8.8 -  fixes u :: "'a \<Rightarrow> real"
8.9 -  assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"
8.10 -  assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f"
8.11 -  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
8.12 -  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
8.13 -  assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
8.14 -  assumes seq: "\<And>U u. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. 0 \<le> U i x) \<Longrightarrow> (\<And>x. (\<lambda>i. U i x) ----> u x) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> P u"
8.15 -  shows "P u"
8.16 -proof -
8.17 -  have "(\<lambda>x. ereal (u x)) \<in> borel_measurable M"
8.18 -    using u by auto
8.19 -  then obtain U where U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and
8.20 -    "\<And>x. (SUP i. U i x) = max 0 (ereal (u x))" and nn: "\<And>i x. 0 \<le> U i x"
8.21 -    using borel_measurable_implies_simple_function_sequence'[of u M] by auto
8.22 -  then have u_eq: "\<And>x. ereal (u x) = (SUP i. U i x)"
8.23 -    using u by (auto simp: max_def)
8.24 -
8.25 -  have [simp]: "\<And>i x. U i x \<noteq> \<infinity>" using U by (auto simp: image_def eq_commute)
8.26 -
8.27 -  { fix i x have [simp]: "U i x \<noteq> -\<infinity>" using nn[of i x] by auto }
8.28 -  note this[simp]
8.29 -
8.30 -  show "P u"
8.31 -  proof (rule seq)
8.32 -    show "\<And>i. (\<lambda>x. real (U i x)) \<in> borel_measurable M"
8.33 -      using U by (auto intro: borel_measurable_simple_function)
8.34 -    show "\<And>i x. 0 \<le> real (U i x)"
8.35 -      using nn by (auto simp: real_of_ereal_pos)
8.36 -    show "incseq (\<lambda>i x. real (U i x))"
8.37 -      using U(2) by (auto simp: incseq_def image_iff le_fun_def intro!: real_of_ereal_positive_mono nn)
8.38 -    then show "\<And>x. (\<lambda>i. real (U i x)) ----> u x"
8.39 -      by (intro SUP_eq_LIMSEQ[THEN iffD1])
8.40 -         (auto simp: incseq_mono incseq_def le_fun_def u_eq ereal_real
8.41 -               intro!: arg_cong2[where f=SUPR] ext)
8.42 -    show "\<And>i. P (\<lambda>x. real (U i x))"
8.43 -    proof (rule cong)
8.44 -      fix x i assume x: "x \<in> space M"
8.45 -      have [simp]: "\<And>A x. real (indicator A x :: ereal) = indicator A x"
8.46 -        by (auto simp: indicator_def one_ereal_def)
8.47 -      { fix y assume "y \<in> U i ` space M"
8.48 -        then have "0 \<le> y" "y \<noteq> \<infinity>" using nn by auto
8.49 -        then have "\<bar>y * indicator (U i -` {y} \<inter> space M) x\<bar> \<noteq> \<infinity>"
8.50 -          by (auto simp: indicator_def) }
8.51 -      then show "real (U i x) = (\<Sum>y \<in> U i ` space M. real y * indicator (U i -` {y} \<inter> space M) x)"
8.52 -        unfolding simple_function_indicator_representation[OF U(1) x]
8.53 -        by (subst setsum_real_of_ereal[symmetric]) auto
8.54 -    next
8.55 -      fix i
8.56 -      have "finite (U i ` space M)" "\<And>x. x \<in> U i ` space M \<Longrightarrow> 0 \<le> x""\<And>x. x \<in> U i ` space M \<Longrightarrow> x \<noteq> \<infinity>"
8.57 -        using U(1) nn by (auto simp: simple_function_def)
8.58 -      then show "P (\<lambda>x. \<Sum>y \<in> U i ` space M. real y * indicator (U i -` {y} \<inter> space M) x)"
8.59 -      proof induct
8.60 -        case empty then show ?case
8.61 -          using set[of "{}"] by (simp add: indicator_def[abs_def])
8.62 -      qed (auto intro!: add mult set simple_functionD U setsum_nonneg borel_measurable_setsum mult_nonneg_nonneg real_of_ereal_pos)
8.63 -    qed (auto intro: borel_measurable_simple_function U simple_functionD intro!: borel_measurable_setsum borel_measurable_times)
8.64 -  qed
8.65 -qed
8.66 -
8.67  lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
8.68    by (auto simp: indicator_def one_ereal_def)
8.69
8.70 @@ -1054,7 +994,7 @@
8.71      by (intro arg_cong2[where f=sigma_sets]) (auto simp: space_PiM image_iff bchoice_iff)
8.72  qed (auto simp: borel_eq_lessThan reals_Archimedean2)
8.73
8.74 -lemma measurable_e2p:
8.75 +lemma measurable_e2p[measurable]:
8.76    "e2p \<in> measurable (borel::'a::ordered_euclidean_space measure) (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))"
8.77  proof (rule measurable_sigma_sets[OF sets_product_borel])
8.78    fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i} |x. True} "
8.79 @@ -1065,7 +1005,11 @@
8.80    then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
8.81  qed (auto simp: e2p_def)
8.82
8.83 -lemma measurable_p2e:
8.84 +(* FIXME: conversion in measurable prover *)
8.85 +lemma lborelD_Collect[measurable]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
8.86 +lemma lborelD[measurable]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
8.87 +
8.88 +lemma measurable_p2e[measurable]:
8.89    "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))
8.90      (borel :: 'a::ordered_euclidean_space measure)"
8.91    (is "p2e \<in> measurable ?P _")
```
```     9.1 --- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
9.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
9.3 @@ -522,23 +522,50 @@
9.4    f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N"
9.5
9.6  lemma
9.7 -  shows distributed_distr_eq_density: "distributed M N X f \<Longrightarrow> distr M N X = density N f"
9.8 -    and distributed_measurable: "distributed M N X f \<Longrightarrow> X \<in> measurable M N"
9.9 -    and distributed_borel_measurable: "distributed M N X f \<Longrightarrow> f \<in> borel_measurable N"
9.10 -    and distributed_AE: "distributed M N X f \<Longrightarrow> (AE x in N. 0 \<le> f x)"
9.11 -  by (simp_all add: distributed_def)
9.12 +  assumes "distributed M N X f"
9.13 +  shows distributed_distr_eq_density: "distr M N X = density N f"
9.14 +    and distributed_measurable: "X \<in> measurable M N"
9.15 +    and distributed_borel_measurable: "f \<in> borel_measurable N"
9.16 +    and distributed_AE: "(AE x in N. 0 \<le> f x)"
9.17 +  using assms by (simp_all add: distributed_def)
9.18 +
9.19 +lemma
9.20 +  assumes D: "distributed M N X f"
9.21 +  shows distributed_measurable'[measurable_dest]:
9.22 +      "g \<in> measurable L M \<Longrightarrow> (\<lambda>x. X (g x)) \<in> measurable L N"
9.23 +    and distributed_borel_measurable'[measurable_dest]:
9.24 +      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
9.25 +  using distributed_measurable[OF D] distributed_borel_measurable[OF D]
9.26 +  by simp_all
9.27
9.28  lemma
9.29    shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N"
9.30      and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)"
9.31    by (simp_all add: distributed_def borel_measurable_ereal_iff)
9.32
9.33 +lemma
9.34 +  assumes D: "distributed M N X (\<lambda>x. ereal (f x))"
9.35 +  shows distributed_real_measurable'[measurable_dest]:
9.36 +      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
9.37 +  using distributed_real_measurable[OF D]
9.38 +  by simp_all
9.39 +
9.40 +lemma
9.41 +  assumes D: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
9.42 +  shows joint_distributed_measurable1[measurable_dest]:
9.43 +      "h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S"
9.44 +    and joint_distributed_measurable2[measurable_dest]:
9.45 +      "h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T"
9.46 +  using measurable_compose[OF distributed_measurable[OF D] measurable_fst]
9.47 +  using measurable_compose[OF distributed_measurable[OF D] measurable_snd]
9.48 +  by auto
9.49 +
9.50  lemma distributed_count_space:
9.51    assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A"
9.52    shows "P a = emeasure M (X -` {a} \<inter> space M)"
9.53  proof -
9.54    have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}"
9.55 -    using X a A by (simp add: distributed_measurable emeasure_distr)
9.56 +    using X a A by (simp add: emeasure_distr)
9.57    also have "\<dots> = emeasure (density (count_space A) P) {a}"
9.58      using X by (simp add: distributed_distr_eq_density)
9.59    also have "\<dots> = (\<integral>\<^isup>+x. P a * indicator {a} x \<partial>count_space A)"
9.60 @@ -583,17 +610,17 @@
9.61
9.62  lemma distributed_emeasure:
9.63    "distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>N)"
9.64 -  by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable
9.65 +  by (auto simp: distributed_AE
9.66                   distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
9.67
9.68  lemma distributed_positive_integral:
9.69    "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^isup>+x. f x * g x \<partial>N) = (\<integral>\<^isup>+x. g (X x) \<partial>M)"
9.70 -  by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable
9.71 +  by (auto simp: distributed_AE
9.72                   distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr)
9.73
9.74  lemma distributed_integral:
9.75    "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)"
9.76 -  by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
9.77 +  by (auto simp: distributed_real_AE
9.78                   distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr)
9.79
9.80  lemma distributed_transform_integral:
9.81 @@ -617,7 +644,7 @@
9.82    shows "AE x in S. Px x = Py x"
9.83  proof -
9.84    interpret X: prob_space "distr M S X"
9.85 -    using distributed_measurable[OF Px] by (rule prob_space_distr)
9.86 +    using Px by (intro prob_space_distr) simp
9.87    have "sigma_finite_measure (distr M S X)" ..
9.88    with sigma_finite_density_unique[of Px S Py ] Px Py
9.89    show ?thesis
9.90 @@ -626,8 +653,8 @@
9.91
9.92  lemma (in prob_space) distributed_jointI:
9.93    assumes "sigma_finite_measure S" "sigma_finite_measure T"
9.94 -  assumes X[simp]: "X \<in> measurable M S" and Y[simp]: "Y \<in> measurable M T"
9.95 -  assumes f[simp]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
9.96 +  assumes X[measurable]: "X \<in> measurable M S" and Y[measurable]: "Y \<in> measurable M T"
9.97 +  assumes [measurable]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" and f: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
9.98    assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow>
9.99      emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)"
9.100    shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
9.101 @@ -655,18 +682,18 @@
9.102        using F by (auto simp: space_pair_measure)
9.103    next
9.104      fix E assume "E \<in> ?E"
9.105 -    then obtain A B where E[simp]: "E = A \<times> B" and A[simp]: "A \<in> sets S" and B[simp]: "B \<in> sets T" by auto
9.106 +    then obtain A B where E[simp]: "E = A \<times> B"
9.107 +      and A[measurable]: "A \<in> sets S" and B[measurable]: "B \<in> sets T" by auto
9.108      have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
9.109        by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
9.110      also have "\<dots> = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
9.111 -      by (auto simp add: eq measurable_Pair measurable_compose[OF _ f(1)] positive_integral_multc
9.112 -               intro!: positive_integral_cong)
9.113 +      using f by (auto simp add: eq positive_integral_multc intro!: positive_integral_cong)
9.114      also have "\<dots> = emeasure ?R E"
9.115        by (auto simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric]
9.116                 intro!: positive_integral_cong split: split_indicator)
9.117      finally show "emeasure ?L E = emeasure ?R E" .
9.118    qed
9.119 -qed (auto intro!: measurable_Pair)
9.120 +qed (auto simp: f)
9.121
9.122  lemma (in prob_space) distributed_swap:
9.123    assumes "sigma_finite_measure S" "sigma_finite_measure T"
9.124 @@ -678,14 +705,14 @@
9.125    interpret ST: pair_sigma_finite S T by default
9.126    interpret TS: pair_sigma_finite T S by default
9.127
9.128 -  note measurable_Pxy = measurable_compose[OF _ distributed_borel_measurable[OF Pxy]]
9.129 +  note Pxy[measurable]
9.130    show ?thesis
9.131      apply (subst TS.distr_pair_swap)
9.132      unfolding distributed_def
9.133    proof safe
9.134      let ?D = "distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))"
9.135      show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D"
9.136 -      by (auto simp: measurable_split_conv intro!: measurable_Pair measurable_Pxy)
9.137 +      by auto
9.138      with Pxy
9.139      show "AE x in distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x)). 0 \<le> (case x of (x, y) \<Rightarrow> Pxy (y, x))"
9.140        by (subst AE_distr_iff)
9.141 @@ -693,9 +720,7 @@
9.142                 simp: measurable_split_conv split_beta
9.143                 intro!: measurable_Pair borel_measurable_ereal_le)
9.144      show 2: "random_variable (distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))"
9.145 -      using measurable_compose[OF distributed_measurable[OF Pxy] measurable_fst]
9.146 -      using measurable_compose[OF distributed_measurable[OF Pxy] measurable_snd]
9.147 -      by (auto intro!: measurable_Pair)
9.148 +      using Pxy by auto
9.149      { fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)"
9.150        let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^isub>M T)"
9.151        from sets_into_space[OF A]
9.152 @@ -703,7 +728,7 @@
9.153          emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
9.154          by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
9.155        also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^isub>M T))"
9.156 -        using Pxy A by (intro distributed_emeasure measurable_sets) (auto simp: measurable_split_conv measurable_Pair)
9.157 +        using Pxy A by (intro distributed_emeasure) auto
9.158        finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
9.159          (\<integral>\<^isup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^isub>M T))"
9.160          by (auto intro!: positive_integral_cong split: split_indicator) }
9.161 @@ -712,7 +737,7 @@
9.162        apply (intro measure_eqI)
9.163        apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
9.164        apply (subst positive_integral_distr)
9.165 -      apply (auto intro!: measurable_pair measurable_Pxy * simp: comp_def split_beta)
9.166 +      apply (auto intro!: * simp: comp_def split_beta)
9.167        done
9.168    qed
9.169  qed
9.170 @@ -728,33 +753,29 @@
9.171    interpret T: sigma_finite_measure T by fact
9.172    interpret ST: pair_sigma_finite S T by default
9.173
9.174 -  have XY: "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
9.175 -    using Pxy by (rule distributed_measurable)
9.176 -  then show X: "X \<in> measurable M S"
9.177 -    unfolding measurable_pair_iff by (simp add: comp_def)
9.178 -  from XY have Y: "Y \<in> measurable M T"
9.179 -    unfolding measurable_pair_iff by (simp add: comp_def)
9.180 +  note Pxy[measurable]
9.181 +  show X: "X \<in> measurable M S" by simp
9.182
9.183 -  from Pxy show borel: "Px \<in> borel_measurable S"
9.184 -    by (auto intro!: T.positive_integral_fst_measurable dest!: distributed_borel_measurable simp: Px_def)
9.185 +  show borel: "Px \<in> borel_measurable S"
9.186 +    by (auto intro!: T.positive_integral_fst_measurable simp: Px_def)
9.187
9.188    interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
9.189 -    using XY by (rule prob_space_distr)
9.190 +    by (intro prob_space_distr) simp
9.191    have "(\<integral>\<^isup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
9.192      using Pxy
9.193 -    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_borel_measurable distributed_AE)
9.194 +    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
9.195
9.196    show "distr M S X = density S Px"
9.197    proof (rule measure_eqI)
9.198      fix A assume A: "A \<in> sets (distr M S X)"
9.199 -    with X Y XY have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
9.200 -      by (auto simp add: emeasure_distr
9.201 -               intro!: arg_cong[where f="emeasure M"] dest: measurable_space)
9.202 +    with X measurable_space[of Y M T]
9.203 +    have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
9.204 +      by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"])
9.205      also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)"
9.206        using Pxy by (simp add: distributed_def)
9.207      also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
9.208        using A borel Pxy
9.209 -      by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric] distributed_def)
9.210 +      by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric])
9.211      also have "\<dots> = \<integral>\<^isup>+ x. Px x * indicator A x \<partial>S"
9.212        apply (rule positive_integral_cong_AE)
9.213        using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
9.214 @@ -763,7 +784,7 @@
9.215        moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
9.216          by (auto simp: indicator_def)
9.217        ultimately have "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) * indicator A x"
9.218 -        using Pxy[THEN distributed_borel_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong)
9.219 +        by (simp add: eq positive_integral_multc cong: positive_integral_cong)
9.220        also have "(\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) = Px x"
9.221          by (simp add: Px_def ereal_real positive_integral_positive)
9.222        finally show "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
9.223 @@ -800,7 +821,7 @@
9.224
9.225  lemma (in prob_space) distributed_joint_indep':
9.226    assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
9.227 -  assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"
9.228 +  assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py"
9.229    assumes indep: "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
9.230    shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
9.231    unfolding distributed_def
9.232 @@ -811,30 +832,23 @@
9.233
9.234    interpret X: prob_space "density S Px"
9.235      unfolding distributed_distr_eq_density[OF X, symmetric]
9.236 -    using distributed_measurable[OF X]
9.237 -    by (rule prob_space_distr)
9.238 +    by (rule prob_space_distr) simp
9.239    have sf_X: "sigma_finite_measure (density S Px)" ..
9.240
9.241    interpret Y: prob_space "density T Py"
9.242      unfolding distributed_distr_eq_density[OF Y, symmetric]
9.243 -    using distributed_measurable[OF Y]
9.244 -    by (rule prob_space_distr)
9.245 +    by (rule prob_space_distr) simp
9.246    have sf_Y: "sigma_finite_measure (density T Py)" ..
9.247
9.248    show "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). Px x * Py y)"
9.249      unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
9.250      using distributed_borel_measurable[OF X] distributed_AE[OF X]
9.251      using distributed_borel_measurable[OF Y] distributed_AE[OF Y]
9.252 -    by (rule pair_measure_density[OF _ _ _ _ S T sf_X sf_Y])
9.253 +    by (rule pair_measure_density[OF _ _ _ _ T sf_Y])
9.254
9.255 -  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
9.256 -    using distributed_measurable[OF X] distributed_measurable[OF Y]
9.257 -    by (auto intro: measurable_Pair)
9.258 +  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" by auto
9.259
9.260 -  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)"
9.261 -    by (auto simp: split_beta'
9.262 -             intro!: measurable_compose[OF _ distributed_borel_measurable[OF X]]
9.263 -                     measurable_compose[OF _ distributed_borel_measurable[OF Y]])
9.264 +  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)" by auto
9.265
9.266    show "AE x in S \<Otimes>\<^isub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)"
9.267      apply (intro ST.AE_pair_measure borel_measurable_ereal_le Pxy borel_measurable_const)
```
```    10.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Nov 02 14:23:40 2012 +0100
10.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Nov 02 14:23:54 2012 +0100
10.3 @@ -47,7 +47,7 @@
10.4    shows "\<exists>h\<in>borel_measurable M. integral\<^isup>P M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>) \<and> (\<forall>x. 0 \<le> h x)"
10.5  proof -
10.6    obtain A :: "nat \<Rightarrow> 'a set" where
10.7 -    range: "range A \<subseteq> sets M" and
10.8 +    range[measurable]: "range A \<subseteq> sets M" and
10.9      space: "(\<Union>i. A i) = space M" and
10.10      measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>" and
10.11      disjoint: "disjoint_family A"
10.12 @@ -97,10 +97,7 @@
10.13        assume "x \<notin> space M" then have "\<And>i. x \<notin> A i" using space by auto
10.14        then show "0 \<le> ?h x" by auto
10.15      qed
10.16 -  next
10.17 -    show "?h \<in> borel_measurable M" using range n
10.18 -      by (auto intro!: borel_measurable_psuminf borel_measurable_ereal_times ereal_0_le_mult intro: less_imp_le)
10.19 -  qed
10.20 +  qed measurable
10.21  qed
10.22
10.23  subsection "Absolutely continuous"
10.24 @@ -298,6 +295,8 @@
10.25  proof -
10.26    interpret N: finite_measure N by fact
10.27    def G \<equiv> "{g \<in> borel_measurable M. (\<forall>x. 0 \<le> g x) \<and> (\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> N A)}"
10.28 +  { fix f have "f \<in> G \<Longrightarrow> f \<in> borel_measurable M" by (auto simp: G_def) }
10.29 +  note this[measurable_dest]
10.30    have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
10.31    hence "G \<noteq> {}" by auto
10.32    { fix f g assume f: "f \<in> G" and g: "g \<in> G"
10.33 @@ -329,10 +328,10 @@
10.34      qed }
10.35    note max_in_G = this
10.36    { fix f assume  "incseq f" and f: "\<And>i. f i \<in> G"
10.37 +    then have [measurable]: "\<And>i. f i \<in> borel_measurable M" by (auto simp: G_def)
10.38      have "(\<lambda>x. SUP i. f i x) \<in> G" unfolding G_def
10.39      proof safe
10.40 -      show "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M"
10.41 -        using f by (auto simp: G_def)
10.42 +      show "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M" by measurable
10.43        { fix x show "0 \<le> (SUP i. f i x)"
10.44            using f by (auto simp: G_def intro: SUP_upper2) }
10.45      next
10.46 @@ -379,7 +378,7 @@
10.47    note g_in_G = this
10.48    have "incseq ?g" using gs_not_empty
10.49      by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc)
10.50 -  from SUP_in_G[OF this g_in_G] have "f \<in> G" unfolding f_def .
10.51 +  from SUP_in_G[OF this g_in_G] have [measurable]: "f \<in> G" unfolding f_def .
10.52    then have [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
10.53    have "integral\<^isup>P M f = (SUP i. integral\<^isup>P M (?g i))" unfolding f_def
10.54      using g_in_G `incseq ?g`
10.55 @@ -467,7 +466,7 @@
10.56        hence "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) =
10.57            (\<integral>\<^isup>+x. f x * indicator A x \<partial>M) + b * emeasure M (A \<inter> A0)"
10.58          using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A b `f \<in> G`
10.61      note f0_eq = this
10.62      { fix A assume A: "A \<in> sets M"
10.63        hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
10.64 @@ -484,8 +483,8 @@
10.65          using f_le_v N.emeasure_eq_measure[of A] positive_integral_positive[of M "?F A"]
10.66          by (cases "\<integral>\<^isup>+x. ?F A x \<partial>M", cases "N A") auto
10.67        finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) \<le> N A" . }
10.68 -    hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` unfolding G_def
10.69 -      by (auto intro!: ereal_add_nonneg_nonneg)
10.70 +    hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G`
10.71 +      by (auto intro!: ereal_add_nonneg_nonneg simp: G_def)
10.72      have int_f_finite: "integral\<^isup>P M f \<noteq> \<infinity>"
10.73        by (metis N.emeasure_finite ereal_infty_less_eq2(1) int_f_eq_y y_le)
10.74      have  "0 < ?M (space M) - emeasure ?Mb (space M)"
10.75 @@ -676,6 +675,7 @@
10.76      with Q_fin show "finite_measure (?N i)"
10.77        by (auto intro!: finite_measureI)
10.78      show "sets (?N i) = sets (?M i)" by (simp add: sets_eq)
10.79 +    have [measurable]: "\<And>A. A \<in> sets M \<Longrightarrow> A \<in> sets N" by (simp add: sets_eq)
10.80      show "absolutely_continuous (?M i) (?N i)"
10.81        using `absolutely_continuous M N` `Q i \<in> sets M`
10.82        by (auto simp: absolutely_continuous_def null_sets_density_iff sets_eq
10.83 @@ -731,9 +731,7 @@
10.84        ultimately have "N A = (\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M)"
10.85          using plus_emeasure[of "(\<Union>i. Q i) \<inter> A" N "Q0 \<inter> A"] by (simp add: sets_eq)
10.86        with `A \<in> sets M` borel Q Q0(1) show "emeasure (density M ?f) A = N A"
10.87 -        by (subst emeasure_density)
10.88 -           (auto intro!: borel_measurable_ereal_add borel_measurable_psuminf measurable_If
10.89 -                 simp: subset_eq)
10.90 +        by (auto simp: subset_eq emeasure_density)
10.92    qed
10.93  qed
10.94 @@ -845,7 +843,7 @@
10.95      unfolding indicator_def by auto
10.96    have "\<forall>i. AE x in M. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos
10.97      by (intro finite_density_unique[THEN iffD1] allI)
10.98 -       (auto intro!: borel_measurable_ereal_times f measure_eqI Int simp: emeasure_density * subset_eq)
10.99 +       (auto intro!: f measure_eqI simp: emeasure_density * subset_eq)
10.100    moreover have "AE x in M. ?f Q0 x = ?f' Q0 x"
10.101    proof (rule AE_I')
10.102      { fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
10.103 @@ -1083,7 +1081,7 @@
10.104
10.105  lemma (in sigma_finite_measure) RN_deriv:
10.106    assumes "absolutely_continuous M N" "sets N = sets M"
10.107 -  shows borel_measurable_RN_deriv: "RN_deriv M N \<in> borel_measurable M" (is ?borel)
10.108 +  shows borel_measurable_RN_deriv[measurable]: "RN_deriv M N \<in> borel_measurable M" (is ?borel)
10.109      and density_RN_deriv: "density M (RN_deriv M N) = N" (is ?density)
10.110      and RN_deriv_nonneg: "0 \<le> RN_deriv M N x" (is ?pos)
10.111  proof -
10.112 @@ -1164,7 +1162,7 @@
10.113      qed
10.114    qed
10.115    have "(RN_deriv ?M' ?N') \<circ> T \<in> borel_measurable M"
10.116 -    using T ac by (intro measurable_comp[where b="?M'"] M'.borel_measurable_RN_deriv) simp_all
10.117 +    using T ac by measurable simp
10.118    then show "(\<lambda>x. RN_deriv ?M' ?N' (T x)) \<in> borel_measurable M"
10.120    show "AE x in M. 0 \<le> RN_deriv ?M' ?N' (T x)" using M'.RN_deriv_nonneg[OF ac] by auto
```
```    11.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:23:40 2012 +0100
11.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:23:54 2012 +0100
11.3 @@ -1263,6 +1263,11 @@
11.4    shows "f \<in> measurable M (measure_of \<Omega> N \<mu>) \<longleftrightarrow> (\<forall>A\<in>N. f -` A \<inter> space M \<in> sets M)"
11.5    by (metis assms in_measure_of measurable_measure_of assms measurable_sets)
11.6
11.7 +lemma measurable_cong_sets:
11.8 +  assumes sets: "sets M = sets M'" "sets N = sets N'"
11.9 +  shows "measurable M N = measurable M' N'"
11.10 +  using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def)
11.11 +
11.12  lemma measurable_cong:
11.13    assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
11.14    shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'"
11.15 @@ -1275,7 +1280,22 @@
11.16        \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
11.17    by (simp add: measurable_def sigma_algebra_iff2)
11.18
11.19 -lemma measurable_const[intro, simp]:
11.20 +lemma measurable_compose:
11.21 +  assumes f: "f \<in> measurable M N" and g: "g \<in> measurable N L"
11.22 +  shows "(\<lambda>x. g (f x)) \<in> measurable M L"
11.23 +proof -
11.24 +  have "\<And>A. (\<lambda>x. g (f x)) -` A \<inter> space M = f -` (g -` A \<inter> space N) \<inter> space M"
11.25 +    using measurable_space[OF f] by auto
11.26 +  with measurable_space[OF f] measurable_space[OF g] show ?thesis
11.27 +    by (auto intro: measurable_sets[OF f] measurable_sets[OF g]
11.28 +             simp del: vimage_Int simp add: measurable_def)
11.29 +qed
11.30 +
11.31 +lemma measurable_comp:
11.32 +  "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> g \<circ> f \<in> measurable M L"
11.33 +  using measurable_compose[of f M N g L] by (simp add: comp_def)
11.34 +
11.35 +lemma measurable_const:
11.36    "c \<in> space M' \<Longrightarrow> (\<lambda>x. c) \<in> measurable M M'"
11.37    by (auto simp add: measurable_def)
11.38
11.39 @@ -1308,23 +1328,11 @@
11.40    thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<inter> space M \<in> sets M` by auto
11.41  qed
11.42
11.43 -lemma measurable_ident[intro, simp]: "id \<in> measurable M M"
11.44 -  by (auto simp add: measurable_def)
11.45 -
11.46 -lemma measurable_ident'[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
11.47 +lemma measurable_ident: "id \<in> measurable M M"
11.48    by (auto simp add: measurable_def)
11.49
11.50 -lemma measurable_comp[intro]:
11.51 -  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
11.52 -  shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
11.53 -  apply (auto simp add: measurable_def vimage_compose)
11.54 -  apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
11.55 -  apply force+
11.56 -  done
11.57 -
11.58 -lemma measurable_compose:
11.59 -  "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> (\<lambda>x. g (f x)) \<in> measurable M L"
11.60 -  using measurable_comp[of f M N g L] by (simp add: comp_def)
11.61 +lemma measurable_ident': "(\<lambda>x. x) \<in> measurable M M"
11.62 +  by (auto simp add: measurable_def)
11.63
11.64  lemma sets_Least:
11.65    assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
11.66 @@ -1469,7 +1477,7 @@
11.67
11.68  lemma measurable_count_space_const:
11.69    "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
11.70 -  by auto
11.71 +  by (simp add: measurable_const)
11.72
11.73  lemma measurable_count_space:
11.74    "f \<in> measurable (count_space A) (count_space UNIV)"
11.75 @@ -1489,10 +1497,10 @@
11.76
11.77  structure Data = Generic_Data
11.78  (
11.79 -  type T = thm list * thm list;
11.80 -  val empty = ([], []);
11.81 +  type T = (thm list * thm list) * thm list;
11.82 +  val empty = (([], []), []);
11.83    val extend = I;
11.84 -  val merge = fn ((a, b), (c, d)) => (a @ c, b @ d);
11.85 +  val merge = fn (((c1, g1), d1), ((c2, g2), d2)) => ((c1 @ c2, g1 @ g2), d1 @ d2);
11.86  );
11.87
11.88  val debug =
11.89 @@ -1501,12 +1509,15 @@
11.90  val backtrack =
11.91    Attrib.setup_config_int @{binding measurable_backtrack} (K 40)
11.92
11.93 -fun get lv = (case lv of Concrete => fst | Generic => snd) o Data.get o Context.Proof;
11.94 +fun get lv = (case lv of Concrete => fst | Generic => snd) o fst o Data.get o Context.Proof;
11.95  fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
11.96
11.97 -fun update f lv = Data.map (case lv of Concrete => apfst f | Generic => apsnd f);
11.98 +fun update f lv = Data.map (apfst (case lv of Concrete => apfst f | Generic => apsnd f));
11.99  fun add thms' = update (fn thms => thms @ thms');
11.100
11.101 +val get_dest = snd o Data.get;
11.102 +fun add_dest thm = Data.map (apsnd (fn thms => thms @ [thm]));
11.103 +
11.104  fun TRYALL' tacs = fold_rev (curry op APPEND') tacs (K no_tac);
11.105
11.106  fun is_too_generic thm =
11.107 @@ -1515,11 +1526,10 @@
11.108      val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
11.109    in is_Var (head_of concl') end
11.110
11.111 -fun import_theorem thm = if is_too_generic thm then [] else
11.112 -  [thm] @ map_filter (try (fn th' => thm RS th'))
11.113 -    [@{thm measurable_compose_rev}, @{thm pred_sets1}, @{thm pred_sets2}, @{thm sets_into_space}];
11.114 +fun import_theorem ctxt thm = if is_too_generic thm then [] else
11.115 +  [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
11.116
11.117 -fun add_thm (raw, lv) thm = add (if raw then [thm] else import_theorem thm) lv;
11.118 +fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
11.119
11.120  fun debug_tac ctxt msg f = if Config.get ctxt debug then K (print_tac (msg ())) THEN' f else f
11.121
11.122 @@ -1573,8 +1583,9 @@
11.123      handle TERM _ => no_tac) 1)
11.124
11.125  fun single_measurable_tac ctxt facts =
11.126 -  debug_tac ctxt (fn () => "single + " ^ Pretty.str_of (Pretty.block (map (Syntax.pretty_term ctxt o prop_of) facts)))
11.127 -  (resolve_tac ((maps (import_theorem o Simplifier.norm_hhf) facts) @ get_all ctxt)
11.128 +  debug_tac ctxt (fn () => "single + " ^
11.129 +    Pretty.str_of (Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)))))
11.130 +  (resolve_tac ((maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt)
11.131      APPEND' (split_fun_tac ctxt));
11.132
11.133  fun is_cond_formlua n thm = if length (prems_of thm) < n then false else
11.134 @@ -1598,6 +1609,9 @@
11.135    Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.\$\$\$ "raw" >> K true) false --
11.136       Scan.optional (Args.\$\$\$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
11.137
11.138 +val dest_attr : attribute context_parser =
11.139 +  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
11.140 +
11.141  val method : (Proof.context -> Method.method) context_parser =
11.142    Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts 1)));
11.143
11.144 @@ -1613,10 +1627,17 @@
11.145  *}
11.146
11.147  attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
11.148 +attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
11.149  method_setup measurable = {* Measurable.method *} "measurability prover"
11.150  simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
11.151
11.152  declare
11.153 +  measurable_compose_rev[measurable_dest]
11.154 +  pred_sets1[measurable_dest]
11.155 +  pred_sets2[measurable_dest]
11.156 +  sets_into_space[measurable_dest]
11.157 +
11.158 +declare
11.159    top[measurable]
11.160    empty_sets[measurable (raw)]
11.161    Un[measurable (raw)]
11.162 @@ -1670,7 +1691,7 @@
11.163    "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
11.164    "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))"
11.165    "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
11.166 -  by (auto intro!: sets_Collect simp: iff_conv_conj_imp pred_def)
11.167 +  by (auto simp: iff_conv_conj_imp pred_def)
11.168
11.169  lemma pred_intros_countable[measurable (raw)]:
11.170    fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
11.171 @@ -1743,6 +1764,34 @@
11.172  declare
11.173    Int[measurable (raw)]
11.174
11.175 +lemma pred_in_If[measurable (raw)]:
11.176 +  "pred M (\<lambda>x. (P x \<longrightarrow> x \<in> A x) \<and> (\<not> P x \<longrightarrow> x \<in> B x)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (if P x then A x else B x))"
11.177 +  by auto
11.178 +
11.179 +lemma sets_range[measurable_dest]:
11.180 +  "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
11.181 +  by auto
11.182 +
11.183 +lemma pred_sets_range[measurable_dest]:
11.184 +  "A ` I \<subseteq> sets N \<Longrightarrow> i \<in> I \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
11.185 +  using pred_sets2[OF sets_range] by auto
11.186 +
11.187 +lemma sets_All[measurable_dest]:
11.188 +  "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
11.189 +  by auto
11.190 +
11.191 +lemma pred_sets_All[measurable_dest]:
11.192 +  "\<forall>i. A i \<in> sets (N i) \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
11.193 +  using pred_sets2[OF sets_All, of A N f] by auto
11.194 +
11.195 +lemma sets_Ball[measurable_dest]:
11.196 +  "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
11.197 +  by auto
11.198 +
11.199 +lemma pred_sets_Ball[measurable_dest]:
11.200 +  "\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
11.201 +  using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
11.202 +
11.203  hide_const (open) pred
11.204
11.205  subsection {* Extend measure *}
```