src/HOL/Probability/Independent_Family.thy
changeset 57235 b0b9a10e4bf4
parent 56154 f0a927235162
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Jun 11 13:39:38 2014 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Thu Jun 12 15:47:36 2014 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:      HOL/Probability/Independent_Family.thy
     1.5      Author:     Johannes Hölzl, TU München
     1.6 +    Author:     Sudeep Kanav, TU München
     1.7  *)
     1.8  
     1.9  header {* Independent families of events, event sets, and random variables *}
    1.10 @@ -478,6 +479,107 @@
    1.11      by (simp cong: indep_sets_cong)
    1.12  qed
    1.13  
    1.14 +lemma (in prob_space) indep_vars_restrict:
    1.15 +  assumes ind: "indep_vars M' X I" and K: "\<And>j. j \<in> L \<Longrightarrow> K j \<subseteq> I" and J: "disjoint_family_on K L"
    1.16 +  shows "indep_vars (\<lambda>j. PiM (K j) M') (\<lambda>j \<omega>. restrict (\<lambda>i. X i \<omega>) (K j)) L"
    1.17 +  unfolding indep_vars_def
    1.18 +proof safe
    1.19 +  fix j assume "j \<in> L" then show "random_variable (Pi\<^sub>M (K j) M') (\<lambda>\<omega>. \<lambda>i\<in>K j. X i \<omega>)"
    1.20 +    using K ind by (auto simp: indep_vars_def intro!: measurable_restrict)
    1.21 +next
    1.22 +  have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable M (M' i)"
    1.23 +    using ind by (auto simp: indep_vars_def)
    1.24 +  let ?proj = "\<lambda>j S. {(\<lambda>\<omega>. \<lambda>i\<in>K j. X i \<omega>) -` A \<inter> space M |A. A \<in> S}"
    1.25 +  let ?UN = "\<lambda>j. sigma_sets (space M) (\<Union>i\<in>K j. { X i -` A \<inter> space M| A. A \<in> sets (M' i) })"
    1.26 +  show "indep_sets (\<lambda>i. sigma_sets (space M) (?proj i (sets (Pi\<^sub>M (K i) M')))) L"
    1.27 +  proof (rule indep_sets_mono_sets)
    1.28 +    fix j assume j: "j \<in> L"
    1.29 +    have "sigma_sets (space M) (?proj j (sets (Pi\<^sub>M (K j) M'))) = 
    1.30 +      sigma_sets (space M) (sigma_sets (space M) (?proj j (prod_algebra (K j) M')))"
    1.31 +      using j K X[THEN measurable_space] unfolding sets_PiM
    1.32 +      by (subst sigma_sets_vimage_commute) (auto simp add: Pi_iff)
    1.33 +    also have "\<dots> = sigma_sets (space M) (?proj j (prod_algebra (K j) M'))"
    1.34 +      by (rule sigma_sets_sigma_sets_eq) auto
    1.35 +    also have "\<dots> \<subseteq> ?UN j"
    1.36 +    proof (rule sigma_sets_mono, safe del: disjE elim!: prod_algebraE)
    1.37 +      fix J E assume J: "finite J" "J \<noteq> {} \<or> K j = {}"  "J \<subseteq> K j" and E: "\<forall>i. i \<in> J \<longrightarrow> E i \<in> sets (M' i)"
    1.38 +      show "(\<lambda>\<omega>. \<lambda>i\<in>K j. X i \<omega>) -` prod_emb (K j) M' J (Pi\<^sub>E J E) \<inter> space M \<in> ?UN j"
    1.39 +      proof cases
    1.40 +        assume "K j = {}" with J show ?thesis
    1.41 +          by (auto simp add: sigma_sets_empty_eq prod_emb_def)
    1.42 +      next
    1.43 +        assume "K j \<noteq> {}" with J have "J \<noteq> {}"
    1.44 +          by auto
    1.45 +        { interpret sigma_algebra "space M" "?UN j"
    1.46 +            by (rule sigma_algebra_sigma_sets) auto 
    1.47 +          have "\<And>A. (\<And>i. i \<in> J \<Longrightarrow> A i \<in> ?UN j) \<Longrightarrow> INTER J A \<in> ?UN j"
    1.48 +            using `finite J` `J \<noteq> {}` by (rule finite_INT) blast }
    1.49 +        note INT = this
    1.50 +
    1.51 +        from `J \<noteq> {}` J K E[rule_format, THEN sets.sets_into_space] j
    1.52 +        have "(\<lambda>\<omega>. \<lambda>i\<in>K j. X i \<omega>) -` prod_emb (K j) M' J (Pi\<^sub>E J E) \<inter> space M
    1.53 +          = (\<Inter>i\<in>J. X i -` E i \<inter> space M)"
    1.54 +          apply (subst prod_emb_PiE[OF _ ])
    1.55 +          apply auto []
    1.56 +          apply auto []
    1.57 +          apply (auto simp add: Pi_iff intro!: X[THEN measurable_space])
    1.58 +          apply (erule_tac x=i in ballE)
    1.59 +          apply auto
    1.60 +          done
    1.61 +        also have "\<dots> \<in> ?UN j"
    1.62 +          apply (rule INT)
    1.63 +          apply (rule sigma_sets.Basic)
    1.64 +          using `J \<subseteq> K j` E
    1.65 +          apply auto
    1.66 +          done
    1.67 +        finally show ?thesis .
    1.68 +      qed
    1.69 +    qed
    1.70 +    finally show "sigma_sets (space M) (?proj j (sets (Pi\<^sub>M (K j) M'))) \<subseteq> ?UN j" .
    1.71 +  next
    1.72 +    show "indep_sets ?UN L"
    1.73 +    proof (rule indep_sets_collect_sigma)
    1.74 +      show "indep_sets (\<lambda>i. {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) (\<Union>j\<in>L. K j)"
    1.75 +      proof (rule indep_sets_mono_index)
    1.76 +        show "indep_sets (\<lambda>i. {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
    1.77 +          using ind unfolding indep_vars_def2 by auto
    1.78 +        show "(\<Union>l\<in>L. K l) \<subseteq> I"
    1.79 +          using K by auto
    1.80 +      qed
    1.81 +    next
    1.82 +      fix l i assume "l \<in> L" "i \<in> K l"
    1.83 +      show "Int_stable {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
    1.84 +        apply (auto simp: Int_stable_def)
    1.85 +        apply (rule_tac x="A \<inter> Aa" in exI)
    1.86 +        apply auto
    1.87 +        done
    1.88 +    qed fact
    1.89 +  qed
    1.90 +qed
    1.91 +
    1.92 +lemma (in prob_space) indep_var_restrict:
    1.93 +  assumes ind: "indep_vars M' X I" and AB: "A \<inter> B = {}" "A \<subseteq> I" "B \<subseteq> I"
    1.94 +  shows "indep_var (PiM A M') (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) A) (PiM B M') (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) B)"
    1.95 +proof -
    1.96 +  have *:
    1.97 +    "case_bool (Pi\<^sub>M A M') (Pi\<^sub>M B M') = (\<lambda>b. PiM (case_bool A B b) M')"
    1.98 +    "case_bool (\<lambda>\<omega>. \<lambda>i\<in>A. X i \<omega>) (\<lambda>\<omega>. \<lambda>i\<in>B. X i \<omega>) = (\<lambda>b \<omega>. \<lambda>i\<in>case_bool A B b. X i \<omega>)"
    1.99 +    by (simp_all add: fun_eq_iff split: bool.split)
   1.100 +  show ?thesis
   1.101 +    unfolding indep_var_def * using AB
   1.102 +    by (intro indep_vars_restrict[OF ind]) (auto simp: disjoint_family_on_def split: bool.split)
   1.103 +qed
   1.104 +
   1.105 +lemma (in prob_space) indep_vars_subset:
   1.106 +  assumes "indep_vars M' X I" "J \<subseteq> I"
   1.107 +  shows "indep_vars M' X J"
   1.108 +  using assms unfolding indep_vars_def indep_sets_def
   1.109 +  by auto
   1.110 +
   1.111 +lemma (in prob_space) indep_vars_cong:
   1.112 +  "I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> X i = Y i) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> M' i = N' i) \<Longrightarrow> indep_vars M' X I \<longleftrightarrow> indep_vars N' Y J"
   1.113 +  unfolding indep_vars_def2 by (intro conj_cong indep_sets_cong) auto
   1.114 +
   1.115  definition (in prob_space) tail_events where
   1.116    "tail_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
   1.117  
   1.118 @@ -801,6 +903,69 @@
   1.119    qed
   1.120  qed
   1.121  
   1.122 +lemma (in prob_space) indep_var_compose:
   1.123 +  assumes "indep_var M1 X1 M2 X2" "Y1 \<in> measurable M1 N1" "Y2 \<in> measurable M2 N2"
   1.124 +  shows "indep_var N1 (Y1 \<circ> X1) N2 (Y2 \<circ> X2)"
   1.125 +proof -
   1.126 +  have "indep_vars (case_bool N1 N2) (\<lambda>b. case_bool Y1 Y2 b \<circ> case_bool X1 X2 b) UNIV"
   1.127 +    using assms
   1.128 +    by (intro indep_vars_compose[where M'="case_bool M1 M2"])
   1.129 +       (auto simp: indep_var_def split: bool.split)
   1.130 +  also have "(\<lambda>b. case_bool Y1 Y2 b \<circ> case_bool X1 X2 b) = case_bool (Y1 \<circ> X1) (Y2 \<circ> X2)"
   1.131 +    by (simp add: fun_eq_iff split: bool.split)
   1.132 +  finally show ?thesis
   1.133 +    unfolding indep_var_def .
   1.134 +qed
   1.135 +
   1.136 +lemma (in prob_space) indep_vars_Min:
   1.137 +  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   1.138 +  assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
   1.139 +  shows "indep_var borel (X i) borel (\<lambda>\<omega>. Min ((\<lambda>i. X i \<omega>)`I))"
   1.140 +proof -
   1.141 +  have "indep_var
   1.142 +    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
   1.143 +    borel ((\<lambda>f. Min (f`I)) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
   1.144 +    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] borel_measurable_Min) auto
   1.145 +  also have "((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i})) = X i"
   1.146 +    by auto
   1.147 +  also have "((\<lambda>f. Min (f`I)) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I)) = (\<lambda>\<omega>. Min ((\<lambda>i. X i \<omega>)`I))"
   1.148 +    by (auto cong: rev_conj_cong)
   1.149 +  finally show ?thesis
   1.150 +    unfolding indep_var_def .
   1.151 +qed
   1.152 +
   1.153 +lemma (in prob_space) indep_vars_setsum:
   1.154 +  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   1.155 +  assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
   1.156 +  shows "indep_var borel (X i) borel (\<lambda>\<omega>. \<Sum>i\<in>I. X i \<omega>)"
   1.157 +proof -
   1.158 +  have "indep_var 
   1.159 +    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
   1.160 +    borel ((\<lambda>f. \<Sum>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
   1.161 +    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] ) auto
   1.162 +  also have "((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i})) = X i"
   1.163 +    by auto
   1.164 +  also have "((\<lambda>f. \<Sum>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I)) = (\<lambda>\<omega>. \<Sum>i\<in>I. X i \<omega>)"
   1.165 +    by (auto cong: rev_conj_cong)
   1.166 +  finally show ?thesis .
   1.167 +qed
   1.168 +
   1.169 +lemma (in prob_space) indep_vars_setprod:
   1.170 +  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   1.171 +  assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
   1.172 +  shows "indep_var borel (X i) borel (\<lambda>\<omega>. \<Prod>i\<in>I. X i \<omega>)"
   1.173 +proof -
   1.174 +  have "indep_var 
   1.175 +    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
   1.176 +    borel ((\<lambda>f. \<Prod>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
   1.177 +    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] ) auto
   1.178 +  also have "((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i})) = X i"
   1.179 +    by auto
   1.180 +  also have "((\<lambda>f. \<Prod>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I)) = (\<lambda>\<omega>. \<Prod>i\<in>I. X i \<omega>)"
   1.181 +    by (auto cong: rev_conj_cong)
   1.182 +  finally show ?thesis .
   1.183 +qed
   1.184 +
   1.185  lemma (in prob_space) indep_varsD_finite:
   1.186    assumes X: "indep_vars M' X I"
   1.187    assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)"
   1.188 @@ -933,6 +1098,20 @@
   1.189    finally show ?thesis .
   1.190  qed
   1.191  
   1.192 +lemma (in prob_space) prob_indep_random_variable:
   1.193 +  assumes ind[simp]: "indep_var N X N Y"
   1.194 +  assumes [simp]: "A \<in> sets N" "B \<in> sets N"
   1.195 +  shows "\<P>(x in M. X x \<in> A \<and> Y x \<in> B) = \<P>(x in M. X x \<in> A) * \<P>(x in M. Y x \<in> B)"
   1.196 +proof-
   1.197 +  have  " \<P>(x in M. (X x)\<in>A \<and>  (Y x)\<in> B ) = prob ((\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M)" 
   1.198 +    by (auto intro!: arg_cong[where f= prob])
   1.199 +  also have "...=  prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"  
   1.200 +    by (auto intro!: indep_varD[where Ma=N and Mb=N])     
   1.201 +  also have "... = \<P>(x in M. X x \<in> A) * \<P>(x in M. Y x \<in> B)"
   1.202 +    by (auto intro!: arg_cong2[where f= "op *"] arg_cong[where f= prob])
   1.203 +  finally show ?thesis .
   1.204 +qed
   1.205 +
   1.206  lemma (in prob_space)
   1.207    assumes "indep_var S X T Y"
   1.208    shows indep_var_rv1: "random_variable S X"
   1.209 @@ -1023,4 +1202,115 @@
   1.210    using indep_var_distribution_eq[of S X T Y] indep
   1.211    by (intro distributed_joint_indep'[OF S T X Y]) auto
   1.212  
   1.213 +lemma (in prob_space) indep_vars_nn_integral:
   1.214 +  assumes I: "finite I" "indep_vars (\<lambda>_. borel) X I" "\<And>i \<omega>. i \<in> I \<Longrightarrow> 0 \<le> X i \<omega>"
   1.215 +  shows "(\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)"
   1.216 +proof cases
   1.217 +  assume "I \<noteq> {}"
   1.218 +  def Y \<equiv> "\<lambda>i \<omega>. if i \<in> I then X i \<omega> else 0"
   1.219 +  { fix i have "i \<in> I \<Longrightarrow> random_variable borel (X i)"
   1.220 +    using I(2) by (cases "i\<in>I") (auto simp: indep_vars_def) }
   1.221 +  note rv_X = this
   1.222 +
   1.223 +  { fix i have "random_variable borel (Y i)"
   1.224 +    using I(2) by (cases "i\<in>I") (auto simp: Y_def rv_X) }
   1.225 +  note rv_Y = this[measurable]
   1.226 +    
   1.227 +  interpret Y: prob_space "distr M borel (Y i)" for i
   1.228 +    using I(2) by (cases "i \<in> I") (auto intro!: prob_space_distr simp: Y_def indep_vars_def)
   1.229 +  interpret product_sigma_finite "\<lambda>i. distr M borel (Y i)"
   1.230 +    ..
   1.231 +  
   1.232 +  have indep_Y: "indep_vars (\<lambda>i. borel) Y I"
   1.233 +    by (rule indep_vars_cong[THEN iffD1, OF _ _ _ I(2)]) (auto simp: Y_def)
   1.234 +
   1.235 +  have "(\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (Y i \<omega>)) \<partial>M)"
   1.236 +    using I(3) by (auto intro!: nn_integral_cong setprod_cong simp add: Y_def max_def)
   1.237 +  also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (\<omega> i)) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))"
   1.238 +    by (subst nn_integral_distr) auto
   1.239 +  also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (\<omega> i)) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
   1.240 +    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] ..
   1.241 +  also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^sup>+\<omega>. max 0 \<omega> \<partial>distr M borel (Y i)))"
   1.242 +    by (rule product_nn_integral_setprod) (auto intro: `finite I`)
   1.243 +  also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)"
   1.244 +    by (intro setprod_cong nn_integral_cong)
   1.245 +       (auto simp: nn_integral_distr nn_integral_max_0 Y_def rv_X)
   1.246 +  finally show ?thesis .
   1.247 +qed (simp add: emeasure_space_1)
   1.248 +
   1.249 +lemma (in prob_space)
   1.250 +  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{real_normed_field, banach, second_countable_topology}"
   1.251 +  assumes I: "finite I" "indep_vars (\<lambda>_. borel) X I" "\<And>i. i \<in> I \<Longrightarrow> integrable M (X i)"
   1.252 +  shows indep_vars_lebesgue_integral: "(\<integral>\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)" (is ?eq)
   1.253 +    and indep_vars_integrable: "integrable M (\<lambda>\<omega>. (\<Prod>i\<in>I. X i \<omega>))" (is ?int)
   1.254 +proof (induct rule: case_split)
   1.255 +  assume "I \<noteq> {}"
   1.256 +  def Y \<equiv> "\<lambda>i \<omega>. if i \<in> I then X i \<omega> else 0"
   1.257 +  { fix i have "i \<in> I \<Longrightarrow> random_variable borel (X i)"
   1.258 +    using I(2) by (cases "i\<in>I") (auto simp: indep_vars_def) }
   1.259 +  note rv_X = this[measurable]
   1.260 +
   1.261 +  { fix i have "random_variable borel (Y i)"
   1.262 +    using I(2) by (cases "i\<in>I") (auto simp: Y_def rv_X) }
   1.263 +  note rv_Y = this[measurable]
   1.264 +
   1.265 +  { fix i have "integrable M (Y i)"
   1.266 +    using I(3) by (cases "i\<in>I") (auto simp: Y_def) }
   1.267 +  note int_Y = this
   1.268 +    
   1.269 +  interpret Y: prob_space "distr M borel (Y i)" for i
   1.270 +    using I(2) by (cases "i \<in> I") (auto intro!: prob_space_distr simp: Y_def indep_vars_def)
   1.271 +  interpret product_sigma_finite "\<lambda>i. distr M borel (Y i)"
   1.272 +    ..
   1.273 +  
   1.274 +  have indep_Y: "indep_vars (\<lambda>i. borel) Y I"
   1.275 +    by (rule indep_vars_cong[THEN iffD1, OF _ _ _ I(2)]) (auto simp: Y_def)
   1.276 +
   1.277 +  have "(\<integral>\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<omega>. (\<Prod>i\<in>I. Y i \<omega>) \<partial>M)"
   1.278 +    using I(3) by (simp add: Y_def)
   1.279 +  also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))"
   1.280 +    by (subst integral_distr) auto
   1.281 +  also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
   1.282 +    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] ..
   1.283 +  also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<omega>. \<omega> \<partial>distr M borel (Y i)))"
   1.284 +    by (rule product_integral_setprod) (auto intro: `finite I` simp: integrable_distr_eq int_Y)
   1.285 +  also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)"
   1.286 +    by (intro setprod_cong integral_cong)
   1.287 +       (auto simp: integral_distr Y_def rv_X)
   1.288 +  finally show ?eq .
   1.289 +
   1.290 +  have "integrable (distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x)) (\<lambda>\<omega>. (\<Prod>i\<in>I. \<omega> i))"
   1.291 +    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y]
   1.292 +    by (intro product_integrable_setprod[OF `finite I`])
   1.293 +       (simp add: integrable_distr_eq int_Y)
   1.294 +  then show ?int
   1.295 +    by (simp add: integrable_distr_eq Y_def)
   1.296 +qed (simp_all add: prob_space)
   1.297 +
   1.298 +lemma (in prob_space)
   1.299 +  fixes X1 X2 :: "'a \<Rightarrow> 'b::{real_normed_field, banach, second_countable_topology}"
   1.300 +  assumes "indep_var borel X1 borel X2" "integrable M X1" "integrable M X2"
   1.301 +  shows indep_var_lebesgue_integral: "(\<integral>\<omega>. X1 \<omega> * X2 \<omega> \<partial>M) = (\<integral>\<omega>. X1 \<omega> \<partial>M) * (\<integral>\<omega>. X2 \<omega> \<partial>M)" (is ?eq)
   1.302 +    and indep_var_integrable: "integrable M (\<lambda>\<omega>. X1 \<omega> * X2 \<omega>)" (is ?int)
   1.303 +unfolding indep_var_def
   1.304 +proof -
   1.305 +  have *: "(\<lambda>\<omega>. X1 \<omega> * X2 \<omega>) = (\<lambda>\<omega>. \<Prod>i\<in>UNIV. (case_bool X1 X2 i \<omega>))"
   1.306 +    by (simp add: UNIV_bool mult_commute)
   1.307 +  have **: "(\<lambda> _. borel) = case_bool borel borel"
   1.308 +    by (rule ext, metis (full_types) bool.simps(3) bool.simps(4))
   1.309 +  show ?eq
   1.310 +    apply (subst *)
   1.311 +    apply (subst indep_vars_lebesgue_integral)
   1.312 +    apply (auto)
   1.313 +    apply (subst **, subst indep_var_def [symmetric], rule assms)
   1.314 +    apply (simp split: bool.split add: assms)
   1.315 +    by (simp add: UNIV_bool mult_commute)
   1.316 +  show ?int
   1.317 +    apply (subst *)
   1.318 +    apply (rule indep_vars_integrable)
   1.319 +    apply auto
   1.320 +    apply (subst **, subst indep_var_def [symmetric], rule assms)
   1.321 +    by (simp split: bool.split add: assms)
   1.322 +qed
   1.323 +
   1.324  end