# Theory Extended_Real_Limits

Up to index of Isabelle/HOL/HOL-Multivariate_Analysis

theory Extended_Real_Limits
imports Topology_Euclidean_Space Extended_Real
`(*  Title:      HOL/Multivariate_Analysis/Extended_Real_Limits.thy    Author:     Johannes Hölzl, TU München    Author:     Robert Himmelmann, TU München    Author:     Armin Heller, TU München    Author:     Bogdan Grechuk, University of Edinburgh*)header {* Limits on the Extended real number line *}theory Extended_Real_Limits  imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real"beginlemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"  unfolding continuous_on_topological open_ereal_def by autolemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal"  using continuous_on_eq_continuous_at[of UNIV] by autolemma continuous_within_ereal[intro, simp]: "x ∈ A ==> continuous (at x within A) ereal"  using continuous_on_eq_continuous_within[of A] by autolemma ereal_open_uminus:  fixes S :: "ereal set"  assumes "open S"  shows "open (uminus ` S)"  unfolding open_ereal_defproof (intro conjI impI)  obtain x y where    S: "open (ereal -` S)" "∞ ∈ S ==> {ereal x<..} ⊆ S" "-∞ ∈ S ==> {..< ereal y} ⊆ S"    using `open S` unfolding open_ereal_def by auto  have "ereal -` uminus ` S = uminus ` (ereal -` S)"  proof safe    fix x y    assume "ereal x = - y" "y ∈ S"    then show "x ∈ uminus ` ereal -` S" by (cases y) auto  next    fix x    assume "ereal x ∈ S"    then show "- x ∈ ereal -` uminus ` S"      by (auto intro: image_eqI[of _ _ "ereal x"])  qed  then show "open (ereal -` uminus ` S)"    using S by (auto intro: open_negations)  { assume "∞ ∈ uminus ` S"    then have "-∞ ∈ S" by (metis image_iff ereal_uminus_uminus)    then have "uminus ` {..<ereal y} ⊆ uminus ` S" using S by (intro image_mono) auto    then show "∃x. {ereal x<..} ⊆ uminus ` S" using ereal_uminus_lessThan by auto }  { assume "-∞ ∈ uminus ` S"    then have "∞ : S" by (metis image_iff ereal_uminus_uminus)    then have "uminus ` {ereal x<..} <= uminus ` S" using S by (intro image_mono) auto    then show "∃y. {..<ereal y} <= uminus ` S" using ereal_uminus_greaterThan by auto }qedlemma ereal_uminus_complement:  fixes S :: "ereal set"  shows "uminus ` (- S) = - uminus ` S"  by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)lemma ereal_closed_uminus:  fixes S :: "ereal set"  assumes "closed S"  shows "closed (uminus ` S)"  using assms unfolding closed_def  using ereal_open_uminus[of "- S"] ereal_uminus_complement by autoinstance ereal :: perfect_spaceproof (default, rule)  fix a :: ereal assume a: "open {a}"  show False  proof (cases a)    case MInf    then obtain y where "{..<ereal y} <= {a}" using a open_MInfty2[of "{a}"] by auto    then have "ereal(y - 1):{a}" apply (subst subsetD[of "{..<ereal y}"]) by auto    then show False using `a=(-∞)` by auto  next    case PInf    then obtain y where "{ereal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto    then have "ereal(y+1):{a}" apply (subst subsetD[of "{ereal y<..}"]) by auto    then show False using `a=∞` by auto  next    case (real r) then have fin: "¦a¦ ≠ ∞" by simp    from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this    then obtain b where b_def: "a<b & b<a+e"      using fin ereal_between ereal_dense[of a "a+e"] by auto    then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto    then show False using b_def e by auto  qedqedlemma ereal_closed_contains_Inf:  fixes S :: "ereal set"  assumes "closed S" "S ~= {}"  shows "Inf S : S"proof (rule ccontr)  assume "Inf S ∉ S"  then have a: "open (-S)" "Inf S:(- S)" using assms by auto  show False  proof (cases "Inf S")    case MInf    then have "(-∞) : - S" using a by auto    then obtain y where "{..<ereal y} <= (-S)" using a open_MInfty2[of "- S"] by auto    then have "ereal y <= Inf S" by (metis Compl_anti_mono Compl_lessThan atLeast_iff      complete_lattice_class.Inf_greatest double_complement set_rev_mp)    then show False using MInf by auto  next    case PInf    then have "S={∞}" by (metis Inf_eq_PInfty assms(2))    then show False using `Inf S ~: S` by (simp add: top_ereal_def)  next    case (real r)    then have fin: "¦Inf S¦ ≠ ∞" by simp    from ereal_open_cont_interval[OF a this] guess e . note e = this    { fix x      assume "x:S" then have "x>=Inf S" by (rule complete_lattice_class.Inf_lower)      then have *: "x>Inf S-e" using e by (metis fin ereal_between(1) order_less_le_trans)      { assume "x<Inf S+e"        then have "x:{Inf S-e <..< Inf S+e}" using * by auto        then have False using e `x:S` by auto      } then have "x>=Inf S+e" by (metis linorder_le_less_linear)    }    then have "Inf S + e <= Inf S" by (metis le_Inf_iff)    then show False using real e by (cases e) auto  qedqedlemma ereal_closed_contains_Sup:  fixes S :: "ereal set"  assumes "closed S" "S ~= {}"  shows "Sup S : S"proof -  have "closed (uminus ` S)"    by (metis assms(1) ereal_closed_uminus)  then have "Inf (uminus ` S) : uminus ` S"    using assms ereal_closed_contains_Inf[of "uminus ` S"] by auto  then have "- Sup S : uminus ` S"    using ereal_Sup_uminus_image_eq[of "uminus ` S"] by (auto simp: image_image)  then show ?thesis    by (metis imageI ereal_uminus_uminus ereal_minus_minus_image)qedlemma ereal_open_closed_aux:  fixes S :: "ereal set"  assumes "open S" "closed S"    and S: "(-∞) ~: S"  shows "S = {}"proof (rule ccontr)  assume "S ~= {}"  then have *: "(Inf S):S" by (metis assms(2) ereal_closed_contains_Inf)  { assume "Inf S=(-∞)"    then have False using * assms(3) by auto }  moreover  { assume "Inf S=∞"    then have "S={∞}" by (metis Inf_eq_PInfty `S ~= {}`)    then have False by (metis assms(1) not_open_singleton) }  moreover  { assume fin: "¦Inf S¦ ≠ ∞"    from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this    then obtain b where b_def: "Inf S-e<b & b<Inf S"      using fin ereal_between[of "Inf S" e] ereal_dense[of "Inf S-e"] by auto    then have "b: {Inf S-e <..< Inf S+e}" using e fin ereal_between[of "Inf S" e]      by auto    then have "b:S" using e by auto    then have False using b_def by (metis complete_lattice_class.Inf_lower leD)  } ultimately show False by autoqedlemma ereal_open_closed:  fixes S :: "ereal set"  shows "(open S & closed S) <-> (S = {} | S = UNIV)"proof -  { assume lhs: "open S & closed S"    { assume "(-∞) ~: S"      then have "S={}" using lhs ereal_open_closed_aux by auto }    moreover    { assume "(-∞) : S"      then have "(- S)={}" using lhs ereal_open_closed_aux[of "-S"] by auto }    ultimately have "S = {} | S = UNIV" by auto  } then show ?thesis by autoqedlemma ereal_open_affinity_pos:  fixes S :: "ereal set"  assumes "open S" and m: "m ≠ ∞" "0 < m" and t: "¦t¦ ≠ ∞"  shows "open ((λx. m * x + t) ` S)"proof -  obtain r where r[simp]: "m = ereal r" using m by (cases m) auto  obtain p where p[simp]: "t = ereal p" using t by auto  have "r ≠ 0" "0 < r" and m': "m ≠ ∞" "m ≠ -∞" "m ≠ 0" using m by auto  from `open S`[THEN ereal_openE] guess l u . note T = this  let ?f = "(λx. m * x + t)"  show ?thesis    unfolding open_ereal_def  proof (intro conjI impI exI subsetI)    have "ereal -` ?f ` S = (λx. r * x + p) ` (ereal -` S)"    proof safe      fix x y      assume "ereal y = m * x + t" "x ∈ S"      then show "y ∈ (λx. r * x + p) ` ereal -` S"        using `r ≠ 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm)    qed force    then show "open (ereal -` ?f ` S)"      using open_affinity[OF T(1) `r ≠ 0`] by (auto simp: ac_simps)  next    assume "∞ ∈ ?f`S"    with `0 < r` have "∞ ∈ S" by auto    fix x    assume "x ∈ {ereal (r * l + p)<..}"    then have [simp]: "ereal (r * l + p) < x" by auto    show "x ∈ ?f`S"    proof (rule image_eqI)      show "x = m * ((x - t) / m) + t"        using m t by (cases rule: ereal3_cases[of m x t]) auto      have "ereal l < (x - t)/m"        using m t by (simp add: ereal_less_divide_pos ereal_less_minus)      then show "(x - t)/m ∈ S" using T(2)[OF `∞ ∈ S`] by auto    qed  next    assume "-∞ ∈ ?f`S" with `0 < r` have "-∞ ∈ S" by auto    fix x assume "x ∈ {..<ereal (r * u + p)}"    then have [simp]: "x < ereal (r * u + p)" by auto    show "x ∈ ?f`S"    proof (rule image_eqI)      show "x = m * ((x - t) / m) + t"        using m t by (cases rule: ereal3_cases[of m x t]) auto      have "(x - t)/m < ereal u"        using m t by (simp add: ereal_divide_less_pos ereal_minus_less)      then show "(x - t)/m ∈ S" using T(3)[OF `-∞ ∈ S`] by auto    qed  qedqedlemma ereal_open_affinity:  fixes S :: "ereal set"  assumes "open S"    and m: "¦m¦ ≠ ∞" "m ≠ 0"    and t: "¦t¦ ≠ ∞"  shows "open ((λx. m * x + t) ` S)"proof cases  assume "0 < m"  then show ?thesis    using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m by autonext  assume "¬ 0 < m" then  have "0 < -m" using `m ≠ 0` by (cases m) auto  then have m: "-m ≠ ∞" "0 < -m" using `¦m¦ ≠ ∞`    by (auto simp: ereal_uminus_eq_reorder)  from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t]  show ?thesis unfolding image_image by simpqedlemma ereal_lim_mult:  fixes X :: "'a => ereal"  assumes lim: "(X ---> L) net"    and a: "¦a¦ ≠ ∞"  shows "((λi. a * X i) ---> a * L) net"proof cases  assume "a ≠ 0"  show ?thesis  proof (rule topological_tendstoI)    fix S    assume "open S" "a * L ∈ S"    have "a * L / a = L"      using `a ≠ 0` a by (cases rule: ereal2_cases[of a L]) auto    then have L: "L ∈ ((λx. x / a) ` S)"      using `a * L ∈ S` by (force simp: image_iff)    moreover have "open ((λx. x / a) ` S)"      using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a ≠ 0` a      by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps)    note * = lim[THEN topological_tendstoD, OF this L]    { fix x      from a `a ≠ 0` have "a * (x / a) = x"        by (cases rule: ereal2_cases[of a x]) auto }    note this[simp]    show "eventually (λx. a * X x ∈ S) net"      by (rule eventually_mono[OF _ *]) auto  qedqed autolemma ereal_lim_uminus:  fixes X :: "'a => ereal"  shows "((λi. - X i) ---> -L) net <-> (X ---> L) net"  using ereal_lim_mult[of X L net "ereal (-1)"]    ereal_lim_mult[of "(λi. - X i)" "-L" net "ereal (-1)"]  by (auto simp add: algebra_simps)lemma Lim_bounded2_ereal:  assumes lim:"f ----> (l :: ereal)"    and ge: "ALL n>=N. f n >= C"  shows "l>=C"proof -  def g == "(%i. -(f i))"  { fix n    assume "n>=N"    then have "g n <= -C" using assms ereal_minus_le_minus g_def by auto }  then have "ALL n>=N. g n <= -C" by auto  moreover have limg: "g ----> (-l)" using g_def ereal_lim_uminus lim by auto  ultimately have "-l <= -C" using Lim_bounded_ereal[of g "-l" _ "-C"] by auto  then show ?thesis using ereal_minus_le_minus by autoqedlemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} <-> x = -∞"proof  assume "x = -∞" then have "{x..} = UNIV" by auto  then show "open {x..}" by autonext  assume "open {x..}"  then have "open {x..} ∧ closed {x..}" by auto  then have "{x..} = UNIV" unfolding ereal_open_closed by auto  then show "x = -∞" by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)qedlemma ereal_open_mono_set:  fixes S :: "ereal set"  shows "(open S ∧ mono_set S) <-> (S = UNIV ∨ S = {Inf S <..})"  by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast    ereal_open_closed mono_set_iff open_ereal_greaterThan)lemma ereal_closed_mono_set:  fixes S :: "ereal set"  shows "(closed S ∧ mono_set S) <-> (S = {} ∨ S = {Inf S ..})"  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast    ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)lemma ereal_Liminf_Sup_monoset:  fixes f :: "'a => ereal"  shows "Liminf net f =    Sup {l. ∀S. open S --> mono_set S --> l ∈ S --> eventually (λx. f x ∈ S) net}"  unfolding Liminf_Supproof (intro arg_cong[where f="λP. Sup (Collect P)"] ext iffI allI impI)  fix l S  assume ev: "∀y<l. eventually (λx. y < f x) net" and "open S" "mono_set S" "l ∈ S"  then have "S = UNIV ∨ S = {Inf S <..}"    using ereal_open_mono_set[of S] by auto  then show "eventually (λx. f x ∈ S) net"  proof    assume S: "S = {Inf S<..}"    then have "Inf S < l" using `l ∈ S` by auto    then have "eventually (λx. Inf S < f x) net" using ev by auto    then show "eventually (λx. f x ∈ S) net" by (subst S) auto  qed autonext  fix l y  assume S: "∀S. open S --> mono_set S --> l ∈ S --> eventually  (λx. f x ∈ S) net" "y < l"  have "eventually  (λx. f x ∈ {y <..}) net"    using `y < l` by (intro S[rule_format]) auto  then show "eventually (λx. y < f x) net" by autoqedlemma ereal_Limsup_Inf_monoset:  fixes f :: "'a => ereal"  shows "Limsup net f =    Inf {l. ∀S. open S --> mono_set (uminus ` S) --> l ∈ S --> eventually (λx. f x ∈ S) net}"  unfolding Limsup_Infproof (intro arg_cong[where f="λP. Inf (Collect P)"] ext iffI allI impI)  fix l S  assume ev: "∀y>l. eventually (λx. f x < y) net" and "open S" "mono_set (uminus`S)" "l ∈ S"  then have "open (uminus`S) ∧ mono_set (uminus`S)" by (simp add: ereal_open_uminus)  then have "S = UNIV ∨ S = {..< Sup S}"    unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp  then show "eventually (λx. f x ∈ S) net"  proof    assume S: "S = {..< Sup S}"    then have "l < Sup S" using `l ∈ S` by auto    then have "eventually (λx. f x < Sup S) net" using ev by auto    then show "eventually (λx. f x ∈ S) net"  by (subst S) auto  qed autonext  fix l y  assume S: "∀S. open S --> mono_set (uminus`S) --> l ∈ S --> eventually  (λx. f x ∈ S) net" "l < y"  have "eventually  (λx. f x ∈ {..< y}) net"    using `l < y` by (intro S[rule_format]) auto  then show "eventually (λx. f x < y) net" by autoqedlemma open_uminus_iff: "open (uminus ` S) <-> open (S::ereal set)"  using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by autolemma ereal_Limsup_uminus:  fixes f :: "'a => ereal"  shows "Limsup net (λx. - (f x)) = -(Liminf net f)"proof -  { fix P l    have "(∃x. (l::ereal) = -x ∧ P x) <-> P (-l)"      by (auto intro!: exI[of _ "-l"]) }  note Ex_cancel = this  { fix P :: "ereal set => bool"    have "(∀S. P S) <-> (∀S. P (uminus`S))"      apply auto      apply (erule_tac x="uminus`S" in allE)      apply (auto simp: image_image)      done }  note add_uminus_image = this  { fix x S    have "(x::ereal) ∈ uminus`S <-> -x∈S"      by (auto intro!: image_eqI[of _ _ "-x"]) }  note remove_uminus_image = this  show ?thesis    unfolding ereal_Limsup_Inf_monoset ereal_Liminf_Sup_monoset    unfolding ereal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel    by (subst add_uminus_image) (simp add: open_uminus_iff remove_uminus_image)qedlemma ereal_Liminf_uminus:  fixes f :: "'a => ereal"  shows "Liminf net (λx. - (f x)) = -(Limsup net f)"  using ereal_Limsup_uminus[of _ "(λx. - (f x))"] by autolemma ereal_Lim_uminus:  fixes f :: "'a => ereal"  shows "(f ---> f0) net <-> ((λx. - f x) ---> - f0) net"  using    ereal_lim_mult[of f f0 net "- 1"]    ereal_lim_mult[of "λx. - (f x)" "-f0" net "- 1"]  by (auto simp: ereal_uminus_reorder)lemma lim_imp_Limsup:  fixes f :: "'a => ereal"  assumes "¬ trivial_limit net"    and lim: "(f ---> f0) net"  shows "Limsup net f = f0"  using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]     ereal_Liminf_uminus[of net f] assms by simplemma convergent_ereal_limsup:  fixes X :: "nat => ereal"  shows "convergent X ==> limsup X = lim X"  by (auto simp: convergent_def limI lim_imp_Limsup)lemma Liminf_PInfty:  fixes f :: "'a => ereal"  assumes "¬ trivial_limit net"  shows "(f ---> ∞) net <-> Liminf net f = ∞"proof (intro lim_imp_Liminf iffI assms)  assume rhs: "Liminf net f = ∞"  { fix S :: "ereal set"    assume "open S & ∞ : S"    then obtain m where "{ereal m<..} <= S" using open_PInfty2 by auto    moreover    have "eventually (λx. f x ∈ {ereal m<..}) net"      using rhs      unfolding Liminf_Sup top_ereal_def[symmetric] Sup_eq_top_iff      by (auto elim!: allE[where x="ereal m"] simp: top_ereal_def)    ultimately    have "eventually (%x. f x : S) net"      apply (subst eventually_mono)      apply auto      done  }  then show "(f ---> ∞) net" unfolding tendsto_def by autoqedlemma Limsup_MInfty:  fixes f :: "'a => ereal"  assumes "¬ trivial_limit net"  shows "(f ---> -∞) net <-> Limsup net f = -∞"  using assms ereal_Lim_uminus[of f "-∞"] Liminf_PInfty[of _ "λx. - (f x)"]        ereal_Liminf_uminus[of _ f] by (auto simp: ereal_uminus_eq_reorder)lemma ereal_Liminf_eq_Limsup:  fixes f :: "'a => ereal"  assumes ntriv: "¬ trivial_limit net"    and lim: "Liminf net f = f0" "Limsup net f = f0"  shows "(f ---> f0) net"proof (cases f0)  case PInf  then show ?thesis using Liminf_PInfty[OF ntriv] lim by autonext  case MInf  then show ?thesis using Limsup_MInfty[OF ntriv] lim by autonext  case (real r)  show "(f ---> f0) net"  proof (rule topological_tendstoI)    fix S    assume "open S""f0 ∈ S"    then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} ⊆ S"      using ereal_open_cont_interval2[of S f0] real lim by auto    then have "eventually (λx. f x ∈ {a<..<b}) net"      unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff      by (auto intro!: eventually_conj)    with `{a<..<b} ⊆ S` show "eventually (%x. f x : S) net"      by (rule_tac eventually_mono) auto  qedqedlemma ereal_Liminf_eq_Limsup_iff:  fixes f :: "'a => ereal"  assumes "¬ trivial_limit net"  shows "(f ---> f0) net <-> Liminf net f = f0 ∧ Limsup net f = f0"  by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)lemma convergent_ereal:  fixes X :: "nat => ereal"  shows "convergent X <-> limsup X = liminf X"  using ereal_Liminf_eq_Limsup_iff[of sequentially]  by (auto simp: convergent_def)lemma limsup_INFI_SUPR:  fixes f :: "nat => ereal"  shows "limsup f = (INF n. SUP m:{n..}. f m)"  using ereal_Limsup_uminus[of sequentially "λx. - f x"]  by (simp add: liminf_SUPR_INFI ereal_INFI_uminus ereal_SUPR_uminus)lemma liminf_PInfty:  fixes X :: "nat => ereal"  shows "X ----> ∞ <-> liminf X = ∞"  by (metis Liminf_PInfty trivial_limit_sequentially)lemma limsup_MInfty:  fixes X :: "nat => ereal"  shows "X ----> (-∞) <-> limsup X = (-∞)"  by (metis Limsup_MInfty trivial_limit_sequentially)lemma ereal_lim_mono:  fixes X Y :: "nat => ereal"  assumes "!!n. N ≤ n ==> X n <= Y n"    and "X ----> x" "Y ----> y"  shows "x <= y"  by (metis ereal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)lemma incseq_le_ereal:  fixes X :: "nat => ereal"  assumes inc: "incseq X" and lim: "X ----> L"  shows "X N ≤ L"  using inc by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)lemma decseq_ge_ereal:  assumes dec: "decseq X"    and lim: "X ----> (L::ereal)"  shows "X N >= L"  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)lemma liminf_bounded_open:  fixes x :: "nat => ereal"  shows "x0 ≤ liminf x <-> (∀S. open S --> mono_set S --> x0 ∈ S --> (∃N. ∀n≥N. x n ∈ S))"  (is "_ <-> ?P x0")proof  assume "?P x0"  then show "x0 ≤ liminf x"    unfolding ereal_Liminf_Sup_monoset eventually_sequentially    by (intro complete_lattice_class.Sup_upper) autonext  assume "x0 ≤ liminf x"  { fix S :: "ereal set"    assume om: "open S & mono_set S & x0:S"    { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }    moreover    { assume "~(S=UNIV)"      then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto      then have "B<x0" using om by auto      then have "EX N. ALL n>=N. x n : S"        unfolding B_def using `x0 ≤ liminf x` liminf_bounded_iff by auto    }    ultimately have "EX N. (ALL n>=N. x n : S)" by auto  }  then show "?P x0" by autoqedlemma limsup_subseq_mono:  fixes X :: "nat => ereal"  assumes "subseq r"  shows "limsup (X o r) ≤ limsup X"proof -  have "(λn. - X n) o r = (λn. - (X o r) n)" by (simp add: fun_eq_iff)  then have "- limsup X ≤ - limsup (X o r)"     using liminf_subseq_mono[of r "(%n. - X n)"]       ereal_Liminf_uminus[of sequentially X]       ereal_Liminf_uminus[of sequentially "X o r"] assms by auto  then show ?thesis by autoqedlemma bounded_abs:  assumes "(a::real)<=x" "x<=b"  shows "abs x <= max (abs a) (abs b)"  by (metis abs_less_iff assms leI le_max_iff_disj    less_eq_real_def less_le_not_le less_minus_iff minus_minus)lemma bounded_increasing_convergent2:  fixes f::"nat => real"  assumes "ALL n. f n <= B" "ALL n m. n>=m --> f n >= f m"  shows "EX l. (f ---> l) sequentially"proof -  def N == "max (abs (f 0)) (abs B)"  { fix n    have "abs (f n) <= N"      unfolding N_def      apply (subst bounded_abs)      using assms apply auto      done }  then have "bounded {f n| n::nat. True}"    unfolding bounded_real by auto  then show ?thesis    apply (rule Topology_Euclidean_Space.bounded_increasing_convergent)    using assms apply auto    doneqedlemma lim_ereal_increasing:  assumes "!!n m. n >= m ==> f n >= f m"  obtains l where "f ----> (l::ereal)"proof (cases "f = (λx. - ∞)")  case True  then show thesis    using tendsto_const[of "- ∞" sequentially] by (intro that[of "-∞"]) autonext  case False  then obtain N where N_def: "f N > (-∞)" by (auto simp: fun_eq_iff)  have "ALL n>=N. f n >= f N" using assms by auto  then have minf: "ALL n>=N. f n > (-∞)" using N_def by auto  def Y == "(%n. (if n>=N then f n else f N))"  then have incy: "!!n m. n>=m ==> Y n >= Y m" using assms by auto  from minf have minfy: "ALL n. Y n ~= (-∞)" using Y_def by auto  show thesis  proof (cases "EX B. ALL n. f n < ereal B")    case False    then show thesis      apply -      apply (rule that[of ∞])      unfolding Lim_PInfty not_ex not_all      apply safe      apply (erule_tac x=B in allE, safe)      apply (rule_tac x=x in exI, safe)      apply (rule order_trans[OF _ assms[rule_format]])      apply auto      done  next    case True    then guess B ..    then have "ALL n. Y n < ereal B" using Y_def by auto    note B = this[rule_format]    { fix n      have "Y n < ∞"        using B[of n]        apply (subst less_le_trans)        apply auto        done      then have "Y n ~= ∞ & Y n ~= (-∞)" using minfy by auto    }    then have *: "ALL n. ¦Y n¦ ≠ ∞" by auto    { fix n      have "real (Y n) < B"      proof -        case goal1        then show ?case          using B[of n] apply-apply(subst(asm) ereal_real'[THEN sym]) defer defer          unfolding ereal_less using * by auto      qed    }    then have B': "ALL n. (real (Y n) <= B)" using less_imp_le by auto    have "EX l. (%n. real (Y n)) ----> l"      apply (rule bounded_increasing_convergent2)    proof safe      show "!!n. real (Y n) <= B" using B' by auto      fix n m :: nat      assume "n<=m"      then have "ereal (real (Y n)) <= ereal (real (Y m))"        using incy[rule_format,of n m] apply(subst ereal_real)+        using *[rule_format, of n] *[rule_format, of m] by auto      then show "real (Y n) <= real (Y m)" by auto    qed    then guess l .. note l=this    have "Y ----> ereal l"      using l      apply -      apply (subst(asm) lim_ereal[THEN sym])      unfolding ereal_real      using * apply auto      done    then show thesis      apply -      apply (rule that[of "ereal l"])      apply (subst tail_same_limit[of Y _ N])      using Y_def apply auto      done  qedqedlemma lim_ereal_decreasing:  assumes "!!n m. n >= m ==> f n <= f m"  obtains l where "f ----> (l::ereal)"proof -  from lim_ereal_increasing[of "λx. - f x"] assms  obtain l where "(λx. - f x) ----> l" by auto  from ereal_lim_mult[OF this, of "- 1"] show thesis    by (intro that[of "-l"]) (simp add: ereal_uminus_eq_reorder)qedlemma compact_ereal:  fixes X :: "nat => ereal"  shows "∃l r. subseq r ∧ (X o r) ----> l"proof -  obtain r where "subseq r" and mono: "monoseq (X o r)"    using seq_monosub[of X] unfolding comp_def by auto  then have "(∀n m. m ≤ n --> (X o r) m ≤ (X o r) n) ∨ (∀n m. m ≤ n --> (X o r) n ≤ (X o r) m)"    by (auto simp add: monoseq_def)  then obtain l where "(Xor) ----> l"     using lim_ereal_increasing[of "X o r"] lim_ereal_decreasing[of "X o r"] by auto  then show ?thesis using `subseq r` by autoqedlemma ereal_Sup_lim:  assumes "!!n. b n ∈ s" "b ----> (a::ereal)"  shows "a ≤ Sup s"  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)lemma ereal_Inf_lim:  assumes "!!n. b n ∈ s" "b ----> (a::ereal)"  shows "Inf s ≤ a"  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)lemma SUP_Lim_ereal:  fixes X :: "nat => ereal"  assumes "incseq X" "X ----> l"  shows "(SUP n. X n) = l"proof (rule ereal_SUPI)  fix n from assms show "X n ≤ l"    by (intro incseq_le_ereal) (simp add: incseq_def)next  fix y assume "!!n. n ∈ UNIV ==> X n ≤ y"  with ereal_Sup_lim[OF _ `X ----> l`, of "{..y}"] show "l ≤ y" by autoqedlemma LIMSEQ_ereal_SUPR:  fixes X :: "nat => ereal"  assumes "incseq X"  shows "X ----> (SUP n. X n)"proof (rule lim_ereal_increasing)  fix n m :: nat  assume "m ≤ n"  then show "X m ≤ X n" using `incseq X` by (simp add: incseq_def)next  fix l  assume "X ----> l"  with SUP_Lim_ereal[of X, OF assms this] show ?thesis by simpqedlemma INF_Lim_ereal: "decseq X ==> X ----> l ==> (INF n. X n) = (l::ereal)"  using SUP_Lim_ereal[of "λi. - X i" "- l"]  by (simp add: ereal_SUPR_uminus ereal_lim_uminus)lemma LIMSEQ_ereal_INFI: "decseq X ==> X ----> (INF n. X n :: ereal)"  using LIMSEQ_ereal_SUPR[of "λi. - X i"]  by (simp add: ereal_SUPR_uminus ereal_lim_uminus)lemma SUP_eq_LIMSEQ:  assumes "mono f"  shows "(SUP n. ereal (f n)) = ereal x <-> f ----> x"proof  have inc: "incseq (λi. ereal (f i))"    using `mono f` unfolding mono_def incseq_def by auto  { assume "f ----> x"    then have "(λi. ereal (f i)) ----> ereal x" by auto    from SUP_Lim_ereal[OF inc this]    show "(SUP n. ereal (f n)) = ereal x" . }  { assume "(SUP n. ereal (f n)) = ereal x"    with LIMSEQ_ereal_SUPR[OF inc]    show "f ----> x" by auto }qedlemma Liminf_within:  fixes f :: "'a::metric_space => ereal"  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"proof -  let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"  { fix T    assume T_def: "open T & mono_set T & ?l:T"    have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"    proof -      { assume "T=UNIV" then have ?thesis by (simp add: gt_ex) }      moreover      { assume "~(T=UNIV)"        then obtain B where "T={B<..}" using T_def ereal_open_mono_set[of T] by auto        then have "B<?l" using T_def by auto        then obtain d where d_def: "0<d & B<(INF y:(S Int ball x d - {x}). f y)"          unfolding less_SUP_iff by auto        { fix y assume "y:S & 0 < dist y x & dist y x < d"          then have "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)          then have "f y:T" using d_def INF_lower[of y "S Int ball x d - {x}" f] `T={B<..}` by auto        } then have ?thesis apply(rule_tac x="d" in exI) using d_def by auto      }      ultimately show ?thesis by auto    qed  }  moreover  { fix z    assume a: "ALL T. open T --> mono_set T --> z : T -->       (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"    { fix B      assume "B<z"      then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"         using a[rule_format, of "{B<..}"] mono_greaterThan by auto      { fix y        assume "y:(S Int ball x d - {x})"        then have "y:S & 0 < dist y x & dist y x < d"          unfolding ball_def          apply (simp add: dist_commute)          apply (metis dist_eq_0_iff less_le zero_le_dist)          done        then have "B <= f y" using d_def by auto      }      then have "B <= INFI (S Int ball x d - {x}) f"        apply (subst INF_greatest)        apply auto        done      also have "...<=?l"        apply (subst SUP_upper)        using d_def apply auto        done      finally have "B<=?l" by auto    }    then have "z <= ?l" using ereal_le_ereal[of z "?l"] by auto  }  ultimately show ?thesis    unfolding ereal_Liminf_Sup_monoset eventually_within    apply (subst ereal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e - {x}) f)"])    apply auto    doneqedlemma Limsup_within:  fixes f :: "'a::metric_space => ereal"  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"proof -  let ?l = "(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"  { fix T    assume T_def: "open T & mono_set (uminus ` T) & ?l:T"    have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"    proof -      { assume "T = UNIV"        then have ?thesis by (simp add: gt_ex) }      moreover      { assume "T ≠ UNIV"        then have "~(uminus ` T = UNIV)"          by (metis Int_UNIV_right Int_absorb1 image_mono ereal_minus_minus_image subset_UNIV)        then have "uminus ` T = {Inf (uminus ` T)<..}"          using T_def ereal_open_mono_set[of "uminus ` T"] ereal_open_uminus[of T] by auto        then obtain B where "T={..<B}"          unfolding ereal_Inf_uminus_image_eq ereal_uminus_lessThan[symmetric]          unfolding inj_image_eq_iff[OF ereal_inj_on_uminus] by simp        then have "?l<B" using T_def by auto        then obtain d where d_def: "0<d & (SUP y:(S Int ball x d - {x}). f y)<B"          unfolding INF_less_iff by auto        { fix y          assume "y:S & 0 < dist y x & dist y x < d"          then have "y:(S Int ball x d - {x})"            unfolding ball_def by (auto simp add: dist_commute)          then have "f y:T"            using d_def SUP_upper[of y "S Int ball x d - {x}" f] `T={..<B}` by auto        }        then have ?thesis          apply (rule_tac x="d" in exI)          using d_def apply auto          done      }      ultimately show ?thesis by auto    qed  }  moreover  { fix z    assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T -->       (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"    { fix B      assume "z<B"      then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"         using a[rule_format, of "{..<B}"] by auto      { fix y        assume "y:(S Int ball x d - {x})"        then have "y:S & 0 < dist y x & dist y x < d"          unfolding ball_def          apply (simp add: dist_commute)          apply (metis dist_eq_0_iff less_le zero_le_dist)          done        then have "f y <= B" using d_def by auto      }      then have "SUPR (S Int ball x d - {x}) f <= B"        apply (subst SUP_least)        apply auto        done      moreover      have "?l<=SUPR (S Int ball x d - {x}) f"        apply (subst INF_lower)        using d_def apply auto        done      ultimately have "?l<=B" by auto    } then have "?l <= z" using ereal_ge_ereal[of z "?l"] by auto  }  ultimately show ?thesis    unfolding ereal_Limsup_Inf_monoset eventually_within    apply (subst ereal_InfI)    apply auto    doneqedlemma Liminf_within_UNIV:  fixes f :: "'a::metric_space => ereal"  shows "Liminf (at x) f = Liminf (at x within UNIV) f"  by simp (* TODO: delete *)lemma Liminf_at:  fixes f :: "'a::metric_space => ereal"  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"  using Liminf_within[of x UNIV f] by simplemma Limsup_within_UNIV:  fixes f :: "'a::metric_space => ereal"  shows "Limsup (at x) f = Limsup (at x within UNIV) f"  by simp (* TODO: delete *)lemma Limsup_at:  fixes f :: "'a::metric_space => ereal"  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"  using Limsup_within[of x UNIV f] by simplemma Lim_within_constant:  assumes "ALL y:S. f y = C"  shows "(f ---> C) (at x within S)"  unfolding tendsto_def Limits.eventually_within eventually_at_topological  using assms by simp (metis open_UNIV UNIV_I)lemma Liminf_within_constant:  fixes f :: "'a::topological_space => ereal"  assumes "ALL y:S. f y = C"    and "~trivial_limit (at x within S)"  shows "Liminf (at x within S) f = C"  by (metis Lim_within_constant assms lim_imp_Liminf)lemma Limsup_within_constant:  fixes f :: "'a::topological_space => ereal"  assumes "ALL y:S. f y = C"    and "~trivial_limit (at x within S)"  shows "Limsup (at x within S) f = C"  by (metis Lim_within_constant assms lim_imp_Limsup)lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"  unfolding islimpt_def by blastlemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"  unfolding closure_def using islimpt_punctured by blastlemma not_trivial_limit_within: "~trivial_limit (at x within S) = (x:closure(S-{x}))"  using islimpt_in_closure by (metis trivial_limit_within)lemma not_trivial_limit_within_ball:  "(~trivial_limit (at x within S)) = (ALL e>0. S Int ball x e - {x} ~= {})"  (is "?lhs = ?rhs")proof -  { assume "?lhs"    { fix e :: real      assume "e>0"      then obtain y where "y:(S-{x}) & dist y x < e"        using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]        by auto      then have "y : (S Int ball x e - {x})"        unfolding ball_def by (simp add: dist_commute)      then have "S Int ball x e - {x} ~= {}" by blast    } then have "?rhs" by auto  }  moreover  { assume "?rhs"    { fix e :: real      assume "e>0"      then obtain y where "y : (S Int ball x e - {x})" using `?rhs` by blast      then have "y:(S-{x}) & dist y x < e"        unfolding ball_def by (simp add: dist_commute)      then have "EX y:(S-{x}). dist y x < e" by auto    }    then have "?lhs"      using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto  }  ultimately show ?thesis by autoqedlemma liminf_ereal_cminus:  fixes f :: "nat => ereal"  assumes "c ≠ -∞"  shows "liminf (λx. c - f x) = c - limsup f"proof (cases c)  case PInf  then show ?thesis by (simp add: Liminf_const)next  case (real r)  then show ?thesis    unfolding liminf_SUPR_INFI limsup_INFI_SUPR    apply (subst INFI_ereal_cminus)    apply auto    apply (subst SUPR_ereal_cminus)    apply auto    doneqed (insert `c ≠ -∞`, simp)subsubsection {* Continuity *}lemma continuous_imp_tendsto:  assumes "continuous (at x0) f"    and "x ----> x0"  shows "(f o x) ----> (f x0)"proof -  { fix S    assume "open S & (f x0):S"    then obtain T where T_def: "open T & x0 : T & (ALL x:T. f x : S)"       using assms continuous_at_open by metis    then have "(EX N. ALL n>=N. x n : T)"      using assms tendsto_explicit T_def by auto    then have "(EX N. ALL n>=N. f(x n) : S)" using T_def by auto  }  then show ?thesis using tendsto_explicit[of "f o x" "f x0"] by autoqedlemma continuous_at_sequentially2:  fixes f :: "'a::metric_space => 'b:: topological_space"  shows "continuous (at x0) f <-> (ALL x. (x ----> x0) --> (f o x) ----> (f x0))"proof -  { assume "~(continuous (at x0) f)"    then obtain T where      T_def: "open T & f x0 : T & (ALL S. (open S & x0 : S) --> (EX x':S. f x' ~: T))"      using continuous_at_open[of x0 f] by metis    def X == "{x'. f x' ~: T}"    then have "x0 islimpt X"      unfolding islimpt_def using T_def by auto    then obtain x where x_def: "(ALL n. x n : X) & x ----> x0"      using islimpt_sequential[of x0 X] by auto    then have "~(f o x) ----> (f x0)"      unfolding tendsto_explicit using X_def T_def by auto    then have "EX x. x ----> x0 & (~(f o x) ----> (f x0))" using x_def by auto  }  then show ?thesis using continuous_imp_tendsto by autoqedlemma continuous_at_of_ereal:  fixes x0 :: ereal  assumes "¦x0¦ ≠ ∞"  shows "continuous (at x0) real"proof -  { fix T    assume T_def: "open T & real x0 : T"    def S == "ereal ` T"    then have "ereal (real x0) : S" using T_def by auto    then have "x0 : S" using assms ereal_real by auto    moreover have "open S" using open_ereal S_def T_def by auto    moreover have "ALL y:S. real y : T" using S_def T_def by auto    ultimately have "EX S. x0 : S & open S & (ALL y:S. real y : T)" by auto  }  then show ?thesis unfolding continuous_at_open by blastqedlemma continuous_at_iff_ereal:  fixes f :: "'a::t2_space => real"  shows "continuous (at x0) f <-> continuous (at x0) (ereal o f)"proof -  { assume "continuous (at x0) f"    then have "continuous (at x0) (ereal o f)"      using continuous_at_ereal continuous_at_compose[of x0 f ereal] by auto  }  moreover  { assume "continuous (at x0) (ereal o f)"    then have "continuous (at x0) (real o (ereal o f))"      using continuous_at_of_ereal by (intro continuous_at_compose[of x0 "ereal o f"]) auto    moreover have "real o (ereal o f) = f" using real_ereal_id by (simp add: o_assoc)    ultimately have "continuous (at x0) f" by auto  } ultimately show ?thesis by autoqedlemma continuous_on_iff_ereal:  fixes f :: "'a::t2_space => real"  fixes A assumes "open A"  shows "continuous_on A f <-> continuous_on A (ereal o f)"  using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at)lemma continuous_on_real: "continuous_on (UNIV-{∞,(-∞::ereal)}) real"  using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal by autolemma continuous_on_iff_real:  fixes f :: "'a::t2_space => ereal"  assumes "!!x. x ∈ A ==> ¦f x¦ ≠ ∞"  shows "continuous_on A f <-> continuous_on A (real o f)"proof -  have "f ` A <= UNIV-{∞,(-∞)}" using assms by force  then have *: "continuous_on (f ` A) real"    using continuous_on_real by (simp add: continuous_on_subset)  have **: "continuous_on ((real o f) ` A) ereal"    using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real o f) ` A"] by blast  { assume "continuous_on A f"    then have "continuous_on A (real o f)"      apply (subst continuous_on_compose)      using * apply auto      done  }  moreover  { assume "continuous_on A (real o f)"    then have "continuous_on A (ereal o (real o f))"      apply (subst continuous_on_compose)      using ** apply auto      done    then have "continuous_on A f"      apply (subst continuous_on_eq[of A "ereal o (real o f)" f])      using assms ereal_real apply auto      done  }  ultimately show ?thesis by autoqedlemma continuous_at_const:  fixes f :: "'a::t2_space => ereal"  assumes "ALL x. (f x = C)"  shows "ALL x. continuous (at x) f"  unfolding continuous_at_open using assms t1_space by autolemma closure_contains_Inf:  fixes S :: "real set"  assumes "S ~= {}" "EX B. ALL x:S. B<=x"  shows "Inf S : closure S"proof -  have *: "ALL x:S. Inf S <= x"    using Inf_lower_EX[of _ S] assms by metis  { fix e    assume "e>(0 :: real)"    then obtain x where x_def: "x:S & x < Inf S + e" using Inf_close `S ~= {}` by auto    moreover then have "x > Inf S - e" using * by auto    ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)    then have "EX x:S. abs (x - Inf S) < e" using x_def by auto  }  then show ?thesis    apply (subst closure_approachable)    unfolding dist_norm apply auto    doneqedlemma closed_contains_Inf:  fixes S :: "real set"  assumes "S ~= {}" "EX B. ALL x:S. B<=x"    and "closed S"  shows "Inf S : S"  by (metis closure_contains_Inf closure_closed assms)lemma mono_closed_real:  fixes S :: "real set"  assumes mono: "ALL y z. y:S & y<=z --> z:S"    and "closed S"  shows "S = {} | S = UNIV | (EX a. S = {a ..})"proof -  { assume "S ~= {}"    { assume ex: "EX B. ALL x:S. B<=x"      then have *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] ex by metis      then have "Inf S : S" apply (subst closed_contains_Inf) using ex `S ~= {}` `closed S` by auto      then have "ALL x. (Inf S <= x <-> x:S)" using mono[rule_format, of "Inf S"] * by auto      then have "S = {Inf S ..}" by auto      then have "EX a. S = {a ..}" by auto    }    moreover    { assume "~(EX B. ALL x:S. B<=x)"      then have nex: "ALL B. EX x:S. x<B" by (simp add: not_le)      { fix y        obtain x where "x:S & x < y" using nex by auto        then have "y:S" using mono[rule_format, of x y] by auto      } then have "S = UNIV" by auto    }    ultimately have "S = UNIV | (EX a. S = {a ..})" by blast  } then show ?thesis by blastqedlemma mono_closed_ereal:  fixes S :: "real set"  assumes mono: "ALL y z. y:S & y<=z --> z:S"    and "closed S"  shows "EX a. S = {x. a <= ereal x}"proof -  { assume "S = {}"    then have ?thesis apply(rule_tac x=PInfty in exI) by auto }  moreover  { assume "S = UNIV"    then have ?thesis apply(rule_tac x="-∞" in exI) by auto }  moreover  { assume "EX a. S = {a ..}"    then obtain a where "S={a ..}" by auto    then have ?thesis apply(rule_tac x="ereal a" in exI) by auto  }  ultimately show ?thesis using mono_closed_real[of S] assms by autoqedsubsection {* Sums *}lemma setsum_ereal[simp]: "(∑x∈A. ereal (f x)) = ereal (∑x∈A. f x)"proof cases  assume "finite A"  then show ?thesis by induct autoqed simplemma setsum_Pinfty:  fixes f :: "'a => ereal"  shows "(∑x∈P. f x) = ∞ <-> (finite P ∧ (∃i∈P. f i = ∞))"proof safe  assume *: "setsum f P = ∞"  show "finite P"  proof (rule ccontr) assume "infinite P" with * show False by auto qed  show "∃i∈P. f i = ∞"  proof (rule ccontr)    assume "¬ ?thesis" then have "!!i. i ∈ P ==> f i ≠ ∞" by auto    from `finite P` this have "setsum f P ≠ ∞"      by induct auto    with * show False by auto  qednext  fix i assume "finite P" "i ∈ P" "f i = ∞"  then show "setsum f P = ∞"  proof induct    case (insert x A)    show ?case using insert by (cases "x = i") auto  qed simpqedlemma setsum_Inf:  fixes f :: "'a => ereal"  shows "¦setsum f A¦ = ∞ <-> (finite A ∧ (∃i∈A. ¦f i¦ = ∞))"proof  assume *: "¦setsum f A¦ = ∞"  have "finite A" by (rule ccontr) (insert *, auto)  moreover have "∃i∈A. ¦f i¦ = ∞"  proof (rule ccontr)    assume "¬ ?thesis" then have "∀i∈A. ∃r. f i = ereal r" by auto    from bchoice[OF this] guess r ..    with * show False by auto  qed  ultimately show "finite A ∧ (∃i∈A. ¦f i¦ = ∞)" by autonext  assume "finite A ∧ (∃i∈A. ¦f i¦ = ∞)"  then obtain i where "finite A" "i ∈ A" "¦f i¦ = ∞" by auto  then show "¦setsum f A¦ = ∞"  proof induct    case (insert j A) then show ?case      by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto  qed simpqedlemma setsum_real_of_ereal:  fixes f :: "'i => ereal"  assumes "!!x. x ∈ S ==> ¦f x¦ ≠ ∞"  shows "(∑x∈S. real (f x)) = real (setsum f S)"proof -  have "∀x∈S. ∃r. f x = ereal r"  proof    fix x assume "x ∈ S"    from assms[OF this] show "∃r. f x = ereal r" by (cases "f x") auto  qed  from bchoice[OF this] guess r ..  then show ?thesis by simpqedlemma setsum_ereal_0:  fixes f :: "'a => ereal" assumes "finite A" "!!i. i ∈ A ==> 0 ≤ f i"  shows "(∑x∈A. f x) = 0 <-> (∀i∈A. f i = 0)"proof  assume *: "(∑x∈A. f x) = 0"  then have "(∑x∈A. f x) ≠ ∞" by auto  then have "∀i∈A. ¦f i¦ ≠ ∞" using assms by (force simp: setsum_Pinfty)  then have "∀i∈A. ∃r. f i = ereal r" by auto  from bchoice[OF this] * assms show "∀i∈A. f i = 0"    using setsum_nonneg_eq_0_iff[of A "λi. real (f i)"] by autoqed (rule setsum_0')lemma setsum_ereal_right_distrib:  fixes f :: "'a => ereal"  assumes "!!i. i ∈ A ==> 0 ≤ f i"  shows "r * setsum f A = (∑n∈A. r * f n)"proof cases  assume "finite A"  then show ?thesis using assms    by induct (auto simp: ereal_right_distrib setsum_nonneg)qed simplemma sums_ereal_positive:  fixes f :: "nat => ereal"  assumes "!!i. 0 ≤ f i"  shows "f sums (SUP n. ∑i<n. f i)"proof -  have "incseq (λi. ∑j=0..<i. f j)"    using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)  from LIMSEQ_ereal_SUPR[OF this]  show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)qedlemma summable_ereal_pos:  fixes f :: "nat => ereal"  assumes "!!i. 0 ≤ f i"  shows "summable f"  using sums_ereal_positive[of f, OF assms] unfolding summable_def by autolemma suminf_ereal_eq_SUPR:  fixes f :: "nat => ereal"  assumes "!!i. 0 ≤ f i"  shows "(∑x. f x) = (SUP n. ∑i<n. f i)"  using sums_ereal_positive[of f, OF assms, THEN sums_unique] by simplemma sums_ereal: "(λx. ereal (f x)) sums ereal x <-> f sums x"  unfolding sums_def by simplemma suminf_bound:  fixes f :: "nat => ereal"  assumes "∀N. (∑n<N. f n) ≤ x" and pos: "!!n. 0 ≤ f n"  shows "suminf f ≤ x"proof (rule Lim_bounded_ereal)  have "summable f" using pos[THEN summable_ereal_pos] .  then show "(λN. ∑n<N. f n) ----> suminf f"    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)  show "∀n≥0. setsum f {..<n} ≤ x"    using assms by autoqedlemma suminf_bound_add:  fixes f :: "nat => ereal"  assumes "∀N. (∑n<N. f n) + y ≤ x"    and pos: "!!n. 0 ≤ f n"    and "y ≠ -∞"  shows "suminf f + y ≤ x"proof (cases y)  case (real r)  then have "∀N. (∑n<N. f n) ≤ x - y"    using assms by (simp add: ereal_le_minus)  then have "(∑ n. f n) ≤ x - y" using pos by (rule suminf_bound)  then show "(∑ n. f n) + y ≤ x"    using assms real by (simp add: ereal_le_minus)qed (insert assms, auto)lemma suminf_upper:  fixes f :: "nat => ereal"  assumes "!!n. 0 ≤ f n"  shows "(∑n<N. f n) ≤ (∑n. f n)"  unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def  by (auto intro: complete_lattice_class.Sup_upper)lemma suminf_0_le:  fixes f :: "nat => ereal"  assumes "!!n. 0 ≤ f n"  shows "0 ≤ (∑n. f n)"  using suminf_upper[of f 0, OF assms] by simplemma suminf_le_pos:  fixes f g :: "nat => ereal"  assumes "!!N. f N ≤ g N" "!!N. 0 ≤ f N"  shows "suminf f ≤ suminf g"proof (safe intro!: suminf_bound)  fix n  { fix N have "0 ≤ g N" using assms(2,1)[of N] by auto }  have "setsum f {..<n} ≤ setsum g {..<n}"    using assms by (auto intro: setsum_mono)  also have "... ≤ suminf g" using `!!N. 0 ≤ g N` by (rule suminf_upper)  finally show "setsum f {..<n} ≤ suminf g" .qed (rule assms(2))lemma suminf_half_series_ereal: "(∑n. (1/2 :: ereal)^Suc n) = 1"  using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]  by (simp add: one_ereal_def)lemma suminf_add_ereal:  fixes f g :: "nat => ereal"  assumes "!!i. 0 ≤ f i" "!!i. 0 ≤ g i"  shows "(∑i. f i + g i) = suminf f + suminf g"  apply (subst (1 2 3) suminf_ereal_eq_SUPR)  unfolding setsum_addf  apply (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+  donelemma suminf_cmult_ereal:  fixes f g :: "nat => ereal"  assumes "!!i. 0 ≤ f i" "0 ≤ a"  shows "(∑i. a * f i) = a * suminf f"  by (auto simp: setsum_ereal_right_distrib[symmetric] assms                 ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR           intro!: SUPR_ereal_cmult )lemma suminf_PInfty:  fixes f :: "nat => ereal"  assumes "!!i. 0 ≤ f i" "suminf f ≠ ∞"  shows "f i ≠ ∞"proof -  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)  have "(∑i<Suc i. f i) ≠ ∞" by auto  then show ?thesis unfolding setsum_Pinfty by simpqedlemma suminf_PInfty_fun:  assumes "!!i. 0 ≤ f i" "suminf f ≠ ∞"  shows "∃f'. f = (λx. ereal (f' x))"proof -  have "∀i. ∃r. f i = ereal r"  proof    fix i show "∃r. f i = ereal r"      using suminf_PInfty[OF assms] assms(1)[of i] by (cases "f i") auto  qed  from choice[OF this] show ?thesis by autoqedlemma summable_ereal:  assumes "!!i. 0 ≤ f i" "(∑i. ereal (f i)) ≠ ∞"  shows "summable f"proof -  have "0 ≤ (∑i. ereal (f i))"    using assms by (intro suminf_0_le) auto  with assms obtain r where r: "(∑i. ereal (f i)) = ereal r"    by (cases "∑i. ereal (f i)") auto  from summable_ereal_pos[of "λx. ereal (f x)"]  have "summable (λx. ereal (f x))" using assms by auto  from summable_sums[OF this]  have "(λx. ereal (f x)) sums (∑x. ereal (f x))" by auto  then show "summable f"    unfolding r sums_ereal summable_def ..qedlemma suminf_ereal:  assumes "!!i. 0 ≤ f i" "(∑i. ereal (f i)) ≠ ∞"  shows "(∑i. ereal (f i)) = ereal (suminf f)"proof (rule sums_unique[symmetric])  from summable_ereal[OF assms]  show "(λx. ereal (f x)) sums (ereal (suminf f))"    unfolding sums_ereal using assms by (intro summable_sums summable_ereal)qedlemma suminf_ereal_minus:  fixes f g :: "nat => ereal"  assumes ord: "!!i. g i ≤ f i" "!!i. 0 ≤ g i" and fin: "suminf f ≠ ∞" "suminf g ≠ ∞"  shows "(∑i. f i - g i) = suminf f - suminf g"proof -  { fix i have "0 ≤ f i" using ord[of i] by auto }  moreover  from suminf_PInfty_fun[OF `!!i. 0 ≤ f i` fin(1)] guess f' .. note this[simp]  from suminf_PInfty_fun[OF `!!i. 0 ≤ g i` fin(2)] guess g' .. note this[simp]  { fix i have "0 ≤ f i - g i" using ord[of i] by (auto simp: ereal_le_minus_iff) }  moreover  have "suminf (λi. f i - g i) ≤ suminf f"    using assms by (auto intro!: suminf_le_pos simp: field_simps)  then have "suminf (λi. f i - g i) ≠ ∞" using fin by auto  ultimately show ?thesis using assms `!!i. 0 ≤ f i`    apply simp    apply (subst (1 2 3) suminf_ereal)    apply (auto intro!: suminf_diff[symmetric] summable_ereal)    doneqedlemma suminf_ereal_PInf [simp]: "(∑x. ∞::ereal) = ∞"proof -  have "(∑i<Suc 0. ∞) ≤ (∑x. ∞::ereal)" by (rule suminf_upper) auto  then show ?thesis by simpqedlemma summable_real_of_ereal:  fixes f :: "nat => ereal"  assumes f: "!!i. 0 ≤ f i"    and fin: "(∑i. f i) ≠ ∞"  shows "summable (λi. real (f i))"proof (rule summable_def[THEN iffD2])  have "0 ≤ (∑i. f i)" using assms by (auto intro: suminf_0_le)  with fin obtain r where r: "ereal r = (∑i. f i)" by (cases "(∑i. f i)") auto  { fix i have "f i ≠ ∞" using f by (intro suminf_PInfty[OF _ fin]) auto    then have "¦f i¦ ≠ ∞" using f[of i] by auto }  note fin = this  have "(λi. ereal (real (f i))) sums (∑i. ereal (real (f i)))"    using f by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)  also have "… = ereal r" using fin r by (auto simp: ereal_real)  finally show "∃r. (λi. real (f i)) sums r" by (auto simp: sums_ereal)qedlemma suminf_SUP_eq:  fixes f :: "nat => nat => ereal"  assumes "!!i. incseq (λn. f n i)" "!!n i. 0 ≤ f n i"  shows "(∑i. SUP n. f n i) = (SUP n. ∑i. f n i)"proof -  { fix n :: nat    have "(∑i<n. SUP k. f k i) = (SUP k. ∑i<n. f k i)"      using assms by (auto intro!: SUPR_ereal_setsum[symmetric]) }  note * = this  show ?thesis using assms    apply (subst (1 2) suminf_ereal_eq_SUPR)    unfolding *    apply (auto intro!: SUP_upper2)    apply (subst SUP_commute)    apply rule    doneqedlemma suminf_setsum_ereal:  fixes f :: "_ => _ => ereal"  assumes nonneg: "!!i a. a ∈ A ==> 0 ≤ f i a"  shows "(∑i. ∑a∈A. f i a) = (∑a∈A. ∑i. f i a)"proof cases  assume "finite A"  then show ?thesis using nonneg    by induct (simp_all add: suminf_add_ereal setsum_nonneg)qed simplemma suminf_ereal_eq_0:  fixes f :: "nat => ereal"  assumes nneg: "!!i. 0 ≤ f i"  shows "(∑i. f i) = 0 <-> (∀i. f i = 0)"proof  assume "(∑i. f i) = 0"  { fix i assume "f i ≠ 0"    with nneg have "0 < f i" by (auto simp: less_le)    also have "f i = (∑j. if j = i then f i else 0)"      by (subst suminf_finite[where N="{i}"]) auto    also have "… ≤ (∑i. f i)"      using nneg by (auto intro!: suminf_le_pos)    finally have False using `(∑i. f i) = 0` by auto }  then show "∀i. f i = 0" by autoqed simpend`