merged
authorhoelzl
Thu Dec 09 10:22:17 2010 +0100 (2010-12-09)
changeset 41098ababba14c965
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