src/HOL/Probability/Binary_Product_Measure.thy

   by auto
 
 lemma rev_Pair_vimage_times[simp]: "(\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
   by auto
 
-section "Binary products"
+subsection "Binary products"
 
 definition pair_measure (infixr "\<Otimes>\<^sub>M" 80) where
   "A \<Otimes>\<^sub>M B = measure_of (space A \<times> space B)
       {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}
       (\<lambda>X. \<integral>\<^sup>+x. (\<integral>\<^sup>+y. indicator X (x,y) \<partial>B) \<partial>A)"

     apply (subst Q.AE_pair_iff)
     apply simp_all
     done
 qed
 
-section "Fubinis theorem"
+subsection "Fubinis theorem"
 
 lemma measurable_compose_Pair1:
   "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^sub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
   by simp
 

 lemma (in pair_sigma_finite) Fubini:
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
   shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M2) \<partial>M1)"
   unfolding positive_integral_snd[OF assms] M2.positive_integral_fst[OF assms] ..
 
-section {* Products on counting spaces, densities and distributions *}
+subsection {* Products on counting spaces, densities and distributions *}
 
 lemma sigma_sets_pair_measure_generator_finite:
   assumes "finite A" and "finite B"
   shows "sigma_sets (A \<times> B) { a \<times> b | a b. a \<subseteq> A \<and> b \<subseteq> B} = Pow (A \<times> B)"
   (is "sigma_sets ?prod ?sets = _")