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