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