src/HOL/Probability/Bochner_Integration.thy

   fixes f :: "'a \<Rightarrow> real"
   shows "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x \<le> g x) \<Longrightarrow> 
     integral\<^sup>L M f \<le> integral\<^sup>L M g"
   by (intro integral_mono_AE) auto
 
-section {* Measure spaces with an associated density *}
+subsection {* Measure spaces with an associated density *}
 
 lemma integrable_density:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
   assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
     and nn: "AE x in M. 0 \<le> g x"

   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   shows "f \<in> borel_measurable N \<Longrightarrow> g \<in> measurable M N \<Longrightarrow>
     has_bochner_integral M (\<lambda>x. f (g x)) x \<Longrightarrow> has_bochner_integral (distr M N g) f x"
   by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
 
-section {* Lebesgue integration on @{const count_space} *}
+subsection {* Lebesgue integration on @{const count_space} *}
 
 lemma integrable_count_space:
   fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
   shows "finite X \<Longrightarrow> integrable (count_space X) f"
   by (auto simp: positive_integral_count_space integrable_iff_bounded)

 
 lemma lebesgue_integral_count_space_finite: "finite A \<Longrightarrow> (\<integral>x. f x \<partial>count_space A) = (\<Sum>a\<in>A. f a)"
   by (subst lebesgue_integral_count_space_finite_support)
      (auto intro!: setsum_mono_zero_cong_left)
 
-section {* Point measure *}
+subsection {* Point measure *}
 
 lemma lebesgue_integral_point_measure_finite:
   fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   shows "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow>
     integral\<^sup>L (point_measure A f) g = (\<Sum>a\<in>A. f a *\<^sub>R g a)"

   apply (subst density_ereal_max_0)
   apply (subst integrable_density)
   apply (auto simp: AE_count_space integrable_count_space)
   done
 
-subsection {* Legacy lemmas for the real-valued Lebesgue integral\<^sup>L *}
+subsection {* Legacy lemmas for the real-valued Lebesgue integral *}
 
 lemma real_lebesgue_integral_def:
   assumes f: "integrable M f"
   shows "integral\<^sup>L M f = real (\<integral>\<^sup>+x. f x \<partial>M) - real (\<integral>\<^sup>+x. - f x \<partial>M)"
 proof -

   then show "integrable M f" "integral\<^sup>L M f = x"
     by (auto simp: _has_bochner_integral_iff)
 qed
 
 
-section "Lebesgue integration on countable spaces"
+subsection {* Lebesgue integration on countable spaces *}
 
 lemma integral_on_countable:
   fixes f :: "real \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   and bij: "bij_betw enum S (f ` space M)"