tagged a theory for the Analysis manual
authorAngeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
Thu Nov 01 18:19:33 2018 +0000 (6 months ago)
changeset 6922121ee588bac7d
parent 69220 c6b15fc78f78
child 69229 043cbeb0b1cf
tagged a theory for the Analysis manual
src/HOL/Analysis/Extended_Real_Limits.thy
     1.1 --- a/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Nov 01 14:36:19 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Nov 01 18:19:33 2018 +0000
     1.3 @@ -5,7 +5,8 @@
     1.4      Author:     Bogdan Grechuk, University of Edinburgh
     1.5  *)
     1.6  
     1.7 -section \<open>Limits on the Extended real number line\<close>
     1.8 +section%important \<open>Limits on the Extended real number line\<close> (* TO FIX: perhaps put all Nonstandard Analysis related
     1.9 +topics together? *)
    1.10  
    1.11  theory Extended_Real_Limits
    1.12  imports
    1.13 @@ -15,23 +16,23 @@
    1.14    "HOL-Library.Indicator_Function"
    1.15  begin
    1.16  
    1.17 -lemma compact_UNIV:
    1.18 +lemma%important compact_UNIV:
    1.19    "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)"
    1.20 -  using compact_complete_linorder
    1.21 +  using%unimportant compact_complete_linorder
    1.22    by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def)
    1.23  
    1.24 -lemma compact_eq_closed:
    1.25 +lemma%important compact_eq_closed:
    1.26    fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
    1.27    shows "compact S \<longleftrightarrow> closed S"
    1.28 -  using closed_Int_compact[of S, OF _ compact_UNIV] compact_imp_closed
    1.29 +  using%unimportant closed_Int_compact[of S, OF _ compact_UNIV] compact_imp_closed
    1.30    by auto
    1.31  
    1.32 -lemma closed_contains_Sup_cl:
    1.33 +lemma%important closed_contains_Sup_cl:
    1.34    fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
    1.35    assumes "closed S"
    1.36      and "S \<noteq> {}"
    1.37    shows "Sup S \<in> S"
    1.38 -proof -
    1.39 +proof%unimportant -
    1.40    from compact_eq_closed[of S] compact_attains_sup[of S] assms
    1.41    obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s"
    1.42      by auto
    1.43 @@ -41,12 +42,12 @@
    1.44      by simp
    1.45  qed
    1.46  
    1.47 -lemma closed_contains_Inf_cl:
    1.48 +lemma%important closed_contains_Inf_cl:
    1.49    fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
    1.50    assumes "closed S"
    1.51      and "S \<noteq> {}"
    1.52    shows "Inf S \<in> S"
    1.53 -proof -
    1.54 +proof%unimportant -
    1.55    from compact_eq_closed[of S] compact_attains_inf[of S] assms
    1.56    obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t"
    1.57      by auto
    1.58 @@ -65,8 +66,8 @@
    1.59    qed (simp add: open_enat_def)
    1.60  qed
    1.61  
    1.62 -instance ereal :: second_countable_topology
    1.63 -proof (standard, intro exI conjI)
    1.64 +instance%important ereal :: second_countable_topology
    1.65 +proof%unimportant (standard, intro exI conjI)
    1.66    let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
    1.67    show "countable ?B"
    1.68      by (auto intro: countable_rat)
    1.69 @@ -97,8 +98,8 @@
    1.70  
    1.71  text \<open>This is a copy from \<open>ereal :: second_countable_topology\<close>. Maybe find a common super class of
    1.72  topological spaces where the rational numbers are densely embedded ?\<close>
    1.73 -instance ennreal :: second_countable_topology
    1.74 -proof (standard, intro exI conjI)
    1.75 +instance%important ennreal :: second_countable_topology
    1.76 +proof%unimportant (standard, intro exI conjI)
    1.77    let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ennreal set set)"
    1.78    show "countable ?B"
    1.79      by (auto intro: countable_rat)
    1.80 @@ -127,13 +128,13 @@
    1.81    qed
    1.82  qed
    1.83  
    1.84 -lemma ereal_open_closed_aux:
    1.85 +lemma%important ereal_open_closed_aux:
    1.86    fixes S :: "ereal set"
    1.87    assumes "open S"
    1.88      and "closed S"
    1.89      and S: "(-\<infinity>) \<notin> S"
    1.90    shows "S = {}"
    1.91 -proof (rule ccontr)
    1.92 +proof%unimportant (rule ccontr)
    1.93    assume "\<not> ?thesis"
    1.94    then have *: "Inf S \<in> S"
    1.95  
    1.96 @@ -171,10 +172,10 @@
    1.97      by auto
    1.98  qed
    1.99  
   1.100 -lemma ereal_open_closed:
   1.101 +lemma%important ereal_open_closed:
   1.102    fixes S :: "ereal set"
   1.103    shows "open S \<and> closed S \<longleftrightarrow> S = {} \<or> S = UNIV"
   1.104 -proof -
   1.105 +proof%unimportant -
   1.106    {
   1.107      assume lhs: "open S \<and> closed S"
   1.108      {
   1.109 @@ -195,10 +196,10 @@
   1.110      by auto
   1.111  qed
   1.112  
   1.113 -lemma ereal_open_atLeast:
   1.114 +lemma%important ereal_open_atLeast:
   1.115    fixes x :: ereal
   1.116    shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
   1.117 -proof
   1.118 +proof%unimportant
   1.119    assume "x = -\<infinity>"
   1.120    then have "{x..} = UNIV"
   1.121      by auto
   1.122 @@ -214,12 +215,12 @@
   1.123      by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
   1.124  qed
   1.125  
   1.126 -lemma mono_closed_real:
   1.127 +lemma%important mono_closed_real:
   1.128    fixes S :: "real set"
   1.129    assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
   1.130      and "closed S"
   1.131    shows "S = {} \<or> S = UNIV \<or> (\<exists>a. S = {a..})"
   1.132 -proof -
   1.133 +proof%unimportant -
   1.134    {
   1.135      assume "S \<noteq> {}"
   1.136      { assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x"
   1.137 @@ -260,12 +261,12 @@
   1.138      by blast
   1.139  qed
   1.140  
   1.141 -lemma mono_closed_ereal:
   1.142 +lemma%important mono_closed_ereal:
   1.143    fixes S :: "real set"
   1.144    assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
   1.145      and "closed S"
   1.146    shows "\<exists>a. S = {x. a \<le> ereal x}"
   1.147 -proof -
   1.148 +proof%unimportant -
   1.149    {
   1.150      assume "S = {}"
   1.151      then have ?thesis
   1.152 @@ -295,11 +296,11 @@
   1.153      using mono_closed_real[of S] assms by auto
   1.154  qed
   1.155  
   1.156 -lemma Liminf_within:
   1.157 +lemma%important Liminf_within:
   1.158    fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   1.159    shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
   1.160    unfolding Liminf_def eventually_at
   1.161 -proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
   1.162 +proof%unimportant (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
   1.163    fix P d
   1.164    assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   1.165    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   1.166 @@ -315,11 +316,11 @@
   1.167         (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
   1.168  qed
   1.169  
   1.170 -lemma Limsup_within:
   1.171 +lemma%important Limsup_within:
   1.172    fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   1.173    shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
   1.174    unfolding Limsup_def eventually_at
   1.175 -proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
   1.176 +proof%unimportant (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
   1.177    fix P d
   1.178    assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   1.179    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   1.180 @@ -359,7 +360,7 @@
   1.181    done
   1.182  
   1.183  
   1.184 -subsection \<open>Extended-Real.thy\<close>
   1.185 +subsection%important \<open>Extended-Real.thy\<close> (*FIX title *)
   1.186  
   1.187  lemma sum_constant_ereal:
   1.188    fixes a::ereal
   1.189 @@ -379,10 +380,10 @@
   1.190    ultimately show ?thesis by (metis (mono_tags, lifting) eventually_mono)
   1.191  qed
   1.192  
   1.193 -lemma ereal_Inf_cmult:
   1.194 +lemma%important ereal_Inf_cmult:
   1.195    assumes "c>(0::real)"
   1.196    shows "Inf {ereal c * x |x. P x} = ereal c * Inf {x. P x}"
   1.197 -proof -
   1.198 +proof%unimportant -
   1.199    have "(\<lambda>x::ereal. c * x) (Inf {x::ereal. P x}) = Inf ((\<lambda>x::ereal. c * x)`{x::ereal. P x})"
   1.200      apply (rule mono_bij_Inf)
   1.201      apply (simp add: assms ereal_mult_left_mono less_imp_le mono_def)
   1.202 @@ -393,7 +394,7 @@
   1.203  qed
   1.204  
   1.205  
   1.206 -subsubsection \<open>Continuity of addition\<close>
   1.207 +subsubsection%important \<open>Continuity of addition\<close>
   1.208  
   1.209  text \<open>The next few lemmas remove an unnecessary assumption in \verb+tendsto_add_ereal+, culminating
   1.210  in \verb+tendsto_add_ereal_general+ which essentially says that the addition
   1.211 @@ -401,12 +402,12 @@
   1.212  It is much more convenient in many situations, see for instance the proof of
   1.213  \verb+tendsto_sum_ereal+ below.\<close>
   1.214  
   1.215 -lemma tendsto_add_ereal_PInf:
   1.216 +lemma%important tendsto_add_ereal_PInf:
   1.217    fixes y :: ereal
   1.218    assumes y: "y \<noteq> -\<infinity>"
   1.219    assumes f: "(f \<longlongrightarrow> \<infinity>) F" and g: "(g \<longlongrightarrow> y) F"
   1.220    shows "((\<lambda>x. f x + g x) \<longlongrightarrow> \<infinity>) F"
   1.221 -proof -
   1.222 +proof%unimportant -
   1.223    have "\<exists>C. eventually (\<lambda>x. g x > ereal C) F"
   1.224    proof (cases y)
   1.225      case (real r)
   1.226 @@ -439,12 +440,12 @@
   1.227  that $-(x+y)$ is in general different from $(-x) + (-y)$ in ereal creates difficulties,
   1.228  so it is more efficient to copy the previous proof.\<close>
   1.229  
   1.230 -lemma tendsto_add_ereal_MInf:
   1.231 +lemma%important tendsto_add_ereal_MInf:
   1.232    fixes y :: ereal
   1.233    assumes y: "y \<noteq> \<infinity>"
   1.234    assumes f: "(f \<longlongrightarrow> -\<infinity>) F" and g: "(g \<longlongrightarrow> y) F"
   1.235    shows "((\<lambda>x. f x + g x) \<longlongrightarrow> -\<infinity>) F"
   1.236 -proof -
   1.237 +proof%unimportant -
   1.238    have "\<exists>C. eventually (\<lambda>x. g x < ereal C) F"
   1.239    proof (cases y)
   1.240      case (real r)
   1.241 @@ -472,12 +473,12 @@
   1.242    then show ?thesis by (simp add: tendsto_MInfty)
   1.243  qed
   1.244  
   1.245 -lemma tendsto_add_ereal_general1:
   1.246 +lemma%important tendsto_add_ereal_general1:
   1.247    fixes x y :: ereal
   1.248    assumes y: "\<bar>y\<bar> \<noteq> \<infinity>"
   1.249    assumes f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   1.250    shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   1.251 -proof (cases x)
   1.252 +proof%unimportant (cases x)
   1.253    case (real r)
   1.254    have a: "\<bar>x\<bar> \<noteq> \<infinity>" by (simp add: real)
   1.255    show ?thesis by (rule tendsto_add_ereal[OF a, OF y, OF f, OF g])
   1.256 @@ -490,12 +491,12 @@
   1.257      by (metis abs_ereal.simps(3) ereal_MInfty_eq_plus)
   1.258  qed
   1.259  
   1.260 -lemma tendsto_add_ereal_general2:
   1.261 +lemma%important tendsto_add_ereal_general2:
   1.262    fixes x y :: ereal
   1.263    assumes x: "\<bar>x\<bar> \<noteq> \<infinity>"
   1.264        and f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   1.265    shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   1.266 -proof -
   1.267 +proof%unimportant -
   1.268    have "((\<lambda>x. g x + f x) \<longlongrightarrow> x + y) F"
   1.269      using tendsto_add_ereal_general1[OF x, OF g, OF f] add.commute[of "y", of "x"] by simp
   1.270    moreover have "\<And>x. g x + f x = f x + g x" using add.commute by auto
   1.271 @@ -505,12 +506,12 @@
   1.272  text \<open>The next lemma says that the addition is continuous on ereal, except at
   1.273  the pairs $(-\infty, \infty)$ and $(\infty, -\infty)$.\<close>
   1.274  
   1.275 -lemma tendsto_add_ereal_general [tendsto_intros]:
   1.276 +lemma%important tendsto_add_ereal_general [tendsto_intros]:
   1.277    fixes x y :: ereal
   1.278    assumes "\<not>((x=\<infinity> \<and> y=-\<infinity>) \<or> (x=-\<infinity> \<and> y=\<infinity>))"
   1.279        and f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   1.280    shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   1.281 -proof (cases x)
   1.282 +proof%unimportant (cases x)
   1.283    case (real r)
   1.284    show ?thesis
   1.285      apply (rule tendsto_add_ereal_general2) using real assms by auto
   1.286 @@ -524,16 +525,16 @@
   1.287    then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
   1.288  qed
   1.289  
   1.290 -subsubsection \<open>Continuity of multiplication\<close>
   1.291 +subsubsection%important \<open>Continuity of multiplication\<close>
   1.292  
   1.293  text \<open>In the same way as for addition, we prove that the multiplication is continuous on
   1.294  ereal times ereal, except at $(\infty, 0)$ and $(-\infty, 0)$ and $(0, \infty)$ and $(0, -\infty)$,
   1.295  starting with specific situations.\<close>
   1.296  
   1.297 -lemma tendsto_mult_real_ereal:
   1.298 +lemma%important tendsto_mult_real_ereal:
   1.299    assumes "(u \<longlongrightarrow> ereal l) F" "(v \<longlongrightarrow> ereal m) F"
   1.300    shows "((\<lambda>n. u n * v n) \<longlongrightarrow> ereal l * ereal m) F"
   1.301 -proof -
   1.302 +proof%unimportant -
   1.303    have ureal: "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) F" by (rule real_lim_then_eventually_real[OF assms(1)])
   1.304    then have "((\<lambda>n. ereal(real_of_ereal(u n))) \<longlongrightarrow> ereal l) F" using assms by auto
   1.305    then have limu: "((\<lambda>n. real_of_ereal(u n)) \<longlongrightarrow> l) F" by auto
   1.306 @@ -553,11 +554,11 @@
   1.307    then show ?thesis using * filterlim_cong by fastforce
   1.308  qed
   1.309  
   1.310 -lemma tendsto_mult_ereal_PInf:
   1.311 +lemma%important tendsto_mult_ereal_PInf:
   1.312    fixes f g::"_ \<Rightarrow> ereal"
   1.313    assumes "(f \<longlongrightarrow> l) F" "l>0" "(g \<longlongrightarrow> \<infinity>) F"
   1.314    shows "((\<lambda>x. f x * g x) \<longlongrightarrow> \<infinity>) F"
   1.315 -proof -
   1.316 +proof%unimportant -
   1.317    obtain a::real where "0 < ereal a" "a < l" using assms(2) using ereal_dense2 by blast
   1.318    have *: "eventually (\<lambda>x. f x > a) F" using \<open>a < l\<close> assms(1) by (simp add: order_tendsto_iff)
   1.319    {
   1.320 @@ -581,11 +582,11 @@
   1.321    then show ?thesis by (auto simp add: tendsto_PInfty)
   1.322  qed
   1.323  
   1.324 -lemma tendsto_mult_ereal_pos:
   1.325 +lemma%important tendsto_mult_ereal_pos:
   1.326    fixes f g::"_ \<Rightarrow> ereal"
   1.327    assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "l>0" "m>0"
   1.328    shows "((\<lambda>x. f x * g x) \<longlongrightarrow> l * m) F"
   1.329 -proof (cases)
   1.330 +proof%unimportant (cases)
   1.331    assume *: "l = \<infinity> \<or> m = \<infinity>"
   1.332    then show ?thesis
   1.333    proof (cases)
   1.334 @@ -620,11 +621,11 @@
   1.335    shows "sgn(l) * sgn(l) = 1"
   1.336  apply (cases l) using assms by (auto simp add: one_ereal_def sgn_if)
   1.337  
   1.338 -lemma tendsto_mult_ereal [tendsto_intros]:
   1.339 +lemma%important tendsto_mult_ereal [tendsto_intros]:
   1.340    fixes f g::"_ \<Rightarrow> ereal"
   1.341    assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "\<not>((l=0 \<and> abs(m) = \<infinity>) \<or> (m=0 \<and> abs(l) = \<infinity>))"
   1.342    shows "((\<lambda>x. f x * g x) \<longlongrightarrow> l * m) F"
   1.343 -proof (cases)
   1.344 +proof%unimportant (cases)
   1.345    assume "l=0 \<or> m=0"
   1.346    then have "abs(l) \<noteq> \<infinity>" "abs(m) \<noteq> \<infinity>" using assms(3) by auto
   1.347    then obtain lr mr where "l = ereal lr" "m = ereal mr" by auto
   1.348 @@ -661,13 +662,13 @@
   1.349  by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
   1.350  
   1.351  
   1.352 -subsubsection \<open>Continuity of division\<close>
   1.353 +subsubsection%important \<open>Continuity of division\<close>
   1.354  
   1.355 -lemma tendsto_inverse_ereal_PInf:
   1.356 +lemma%important tendsto_inverse_ereal_PInf:
   1.357    fixes u::"_ \<Rightarrow> ereal"
   1.358    assumes "(u \<longlongrightarrow> \<infinity>) F"
   1.359    shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 0) F"
   1.360 -proof -
   1.361 +proof%unimportant -
   1.362    {
   1.363      fix e::real assume "e>0"
   1.364      have "1/e < \<infinity>" by auto
   1.365 @@ -704,11 +705,11 @@
   1.366    shows "(u \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. 1/ u x) \<longlongrightarrow> 1/l) F"
   1.367    using tendsto_inverse unfolding inverse_eq_divide .
   1.368  
   1.369 -lemma tendsto_inverse_ereal [tendsto_intros]:
   1.370 +lemma%important tendsto_inverse_ereal [tendsto_intros]:
   1.371    fixes u::"_ \<Rightarrow> ereal"
   1.372    assumes "(u \<longlongrightarrow> l) F" "l \<noteq> 0"
   1.373    shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 1/l) F"
   1.374 -proof (cases l)
   1.375 +proof%unimportant (cases l)
   1.376    case (real r)
   1.377    then have "r \<noteq> 0" using assms(2) by auto
   1.378    then have "1/l = ereal(1/r)" using real by (simp add: one_ereal_def)
   1.379 @@ -749,11 +750,11 @@
   1.380    then show ?thesis unfolding v_def using Lim_transform_eventually[OF *] \<open> 1/l = 0 \<close> by auto
   1.381  qed
   1.382  
   1.383 -lemma tendsto_divide_ereal [tendsto_intros]:
   1.384 +lemma%important tendsto_divide_ereal [tendsto_intros]:
   1.385    fixes f g::"_ \<Rightarrow> ereal"
   1.386    assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "m \<noteq> 0" "\<not>(abs(l) = \<infinity> \<and> abs(m) = \<infinity>)"
   1.387    shows "((\<lambda>x. f x / g x) \<longlongrightarrow> l / m) F"
   1.388 -proof -
   1.389 +proof%unimportant -
   1.390    define h where "h = (\<lambda>x. 1/ g x)"
   1.391    have *: "(h \<longlongrightarrow> 1/m) F" unfolding h_def using assms(2) assms(3) tendsto_inverse_ereal by auto
   1.392    have "((\<lambda>x. f x * h x) \<longlongrightarrow> l * (1/m)) F"
   1.393 @@ -764,15 +765,15 @@
   1.394  qed
   1.395  
   1.396  
   1.397 -subsubsection \<open>Further limits\<close>
   1.398 +subsubsection%important \<open>Further limits\<close>
   1.399  
   1.400  text \<open>The assumptions of @{thm tendsto_diff_ereal} are too strong, we weaken them here.\<close>
   1.401  
   1.402 -lemma tendsto_diff_ereal_general [tendsto_intros]:
   1.403 +lemma%important tendsto_diff_ereal_general [tendsto_intros]:
   1.404    fixes u v::"'a \<Rightarrow> ereal"
   1.405    assumes "(u \<longlongrightarrow> l) F" "(v \<longlongrightarrow> m) F" "\<not>((l = \<infinity> \<and> m = \<infinity>) \<or> (l = -\<infinity> \<and> m = -\<infinity>))"
   1.406    shows "((\<lambda>n. u n - v n) \<longlongrightarrow> l - m) F"
   1.407 -proof -
   1.408 +proof%unimportant -
   1.409    have "((\<lambda>n. u n + (-v n)) \<longlongrightarrow> l + (-m)) F"
   1.410      apply (intro tendsto_intros assms) using assms by (auto simp add: ereal_uminus_eq_reorder)
   1.411    then show ?thesis by (simp add: minus_ereal_def)
   1.412 @@ -782,11 +783,11 @@
   1.413    "(\<lambda> n::nat. real n) \<longlonglongrightarrow> \<infinity>"
   1.414  by (simp add: filterlim_real_sequentially tendsto_PInfty_eq_at_top)
   1.415  
   1.416 -lemma tendsto_at_top_pseudo_inverse [tendsto_intros]:
   1.417 +lemma%important tendsto_at_top_pseudo_inverse [tendsto_intros]:
   1.418    fixes u::"nat \<Rightarrow> nat"
   1.419    assumes "LIM n sequentially. u n :> at_top"
   1.420    shows "LIM n sequentially. Inf {N. u N \<ge> n} :> at_top"
   1.421 -proof -
   1.422 +proof%unimportant -
   1.423    {
   1.424      fix C::nat
   1.425      define M where "M = Max {u n| n. n \<le> C}+1"
   1.426 @@ -813,11 +814,11 @@
   1.427    then show ?thesis using filterlim_at_top by auto
   1.428  qed
   1.429  
   1.430 -lemma pseudo_inverse_finite_set:
   1.431 +lemma%important pseudo_inverse_finite_set:
   1.432    fixes u::"nat \<Rightarrow> nat"
   1.433    assumes "LIM n sequentially. u n :> at_top"
   1.434    shows "finite {N. u N \<le> n}"
   1.435 -proof -
   1.436 +proof%unimportant -
   1.437    fix n
   1.438    have "eventually (\<lambda>N. u N \<ge> n+1) sequentially" using assms
   1.439      by (simp add: filterlim_at_top)
   1.440 @@ -862,11 +863,11 @@
   1.441    then show ?thesis by auto
   1.442  qed
   1.443  
   1.444 -lemma ereal_truncation_real_top [tendsto_intros]:
   1.445 +lemma%important ereal_truncation_real_top [tendsto_intros]:
   1.446    fixes x::ereal
   1.447    assumes "x \<noteq> - \<infinity>"
   1.448    shows "(\<lambda>n::nat. real_of_ereal(min x n)) \<longlonglongrightarrow> x"
   1.449 -proof (cases x)
   1.450 +proof%unimportant (cases x)
   1.451    case (real r)
   1.452    then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   1.453    then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   1.454 @@ -880,10 +881,10 @@
   1.455    then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto
   1.456  qed (simp add: assms)
   1.457  
   1.458 -lemma ereal_truncation_bottom [tendsto_intros]:
   1.459 +lemma%important ereal_truncation_bottom [tendsto_intros]:
   1.460    fixes x::ereal
   1.461    shows "(\<lambda>n::nat. max x (- real n)) \<longlonglongrightarrow> x"
   1.462 -proof (cases x)
   1.463 +proof%unimportant (cases x)
   1.464    case (real r)
   1.465    then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   1.466    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
   1.467 @@ -901,11 +902,11 @@
   1.468    then show ?thesis by auto
   1.469  qed
   1.470  
   1.471 -lemma ereal_truncation_real_bottom [tendsto_intros]:
   1.472 +lemma%important ereal_truncation_real_bottom [tendsto_intros]:
   1.473    fixes x::ereal
   1.474    assumes "x \<noteq> \<infinity>"
   1.475    shows "(\<lambda>n::nat. real_of_ereal(max x (- real n))) \<longlonglongrightarrow> x"
   1.476 -proof (cases x)
   1.477 +proof%unimportant (cases x)
   1.478    case (real r)
   1.479    then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   1.480    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
   1.481 @@ -933,9 +934,9 @@
   1.482  qed(simp)
   1.483  
   1.484  
   1.485 -lemma continuous_ereal_abs:
   1.486 +lemma%important continuous_ereal_abs:
   1.487    "continuous_on (UNIV::ereal set) abs"
   1.488 -proof -
   1.489 +proof%unimportant -
   1.490    have "continuous_on ({..0} \<union> {(0::ereal)..}) abs"
   1.491      apply (rule continuous_on_closed_Un, auto)
   1.492      apply (rule iffD1[OF continuous_on_cong, of "{..0}" _ "\<lambda>x. -x"])
   1.493 @@ -960,7 +961,7 @@
   1.494  by (subst uminus_ereal.simps(1)[symmetric], intro tendsto_intros)
   1.495  
   1.496  
   1.497 -subsection \<open>Extended-Nonnegative-Real.thy\<close>
   1.498 +subsection%important \<open>Extended-Nonnegative-Real.thy\<close> (*FIX title *)
   1.499  
   1.500  lemma tendsto_diff_ennreal_general [tendsto_intros]:
   1.501    fixes u v::"'a \<Rightarrow> ennreal"
   1.502 @@ -972,11 +973,11 @@
   1.503    then show ?thesis by auto
   1.504  qed
   1.505  
   1.506 -lemma tendsto_mult_ennreal [tendsto_intros]:
   1.507 +lemma%important tendsto_mult_ennreal [tendsto_intros]:
   1.508    fixes l m::ennreal
   1.509    assumes "(u \<longlongrightarrow> l) F" "(v \<longlongrightarrow> m) F" "\<not>((l = 0 \<and> m = \<infinity>) \<or> (l = \<infinity> \<and> m = 0))"
   1.510    shows "((\<lambda>n. u n * v n) \<longlongrightarrow> l * m) F"
   1.511 -proof -
   1.512 +proof%unimportant -
   1.513    have "((\<lambda>n. e2ennreal(enn2ereal (u n) * enn2ereal (v n))) \<longlongrightarrow> e2ennreal(enn2ereal l * enn2ereal m)) F"
   1.514      apply (intro tendsto_intros) using assms apply auto
   1.515      using enn2ereal_inject zero_ennreal.rep_eq by fastforce+
   1.516 @@ -989,9 +990,9 @@
   1.517  qed
   1.518  
   1.519  
   1.520 -subsection \<open>monoset\<close>
   1.521 +subsection%important \<open>monoset\<close>
   1.522  
   1.523 -definition (in order) mono_set:
   1.524 +definition%important (in order) mono_set:
   1.525    "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
   1.526  
   1.527  lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
   1.528 @@ -999,11 +1000,11 @@
   1.529  lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
   1.530  lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
   1.531  
   1.532 -lemma (in complete_linorder) mono_set_iff:
   1.533 +lemma%important (in complete_linorder) mono_set_iff:
   1.534    fixes S :: "'a set"
   1.535    defines "a \<equiv> Inf S"
   1.536    shows "mono_set S \<longleftrightarrow> S = {a <..} \<or> S = {a..}" (is "_ = ?c")
   1.537 -proof
   1.538 +proof%unimportant
   1.539    assume "mono_set S"
   1.540    then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S"
   1.541      by (auto simp: mono_set)
   1.542 @@ -1045,12 +1046,12 @@
   1.543    by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
   1.544      ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
   1.545  
   1.546 -lemma ereal_Liminf_Sup_monoset:
   1.547 +lemma%important ereal_Liminf_Sup_monoset:
   1.548    fixes f :: "'a \<Rightarrow> ereal"
   1.549    shows "Liminf net f =
   1.550      Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
   1.551      (is "_ = Sup ?A")
   1.552 -proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
   1.553 +proof%unimportant (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
   1.554    fix P
   1.555    assume P: "eventually P net"
   1.556    fix S
   1.557 @@ -1084,12 +1085,12 @@
   1.558    qed
   1.559  qed
   1.560  
   1.561 -lemma ereal_Limsup_Inf_monoset:
   1.562 +lemma%important ereal_Limsup_Inf_monoset:
   1.563    fixes f :: "'a \<Rightarrow> ereal"
   1.564    shows "Limsup net f =
   1.565      Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
   1.566      (is "_ = Inf ?A")
   1.567 -proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
   1.568 +proof%unimportant (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
   1.569    fix P
   1.570    assume P: "eventually P net"
   1.571    fix S
   1.572 @@ -1123,11 +1124,11 @@
   1.573    qed
   1.574  qed
   1.575  
   1.576 -lemma liminf_bounded_open:
   1.577 +lemma%important liminf_bounded_open:
   1.578    fixes x :: "nat \<Rightarrow> ereal"
   1.579    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))"
   1.580    (is "_ \<longleftrightarrow> ?P x0")
   1.581 -proof
   1.582 +proof%unimportant
   1.583    assume "?P x0"
   1.584    then show "x0 \<le> liminf x"
   1.585      unfolding ereal_Liminf_Sup_monoset eventually_sequentially
   1.586 @@ -1161,11 +1162,11 @@
   1.587      by auto
   1.588  qed
   1.589  
   1.590 -lemma limsup_finite_then_bounded:
   1.591 +lemma%important limsup_finite_then_bounded:
   1.592    fixes u::"nat \<Rightarrow> real"
   1.593    assumes "limsup u < \<infinity>"
   1.594    shows "\<exists>C. \<forall>n. u n \<le> C"
   1.595 -proof -
   1.596 +proof%unimportant -
   1.597    obtain C where C: "limsup u < C" "C < \<infinity>" using assms ereal_dense2 by blast
   1.598    then have "C = ereal(real_of_ereal C)" using ereal_real by force
   1.599    have "eventually (\<lambda>n. u n < C) sequentially" using C(1) unfolding Limsup_def
   1.600 @@ -1275,11 +1276,11 @@
   1.601    then show ?case using Suc.IH by simp
   1.602  qed (auto)
   1.603  
   1.604 -lemma Limsup_obtain:
   1.605 +lemma%important Limsup_obtain:
   1.606    fixes u::"_ \<Rightarrow> 'a :: complete_linorder"
   1.607    assumes "Limsup F u > c"
   1.608    shows "\<exists>i. u i > c"
   1.609 -proof -
   1.610 +proof%unimportant -
   1.611    have "(INF P:{P. eventually P F}. SUP x:{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
   1.612    then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff)
   1.613  qed
   1.614 @@ -1287,10 +1288,10 @@
   1.615  text \<open>The next lemma is extremely useful, as it often makes it possible to reduce statements
   1.616  about limsups to statements about limits.\<close>
   1.617  
   1.618 -lemma limsup_subseq_lim:
   1.619 +lemma%important limsup_subseq_lim:
   1.620    fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   1.621    shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> limsup u"
   1.622 -proof (cases)
   1.623 +proof%unimportant (cases)
   1.624    assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<le> u p"
   1.625    then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<le> u (r n)) \<and> r n < r (Suc n)"
   1.626      by (intro dependent_nat_choice) (auto simp: conj_commute)
   1.627 @@ -1380,10 +1381,10 @@
   1.628    then show ?thesis using \<open>strict_mono r\<close> by auto
   1.629  qed
   1.630  
   1.631 -lemma liminf_subseq_lim:
   1.632 +lemma%important liminf_subseq_lim:
   1.633    fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   1.634    shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> liminf u"
   1.635 -proof (cases)
   1.636 +proof%unimportant (cases)
   1.637    assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<ge> u p"
   1.638    then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<ge> u (r n)) \<and> r n < r (Suc n)"
   1.639      by (intro dependent_nat_choice) (auto simp: conj_commute)
   1.640 @@ -1478,10 +1479,10 @@
   1.641  subsequences thanks to \verb+limsup_subseq_lim+. The statement for limits follows for instance from
   1.642  \verb+tendsto_add_ereal_general+.\<close>
   1.643  
   1.644 -lemma ereal_limsup_add_mono:
   1.645 +lemma%important ereal_limsup_add_mono:
   1.646    fixes u v::"nat \<Rightarrow> ereal"
   1.647    shows "limsup (\<lambda>n. u n + v n) \<le> limsup u + limsup v"
   1.648 -proof (cases)
   1.649 +proof%unimportant (cases)
   1.650    assume "(limsup u = \<infinity>) \<or> (limsup v = \<infinity>)"
   1.651    then have "limsup u + limsup v = \<infinity>" by simp
   1.652    then show ?thesis by auto
   1.653 @@ -1524,11 +1525,11 @@
   1.654  This explains why there are more assumptions in the next lemma dealing with liminfs that in the
   1.655  previous one about limsups.\<close>
   1.656  
   1.657 -lemma ereal_liminf_add_mono:
   1.658 +lemma%important ereal_liminf_add_mono:
   1.659    fixes u v::"nat \<Rightarrow> ereal"
   1.660    assumes "\<not>((liminf u = \<infinity> \<and> liminf v = -\<infinity>) \<or> (liminf u = -\<infinity> \<and> liminf v = \<infinity>))"
   1.661    shows "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
   1.662 -proof (cases)
   1.663 +proof%unimportant (cases)
   1.664    assume "(liminf u = -\<infinity>) \<or> (liminf v = -\<infinity>)"
   1.665    then have *: "liminf u + liminf v = -\<infinity>" using assms by auto
   1.666    show ?thesis by (simp add: *)
   1.667 @@ -1567,11 +1568,11 @@
   1.668    then show ?thesis unfolding w_def by simp
   1.669  qed
   1.670  
   1.671 -lemma ereal_limsup_lim_add:
   1.672 +lemma%important ereal_limsup_lim_add:
   1.673    fixes u v::"nat \<Rightarrow> ereal"
   1.674    assumes "u \<longlonglongrightarrow> a" "abs(a) \<noteq> \<infinity>"
   1.675    shows "limsup (\<lambda>n. u n + v n) = a + limsup v"
   1.676 -proof -
   1.677 +proof%unimportant -
   1.678    have "limsup u = a" using assms(1) using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
   1.679    have "(\<lambda>n. -u n) \<longlonglongrightarrow> -a" using assms(1) by auto
   1.680    then have "limsup (\<lambda>n. -u n) = -a" using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
   1.681 @@ -1598,11 +1599,11 @@
   1.682    then show ?thesis using up by simp
   1.683  qed
   1.684  
   1.685 -lemma ereal_limsup_lim_mult:
   1.686 +lemma%important ereal_limsup_lim_mult:
   1.687    fixes u v::"nat \<Rightarrow> ereal"
   1.688    assumes "u \<longlonglongrightarrow> a" "a>0" "a \<noteq> \<infinity>"
   1.689    shows "limsup (\<lambda>n. u n * v n) = a * limsup v"
   1.690 -proof -
   1.691 +proof%unimportant -
   1.692    define w where "w = (\<lambda>n. u n * v n)"
   1.693    obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
   1.694    have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
   1.695 @@ -1628,11 +1629,11 @@
   1.696    then show ?thesis using I unfolding w_def by auto
   1.697  qed
   1.698  
   1.699 -lemma ereal_liminf_lim_mult:
   1.700 +lemma%important ereal_liminf_lim_mult:
   1.701    fixes u v::"nat \<Rightarrow> ereal"
   1.702    assumes "u \<longlonglongrightarrow> a" "a>0" "a \<noteq> \<infinity>"
   1.703    shows "liminf (\<lambda>n. u n * v n) = a * liminf v"
   1.704 -proof -
   1.705 +proof%unimportant -
   1.706    define w where "w = (\<lambda>n. u n * v n)"
   1.707    obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
   1.708    have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
   1.709 @@ -1658,11 +1659,11 @@
   1.710    then show ?thesis using I unfolding w_def by auto
   1.711  qed
   1.712  
   1.713 -lemma ereal_liminf_lim_add:
   1.714 +lemma%important ereal_liminf_lim_add:
   1.715    fixes u v::"nat \<Rightarrow> ereal"
   1.716    assumes "u \<longlonglongrightarrow> a" "abs(a) \<noteq> \<infinity>"
   1.717    shows "liminf (\<lambda>n. u n + v n) = a + liminf v"
   1.718 -proof -
   1.719 +proof%unimportant -
   1.720    have "liminf u = a" using assms(1) tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
   1.721    then have *: "abs(liminf u) \<noteq> \<infinity>" using assms(2) by auto
   1.722    have "(\<lambda>n. -u n) \<longlonglongrightarrow> -a" using assms(1) by auto
   1.723 @@ -1691,10 +1692,10 @@
   1.724    then show ?thesis using up by simp
   1.725  qed
   1.726  
   1.727 -lemma ereal_liminf_limsup_add:
   1.728 +lemma%important ereal_liminf_limsup_add:
   1.729    fixes u v::"nat \<Rightarrow> ereal"
   1.730    shows "liminf (\<lambda>n. u n + v n) \<le> liminf u + limsup v"
   1.731 -proof (cases)
   1.732 +proof%unimportant (cases)
   1.733    assume "limsup v = \<infinity> \<or> liminf u = \<infinity>"
   1.734    then show ?thesis by auto
   1.735  next
   1.736 @@ -1743,12 +1744,12 @@
   1.737    done
   1.738  
   1.739  
   1.740 -lemma liminf_minus_ennreal:
   1.741 +lemma%important liminf_minus_ennreal:
   1.742    fixes u v::"nat \<Rightarrow> ennreal"
   1.743    shows "(\<And>n. v n \<le> u n) \<Longrightarrow> liminf (\<lambda>n. u n - v n) \<le> limsup u - limsup v"
   1.744    unfolding liminf_SUP_INF limsup_INF_SUP
   1.745    including ennreal.lifting
   1.746 -proof (transfer, clarsimp)
   1.747 +proof%unimportant (transfer, clarsimp)
   1.748    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"
   1.749    moreover have "0 \<le> limsup u - limsup v"
   1.750      using * by (intro ereal_diff_positive Limsup_mono always_eventually) simp
   1.751 @@ -1761,7 +1762,7 @@
   1.752      by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
   1.753  qed
   1.754  
   1.755 -subsection "Relate extended reals and the indicator function"
   1.756 +subsection%unimportant "Relate extended reals and the indicator function"
   1.757  
   1.758  lemma ereal_indicator_le_0: "(indicator S x::ereal) \<le> 0 \<longleftrightarrow> x \<notin> S"
   1.759    by (auto split: split_indicator simp: one_ereal_def)