src/HOL/Probability/Probability_Measure.thy

   also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
     using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
   finally show ?thesis .
 qed
 
+lemma distributed_integrable_var:
+  fixes X :: "'a \<Rightarrow> real"
+  shows "distributed M lborel X (\<lambda>x. ereal (f x)) \<Longrightarrow> integrable lborel (\<lambda>x. f x * x) \<Longrightarrow> integrable M X"
+  using distributed_integrable[of M lborel X f "\<lambda>x. x"] by simp
+
 lemma (in prob_space) distributed_variance:
   fixes f::"real \<Rightarrow> real"
   assumes D: "distributed M lborel X f"
   shows "variance X = (\<integral>x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)"
 proof (subst distributed_integral[OF D, symmetric])