src/HOL/Probability/Probability_Measure.thy

 abbreviation (in prob_space) "events \<equiv> sets M"
 abbreviation (in prob_space) "prob \<equiv> measure M"
 abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'"
 abbreviation (in prob_space) "expectation \<equiv> integral\<^sup>L M"
 abbreviation (in prob_space) "variance X \<equiv> integral\<^sup>L M (\<lambda>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 \<in> measurable M M'" shows "prob_space (distr M M' f)"
 proof (rule prob_spaceI)
   have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)

   by (simp add: field_simps prob_space power2_diff power2_eq_square[symmetric])
 
 lemma (in prob_space) variance_positive: "0 \<le> variance (X::'a \<Rightarrow> real)"
   by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE)
 
+lemma (in prob_space) variance_mean_zero:
+  "expectation X = 0 \<Longrightarrow> variance X = expectation (\<lambda>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 \<subseteq> P: prob_space "M1 \<Otimes>\<^sub>M M2"
 proof
   show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) = 1"

     and [measurable]: "f \<in> borel_measurable borel" and f[simp]: "AE x in lborel. 0 \<le> f x"
     and g_eq: "\<And>a. (\<integral>\<^sup>+x. f x * indicator {..a} x \<partial>lborel)  = ereal (g a)"
     and M_eq: "\<And>a. emeasure M {x\<in>space M. X x \<le> 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)
   have vimage_eq: "\<And>a. (X -` {..a} \<inter> space M) = {x\<in>space M. X x \<le> a}" by auto
   def A \<equiv> "\<lambda>i::nat. {.. real i}"