diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Mon Jun 30 15:45:03 2014 +0200 +++ b/src/HOL/Probability/Probability_Measure.thy Mon Jun 30 15:45:21 2014 +0200 @@ -29,6 +29,9 @@ abbreviation (in prob_space) "expectation \ integral\<^sup>L M" abbreviation (in prob_space) "variance X \ integral\<^sup>L M (\x. (X x - expectation X)\<^sup>2)" +lemma (in prob_space) finite_measure [simp]: "finite_measure M" + by unfold_locales + lemma (in prob_space) prob_space_distr: assumes f: "f \ measurable M M'" shows "prob_space (distr M M' f)" proof (rule prob_spaceI) @@ -344,6 +347,10 @@ lemma (in prob_space) variance_positive: "0 \ variance (X::'a \ real)" by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE) +lemma (in prob_space) variance_mean_zero: + "expectation X = 0 \ variance X = expectation (\x. (X x)^2)" + by simp + locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2 sublocale pair_prob_space \ P: prob_space "M1 \\<^sub>M M2" @@ -988,7 +995,7 @@ and M_eq: "\a. emeasure M {x\space M. X x \ a} = ereal (g a)" shows "distributed M lborel X f" proof (rule distributedI_real) - show "sets lborel = sigma_sets (space lborel) (range atMost)" + show "sets (lborel::real measure) = sigma_sets (space lborel) (range atMost)" by (simp add: borel_eq_atMost) show "Int_stable (range atMost :: real set set)" by (auto simp: Int_stable_def)