src/HOL/Probability/Independent_Family.thy
changeset 53015 a1119cf551e8
parent 50244 de72bbe42190
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -829,16 +829,16 @@
     1.4    assumes "I \<noteq> {}"
     1.5    assumes rv: "\<And>i. random_variable (M' i) (X i)"
     1.6    shows "indep_vars M' X I \<longleftrightarrow>
     1.7 -    distr M (\<Pi>\<^isub>M i\<in>I. M' i) (\<lambda>x. \<lambda>i\<in>I. X i x) = (\<Pi>\<^isub>M i\<in>I. distr M (M' i) (X i))"
     1.8 +    distr M (\<Pi>\<^sub>M i\<in>I. M' i) (\<lambda>x. \<lambda>i\<in>I. X i x) = (\<Pi>\<^sub>M i\<in>I. distr M (M' i) (X i))"
     1.9  proof -
    1.10 -  let ?P = "\<Pi>\<^isub>M i\<in>I. M' i"
    1.11 +  let ?P = "\<Pi>\<^sub>M i\<in>I. M' i"
    1.12    let ?X = "\<lambda>x. \<lambda>i\<in>I. X i x"
    1.13    let ?D = "distr M ?P ?X"
    1.14    have X: "random_variable ?P ?X" by (intro measurable_restrict rv)
    1.15    interpret D: prob_space ?D by (intro prob_space_distr X)
    1.16  
    1.17    let ?D' = "\<lambda>i. distr M (M' i) (X i)"
    1.18 -  let ?P' = "\<Pi>\<^isub>M i\<in>I. distr M (M' i) (X i)"
    1.19 +  let ?P' = "\<Pi>\<^sub>M i\<in>I. distr M (M' i) (X i)"
    1.20    interpret D': prob_space "?D' i" for i by (intro prob_space_distr rv)
    1.21    interpret P: product_prob_space ?D' I ..
    1.22      
    1.23 @@ -855,10 +855,10 @@
    1.24          by (simp add: sets_PiM space_PiM)
    1.25        show "sets ?P' = sigma_sets (space ?P) (prod_algebra I M')"
    1.26          by (simp add: sets_PiM space_PiM cong: prod_algebra_cong)
    1.27 -      let ?A = "\<lambda>i. \<Pi>\<^isub>E i\<in>I. space (M' i)"
    1.28 -      show "range ?A \<subseteq> prod_algebra I M'" "(\<Union>i. ?A i) = space (Pi\<^isub>M I M')"
    1.29 +      let ?A = "\<lambda>i. \<Pi>\<^sub>E i\<in>I. space (M' i)"
    1.30 +      show "range ?A \<subseteq> prod_algebra I M'" "(\<Union>i. ?A i) = space (Pi\<^sub>M I M')"
    1.31          by (auto simp: space_PiM intro!: space_in_prod_algebra cong: prod_algebra_cong)
    1.32 -      { fix i show "emeasure ?D (\<Pi>\<^isub>E i\<in>I. space (M' i)) \<noteq> \<infinity>" by auto }
    1.33 +      { fix i show "emeasure ?D (\<Pi>\<^sub>E i\<in>I. space (M' i)) \<noteq> \<infinity>" by auto }
    1.34      next
    1.35        fix E assume E: "E \<in> prod_algebra I M'"
    1.36        from prod_algebraE[OF E] guess J Y . note J = this
    1.37 @@ -896,7 +896,7 @@
    1.38        qed
    1.39        from bchoice[OF this] obtain Y where
    1.40          Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j -` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto
    1.41 -      let ?E = "prod_emb I M' J (Pi\<^isub>E J Y)"
    1.42 +      let ?E = "prod_emb I M' J (Pi\<^sub>E J Y)"
    1.43        from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M"
    1.44          using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
    1.45        then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)"
    1.46 @@ -946,18 +946,18 @@
    1.47  
    1.48  lemma (in prob_space) indep_var_distribution_eq:
    1.49    "indep_var S X T Y \<longleftrightarrow> random_variable S X \<and> random_variable T Y \<and>
    1.50 -    distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" (is "_ \<longleftrightarrow> _ \<and> _ \<and> ?S \<Otimes>\<^isub>M ?T = ?J")
    1.51 +    distr M S X \<Otimes>\<^sub>M distr M T Y = distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))" (is "_ \<longleftrightarrow> _ \<and> _ \<and> ?S \<Otimes>\<^sub>M ?T = ?J")
    1.52  proof safe
    1.53    assume "indep_var S X T Y"
    1.54    then show rvs: "random_variable S X" "random_variable T Y"
    1.55      by (blast dest: indep_var_rv1 indep_var_rv2)+
    1.56 -  then have XY: "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
    1.57 +  then have XY: "random_variable (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
    1.58      by (rule measurable_Pair)
    1.59  
    1.60    interpret X: prob_space ?S by (rule prob_space_distr) fact
    1.61    interpret Y: prob_space ?T by (rule prob_space_distr) fact
    1.62    interpret XY: pair_prob_space ?S ?T ..
    1.63 -  show "?S \<Otimes>\<^isub>M ?T = ?J"
    1.64 +  show "?S \<Otimes>\<^sub>M ?T = ?J"
    1.65    proof (rule pair_measure_eqI)
    1.66      show "sigma_finite_measure ?S" ..
    1.67      show "sigma_finite_measure ?T" ..
    1.68 @@ -973,7 +973,7 @@
    1.69    qed simp
    1.70  next
    1.71    assume rvs: "random_variable S X" "random_variable T Y"
    1.72 -  then have XY: "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
    1.73 +  then have XY: "random_variable (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
    1.74      by (rule measurable_Pair)
    1.75  
    1.76    let ?S = "distr M S X" and ?T = "distr M T Y"
    1.77 @@ -981,7 +981,7 @@
    1.78    interpret Y: prob_space ?T by (rule prob_space_distr) fact
    1.79    interpret XY: pair_prob_space ?S ?T ..
    1.80  
    1.81 -  assume "?S \<Otimes>\<^isub>M ?T = ?J"
    1.82 +  assume "?S \<Otimes>\<^sub>M ?T = ?J"
    1.83  
    1.84    { fix S and X
    1.85      have "Int_stable {X -` A \<inter> space M |A. A \<in> sets S}"
    1.86 @@ -1004,8 +1004,8 @@
    1.87        fix A B assume ab: "A \<in> sets S" "B \<in> sets T"
    1.88        then have "ereal (prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M))) = emeasure ?J (A \<times> B)"
    1.89          using XY by (auto simp add: emeasure_distr emeasure_eq_measure intro!: arg_cong[where f="prob"])
    1.90 -      also have "\<dots> = emeasure (?S \<Otimes>\<^isub>M ?T) (A \<times> B)"
    1.91 -        unfolding `?S \<Otimes>\<^isub>M ?T = ?J` ..
    1.92 +      also have "\<dots> = emeasure (?S \<Otimes>\<^sub>M ?T) (A \<times> B)"
    1.93 +        unfolding `?S \<Otimes>\<^sub>M ?T = ?J` ..
    1.94        also have "\<dots> = emeasure ?S A * emeasure ?T B"
    1.95          using ab by (simp add: Y.emeasure_pair_measure_Times)
    1.96        finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) =
    1.97 @@ -1019,7 +1019,7 @@
    1.98    assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
    1.99    assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"
   1.100    assumes indep: "indep_var S X T Y"
   1.101 -  shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
   1.102 +  shows "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
   1.103    using indep_var_distribution_eq[of S X T Y] indep
   1.104    by (intro distributed_joint_indep'[OF S T X Y]) auto
   1.105