src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
author hoelzl
Thu Jan 31 11:31:30 2013 +0100 (2013-01-31)
changeset 51000 c9adb50f74ad
parent 50104 de19856feb54
child 51329 4a3c453f99a1
permissions -rw-r--r--
use order topology for extended reals
     1 (*  Title:      HOL/Multivariate_Analysis/Extended_Real_Limits.thy
     2     Author:     Johannes Hölzl, TU München
     3     Author:     Robert Himmelmann, TU München
     4     Author:     Armin Heller, TU München
     5     Author:     Bogdan Grechuk, University of Edinburgh
     6 *)
     7 
     8 header {* Limits on the Extended real number line *}
     9 
    10 theory Extended_Real_Limits
    11   imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real"
    12 begin
    13 
    14 lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
    15   unfolding continuous_on_topological open_ereal_def by auto
    16 
    17 lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal"
    18   using continuous_on_eq_continuous_at[of UNIV] by auto
    19 
    20 lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
    21   using continuous_on_eq_continuous_within[of A] by auto
    22 
    23 lemma ereal_open_uminus:
    24   fixes S :: "ereal set"
    25   assumes "open S"
    26   shows "open (uminus ` S)"
    27   unfolding open_ereal_def
    28 proof (intro conjI impI)
    29   obtain x y where
    30     S: "open (ereal -` S)" "\<infinity> \<in> S \<Longrightarrow> {ereal x<..} \<subseteq> S" "-\<infinity> \<in> S \<Longrightarrow> {..< ereal y} \<subseteq> S"
    31     using `open S` unfolding open_ereal_def by auto
    32   have "ereal -` uminus ` S = uminus ` (ereal -` S)"
    33   proof safe
    34     fix x y
    35     assume "ereal x = - y" "y \<in> S"
    36     then show "x \<in> uminus ` ereal -` S" by (cases y) auto
    37   next
    38     fix x
    39     assume "ereal x \<in> S"
    40     then show "- x \<in> ereal -` uminus ` S"
    41       by (auto intro: image_eqI[of _ _ "ereal x"])
    42   qed
    43   then show "open (ereal -` uminus ` S)"
    44     using S by (auto intro: open_negations)
    45   { assume "\<infinity> \<in> uminus ` S"
    46     then have "-\<infinity> \<in> S" by (metis image_iff ereal_uminus_uminus)
    47     then have "uminus ` {..<ereal y} \<subseteq> uminus ` S" using S by (intro image_mono) auto
    48     then show "\<exists>x. {ereal x<..} \<subseteq> uminus ` S" using ereal_uminus_lessThan by auto }
    49   { assume "-\<infinity> \<in> uminus ` S"
    50     then have "\<infinity> : S" by (metis image_iff ereal_uminus_uminus)
    51     then have "uminus ` {ereal x<..} <= uminus ` S" using S by (intro image_mono) auto
    52     then show "\<exists>y. {..<ereal y} <= uminus ` S" using ereal_uminus_greaterThan by auto }
    53 qed
    54 
    55 lemma ereal_uminus_complement:
    56   fixes S :: "ereal set"
    57   shows "uminus ` (- S) = - uminus ` S"
    58   by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
    59 
    60 lemma ereal_closed_uminus:
    61   fixes S :: "ereal set"
    62   assumes "closed S"
    63   shows "closed (uminus ` S)"
    64   using assms unfolding closed_def
    65   using ereal_open_uminus[of "- S"] ereal_uminus_complement by auto
    66 
    67 instance ereal :: perfect_space
    68 proof (default, rule)
    69   fix a :: ereal assume a: "open {a}"
    70   show False
    71   proof (cases a)
    72     case MInf
    73     then obtain y where "{..<ereal y} <= {a}" using a open_MInfty2[of "{a}"] by auto
    74     then have "ereal(y - 1):{a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
    75     then show False using `a=(-\<infinity>)` by auto
    76   next
    77     case PInf
    78     then obtain y where "{ereal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto
    79     then have "ereal(y+1):{a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
    80     then show False using `a=\<infinity>` by auto
    81   next
    82     case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
    83     from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
    84     then obtain b where b_def: "a<b & b<a+e"
    85       using fin ereal_between ereal_dense[of a "a+e"] by auto
    86     then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
    87     then show False using b_def e by auto
    88   qed
    89 qed
    90 
    91 lemma ereal_closed_contains_Inf:
    92   fixes S :: "ereal set"
    93   assumes "closed S" "S ~= {}"
    94   shows "Inf S : S"
    95 proof (rule ccontr)
    96   assume "Inf S \<notin> S"
    97   then have a: "open (-S)" "Inf S:(- S)" using assms by auto
    98   show False
    99   proof (cases "Inf S")
   100     case MInf
   101     then have "(-\<infinity>) : - S" using a by auto
   102     then obtain y where "{..<ereal y} <= (-S)" using a open_MInfty2[of "- S"] by auto
   103     then have "ereal y <= Inf S" by (metis Compl_anti_mono Compl_lessThan atLeast_iff
   104       complete_lattice_class.Inf_greatest double_complement set_rev_mp)
   105     then show False using MInf by auto
   106   next
   107     case PInf
   108     then have "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))
   109     then show False using `Inf S ~: S` by (simp add: top_ereal_def)
   110   next
   111     case (real r)
   112     then have fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" by simp
   113     from ereal_open_cont_interval[OF a this] guess e . note e = this
   114     { fix x
   115       assume "x:S" then have "x>=Inf S" by (rule complete_lattice_class.Inf_lower)
   116       then have *: "x>Inf S-e" using e by (metis fin ereal_between(1) order_less_le_trans)
   117       { assume "x<Inf S+e"
   118         then have "x:{Inf S-e <..< Inf S+e}" using * by auto
   119         then have False using e `x:S` by auto
   120       } then have "x>=Inf S+e" by (metis linorder_le_less_linear)
   121     }
   122     then have "Inf S + e <= Inf S" by (metis le_Inf_iff)
   123     then show False using real e by (cases e) auto
   124   qed
   125 qed
   126 
   127 lemma ereal_closed_contains_Sup:
   128   fixes S :: "ereal set"
   129   assumes "closed S" "S ~= {}"
   130   shows "Sup S : S"
   131 proof -
   132   have "closed (uminus ` S)"
   133     by (metis assms(1) ereal_closed_uminus)
   134   then have "Inf (uminus ` S) : uminus ` S"
   135     using assms ereal_closed_contains_Inf[of "uminus ` S"] by auto
   136   then have "- Sup S : uminus ` S"
   137     using ereal_Sup_uminus_image_eq[of "uminus ` S"] by (auto simp: image_image)
   138   then show ?thesis
   139     by (metis imageI ereal_uminus_uminus ereal_minus_minus_image)
   140 qed
   141 
   142 lemma ereal_open_closed_aux:
   143   fixes S :: "ereal set"
   144   assumes "open S" "closed S"
   145     and S: "(-\<infinity>) ~: S"
   146   shows "S = {}"
   147 proof (rule ccontr)
   148   assume "S ~= {}"
   149   then have *: "(Inf S):S" by (metis assms(2) ereal_closed_contains_Inf)
   150   { assume "Inf S=(-\<infinity>)"
   151     then have False using * assms(3) by auto }
   152   moreover
   153   { assume "Inf S=\<infinity>"
   154     then have "S={\<infinity>}" by (metis Inf_eq_PInfty `S ~= {}`)
   155     then have False by (metis assms(1) not_open_singleton) }
   156   moreover
   157   { assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
   158     from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this
   159     then obtain b where b_def: "Inf S-e<b & b<Inf S"
   160       using fin ereal_between[of "Inf S" e] ereal_dense[of "Inf S-e"] by auto
   161     then have "b: {Inf S-e <..< Inf S+e}" using e fin ereal_between[of "Inf S" e]
   162       by auto
   163     then have "b:S" using e by auto
   164     then have False using b_def by (metis complete_lattice_class.Inf_lower leD)
   165   } ultimately show False by auto
   166 qed
   167 
   168 lemma ereal_open_closed:
   169   fixes S :: "ereal set"
   170   shows "(open S & closed S) <-> (S = {} | S = UNIV)"
   171 proof -
   172   { assume lhs: "open S & closed S"
   173     { assume "(-\<infinity>) ~: S"
   174       then have "S={}" using lhs ereal_open_closed_aux by auto }
   175     moreover
   176     { assume "(-\<infinity>) : S"
   177       then have "(- S)={}" using lhs ereal_open_closed_aux[of "-S"] by auto }
   178     ultimately have "S = {} | S = UNIV" by auto
   179   } then show ?thesis by auto
   180 qed
   181 
   182 lemma ereal_open_affinity_pos:
   183   fixes S :: "ereal set"
   184   assumes "open S" and m: "m \<noteq> \<infinity>" "0 < m" and t: "\<bar>t\<bar> \<noteq> \<infinity>"
   185   shows "open ((\<lambda>x. m * x + t) ` S)"
   186 proof -
   187   obtain r where r[simp]: "m = ereal r" using m by (cases m) auto
   188   obtain p where p[simp]: "t = ereal p" using t by auto
   189   have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0" using m by auto
   190   from `open S`[THEN ereal_openE] guess l u . note T = this
   191   let ?f = "(\<lambda>x. m * x + t)"
   192   show ?thesis
   193     unfolding open_ereal_def
   194   proof (intro conjI impI exI subsetI)
   195     have "ereal -` ?f ` S = (\<lambda>x. r * x + p) ` (ereal -` S)"
   196     proof safe
   197       fix x y
   198       assume "ereal y = m * x + t" "x \<in> S"
   199       then show "y \<in> (\<lambda>x. r * x + p) ` ereal -` S"
   200         using `r \<noteq> 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm)
   201     qed force
   202     then show "open (ereal -` ?f ` S)"
   203       using open_affinity[OF T(1) `r \<noteq> 0`] by (auto simp: ac_simps)
   204   next
   205     assume "\<infinity> \<in> ?f`S"
   206     with `0 < r` have "\<infinity> \<in> S" by auto
   207     fix x
   208     assume "x \<in> {ereal (r * l + p)<..}"
   209     then have [simp]: "ereal (r * l + p) < x" by auto
   210     show "x \<in> ?f`S"
   211     proof (rule image_eqI)
   212       show "x = m * ((x - t) / m) + t"
   213         using m t by (cases rule: ereal3_cases[of m x t]) auto
   214       have "ereal l < (x - t)/m"
   215         using m t by (simp add: ereal_less_divide_pos ereal_less_minus)
   216       then show "(x - t)/m \<in> S" using T(2)[OF `\<infinity> \<in> S`] by auto
   217     qed
   218   next
   219     assume "-\<infinity> \<in> ?f`S" with `0 < r` have "-\<infinity> \<in> S" by auto
   220     fix x assume "x \<in> {..<ereal (r * u + p)}"
   221     then have [simp]: "x < ereal (r * u + p)" by auto
   222     show "x \<in> ?f`S"
   223     proof (rule image_eqI)
   224       show "x = m * ((x - t) / m) + t"
   225         using m t by (cases rule: ereal3_cases[of m x t]) auto
   226       have "(x - t)/m < ereal u"
   227         using m t by (simp add: ereal_divide_less_pos ereal_minus_less)
   228       then show "(x - t)/m \<in> S" using T(3)[OF `-\<infinity> \<in> S`] by auto
   229     qed
   230   qed
   231 qed
   232 
   233 lemma ereal_open_affinity:
   234   fixes S :: "ereal set"
   235   assumes "open S"
   236     and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0"
   237     and t: "\<bar>t\<bar> \<noteq> \<infinity>"
   238   shows "open ((\<lambda>x. m * x + t) ` S)"
   239 proof cases
   240   assume "0 < m"
   241   then show ?thesis
   242     using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m by auto
   243 next
   244   assume "\<not> 0 < m" then
   245   have "0 < -m" using `m \<noteq> 0` by (cases m) auto
   246   then have m: "-m \<noteq> \<infinity>" "0 < -m" using `\<bar>m\<bar> \<noteq> \<infinity>`
   247     by (auto simp: ereal_uminus_eq_reorder)
   248   from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t]
   249   show ?thesis unfolding image_image by simp
   250 qed
   251 
   252 lemma ereal_lim_mult:
   253   fixes X :: "'a \<Rightarrow> ereal"
   254   assumes lim: "(X ---> L) net"
   255     and a: "\<bar>a\<bar> \<noteq> \<infinity>"
   256   shows "((\<lambda>i. a * X i) ---> a * L) net"
   257 proof cases
   258   assume "a \<noteq> 0"
   259   show ?thesis
   260   proof (rule topological_tendstoI)
   261     fix S
   262     assume "open S" "a * L \<in> S"
   263     have "a * L / a = L"
   264       using `a \<noteq> 0` a by (cases rule: ereal2_cases[of a L]) auto
   265     then have L: "L \<in> ((\<lambda>x. x / a) ` S)"
   266       using `a * L \<in> S` by (force simp: image_iff)
   267     moreover have "open ((\<lambda>x. x / a) ` S)"
   268       using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a
   269       by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps)
   270     note * = lim[THEN topological_tendstoD, OF this L]
   271     { fix x
   272       from a `a \<noteq> 0` have "a * (x / a) = x"
   273         by (cases rule: ereal2_cases[of a x]) auto }
   274     note this[simp]
   275     show "eventually (\<lambda>x. a * X x \<in> S) net"
   276       by (rule eventually_mono[OF _ *]) auto
   277   qed
   278 qed auto
   279 
   280 lemma ereal_lim_uminus:
   281   fixes X :: "'a \<Rightarrow> ereal"
   282   shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net"
   283   using ereal_lim_mult[of X L net "ereal (-1)"]
   284     ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"]
   285   by (auto simp add: algebra_simps)
   286 
   287 lemma Lim_bounded2_ereal:
   288   assumes lim:"f ----> (l :: ereal)"
   289     and ge: "ALL n>=N. f n >= C"
   290   shows "l>=C"
   291   using ge
   292   by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
   293      (auto simp: eventually_sequentially)
   294 
   295 lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
   296 proof
   297   assume "x = -\<infinity>" then have "{x..} = UNIV" by auto
   298   then show "open {x..}" by auto
   299 next
   300   assume "open {x..}"
   301   then have "open {x..} \<and> closed {x..}" by auto
   302   then have "{x..} = UNIV" unfolding ereal_open_closed by auto
   303   then show "x = -\<infinity>" by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
   304 qed
   305 
   306 lemma ereal_open_mono_set:
   307   fixes S :: "ereal set"
   308   shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})"
   309   by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
   310     ereal_open_closed mono_set_iff open_ereal_greaterThan)
   311 
   312 lemma ereal_closed_mono_set:
   313   fixes S :: "ereal set"
   314   shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
   315   by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
   316     ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
   317 
   318 lemma ereal_Liminf_Sup_monoset:
   319   fixes f :: "'a => ereal"
   320   shows "Liminf net f =
   321     Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
   322     (is "_ = Sup ?A")
   323 proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
   324   fix P assume P: "eventually P net"
   325   fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
   326   { fix x assume "P x"
   327     then have "INFI (Collect P) f \<le> f x"
   328       by (intro complete_lattice_class.INF_lower) simp
   329     with S have "f x \<in> S"
   330       by (simp add: mono_set) }
   331   with P show "eventually (\<lambda>x. f x \<in> S) net"
   332     by (auto elim: eventually_elim1)
   333 next
   334   fix y l
   335   assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   336   assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
   337   show "l \<le> y"
   338   proof (rule ereal_le_ereal)
   339     fix B assume "B < l"
   340     then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
   341       by (intro S[rule_format]) auto
   342     then have "INFI {x. B < f x} f \<le> y"
   343       using P by auto
   344     moreover have "B \<le> INFI {x. B < f x} f"
   345       by (intro INF_greatest) auto
   346     ultimately show "B \<le> y"
   347       by simp
   348   qed
   349 qed
   350 
   351 lemma ereal_Limsup_Inf_monoset:
   352   fixes f :: "'a => ereal"
   353   shows "Limsup net f =
   354     Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
   355     (is "_ = Inf ?A")
   356 proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
   357   fix P assume P: "eventually P net"
   358   fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
   359   { fix x assume "P x"
   360     then have "f x \<le> SUPR (Collect P) f"
   361       by (intro complete_lattice_class.SUP_upper) simp
   362     with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
   363     have "f x \<in> S"
   364       by (simp add: inj_image_mem_iff) }
   365   with P show "eventually (\<lambda>x. f x \<in> S) net"
   366     by (auto elim: eventually_elim1)
   367 next
   368   fix y l
   369   assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   370   assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
   371   show "y \<le> l"
   372   proof (rule ereal_ge_ereal, safe)
   373     fix B assume "l < B"
   374     then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
   375       by (intro S[rule_format]) auto
   376     then have "y \<le> SUPR {x. f x < B} f"
   377       using P by auto
   378     moreover have "SUPR {x. f x < B} f \<le> B"
   379       by (intro SUP_least) auto
   380     ultimately show "y \<le> B"
   381       by simp
   382   qed
   383 qed
   384 
   385 lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)"
   386   using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto
   387 
   388 lemma ereal_Limsup_uminus:
   389   fixes f :: "'a => ereal"
   390   shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
   391 proof -
   392   { fix P l
   393     have "(\<exists>x. (l::ereal) = -x \<and> P x) \<longleftrightarrow> P (-l)"
   394       by (auto intro!: exI[of _ "-l"]) }
   395   note Ex_cancel = this
   396   { fix P :: "ereal set \<Rightarrow> bool"
   397     have "(\<forall>S. P S) \<longleftrightarrow> (\<forall>S. P (uminus`S))"
   398       apply auto
   399       apply (erule_tac x="uminus`S" in allE)
   400       apply (auto simp: image_image)
   401       done }
   402   note add_uminus_image = this
   403   { fix x S
   404     have "(x::ereal) \<in> uminus`S \<longleftrightarrow> -x\<in>S"
   405       by (auto intro!: image_eqI[of _ _ "-x"]) }
   406   note remove_uminus_image = this
   407   show ?thesis
   408     unfolding ereal_Limsup_Inf_monoset ereal_Liminf_Sup_monoset
   409     unfolding ereal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel
   410     by (subst add_uminus_image) (simp add: open_uminus_iff remove_uminus_image)
   411 qed
   412 
   413 lemma ereal_Liminf_uminus:
   414   fixes f :: "'a => ereal"
   415   shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)"
   416   using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
   417 
   418 lemma ereal_Lim_uminus:
   419   fixes f :: "'a \<Rightarrow> ereal"
   420   shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net"
   421   using
   422     ereal_lim_mult[of f f0 net "- 1"]
   423     ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
   424   by (auto simp: ereal_uminus_reorder)
   425 
   426 lemma lim_imp_Limsup:
   427   fixes f :: "'a => ereal"
   428   assumes "\<not> trivial_limit net"
   429     and lim: "(f ---> f0) net"
   430   shows "Limsup net f = f0"
   431   using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]
   432      ereal_Liminf_uminus[of net f] assms by simp
   433 
   434 lemma convergent_ereal_limsup:
   435   fixes X :: "nat \<Rightarrow> ereal"
   436   shows "convergent X \<Longrightarrow> limsup X = lim X"
   437   by (auto simp: convergent_def limI lim_imp_Limsup)
   438 
   439 lemma Liminf_PInfty:
   440   fixes f :: "'a \<Rightarrow> ereal"
   441   assumes "\<not> trivial_limit net"
   442   shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
   443 proof (intro lim_imp_Liminf iffI assms)
   444   assume rhs: "Liminf net f = \<infinity>"
   445   show "(f ---> \<infinity>) net"
   446     unfolding tendsto_PInfty
   447   proof
   448     fix r :: real
   449     have "ereal r < top" unfolding top_ereal_def by simp
   450     with rhs obtain P where "eventually P net" "r < INFI (Collect P) f"
   451       unfolding Liminf_def SUP_eq_top_iff top_ereal_def[symmetric] by auto
   452     then show "eventually (\<lambda>x. ereal r < f x) net"
   453       by (auto elim!: eventually_elim1 dest: less_INF_D)
   454   qed
   455 qed
   456 
   457 lemma Limsup_MInfty:
   458   fixes f :: "'a \<Rightarrow> ereal"
   459   assumes "\<not> trivial_limit net"
   460   shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
   461   using assms ereal_Lim_uminus[of f "-\<infinity>"] Liminf_PInfty[of _ "\<lambda>x. - (f x)"]
   462         ereal_Liminf_uminus[of _ f] by (auto simp: ereal_uminus_eq_reorder)
   463 
   464 lemma ereal_Liminf_eq_Limsup:
   465   fixes f :: "'a \<Rightarrow> ereal"
   466   assumes ntriv: "\<not> trivial_limit net"
   467     and lim: "Liminf net f = f0" "Limsup net f = f0"
   468   shows "(f ---> f0) net"
   469 proof (cases f0)
   470   case PInf
   471   then show ?thesis using Liminf_PInfty[OF ntriv] lim by auto
   472 next
   473   case MInf
   474   then show ?thesis using Limsup_MInfty[OF ntriv] lim by auto
   475 next
   476   case (real r)
   477   show "(f ---> f0) net"
   478   proof (rule topological_tendstoI)
   479     fix S
   480     assume "open S" "f0 \<in> S"
   481     then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
   482       using ereal_open_cont_interval2[of S f0] real lim by auto
   483     then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
   484       unfolding Liminf_def Limsup_def less_SUP_iff INF_less_iff
   485       by (auto intro!: eventually_conj elim: eventually_elim1 dest: less_INF_D SUP_lessD)
   486     with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
   487       by (rule_tac eventually_mono) auto
   488   qed
   489 qed
   490 
   491 lemma ereal_Liminf_eq_Limsup_iff:
   492   fixes f :: "'a \<Rightarrow> ereal"
   493   assumes "\<not> trivial_limit net"
   494   shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
   495   by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
   496 
   497 lemma convergent_ereal:
   498   fixes X :: "nat \<Rightarrow> ereal"
   499   shows "convergent X \<longleftrightarrow> limsup X = liminf X"
   500   using ereal_Liminf_eq_Limsup_iff[of sequentially]
   501   by (auto simp: convergent_def)
   502 
   503 lemma limsup_INFI_SUPR:
   504   fixes f :: "nat \<Rightarrow> ereal"
   505   shows "limsup f = (INF n. SUP m:{n..}. f m)"
   506   using ereal_Limsup_uminus[of sequentially "\<lambda>x. - f x"]
   507   by (simp add: liminf_SUPR_INFI ereal_INFI_uminus ereal_SUPR_uminus)
   508 
   509 lemma liminf_PInfty:
   510   fixes X :: "nat => ereal"
   511   shows "X ----> \<infinity> <-> liminf X = \<infinity>"
   512   by (metis Liminf_PInfty trivial_limit_sequentially)
   513 
   514 lemma limsup_MInfty:
   515   fixes X :: "nat => ereal"
   516   shows "X ----> (-\<infinity>) <-> limsup X = (-\<infinity>)"
   517   by (metis Limsup_MInfty trivial_limit_sequentially)
   518 
   519 lemma ereal_lim_mono:
   520   fixes X Y :: "nat => ereal"
   521   assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
   522     and "X ----> x" "Y ----> y"
   523   shows "x <= y"
   524   using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
   525 
   526 lemma incseq_le_ereal:
   527   fixes X :: "nat \<Rightarrow> ereal"
   528   assumes inc: "incseq X" and lim: "X ----> L"
   529   shows "X N \<le> L"
   530   using inc by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
   531 
   532 lemma decseq_ge_ereal:
   533   assumes dec: "decseq X"
   534     and lim: "X ----> (L::ereal)"
   535   shows "X N >= L"
   536   using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
   537 
   538 lemma liminf_bounded_open:
   539   fixes x :: "nat \<Rightarrow> ereal"
   540   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))"
   541   (is "_ \<longleftrightarrow> ?P x0")
   542 proof
   543   assume "?P x0"
   544   then show "x0 \<le> liminf x"
   545     unfolding ereal_Liminf_Sup_monoset eventually_sequentially
   546     by (intro complete_lattice_class.Sup_upper) auto
   547 next
   548   assume "x0 \<le> liminf x"
   549   { fix S :: "ereal set"
   550     assume om: "open S & mono_set S & x0:S"
   551     { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }
   552     moreover
   553     { assume "~(S=UNIV)"
   554       then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
   555       then have "B<x0" using om by auto
   556       then have "EX N. ALL n>=N. x n : S"
   557         unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
   558     }
   559     ultimately have "EX N. (ALL n>=N. x n : S)" by auto
   560   }
   561   then show "?P x0" by auto
   562 qed
   563 
   564 lemma limsup_subseq_mono:
   565   fixes X :: "nat \<Rightarrow> ereal"
   566   assumes "subseq r"
   567   shows "limsup (X \<circ> r) \<le> limsup X"
   568 proof -
   569   have "(\<lambda>n. - X n) \<circ> r = (\<lambda>n. - (X \<circ> r) n)" by (simp add: fun_eq_iff)
   570   then have "- limsup X \<le> - limsup (X \<circ> r)"
   571      using liminf_subseq_mono[of r "(%n. - X n)"]
   572        ereal_Liminf_uminus[of sequentially X]
   573        ereal_Liminf_uminus[of sequentially "X o r"] assms by auto
   574   then show ?thesis by auto
   575 qed
   576 
   577 lemma bounded_abs:
   578   assumes "(a::real)<=x" "x<=b"
   579   shows "abs x <= max (abs a) (abs b)"
   580   by (metis abs_less_iff assms leI le_max_iff_disj
   581     less_eq_real_def less_le_not_le less_minus_iff minus_minus)
   582 
   583 lemma lim_ereal_increasing:
   584   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
   585   obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
   586 proof
   587   show "f ----> (SUP n. f n)"
   588     using assms
   589     by (intro increasing_tendsto)
   590        (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
   591 qed
   592 
   593 lemma lim_ereal_decreasing:
   594   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
   595   obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
   596 proof
   597   show "f ----> (INF n. f n)"
   598     using assms
   599     by (intro decreasing_tendsto)
   600        (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
   601 qed
   602 
   603 lemma compact_ereal:
   604   fixes X :: "nat \<Rightarrow> ereal"
   605   shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
   606 proof -
   607   obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
   608     using seq_monosub[of X] unfolding comp_def by auto
   609   then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
   610     by (auto simp add: monoseq_def)
   611   then obtain l where "(X\<circ>r) ----> l"
   612      using lim_ereal_increasing[of "X \<circ> r"] lim_ereal_decreasing[of "X \<circ> r"] by auto
   613   then show ?thesis using `subseq r` by auto
   614 qed
   615 
   616 lemma ereal_Sup_lim:
   617   assumes "\<And>n. b n \<in> s" "b ----> (a::ereal)"
   618   shows "a \<le> Sup s"
   619   by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
   620 
   621 lemma ereal_Inf_lim:
   622   assumes "\<And>n. b n \<in> s" "b ----> (a::ereal)"
   623   shows "Inf s \<le> a"
   624   by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
   625 
   626 lemma SUP_Lim_ereal:
   627   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
   628   assumes inc: "incseq X" and l: "X ----> l"
   629   shows "(SUP n. X n) = l"
   630   using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] by simp
   631 
   632 lemma INF_Lim_ereal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::ereal)"
   633   using SUP_Lim_ereal[of "\<lambda>i. - X i" "- l"]
   634   by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
   635 
   636 lemma LIMSEQ_ereal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: ereal)"
   637   using LIMSEQ_SUP[of "\<lambda>i. - X i"]
   638   by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
   639 
   640 lemma SUP_eq_LIMSEQ:
   641   assumes "mono f"
   642   shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
   643 proof
   644   have inc: "incseq (\<lambda>i. ereal (f i))"
   645     using `mono f` unfolding mono_def incseq_def by auto
   646   { assume "f ----> x"
   647     then have "(\<lambda>i. ereal (f i)) ----> ereal x" by auto
   648     from SUP_Lim_ereal[OF inc this]
   649     show "(SUP n. ereal (f n)) = ereal x" . }
   650   { assume "(SUP n. ereal (f n)) = ereal x"
   651     with LIMSEQ_SUP[OF inc]
   652     show "f ----> x" by auto }
   653 qed
   654 
   655 lemma Liminf_within:
   656   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   657   shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
   658   unfolding Liminf_def eventually_within
   659 proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
   660   fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
   661   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   662     by (auto simp: zero_less_dist_iff dist_commute)
   663   then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
   664     by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
   665 next
   666   fix d :: real assume "0 < d"
   667   then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   668     INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
   669     by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   670        (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
   671 qed
   672 
   673 lemma Limsup_within:
   674   fixes f :: "'a::metric_space => 'b::complete_lattice"
   675   shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
   676   unfolding Limsup_def eventually_within
   677 proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
   678   fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
   679   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   680     by (auto simp: zero_less_dist_iff dist_commute)
   681   then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
   682     by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
   683 next
   684   fix d :: real assume "0 < d"
   685   then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   686     SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
   687     by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   688        (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
   689 qed
   690 
   691 lemma Liminf_within_UNIV:
   692   fixes f :: "'a::metric_space => _"
   693   shows "Liminf (at x) f = Liminf (at x within UNIV) f"
   694   by simp (* TODO: delete *)
   695 
   696 
   697 lemma Liminf_at:
   698   fixes f :: "'a::metric_space => _"
   699   shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
   700   using Liminf_within[of x UNIV f] by simp
   701 
   702 
   703 lemma Limsup_within_UNIV:
   704   fixes f :: "'a::metric_space => _"
   705   shows "Limsup (at x) f = Limsup (at x within UNIV) f"
   706   by simp (* TODO: delete *)
   707 
   708 
   709 lemma Limsup_at:
   710   fixes f :: "'a::metric_space => _"
   711   shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
   712   using Limsup_within[of x UNIV f] by simp
   713 
   714 lemma Lim_within_constant:
   715   assumes "ALL y:S. f y = C"
   716   shows "(f ---> C) (at x within S)"
   717   unfolding tendsto_def Limits.eventually_within eventually_at_topological
   718   using assms by simp (metis open_UNIV UNIV_I)
   719 
   720 lemma Liminf_within_constant:
   721   fixes f :: "'a::topological_space \<Rightarrow> ereal"
   722   assumes "ALL y:S. f y = C"
   723     and "~trivial_limit (at x within S)"
   724   shows "Liminf (at x within S) f = C"
   725   by (metis Lim_within_constant assms lim_imp_Liminf)
   726 
   727 lemma Limsup_within_constant:
   728   fixes f :: "'a::topological_space \<Rightarrow> ereal"
   729   assumes "ALL y:S. f y = C"
   730     and "~trivial_limit (at x within S)"
   731   shows "Limsup (at x within S) f = C"
   732   by (metis Lim_within_constant assms lim_imp_Limsup)
   733 
   734 lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
   735   unfolding islimpt_def by blast
   736 
   737 
   738 lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
   739   unfolding closure_def using islimpt_punctured by blast
   740 
   741 
   742 lemma not_trivial_limit_within: "~trivial_limit (at x within S) = (x:closure(S-{x}))"
   743   using islimpt_in_closure by (metis trivial_limit_within)
   744 
   745 
   746 lemma not_trivial_limit_within_ball:
   747   "(~trivial_limit (at x within S)) = (ALL e>0. S Int ball x e - {x} ~= {})"
   748   (is "?lhs = ?rhs")
   749 proof -
   750   { assume "?lhs"
   751     { fix e :: real
   752       assume "e>0"
   753       then obtain y where "y:(S-{x}) & dist y x < e"
   754         using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
   755         by auto
   756       then have "y : (S Int ball x e - {x})"
   757         unfolding ball_def by (simp add: dist_commute)
   758       then have "S Int ball x e - {x} ~= {}" by blast
   759     } then have "?rhs" by auto
   760   }
   761   moreover
   762   { assume "?rhs"
   763     { fix e :: real
   764       assume "e>0"
   765       then obtain y where "y : (S Int ball x e - {x})" using `?rhs` by blast
   766       then have "y:(S-{x}) & dist y x < e"
   767         unfolding ball_def by (simp add: dist_commute)
   768       then have "EX y:(S-{x}). dist y x < e" by auto
   769     }
   770     then have "?lhs"
   771       using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
   772   }
   773   ultimately show ?thesis by auto
   774 qed
   775 
   776 lemma liminf_ereal_cminus:
   777   fixes f :: "nat \<Rightarrow> ereal"
   778   assumes "c \<noteq> -\<infinity>"
   779   shows "liminf (\<lambda>x. c - f x) = c - limsup f"
   780 proof (cases c)
   781   case PInf
   782   then show ?thesis by (simp add: Liminf_const)
   783 next
   784   case (real r)
   785   then show ?thesis
   786     unfolding liminf_SUPR_INFI limsup_INFI_SUPR
   787     apply (subst INFI_ereal_cminus)
   788     apply auto
   789     apply (subst SUPR_ereal_cminus)
   790     apply auto
   791     done
   792 qed (insert `c \<noteq> -\<infinity>`, simp)
   793 
   794 
   795 subsubsection {* Continuity *}
   796 
   797 lemma continuous_imp_tendsto:
   798   assumes "continuous (at x0) f"
   799     and "x ----> x0"
   800   shows "(f o x) ----> (f x0)"
   801 proof -
   802   { fix S
   803     assume "open S & (f x0):S"
   804     then obtain T where T_def: "open T & x0 : T & (ALL x:T. f x : S)"
   805        using assms continuous_at_open by metis
   806     then have "(EX N. ALL n>=N. x n : T)"
   807       using assms tendsto_explicit T_def by auto
   808     then have "(EX N. ALL n>=N. f(x n) : S)" using T_def by auto
   809   }
   810   then show ?thesis using tendsto_explicit[of "f o x" "f x0"] by auto
   811 qed
   812 
   813 
   814 lemma continuous_at_sequentially2:
   815   fixes f :: "'a::metric_space => 'b:: topological_space"
   816   shows "continuous (at x0) f <-> (ALL x. (x ----> x0) --> (f o x) ----> (f x0))"
   817 proof -
   818   { assume "~(continuous (at x0) f)"
   819     then obtain T where
   820       T_def: "open T & f x0 : T & (ALL S. (open S & x0 : S) --> (EX x':S. f x' ~: T))"
   821       using continuous_at_open[of x0 f] by metis
   822     def X == "{x'. f x' ~: T}"
   823     then have "x0 islimpt X"
   824       unfolding islimpt_def using T_def by auto
   825     then obtain x where x_def: "(ALL n. x n : X) & x ----> x0"
   826       using islimpt_sequential[of x0 X] by auto
   827     then have "~(f o x) ----> (f x0)"
   828       unfolding tendsto_explicit using X_def T_def by auto
   829     then have "EX x. x ----> x0 & (~(f o x) ----> (f x0))" using x_def by auto
   830   }
   831   then show ?thesis using continuous_imp_tendsto by auto
   832 qed
   833 
   834 lemma continuous_at_of_ereal:
   835   fixes x0 :: ereal
   836   assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
   837   shows "continuous (at x0) real"
   838 proof -
   839   { fix T
   840     assume T_def: "open T & real x0 : T"
   841     def S == "ereal ` T"
   842     then have "ereal (real x0) : S" using T_def by auto
   843     then have "x0 : S" using assms ereal_real by auto
   844     moreover have "open S" using open_ereal S_def T_def by auto
   845     moreover have "ALL y:S. real y : T" using S_def T_def by auto
   846     ultimately have "EX S. x0 : S & open S & (ALL y:S. real y : T)" by auto
   847   }
   848   then show ?thesis unfolding continuous_at_open by blast
   849 qed
   850 
   851 
   852 lemma continuous_at_iff_ereal:
   853   fixes f :: "'a::t2_space => real"
   854   shows "continuous (at x0) f <-> continuous (at x0) (ereal o f)"
   855 proof -
   856   { assume "continuous (at x0) f"
   857     then have "continuous (at x0) (ereal o f)"
   858       using continuous_at_ereal continuous_at_compose[of x0 f ereal] by auto
   859   }
   860   moreover
   861   { assume "continuous (at x0) (ereal o f)"
   862     then have "continuous (at x0) (real o (ereal o f))"
   863       using continuous_at_of_ereal by (intro continuous_at_compose[of x0 "ereal o f"]) auto
   864     moreover have "real o (ereal o f) = f" using real_ereal_id by (simp add: o_assoc)
   865     ultimately have "continuous (at x0) f" by auto
   866   } ultimately show ?thesis by auto
   867 qed
   868 
   869 
   870 lemma continuous_on_iff_ereal:
   871   fixes f :: "'a::t2_space => real"
   872   fixes A assumes "open A"
   873   shows "continuous_on A f <-> continuous_on A (ereal o f)"
   874   using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at)
   875 
   876 
   877 lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>::ereal)}) real"
   878   using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal by auto
   879 
   880 
   881 lemma continuous_on_iff_real:
   882   fixes f :: "'a::t2_space => ereal"
   883   assumes "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
   884   shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
   885 proof -
   886   have "f ` A <= UNIV-{\<infinity>,(-\<infinity>)}" using assms by force
   887   then have *: "continuous_on (f ` A) real"
   888     using continuous_on_real by (simp add: continuous_on_subset)
   889   have **: "continuous_on ((real o f) ` A) ereal"
   890     using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real o f) ` A"] by blast
   891   { assume "continuous_on A f"
   892     then have "continuous_on A (real o f)"
   893       apply (subst continuous_on_compose)
   894       using * apply auto
   895       done
   896   }
   897   moreover
   898   { assume "continuous_on A (real o f)"
   899     then have "continuous_on A (ereal o (real o f))"
   900       apply (subst continuous_on_compose)
   901       using ** apply auto
   902       done
   903     then have "continuous_on A f"
   904       apply (subst continuous_on_eq[of A "ereal o (real o f)" f])
   905       using assms ereal_real apply auto
   906       done
   907   }
   908   ultimately show ?thesis by auto
   909 qed
   910 
   911 
   912 lemma continuous_at_const:
   913   fixes f :: "'a::t2_space => ereal"
   914   assumes "ALL x. (f x = C)"
   915   shows "ALL x. continuous (at x) f"
   916   unfolding continuous_at_open using assms t1_space by auto
   917 
   918 
   919 lemma closure_contains_Inf:
   920   fixes S :: "real set"
   921   assumes "S ~= {}" "EX B. ALL x:S. B<=x"
   922   shows "Inf S : closure S"
   923 proof -
   924   have *: "ALL x:S. Inf S <= x"
   925     using Inf_lower_EX[of _ S] assms by metis
   926   { fix e
   927     assume "e>(0 :: real)"
   928     then obtain x where x_def: "x:S & x < Inf S + e" using Inf_close `S ~= {}` by auto
   929     moreover then have "x > Inf S - e" using * by auto
   930     ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
   931     then have "EX x:S. abs (x - Inf S) < e" using x_def by auto
   932   }
   933   then show ?thesis
   934     apply (subst closure_approachable)
   935     unfolding dist_norm apply auto
   936     done
   937 qed
   938 
   939 
   940 lemma closed_contains_Inf:
   941   fixes S :: "real set"
   942   assumes "S ~= {}" "EX B. ALL x:S. B<=x"
   943     and "closed S"
   944   shows "Inf S : S"
   945   by (metis closure_contains_Inf closure_closed assms)
   946 
   947 
   948 lemma mono_closed_real:
   949   fixes S :: "real set"
   950   assumes mono: "ALL y z. y:S & y<=z --> z:S"
   951     and "closed S"
   952   shows "S = {} | S = UNIV | (EX a. S = {a ..})"
   953 proof -
   954   { assume "S ~= {}"
   955     { assume ex: "EX B. ALL x:S. B<=x"
   956       then have *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] ex by metis
   957       then have "Inf S : S" apply (subst closed_contains_Inf) using ex `S ~= {}` `closed S` by auto
   958       then have "ALL x. (Inf S <= x <-> x:S)" using mono[rule_format, of "Inf S"] * by auto
   959       then have "S = {Inf S ..}" by auto
   960       then have "EX a. S = {a ..}" by auto
   961     }
   962     moreover
   963     { assume "~(EX B. ALL x:S. B<=x)"
   964       then have nex: "ALL B. EX x:S. x<B" by (simp add: not_le)
   965       { fix y
   966         obtain x where "x:S & x < y" using nex by auto
   967         then have "y:S" using mono[rule_format, of x y] by auto
   968       } then have "S = UNIV" by auto
   969     }
   970     ultimately have "S = UNIV | (EX a. S = {a ..})" by blast
   971   } then show ?thesis by blast
   972 qed
   973 
   974 
   975 lemma mono_closed_ereal:
   976   fixes S :: "real set"
   977   assumes mono: "ALL y z. y:S & y<=z --> z:S"
   978     and "closed S"
   979   shows "EX a. S = {x. a <= ereal x}"
   980 proof -
   981   { assume "S = {}"
   982     then have ?thesis apply(rule_tac x=PInfty in exI) by auto }
   983   moreover
   984   { assume "S = UNIV"
   985     then have ?thesis apply(rule_tac x="-\<infinity>" in exI) by auto }
   986   moreover
   987   { assume "EX a. S = {a ..}"
   988     then obtain a where "S={a ..}" by auto
   989     then have ?thesis apply(rule_tac x="ereal a" in exI) by auto
   990   }
   991   ultimately show ?thesis using mono_closed_real[of S] assms by auto
   992 qed
   993 
   994 subsection {* Sums *}
   995 
   996 lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
   997 proof cases
   998   assume "finite A"
   999   then show ?thesis by induct auto
  1000 qed simp
  1001 
  1002 lemma setsum_Pinfty:
  1003   fixes f :: "'a \<Rightarrow> ereal"
  1004   shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))"
  1005 proof safe
  1006   assume *: "setsum f P = \<infinity>"
  1007   show "finite P"
  1008   proof (rule ccontr) assume "infinite P" with * show False by auto qed
  1009   show "\<exists>i\<in>P. f i = \<infinity>"
  1010   proof (rule ccontr)
  1011     assume "\<not> ?thesis" then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>" by auto
  1012     from `finite P` this have "setsum f P \<noteq> \<infinity>"
  1013       by induct auto
  1014     with * show False by auto
  1015   qed
  1016 next
  1017   fix i assume "finite P" "i \<in> P" "f i = \<infinity>"
  1018   then show "setsum f P = \<infinity>"
  1019   proof induct
  1020     case (insert x A)
  1021     show ?case using insert by (cases "x = i") auto
  1022   qed simp
  1023 qed
  1024 
  1025 lemma setsum_Inf:
  1026   fixes f :: "'a \<Rightarrow> ereal"
  1027   shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>))"
  1028 proof
  1029   assume *: "\<bar>setsum f A\<bar> = \<infinity>"
  1030   have "finite A" by (rule ccontr) (insert *, auto)
  1031   moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>"
  1032   proof (rule ccontr)
  1033     assume "\<not> ?thesis" then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto
  1034     from bchoice[OF this] guess r ..
  1035     with * show False by auto
  1036   qed
  1037   ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" by auto
  1038 next
  1039   assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
  1040   then obtain i where "finite A" "i \<in> A" "\<bar>f i\<bar> = \<infinity>" by auto
  1041   then show "\<bar>setsum f A\<bar> = \<infinity>"
  1042   proof induct
  1043     case (insert j A) then show ?case
  1044       by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
  1045   qed simp
  1046 qed
  1047 
  1048 lemma setsum_real_of_ereal:
  1049   fixes f :: "'i \<Rightarrow> ereal"
  1050   assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
  1051   shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
  1052 proof -
  1053   have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
  1054   proof
  1055     fix x assume "x \<in> S"
  1056     from assms[OF this] show "\<exists>r. f x = ereal r" by (cases "f x") auto
  1057   qed
  1058   from bchoice[OF this] guess r ..
  1059   then show ?thesis by simp
  1060 qed
  1061 
  1062 lemma setsum_ereal_0:
  1063   fixes f :: "'a \<Rightarrow> ereal" assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
  1064   shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
  1065 proof
  1066   assume *: "(\<Sum>x\<in>A. f x) = 0"
  1067   then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>" by auto
  1068   then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>" using assms by (force simp: setsum_Pinfty)
  1069   then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto
  1070   from bchoice[OF this] * assms show "\<forall>i\<in>A. f i = 0"
  1071     using setsum_nonneg_eq_0_iff[of A "\<lambda>i. real (f i)"] by auto
  1072 qed (rule setsum_0')
  1073 
  1074 
  1075 lemma setsum_ereal_right_distrib:
  1076   fixes f :: "'a \<Rightarrow> ereal"
  1077   assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
  1078   shows "r * setsum f A = (\<Sum>n\<in>A. r * f n)"
  1079 proof cases
  1080   assume "finite A"
  1081   then show ?thesis using assms
  1082     by induct (auto simp: ereal_right_distrib setsum_nonneg)
  1083 qed simp
  1084 
  1085 lemma sums_ereal_positive:
  1086   fixes f :: "nat \<Rightarrow> ereal"
  1087   assumes "\<And>i. 0 \<le> f i"
  1088   shows "f sums (SUP n. \<Sum>i<n. f i)"
  1089 proof -
  1090   have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
  1091     using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)
  1092   from LIMSEQ_SUP[OF this]
  1093   show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)
  1094 qed
  1095 
  1096 lemma summable_ereal_pos:
  1097   fixes f :: "nat \<Rightarrow> ereal"
  1098   assumes "\<And>i. 0 \<le> f i"
  1099   shows "summable f"
  1100   using sums_ereal_positive[of f, OF assms] unfolding summable_def by auto
  1101 
  1102 lemma suminf_ereal_eq_SUPR:
  1103   fixes f :: "nat \<Rightarrow> ereal"
  1104   assumes "\<And>i. 0 \<le> f i"
  1105   shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
  1106   using sums_ereal_positive[of f, OF assms, THEN sums_unique] by simp
  1107 
  1108 lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
  1109   unfolding sums_def by simp
  1110 
  1111 lemma suminf_bound:
  1112   fixes f :: "nat \<Rightarrow> ereal"
  1113   assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x" and pos: "\<And>n. 0 \<le> f n"
  1114   shows "suminf f \<le> x"
  1115 proof (rule Lim_bounded_ereal)
  1116   have "summable f" using pos[THEN summable_ereal_pos] .
  1117   then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
  1118     by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
  1119   show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
  1120     using assms by auto
  1121 qed
  1122 
  1123 lemma suminf_bound_add:
  1124   fixes f :: "nat \<Rightarrow> ereal"
  1125   assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
  1126     and pos: "\<And>n. 0 \<le> f n"
  1127     and "y \<noteq> -\<infinity>"
  1128   shows "suminf f + y \<le> x"
  1129 proof (cases y)
  1130   case (real r)
  1131   then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
  1132     using assms by (simp add: ereal_le_minus)
  1133   then have "(\<Sum> n. f n) \<le> x - y" using pos by (rule suminf_bound)
  1134   then show "(\<Sum> n. f n) + y \<le> x"
  1135     using assms real by (simp add: ereal_le_minus)
  1136 qed (insert assms, auto)
  1137 
  1138 lemma suminf_upper:
  1139   fixes f :: "nat \<Rightarrow> ereal"
  1140   assumes "\<And>n. 0 \<le> f n"
  1141   shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
  1142   unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
  1143   by (auto intro: complete_lattice_class.Sup_upper)
  1144 
  1145 lemma suminf_0_le:
  1146   fixes f :: "nat \<Rightarrow> ereal"
  1147   assumes "\<And>n. 0 \<le> f n"
  1148   shows "0 \<le> (\<Sum>n. f n)"
  1149   using suminf_upper[of f 0, OF assms] by simp
  1150 
  1151 lemma suminf_le_pos:
  1152   fixes f g :: "nat \<Rightarrow> ereal"
  1153   assumes "\<And>N. f N \<le> g N" "\<And>N. 0 \<le> f N"
  1154   shows "suminf f \<le> suminf g"
  1155 proof (safe intro!: suminf_bound)
  1156   fix n
  1157   { fix N have "0 \<le> g N" using assms(2,1)[of N] by auto }
  1158   have "setsum f {..<n} \<le> setsum g {..<n}"
  1159     using assms by (auto intro: setsum_mono)
  1160   also have "... \<le> suminf g" using `\<And>N. 0 \<le> g N` by (rule suminf_upper)
  1161   finally show "setsum f {..<n} \<le> suminf g" .
  1162 qed (rule assms(2))
  1163 
  1164 lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal)^Suc n) = 1"
  1165   using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
  1166   by (simp add: one_ereal_def)
  1167 
  1168 lemma suminf_add_ereal:
  1169   fixes f g :: "nat \<Rightarrow> ereal"
  1170   assumes "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
  1171   shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
  1172   apply (subst (1 2 3) suminf_ereal_eq_SUPR)
  1173   unfolding setsum_addf
  1174   apply (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
  1175   done
  1176 
  1177 lemma suminf_cmult_ereal:
  1178   fixes f g :: "nat \<Rightarrow> ereal"
  1179   assumes "\<And>i. 0 \<le> f i" "0 \<le> a"
  1180   shows "(\<Sum>i. a * f i) = a * suminf f"
  1181   by (auto simp: setsum_ereal_right_distrib[symmetric] assms
  1182                  ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR
  1183            intro!: SUPR_ereal_cmult )
  1184 
  1185 lemma suminf_PInfty:
  1186   fixes f :: "nat \<Rightarrow> ereal"
  1187   assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>"
  1188   shows "f i \<noteq> \<infinity>"
  1189 proof -
  1190   from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
  1191   have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>" by auto
  1192   then show ?thesis unfolding setsum_Pinfty by simp
  1193 qed
  1194 
  1195 lemma suminf_PInfty_fun:
  1196   assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>"
  1197   shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
  1198 proof -
  1199   have "\<forall>i. \<exists>r. f i = ereal r"
  1200   proof
  1201     fix i show "\<exists>r. f i = ereal r"
  1202       using suminf_PInfty[OF assms] assms(1)[of i] by (cases "f i") auto
  1203   qed
  1204   from choice[OF this] show ?thesis by auto
  1205 qed
  1206 
  1207 lemma summable_ereal:
  1208   assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
  1209   shows "summable f"
  1210 proof -
  1211   have "0 \<le> (\<Sum>i. ereal (f i))"
  1212     using assms by (intro suminf_0_le) auto
  1213   with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
  1214     by (cases "\<Sum>i. ereal (f i)") auto
  1215   from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
  1216   have "summable (\<lambda>x. ereal (f x))" using assms by auto
  1217   from summable_sums[OF this]
  1218   have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))" by auto
  1219   then show "summable f"
  1220     unfolding r sums_ereal summable_def ..
  1221 qed
  1222 
  1223 lemma suminf_ereal:
  1224   assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
  1225   shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
  1226 proof (rule sums_unique[symmetric])
  1227   from summable_ereal[OF assms]
  1228   show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
  1229     unfolding sums_ereal using assms by (intro summable_sums summable_ereal)
  1230 qed
  1231 
  1232 lemma suminf_ereal_minus:
  1233   fixes f g :: "nat \<Rightarrow> ereal"
  1234   assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i" and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
  1235   shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
  1236 proof -
  1237   { fix i have "0 \<le> f i" using ord[of i] by auto }
  1238   moreover
  1239   from suminf_PInfty_fun[OF `\<And>i. 0 \<le> f i` fin(1)] guess f' .. note this[simp]
  1240   from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] guess g' .. note this[simp]
  1241   { fix i have "0 \<le> f i - g i" using ord[of i] by (auto simp: ereal_le_minus_iff) }
  1242   moreover
  1243   have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
  1244     using assms by (auto intro!: suminf_le_pos simp: field_simps)
  1245   then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>" using fin by auto
  1246   ultimately show ?thesis using assms `\<And>i. 0 \<le> f i`
  1247     apply simp
  1248     apply (subst (1 2 3) suminf_ereal)
  1249     apply (auto intro!: suminf_diff[symmetric] summable_ereal)
  1250     done
  1251 qed
  1252 
  1253 lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
  1254 proof -
  1255   have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)" by (rule suminf_upper) auto
  1256   then show ?thesis by simp
  1257 qed
  1258 
  1259 lemma summable_real_of_ereal:
  1260   fixes f :: "nat \<Rightarrow> ereal"
  1261   assumes f: "\<And>i. 0 \<le> f i"
  1262     and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
  1263   shows "summable (\<lambda>i. real (f i))"
  1264 proof (rule summable_def[THEN iffD2])
  1265   have "0 \<le> (\<Sum>i. f i)" using assms by (auto intro: suminf_0_le)
  1266   with fin obtain r where r: "ereal r = (\<Sum>i. f i)" by (cases "(\<Sum>i. f i)") auto
  1267   { fix i have "f i \<noteq> \<infinity>" using f by (intro suminf_PInfty[OF _ fin]) auto
  1268     then have "\<bar>f i\<bar> \<noteq> \<infinity>" using f[of i] by auto }
  1269   note fin = this
  1270   have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
  1271     using f by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
  1272   also have "\<dots> = ereal r" using fin r by (auto simp: ereal_real)
  1273   finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" by (auto simp: sums_ereal)
  1274 qed
  1275 
  1276 lemma suminf_SUP_eq:
  1277   fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
  1278   assumes "\<And>i. incseq (\<lambda>n. f n i)" "\<And>n i. 0 \<le> f n i"
  1279   shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
  1280 proof -
  1281   { fix n :: nat
  1282     have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
  1283       using assms by (auto intro!: SUPR_ereal_setsum[symmetric]) }
  1284   note * = this
  1285   show ?thesis using assms
  1286     apply (subst (1 2) suminf_ereal_eq_SUPR)
  1287     unfolding *
  1288     apply (auto intro!: SUP_upper2)
  1289     apply (subst SUP_commute)
  1290     apply rule
  1291     done
  1292 qed
  1293 
  1294 lemma suminf_setsum_ereal:
  1295   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
  1296   assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
  1297   shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
  1298 proof cases
  1299   assume "finite A"
  1300   then show ?thesis using nonneg
  1301     by induct (simp_all add: suminf_add_ereal setsum_nonneg)
  1302 qed simp
  1303 
  1304 lemma suminf_ereal_eq_0:
  1305   fixes f :: "nat \<Rightarrow> ereal"
  1306   assumes nneg: "\<And>i. 0 \<le> f i"
  1307   shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
  1308 proof
  1309   assume "(\<Sum>i. f i) = 0"
  1310   { fix i assume "f i \<noteq> 0"
  1311     with nneg have "0 < f i" by (auto simp: less_le)
  1312     also have "f i = (\<Sum>j. if j = i then f i else 0)"
  1313       by (subst suminf_finite[where N="{i}"]) auto
  1314     also have "\<dots> \<le> (\<Sum>i. f i)"
  1315       using nneg by (auto intro!: suminf_le_pos)
  1316     finally have False using `(\<Sum>i. f i) = 0` by auto }
  1317   then show "\<forall>i. f i = 0" by auto
  1318 qed simp
  1319 
  1320 end