src/HOL/Analysis/Extended_Real_Limits.thy

   apply auto
   apply (metis (no_types, lifting) INF_insert centre_in_ball greaterThan_iff image_cong inf_commute insert_Diff)
   done
 
 
-subsection%important \<open>Extended-Real.thy\<close> (*FIX ME change title *)
+subsection \<open>Extended-Real.thy\<close> (*FIX ME change title *)
 
 lemma sum_constant_ereal:
   fixes a::ereal
   shows "(\<Sum>i\<in>I. a) = a * card I"
 apply (cases "finite I", induct set: finite, simp_all)

     done
   then show ?thesis by (simp only: setcompr_eq_image[symmetric])
 qed
 
 
-subsubsection%important \<open>Continuity of addition\<close>
+subsubsection \<open>Continuity of addition\<close>
 
 text \<open>The next few lemmas remove an unnecessary assumption in \<open>tendsto_add_ereal\<close>, culminating
 in \<open>tendsto_add_ereal_general\<close> which essentially says that the addition
 is continuous on ereal times ereal, except at \<open>(-\<infinity>, \<infinity>)\<close> and \<open>(\<infinity>, -\<infinity>)\<close>.
 It is much more convenient in many situations, see for instance the proof of

   case (MInf)
   then have "y \<noteq> \<infinity>" using assms by simp
   then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
 qed
 
-subsubsection%important \<open>Continuity of multiplication\<close>
+subsubsection \<open>Continuity of multiplication\<close>
 
 text \<open>In the same way as for addition, we prove that the multiplication is continuous on
 ereal times ereal, except at \<open>(\<infinity>, 0)\<close> and \<open>(-\<infinity>, 0)\<close> and \<open>(0, \<infinity>)\<close> and \<open>(0, -\<infinity>)\<close>,
 starting with specific situations.\<close>
 

   assumes "(f \<longlongrightarrow> l) F" "\<not> (l=0 \<and> abs(c) = \<infinity>)"
   shows "((\<lambda>x. c * f x) \<longlongrightarrow> c * l) F"
 by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
 
 
-subsubsection%important \<open>Continuity of division\<close>
+subsubsection \<open>Continuity of division\<close>
 
 lemma tendsto_inverse_ereal_PInf:
   fixes u::"_ \<Rightarrow> ereal"
   assumes "(u \<longlongrightarrow> \<infinity>) F"
   shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 0) F"

   moreover have "l * (1/m) = l/m" by (simp add: divide_ereal_def)
   ultimately show ?thesis unfolding h_def using Lim_transform_eventually by auto
 qed
 
 
-subsubsection%important \<open>Further limits\<close>
+subsubsection \<open>Further limits\<close>
 
 text \<open>The assumptions of @{thm tendsto_diff_ereal} are too strong, we weaken them here.\<close>
 
 lemma tendsto_diff_ereal_general [tendsto_intros]:
   fixes u v::"'a \<Rightarrow> ereal"

 lemma ereal_minus_real_tendsto_MInf [tendsto_intros]:
   "(\<lambda>x. ereal (- real x)) \<longlonglongrightarrow> - \<infinity>"
 by (subst uminus_ereal.simps(1)[symmetric], intro tendsto_intros)
 
 
-subsection%important \<open>Extended-Nonnegative-Real.thy\<close> (*FIX title *)
+subsection \<open>Extended-Nonnegative-Real.thy\<close> (*FIX title *)
 
 lemma tendsto_diff_ennreal_general [tendsto_intros]:
   fixes u v::"'a \<Rightarrow> ennreal"
   assumes "(u \<longlongrightarrow> l) F" "(v \<longlongrightarrow> m) F" "\<not>(l = \<infinity> \<and> m = \<infinity>)"
   shows "((\<lambda>n. u n - v n) \<longlongrightarrow> l - m) F"

   ultimately show ?thesis
     by auto
 qed
 
 
-subsection%important \<open>monoset\<close> (*FIX ME title *)
+subsection \<open>monoset\<close> (*FIX ME title *)
 
 definition (in order) mono_set:
   "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
 
 lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto

   ultimately show "(SUP n. INF n\<in>{n..}. max 0 (u n - v n))
             \<le> max 0 ((INF x. max 0 (Sup (u ` {x..}))) - (INF x. max 0 (Sup (v ` {x..}))))"
     by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
 qed
 
-subsection%important "Relate extended reals and the indicator function"
+subsection "Relate extended reals and the indicator function"
 
 lemma ereal_indicator_le_0: "(indicator S x::ereal) \<le> 0 \<longleftrightarrow> x \<notin> S"
   by (auto split: split_indicator simp: one_ereal_def)
 
 lemma ereal_indicator: "ereal (indicator A x) = indicator A x"