author hoelzl Thu Dec 09 10:22:17 2010 +0100 (2010-12-09) changeset 41098 ababba14c965 parent 41094 1dc7652ce404 parent 41097 a1abfa4e2b44 child 41102 3933a73dbcb3
merged
```     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Thu Dec 09 08:46:04 2010 +0100
1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Thu Dec 09 10:22:17 2010 +0100
1.3 @@ -1347,6 +1347,16 @@
1.4      by (auto intro!: measurable_If)
1.5  qed
1.6
1.7 +lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
1.8 +  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
1.9 +  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
1.10 +  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
1.11 +proof cases
1.12 +  assume "finite S"
1.13 +  thus ?thesis using assms
1.14 +    by induct auto
1.15 +qed (simp add: borel_measurable_const)
1.16 +
1.17  lemma (in sigma_algebra) borel_measurable_pextreal_times[intro, simp]:
1.18    fixes f :: "'a \<Rightarrow> pextreal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1.19    shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
1.20 @@ -1359,15 +1369,14 @@
1.21      by (auto intro!: measurable_If)
1.22  qed
1.23
1.24 -lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
1.25 +lemma (in sigma_algebra) borel_measurable_pextreal_setprod[simp, intro]:
1.26    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
1.27    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
1.28 -  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
1.29 +  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
1.30  proof cases
1.31    assume "finite S"
1.32 -  thus ?thesis using assms
1.33 -    by induct auto
1.34 -qed (simp add: borel_measurable_const)
1.35 +  thus ?thesis using assms by induct auto
1.36 +qed simp
1.37
1.38  lemma (in sigma_algebra) borel_measurable_pextreal_min[simp, intro]:
1.39    fixes f g :: "'a \<Rightarrow> pextreal"
1.40 @@ -1386,7 +1395,7 @@
1.41  lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]:
1.42    fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> pextreal"
1.43    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
1.44 -  shows "(SUP i : A. f i) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
1.45 +  shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
1.46    unfolding borel_measurable_pextreal_iff_greater
1.47  proof safe
1.48    fix a
1.49 @@ -1399,7 +1408,7 @@
1.50  lemma (in sigma_algebra) borel_measurable_INF[simp, intro]:
1.51    fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> pextreal"
1.52    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
1.53 -  shows "(INF i : A. f i) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
1.54 +  shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
1.55    unfolding borel_measurable_pextreal_iff_less
1.56  proof safe
1.57    fix a
1.58 @@ -1423,20 +1432,10 @@
1.59      using assms by auto
1.60  qed
1.61
1.62 -lemma INFI_fun_expand:
1.63 -  "(INF y:A. f y) = (\<lambda>x. (INF y:A. f y x))"
1.64 -  by (simp add: fun_eq_iff INFI_apply)
1.65 -
1.66 -lemma SUPR_fun_expand:
1.67 -  "(SUP y:A. f y) = (\<lambda>x. (SUP y:A. f y x))"
1.68 -  by (simp add: fun_eq_iff SUPR_apply)
1.69 -
1.70  lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]:
1.71    assumes "\<And>i. f i \<in> borel_measurable M"
1.72    shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
1.73 -  using assms unfolding psuminf_def
1.74 -  by (auto intro!: borel_measurable_SUP [unfolded SUPR_fun_expand])
1.75 -
1.76 +  using assms unfolding psuminf_def by auto
1.77
1.78  section "LIMSEQ is borel measurable"
1.79
1.80 @@ -1459,13 +1458,12 @@
1.81    note eq = this
1.82    have *: "\<And>x. real (Real (u' x)) - real (Real (- u' x)) = u' x"
1.83      by auto
1.84 -  have "(SUP n. INF m. (\<lambda>x. Real (u (n + m) x))) \<in> borel_measurable M"
1.85 -       "(SUP n. INF m. (\<lambda>x. Real (- u (n + m) x))) \<in> borel_measurable M"
1.86 -    using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real)
1.87 +  have "(\<lambda>x. SUP n. INF m. Real (u (n + m) x)) \<in> borel_measurable M"
1.88 +       "(\<lambda>x. SUP n. INF m. Real (- u (n + m) x)) \<in> borel_measurable M"
1.89 +    using u by auto
1.90    with eq[THEN measurable_cong, of M "\<lambda>x. x" borel]
1.91    have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
1.92 -       "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
1.93 -    unfolding SUPR_fun_expand INFI_fun_expand by auto
1.94 +       "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M" by auto
1.95    note this[THEN borel_measurable_real]
1.96    from borel_measurable_diff[OF this]
1.97    show ?thesis unfolding * .
```
```     2.1 --- a/src/HOL/Probability/Complete_Measure.thy	Thu Dec 09 08:46:04 2010 +0100
2.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Thu Dec 09 10:22:17 2010 +0100
2.3 @@ -257,17 +257,14 @@
2.4    show ?thesis
2.5    proof (intro bexI)
2.6      from AE[unfolded all_AE_countable]
2.7 -    show "AE x. g x = (SUP i. f' i) x" (is "AE x. g x = ?f x")
2.8 +    show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
2.9      proof (rule AE_mp, safe intro!: AE_cong)
2.10        fix x assume eq: "\<forall>i. f i x = f' i x"
2.11 -      have "g x = (SUP i. f i x)"
2.12 -        using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto
2.13 -      then show "g x = ?f x"
2.14 -        using eq unfolding SUPR_fun_expand by auto
2.15 +      moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
2.16 +      ultimately show "g x = ?f x" by (simp add: SUPR_apply)
2.17      qed
2.18      show "?f \<in> borel_measurable M"
2.19 -      using sf by (auto intro!: borel_measurable_SUP
2.20 -        intro: borel_measurable_simple_function)
2.21 +      using sf by (auto intro: borel_measurable_simple_function)
2.22    qed
2.23  qed
2.24
```
```     3.1 --- a/src/HOL/Probability/Information.thy	Thu Dec 09 08:46:04 2010 +0100
3.2 +++ b/src/HOL/Probability/Information.thy	Thu Dec 09 10:22:17 2010 +0100
3.3 @@ -188,7 +188,7 @@
3.4      using f by (rule \<nu>.measure_space_isomorphic)
3.5
3.6    let ?RN = "sigma_finite_measure.RN_deriv ?M ?\<mu> ?\<nu>"
3.7 -  from RN_deriv_vimage[OF f \<nu>]
3.8 +  from RN_deriv_vimage[OF f[THEN bij_inv_the_inv_into] \<nu>]
3.9    have *: "\<nu>.almost_everywhere (\<lambda>x. ?RN (the_inv_into S f x) = RN_deriv \<nu> x)"
3.10      by (rule absolutely_continuous_AE[OF \<nu>])
3.11
```
```     4.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Dec 09 08:46:04 2010 +0100
4.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Dec 09 10:22:17 2010 +0100
4.3 @@ -1069,16 +1069,16 @@
4.4
4.5  lemma (in measure_space) positive_integral_vimage_inv:
4.6    fixes g :: "'d \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
4.7 -  assumes f: "bij_betw f S (space M)"
4.8 +  assumes f: "bij_inv S (space M) f h"
4.9    shows "measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) g =
4.10 -      positive_integral (\<lambda>x. g (the_inv_into S f x))"
4.11 +      positive_integral (\<lambda>x. g (h x))"
4.12  proof -
4.13    interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
4.14 -    using f by (rule measure_space_isomorphic)
4.15 +    using f by (rule measure_space_isomorphic[OF bij_inv_bij_betw(1)])
4.16    show ?thesis
4.17 -    unfolding positive_integral_vimage[OF f, of "\<lambda>x. g (the_inv_into S f x)"]
4.18 -    using f[unfolded bij_betw_def]
4.19 -    by (auto intro!: v.positive_integral_cong simp: the_inv_into_f_f)
4.20 +    unfolding positive_integral_vimage[OF f[THEN bij_inv_bij_betw(1)], of "\<lambda>x. g (h x)"]
4.21 +    using f[unfolded bij_inv_def]
4.22 +    by (auto intro!: v.positive_integral_cong)
4.23  qed
4.24
4.25  lemma (in measure_space) positive_integral_SUP_approx:
4.26 @@ -1176,8 +1176,6 @@
4.27      apply (rule positive_integral_mono)
4.28      using `f \<up> u` unfolding isoton_def le_fun_def by auto
4.29  next
4.30 -  have "u \<in> borel_measurable M"
4.31 -    using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def)
4.32    have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto
4.33
4.34    show "(SUP i. positive_integral (f i)) = positive_integral u"
4.35 @@ -1198,8 +1196,6 @@
4.36    shows "(SUP i. positive_integral (f i)) = positive_integral (\<lambda>x. SUP i. f i x)"
4.37      (is "_ = positive_integral ?u")
4.38  proof -
4.39 -  have "?u \<in> borel_measurable M"
4.40 -    using borel_measurable_SUP[of _ f] assms by (simp add: SUPR_fun_expand)
4.41    show ?thesis
4.42    proof (rule antisym)
4.43      show "(SUP j. positive_integral (f j)) \<le> positive_integral ?u"
4.44 @@ -1209,9 +1205,9 @@
4.45      have "\<And>i. rf i \<in> borel_measurable M" unfolding rf_def
4.46        using assms by (simp cong: measurable_cong)
4.47      moreover have iso: "rf \<up> ru" using assms unfolding rf_def ru_def
4.48 -      unfolding isoton_def SUPR_fun_expand le_fun_def fun_eq_iff
4.49 +      unfolding isoton_def le_fun_def fun_eq_iff SUPR_apply
4.50        using SUP_const[OF UNIV_not_empty]
4.51 -      by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff)
4.52 +      by (auto simp: restrict_def le_fun_def fun_eq_iff)
4.53      ultimately have "positive_integral ru \<le> (SUP i. positive_integral (rf i))"
4.54        unfolding positive_integral_alt[of ru]
4.55        by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx)
4.56 @@ -1283,6 +1279,11 @@
4.57    shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f"
4.58    using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto
4.59
4.60 +lemma (in measure_space) positive_integral_multc:
4.61 +  assumes "f \<in> borel_measurable M"
4.62 +  shows "positive_integral (\<lambda>x. f x * c) = positive_integral f * c"
4.63 +  unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
4.64 +
4.65  lemma (in measure_space) positive_integral_indicator[simp]:
4.66    "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A"
4.67  by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
4.68 @@ -1349,24 +1350,16 @@
4.69  lemma (in measure_space) positive_integral_lim_INF:
4.70    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pextreal"
4.71    assumes "\<And>i. u i \<in> borel_measurable M"
4.72 -  shows "positive_integral (SUP n. INF m. u (m + n)) \<le>
4.73 +  shows "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x) \<le>
4.74      (SUP n. INF m. positive_integral (u (m + n)))"
4.75  proof -
4.76 -  have "(SUP n. INF m. u (m + n)) \<in> borel_measurable M"
4.77 -    by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
4.78 -
4.79 -  have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
4.80 -  proof (unfold isoton_def, safe intro!: INF_mono bexI)
4.81 -    fix i m show "u (Suc m + i) \<le> u (m + Suc i)" by simp
4.82 -  qed simp
4.83 -  from positive_integral_isoton[OF this] assms
4.84 -  have "positive_integral (SUP n. INF m. u (m + n)) =
4.85 -    (SUP n. positive_integral (INF m. u (m + n)))"
4.86 -    unfolding isoton_def by (simp add: borel_measurable_INF)
4.87 +  have "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x)
4.88 +      = (SUP n. positive_integral (\<lambda>x. INF m. u (m + n) x))"
4.89 +    using assms
4.90 +    by (intro positive_integral_monotone_convergence_SUP[symmetric] INF_mono)
4.91 +       (auto simp del: add_Suc simp add: add_Suc[symmetric])
4.92    also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
4.93 -    apply (rule SUP_mono)
4.94 -    apply (rule_tac x=n in bexI)
4.95 -    by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand)
4.96 +    by (auto intro!: SUP_mono bexI le_INFI positive_integral_mono INF_leI)
4.97    finally show ?thesis .
4.98  qed
4.99
4.100 @@ -1763,6 +1756,11 @@
4.101    thus ?P ?I by auto
4.102  qed
4.103
4.104 +lemma (in measure_space) integral_multc:
4.105 +  assumes "integrable f"
4.106 +  shows "integral (\<lambda>x. f x * c) = integral f * c"
4.107 +  unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
4.108 +
4.109  lemma (in measure_space) integral_mono_AE:
4.110    assumes fg: "integrable f" "integrable g"
4.111    and mono: "AE t. f t \<le> g t"
4.112 @@ -1950,10 +1948,10 @@
4.113
4.114    have borel_f: "\<And>i. (\<lambda>x. Real (f i x)) \<in> borel_measurable M"
4.115      using i unfolding integrable_def by auto
4.116 -  hence "(SUP i. (\<lambda>x. Real (f i x))) \<in> borel_measurable M"
4.117 +  hence "(\<lambda>x. SUP i. Real (f i x)) \<in> borel_measurable M"
4.118      by auto
4.119    hence borel_u: "u \<in> borel_measurable M"
4.120 -    using pos_u by (auto simp: borel_measurable_Real_eq SUPR_fun_expand SUP_F)
4.121 +    using pos_u by (auto simp: borel_measurable_Real_eq SUP_F)
4.122
4.123    have integral_eq: "\<And>n. positive_integral (\<lambda>x. Real (f n x)) = Real (integral (f n))"
4.124      using i unfolding integral_def integrable_def by (auto simp: Real_real)
4.125 @@ -2134,8 +2132,8 @@
4.126      thus ?thesis by simp
4.127    next
4.128      assume neq_0: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> 0"
4.129 -    have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (SUP n. INF m. (\<lambda>x. Real (?diff (m + n) x)))"
4.130 -    proof (rule positive_integral_cong, unfold SUPR_fun_expand INFI_fun_expand, subst add_commute)
4.131 +    have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (\<lambda>x. SUP n. INF m. Real (?diff (m + n) x))"
4.132 +    proof (rule positive_integral_cong, subst add_commute)
4.133        fix x assume x: "x \<in> space M"
4.134        show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))"
4.135        proof (rule LIMSEQ_imp_lim_INF[symmetric])
```
```     5.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Dec 09 08:46:04 2010 +0100
5.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Dec 09 10:22:17 2010 +0100
5.3 @@ -552,10 +552,10 @@
5.4  proof -
5.5    from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
5.6    show ?ilim using mono lim i by auto
5.7 -  have "(SUP i. f i) = u" using mono lim SUP_Lim_pextreal
5.8 -    unfolding fun_eq_iff SUPR_fun_expand mono_def by auto
5.9 -  moreover have "(SUP i. f i) \<in> borel_measurable M"
5.10 -    using i by (rule borel_measurable_SUP)
5.11 +  have "\<And>x. (SUP i. f i x) = u x" using mono lim SUP_Lim_pextreal
5.12 +    unfolding fun_eq_iff mono_def by auto
5.13 +  moreover have "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M"
5.14 +    using i by auto
5.15    ultimately show "u \<in> borel_measurable M" by simp
5.16  qed
5.17
5.18 @@ -647,44 +647,20 @@
5.19  definition p2e :: "(nat \<Rightarrow> real) \<Rightarrow> 'a::ordered_euclidean_space" where
5.20    "p2e x = (\<chi>\<chi> i. x i)"
5.21
5.22 -lemma bij_euclidean_component:
5.23 -  "bij_betw (e2p::'a::ordered_euclidean_space \<Rightarrow> _) (UNIV :: 'a set)
5.24 -  ({..<DIM('a)} \<rightarrow>\<^isub>E (UNIV :: real set))"
5.25 -  unfolding bij_betw_def e2p_def_raw
5.26 -proof let ?e = "\<lambda>x.\<lambda>i\<in>{..<DIM('a::ordered_euclidean_space)}. (x::'a)\$\$i"
5.27 -  show "inj ?e" unfolding inj_on_def restrict_def apply(subst euclidean_eq) apply safe
5.28 -    apply(drule_tac x=i in fun_cong) by auto
5.29 -  { fix x::"nat \<Rightarrow> real" assume x:"\<forall>i. i \<notin> {..<DIM('a)} \<longrightarrow> x i = undefined"
5.30 -    hence "x = ?e (\<chi>\<chi> i. x i)" apply-apply(rule,case_tac "xa<DIM('a)") by auto
5.31 -    hence "x \<in> range ?e" by fastsimp
5.32 -  } thus "range ?e = ({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}"
5.33 -    unfolding extensional_def using DIM_positive by auto
5.34 -qed
5.35 +lemma e2p_p2e[simp]:
5.36 +  "x \<in> extensional {..<DIM('a)} \<Longrightarrow> e2p (p2e x::'a::ordered_euclidean_space) = x"
5.37 +  by (auto simp: fun_eq_iff extensional_def p2e_def e2p_def)
5.38
5.39 -lemma bij_p2e:
5.40 -  "bij_betw (p2e::_ \<Rightarrow> 'a::ordered_euclidean_space) ({..<DIM('a)} \<rightarrow>\<^isub>E (UNIV :: real set))
5.41 -  (UNIV :: 'a set)" (is "bij_betw ?p ?U _")
5.42 -  unfolding bij_betw_def
5.43 -proof show "inj_on ?p ?U" unfolding inj_on_def p2e_def
5.44 -    apply(subst euclidean_eq) apply(safe,rule) unfolding extensional_def
5.45 -    apply(case_tac "xa<DIM('a)") by auto
5.46 -  { fix x::'a have "x \<in> ?p ` extensional {..<DIM('a)}"
5.47 -      unfolding image_iff apply(rule_tac x="\<lambda>i. if i<DIM('a) then x\$\$i else undefined" in bexI)
5.48 -      apply(subst euclidean_eq,safe) unfolding p2e_def extensional_def by auto
5.49 -  } thus "?p ` ?U = UNIV" by auto
5.50 -qed
5.51 +lemma p2e_e2p[simp]:
5.52 +  "p2e (e2p x) = (x::'a::ordered_euclidean_space)"
5.53 +  by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def)
5.54
5.55 -lemma e2p_p2e[simp]: fixes z::"'a::ordered_euclidean_space"
5.56 -  assumes "x \<in> extensional {..<DIM('a)}"
5.57 -  shows "e2p (p2e x::'a) = x"
5.58 -proof fix i::nat
5.59 -  show "e2p (p2e x::'a) i = x i" unfolding e2p_def p2e_def restrict_def
5.60 -    using assms unfolding extensional_def by auto
5.61 -qed
5.62 -
5.63 -lemma p2e_e2p[simp]: fixes x::"'a::ordered_euclidean_space"
5.64 -  shows "p2e (e2p x) = x"
5.65 -  apply(subst euclidean_eq) unfolding e2p_def p2e_def restrict_def by auto
5.66 +lemma bij_inv_p2e_e2p:
5.67 +  shows "bij_inv ({..<DIM('a)} \<rightarrow>\<^isub>E UNIV) (UNIV :: 'a::ordered_euclidean_space set)
5.68 +     p2e e2p" (is "bij_inv ?P ?U _ _")
5.69 +proof (rule bij_invI)
5.70 +  show "p2e \<in> ?P \<rightarrow> ?U" "e2p \<in> ?U \<rightarrow> ?P" by (auto simp: e2p_def)
5.71 +qed auto
5.72
5.73  interpretation borel_product: product_sigma_finite "\<lambda>x. borel::real algebra" "\<lambda>x. lmeasure"
5.74    by default
5.75 @@ -692,71 +668,80 @@
5.76  lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
5.77    unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
5.78
5.79 -lemma borel_vimage_algebra_eq:
5.80 -  "sigma_algebra.vimage_algebra
5.81 -         (borel :: ('a::ordered_euclidean_space) algebra) ({..<DIM('a)} \<rightarrow>\<^isub>E UNIV) p2e =
5.82 -  sigma (product_algebra (\<lambda>x. \<lparr> space = UNIV::real set, sets = range (\<lambda>a. {..<a}) \<rparr>) {..<DIM('a)} )"
5.83 -proof- note bor = borel_eq_lessThan
5.84 -  def F \<equiv> "product_algebra (\<lambda>x. \<lparr> space = UNIV::real set, sets = range (\<lambda>a. {..<a}) \<rparr>) {..<DIM('a)}"
5.85 -  def E \<equiv> "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
5.86 -  have *:"(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}) = space F" unfolding F_def by auto
5.87 -  show ?thesis unfolding F_def[symmetric] * bor
5.88 -  proof(rule vimage_algebra_sigma,unfold E_def[symmetric])
5.89 -    show "sets E \<subseteq> Pow (space E)" "p2e \<in> space F \<rightarrow> space E" unfolding E_def by auto
5.90 -  next fix A assume "A \<in> sets F"
5.91 -    hence A:"A \<in> (Pi\<^isub>E {..<DIM('a)}) ` ({..<DIM('a)} \<rightarrow> range lessThan)"
5.92 -      unfolding F_def product_algebra_def algebra.simps .
5.93 -    then guess B unfolding image_iff .. note B=this
5.94 -    hence "\<forall>x<DIM('a). B x \<in> range lessThan" by auto
5.95 -    hence "\<forall>x. \<exists>xa. x<DIM('a) \<longrightarrow> B x = {..<xa}" unfolding image_iff by auto
5.96 -    from choice[OF this] guess b .. note b=this
5.97 -    hence b':"\<forall>i<DIM('a). Sup (B i) = b i" using Sup_lessThan by auto
5.98 +lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
5.99 +  unfolding Pi_def by auto
5.100
5.101 -    show "A \<in> (\<lambda>X. p2e -` X \<inter> space F) ` sets E" unfolding image_iff B
5.102 -    proof(rule_tac x="{..< \<chi>\<chi> i. Sup (B i)}" in bexI)
5.103 -      show "Pi\<^isub>E {..<DIM('a)} B = p2e -` {..<(\<chi>\<chi> i. Sup (B i))::'a} \<inter> space F"
5.104 -        unfolding F_def E_def product_algebra_def algebra.simps
5.105 -      proof(rule,unfold subset_eq,rule_tac[!] ballI)
5.106 -        fix x assume "x \<in> Pi\<^isub>E {..<DIM('a)} B"
5.107 -        hence *:"\<forall>i<DIM('a). x i < b i" "\<forall>i\<ge>DIM('a). x i = undefined"
5.108 -          unfolding Pi_def extensional_def using b by auto
5.109 -        have "(p2e x::'a) < (\<chi>\<chi> i. Sup (B i))" unfolding less_prod_def eucl_less[of "p2e x"]
5.110 -          apply safe unfolding euclidean_lambda_beta b'[rule_format] p2e_def using * by auto
5.111 -        moreover have "x \<in> extensional {..<DIM('a)}"
5.112 -          using *(2) unfolding extensional_def by auto
5.113 -        ultimately show "x \<in> p2e -` {..<(\<chi>\<chi> i. Sup (B i)) ::'a} \<inter>
5.114 -          (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})" by auto
5.115 -      next fix x assume as:"x \<in> p2e -` {..<(\<chi>\<chi> i. Sup (B i))::'a} \<inter>
5.116 -          (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
5.117 -        hence "p2e x < ((\<chi>\<chi> i. Sup (B i))::'a)" by auto
5.118 -        hence "\<forall>i<DIM('a). x i \<in> B i" apply-apply(subst(asm) eucl_less)
5.119 -          unfolding p2e_def using b b' by auto
5.120 -        thus "x \<in> Pi\<^isub>E {..<DIM('a)} B" using as unfolding Pi_def extensional_def by auto
5.121 -      qed
5.122 -      show "{..<(\<chi>\<chi> i. Sup (B i))::'a} \<in> sets E" unfolding E_def algebra.simps by auto
5.123 -    qed
5.124 -  next fix A assume "A \<in> sets E"
5.125 -    then guess a unfolding E_def algebra.simps image_iff .. note a = this(2)
5.126 -    def B \<equiv> "\<lambda>i. {..<a \$\$ i}"
5.127 -    show "p2e -` A \<inter> space F \<in> sets F" unfolding F_def
5.128 -      unfolding product_algebra_def algebra.simps image_iff
5.129 -      apply(rule_tac x=B in bexI) apply rule unfolding subset_eq apply(rule_tac[1-2] ballI)
5.130 -    proof- show "B \<in> {..<DIM('a)} \<rightarrow> range lessThan" unfolding B_def by auto
5.131 -      fix x assume as:"x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
5.132 -      hence "p2e x \<in> A" by auto
5.133 -      hence "\<forall>i<DIM('a). x i \<in> B i" unfolding B_def a lessThan_iff
5.134 -        apply-apply(subst (asm) eucl_less) unfolding p2e_def by auto
5.135 -      thus "x \<in> Pi\<^isub>E {..<DIM('a)} B" using as unfolding Pi_def extensional_def by auto
5.136 -    next fix x assume x:"x \<in> Pi\<^isub>E {..<DIM('a)} B"
5.137 -      moreover have "p2e x \<in> A" unfolding a lessThan_iff p2e_def apply(subst eucl_less)
5.138 -        using x unfolding Pi_def extensional_def B_def by auto
5.139 -      ultimately show "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})" by auto
5.140 -    qed
5.141 -  qed
5.142 +lemma measurable_e2p_on_generator:
5.143 +  "e2p \<in> measurable \<lparr> space = UNIV::'a set, sets = range lessThan \<rparr>
5.144 +  (product_algebra
5.145 +    (\<lambda>x. \<lparr> space = UNIV::real set, sets = range lessThan \<rparr>)
5.146 +    {..<DIM('a::ordered_euclidean_space)})"
5.147 +  (is "e2p \<in> measurable ?E ?P")
5.148 +proof (unfold measurable_def, intro CollectI conjI ballI)
5.149 +  show "e2p \<in> space ?E \<rightarrow> space ?P" by (auto simp: e2p_def)
5.150 +  fix A assume "A \<in> sets ?P"
5.151 +  then obtain E where A: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. E i)"
5.152 +    and "E \<in> {..<DIM('a)} \<rightarrow> (range lessThan)"
5.153 +    by (auto elim!: product_algebraE)
5.154 +  then have "\<forall>i\<in>{..<DIM('a)}. \<exists>xs. E i = {..< xs}" by auto
5.155 +  from this[THEN bchoice] guess xs ..
5.156 +  then have A_eq: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< xs i})"
5.157 +    using A by auto
5.158 +  have "e2p -` A = {..< (\<chi>\<chi> i. xs i) :: 'a}"
5.159 +    using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def A_eq
5.160 +      euclidean_eq[where 'a='a] eucl_less[where 'a='a])
5.161 +  then show "e2p -` A \<inter> space ?E \<in> sets ?E" by simp
5.162  qed
5.163
5.164 +lemma measurable_p2e_on_generator:
5.165 +  "p2e \<in> measurable
5.166 +    (product_algebra
5.167 +      (\<lambda>x. \<lparr> space = UNIV::real set, sets = range lessThan \<rparr>)
5.168 +      {..<DIM('a::ordered_euclidean_space)})
5.169 +    \<lparr> space = UNIV::'a set, sets = range lessThan \<rparr>"
5.170 +  (is "p2e \<in> measurable ?P ?E")
5.171 +proof (unfold measurable_def, intro CollectI conjI ballI)
5.172 +  show "p2e \<in> space ?P \<rightarrow> space ?E" by simp
5.173 +  fix A assume "A \<in> sets ?E"
5.174 +  then obtain x where "A = {..<x}" by auto
5.175 +  then have "p2e -` A \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< x \$\$ i})"
5.176 +    using DIM_positive
5.177 +    by (auto simp: Pi_iff set_eq_iff p2e_def
5.178 +                   euclidean_eq[where 'a='a] eucl_less[where 'a='a])
5.179 +  then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto
5.180 +qed
5.181 +
5.182 +lemma borel_vimage_algebra_eq:
5.183 +  defines "F \<equiv> product_algebra (\<lambda>x. \<lparr> space = (UNIV::real set), sets = range lessThan \<rparr>) {..<DIM('a::ordered_euclidean_space)}"
5.184 +  shows "sigma_algebra.vimage_algebra (borel::'a::ordered_euclidean_space algebra) (space (sigma F)) p2e = sigma F"
5.185 +  unfolding borel_eq_lessThan
5.186 +proof (intro vimage_algebra_sigma)
5.187 +  let ?E = "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
5.188 +  show "bij_inv (space (sigma F)) (space (sigma ?E)) p2e e2p"
5.189 +    using bij_inv_p2e_e2p unfolding F_def by simp
5.190 +  show "sets F \<subseteq> Pow (space F)" "sets ?E \<subseteq> Pow (space ?E)" unfolding F_def
5.191 +    by (intro product_algebra_sets_into_space) auto
5.192 +  show "p2e \<in> measurable F ?E"
5.193 +    "e2p \<in> measurable ?E F"
5.194 +    unfolding F_def using measurable_p2e_on_generator measurable_e2p_on_generator by auto
5.195 +qed
5.196 +
5.197 +lemma product_borel_eq_vimage:
5.198 +  "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
5.199 +  sigma_algebra.vimage_algebra borel (extensional {..<DIM('a)})
5.200 +  (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
5.201 +  unfolding borel_vimage_algebra_eq[simplified]
5.202 +  unfolding borel_eq_lessThan
5.203 +  apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
5.204 +  unfolding lessThan_iff
5.205 +proof- fix i assume i:"i<DIM('a)"
5.206 +  show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
5.207 +    by(auto intro!:real_arch_lt isotoneI)
5.208 +qed auto
5.209 +
5.210  lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
5.211 -  apply(rule image_Int[THEN sym]) using bij_euclidean_component
5.212 +  apply(rule image_Int[THEN sym])
5.213 +  using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)]
5.214    unfolding bij_betw_def by auto
5.215
5.216  lemma Int_stable_cuboids: fixes x::"'a::ordered_euclidean_space"
5.217 @@ -775,18 +760,6 @@
5.218    unfolding Int_stable_def algebra.select_convs
5.219    apply safe unfolding inter_interval by auto
5.220
5.221 -lemma product_borel_eq_vimage:
5.222 -  "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
5.223 -  sigma_algebra.vimage_algebra borel (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})
5.224 -  (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
5.225 -  unfolding borel_vimage_algebra_eq unfolding borel_eq_lessThan
5.226 -  apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
5.227 -  unfolding lessThan_iff
5.228 -proof- fix i assume i:"i<DIM('a)"
5.229 -  show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
5.230 -    by(auto intro!:real_arch_lt isotoneI)
5.231 -qed auto
5.232 -
5.233  lemma inj_on_disjoint_family_on: assumes "disjoint_family_on A S" "inj f"
5.234    shows "disjoint_family_on (\<lambda>x. f ` A x) S"
5.235    unfolding disjoint_family_on_def
5.236 @@ -808,12 +781,12 @@
5.237    unfolding e2p_def by auto
5.238
5.239  lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
5.240 -  shows "e2p ` A = p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
5.241 +  shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
5.242  proof(rule set_eqI,rule)
5.243    fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
5.244 -  show "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
5.245 +  show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
5.246      apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
5.247 -next fix x assume "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
5.248 +next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
5.249    thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
5.250  qed
5.251
5.252 @@ -879,17 +852,15 @@
5.253        qed
5.254
5.255        show "disjoint_family (\<lambda>n. e2p ` A n)" apply(rule inj_on_disjoint_family_on)
5.256 -        using bij_euclidean_component using A(2) unfolding bij_betw_def by auto
5.257 +        using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)] using A(2) unfolding bij_betw_def by auto
5.258        show "(\<Union>n. e2p ` A n) \<in> sets (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
5.259          unfolding product_borel_eq_vimage borel.in_vimage_algebra
5.260        proof(rule bexI[OF _ A(3)],rule set_eqI,rule)
5.261          fix x assume x:"x \<in> (\<Union>n. e2p ` A n)" hence "p2e x \<in> (\<Union>i. A i)" by auto
5.262          moreover have "x \<in> extensional {..<DIM('a)}"
5.263            using x unfolding extensional_def e2p_def_raw by auto
5.264 -        ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter>
5.265 -          extensional {..<DIM('a)})" by auto
5.266 -      next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter>
5.267 -          extensional {..<DIM('a)})"
5.268 +        ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}" by auto
5.269 +      next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}"
5.270          hence "p2e x \<in> (\<Union>i. A i)" by auto
5.271          hence "\<exists>n. x \<in> e2p ` A n" apply safe apply(rule_tac x=i in exI)
5.272            unfolding image_iff apply(rule_tac x="p2e x" in bexI)
5.273 @@ -925,23 +896,20 @@
5.274    assumes f: "f \<in> borel_measurable borel"
5.275    shows "borel.positive_integral f =
5.276            borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)"
5.277 -proof- def U \<equiv> "(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}):: (nat \<Rightarrow> real) set"
5.278 +proof- def U \<equiv> "extensional {..<DIM('a)} :: (nat \<Rightarrow> real) set"
5.279    interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
5.280 -  have "\<And>x. \<exists>i::nat. x < real i" by (metis real_arch_lt)
5.281 -  hence "(\<lambda>n::nat. {..<real n}) \<up> UNIV" apply-apply(rule isotoneI) by auto
5.282 -  hence *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
5.283 +  have *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
5.284      = sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)})"
5.285 -    unfolding U_def apply-apply(subst borel_vimage_algebra_eq)
5.286 -    apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>x. \<lambda>n. {..<(\<chi>\<chi> i. real n)}", THEN sym])
5.287 -    unfolding borel_eq_lessThan[THEN sym] by auto
5.288 -  show ?thesis unfolding borel.positive_integral_vimage[unfolded space_borel,OF bij_p2e]
5.289 +    unfolding U_def product_borel_eq_vimage[symmetric] ..
5.290 +  show ?thesis
5.291 +    unfolding borel.positive_integral_vimage[unfolded space_borel, OF bij_inv_p2e_e2p[THEN bij_inv_bij_betw(1)]]
5.292      apply(subst fprod.positive_integral_cong_measure[THEN sym, of "\<lambda>A. lmeasure (p2e ` A)"])
5.293      unfolding U_def[symmetric] *[THEN sym] o_def
5.294    proof- fix A assume A:"A \<in> sets (sigma_algebra.vimage_algebra borel U (p2e ::_ \<Rightarrow> 'a))"
5.295      hence *:"A \<subseteq> extensional {..<DIM('a)}" unfolding U_def by auto
5.296 -    from A guess B unfolding borel.in_vimage_algebra U_def .. note B=this
5.297 -    have "(p2e ` A::'a set) \<in> sets borel" unfolding B apply(subst Int_left_commute)
5.298 -      apply(subst Int_absorb1) unfolding p2e_inv_extensional[of B,THEN sym] using B(1) by auto
5.299 +    from A guess B unfolding borel.in_vimage_algebra U_def ..
5.300 +    then have "(p2e ` A::'a set) \<in> sets borel"
5.301 +      by (simp add: p2e_inv_extensional[of B, symmetric])
5.302      from lmeasure_measure_eq_borel_prod[OF this] show "lmeasure (p2e ` A::'a set) =
5.303        finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} A"
5.304        unfolding e2p_p2e'[OF *] .
```
```     6.1 --- a/src/HOL/Probability/Positive_Extended_Real.thy	Thu Dec 09 08:46:04 2010 +0100
6.2 +++ b/src/HOL/Probability/Positive_Extended_Real.thy	Thu Dec 09 10:22:17 2010 +0100
6.3 @@ -260,6 +260,9 @@
6.4  qed
6.5  end
6.6
6.7 +lemma Real_minus_abs[simp]: "Real (- \<bar>x\<bar>) = 0"
6.8 +  by simp
6.9 +
6.10  lemma pextreal_plus_eq_\<omega>[simp]: "(a :: pextreal) + b = \<omega> \<longleftrightarrow> a = \<omega> \<or> b = \<omega>"
6.11    by (cases a, cases b) auto
6.12
```
```     7.1 --- a/src/HOL/Probability/Probability_Space.thy	Thu Dec 09 08:46:04 2010 +0100
7.2 +++ b/src/HOL/Probability/Probability_Space.thy	Thu Dec 09 10:22:17 2010 +0100
7.3 @@ -352,7 +352,7 @@
7.4    show "sigma_algebra (sigma (pair_algebra MX MY))" by default
7.5    have sa: "sigma_algebra M" by default
7.6    show "(\<lambda>x. (X x, Y x)) \<in> measurable M (sigma (pair_algebra MX MY))"
7.7 -    unfolding P.measurable_pair[OF sa] using assms by (simp add: comp_def)
7.8 +    unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def)
7.9  qed
7.10
7.11  lemma (in prob_space) distribution_order:
7.12 @@ -410,8 +410,9 @@
7.13        assume A: "range A \<subseteq> sets XY.P" and df: "disjoint_family A"
7.14        have "(\<Sum>\<^isub>\<infinity>n. \<mu> (?X (A n))) = \<mu> (\<Union>x. ?X (A x))"
7.15        proof (intro measure_countably_additive)
7.16 -        from assms have *: "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
7.17 -          by (intro XY.measurable_prod_sigma) (simp_all add: comp_def, default)
7.18 +        have "sigma_algebra M" by default
7.19 +        then have *: "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
7.20 +          using assms by (simp add: XY.measurable_pair comp_def)
7.21          show "range (\<lambda>n. ?X (A n)) \<subseteq> events"
7.22            using measurable_sets[OF *] A by auto
7.23          show "disjoint_family (\<lambda>n. ?X (A n))"
7.24 @@ -503,7 +504,7 @@
7.25    show "finite_sigma_algebra (sigma (pair_algebra MX MY))" by default
7.26    have sa: "sigma_algebra M" by default
7.27    show "(\<lambda>x. (X x, Y x)) \<in> measurable M (sigma (pair_algebra MX MY))"
7.28 -    unfolding P.measurable_pair[OF sa] using assms by (simp add: comp_def)
7.29 +    unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def)
7.30  qed
7.31
7.32  lemma (in prob_space) finite_random_variable_imp_sets:
7.33 @@ -640,7 +641,7 @@
7.34    proof
7.35      fix x assume "x \<in> space XY.P"
7.36      moreover have "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
7.37 -      using X Y by (subst XY.measurable_pair) (simp_all add: o_def, default)
7.38 +      using X Y by (intro XY.measurable_pair) (simp_all add: o_def, default)
7.39      ultimately have "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M \<in> sets M"
7.40        unfolding measurable_def by simp
7.41      then show "joint_distribution X Y {x} \<noteq> \<omega>"
7.42 @@ -1068,13 +1069,13 @@
7.43
7.44    show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
7.45    proof (intro ballI bexI)
7.46 -    show "(SUP i. g i) \<in> borel_measurable M'"
7.47 +    show "(\<lambda>x. SUP i. g i x) \<in> borel_measurable M'"
7.48        using g by (auto intro: M'.borel_measurable_simple_function)
7.49      fix x assume "x \<in> space M"
7.50      have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp
7.51 -    also have "\<dots> = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand
7.52 +    also have "\<dots> = (SUP i. g i (Y x))" unfolding SUPR_apply
7.53        using g `x \<in> space M` by simp
7.54 -    finally show "Z x = (SUP i. g i) (Y x)" .
7.55 +    finally show "Z x = (SUP i. g i (Y x))" .
7.56    qed
7.57  qed
7.58
```
```     8.1 --- a/src/HOL/Probability/Product_Measure.thy	Thu Dec 09 08:46:04 2010 +0100
8.2 +++ b/src/HOL/Probability/Product_Measure.thy	Thu Dec 09 10:22:17 2010 +0100
8.3 @@ -92,6 +92,12 @@
8.4    shows "a \<in> extensional (insert i I)"
8.5    using assms unfolding extensional_def by auto
8.6
8.7 +lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I x {i} y = restrict (x(i := y i)) (insert i I)"
8.8 +  unfolding merge_def by (auto simp: fun_eq_iff)
8.9 +
8.10 +lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
8.11 +  by auto
8.12 +
8.13  lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)"
8.14    by auto
8.15
8.16 @@ -107,6 +113,64 @@
8.17  lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
8.18    by (auto simp: Pi_def)
8.19
8.20 +lemma restrict_vimage:
8.21 +  assumes "I \<inter> J = {}"
8.22 +  shows "(\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I E J F)"
8.23 +  using assms by (auto simp: restrict_Pi_cancel)
8.24 +
8.25 +lemma merge_vimage:
8.26 +  assumes "I \<inter> J = {}"
8.27 +  shows "(\<lambda>(x,y). merge I x J y) -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
8.28 +  using assms by (auto simp: restrict_Pi_cancel)
8.29 +
8.30 +lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
8.31 +  by (auto simp: restrict_def intro!: ext)
8.32 +
8.33 +lemma merge_restrict[simp]:
8.34 +  "merge I (restrict x I) J y = merge I x J y"
8.35 +  "merge I x J (restrict y J) = merge I x J y"
8.36 +  unfolding merge_def by (auto intro!: ext)
8.37 +
8.38 +lemma merge_x_x_eq_restrict[simp]:
8.39 +  "merge I x J x = restrict x (I \<union> J)"
8.40 +  unfolding merge_def by (auto intro!: ext)
8.41 +
8.42 +lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
8.43 +  apply auto
8.44 +  apply (drule_tac x=x in Pi_mem)
8.45 +  apply (simp_all split: split_if_asm)
8.46 +  apply (drule_tac x=i in Pi_mem)
8.47 +  apply (auto dest!: Pi_mem)
8.48 +  done
8.49 +
8.50 +lemma Pi_UN:
8.51 +  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
8.52 +  assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
8.53 +  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
8.54 +proof (intro set_eqI iffI)
8.55 +  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
8.56 +  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
8.57 +  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
8.58 +  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
8.59 +    using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
8.60 +  have "f \<in> Pi I (A k)"
8.61 +  proof (intro Pi_I)
8.62 +    fix i assume "i \<in> I"
8.63 +    from mono[OF this, of "n i" k] k[OF this] n[OF this]
8.64 +    show "f i \<in> A k i" by auto
8.65 +  qed
8.66 +  then show "f \<in> (\<Union>n. Pi I (A n))" by auto
8.67 +qed auto
8.68 +
8.69 +lemma PiE_cong:
8.70 +  assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
8.71 +  shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
8.72 +  using assms by (auto intro!: Pi_cong)
8.73 +
8.74 +lemma restrict_upd[simp]:
8.75 +  "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
8.76 +  by (auto simp: fun_eq_iff)
8.77 +
8.78  section "Binary products"
8.79
8.80  definition
8.81 @@ -134,6 +198,14 @@
8.82    "space (pair_algebra A B) = space A \<times> space B"
8.83    by (simp add: pair_algebra_def)
8.84
8.85 +lemma sets_pair_algebra: "sets (pair_algebra N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)"
8.86 +  unfolding pair_algebra_def by auto
8.87 +
8.88 +lemma pair_algebra_sets_into_space:
8.89 +  assumes "sets M \<subseteq> Pow (space M)" "sets N \<subseteq> Pow (space N)"
8.90 +  shows "sets (pair_algebra M N) \<subseteq> Pow (space (pair_algebra M N))"
8.91 +  using assms by (auto simp: pair_algebra_def)
8.92 +
8.93  lemma pair_algebra_Int_snd:
8.94    assumes "sets S1 \<subseteq> Pow (space S1)"
8.95    shows "pair_algebra S1 (algebra.restricted_space S2 A) =
8.96 @@ -176,7 +248,7 @@
8.97    then show ?fst ?snd by auto
8.98  qed
8.99
8.100 -lemma (in pair_sigma_algebra) measurable_pair:
8.101 +lemma (in pair_sigma_algebra) measurable_pair_iff:
8.102    assumes "sigma_algebra M"
8.103    shows "f \<in> measurable M P \<longleftrightarrow>
8.104      (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
8.105 @@ -205,42 +277,11 @@
8.106    qed
8.107  qed
8.108
8.109 -lemma (in pair_sigma_algebra) measurable_prod_sigma:
8.110 +lemma (in pair_sigma_algebra) measurable_pair:
8.111    assumes "sigma_algebra M"
8.112 -  assumes 1: "(fst \<circ> f) \<in> measurable M M1" and 2: "(snd \<circ> f) \<in> measurable M M2"
8.113 +  assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
8.114    shows "f \<in> measurable M P"
8.115 -proof -
8.116 -  interpret M: sigma_algebra M by fact
8.117 -  from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space M1"
8.118 -     and q1: "\<forall>y\<in>sets M1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
8.119 -    by (auto simp add: measurable_def)
8.120 -  from 2 have fn2: "snd \<circ> f \<in> space M \<rightarrow> space M2"
8.121 -     and q2: "\<forall>y\<in>sets M2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
8.122 -    by (auto simp add: measurable_def)
8.123 -  show ?thesis
8.124 -  proof (rule M.measurable_sigma)
8.125 -    show "sets E \<subseteq> Pow (space E)"
8.126 -      using M1.space_closed M2.space_closed
8.127 -      by (auto simp add: sigma_algebra_iff pair_algebra_def)
8.128 -  next
8.129 -    show "f \<in> space M \<rightarrow> space E"
8.130 -      by (simp add: space_pair_algebra) (rule prod_final [OF fn1 fn2])
8.131 -  next
8.132 -    fix z
8.133 -    assume z: "z \<in> sets E"
8.134 -    thus "f -` z \<inter> space M \<in> sets M"
8.135 -    proof (auto simp add: pair_algebra_def vimage_Times)
8.136 -      fix x y
8.137 -      assume x: "x \<in> sets M1" and y: "y \<in> sets M2"
8.138 -      have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M =
8.139 -            ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
8.140 -        by blast
8.141 -      also have "...  \<in> sets M" using x y q1 q2
8.142 -        by blast
8.143 -      finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
8.144 -    qed
8.145 -  qed
8.146 -qed
8.147 +  unfolding measurable_pair_iff[OF assms(1)] using assms(2,3) by simp
8.148
8.149  lemma pair_algebraE:
8.150    assumes "X \<in> sets (pair_algebra M1 M2)"
8.151 @@ -726,11 +767,11 @@
8.152    then have F_borel: "\<And>i. F i \<in> borel_measurable P"
8.153      and F_mono: "\<And>i x. F i x \<le> F (Suc i) x"
8.154      and F_SUPR: "\<And>x. (SUP i. F i x) = f x"
8.155 -    unfolding isoton_def le_fun_def SUPR_fun_expand
8.156 +    unfolding isoton_fun_expand unfolding isoton_def le_fun_def
8.157      by (auto intro: borel_measurable_simple_function)
8.158    note sf = simple_function_cut[OF F(1)]
8.159 -  then have "(SUP i. ?C (F i)) \<in> borel_measurable M1"
8.160 -    using F(1) by (auto intro!: M1.borel_measurable_SUP)
8.161 +  then have "(\<lambda>x. SUP i. ?C (F i) x) \<in> borel_measurable M1"
8.162 +    using F(1) by auto
8.163    moreover
8.164    { fix x assume "x \<in> space M1"
8.165      have isotone: "(\<lambda> i y. F i (x, y)) \<up> (\<lambda>y. f (x, y))"
8.166 @@ -742,7 +783,7 @@
8.167        by (simp add: isoton_def) }
8.168    note SUPR_C = this
8.169    ultimately show "?C f \<in> borel_measurable M1"
8.170 -    unfolding SUPR_fun_expand by (simp cong: measurable_cong)
8.171 +    by (simp cong: measurable_cong)
8.172    have "positive_integral (\<lambda>x. SUP i. F i x) = (SUP i. positive_integral (F i))"
8.173      using F_borel F_mono
8.174      by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])
8.175 @@ -1003,10 +1044,25 @@
8.176  sublocale finite_product_sigma_algebra \<subseteq> sigma_algebra P
8.177    using product_algebra_into_space by (rule sigma_algebra_sigma)
8.178
8.179 +lemma product_algebraE:
8.180 +  assumes "A \<in> sets (product_algebra M I)"
8.181 +  obtains E where "A = Pi\<^isub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
8.182 +  using assms unfolding product_algebra_def by auto
8.183 +
8.184 +lemma product_algebraI[intro]:
8.185 +  assumes "E \<in> (\<Pi> i\<in>I. sets (M i))"
8.186 +  shows "Pi\<^isub>E I E \<in> sets (product_algebra M I)"
8.187 +  using assms unfolding product_algebra_def by auto
8.188 +
8.189  lemma space_product_algebra[simp]:
8.190    "space (product_algebra M I) = Pi\<^isub>E I (\<lambda>i. space (M i))"
8.191    unfolding product_algebra_def by simp
8.192
8.193 +lemma product_algebra_sets_into_space:
8.194 +  assumes "\<And>i. i\<in>I \<Longrightarrow> sets (M i) \<subseteq> Pow (space (M i))"
8.195 +  shows "sets (product_algebra M I) \<subseteq> Pow (space (product_algebra M I))"
8.196 +  using assms by (auto simp: product_algebra_def) blast
8.197 +
8.198  lemma (in finite_product_sigma_algebra) P_empty:
8.199    "I = {} \<Longrightarrow> P = \<lparr> space = {\<lambda>k. undefined}, sets = { {}, {\<lambda>k. undefined} }\<rparr>"
8.200    unfolding product_algebra_def by (simp add: sigma_def image_constant)
8.201 @@ -1015,34 +1071,122 @@
8.202    "\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
8.203    by (auto simp: product_algebra_def sets_sigma intro!: sigma_sets.Basic)
8.204
8.205 -lemma bij_betw_prod_fold:
8.206 -  assumes "i \<notin> I"
8.207 -  shows "bij_betw (\<lambda>x. (x(i:=undefined), x i)) (\<Pi>\<^isub>E j\<in>insert i I. space (M j)) ((\<Pi>\<^isub>E j\<in>I. space (M j)) \<times> space (M i))"
8.208 -    (is "bij_betw ?f ?P ?F")
8.209 -    using `i \<notin> I`
8.210 -proof (unfold bij_betw_def, intro conjI set_eqI iffI)
8.211 -  show "inj_on ?f ?P"
8.212 -  proof (safe intro!: inj_onI ext)
8.213 -    fix a b x assume "a(i:=undefined) = b(i:=undefined)" "a i = b i"
8.214 -    then show "a x = b x"
8.215 -      by (cases "x = i") (auto simp: fun_eq_iff split: split_if_asm)
8.216 +lemma (in product_sigma_algebra) bij_inv_restrict_merge:
8.217 +  assumes [simp]: "I \<inter> J = {}"
8.218 +  shows "bij_inv
8.219 +    (space (sigma (product_algebra M (I \<union> J))))
8.220 +    (space (sigma (pair_algebra (product_algebra M I) (product_algebra M J))))
8.221 +    (\<lambda>x. (restrict x I, restrict x J)) (\<lambda>(x, y). merge I x J y)"
8.222 +  by (rule bij_invI) (auto simp: space_pair_algebra extensional_restrict)
8.223 +
8.224 +lemma (in product_sigma_algebra) bij_inv_singleton:
8.225 +  "bij_inv (space (sigma (product_algebra M {i}))) (space (M i))
8.226 +    (\<lambda>x. x i) (\<lambda>x. (\<lambda>j\<in>{i}. x))"
8.227 +  by (rule bij_invI) (auto simp: restrict_def extensional_def fun_eq_iff)
8.228 +
8.229 +lemma (in product_sigma_algebra) bij_inv_restrict_insert:
8.230 +  assumes [simp]: "i \<notin> I"
8.231 +  shows "bij_inv
8.232 +    (space (sigma (product_algebra M (insert i I))))
8.233 +    (space (sigma (pair_algebra (product_algebra M I) (M i))))
8.234 +    (\<lambda>x. (restrict x I, x i)) (\<lambda>(x, y). x(i := y))"
8.235 +  by (rule bij_invI) (auto simp: space_pair_algebra extensional_restrict)
8.236 +
8.237 +lemma (in product_sigma_algebra) measurable_restrict_on_generating:
8.238 +  assumes [simp]: "I \<inter> J = {}"
8.239 +  shows "(\<lambda>x. (restrict x I, restrict x J)) \<in> measurable
8.240 +    (product_algebra M (I \<union> J))
8.241 +    (pair_algebra (product_algebra M I) (product_algebra M J))"
8.242 +    (is "?R \<in> measurable ?IJ ?P")
8.243 +proof (unfold measurable_def, intro CollectI conjI ballI)
8.244 +  show "?R \<in> space ?IJ \<rightarrow> space ?P" by (auto simp: space_pair_algebra)
8.245 +  { fix F E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))"
8.246 +    then have "Pi (I \<union> J) (merge I E J F) \<inter> (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i)) =
8.247 +        Pi\<^isub>E (I \<union> J) (merge I E J F)"
8.248 +      using M.sets_into_space by auto blast+ }
8.249 +  note this[simp]
8.250 +  show "\<And>A. A \<in> sets ?P \<Longrightarrow> ?R -` A \<inter> space ?IJ \<in> sets ?IJ"
8.251 +    by (force elim!: pair_algebraE product_algebraE
8.252 +              simp del: vimage_Int simp: restrict_vimage merge_vimage space_pair_algebra)
8.253 +  qed
8.254 +
8.255 +lemma (in product_sigma_algebra) measurable_merge_on_generating:
8.256 +  assumes [simp]: "I \<inter> J = {}"
8.257 +  shows "(\<lambda>(x, y). merge I x J y) \<in> measurable
8.258 +    (pair_algebra (product_algebra M I) (product_algebra M J))
8.259 +    (product_algebra M (I \<union> J))"
8.260 +    (is "?M \<in> measurable ?P ?IJ")
8.261 +proof (unfold measurable_def, intro CollectI conjI ballI)
8.262 +  show "?M \<in> space ?P \<rightarrow> space ?IJ" by (auto simp: space_pair_algebra)
8.263 +  { fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "E \<in> (\<Pi> i\<in>J. sets (M i))"
8.264 +    then have "Pi I E \<times> Pi J E \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) \<times> (\<Pi>\<^isub>E i\<in>J. space (M i)) =
8.265 +        Pi\<^isub>E I E \<times> Pi\<^isub>E J E"
8.266 +      using M.sets_into_space by auto blast+ }
8.267 +  note this[simp]
8.268 +  show "\<And>A. A \<in> sets ?IJ \<Longrightarrow> ?M -` A \<inter> space ?P \<in> sets ?P"
8.269 +    by (force elim!: pair_algebraE product_algebraE
8.270 +              simp del: vimage_Int simp: restrict_vimage merge_vimage space_pair_algebra)
8.271    qed
8.272 -next
8.273 -  fix X assume *: "X \<in> ?F" show "X \<in> ?f ` ?P"
8.274 -  proof (cases X)
8.275 -    case (Pair a b) with * `i \<notin> I` show ?thesis
8.276 -      by (auto intro!: image_eqI[where x="a (i := b)"] ext simp: extensional_def)
8.277 -  qed
8.278 -qed auto
8.279 +
8.280 +lemma (in product_sigma_algebra) measurable_singleton_on_generator:
8.281 +  "(\<lambda>x. \<lambda>j\<in>{i}. x) \<in> measurable (M i) (product_algebra M {i})"
8.282 +  (is "?f \<in> measurable _ ?P")
8.283 +proof (unfold measurable_def, intro CollectI conjI)
8.284 +  show "?f \<in> space (M i) \<rightarrow> space ?P" by auto
8.285 +  have "\<And>E. E i \<in> sets (M i) \<Longrightarrow> ?f -` Pi\<^isub>E {i} E \<inter> space (M i) = E i"
8.286 +    using M.sets_into_space by auto
8.287 +  then show "\<forall>A \<in> sets ?P. ?f -` A \<inter> space (M i) \<in> sets (M i)"
8.288 +    by (auto elim!: product_algebraE)
8.289 +qed
8.290 +
8.291 +lemma (in product_sigma_algebra) measurable_component_on_generator:
8.292 +  assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (product_algebra M I) (M i)"
8.293 +  (is "?f \<in> measurable ?P _")
8.294 +proof (unfold measurable_def, intro CollectI conjI ballI)
8.295 +  show "?f \<in> space ?P \<rightarrow> space (M i)" using `i \<in> I` by auto
8.296 +  fix A assume "A \<in> sets (M i)"
8.297 +  moreover then have "(\<lambda>x. x i) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) =
8.298 +      (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
8.299 +    using M.sets_into_space `i \<in> I`
8.300 +    by (fastsimp dest: Pi_mem split: split_if_asm)
8.301 +  ultimately show "?f -` A \<inter> space ?P \<in> sets ?P"
8.302 +    by (auto intro!: product_algebraI)
8.303 +qed
8.304
8.305 -lemma borel_measurable_product_component:
8.306 -  assumes "i \<in> I"
8.307 -  shows "(\<lambda>x. x i) \<in> borel_measurable (sigma (product_algebra (\<lambda>x. borel) I))"
8.308 -proof -
8.309 -  have *: "\<And>A. (\<lambda>x. x i) -` A \<inter> extensional I = (\<Pi>\<^isub>E j\<in>I. if j = i then A else UNIV)"
8.310 -    using `i \<in> I` by (auto elim!: PiE)
8.311 -  show ?thesis
8.312 -    by (auto simp: * measurable_def product_algebra_def)
8.313 +lemma (in product_sigma_algebra) measurable_restrict_singleton_on_generating:
8.314 +  assumes [simp]: "i \<notin> I"
8.315 +  shows "(\<lambda>x. (restrict x I, x i)) \<in> measurable
8.316 +    (product_algebra M (insert i I))
8.317 +    (pair_algebra (product_algebra M I) (M i))"
8.318 +    (is "?R \<in> measurable ?I ?P")
8.319 +proof (unfold measurable_def, intro CollectI conjI ballI)
8.320 +  show "?R \<in> space ?I \<rightarrow> space ?P" by (auto simp: space_pair_algebra)
8.321 +  { fix E F assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> sets (M i)"
8.322 +    then have "(\<lambda>x. (restrict x I, x i)) -` (Pi\<^isub>E I E \<times> F) \<inter> (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) =
8.323 +        Pi\<^isub>E (insert i I) (E(i := F))"
8.324 +      using M.sets_into_space using `i\<notin>I` by (auto simp: restrict_Pi_cancel) blast+ }
8.325 +  note this[simp]
8.326 +  show "\<And>A. A \<in> sets ?P \<Longrightarrow> ?R -` A \<inter> space ?I \<in> sets ?I"
8.327 +    by (force elim!: pair_algebraE product_algebraE
8.328 +              simp del: vimage_Int simp: space_pair_algebra)
8.329 +qed
8.330 +
8.331 +lemma (in product_sigma_algebra) measurable_merge_singleton_on_generating:
8.332 +  assumes [simp]: "i \<notin> I"
8.333 +  shows "(\<lambda>(x, y). x(i := y)) \<in> measurable
8.334 +    (pair_algebra (product_algebra M I) (M i))
8.335 +    (product_algebra M (insert i I))"
8.336 +    (is "?M \<in> measurable ?P ?IJ")
8.337 +proof (unfold measurable_def, intro CollectI conjI ballI)
8.338 +  show "?M \<in> space ?P \<rightarrow> space ?IJ" by (auto simp: space_pair_algebra)
8.339 +  { fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "E i \<in> sets (M i)"
8.340 +    then have "(\<lambda>(x, y). x(i := y)) -` Pi\<^isub>E (insert i I) E \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) \<times> space (M i) =
8.341 +        Pi\<^isub>E I E \<times> E i"
8.342 +      using M.sets_into_space by auto blast+ }
8.343 +  note this[simp]
8.344 +  show "\<And>A. A \<in> sets ?IJ \<Longrightarrow> ?M -` A \<inter> space ?P \<in> sets ?P"
8.345 +    by (force elim!: pair_algebraE product_algebraE
8.346 +              simp del: vimage_Int simp: space_pair_algebra)
8.347  qed
8.348
8.349  section "Generating set generates also product algebra"
8.350 @@ -1108,38 +1252,6 @@
8.351      by (simp add: pair_algebra_def sigma_def)
8.352  qed
8.353
8.354 -lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
8.355 -  apply auto
8.356 -  apply (drule_tac x=x in Pi_mem)
8.357 -  apply (simp_all split: split_if_asm)
8.358 -  apply (drule_tac x=i in Pi_mem)
8.359 -  apply (auto dest!: Pi_mem)
8.360 -  done
8.361 -
8.362 -lemma Pi_UN:
8.363 -  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
8.364 -  assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
8.365 -  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
8.366 -proof (intro set_eqI iffI)
8.367 -  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
8.368 -  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
8.369 -  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
8.370 -  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
8.371 -    using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
8.372 -  have "f \<in> Pi I (A k)"
8.373 -  proof (intro Pi_I)
8.374 -    fix i assume "i \<in> I"
8.375 -    from mono[OF this, of "n i" k] k[OF this] n[OF this]
8.376 -    show "f i \<in> A k i" by auto
8.377 -  qed
8.378 -  then show "f \<in> (\<Union>n. Pi I (A n))" by auto
8.379 -qed auto
8.380 -
8.381 -lemma PiE_cong:
8.382 -  assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
8.383 -  shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
8.384 -  using assms by (auto intro!: Pi_cong)
8.385 -
8.386  lemma sigma_product_algebra_sigma_eq:
8.387    assumes "finite I"
8.388    assumes isotone: "\<And>i. i \<in> I \<Longrightarrow> (S i) \<up> (space (E i))"
8.389 @@ -1209,150 +1321,163 @@
8.390      by (simp add: product_algebra_def sigma_def)
8.391  qed
8.392
8.393 -lemma (in finite_product_sigma_algebra) pair_sigma_algebra_finite_product_space:
8.394 -  "sigma (pair_algebra P (M i)) = sigma (pair_algebra G (M i))"
8.395 -proof -
8.396 -  have "sigma (pair_algebra P (M i)) = sigma (pair_algebra P (sigma (M i)))" by simp
8.397 -  also have "\<dots> = sigma (pair_algebra G (M i))"
8.398 -  proof (rule pair_sigma_algebra_sigma)
8.399 -    show "(\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)) \<up> space G"
8.400 -      "(\<lambda>_. space (M i)) \<up> space (M i)"
8.401 -      by (simp_all add: isoton_const)
8.402 -    show "range (\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)) \<subseteq> sets G" "range (\<lambda>_. space (M i)) \<subseteq> sets (M i)"
8.403 -      by (auto intro!: image_eqI[where x="\<lambda>i\<in>I. space (M i)"] dest: Pi_mem
8.404 -               simp: product_algebra_def)
8.405 -    show "sets G \<subseteq> Pow (space G)" "sets (M i) \<subseteq> Pow (space (M i))"
8.406 -      using product_algebra_into_space M.sets_into_space by auto
8.407 -  qed
8.408 -  finally show ?thesis .
8.409 -qed
8.410 -
8.411 -lemma sets_pair_algebra: "sets (pair_algebra N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)"
8.412 -  unfolding pair_algebra_def by auto
8.413 -
8.414 -lemma (in finite_product_sigma_algebra) sigma_pair_algebra_sigma_eq:
8.415 +lemma (in product_sigma_algebra) sigma_pair_algebra_sigma_eq:
8.416    "sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))) =
8.417     sigma (pair_algebra (product_algebra M I) (product_algebra M J))"
8.418    using M.sets_into_space
8.419    by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)", of _ "\<lambda>_. \<Pi>\<^isub>E i\<in>J. space (M i)"])
8.420       (auto simp: isoton_const product_algebra_def, blast+)
8.421
8.422 +lemma (in product_sigma_algebra) sigma_pair_algebra_product_singleton:
8.423 +  "sigma (pair_algebra (sigma (product_algebra M I)) (M i)) =
8.424 +   sigma (pair_algebra (product_algebra M I) (M i))"
8.425 +  using M.sets_into_space apply (subst M.sigma_eq[symmetric])
8.426 +  by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)" _ "\<lambda>_. space (M i)"])
8.427 +     (auto simp: isoton_const product_algebra_def, blast+)
8.428 +
8.429 +lemma (in product_sigma_algebra) measurable_restrict:
8.430 +  assumes [simp]: "I \<inter> J = {}"
8.431 +  shows "(\<lambda>x. (restrict x I, restrict x J)) \<in> measurable
8.432 +    (sigma (product_algebra M (I \<union> J)))
8.433 +    (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))"
8.434 +  unfolding sigma_pair_algebra_sigma_eq using M.sets_into_space
8.435 +  by (intro measurable_sigma_sigma measurable_restrict_on_generating
8.436 +            pair_algebra_sets_into_space product_algebra_sets_into_space)
8.437 +     auto
8.438 +
8.439 +lemma (in product_sigma_algebra) measurable_merge:
8.440 +  assumes [simp]: "I \<inter> J = {}"
8.441 +  shows "(\<lambda>(x, y). merge I x J y) \<in> measurable
8.442 +    (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
8.443 +    (sigma (product_algebra M (I \<union> J)))"
8.444 +  unfolding sigma_pair_algebra_sigma_eq using M.sets_into_space
8.445 +  by (intro measurable_sigma_sigma measurable_merge_on_generating
8.446 +            pair_algebra_sets_into_space product_algebra_sets_into_space)
8.447 +     auto
8.448 +
8.449  lemma (in product_sigma_algebra) product_product_vimage_algebra:
8.450 -  assumes [simp]: "I \<inter> J = {}" and "finite I" "finite J"
8.451 +  assumes [simp]: "I \<inter> J = {}"
8.452    shows "sigma_algebra.vimage_algebra
8.453      (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
8.454 -    (space (product_algebra M (I \<union> J))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
8.455 +    (space (sigma (product_algebra M (I \<union> J)))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
8.456      sigma (product_algebra M (I \<union> J))"
8.457 -    (is "sigma_algebra.vimage_algebra _ (space ?IJ) ?f = sigma ?IJ")
8.458 -proof -
8.459 -  have "finite (I \<union> J)" using assms by auto
8.460 -  interpret I: finite_product_sigma_algebra M I by default fact
8.461 -  interpret J: finite_product_sigma_algebra M J by default fact
8.462 -  interpret IJ: finite_product_sigma_algebra M "I \<union> J" by default fact
8.463 -  interpret pair_sigma_algebra I.P J.P by default
8.464 +  unfolding sigma_pair_algebra_sigma_eq using sets_into_space
8.465 +  by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge]
8.466 +            pair_algebra_sets_into_space product_algebra_sets_into_space
8.467 +            measurable_merge_on_generating measurable_restrict_on_generating)
8.468 +     auto
8.469 +
8.470 +lemma (in product_sigma_algebra) pair_product_product_vimage_algebra:
8.471 +  assumes [simp]: "I \<inter> J = {}"
8.472 +  shows "sigma_algebra.vimage_algebra (sigma (product_algebra M (I \<union> J)))
8.473 +    (space (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))) (\<lambda>(x,y). merge I x J y) =
8.474 +    (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))"
8.475 +  unfolding sigma_pair_algebra_sigma_eq using sets_into_space
8.476 +  by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge[symmetric]]
8.477 +            pair_algebra_sets_into_space product_algebra_sets_into_space
8.478 +            measurable_merge_on_generating measurable_restrict_on_generating)
8.479 +     auto
8.480 +
8.481 +lemma (in product_sigma_algebra) pair_product_singleton_vimage_algebra:
8.482 +  assumes [simp]: "i \<notin> I"
8.483 +  shows "sigma_algebra.vimage_algebra (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
8.484 +    (space (sigma (product_algebra M (insert i I)))) (\<lambda>x. (restrict x I, x i)) =
8.485 +    (sigma (product_algebra M (insert i I)))"
8.486 +  unfolding sigma_pair_algebra_product_singleton using sets_into_space
8.487 +  by (intro vimage_algebra_sigma[OF bij_inv_restrict_insert]
8.488 +            pair_algebra_sets_into_space product_algebra_sets_into_space
8.489 +            measurable_merge_singleton_on_generating measurable_restrict_singleton_on_generating)
8.490 +      auto
8.491
8.492 -  show "vimage_algebra (space ?IJ) ?f = sigma ?IJ"
8.493 -    unfolding I.sigma_pair_algebra_sigma_eq
8.494 -  proof (rule vimage_algebra_sigma)
8.495 -    from M.sets_into_space
8.496 -    show "sets (pair_algebra I.G J.G) \<subseteq> Pow (space (pair_algebra I.G J.G))"
8.497 -      by (auto simp: sets_pair_algebra space_pair_algebra product_algebra_def) blast+
8.498 -    show "?f \<in> space IJ.G \<rightarrow> space (pair_algebra I.G J.G)"
8.499 -      by (auto simp: space_pair_algebra product_algebra_def)
8.500 -    let ?F = "\<lambda>A. ?f -` A \<inter> (space IJ.G)"
8.501 -    let ?s = "\<lambda>I. Pi\<^isub>E I ` (\<Pi> i\<in>I. sets (M i))"
8.502 -    { fix A assume "A \<in> sets IJ.G"
8.503 -      then obtain F where A: "A = Pi\<^isub>E (I \<union> J) F" "F \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))"
8.504 -        by (auto simp: product_algebra_def)
8.505 -      show "A \<in> ?F ` sets (pair_algebra I.G J.G)"
8.506 -          using A M.sets_into_space
8.507 -          by (auto simp: restrict_Pi_cancel product_algebra_def
8.508 -                   intro!: image_eqI[where x="Pi\<^isub>E I F \<times> Pi\<^isub>E J F"]) blast+ }
8.509 -    { fix A assume "A \<in> sets (pair_algebra I.G J.G)"
8.510 -      then obtain E F where A: "A = Pi\<^isub>E I E \<times> Pi\<^isub>E J F" "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))"
8.511 -        by (auto simp: product_algebra_def sets_pair_algebra)
8.512 -      then show "?F A \<in> sets IJ.G"
8.513 -          using A M.sets_into_space
8.514 -          by (auto simp: restrict_Pi_cancel product_algebra_def
8.515 -                   intro!: image_eqI[where x="merge I E J F"]) blast+ }
8.516 -  qed
8.517 -qed
8.518 +lemma (in product_sigma_algebra) singleton_vimage_algebra:
8.519 +  "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
8.520 +  using sets_into_space
8.521 +  by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
8.522 +             product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
8.523 +     auto
8.524 +
8.525 +lemma (in product_sigma_algebra) measurable_restrict_iff:
8.526 +  assumes IJ[simp]: "I \<inter> J = {}"
8.527 +  shows "f \<in> measurable (sigma (pair_algebra
8.528 +      (sigma (product_algebra M I)) (sigma (product_algebra M J)))) M' \<longleftrightarrow>
8.529 +    (\<lambda>x. f (restrict x I, restrict x J)) \<in> measurable (sigma (product_algebra M (I \<union> J))) M'"
8.530 +  using M.sets_into_space
8.531 +  apply (subst pair_product_product_vimage_algebra[OF IJ, symmetric])
8.532 +  apply (subst sigma_pair_algebra_sigma_eq)
8.533 +  apply (subst sigma_algebra.measurable_vimage_iff_inv[OF _
8.534 +      bij_inv_restrict_merge[symmetric]])
8.535 +  apply (intro sigma_algebra_sigma product_algebra_sets_into_space)
8.536 +  by auto
8.537
8.538 -lemma (in finite_product_sigma_algebra) sigma_pair_algebra_sigma_M_eq:
8.539 -  "sigma (pair_algebra P (M i)) = sigma (pair_algebra G (M i))"
8.540 +lemma (in product_sigma_algebra) measurable_merge_iff:
8.541 +  assumes IJ: "I \<inter> J = {}"
8.542 +  shows "f \<in> measurable (sigma (product_algebra M (I \<union> J))) M' \<longleftrightarrow>
8.543 +    (\<lambda>(x, y). f (merge I x J y)) \<in>
8.544 +      measurable (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J)))) M'"
8.545 +  unfolding measurable_restrict_iff[OF IJ]
8.546 +  by (rule measurable_cong) (auto intro!: arg_cong[where f=f] simp: extensional_restrict)
8.547 +
8.548 +lemma (in product_sigma_algebra) measurable_component:
8.549 +  assumes "i \<in> I" and f: "f \<in> measurable (M i) M'"
8.550 +  shows "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M I)) M'"
8.551 +    (is "?f \<in> measurable ?P M'")
8.552  proof -
8.553 -  have "sigma (pair_algebra P (sigma (M i))) = sigma (pair_algebra G (M i))"
8.554 -    using M.sets_into_space
8.555 -    by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)", of _ "\<lambda>_. space (M i)"])
8.556 -       (auto simp: isoton_const product_algebra_def, blast+)
8.557 -  then show ?thesis by simp
8.558 +  have "f \<circ> (\<lambda>x. x i) \<in> measurable ?P M'"
8.559 +    apply (rule measurable_comp[OF _ f])
8.560 +    using measurable_up_sigma[of "product_algebra M I" "M i"]
8.561 +    using measurable_component_on_generator[OF `i \<in> I`]
8.562 +    by auto
8.563 +  then show "?f \<in> measurable ?P M'" by (simp add: comp_def)
8.564  qed
8.565
8.566 -lemma (in product_sigma_algebra) product_singleton_vimage_algebra_eq:
8.567 -  assumes [simp]: "i \<notin> I" "finite I"
8.568 -  shows "sigma_algebra.vimage_algebra
8.569 -    (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
8.570 -    (space (product_algebra M (insert i I))) (\<lambda>x. ((\<lambda>i\<in>I. x i), x i)) =
8.571 -    sigma (product_algebra M (insert i I))"
8.572 -    (is "sigma_algebra.vimage_algebra _ (space ?I') ?f = sigma ?I'")
8.573 -proof -
8.574 -  have "finite (insert i I)" using assms by auto
8.575 -  interpret I: finite_product_sigma_algebra M I by default fact
8.576 -  interpret I': finite_product_sigma_algebra M "insert i I" by default fact
8.577 -  interpret pair_sigma_algebra I.P "M i" by default
8.578 -  show "vimage_algebra (space ?I') ?f = sigma ?I'"
8.579 -    unfolding I.sigma_pair_algebra_sigma_M_eq
8.580 -  proof (rule vimage_algebra_sigma)
8.581 -    from M.sets_into_space
8.582 -    show "sets (pair_algebra I.G (M i)) \<subseteq> Pow (space (pair_algebra I.G (M i)))"
8.583 -      by (auto simp: sets_pair_algebra space_pair_algebra product_algebra_def) blast
8.584 -    show "?f \<in> space I'.G \<rightarrow> space (pair_algebra I.G (M i))"
8.585 -      by (auto simp: space_pair_algebra product_algebra_def)
8.586 -    let ?F = "\<lambda>A. ?f -` A \<inter> (space I'.G)"
8.587 -    { fix A assume "A \<in> sets I'.G"
8.588 -      then obtain F where A: "A = Pi\<^isub>E (insert i I) F" "F \<in> (\<Pi> i\<in>I. sets (M i))" "F i \<in> sets (M i)"
8.589 -        by (auto simp: product_algebra_def)
8.590 -      show "A \<in> ?F ` sets (pair_algebra I.G (M i))"
8.591 -          using A M.sets_into_space
8.592 -          by (auto simp: restrict_Pi_cancel product_algebra_def
8.593 -                   intro!: image_eqI[where x="Pi\<^isub>E I F \<times> F i"]) blast+ }
8.594 -    { fix A assume "A \<in> sets (pair_algebra I.G (M i))"
8.595 -      then obtain E F where A: "A = Pi\<^isub>E I E \<times> F" "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> sets (M i)"
8.596 -        by (auto simp: product_algebra_def sets_pair_algebra)
8.597 -      then show "?F A \<in> sets I'.G"
8.598 -          using A M.sets_into_space
8.599 -          by (auto simp: restrict_Pi_cancel product_algebra_def
8.600 -                   intro!: image_eqI[where x="E(i:= F)"]) blast+ }
8.601 +lemma (in product_sigma_algebra) measurable_component_singleton:
8.602 +  "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
8.603 +    f \<in> measurable (M i) M'"
8.604 +  using sets_into_space
8.605 +  apply (subst singleton_vimage_algebra[symmetric])
8.606 +  apply (subst sigma_algebra.measurable_vimage_iff_inv[OF _ bij_inv_singleton[symmetric]])
8.607 +  by (auto intro!: sigma_algebra_sigma product_algebra_sets_into_space)
8.608 +
8.609 +lemma (in product_sigma_algebra) measurable_component_iff:
8.610 +  assumes "i \<in> I" and not_empty: "\<forall>i\<in>I. space (M i) \<noteq> {}"
8.611 +  shows "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M I)) M' \<longleftrightarrow>
8.612 +    f \<in> measurable (M i) M'"
8.613 +    (is "?f \<in> measurable ?P M' \<longleftrightarrow> _")
8.614 +proof
8.615 +  assume "f \<in> measurable (M i) M'" then show "?f \<in> measurable ?P M'"
8.616 +    by (rule measurable_component[OF `i \<in> I`])
8.617 +next
8.618 +  assume f: "?f \<in> measurable ?P M'"
8.619 +  def t \<equiv> "\<lambda>i. SOME x. x \<in> space (M i)"
8.620 +  have t: "\<And>i. i\<in>I \<Longrightarrow> t i \<in> space (M i)"
8.621 +     unfolding t_def using not_empty by (rule_tac someI_ex) auto
8.622 +  have "?f \<circ> (\<lambda>x. (\<lambda>j\<in>I. if j = i then x else t j)) \<in> measurable (M i) M'"
8.623 +    (is "?f \<circ> ?t \<in> measurable _ _")
8.624 +  proof (rule measurable_comp[OF _ f])
8.625 +    have "?t \<in> measurable (M i) (product_algebra M I)"
8.626 +    proof (unfold measurable_def, intro CollectI conjI ballI)
8.627 +      from t show "?t \<in> space (M i) \<rightarrow> (space (product_algebra M I))" by auto
8.628 +    next
8.629 +      fix A assume A: "A \<in> sets (product_algebra M I)"
8.630 +      { fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))"
8.631 +        then have "?t -` Pi\<^isub>E I E \<inter> space (M i) = (if (\<forall>j\<in>I-{i}. t j \<in> E j) then E i else {})"
8.632 +          using `i \<in> I` sets_into_space by (auto dest: Pi_mem[where B=E]) }
8.633 +      note * = this
8.634 +      with A `i \<in> I` show "?t -` A \<inter> space (M i) \<in> sets (M i)"
8.635 +        by (auto elim!: product_algebraE simp del: vimage_Int)
8.636 +    qed
8.637 +    also have "\<dots> \<subseteq> measurable (M i) (sigma (product_algebra M I))"
8.638 +      using M.sets_into_space by (intro measurable_subset) (auto simp: product_algebra_def, blast)
8.639 +    finally show "?t \<in> measurable (M i) (sigma (product_algebra M I))" .
8.640    qed
8.641 +  then show "f \<in> measurable (M i) M'" unfolding comp_def using `i \<in> I` by simp
8.642  qed
8.643
8.644 -lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
8.645 -  by (auto simp: restrict_def intro!: ext)
8.646 -
8.647 -lemma bij_betw_restrict_I_i:
8.648 -  "i \<notin> I \<Longrightarrow> bij_betw (\<lambda>x. (restrict x I, x i))
8.649 -    (space (product_algebra M (insert i I)))
8.650 -    (space (pair_algebra (sigma (product_algebra M I)) (M i)))"
8.651 -  by (intro bij_betwI[where g="(\<lambda>(x,y). x(i:=y))"])
8.652 -     (auto simp: space_pair_algebra extensional_def intro!: ext)
8.653 -
8.654 -lemma (in product_sigma_algebra) product_singleton_vimage_algebra_inv_eq:
8.655 -  assumes [simp]: "i \<notin> I" "finite I"
8.656 -  shows "sigma_algebra.vimage_algebra
8.657 -    (sigma (product_algebra M (insert i I)))
8.658 -    (space (pair_algebra (sigma (product_algebra M I)) (M i))) (\<lambda>(x,y). x(i:=y)) =
8.659 -    sigma (pair_algebra (sigma (product_algebra M I)) (M i))"
8.660 -proof -
8.661 -  have "finite (insert i I)" using `finite I` by auto
8.662 -  interpret I: finite_product_sigma_algebra M I by default fact
8.663 -  interpret I': finite_product_sigma_algebra M "insert i I" by default fact
8.664 -  interpret pair_sigma_algebra I.P "M i" by default
8.665 -  show ?thesis
8.666 -    unfolding product_singleton_vimage_algebra_eq[OF assms, symmetric]
8.667 -    using bij_betw_restrict_I_i[OF `i \<notin> I`, of M]
8.668 -    by (rule vimage_vimage_inv[unfolded space_sigma])
8.669 -       (auto simp: space_pair_algebra product_algebra_def dest: extensional_restrict)
8.670 -qed
8.671 +lemma (in product_sigma_algebra) measurable_singleton:
8.672 +  shows "f \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
8.673 +    (\<lambda>x. f (\<lambda>j\<in>{i}. x)) \<in> measurable (M i) M'"
8.674 +  using sets_into_space unfolding measurable_component_singleton[symmetric]
8.675 +  by (auto intro!: measurable_cong arg_cong[where f=f] simp: fun_eq_iff extensional_def)
8.676
8.677  locale product_sigma_finite =
8.678    fixes M :: "'i \<Rightarrow> 'a algebra" and \<mu> :: "'i \<Rightarrow> 'a set \<Rightarrow> pextreal"
8.679 @@ -1427,9 +1552,10 @@
8.680    let ?h = "\<lambda>x. (restrict x I, x i)"
8.681    let ?\<nu> = "\<lambda>A. P.pair_measure (?h ` A)"
8.682    interpret I': measure_space "sigma (product_algebra M (insert i I))" ?\<nu>
8.683 -    unfolding product_singleton_vimage_algebra_eq[OF `i \<notin> I` `finite I`, symmetric]
8.684 -    using bij_betw_restrict_I_i[OF `i \<notin> I`, of M]
8.685 -    by (intro P.measure_space_isomorphic) auto
8.686 +    apply (subst pair_product_singleton_vimage_algebra[OF `i \<notin> I`, symmetric])
8.687 +    apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
8.688 +    unfolding sigma_pair_algebra_product_singleton
8.689 +    by (rule bij_inv_restrict_insert[OF `i \<notin> I`])
8.690    show ?case
8.691    proof (intro exI[of _ ?\<nu>] conjI ballI)
8.692      { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
8.693 @@ -1512,6 +1638,17 @@
8.694    "product_integral I \<equiv>
8.695      measure_space.integral (sigma (product_algebra M I)) (product_measure I)"
8.696
8.697 +abbreviation (in product_sigma_finite)
8.698 +  "product_integrable I \<equiv>
8.699 +    measure_space.integrable (sigma (product_algebra M I)) (product_measure I)"
8.700 +
8.701 +lemma (in product_sigma_finite) product_measure_empty[simp]:
8.702 +  "product_measure {} {\<lambda>x. undefined} = 1"
8.703 +proof -
8.704 +  interpret finite_product_sigma_finite M \<mu> "{}" by default auto
8.705 +  from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
8.706 +qed
8.707 +
8.708  lemma (in product_sigma_finite) positive_integral_empty:
8.709    "product_positive_integral {} f = f (\<lambda>k. undefined)"
8.710  proof -
8.711 @@ -1528,46 +1665,6 @@
8.712    qed
8.713  qed
8.714
8.715 -lemma merge_restrict[simp]:
8.716 -  "merge I (restrict x I) J y = merge I x J y"
8.717 -  "merge I x J (restrict y J) = merge I x J y"
8.718 -  unfolding merge_def by (auto intro!: ext)
8.719 -
8.720 -lemma merge_x_x_eq_restrict[simp]:
8.721 -  "merge I x J x = restrict x (I \<union> J)"
8.722 -  unfolding merge_def by (auto intro!: ext)
8.723 -
8.724 -lemma bij_betw_restrict_I_J:
8.725 -  "I \<inter> J = {} \<Longrightarrow> bij_betw (\<lambda>x. (restrict x I, restrict x J))
8.726 -    (space (product_algebra M (I \<union> J)))
8.727 -    (space (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))"
8.728 -  by (intro bij_betwI[where g="\<lambda>(x,y). merge I x J y"])
8.729 -     (auto dest: extensional_restrict simp: space_pair_algebra)
8.730 -
8.731 -lemma (in product_sigma_algebra) product_product_vimage_algebra_eq:
8.732 -  assumes [simp]: "I \<inter> J = {}" and "finite I" "finite J"
8.733 -  shows "sigma_algebra.vimage_algebra
8.734 -    (sigma (product_algebra M (I \<union> J)))
8.735 -    (space (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J)))))
8.736 -    (\<lambda>(x, y). merge I x J y) =
8.737 -    sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J)))"
8.738 -  (is "sigma_algebra.vimage_algebra ?IJ ?S ?m = ?P")
8.739 -proof -
8.740 -  interpret I: finite_product_sigma_algebra M I by default fact
8.741 -  interpret J: finite_product_sigma_algebra M J by default fact
8.742 -  have "finite (I \<union> J)" using assms by auto
8.743 -  interpret IJ: finite_product_sigma_algebra M "I \<union> J" by default fact
8.744 -  interpret P: pair_sigma_algebra I.P J.P by default
8.745 -
8.746 -  let ?g = "\<lambda>x. (restrict x I, restrict x J)"
8.747 -  let ?f = "\<lambda>(x, y). merge I x J y"
8.748 -  show "IJ.vimage_algebra (space P.P) ?f = P.P"
8.749 -    using bij_betw_restrict_I_J[OF `I \<inter> J = {}`]
8.750 -    by (subst P.vimage_vimage_inv[of ?g "space IJ.G" ?f,
8.751 -                   unfolded product_product_vimage_algebra[OF assms]])
8.752 -       (auto simp: pair_algebra_def dest: extensional_restrict)
8.753 -qed
8.754 -
8.755  lemma (in product_sigma_finite) measure_fold:
8.756    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
8.757    assumes A: "A \<in> sets (sigma (product_algebra M (I \<union> J)))"
8.758 @@ -1598,9 +1695,10 @@
8.759        show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
8.760        show "?F \<up> space IJ.G " using F(2) by simp
8.761        show "measure_space IJ.P (\<lambda>A. P.pair_measure (?f ` A))"
8.762 -        unfolding product_product_vimage_algebra[OF IJ fin, symmetric]
8.763 -        using bij_betw_restrict_I_J[OF IJ, of M]
8.764 -        by (auto intro!: P.measure_space_isomorphic)
8.765 +      apply (subst product_product_vimage_algebra[OF IJ, symmetric])
8.766 +      apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
8.767 +      unfolding sigma_pair_algebra_sigma_eq
8.768 +      by (rule bij_inv_restrict_merge[OF `I \<inter> J = {}`])
8.769        show "measure_space IJ.P IJ.measure" by fact
8.770      next
8.771        fix A assume "A \<in> sets IJ.G"
8.772 @@ -1640,14 +1738,16 @@
8.773    interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
8.774    let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
8.775    have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
8.776 -    by (subst product_product_vimage_algebra_eq[OF IJ fin, symmetric])
8.777 -       (auto simp: space_pair_algebra intro!: IJ.measurable_vimage f)
8.778 +    unfolding case_prod_distrib measurable_merge_iff[OF IJ, symmetric] using f .
8.779 +  have bij: "bij_betw ?f (space IJ.P) (space P.P)"
8.780 +    unfolding sigma_pair_algebra_sigma_eq
8.781 +    by (intro bij_inv_bij_betw) (rule bij_inv_restrict_merge[OF IJ])
8.782    have "IJ.positive_integral f =  IJ.positive_integral (\<lambda>x. f (restrict x (I \<union> J)))"
8.783      by (auto intro!: IJ.positive_integral_cong arg_cong[where f=f] dest!: extensional_restrict)
8.784    also have "\<dots> = I.positive_integral (\<lambda>x. J.positive_integral (\<lambda>y. f (merge I x J y)))"
8.785      unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
8.786 -    unfolding P.positive_integral_vimage[unfolded space_sigma, OF bij_betw_restrict_I_J[OF IJ]]
8.787 -    unfolding product_product_vimage_algebra[OF IJ fin]
8.788 +    unfolding P.positive_integral_vimage[OF bij]
8.789 +    unfolding product_product_vimage_algebra[OF IJ]
8.790      apply simp
8.791      apply (rule IJ.positive_integral_cong_measure[symmetric])
8.792      apply (rule measure_fold)
8.793 @@ -1687,6 +1787,59 @@
8.794    qed simp
8.795  qed
8.796
8.797 +lemma (in product_sigma_finite) product_positive_integral_insert:
8.798 +  assumes [simp]: "finite I" "i \<notin> I"
8.799 +    and f: "f \<in> borel_measurable (sigma (product_algebra M (insert i I)))"
8.800 +  shows "product_positive_integral (insert i I) f
8.801 +    = product_positive_integral I (\<lambda>x. M.positive_integral i (\<lambda>y. f (x(i:=y))))"
8.802 +proof -
8.803 +  interpret I: finite_product_sigma_finite M \<mu> I by default auto
8.804 +  interpret i: finite_product_sigma_finite M \<mu> "{i}" by default auto
8.805 +  interpret P: pair_sigma_algebra I.P i.P ..
8.806 +  have IJ: "I \<inter> {i} = {}" by auto
8.807 +  show ?thesis
8.808 +    unfolding product_positive_integral_fold[OF IJ, simplified, OF f]
8.809 +  proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
8.810 +    fix x assume x: "x \<in> space I.P"
8.811 +    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
8.812 +    have f'_eq: "\<And>y. ?f y = f (x(i := y))"
8.813 +      using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
8.814 +    note fP = f[unfolded measurable_merge_iff[OF IJ, simplified]]
8.815 +    show "?f \<in> borel_measurable (M i)"
8.816 +      using P.measurable_pair_image_snd[OF fP x]
8.817 +      unfolding measurable_singleton f'_eq by (simp add: f'_eq)
8.818 +    show "M.positive_integral i ?f = M.positive_integral i (\<lambda>y. f (x(i := y)))"
8.819 +      unfolding f'_eq by simp
8.820 +  qed
8.821 +qed
8.822 +
8.823 +lemma (in product_sigma_finite) product_positive_integral_setprod:
8.824 +  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> pextreal"
8.825 +  assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
8.826 +  shows "product_positive_integral I (\<lambda>x. (\<Prod>i\<in>I. f i (x i))) =
8.827 +    (\<Prod>i\<in>I. M.positive_integral i (f i))"
8.828 +using assms proof induct
8.829 +  case empty
8.830 +  interpret finite_product_sigma_finite M \<mu> "{}" by default auto
8.831 +  then show ?case by simp
8.832 +next
8.833 +  case (insert i I)
8.834 +  note `finite I`[intro, simp]
8.835 +  interpret I: finite_product_sigma_finite M \<mu> I by default auto
8.836 +  have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
8.837 +    using insert by (auto intro!: setprod_cong)
8.838 +  have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
8.839 +    (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (sigma (product_algebra M J))"
8.840 +    using sets_into_space insert
8.841 +    by (intro sigma_algebra.borel_measurable_pextreal_setprod
8.842 +              sigma_algebra_sigma product_algebra_sets_into_space
8.843 +              measurable_component)
8.844 +       auto
8.845 +  show ?case
8.846 +    by (simp add: product_positive_integral_insert[OF insert(1,2) prod])
8.847 +       (simp add: insert I.positive_integral_cmult M.positive_integral_multc * prod subset_insertI)
8.848 +qed
8.849 +
8.850  lemma (in product_sigma_finite) product_integral_singleton:
8.851    assumes f: "f \<in> borel_measurable (M i)"
8.852    shows "product_integral {i} (\<lambda>x. f (x i)) = M.integral i f"
8.853 @@ -1700,45 +1853,6 @@
8.854      unfolding *[THEN product_positive_integral_singleton] ..
8.855  qed
8.856
8.857 -lemma (in product_sigma_finite) borel_measurable_merge_iff:
8.858 -  assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
8.859 -  shows "f \<in> measurable (sigma (pair_algebra
8.860 -      (sigma (product_algebra M I)) (sigma (product_algebra M J)))) M' \<longleftrightarrow>
8.861 -    (\<lambda>x. f (restrict x I, restrict x J)) \<in> measurable (sigma (product_algebra M (I \<union> J))) M'"
8.862 -proof -
8.863 -  interpret I: finite_product_sigma_finite M \<mu> I by default fact
8.864 -  interpret J: finite_product_sigma_finite M \<mu> J by default fact
8.865 -  have "finite (I \<union> J)" using fin by auto
8.866 -  interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
8.867 -  interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
8.868 -  let ?f = "\<lambda>x. (restrict x I, restrict x J)"
8.869 -  let ?S = "space (product_algebra M (I \<union> J))"
8.870 -  { fix p assume p: "p \<in> space (pair_algebra I.P J.P)"
8.871 -    have "?f (the_inv_into ?S ?f p) = p"
8.872 -    proof (intro f_the_inv_into_f[where f="?f"] inj_onI ext)
8.873 -      fix x y t assume "x \<in> ?S" "y \<in> ?S" "?f x = ?f y"
8.874 -      show "x t = y t"
8.875 -      proof cases
8.876 -        assume "t \<in> I \<union> J" then show ?thesis using `?f x = ?f y`
8.877 -          by (auto simp: restrict_def fun_eq_iff split: split_if_asm)
8.878 -      next
8.879 -        assume "t \<notin> I \<union> J" then show ?thesis
8.880 -          using `x \<in> ?S` `y \<in> ?S` by (auto simp: space_pair_algebra extensional_def)
8.881 -      qed
8.882 -    next
8.883 -      show "p \<in> ?f ` ?S" using p
8.884 -        by (intro image_eqI[of _ _ "merge I (fst p) J (snd p)"])
8.885 -           (auto simp: space_pair_algebra extensional_restrict)
8.886 -    qed }
8.887 -  note restrict = this
8.888 -  show ?thesis
8.889 -    apply (subst product_product_vimage_algebra[OF assms, symmetric])
8.890 -    apply (subst P.measurable_vimage_iff_inv)
8.891 -    using bij_betw_restrict_I_J[OF IJ, of M] apply simp
8.892 -    apply (rule measurable_cong)
8.893 -    by (auto simp del: space_product_algebra simp: restrict)
8.894 -qed
8.895 -
8.896  lemma (in product_sigma_finite) product_integral_fold:
8.897    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
8.898    and f: "measure_space.integrable (sigma (product_algebra M (I \<union> J))) (product_measure (I \<union> J)) f"
8.899 @@ -1761,7 +1875,7 @@
8.900    then have f'_borel:
8.901      "(\<lambda>x. Real (?f x)) \<in> borel_measurable P.P"
8.902      "(\<lambda>x. Real (- ?f x)) \<in> borel_measurable P.P"
8.903 -    unfolding borel_measurable_merge_iff[OF IJ fin]
8.904 +    unfolding measurable_restrict_iff[OF IJ]
8.905      by simp_all
8.906    have PI:
8.907      "P.positive_integral (\<lambda>x. Real (?f x)) = IJ.positive_integral (\<lambda>x. Real (f x))"
8.908 @@ -1771,7 +1885,7 @@
8.909      by simp_all
8.910    have "P.integrable ?f" using `IJ.integrable f`
8.911      unfolding P.integrable_def IJ.integrable_def
8.912 -    unfolding borel_measurable_merge_iff[OF IJ fin]
8.913 +    unfolding measurable_restrict_iff[OF IJ]
8.914      using f_restrict PI by simp_all
8.915    show ?thesis
8.916      unfolding P.integrable_fst_measurable(2)[OF `P.integrable ?f`, simplified]
8.917 @@ -1779,6 +1893,84 @@
8.918      unfolding PI by simp
8.919  qed
8.920
8.921 +lemma (in product_sigma_finite) product_integral_insert:
8.922 +  assumes [simp]: "finite I" "i \<notin> I"
8.923 +    and f: "measure_space.integrable (sigma (product_algebra M (insert i I))) (product_measure (insert i I)) f"
8.924 +  shows "product_integral (insert i I) f
8.925 +    = product_integral I (\<lambda>x. M.integral i (\<lambda>y. f (x(i:=y))))"
8.926 +proof -
8.927 +  interpret I: finite_product_sigma_finite M \<mu> I by default auto
8.928 +  interpret I': finite_product_sigma_finite M \<mu> "insert i I" by default auto
8.929 +  interpret i: finite_product_sigma_finite M \<mu> "{i}" by default auto
8.930 +  interpret P: pair_sigma_algebra I.P i.P ..
8.931 +  have IJ: "I \<inter> {i} = {}" by auto
8.932 +  show ?thesis
8.933 +    unfolding product_integral_fold[OF IJ, simplified, OF f]
8.934 +  proof (rule I.integral_cong, subst product_integral_singleton)
8.935 +    fix x assume x: "x \<in> space I.P"
8.936 +    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
8.937 +    have f'_eq: "\<And>y. ?f y = f (x(i := y))"
8.938 +      using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
8.939 +    have "f \<in> borel_measurable I'.P" using f unfolding I'.integrable_def by auto
8.940 +    note fP = this[unfolded measurable_merge_iff[OF IJ, simplified]]
8.941 +    show "?f \<in> borel_measurable (M i)"
8.942 +      using P.measurable_pair_image_snd[OF fP x]
8.943 +      unfolding measurable_singleton f'_eq by (simp add: f'_eq)
8.944 +    show "M.integral i ?f = M.integral i (\<lambda>y. f (x(i := y)))"
8.945 +      unfolding f'_eq by simp
8.946 +  qed
8.947 +qed
8.948 +
8.949 +lemma (in product_sigma_finite) product_integrable_setprod:
8.950 +  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
8.951 +  assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> M.integrable i (f i)"
8.952 +  shows "product_integrable I (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "product_integrable I ?f")
8.953 +proof -
8.954 +  interpret finite_product_sigma_finite M \<mu> I by default fact
8.955 +  have f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
8.956 +    using integrable unfolding M.integrable_def by auto
8.957 +  then have borel: "?f \<in> borel_measurable P"
8.958 +    by (intro borel_measurable_setprod measurable_component) auto
8.959 +  moreover have "integrable (\<lambda>x. \<bar>\<Prod>i\<in>I. f i (x i)\<bar>)"
8.960 +  proof (unfold integrable_def, intro conjI)
8.961 +    show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
8.962 +      using borel by auto
8.963 +    have "positive_integral (\<lambda>x. Real (abs (?f x))) =
8.964 +      positive_integral (\<lambda>x. \<Prod>i\<in>I. Real (abs (f i (x i))))"
8.965 +      by (simp add: Real_setprod abs_setprod)
8.966 +    also have "\<dots> = (\<Prod>i\<in>I. M.positive_integral i (\<lambda>x. Real (abs (f i x))))"
8.967 +      using f by (subst product_positive_integral_setprod) auto
8.968 +    also have "\<dots> < \<omega>"
8.969 +      using integrable[THEN M.integrable_abs]
8.970 +      unfolding pextreal_less_\<omega> setprod_\<omega> M.integrable_def by simp
8.971 +    finally show "positive_integral (\<lambda>x. Real (abs (?f x))) \<noteq> \<omega>" by auto
8.972 +    show "positive_integral (\<lambda>x. Real (- abs (?f x))) \<noteq> \<omega>" by simp
8.973 +  qed
8.974 +  ultimately show ?thesis
8.975 +    by (rule integrable_abs_iff[THEN iffD1])
8.976 +qed
8.977 +
8.978 +lemma (in product_sigma_finite) product_integral_setprod:
8.979 +  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
8.980 +  assumes "finite I" "I \<noteq> {}" and integrable: "\<And>i. i \<in> I \<Longrightarrow> M.integrable i (f i)"
8.981 +  shows "product_integral I (\<lambda>x. (\<Prod>i\<in>I. f i (x i))) = (\<Prod>i\<in>I. M.integral i (f i))"
8.982 +using assms proof (induct rule: finite_ne_induct)
8.983 +  case (singleton i)
8.984 +  then show ?case by (simp add: product_integral_singleton integrable_def)
8.985 +next
8.986 +  case (insert i I)
8.987 +  then have iI: "finite (insert i I)" by auto
8.988 +  then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
8.989 +    product_integrable J (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
8.990 +    by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset)
8.991 +  interpret I: finite_product_sigma_finite M \<mu> I by default fact
8.992 +  have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
8.993 +    using `i \<notin> I` by (auto intro!: setprod_cong)
8.994 +  show ?case
8.995 +    unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
8.996 +    by (simp add: * insert integral_multc I.integral_cmult[OF prod] subset_insertI)
8.997 +qed
8.998 +
8.999  section "Products on finite spaces"
8.1000
8.1001  lemma sigma_sets_pair_algebra_finite:
```
```     9.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Thu Dec 09 08:46:04 2010 +0100
9.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Thu Dec 09 10:22:17 2010 +0100
9.3 @@ -323,9 +323,10 @@
9.4    { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
9.5      have "g \<in> G" unfolding G_def
9.6      proof safe
9.7 -      from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
9.8 +      from `f \<up> g` have [simp]: "g = (\<lambda>x. SUP i. f i x)"
9.9 +        unfolding isoton_def fun_eq_iff SUPR_apply by simp
9.10        have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
9.11 -      thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
9.12 +      thus "g \<in> borel_measurable M" by auto
9.13        fix A assume "A \<in> sets M"
9.14        hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
9.15          using f_borel by (auto intro!: borel_measurable_indicator)
9.16 @@ -1103,42 +1104,36 @@
9.17      unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
9.18  qed
9.19
9.20 -lemma the_inv_into_in:
9.21 -  assumes "inj_on f A" and x: "x \<in> f`A"
9.22 -  shows "the_inv_into A f x \<in> A"
9.23 -  using assms by (auto simp: the_inv_into_f_f)
9.24 -
9.25  lemma (in sigma_finite_measure) RN_deriv_vimage:
9.26    fixes f :: "'b \<Rightarrow> 'a"
9.27 -  assumes f: "bij_betw f S (space M)"
9.28 +  assumes f: "bij_inv S (space M) f g"
9.29    assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
9.30    shows "AE x.
9.31 -    sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) = RN_deriv \<nu> x"
9.32 +    sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (g x) = RN_deriv \<nu> x"
9.33  proof (rule RN_deriv_unique[OF \<nu>])
9.34    interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
9.35 -    using f by (rule sigma_finite_measure_isomorphic)
9.36 +    using f by (rule sigma_finite_measure_isomorphic[OF bij_inv_bij_betw(1)])
9.37    interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
9.38    have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
9.39 -    using f by (rule \<nu>.measure_space_isomorphic)
9.40 +    using f by (rule \<nu>.measure_space_isomorphic[OF bij_inv_bij_betw(1)])
9.41    { fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
9.42 -      using sets_into_space f[unfolded bij_betw_def]
9.43 +      using sets_into_space f[THEN bij_inv_bij_betw(1), unfolded bij_betw_def]
9.44        by (intro image_vimage_inter_eq[where T="space M"]) auto }
9.45    note A_f = this
9.46    then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
9.47      using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
9.48 -  show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x)) \<in> borel_measurable M"
9.49 +  show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x)) \<in> borel_measurable M"
9.50      using sf.RN_deriv(1)[OF \<nu>' ac]
9.51      unfolding measurable_vimage_iff_inv[OF f] comp_def .
9.52    fix A assume "A \<in> sets M"
9.53 -  then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (the_inv_into S f x) = (indicator A x :: pextreal)"
9.54 -    using f[unfolded bij_betw_def]
9.55 -    unfolding indicator_def by (auto simp: f_the_inv_into_f the_inv_into_in)
9.56 +  then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (g x) = (indicator A x :: pextreal)"
9.57 +    using f by (auto simp: bij_inv_def indicator_def)
9.58    have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
9.59      using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
9.60 -  also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
9.61 +  also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
9.62      unfolding positive_integral_vimage_inv[OF f]
9.63      by (simp add: * cong: positive_integral_cong)
9.64 -  finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
9.65 +  finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
9.66      unfolding A_f[OF `A \<in> sets M`] .
9.67  qed
9.68
```
```    10.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Dec 09 08:46:04 2010 +0100
10.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Dec 09 10:22:17 2010 +0100
10.3 @@ -806,13 +806,6 @@
10.4         (simp_all add: f_the_inv_into_f cong: measurable_cong)
10.5  qed
10.6
10.7 -lemma (in sigma_algebra) measurable_vimage_iff_inv:
10.8 -  fixes f :: "'b \<Rightarrow> 'a" assumes f: "bij_betw f S (space M)"
10.9 -  shows "g \<in> measurable (vimage_algebra S f) M' \<longleftrightarrow> (g \<circ> the_inv_into S f) \<in> measurable M M'"
10.10 -  unfolding measurable_vimage_iff[OF f]
10.11 -  using f[unfolded bij_betw_def]
10.12 -  by (auto intro!: measurable_cong simp add: the_inv_into_f_f)
10.13 -
10.14  lemma sigma_sets_vimage:
10.15    assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
10.16    shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
10.17 @@ -871,22 +864,6 @@
10.18    qed
10.19  qed
10.20
10.21 -lemma vimage_algebra_sigma:
10.22 -  assumes E: "sets E \<subseteq> Pow (space E)"
10.23 -    and f: "f \<in> space F \<rightarrow> space E"
10.24 -    and "\<And>A. A \<in> sets F \<Longrightarrow> A \<in> (\<lambda>X. f -` X \<inter> space F) ` sets E"
10.25 -    and "\<And>A. A \<in> sets E \<Longrightarrow> f -` A \<inter> space F \<in> sets F"
10.26 -  shows "sigma_algebra.vimage_algebra (sigma E) (space F) f = sigma F"
10.27 -proof -
10.28 -  interpret sigma_algebra "sigma E"
10.29 -    using assms by (intro sigma_algebra_sigma) auto
10.30 -  have eq: "sets F = (\<lambda>X. f -` X \<inter> space F) ` sets E"
10.31 -    using assms by auto
10.32 -  show "vimage_algebra (space F) f = sigma F"
10.33 -    unfolding vimage_algebra_def using assms
10.34 -    by (simp add: sigma_def eq sigma_sets_vimage)
10.35 -qed
10.36 -
10.37  section {* Conditional space *}
10.38
10.39  definition (in algebra)
10.40 @@ -1420,6 +1397,8 @@
10.41      using E by simp
10.42  qed
10.43
10.44 +subsection "Sigma algebras on finite sets"
10.45 +
10.46  locale finite_sigma_algebra = sigma_algebra +
10.47    assumes finite_space: "finite (space M)"
10.48    and sets_eq_Pow[simp]: "sets M = Pow (space M)"
10.49 @@ -1438,4 +1417,92 @@
10.50      by (auto simp: image_space_def)
10.51  qed
10.52
10.53 +subsection "Bijective functions with inverse"
10.54 +
10.55 +definition "bij_inv A B f g \<longleftrightarrow>
10.56 +  f \<in> A \<rightarrow> B \<and> g \<in> B \<rightarrow> A \<and> (\<forall>x\<in>A. g (f x) = x) \<and> (\<forall>x\<in>B. f (g x) = x)"
10.57 +
10.58 +lemma bij_inv_symmetric[sym]: "bij_inv A B f g \<Longrightarrow> bij_inv B A g f"
10.59 +  unfolding bij_inv_def by auto
10.60 +
10.61 +lemma bij_invI:
10.62 +  assumes "f \<in> A \<rightarrow> B" "g \<in> B \<rightarrow> A"
10.63 +  and "\<And>x. x \<in> A \<Longrightarrow> g (f x) = x"
10.64 +  and "\<And>x. x \<in> B \<Longrightarrow> f (g x) = x"
10.65 +  shows "bij_inv A B f g"
10.66 +  using assms unfolding bij_inv_def by auto
10.67 +
10.68 +lemma bij_invE:
10.69 +  assumes "bij_inv A B f g"
10.70 +    "\<lbrakk> f \<in> A \<rightarrow> B ; g \<in> B \<rightarrow> A ;
10.71 +        (\<And>x. x \<in> A \<Longrightarrow> g (f x) = x) ;
10.72 +        (\<And>x. x \<in> B \<Longrightarrow> f (g x) = x) \<rbrakk> \<Longrightarrow> P"
10.73 +  shows P
10.74 +  using assms unfolding bij_inv_def by auto
10.75 +
10.76 +lemma bij_inv_bij_betw:
10.77 +  assumes "bij_inv A B f g"
10.78 +  shows "bij_betw f A B" "bij_betw g B A"
10.79 +  using assms by (auto intro: bij_betwI elim!: bij_invE)
10.80 +
10.81 +lemma bij_inv_vimage_vimage:
10.82 +  assumes "bij_inv A B f e"
10.83 +  shows "f -` (e -` X \<inter> B) \<inter> A = X \<inter> A"
10.84 +  using assms by (auto elim!: bij_invE)
10.85 +
10.86 +lemma (in sigma_algebra) measurable_vimage_iff_inv:
10.87 +  fixes f :: "'b \<Rightarrow> 'a" assumes "bij_inv S (space M) f g"
10.88 +  shows "h \<in> measurable (vimage_algebra S f) M' \<longleftrightarrow> (\<lambda>x. h (g x)) \<in> measurable M M'"
10.89 +  unfolding measurable_vimage_iff[OF bij_inv_bij_betw(1), OF assms]
10.90 +proof (rule measurable_cong)
10.91 +  fix w assume "w \<in> space (vimage_algebra S f)"
10.92 +  then have "w \<in> S" by auto
10.93 +  then show "h w = ((\<lambda>x. h (g x)) \<circ> f) w"
10.94 +    using assms by (auto elim: bij_invE)
10.95 +qed
10.96 +
10.97 +lemma vimage_algebra_sigma:
10.98 +  assumes bi: "bij_inv (space (sigma F)) (space (sigma E)) f e"
10.99 +    and "sets E \<subseteq> Pow (space E)" and F: "sets F \<subseteq> Pow (space F)"
10.100 +    and "f \<in> measurable F E" "e \<in> measurable E F"
10.101 +  shows "sigma_algebra.vimage_algebra (sigma E) (space (sigma F)) f = sigma F"
10.102 +proof -
10.103 +  interpret sigma_algebra "sigma E"
10.104 +    using assms by (intro sigma_algebra_sigma) auto
10.105 +  have eq: "sets F = (\<lambda>X. f -` X \<inter> space F) ` sets E"
10.106 +  proof safe
10.107 +    fix X assume "X \<in> sets F"
10.108 +    then have "e -` X \<inter> space E \<in> sets E"
10.109 +      using `e \<in> measurable E F` unfolding measurable_def by auto
10.110 +    then show "X \<in>(\<lambda>Y. f -` Y \<inter> space F) ` sets E"
10.111 +      apply (rule rev_image_eqI)
10.112 +      unfolding bij_inv_vimage_vimage[OF bi[simplified]]
10.113 +      using F `X \<in> sets F` by auto
10.114 +  next
10.115 +    fix X assume "X \<in> sets E" then show "f -` X \<inter> space F \<in> sets F"
10.116 +      using `f \<in> measurable F E` unfolding measurable_def by auto
10.117 +  qed
10.118 +  show "vimage_algebra (space (sigma F)) f = sigma F"
10.119 +    unfolding vimage_algebra_def
10.120 +    using assms by (auto simp: bij_inv_def eq sigma_sets_vimage[symmetric] sigma_def)
10.121 +qed
10.122 +
10.123 +lemma measurable_sigma_sigma:
10.124 +  assumes M: "sets M \<subseteq> Pow (space M)" and N: "sets N \<subseteq> Pow (space N)"
10.125 +  shows "f \<in> measurable M N \<Longrightarrow> f \<in> measurable (sigma M) (sigma N)"
10.126 +  using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N]
10.127 +  using measurable_up_sigma[of M N] N by auto
10.128 +
10.129 +lemma bij_inv_the_inv_into:
10.130 +  assumes "bij_betw f A B" shows "bij_inv A B f (the_inv_into A f)"
10.131 +proof (rule bij_invI)
10.132 +  show "the_inv_into A f \<in> B \<rightarrow> A"
10.133 +    using bij_betw_the_inv_into[OF assms] by (rule bij_betw_imp_funcset)
10.134 +  show "f \<in> A \<rightarrow> B" using assms by (rule bij_betw_imp_funcset)
10.135 +  show "\<And>x. x \<in> A \<Longrightarrow> the_inv_into A f (f x) = x"
10.136 +    "\<And>x. x \<in> B \<Longrightarrow> f (the_inv_into A f x) = x"
10.137 +    using the_inv_into_f_f[of f A] f_the_inv_into_f[of f A]
10.138 +    using assms by (auto simp: bij_betw_def)
10.139 +qed
10.140 +
10.141  end
```