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