src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy

     integral\<^sup>N (density M f) g' = (\<integral>\<^sup>+ x. f x * g' x \<partial>M)"
   by (subst (1 2) nn_integral_max_0[symmetric])
      (auto intro!: nn_integral_cong_AE
            simp: measurable_If max_def ereal_zero_le_0_iff nn_integral_density')
 
+lemma density_distr:
+  assumes [measurable]: "f \<in> borel_measurable N" "X \<in> measurable M N"
+  shows "density (distr M N X) f = distr (density M (\<lambda>x. f (X x))) N X"
+  by (intro measure_eqI)
+     (auto simp add: emeasure_density nn_integral_distr emeasure_distr
+           split: split_indicator intro!: nn_integral_cong)
+
 lemma emeasure_restricted:
   assumes S: "S \<in> sets M" and X: "X \<in> sets M"
   shows "emeasure (density M (indicator S)) X = emeasure M (S \<inter> X)"
 proof -
   have "emeasure (density M (indicator S)) X = (\<integral>\<^sup>+x. indicator S x * indicator X x \<partial>M)"