src/HOL/Analysis/Bochner_Integration.thy

   }
   ultimately have "AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0" by auto
   then show ?thesis using \<open>strict_mono r\<close> by auto
 qed
 
-subsection%important \<open>Restricted measure spaces\<close>
+subsection \<open>Restricted measure spaces\<close>
 
 lemma integrable_restrict_space:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
   shows "integrable (restrict_space M \<Omega>) f \<longleftrightarrow> integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"

   have "(\<integral> x. f x \<partial>M) = (\<integral> x. 0 \<partial>M)"
     by(rule integral_cong)(simp_all add: assms)
   thus ?thesis by simp
 qed
 
-subsection%important \<open>Measure spaces with an associated density\<close>
+subsection \<open>Measure spaces with an associated density\<close>
 
 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}" and g :: "'a \<Rightarrow> real"
   shows "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. 0 \<le> g x) \<Longrightarrow>
     has_bochner_integral M (\<lambda>x. g x *\<^sub>R f x) x \<Longrightarrow> has_bochner_integral (density M g) f x"
   by (simp add: has_bochner_integral_iff integrable_density integral_density)
 
-subsection%important \<open>Distributions\<close>
+subsection \<open>Distributions\<close>
 
 lemma integrable_distr_eq:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes [measurable]: "g \<in> measurable M N" "f \<in> borel_measurable N"
   shows "integrable (distr M N g) f \<longleftrightarrow> integrable M (\<lambda>x. f (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)
 
-subsection%important \<open>Lebesgue integration on \<^const>\<open>count_space\<close>\<close>
+subsection \<open>Lebesgue integration on \<^const>\<open>count_space\<close>\<close>
 
 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: nn_integral_count_space integrable_iff_bounded)

 lemma has_bochner_integral_count_space_nat:
   fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
   shows "has_bochner_integral (count_space UNIV) f x \<Longrightarrow> f sums x"
   unfolding has_bochner_integral_iff by (auto intro!: sums_integral_count_space_nat)
 
-subsection%important \<open>Point measure\<close>
+subsection \<open>Point measure\<close>
 
 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 (auto split: split_max simp: ennreal_neg)
   apply (subst integrable_density)
   apply (auto simp: AE_count_space integrable_count_space)
   done
 
-subsection%important \<open>Lebesgue integration on \<^const>\<open>null_measure\<close>\<close>
+subsection \<open>Lebesgue integration on \<^const>\<open>null_measure\<close>\<close>
 
 lemma has_bochner_integral_null_measure_iff[iff]:
   "has_bochner_integral (null_measure M) f 0 \<longleftrightarrow> f \<in> borel_measurable M"
   by (auto simp add: has_bochner_integral.simps simple_bochner_integral_def[abs_def]
            intro!: exI[of _ "\<lambda>n x. 0"] simple_bochner_integrable.intros)

 
 lemma integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0"
   by (cases "integrable (null_measure M) f")
      (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
 
-subsection%important \<open>Legacy lemmas for the real-valued Lebesgue integral\<close>
+subsection \<open>Legacy lemmas for the real-valued Lebesgue integral\<close>
 theorem real_lebesgue_integral_def:
   assumes f[measurable]: "integrable M f"
   shows "integral\<^sup>L M f = enn2real (\<integral>\<^sup>+x. f x \<partial>M) - enn2real (\<integral>\<^sup>+x. ennreal (- f x) \<partial>M)"
 proof -
   have "integral\<^sup>L M f = integral\<^sup>L M (\<lambda>x. max 0 (f x) - max 0 (- f x))"

     by (rule has_bochner_integral_monotone_convergence) fact+
   then show "integrable M f" "integral\<^sup>L M f = x"
     by (auto simp: _has_bochner_integral_iff)
 qed
 
-subsection%important \<open>Product measure\<close>
+subsection \<open>Product measure\<close>
 
 lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
   assumes [measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
   shows "Measurable.pred N (\<lambda>x. integrable M (f x))"