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
```