src/HOL/Analysis/Radon_Nikodym.thy

       then show "0 < ?h x" and "?h x < \<infinity>" using n[of i] by (auto simp: less_top[symmetric]) }
     note pos = this
   qed measurable
 qed
 
-subsection%important "Absolutely continuous"
+subsection "Absolutely continuous"
 
 definition%important absolutely_continuous :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
   "absolutely_continuous M N \<longleftrightarrow> null_sets M \<subseteq> null_sets N"
 
 lemma absolutely_continuousI_count_space: "absolutely_continuous (count_space A) M"

     from \<open>absolutely_continuous M M'\<close> show "N \<in> null_sets M'"
       using N unfolding absolutely_continuous_def sets_eq null_sets_def by auto
   qed
 qed
 
-subsection%important "Existence of the Radon-Nikodym derivative"
+subsection "Existence of the Radon-Nikodym derivative"
 
 lemma%important
  (in finite_measure) Radon_Nikodym_finite_measure:
   assumes "finite_measure N" and sets_eq[simp]: "sets N = sets M"
   assumes "absolutely_continuous M N"

   obtain f where f_borel: "f \<in> borel_measurable M" "density ?MT f = N" by auto
   with nn borel show ?thesis
     by (auto intro!: bexI[of _ "\<lambda>x. h x * f x"] simp: density_density_eq)
 qed
 
-subsection%important \<open>Uniqueness of densities\<close>
+subsection \<open>Uniqueness of densities\<close>
 
 lemma%important finite_density_unique:
   assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
   and fin: "integral\<^sup>N M f \<noteq> \<infinity>"

 lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
   "f \<in> borel_measurable M \<Longrightarrow> sigma_finite_measure (density M f) \<longleftrightarrow> (AE x in M. f x \<noteq> \<infinity>)"
   by (subst sigma_finite_iff_density_finite')
      (auto simp: max_def intro!: measurable_If)
 
-subsection%important \<open>Radon-Nikodym derivative\<close>
+subsection \<open>Radon-Nikodym derivative\<close>
 
 definition%important RN_deriv :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a \<Rightarrow> ennreal" where
   "RN_deriv M N =
     (if \<exists>f. f \<in> borel_measurable M \<and> density M f = N
        then SOME f. f \<in> borel_measurable M \<and> density M f = N