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