src/HOL/Probability/Information.thy
changeset 49999 dfb63b9b8908
parent 49825 bb5db3d1d6dd
child 50002 ce0d316b5b44
     1.1 --- a/src/HOL/Probability/Information.thy	Fri Nov 02 12:00:51 2012 +0100
     1.2 +++ b/src/HOL/Probability/Information.thy	Fri Nov 02 14:00:39 2012 +0100
     1.3 @@ -1128,8 +1128,8 @@
     1.4      using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
     1.5      apply (intro TP.AE_pair_measure)
     1.6      apply (auto simp: comp_def measurable_split_conv
     1.7 -                intro!: measurable_snd'' borel_measurable_ereal_eq borel_measurable_ereal
     1.8 -                        SP.borel_measurable_positive_integral_snd measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
     1.9 +                intro!: measurable_snd'' measurable_fst'' borel_measurable_ereal_eq borel_measurable_ereal
    1.10 +                        S.borel_measurable_positive_integral measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
    1.11                          measurable_Pair
    1.12                  dest: distributed_real_AE distributed_real_measurable)
    1.13      done
    1.14 @@ -1142,7 +1142,7 @@
    1.15             measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
    1.16             measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
    1.17             measurable_compose[OF _ Px[THEN distributed_real_measurable]]
    1.18 -           STP.borel_measurable_positive_integral_snd
    1.19 +           TP.borel_measurable_positive_integral
    1.20    have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
    1.21      apply (subst positive_integral_density)
    1.22      apply (rule distributed_borel_measurable[OF Pxyz])
    1.23 @@ -1418,8 +1418,8 @@
    1.24      using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
    1.25      apply (intro TP.AE_pair_measure)
    1.26      apply (auto simp: comp_def measurable_split_conv
    1.27 -                intro!: measurable_snd'' borel_measurable_ereal_eq borel_measurable_ereal
    1.28 -                        SP.borel_measurable_positive_integral_snd measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
    1.29 +                intro!: measurable_snd'' measurable_fst'' borel_measurable_ereal_eq borel_measurable_ereal
    1.30 +                        S.borel_measurable_positive_integral measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
    1.31                          measurable_Pair
    1.32                  dest: distributed_real_AE distributed_real_measurable)
    1.33      done
    1.34 @@ -1432,7 +1432,7 @@
    1.35             measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
    1.36             measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
    1.37             measurable_compose[OF _ Px[THEN distributed_real_measurable]]
    1.38 -           STP.borel_measurable_positive_integral_snd
    1.39 +           TP.borel_measurable_positive_integral
    1.40    have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
    1.41      apply (subst positive_integral_density)
    1.42      apply (rule distributed_borel_measurable[OF Pxyz])