# HG changeset patch
# User Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
# Date 1541096373 0
# Node ID 21ee588bac7d0fc37c49e351fd851eb94c7974e0
# Parent  c6b15fc78f7813a82622b2f5d29cb7327d9580e2
tagged a theory for the Analysis manual

diff -r c6b15fc78f78 -r 21ee588bac7d src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Nov 01 14:36:19 2018 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Nov 01 18:19:33 2018 +0000
@@ -5,7 +5,8 @@
     Author:     Bogdan Grechuk, University of Edinburgh
 *)
 
-section \<open>Limits on the Extended real number line\<close>
+section%important \<open>Limits on the Extended real number line\<close> (* TO FIX: perhaps put all Nonstandard Analysis related
+topics together? *)
 
 theory Extended_Real_Limits
 imports
@@ -15,23 +16,23 @@
   "HOL-Library.Indicator_Function"
 begin
 
-lemma compact_UNIV:
+lemma%important compact_UNIV:
   "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)"
-  using compact_complete_linorder
+  using%unimportant compact_complete_linorder
   by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def)
 
-lemma compact_eq_closed:
+lemma%important compact_eq_closed:
   fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
   shows "compact S \<longleftrightarrow> closed S"
-  using closed_Int_compact[of S, OF _ compact_UNIV] compact_imp_closed
+  using%unimportant closed_Int_compact[of S, OF _ compact_UNIV] compact_imp_closed
   by auto
 
-lemma closed_contains_Sup_cl:
+lemma%important closed_contains_Sup_cl:
   fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
   assumes "closed S"
     and "S \<noteq> {}"
   shows "Sup S \<in> S"
-proof -
+proof%unimportant -
   from compact_eq_closed[of S] compact_attains_sup[of S] assms
   obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s"
     by auto
@@ -41,12 +42,12 @@
     by simp
 qed
 
-lemma closed_contains_Inf_cl:
+lemma%important closed_contains_Inf_cl:
   fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
   assumes "closed S"
     and "S \<noteq> {}"
   shows "Inf S \<in> S"
-proof -
+proof%unimportant -
   from compact_eq_closed[of S] compact_attains_inf[of S] assms
   obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t"
     by auto
@@ -65,8 +66,8 @@
   qed (simp add: open_enat_def)
 qed
 
-instance ereal :: second_countable_topology
-proof (standard, intro exI conjI)
+instance%important ereal :: second_countable_topology
+proof%unimportant (standard, intro exI conjI)
   let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
   show "countable ?B"
     by (auto intro: countable_rat)
@@ -97,8 +98,8 @@
 
 text \<open>This is a copy from \<open>ereal :: second_countable_topology\<close>. Maybe find a common super class of
 topological spaces where the rational numbers are densely embedded ?\<close>
-instance ennreal :: second_countable_topology
-proof (standard, intro exI conjI)
+instance%important ennreal :: second_countable_topology
+proof%unimportant (standard, intro exI conjI)
   let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ennreal set set)"
   show "countable ?B"
     by (auto intro: countable_rat)
@@ -127,13 +128,13 @@
   qed
 qed
 
-lemma ereal_open_closed_aux:
+lemma%important ereal_open_closed_aux:
   fixes S :: "ereal set"
   assumes "open S"
     and "closed S"
     and S: "(-\<infinity>) \<notin> S"
   shows "S = {}"
-proof (rule ccontr)
+proof%unimportant (rule ccontr)
   assume "\<not> ?thesis"
   then have *: "Inf S \<in> S"
 
@@ -171,10 +172,10 @@
     by auto
 qed
 
-lemma ereal_open_closed:
+lemma%important ereal_open_closed:
   fixes S :: "ereal set"
   shows "open S \<and> closed S \<longleftrightarrow> S = {} \<or> S = UNIV"
-proof -
+proof%unimportant -
   {
     assume lhs: "open S \<and> closed S"
     {
@@ -195,10 +196,10 @@
     by auto
 qed
 
-lemma ereal_open_atLeast:
+lemma%important ereal_open_atLeast:
   fixes x :: ereal
   shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
-proof
+proof%unimportant
   assume "x = -\<infinity>"
   then have "{x..} = UNIV"
     by auto
@@ -214,12 +215,12 @@
     by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
 qed
 
-lemma mono_closed_real:
+lemma%important mono_closed_real:
   fixes S :: "real set"
   assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
     and "closed S"
   shows "S = {} \<or> S = UNIV \<or> (\<exists>a. S = {a..})"
-proof -
+proof%unimportant -
   {
     assume "S \<noteq> {}"
     { assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x"
@@ -260,12 +261,12 @@
     by blast
 qed
 
-lemma mono_closed_ereal:
+lemma%important mono_closed_ereal:
   fixes S :: "real set"
   assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
     and "closed S"
   shows "\<exists>a. S = {x. a \<le> ereal x}"
-proof -
+proof%unimportant -
   {
     assume "S = {}"
     then have ?thesis
@@ -295,11 +296,11 @@
     using mono_closed_real[of S] assms by auto
 qed
 
-lemma Liminf_within:
+lemma%important Liminf_within:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
   unfolding Liminf_def eventually_at
-proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
+proof%unimportant (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
   fix P d
   assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
@@ -315,11 +316,11 @@
        (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
 qed
 
-lemma Limsup_within:
+lemma%important Limsup_within:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
   unfolding Limsup_def eventually_at
-proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
+proof%unimportant (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
   fix P d
   assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
@@ -359,7 +360,7 @@
   done
 
 
-subsection \<open>Extended-Real.thy\<close>
+subsection%important \<open>Extended-Real.thy\<close> (*FIX title *)
 
 lemma sum_constant_ereal:
   fixes a::ereal
@@ -379,10 +380,10 @@
   ultimately show ?thesis by (metis (mono_tags, lifting) eventually_mono)
 qed
 
-lemma ereal_Inf_cmult:
+lemma%important ereal_Inf_cmult:
   assumes "c>(0::real)"
   shows "Inf {ereal c * x |x. P x} = ereal c * Inf {x. P x}"
-proof -
+proof%unimportant -
   have "(\<lambda>x::ereal. c * x) (Inf {x::ereal. P x}) = Inf ((\<lambda>x::ereal. c * x)`{x::ereal. P x})"
     apply (rule mono_bij_Inf)
     apply (simp add: assms ereal_mult_left_mono less_imp_le mono_def)
@@ -393,7 +394,7 @@
 qed
 
 
-subsubsection \<open>Continuity of addition\<close>
+subsubsection%important \<open>Continuity of addition\<close>
 
 text \<open>The next few lemmas remove an unnecessary assumption in \verb+tendsto_add_ereal+, culminating
 in \verb+tendsto_add_ereal_general+ which essentially says that the addition
@@ -401,12 +402,12 @@
 It is much more convenient in many situations, see for instance the proof of
 \verb+tendsto_sum_ereal+ below.\<close>
 
-lemma tendsto_add_ereal_PInf:
+lemma%important tendsto_add_ereal_PInf:
   fixes y :: ereal
   assumes y: "y \<noteq> -\<infinity>"
   assumes f: "(f \<longlongrightarrow> \<infinity>) F" and g: "(g \<longlongrightarrow> y) F"
   shows "((\<lambda>x. f x + g x) \<longlongrightarrow> \<infinity>) F"
-proof -
+proof%unimportant -
   have "\<exists>C. eventually (\<lambda>x. g x > ereal C) F"
   proof (cases y)
     case (real r)
@@ -439,12 +440,12 @@
 that $-(x+y)$ is in general different from $(-x) + (-y)$ in ereal creates difficulties,
 so it is more efficient to copy the previous proof.\<close>
 
-lemma tendsto_add_ereal_MInf:
+lemma%important tendsto_add_ereal_MInf:
   fixes y :: ereal
   assumes y: "y \<noteq> \<infinity>"
   assumes f: "(f \<longlongrightarrow> -\<infinity>) F" and g: "(g \<longlongrightarrow> y) F"
   shows "((\<lambda>x. f x + g x) \<longlongrightarrow> -\<infinity>) F"
-proof -
+proof%unimportant -
   have "\<exists>C. eventually (\<lambda>x. g x < ereal C) F"
   proof (cases y)
     case (real r)
@@ -472,12 +473,12 @@
   then show ?thesis by (simp add: tendsto_MInfty)
 qed
 
-lemma tendsto_add_ereal_general1:
+lemma%important tendsto_add_ereal_general1:
   fixes x y :: ereal
   assumes y: "\<bar>y\<bar> \<noteq> \<infinity>"
   assumes f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
-proof (cases x)
+proof%unimportant (cases x)
   case (real r)
   have a: "\<bar>x\<bar> \<noteq> \<infinity>" by (simp add: real)
   show ?thesis by (rule tendsto_add_ereal[OF a, OF y, OF f, OF g])
@@ -490,12 +491,12 @@
     by (metis abs_ereal.simps(3) ereal_MInfty_eq_plus)
 qed
 
-lemma tendsto_add_ereal_general2:
+lemma%important tendsto_add_ereal_general2:
   fixes x y :: ereal
   assumes x: "\<bar>x\<bar> \<noteq> \<infinity>"
       and f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
-proof -
+proof%unimportant -
   have "((\<lambda>x. g x + f x) \<longlongrightarrow> x + y) F"
     using tendsto_add_ereal_general1[OF x, OF g, OF f] add.commute[of "y", of "x"] by simp
   moreover have "\<And>x. g x + f x = f x + g x" using add.commute by auto
@@ -505,12 +506,12 @@
 text \<open>The next lemma says that the addition is continuous on ereal, except at
 the pairs $(-\infty, \infty)$ and $(\infty, -\infty)$.\<close>
 
-lemma tendsto_add_ereal_general [tendsto_intros]:
+lemma%important tendsto_add_ereal_general [tendsto_intros]:
   fixes x y :: ereal
   assumes "\<not>((x=\<infinity> \<and> y=-\<infinity>) \<or> (x=-\<infinity> \<and> y=\<infinity>))"
       and f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
-proof (cases x)
+proof%unimportant (cases x)
   case (real r)
   show ?thesis
     apply (rule tendsto_add_ereal_general2) using real assms by auto
@@ -524,16 +525,16 @@
   then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
 qed
 
-subsubsection \<open>Continuity of multiplication\<close>
+subsubsection%important \<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 $(\infty, 0)$ and $(-\infty, 0)$ and $(0, \infty)$ and $(0, -\infty)$,
 starting with specific situations.\<close>
 
-lemma tendsto_mult_real_ereal:
+lemma%important tendsto_mult_real_ereal:
   assumes "(u \<longlongrightarrow> ereal l) F" "(v \<longlongrightarrow> ereal m) F"
   shows "((\<lambda>n. u n * v n) \<longlongrightarrow> ereal l * ereal m) F"
-proof -
+proof%unimportant -
   have ureal: "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) F" by (rule real_lim_then_eventually_real[OF assms(1)])
   then have "((\<lambda>n. ereal(real_of_ereal(u n))) \<longlongrightarrow> ereal l) F" using assms by auto
   then have limu: "((\<lambda>n. real_of_ereal(u n)) \<longlongrightarrow> l) F" by auto
@@ -553,11 +554,11 @@
   then show ?thesis using * filterlim_cong by fastforce
 qed
 
-lemma tendsto_mult_ereal_PInf:
+lemma%important tendsto_mult_ereal_PInf:
   fixes f g::"_ \<Rightarrow> ereal"
   assumes "(f \<longlongrightarrow> l) F" "l>0" "(g \<longlongrightarrow> \<infinity>) F"
   shows "((\<lambda>x. f x * g x) \<longlongrightarrow> \<infinity>) F"
-proof -
+proof%unimportant -
   obtain a::real where "0 < ereal a" "a < l" using assms(2) using ereal_dense2 by blast
   have *: "eventually (\<lambda>x. f x > a) F" using \<open>a < l\<close> assms(1) by (simp add: order_tendsto_iff)
   {
@@ -581,11 +582,11 @@
   then show ?thesis by (auto simp add: tendsto_PInfty)
 qed
 
-lemma tendsto_mult_ereal_pos:
+lemma%important tendsto_mult_ereal_pos:
   fixes f g::"_ \<Rightarrow> ereal"
   assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "l>0" "m>0"
   shows "((\<lambda>x. f x * g x) \<longlongrightarrow> l * m) F"
-proof (cases)
+proof%unimportant (cases)
   assume *: "l = \<infinity> \<or> m = \<infinity>"
   then show ?thesis
   proof (cases)
@@ -620,11 +621,11 @@
   shows "sgn(l) * sgn(l) = 1"
 apply (cases l) using assms by (auto simp add: one_ereal_def sgn_if)
 
-lemma tendsto_mult_ereal [tendsto_intros]:
+lemma%important tendsto_mult_ereal [tendsto_intros]:
   fixes f g::"_ \<Rightarrow> ereal"
   assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "\<not>((l=0 \<and> abs(m) = \<infinity>) \<or> (m=0 \<and> abs(l) = \<infinity>))"
   shows "((\<lambda>x. f x * g x) \<longlongrightarrow> l * m) F"
-proof (cases)
+proof%unimportant (cases)
   assume "l=0 \<or> m=0"
   then have "abs(l) \<noteq> \<infinity>" "abs(m) \<noteq> \<infinity>" using assms(3) by auto
   then obtain lr mr where "l = ereal lr" "m = ereal mr" by auto
@@ -661,13 +662,13 @@
 by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
 
 
-subsubsection \<open>Continuity of division\<close>
+subsubsection%important \<open>Continuity of division\<close>
 
-lemma tendsto_inverse_ereal_PInf:
+lemma%important tendsto_inverse_ereal_PInf:
   fixes u::"_ \<Rightarrow> ereal"
   assumes "(u \<longlongrightarrow> \<infinity>) F"
   shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 0) F"
-proof -
+proof%unimportant -
   {
     fix e::real assume "e>0"
     have "1/e < \<infinity>" by auto
@@ -704,11 +705,11 @@
   shows "(u \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. 1/ u x) \<longlongrightarrow> 1/l) F"
   using tendsto_inverse unfolding inverse_eq_divide .
 
-lemma tendsto_inverse_ereal [tendsto_intros]:
+lemma%important tendsto_inverse_ereal [tendsto_intros]:
   fixes u::"_ \<Rightarrow> ereal"
   assumes "(u \<longlongrightarrow> l) F" "l \<noteq> 0"
   shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 1/l) F"
-proof (cases l)
+proof%unimportant (cases l)
   case (real r)
   then have "r \<noteq> 0" using assms(2) by auto
   then have "1/l = ereal(1/r)" using real by (simp add: one_ereal_def)
@@ -749,11 +750,11 @@
   then show ?thesis unfolding v_def using Lim_transform_eventually[OF *] \<open> 1/l = 0 \<close> by auto
 qed
 
-lemma tendsto_divide_ereal [tendsto_intros]:
+lemma%important tendsto_divide_ereal [tendsto_intros]:
   fixes f g::"_ \<Rightarrow> ereal"
   assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "m \<noteq> 0" "\<not>(abs(l) = \<infinity> \<and> abs(m) = \<infinity>)"
   shows "((\<lambda>x. f x / g x) \<longlongrightarrow> l / m) F"
-proof -
+proof%unimportant -
   define h where "h = (\<lambda>x. 1/ g x)"
   have *: "(h \<longlongrightarrow> 1/m) F" unfolding h_def using assms(2) assms(3) tendsto_inverse_ereal by auto
   have "((\<lambda>x. f x * h x) \<longlongrightarrow> l * (1/m)) F"
@@ -764,15 +765,15 @@
 qed
 
 
-subsubsection \<open>Further limits\<close>
+subsubsection%important \<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]:
+lemma%important tendsto_diff_ereal_general [tendsto_intros]:
   fixes u v::"'a \<Rightarrow> ereal"
   assumes "(u \<longlongrightarrow> l) F" "(v \<longlongrightarrow> m) F" "\<not>((l = \<infinity> \<and> m = \<infinity>) \<or> (l = -\<infinity> \<and> m = -\<infinity>))"
   shows "((\<lambda>n. u n - v n) \<longlongrightarrow> l - m) F"
-proof -
+proof%unimportant -
   have "((\<lambda>n. u n + (-v n)) \<longlongrightarrow> l + (-m)) F"
     apply (intro tendsto_intros assms) using assms by (auto simp add: ereal_uminus_eq_reorder)
   then show ?thesis by (simp add: minus_ereal_def)
@@ -782,11 +783,11 @@
   "(\<lambda> n::nat. real n) \<longlonglongrightarrow> \<infinity>"
 by (simp add: filterlim_real_sequentially tendsto_PInfty_eq_at_top)
 
-lemma tendsto_at_top_pseudo_inverse [tendsto_intros]:
+lemma%important tendsto_at_top_pseudo_inverse [tendsto_intros]:
   fixes u::"nat \<Rightarrow> nat"
   assumes "LIM n sequentially. u n :> at_top"
   shows "LIM n sequentially. Inf {N. u N \<ge> n} :> at_top"
-proof -
+proof%unimportant -
   {
     fix C::nat
     define M where "M = Max {u n| n. n \<le> C}+1"
@@ -813,11 +814,11 @@
   then show ?thesis using filterlim_at_top by auto
 qed
 
-lemma pseudo_inverse_finite_set:
+lemma%important pseudo_inverse_finite_set:
   fixes u::"nat \<Rightarrow> nat"
   assumes "LIM n sequentially. u n :> at_top"
   shows "finite {N. u N \<le> n}"
-proof -
+proof%unimportant -
   fix n
   have "eventually (\<lambda>N. u N \<ge> n+1) sequentially" using assms
     by (simp add: filterlim_at_top)
@@ -862,11 +863,11 @@
   then show ?thesis by auto
 qed
 
-lemma ereal_truncation_real_top [tendsto_intros]:
+lemma%important ereal_truncation_real_top [tendsto_intros]:
   fixes x::ereal
   assumes "x \<noteq> - \<infinity>"
   shows "(\<lambda>n::nat. real_of_ereal(min x n)) \<longlonglongrightarrow> x"
-proof (cases x)
+proof%unimportant (cases x)
   case (real r)
   then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
@@ -880,10 +881,10 @@
   then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto
 qed (simp add: assms)
 
-lemma ereal_truncation_bottom [tendsto_intros]:
+lemma%important ereal_truncation_bottom [tendsto_intros]:
   fixes x::ereal
   shows "(\<lambda>n::nat. max x (- real n)) \<longlonglongrightarrow> x"
-proof (cases x)
+proof%unimportant (cases x)
   case (real r)
   then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
@@ -901,11 +902,11 @@
   then show ?thesis by auto
 qed
 
-lemma ereal_truncation_real_bottom [tendsto_intros]:
+lemma%important ereal_truncation_real_bottom [tendsto_intros]:
   fixes x::ereal
   assumes "x \<noteq> \<infinity>"
   shows "(\<lambda>n::nat. real_of_ereal(max x (- real n))) \<longlonglongrightarrow> x"
-proof (cases x)
+proof%unimportant (cases x)
   case (real r)
   then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
@@ -933,9 +934,9 @@
 qed(simp)
 
 
-lemma continuous_ereal_abs:
+lemma%important continuous_ereal_abs:
   "continuous_on (UNIV::ereal set) abs"
-proof -
+proof%unimportant -
   have "continuous_on ({..0} \<union> {(0::ereal)..}) abs"
     apply (rule continuous_on_closed_Un, auto)
     apply (rule iffD1[OF continuous_on_cong, of "{..0}" _ "\<lambda>x. -x"])
@@ -960,7 +961,7 @@
 by (subst uminus_ereal.simps(1)[symmetric], intro tendsto_intros)
 
 
-subsection \<open>Extended-Nonnegative-Real.thy\<close>
+subsection%important \<open>Extended-Nonnegative-Real.thy\<close> (*FIX title *)
 
 lemma tendsto_diff_ennreal_general [tendsto_intros]:
   fixes u v::"'a \<Rightarrow> ennreal"
@@ -972,11 +973,11 @@
   then show ?thesis by auto
 qed
 
-lemma tendsto_mult_ennreal [tendsto_intros]:
+lemma%important tendsto_mult_ennreal [tendsto_intros]:
   fixes l m::ennreal
   assumes "(u \<longlongrightarrow> l) F" "(v \<longlongrightarrow> m) F" "\<not>((l = 0 \<and> m = \<infinity>) \<or> (l = \<infinity> \<and> m = 0))"
   shows "((\<lambda>n. u n * v n) \<longlongrightarrow> l * m) F"
-proof -
+proof%unimportant -
   have "((\<lambda>n. e2ennreal(enn2ereal (u n) * enn2ereal (v n))) \<longlongrightarrow> e2ennreal(enn2ereal l * enn2ereal m)) F"
     apply (intro tendsto_intros) using assms apply auto
     using enn2ereal_inject zero_ennreal.rep_eq by fastforce+
@@ -989,9 +990,9 @@
 qed
 
 
-subsection \<open>monoset\<close>
+subsection%important \<open>monoset\<close>
 
-definition (in order) mono_set:
+definition%important (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
@@ -999,11 +1000,11 @@
 lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
 lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
 
-lemma (in complete_linorder) mono_set_iff:
+lemma%important (in complete_linorder) mono_set_iff:
   fixes S :: "'a set"
   defines "a \<equiv> Inf S"
   shows "mono_set S \<longleftrightarrow> S = {a <..} \<or> S = {a..}" (is "_ = ?c")
-proof
+proof%unimportant
   assume "mono_set S"
   then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S"
     by (auto simp: mono_set)
@@ -1045,12 +1046,12 @@
   by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
     ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
 
-lemma ereal_Liminf_Sup_monoset:
+lemma%important ereal_Liminf_Sup_monoset:
   fixes f :: "'a \<Rightarrow> ereal"
   shows "Liminf net f =
     Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
     (is "_ = Sup ?A")
-proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
+proof%unimportant (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
   fix P
   assume P: "eventually P net"
   fix S
@@ -1084,12 +1085,12 @@
   qed
 qed
 
-lemma ereal_Limsup_Inf_monoset:
+lemma%important ereal_Limsup_Inf_monoset:
   fixes f :: "'a \<Rightarrow> ereal"
   shows "Limsup net f =
     Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
     (is "_ = Inf ?A")
-proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
+proof%unimportant (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
   fix P
   assume P: "eventually P net"
   fix S
@@ -1123,11 +1124,11 @@
   qed
 qed
 
-lemma liminf_bounded_open:
+lemma%important liminf_bounded_open:
   fixes x :: "nat \<Rightarrow> ereal"
   shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
   (is "_ \<longleftrightarrow> ?P x0")
-proof
+proof%unimportant
   assume "?P x0"
   then show "x0 \<le> liminf x"
     unfolding ereal_Liminf_Sup_monoset eventually_sequentially
@@ -1161,11 +1162,11 @@
     by auto
 qed
 
-lemma limsup_finite_then_bounded:
+lemma%important limsup_finite_then_bounded:
   fixes u::"nat \<Rightarrow> real"
   assumes "limsup u < \<infinity>"
   shows "\<exists>C. \<forall>n. u n \<le> C"
-proof -
+proof%unimportant -
   obtain C where C: "limsup u < C" "C < \<infinity>" using assms ereal_dense2 by blast
   then have "C = ereal(real_of_ereal C)" using ereal_real by force
   have "eventually (\<lambda>n. u n < C) sequentially" using C(1) unfolding Limsup_def
@@ -1275,11 +1276,11 @@
   then show ?case using Suc.IH by simp
 qed (auto)
 
-lemma Limsup_obtain:
+lemma%important Limsup_obtain:
   fixes u::"_ \<Rightarrow> 'a :: complete_linorder"
   assumes "Limsup F u > c"
   shows "\<exists>i. u i > c"
-proof -
+proof%unimportant -
   have "(INF P:{P. eventually P F}. SUP x:{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
   then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff)
 qed
@@ -1287,10 +1288,10 @@
 text \<open>The next lemma is extremely useful, as it often makes it possible to reduce statements
 about limsups to statements about limits.\<close>
 
-lemma limsup_subseq_lim:
+lemma%important limsup_subseq_lim:
   fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> limsup u"
-proof (cases)
+proof%unimportant (cases)
   assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<le> u p"
   then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<le> u (r n)) \<and> r n < r (Suc n)"
     by (intro dependent_nat_choice) (auto simp: conj_commute)
@@ -1380,10 +1381,10 @@
   then show ?thesis using \<open>strict_mono r\<close> by auto
 qed
 
-lemma liminf_subseq_lim:
+lemma%important liminf_subseq_lim:
   fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> liminf u"
-proof (cases)
+proof%unimportant (cases)
   assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<ge> u p"
   then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<ge> u (r n)) \<and> r n < r (Suc n)"
     by (intro dependent_nat_choice) (auto simp: conj_commute)
@@ -1478,10 +1479,10 @@
 subsequences thanks to \verb+limsup_subseq_lim+. The statement for limits follows for instance from
 \verb+tendsto_add_ereal_general+.\<close>
 
-lemma ereal_limsup_add_mono:
+lemma%important ereal_limsup_add_mono:
   fixes u v::"nat \<Rightarrow> ereal"
   shows "limsup (\<lambda>n. u n + v n) \<le> limsup u + limsup v"
-proof (cases)
+proof%unimportant (cases)
   assume "(limsup u = \<infinity>) \<or> (limsup v = \<infinity>)"
   then have "limsup u + limsup v = \<infinity>" by simp
   then show ?thesis by auto
@@ -1524,11 +1525,11 @@
 This explains why there are more assumptions in the next lemma dealing with liminfs that in the
 previous one about limsups.\<close>
 
-lemma ereal_liminf_add_mono:
+lemma%important ereal_liminf_add_mono:
   fixes u v::"nat \<Rightarrow> ereal"
   assumes "\<not>((liminf u = \<infinity> \<and> liminf v = -\<infinity>) \<or> (liminf u = -\<infinity> \<and> liminf v = \<infinity>))"
   shows "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
-proof (cases)
+proof%unimportant (cases)
   assume "(liminf u = -\<infinity>) \<or> (liminf v = -\<infinity>)"
   then have *: "liminf u + liminf v = -\<infinity>" using assms by auto
   show ?thesis by (simp add: *)
@@ -1567,11 +1568,11 @@
   then show ?thesis unfolding w_def by simp
 qed
 
-lemma ereal_limsup_lim_add:
+lemma%important ereal_limsup_lim_add:
   fixes u v::"nat \<Rightarrow> ereal"
   assumes "u \<longlonglongrightarrow> a" "abs(a) \<noteq> \<infinity>"
   shows "limsup (\<lambda>n. u n + v n) = a + limsup v"
-proof -
+proof%unimportant -
   have "limsup u = a" using assms(1) using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
   have "(\<lambda>n. -u n) \<longlonglongrightarrow> -a" using assms(1) by auto
   then have "limsup (\<lambda>n. -u n) = -a" using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
@@ -1598,11 +1599,11 @@
   then show ?thesis using up by simp
 qed
 
-lemma ereal_limsup_lim_mult:
+lemma%important ereal_limsup_lim_mult:
   fixes u v::"nat \<Rightarrow> ereal"
   assumes "u \<longlonglongrightarrow> a" "a>0" "a \<noteq> \<infinity>"
   shows "limsup (\<lambda>n. u n * v n) = a * limsup v"
-proof -
+proof%unimportant -
   define w where "w = (\<lambda>n. u n * v n)"
   obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
   have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
@@ -1628,11 +1629,11 @@
   then show ?thesis using I unfolding w_def by auto
 qed
 
-lemma ereal_liminf_lim_mult:
+lemma%important ereal_liminf_lim_mult:
   fixes u v::"nat \<Rightarrow> ereal"
   assumes "u \<longlonglongrightarrow> a" "a>0" "a \<noteq> \<infinity>"
   shows "liminf (\<lambda>n. u n * v n) = a * liminf v"
-proof -
+proof%unimportant -
   define w where "w = (\<lambda>n. u n * v n)"
   obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
   have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
@@ -1658,11 +1659,11 @@
   then show ?thesis using I unfolding w_def by auto
 qed
 
-lemma ereal_liminf_lim_add:
+lemma%important ereal_liminf_lim_add:
   fixes u v::"nat \<Rightarrow> ereal"
   assumes "u \<longlonglongrightarrow> a" "abs(a) \<noteq> \<infinity>"
   shows "liminf (\<lambda>n. u n + v n) = a + liminf v"
-proof -
+proof%unimportant -
   have "liminf u = a" using assms(1) tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
   then have *: "abs(liminf u) \<noteq> \<infinity>" using assms(2) by auto
   have "(\<lambda>n. -u n) \<longlonglongrightarrow> -a" using assms(1) by auto
@@ -1691,10 +1692,10 @@
   then show ?thesis using up by simp
 qed
 
-lemma ereal_liminf_limsup_add:
+lemma%important ereal_liminf_limsup_add:
   fixes u v::"nat \<Rightarrow> ereal"
   shows "liminf (\<lambda>n. u n + v n) \<le> liminf u + limsup v"
-proof (cases)
+proof%unimportant (cases)
   assume "limsup v = \<infinity> \<or> liminf u = \<infinity>"
   then show ?thesis by auto
 next
@@ -1743,12 +1744,12 @@
   done
 
 
-lemma liminf_minus_ennreal:
+lemma%important liminf_minus_ennreal:
   fixes u v::"nat \<Rightarrow> ennreal"
   shows "(\<And>n. v n \<le> u n) \<Longrightarrow> liminf (\<lambda>n. u n - v n) \<le> limsup u - limsup v"
   unfolding liminf_SUP_INF limsup_INF_SUP
   including ennreal.lifting
-proof (transfer, clarsimp)
+proof%unimportant (transfer, clarsimp)
   fix v u :: "nat \<Rightarrow> ereal" assume *: "\<forall>x. 0 \<le> v x" "\<forall>x. 0 \<le> u x" "\<And>n. v n \<le> u n"
   moreover have "0 \<le> limsup u - limsup v"
     using * by (intro ereal_diff_positive Limsup_mono always_eventually) simp
@@ -1761,7 +1762,7 @@
     by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
 qed
 
-subsection "Relate extended reals and the indicator function"
+subsection%unimportant "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)