src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
author wenzelm
Sun Nov 02 17:09:04 2014 +0100 (2014-11-02)
changeset 58877 262572d90bc6
parent 57865 dcfb33c26f50
child 59000 6eb0725503fc
permissions -rw-r--r--
modernized header;
     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 section {* Limits on the Extended real number line *}
     9 
    10 theory Extended_Real_Limits
    11   imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
    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 limsup_le_liminf_real:
   443   fixes X :: "nat \<Rightarrow> real" and L :: real
   444   assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X"
   445   shows "X ----> L"
   446 proof -
   447   from 1 2 have "limsup X \<le> liminf X" by auto
   448   hence 3: "limsup X = liminf X"  
   449     apply (subst eq_iff, rule conjI)
   450     by (rule Liminf_le_Limsup, auto)
   451   hence 4: "convergent (\<lambda>n. ereal (X n))"
   452     by (subst convergent_ereal)
   453   hence "limsup X = lim (\<lambda>n. ereal(X n))"
   454     by (rule convergent_limsup_cl)
   455   also from 1 2 3 have "limsup X = L" by auto
   456   finally have "lim (\<lambda>n. ereal(X n)) = L" ..
   457   hence "(\<lambda>n. ereal (X n)) ----> L"
   458     apply (elim subst)
   459     by (subst convergent_LIMSEQ_iff [symmetric], rule 4) 
   460   thus ?thesis by simp
   461 qed
   462 
   463 lemma liminf_PInfty:
   464   fixes X :: "nat \<Rightarrow> ereal"
   465   shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
   466   by (metis Liminf_PInfty trivial_limit_sequentially)
   467 
   468 lemma limsup_MInfty:
   469   fixes X :: "nat \<Rightarrow> ereal"
   470   shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
   471   by (metis Limsup_MInfty trivial_limit_sequentially)
   472 
   473 lemma ereal_lim_mono:
   474   fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
   475   assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
   476     and "X ----> x"
   477     and "Y ----> y"
   478   shows "x \<le> y"
   479   using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
   480 
   481 lemma incseq_le_ereal:
   482   fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
   483   assumes inc: "incseq X"
   484     and lim: "X ----> L"
   485   shows "X N \<le> L"
   486   using inc
   487   by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
   488 
   489 lemma decseq_ge_ereal:
   490   assumes dec: "decseq X"
   491     and lim: "X ----> (L::'a::linorder_topology)"
   492   shows "X N \<ge> L"
   493   using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
   494 
   495 lemma bounded_abs:
   496   fixes a :: real
   497   assumes "a \<le> x"
   498     and "x \<le> b"
   499   shows "abs x \<le> max (abs a) (abs b)"
   500   by (metis abs_less_iff assms leI le_max_iff_disj
   501     less_eq_real_def less_le_not_le less_minus_iff minus_minus)
   502 
   503 lemma ereal_Sup_lim:
   504   fixes a :: "'a::{complete_linorder,linorder_topology}"
   505   assumes "\<And>n. b n \<in> s"
   506     and "b ----> a"
   507   shows "a \<le> Sup s"
   508   by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
   509 
   510 lemma ereal_Inf_lim:
   511   fixes a :: "'a::{complete_linorder,linorder_topology}"
   512   assumes "\<And>n. b n \<in> s"
   513     and "b ----> a"
   514   shows "Inf s \<le> a"
   515   by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
   516 
   517 lemma SUP_Lim_ereal:
   518   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   519   assumes inc: "incseq X"
   520     and l: "X ----> l"
   521   shows "(SUP n. X n) = l"
   522   using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
   523   by simp
   524 
   525 lemma INF_Lim_ereal:
   526   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   527   assumes dec: "decseq X"
   528     and l: "X ----> l"
   529   shows "(INF n. X n) = l"
   530   using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
   531   by simp
   532 
   533 lemma SUP_eq_LIMSEQ:
   534   assumes "mono f"
   535   shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
   536 proof
   537   have inc: "incseq (\<lambda>i. ereal (f i))"
   538     using `mono f` unfolding mono_def incseq_def by auto
   539   {
   540     assume "f ----> x"
   541     then have "(\<lambda>i. ereal (f i)) ----> ereal x"
   542       by auto
   543     from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
   544   next
   545     assume "(SUP n. ereal (f n)) = ereal x"
   546     with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
   547   }
   548 qed
   549 
   550 lemma liminf_ereal_cminus:
   551   fixes f :: "nat \<Rightarrow> ereal"
   552   assumes "c \<noteq> -\<infinity>"
   553   shows "liminf (\<lambda>x. c - f x) = c - limsup f"
   554 proof (cases c)
   555   case PInf
   556   then show ?thesis
   557     by (simp add: Liminf_const)
   558 next
   559   case (real r)
   560   then show ?thesis
   561     unfolding liminf_SUP_INF limsup_INF_SUP
   562     apply (subst INF_ereal_cminus)
   563     apply auto
   564     apply (subst SUP_ereal_cminus)
   565     apply auto
   566     done
   567 qed (insert `c \<noteq> -\<infinity>`, simp)
   568 
   569 
   570 subsubsection {* Continuity *}
   571 
   572 lemma continuous_at_of_ereal:
   573   fixes x0 :: ereal
   574   assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
   575   shows "continuous (at x0) real"
   576 proof -
   577   {
   578     fix T
   579     assume T: "open T" "real x0 \<in> T"
   580     def S \<equiv> "ereal ` T"
   581     then have "ereal (real x0) \<in> S"
   582       using T by auto
   583     then have "x0 \<in> S"
   584       using assms ereal_real by auto
   585     moreover have "open S"
   586       using open_ereal S_def T by auto
   587     moreover have "\<forall>y\<in>S. real y \<in> T"
   588       using S_def T by auto
   589     ultimately have "\<exists>S. x0 \<in> S \<and> open S \<and> (\<forall>y\<in>S. real y \<in> T)"
   590       by auto
   591   }
   592   then show ?thesis
   593     unfolding continuous_at_open by blast
   594 qed
   595 
   596 lemma nhds_ereal: "nhds (ereal r) = filtermap ereal (nhds r)"
   597   by (simp add: filtermap_nhds_open_map open_ereal continuous_at_of_ereal)
   598 
   599 lemma at_ereal: "at (ereal r) = filtermap ereal (at r)"
   600   by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
   601 
   602 lemma at_left_ereal: "at_left (ereal r) = filtermap ereal (at_left r)"
   603   by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
   604 
   605 lemma at_right_ereal: "at_right (ereal r) = filtermap ereal (at_right r)"
   606   by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
   607 
   608 lemma
   609   shows at_left_PInf: "at_left \<infinity> = filtermap ereal at_top"
   610     and at_right_MInf: "at_right (-\<infinity>) = filtermap ereal at_bot"
   611   unfolding filter_eq_iff eventually_filtermap eventually_at_top_dense eventually_at_bot_dense
   612     eventually_at_left[OF ereal_less(5)] eventually_at_right[OF ereal_less(6)]
   613   by (auto simp add: ereal_all_split ereal_ex_split)
   614 
   615 lemma ereal_tendsto_simps1:
   616   "((f \<circ> real) ---> y) (at_left (ereal x)) \<longleftrightarrow> (f ---> y) (at_left x)"
   617   "((f \<circ> real) ---> y) (at_right (ereal x)) \<longleftrightarrow> (f ---> y) (at_right x)"
   618   "((f \<circ> real) ---> y) (at_left (\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_top"
   619   "((f \<circ> real) ---> y) (at_right (-\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_bot"
   620   unfolding tendsto_compose_filtermap at_left_ereal at_right_ereal at_left_PInf at_right_MInf
   621   by (auto simp: filtermap_filtermap filtermap_ident)
   622 
   623 lemma ereal_tendsto_simps2:
   624   "((ereal \<circ> f) ---> ereal a) F \<longleftrightarrow> (f ---> a) F"
   625   "((ereal \<circ> f) ---> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)"
   626   "((ereal \<circ> f) ---> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)"
   627   unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
   628   using lim_ereal by (simp_all add: comp_def)
   629 
   630 lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
   631 
   632 lemma continuous_at_iff_ereal:
   633   fixes f :: "'a::t2_space \<Rightarrow> real"
   634   shows "continuous (at x0 within s) f \<longleftrightarrow> continuous (at x0 within s) (ereal \<circ> f)"
   635   unfolding continuous_within comp_def lim_ereal ..
   636 
   637 lemma continuous_on_iff_ereal:
   638   fixes f :: "'a::t2_space => real"
   639   assumes "open A"
   640   shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)"
   641   unfolding continuous_on_def comp_def lim_ereal ..
   642 
   643 lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real"
   644   using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
   645   by auto
   646 
   647 lemma continuous_on_iff_real:
   648   fixes f :: "'a::t2_space \<Rightarrow> ereal"
   649   assumes *: "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
   650   shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
   651 proof -
   652   have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
   653     using assms by force
   654   then have *: "continuous_on (f ` A) real"
   655     using continuous_on_real by (simp add: continuous_on_subset)
   656   have **: "continuous_on ((real \<circ> f) ` A) ereal"
   657     using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real \<circ> f) ` A"]
   658     by blast
   659   {
   660     assume "continuous_on A f"
   661     then have "continuous_on A (real \<circ> f)"
   662       apply (subst continuous_on_compose)
   663       using *
   664       apply auto
   665       done
   666   }
   667   moreover
   668   {
   669     assume "continuous_on A (real \<circ> f)"
   670     then have "continuous_on A (ereal \<circ> (real \<circ> f))"
   671       apply (subst continuous_on_compose)
   672       using **
   673       apply auto
   674       done
   675     then have "continuous_on A f"
   676       apply (subst continuous_on_eq[of A "ereal \<circ> (real \<circ> f)" f])
   677       using assms ereal_real
   678       apply auto
   679       done
   680   }
   681   ultimately show ?thesis
   682     by auto
   683 qed
   684 
   685 lemma continuous_at_const:
   686   fixes f :: "'a::t2_space \<Rightarrow> ereal"
   687   assumes "\<forall>x. f x = C"
   688   shows "\<forall>x. continuous (at x) f"
   689   unfolding continuous_at_open
   690   using assms t1_space
   691   by auto
   692 
   693 lemma mono_closed_real:
   694   fixes S :: "real set"
   695   assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
   696     and "closed S"
   697   shows "S = {} \<or> S = UNIV \<or> (\<exists>a. S = {a..})"
   698 proof -
   699   {
   700     assume "S \<noteq> {}"
   701     { assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x"
   702       then have *: "\<forall>x\<in>S. Inf S \<le> x"
   703         using cInf_lower[of _ S] ex by (metis bdd_below_def)
   704       then have "Inf S \<in> S"
   705         apply (subst closed_contains_Inf)
   706         using ex `S \<noteq> {}` `closed S`
   707         apply auto
   708         done
   709       then have "\<forall>x. Inf S \<le> x \<longleftrightarrow> x \<in> S"
   710         using mono[rule_format, of "Inf S"] *
   711         by auto
   712       then have "S = {Inf S ..}"
   713         by auto
   714       then have "\<exists>a. S = {a ..}"
   715         by auto
   716     }
   717     moreover
   718     {
   719       assume "\<not> (\<exists>B. \<forall>x\<in>S. B \<le> x)"
   720       then have nex: "\<forall>B. \<exists>x\<in>S. x < B"
   721         by (simp add: not_le)
   722       {
   723         fix y
   724         obtain x where "x\<in>S" and "x < y"
   725           using nex by auto
   726         then have "y \<in> S"
   727           using mono[rule_format, of x y] by auto
   728       }
   729       then have "S = UNIV"
   730         by auto
   731     }
   732     ultimately have "S = UNIV \<or> (\<exists>a. S = {a ..})"
   733       by blast
   734   }
   735   then show ?thesis
   736     by blast
   737 qed
   738 
   739 lemma mono_closed_ereal:
   740   fixes S :: "real set"
   741   assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
   742     and "closed S"
   743   shows "\<exists>a. S = {x. a \<le> ereal x}"
   744 proof -
   745   {
   746     assume "S = {}"
   747     then have ?thesis
   748       apply (rule_tac x=PInfty in exI)
   749       apply auto
   750       done
   751   }
   752   moreover
   753   {
   754     assume "S = UNIV"
   755     then have ?thesis
   756       apply (rule_tac x="-\<infinity>" in exI)
   757       apply auto
   758       done
   759   }
   760   moreover
   761   {
   762     assume "\<exists>a. S = {a ..}"
   763     then obtain a where "S = {a ..}"
   764       by auto
   765     then have ?thesis
   766       apply (rule_tac x="ereal a" in exI)
   767       apply auto
   768       done
   769   }
   770   ultimately show ?thesis
   771     using mono_closed_real[of S] assms by auto
   772 qed
   773 
   774 
   775 subsection {* Sums *}
   776 
   777 lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
   778 proof (cases "finite A")
   779   case True
   780   then show ?thesis by induct auto
   781 next
   782   case False
   783   then show ?thesis by simp
   784 qed
   785 
   786 lemma setsum_Pinfty:
   787   fixes f :: "'a \<Rightarrow> ereal"
   788   shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
   789 proof safe
   790   assume *: "setsum f P = \<infinity>"
   791   show "finite P"
   792   proof (rule ccontr)
   793     assume "infinite P"
   794     with * show False
   795       by auto
   796   qed
   797   show "\<exists>i\<in>P. f i = \<infinity>"
   798   proof (rule ccontr)
   799     assume "\<not> ?thesis"
   800     then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>"
   801       by auto
   802     with `finite P` have "setsum f P \<noteq> \<infinity>"
   803       by induct auto
   804     with * show False
   805       by auto
   806   qed
   807 next
   808   fix i
   809   assume "finite P" and "i \<in> P" and "f i = \<infinity>"
   810   then show "setsum f P = \<infinity>"
   811   proof induct
   812     case (insert x A)
   813     show ?case using insert by (cases "x = i") auto
   814   qed simp
   815 qed
   816 
   817 lemma setsum_Inf:
   818   fixes f :: "'a \<Rightarrow> ereal"
   819   shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
   820 proof
   821   assume *: "\<bar>setsum f A\<bar> = \<infinity>"
   822   have "finite A"
   823     by (rule ccontr) (insert *, auto)
   824   moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>"
   825   proof (rule ccontr)
   826     assume "\<not> ?thesis"
   827     then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
   828       by auto
   829     from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" ..
   830     with * show False
   831       by auto
   832   qed
   833   ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
   834     by auto
   835 next
   836   assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
   837   then obtain i where "finite A" "i \<in> A" and "\<bar>f i\<bar> = \<infinity>"
   838     by auto
   839   then show "\<bar>setsum f A\<bar> = \<infinity>"
   840   proof induct
   841     case (insert j A)
   842     then show ?case
   843       by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
   844   qed simp
   845 qed
   846 
   847 lemma setsum_real_of_ereal:
   848   fixes f :: "'i \<Rightarrow> ereal"
   849   assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
   850   shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
   851 proof -
   852   have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
   853   proof
   854     fix x
   855     assume "x \<in> S"
   856     from assms[OF this] show "\<exists>r. f x = ereal r"
   857       by (cases "f x") auto
   858   qed
   859   from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" ..
   860   then show ?thesis
   861     by simp
   862 qed
   863 
   864 lemma setsum_ereal_0:
   865   fixes f :: "'a \<Rightarrow> ereal"
   866   assumes "finite A"
   867     and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
   868   shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
   869 proof
   870   assume *: "(\<Sum>x\<in>A. f x) = 0"
   871   then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>"
   872     by auto
   873   then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>"
   874     using assms by (force simp: setsum_Pinfty)
   875   then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
   876     by auto
   877   from bchoice[OF this] * assms show "\<forall>i\<in>A. f i = 0"
   878     using setsum_nonneg_eq_0_iff[of A "\<lambda>i. real (f i)"] by auto
   879 qed (rule setsum.neutral)
   880 
   881 lemma setsum_ereal_right_distrib:
   882   fixes f :: "'a \<Rightarrow> ereal"
   883   assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
   884   shows "r * setsum f A = (\<Sum>n\<in>A. r * f n)"
   885 proof cases
   886   assume "finite A"
   887   then show ?thesis using assms
   888     by induct (auto simp: ereal_right_distrib setsum_nonneg)
   889 qed simp
   890 
   891 lemma sums_ereal_positive:
   892   fixes f :: "nat \<Rightarrow> ereal"
   893   assumes "\<And>i. 0 \<le> f i"
   894   shows "f sums (SUP n. \<Sum>i<n. f i)"
   895 proof -
   896   have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
   897     using ereal_add_mono[OF _ assms]
   898     by (auto intro!: incseq_SucI)
   899   from LIMSEQ_SUP[OF this]
   900   show ?thesis unfolding sums_def
   901     by (simp add: atLeast0LessThan)
   902 qed
   903 
   904 lemma summable_ereal_pos:
   905   fixes f :: "nat \<Rightarrow> ereal"
   906   assumes "\<And>i. 0 \<le> f i"
   907   shows "summable f"
   908   using sums_ereal_positive[of f, OF assms]
   909   unfolding summable_def
   910   by auto
   911 
   912 lemma suminf_ereal_eq_SUP:
   913   fixes f :: "nat \<Rightarrow> ereal"
   914   assumes "\<And>i. 0 \<le> f i"
   915   shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
   916   using sums_ereal_positive[of f, OF assms, THEN sums_unique]
   917   by simp
   918 
   919 lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
   920   unfolding sums_def by simp
   921 
   922 lemma suminf_bound:
   923   fixes f :: "nat \<Rightarrow> ereal"
   924   assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
   925     and pos: "\<And>n. 0 \<le> f n"
   926   shows "suminf f \<le> x"
   927 proof (rule Lim_bounded_ereal)
   928   have "summable f" using pos[THEN summable_ereal_pos] .
   929   then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
   930     by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
   931   show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
   932     using assms by auto
   933 qed
   934 
   935 lemma suminf_bound_add:
   936   fixes f :: "nat \<Rightarrow> ereal"
   937   assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
   938     and pos: "\<And>n. 0 \<le> f n"
   939     and "y \<noteq> -\<infinity>"
   940   shows "suminf f + y \<le> x"
   941 proof (cases y)
   942   case (real r)
   943   then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
   944     using assms by (simp add: ereal_le_minus)
   945   then have "(\<Sum> n. f n) \<le> x - y"
   946     using pos by (rule suminf_bound)
   947   then show "(\<Sum> n. f n) + y \<le> x"
   948     using assms real by (simp add: ereal_le_minus)
   949 qed (insert assms, auto)
   950 
   951 lemma suminf_upper:
   952   fixes f :: "nat \<Rightarrow> ereal"
   953   assumes "\<And>n. 0 \<le> f n"
   954   shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
   955   unfolding suminf_ereal_eq_SUP [OF assms]
   956   by (auto intro: complete_lattice_class.SUP_upper)
   957 
   958 lemma suminf_0_le:
   959   fixes f :: "nat \<Rightarrow> ereal"
   960   assumes "\<And>n. 0 \<le> f n"
   961   shows "0 \<le> (\<Sum>n. f n)"
   962   using suminf_upper[of f 0, OF assms]
   963   by simp
   964 
   965 lemma suminf_le_pos:
   966   fixes f g :: "nat \<Rightarrow> ereal"
   967   assumes "\<And>N. f N \<le> g N"
   968     and "\<And>N. 0 \<le> f N"
   969   shows "suminf f \<le> suminf g"
   970 proof (safe intro!: suminf_bound)
   971   fix n
   972   {
   973     fix N
   974     have "0 \<le> g N"
   975       using assms(2,1)[of N] by auto
   976   }
   977   have "setsum f {..<n} \<le> setsum g {..<n}"
   978     using assms by (auto intro: setsum_mono)
   979   also have "\<dots> \<le> suminf g"
   980     using `\<And>N. 0 \<le> g N`
   981     by (rule suminf_upper)
   982   finally show "setsum f {..<n} \<le> suminf g" .
   983 qed (rule assms(2))
   984 
   985 lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1"
   986   using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
   987   by (simp add: one_ereal_def)
   988 
   989 lemma suminf_add_ereal:
   990   fixes f g :: "nat \<Rightarrow> ereal"
   991   assumes "\<And>i. 0 \<le> f i"
   992     and "\<And>i. 0 \<le> g i"
   993   shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
   994   apply (subst (1 2 3) suminf_ereal_eq_SUP)
   995   unfolding setsum.distrib
   996   apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
   997   done
   998 
   999 lemma suminf_cmult_ereal:
  1000   fixes f g :: "nat \<Rightarrow> ereal"
  1001   assumes "\<And>i. 0 \<le> f i"
  1002     and "0 \<le> a"
  1003   shows "(\<Sum>i. a * f i) = a * suminf f"
  1004   by (auto simp: setsum_ereal_right_distrib[symmetric] assms
  1005        ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
  1006        intro!: SUP_ereal_cmult)
  1007 
  1008 lemma suminf_PInfty:
  1009   fixes f :: "nat \<Rightarrow> ereal"
  1010   assumes "\<And>i. 0 \<le> f i"
  1011     and "suminf f \<noteq> \<infinity>"
  1012   shows "f i \<noteq> \<infinity>"
  1013 proof -
  1014   from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
  1015   have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>"
  1016     by auto
  1017   then show ?thesis
  1018     unfolding setsum_Pinfty by simp
  1019 qed
  1020 
  1021 lemma suminf_PInfty_fun:
  1022   assumes "\<And>i. 0 \<le> f i"
  1023     and "suminf f \<noteq> \<infinity>"
  1024   shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
  1025 proof -
  1026   have "\<forall>i. \<exists>r. f i = ereal r"
  1027   proof
  1028     fix i
  1029     show "\<exists>r. f i = ereal r"
  1030       using suminf_PInfty[OF assms] assms(1)[of i]
  1031       by (cases "f i") auto
  1032   qed
  1033   from choice[OF this] show ?thesis
  1034     by auto
  1035 qed
  1036 
  1037 lemma summable_ereal:
  1038   assumes "\<And>i. 0 \<le> f i"
  1039     and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
  1040   shows "summable f"
  1041 proof -
  1042   have "0 \<le> (\<Sum>i. ereal (f i))"
  1043     using assms by (intro suminf_0_le) auto
  1044   with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
  1045     by (cases "\<Sum>i. ereal (f i)") auto
  1046   from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
  1047   have "summable (\<lambda>x. ereal (f x))"
  1048     using assms by auto
  1049   from summable_sums[OF this]
  1050   have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))"
  1051     by auto
  1052   then show "summable f"
  1053     unfolding r sums_ereal summable_def ..
  1054 qed
  1055 
  1056 lemma suminf_ereal:
  1057   assumes "\<And>i. 0 \<le> f i"
  1058     and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
  1059   shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
  1060 proof (rule sums_unique[symmetric])
  1061   from summable_ereal[OF assms]
  1062   show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
  1063     unfolding sums_ereal
  1064     using assms
  1065     by (intro summable_sums summable_ereal)
  1066 qed
  1067 
  1068 lemma suminf_ereal_minus:
  1069   fixes f g :: "nat \<Rightarrow> ereal"
  1070   assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i"
  1071     and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
  1072   shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
  1073 proof -
  1074   {
  1075     fix i
  1076     have "0 \<le> f i"
  1077       using ord[of i] by auto
  1078   }
  1079   moreover
  1080   from suminf_PInfty_fun[OF `\<And>i. 0 \<le> f i` fin(1)] obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))" ..
  1081   from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))" ..
  1082   {
  1083     fix i
  1084     have "0 \<le> f i - g i"
  1085       using ord[of i] by (auto simp: ereal_le_minus_iff)
  1086   }
  1087   moreover
  1088   have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
  1089     using assms by (auto intro!: suminf_le_pos simp: field_simps)
  1090   then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>"
  1091     using fin by auto
  1092   ultimately show ?thesis
  1093     using assms `\<And>i. 0 \<le> f i`
  1094     apply simp
  1095     apply (subst (1 2 3) suminf_ereal)
  1096     apply (auto intro!: suminf_diff[symmetric] summable_ereal)
  1097     done
  1098 qed
  1099 
  1100 lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
  1101 proof -
  1102   have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)"
  1103     by (rule suminf_upper) auto
  1104   then show ?thesis
  1105     by simp
  1106 qed
  1107 
  1108 lemma summable_real_of_ereal:
  1109   fixes f :: "nat \<Rightarrow> ereal"
  1110   assumes f: "\<And>i. 0 \<le> f i"
  1111     and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
  1112   shows "summable (\<lambda>i. real (f i))"
  1113 proof (rule summable_def[THEN iffD2])
  1114   have "0 \<le> (\<Sum>i. f i)"
  1115     using assms by (auto intro: suminf_0_le)
  1116   with fin obtain r where r: "ereal r = (\<Sum>i. f i)"
  1117     by (cases "(\<Sum>i. f i)") auto
  1118   {
  1119     fix i
  1120     have "f i \<noteq> \<infinity>"
  1121       using f by (intro suminf_PInfty[OF _ fin]) auto
  1122     then have "\<bar>f i\<bar> \<noteq> \<infinity>"
  1123       using f[of i] by auto
  1124   }
  1125   note fin = this
  1126   have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
  1127     using f
  1128     by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
  1129   also have "\<dots> = ereal r"
  1130     using fin r by (auto simp: ereal_real)
  1131   finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
  1132     by (auto simp: sums_ereal)
  1133 qed
  1134 
  1135 lemma suminf_SUP_eq:
  1136   fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
  1137   assumes "\<And>i. incseq (\<lambda>n. f n i)"
  1138     and "\<And>n i. 0 \<le> f n i"
  1139   shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
  1140 proof -
  1141   {
  1142     fix n :: nat
  1143     have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
  1144       using assms
  1145       by (auto intro!: SUP_ereal_setsum [symmetric])
  1146   }
  1147   note * = this
  1148   show ?thesis
  1149     using assms
  1150     apply (subst (1 2) suminf_ereal_eq_SUP)
  1151     unfolding *
  1152     apply (auto intro!: SUP_upper2)
  1153     apply (subst SUP_commute)
  1154     apply rule
  1155     done
  1156 qed
  1157 
  1158 lemma suminf_setsum_ereal:
  1159   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
  1160   assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
  1161   shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
  1162 proof (cases "finite A")
  1163   case True
  1164   then show ?thesis
  1165     using nonneg
  1166     by induct (simp_all add: suminf_add_ereal setsum_nonneg)
  1167 next
  1168   case False
  1169   then show ?thesis by simp
  1170 qed
  1171 
  1172 lemma suminf_ereal_eq_0:
  1173   fixes f :: "nat \<Rightarrow> ereal"
  1174   assumes nneg: "\<And>i. 0 \<le> f i"
  1175   shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
  1176 proof
  1177   assume "(\<Sum>i. f i) = 0"
  1178   {
  1179     fix i
  1180     assume "f i \<noteq> 0"
  1181     with nneg have "0 < f i"
  1182       by (auto simp: less_le)
  1183     also have "f i = (\<Sum>j. if j = i then f i else 0)"
  1184       by (subst suminf_finite[where N="{i}"]) auto
  1185     also have "\<dots> \<le> (\<Sum>i. f i)"
  1186       using nneg
  1187       by (auto intro!: suminf_le_pos)
  1188     finally have False
  1189       using `(\<Sum>i. f i) = 0` by auto
  1190   }
  1191   then show "\<forall>i. f i = 0"
  1192     by auto
  1193 qed simp
  1194 
  1195 lemma Liminf_within:
  1196   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
  1197   shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
  1198   unfolding Liminf_def eventually_at
  1199 proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
  1200   fix P d
  1201   assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
  1202   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
  1203     by (auto simp: zero_less_dist_iff dist_commute)
  1204   then show "\<exists>r>0. INFIMUM (Collect P) f \<le> INFIMUM (S \<inter> ball x r - {x}) f"
  1205     by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
  1206 next
  1207   fix d :: real
  1208   assume "0 < d"
  1209   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>
  1210     INFIMUM (S \<inter> ball x d - {x}) f \<le> INFIMUM (Collect P) f"
  1211     by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
  1212        (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
  1213 qed
  1214 
  1215 lemma Limsup_within:
  1216   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
  1217   shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
  1218   unfolding Limsup_def eventually_at
  1219 proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
  1220   fix P d
  1221   assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
  1222   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
  1223     by (auto simp: zero_less_dist_iff dist_commute)
  1224   then show "\<exists>r>0. SUPREMUM (S \<inter> ball x r - {x}) f \<le> SUPREMUM (Collect P) f"
  1225     by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
  1226 next
  1227   fix d :: real
  1228   assume "0 < d"
  1229   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>
  1230     SUPREMUM (Collect P) f \<le> SUPREMUM (S \<inter> ball x d - {x}) f"
  1231     by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
  1232        (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
  1233 qed
  1234 
  1235 lemma Liminf_at:
  1236   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
  1237   shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
  1238   using Liminf_within[of x UNIV f] by simp
  1239 
  1240 lemma Limsup_at:
  1241   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
  1242   shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
  1243   using Limsup_within[of x UNIV f] by simp
  1244 
  1245 lemma min_Liminf_at:
  1246   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_linorder"
  1247   shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
  1248   unfolding inf_min[symmetric] Liminf_at
  1249   apply (subst inf_commute)
  1250   apply (subst SUP_inf)
  1251   apply (intro SUP_cong[OF refl])
  1252   apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
  1253   apply (drule sym)
  1254   apply auto
  1255   apply (metis INF_absorb centre_in_ball)
  1256   done
  1257 
  1258 
  1259 lemma suminf_ereal_offset_le:
  1260   fixes f :: "nat \<Rightarrow> ereal"
  1261   assumes f: "\<And>i. 0 \<le> f i"
  1262   shows "(\<Sum>i. f (i + k)) \<le> suminf f"
  1263 proof -
  1264   have "(\<lambda>n. \<Sum>i<n. f (i + k)) ----> (\<Sum>i. f (i + k))"
  1265     using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
  1266   moreover have "(\<lambda>n. \<Sum>i<n. f i) ----> (\<Sum>i. f i)"
  1267     using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
  1268   then have "(\<lambda>n. \<Sum>i<n + k. f i) ----> (\<Sum>i. f i)"
  1269     by (rule LIMSEQ_ignore_initial_segment)
  1270   ultimately show ?thesis
  1271   proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
  1272     fix n assume "k \<le> n"
  1273     have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
  1274       by simp
  1275     also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
  1276       by (subst setsum.reindex) auto
  1277     also have "\<dots> \<le> setsum f {..<n + k}"
  1278       by (intro setsum_mono3) (auto simp: f)
  1279     finally show "(\<Sum>i<n. f (i + k)) \<le> setsum f {..<n + k}" .
  1280   qed
  1281 qed
  1282 
  1283 lemma sums_suminf_ereal: "f sums x \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal x"
  1284   by (metis sums_ereal sums_unique)
  1285 
  1286 lemma suminf_ereal': "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal (\<Sum>i. f i)"
  1287   by (metis sums_ereal sums_unique summable_def)
  1288 
  1289 lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
  1290   by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
  1291 
  1292 subsection {* monoset *}
  1293 
  1294 definition (in order) mono_set:
  1295   "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
  1296 
  1297 lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
  1298 lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
  1299 lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
  1300 lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
  1301 
  1302 lemma (in complete_linorder) mono_set_iff:
  1303   fixes S :: "'a set"
  1304   defines "a \<equiv> Inf S"
  1305   shows "mono_set S \<longleftrightarrow> S = {a <..} \<or> S = {a..}" (is "_ = ?c")
  1306 proof
  1307   assume "mono_set S"
  1308   then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S"
  1309     by (auto simp: mono_set)
  1310   show ?c
  1311   proof cases
  1312     assume "a \<in> S"
  1313     show ?c
  1314       using mono[OF _ `a \<in> S`]
  1315       by (auto intro: Inf_lower simp: a_def)
  1316   next
  1317     assume "a \<notin> S"
  1318     have "S = {a <..}"
  1319     proof safe
  1320       fix x assume "x \<in> S"
  1321       then have "a \<le> x"
  1322         unfolding a_def by (rule Inf_lower)
  1323       then show "a < x"
  1324         using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
  1325     next
  1326       fix x assume "a < x"
  1327       then obtain y where "y < x" "y \<in> S"
  1328         unfolding a_def Inf_less_iff ..
  1329       with mono[of y x] show "x \<in> S"
  1330         by auto
  1331     qed
  1332     then show ?c ..
  1333   qed
  1334 qed auto
  1335 
  1336 lemma ereal_open_mono_set:
  1337   fixes S :: "ereal set"
  1338   shows "open S \<and> mono_set S \<longleftrightarrow> S = UNIV \<or> S = {Inf S <..}"
  1339   by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
  1340     ereal_open_closed mono_set_iff open_ereal_greaterThan)
  1341 
  1342 lemma ereal_closed_mono_set:
  1343   fixes S :: "ereal set"
  1344   shows "closed S \<and> mono_set S \<longleftrightarrow> S = {} \<or> S = {Inf S ..}"
  1345   by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
  1346     ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
  1347 
  1348 lemma ereal_Liminf_Sup_monoset:
  1349   fixes f :: "'a \<Rightarrow> ereal"
  1350   shows "Liminf net f =
  1351     Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
  1352     (is "_ = Sup ?A")
  1353 proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
  1354   fix P
  1355   assume P: "eventually P net"
  1356   fix S
  1357   assume S: "mono_set S" "INFIMUM (Collect P) f \<in> S"
  1358   {
  1359     fix x
  1360     assume "P x"
  1361     then have "INFIMUM (Collect P) f \<le> f x"
  1362       by (intro complete_lattice_class.INF_lower) simp
  1363     with S have "f x \<in> S"
  1364       by (simp add: mono_set)
  1365   }
  1366   with P show "eventually (\<lambda>x. f x \<in> S) net"
  1367     by (auto elim: eventually_elim1)
  1368 next
  1369   fix y l
  1370   assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
  1371   assume P: "\<forall>P. eventually P net \<longrightarrow> INFIMUM (Collect P) f \<le> y"
  1372   show "l \<le> y"
  1373   proof (rule dense_le)
  1374     fix B
  1375     assume "B < l"
  1376     then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
  1377       by (intro S[rule_format]) auto
  1378     then have "INFIMUM {x. B < f x} f \<le> y"
  1379       using P by auto
  1380     moreover have "B \<le> INFIMUM {x. B < f x} f"
  1381       by (intro INF_greatest) auto
  1382     ultimately show "B \<le> y"
  1383       by simp
  1384   qed
  1385 qed
  1386 
  1387 lemma ereal_Limsup_Inf_monoset:
  1388   fixes f :: "'a \<Rightarrow> ereal"
  1389   shows "Limsup net f =
  1390     Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
  1391     (is "_ = Inf ?A")
  1392 proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
  1393   fix P
  1394   assume P: "eventually P net"
  1395   fix S
  1396   assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f \<in> S"
  1397   {
  1398     fix x
  1399     assume "P x"
  1400     then have "f x \<le> SUPREMUM (Collect P) f"
  1401       by (intro complete_lattice_class.SUP_upper) simp
  1402     with S(1)[unfolded mono_set, rule_format, of "- SUPREMUM (Collect P) f" "- f x"] S(2)
  1403     have "f x \<in> S"
  1404       by (simp add: inj_image_mem_iff) }
  1405   with P show "eventually (\<lambda>x. f x \<in> S) net"
  1406     by (auto elim: eventually_elim1)
  1407 next
  1408   fix y l
  1409   assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
  1410   assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPREMUM (Collect P) f"
  1411   show "y \<le> l"
  1412   proof (rule dense_ge)
  1413     fix B
  1414     assume "l < B"
  1415     then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
  1416       by (intro S[rule_format]) auto
  1417     then have "y \<le> SUPREMUM {x. f x < B} f"
  1418       using P by auto
  1419     moreover have "SUPREMUM {x. f x < B} f \<le> B"
  1420       by (intro SUP_least) auto
  1421     ultimately show "y \<le> B"
  1422       by simp
  1423   qed
  1424 qed
  1425 
  1426 lemma liminf_bounded_open:
  1427   fixes x :: "nat \<Rightarrow> ereal"
  1428   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))"
  1429   (is "_ \<longleftrightarrow> ?P x0")
  1430 proof
  1431   assume "?P x0"
  1432   then show "x0 \<le> liminf x"
  1433     unfolding ereal_Liminf_Sup_monoset eventually_sequentially
  1434     by (intro complete_lattice_class.Sup_upper) auto
  1435 next
  1436   assume "x0 \<le> liminf x"
  1437   {
  1438     fix S :: "ereal set"
  1439     assume om: "open S" "mono_set S" "x0 \<in> S"
  1440     {
  1441       assume "S = UNIV"
  1442       then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
  1443         by auto
  1444     }
  1445     moreover
  1446     {
  1447       assume "S \<noteq> UNIV"
  1448       then obtain B where B: "S = {B<..}"
  1449         using om ereal_open_mono_set by auto
  1450       then have "B < x0"
  1451         using om by auto
  1452       then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
  1453         unfolding B
  1454         using `x0 \<le> liminf x` liminf_bounded_iff
  1455         by auto
  1456     }
  1457     ultimately have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
  1458       by auto
  1459   }
  1460   then show "?P x0"
  1461     by auto
  1462 qed
  1463 
  1464 subsection "Relate extended reals and the indicator function"
  1465 
  1466 lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
  1467   by (auto simp: indicator_def one_ereal_def)
  1468 
  1469 lemma ereal_mult_indicator: "ereal (x * indicator A y) = ereal x * indicator A y"
  1470   by (simp split: split_indicator)
  1471 
  1472 lemma ereal_indicator_mult: "ereal (indicator A y * x) = indicator A y * ereal x"
  1473   by (simp split: split_indicator)
  1474 
  1475 lemma ereal_indicator_nonneg[simp, intro]: "0 \<le> (indicator A x ::ereal)"
  1476   unfolding indicator_def by auto
  1477 
  1478 end