src/HOL/Library/Extended_Real.thy
author nipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 61225 1a690dce8cfc
parent 61188 b34551d94934
child 61245 b77bf45efe21
permissions -rw-r--r--
tuned references
     1 (*  Title:      HOL/Library/Extended_Real.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 \<open>Extended real number line\<close>
     9 
    10 theory Extended_Real
    11 imports Complex_Main Extended_Nat Liminf_Limsup
    12 begin
    13 
    14 text \<open>
    15 
    16 This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
    17 AFP-entry @{text "Jinja_Thread"} fails, as it does overload certain named from @{theory Complex_Main}.
    18 
    19 \<close>
    20 
    21 lemma continuous_at_left_imp_sup_continuous:
    22   fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
    23   assumes "mono f" "\<And>x. continuous (at_left x) f"
    24   shows "sup_continuous f"
    25   unfolding sup_continuous_def
    26 proof safe
    27   fix M :: "nat \<Rightarrow> 'a" assume "incseq M" then show "f (SUP i. M i) = (SUP i. f (M i))"
    28     using continuous_at_Sup_mono[OF assms, of "range M"] by simp
    29 qed
    30 
    31 lemma sup_continuous_at_left:
    32   fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
    33   assumes f: "sup_continuous f"
    34   shows "continuous (at_left x) f"
    35 proof cases
    36   assume "x = bot" then show ?thesis
    37     by (simp add: trivial_limit_at_left_bot)
    38 next
    39   assume x: "x \<noteq> bot" 
    40   show ?thesis
    41     unfolding continuous_within
    42   proof (intro tendsto_at_left_sequentially[of bot])
    43     fix S :: "nat \<Rightarrow> 'a" assume S: "incseq S" and S_x: "S ----> x"
    44     from S_x have x_eq: "x = (SUP i. S i)"
    45       by (rule LIMSEQ_unique) (intro LIMSEQ_SUP S)
    46     show "(\<lambda>n. f (S n)) ----> f x"
    47       unfolding x_eq sup_continuousD[OF f S]
    48       using S sup_continuous_mono[OF f] by (intro LIMSEQ_SUP) (auto simp: mono_def)
    49   qed (insert x, auto simp: bot_less)
    50 qed
    51 
    52 lemma sup_continuous_iff_at_left:
    53   fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
    54   shows "sup_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_left x) f) \<and> mono f"
    55   using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f]
    56     sup_continuous_mono[of f] by auto
    57   
    58 lemma continuous_at_right_imp_inf_continuous:
    59   fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
    60   assumes "mono f" "\<And>x. continuous (at_right x) f"
    61   shows "inf_continuous f"
    62   unfolding inf_continuous_def
    63 proof safe
    64   fix M :: "nat \<Rightarrow> 'a" assume "decseq M" then show "f (INF i. M i) = (INF i. f (M i))"
    65     using continuous_at_Inf_mono[OF assms, of "range M"] by simp
    66 qed
    67 
    68 lemma inf_continuous_at_right:
    69   fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
    70   assumes f: "inf_continuous f"
    71   shows "continuous (at_right x) f"
    72 proof cases
    73   assume "x = top" then show ?thesis
    74     by (simp add: trivial_limit_at_right_top)
    75 next
    76   assume x: "x \<noteq> top" 
    77   show ?thesis
    78     unfolding continuous_within
    79   proof (intro tendsto_at_right_sequentially[of _ top])
    80     fix S :: "nat \<Rightarrow> 'a" assume S: "decseq S" and S_x: "S ----> x"
    81     from S_x have x_eq: "x = (INF i. S i)"
    82       by (rule LIMSEQ_unique) (intro LIMSEQ_INF S)
    83     show "(\<lambda>n. f (S n)) ----> f x"
    84       unfolding x_eq inf_continuousD[OF f S]
    85       using S inf_continuous_mono[OF f] by (intro LIMSEQ_INF) (auto simp: mono_def antimono_def)
    86   qed (insert x, auto simp: less_top)
    87 qed
    88 
    89 lemma inf_continuous_iff_at_right:
    90   fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
    91   shows "inf_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_right x) f) \<and> mono f"
    92   using inf_continuous_at_right[of f] continuous_at_right_imp_inf_continuous[of f]
    93     inf_continuous_mono[of f] by auto
    94 
    95 instantiation enat :: linorder_topology
    96 begin
    97 
    98 definition open_enat :: "enat set \<Rightarrow> bool" where
    99   "open_enat = generate_topology (range lessThan \<union> range greaterThan)"
   100 
   101 instance
   102   proof qed (rule open_enat_def)
   103 
   104 end
   105 
   106 lemma open_enat: "open {enat n}"
   107 proof (cases n)
   108   case 0
   109   then have "{enat n} = {..< eSuc 0}"
   110     by (auto simp: enat_0)
   111   then show ?thesis
   112     by simp
   113 next
   114   case (Suc n')
   115   then have "{enat n} = {enat n' <..< enat (Suc n)}"
   116     apply auto
   117     apply (case_tac x)
   118     apply auto
   119     done
   120   then show ?thesis
   121     by simp
   122 qed
   123 
   124 lemma open_enat_iff:
   125   fixes A :: "enat set"
   126   shows "open A \<longleftrightarrow> (\<infinity> \<in> A \<longrightarrow> (\<exists>n::nat. {n <..} \<subseteq> A))"
   127 proof safe
   128   assume "\<infinity> \<notin> A"
   129   then have "A = (\<Union>n\<in>{n. enat n \<in> A}. {enat n})"
   130     apply auto
   131     apply (case_tac x)
   132     apply auto
   133     done
   134   moreover have "open \<dots>"
   135     by (auto intro: open_enat)
   136   ultimately show "open A"
   137     by simp
   138 next
   139   fix n assume "{enat n <..} \<subseteq> A"
   140   then have "A = (\<Union>n\<in>{n. enat n \<in> A}. {enat n}) \<union> {enat n <..}"
   141     apply auto
   142     apply (case_tac x)
   143     apply auto
   144     done
   145   moreover have "open \<dots>"
   146     by (intro open_Un open_UN ballI open_enat open_greaterThan)
   147   ultimately show "open A"
   148     by simp
   149 next
   150   assume "open A" "\<infinity> \<in> A"
   151   then have "generate_topology (range lessThan \<union> range greaterThan) A" "\<infinity> \<in> A"
   152     unfolding open_enat_def by auto
   153   then show "\<exists>n::nat. {n <..} \<subseteq> A"
   154   proof induction
   155     case (Int A B)
   156     then obtain n m where "{enat n<..} \<subseteq> A" "{enat m<..} \<subseteq> B"
   157       by auto
   158     then have "{enat (max n m) <..} \<subseteq> A \<inter> B"
   159       by (auto simp add: subset_eq Ball_def max_def enat_ord_code(1)[symmetric] simp del: enat_ord_code(1))
   160     then show ?case
   161       by auto
   162   next
   163     case (UN K)
   164     then obtain k where "k \<in> K" "\<infinity> \<in> k"
   165       by auto
   166     with UN.IH[OF this] show ?case
   167       by auto
   168   qed auto
   169 qed
   170 
   171 
   172 text \<open>
   173 
   174 For more lemmas about the extended real numbers go to
   175   @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
   176 
   177 \<close>
   178 
   179 subsection \<open>Definition and basic properties\<close>
   180 
   181 datatype ereal = ereal real | PInfty | MInfty
   182 
   183 instantiation ereal :: uminus
   184 begin
   185 
   186 fun uminus_ereal where
   187   "- (ereal r) = ereal (- r)"
   188 | "- PInfty = MInfty"
   189 | "- MInfty = PInfty"
   190 
   191 instance ..
   192 
   193 end
   194 
   195 instantiation ereal :: infinity
   196 begin
   197 
   198 definition "(\<infinity>::ereal) = PInfty"
   199 instance ..
   200 
   201 end
   202 
   203 declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
   204 
   205 lemma ereal_uminus_uminus[simp]:
   206   fixes a :: ereal
   207   shows "- (- a) = a"
   208   by (cases a) simp_all
   209 
   210 lemma
   211   shows PInfty_eq_infinity[simp]: "PInfty = \<infinity>"
   212     and MInfty_eq_minfinity[simp]: "MInfty = - \<infinity>"
   213     and MInfty_neq_PInfty[simp]: "\<infinity> \<noteq> - (\<infinity>::ereal)" "- \<infinity> \<noteq> (\<infinity>::ereal)"
   214     and MInfty_neq_ereal[simp]: "ereal r \<noteq> - \<infinity>" "- \<infinity> \<noteq> ereal r"
   215     and PInfty_neq_ereal[simp]: "ereal r \<noteq> \<infinity>" "\<infinity> \<noteq> ereal r"
   216     and PInfty_cases[simp]: "(case \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = y"
   217     and MInfty_cases[simp]: "(case - \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = z"
   218   by (simp_all add: infinity_ereal_def)
   219 
   220 declare
   221   PInfty_eq_infinity[code_post]
   222   MInfty_eq_minfinity[code_post]
   223 
   224 lemma [code_unfold]:
   225   "\<infinity> = PInfty"
   226   "- PInfty = MInfty"
   227   by simp_all
   228 
   229 lemma inj_ereal[simp]: "inj_on ereal A"
   230   unfolding inj_on_def by auto
   231 
   232 lemma ereal_cases[cases type: ereal]:
   233   obtains (real) r where "x = ereal r"
   234     | (PInf) "x = \<infinity>"
   235     | (MInf) "x = -\<infinity>"
   236   using assms by (cases x) auto
   237 
   238 lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
   239 lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]
   240 
   241 lemma ereal_all_split: "\<And>P. (\<forall>x::ereal. P x) \<longleftrightarrow> P \<infinity> \<and> (\<forall>x. P (ereal x)) \<and> P (-\<infinity>)"
   242   by (metis ereal_cases)
   243 
   244 lemma ereal_ex_split: "\<And>P. (\<exists>x::ereal. P x) \<longleftrightarrow> P \<infinity> \<or> (\<exists>x. P (ereal x)) \<or> P (-\<infinity>)"
   245   by (metis ereal_cases)
   246 
   247 lemma ereal_uminus_eq_iff[simp]:
   248   fixes a b :: ereal
   249   shows "-a = -b \<longleftrightarrow> a = b"
   250   by (cases rule: ereal2_cases[of a b]) simp_all
   251 
   252 instantiation ereal :: real_of
   253 begin
   254 
   255 function real_ereal :: "ereal \<Rightarrow> real" where
   256   "real_ereal (ereal r) = r"
   257 | "real_ereal \<infinity> = 0"
   258 | "real_ereal (-\<infinity>) = 0"
   259   by (auto intro: ereal_cases)
   260 termination by standard (rule wf_empty)
   261 
   262 instance ..
   263 end
   264 
   265 lemma real_of_ereal[simp]:
   266   "real (- x :: ereal) = - (real x)"
   267   by (cases x) simp_all
   268 
   269 lemma range_ereal[simp]: "range ereal = UNIV - {\<infinity>, -\<infinity>}"
   270 proof safe
   271   fix x
   272   assume "x \<notin> range ereal" "x \<noteq> \<infinity>"
   273   then show "x = -\<infinity>"
   274     by (cases x) auto
   275 qed auto
   276 
   277 lemma ereal_range_uminus[simp]: "range uminus = (UNIV::ereal set)"
   278 proof safe
   279   fix x :: ereal
   280   show "x \<in> range uminus"
   281     by (intro image_eqI[of _ _ "-x"]) auto
   282 qed auto
   283 
   284 instantiation ereal :: abs
   285 begin
   286 
   287 function abs_ereal where
   288   "\<bar>ereal r\<bar> = ereal \<bar>r\<bar>"
   289 | "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"
   290 | "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"
   291 by (auto intro: ereal_cases)
   292 termination proof qed (rule wf_empty)
   293 
   294 instance ..
   295 
   296 end
   297 
   298 lemma abs_eq_infinity_cases[elim!]:
   299   fixes x :: ereal
   300   assumes "\<bar>x\<bar> = \<infinity>"
   301   obtains "x = \<infinity>" | "x = -\<infinity>"
   302   using assms by (cases x) auto
   303 
   304 lemma abs_neq_infinity_cases[elim!]:
   305   fixes x :: ereal
   306   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
   307   obtains r where "x = ereal r"
   308   using assms by (cases x) auto
   309 
   310 lemma abs_ereal_uminus[simp]:
   311   fixes x :: ereal
   312   shows "\<bar>- x\<bar> = \<bar>x\<bar>"
   313   by (cases x) auto
   314 
   315 lemma ereal_infinity_cases:
   316   fixes a :: ereal
   317   shows "a \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
   318   by auto
   319 
   320 
   321 subsubsection "Addition"
   322 
   323 instantiation ereal :: "{one,comm_monoid_add,zero_neq_one}"
   324 begin
   325 
   326 definition "0 = ereal 0"
   327 definition "1 = ereal 1"
   328 
   329 function plus_ereal where
   330   "ereal r + ereal p = ereal (r + p)"
   331 | "\<infinity> + a = (\<infinity>::ereal)"
   332 | "a + \<infinity> = (\<infinity>::ereal)"
   333 | "ereal r + -\<infinity> = - \<infinity>"
   334 | "-\<infinity> + ereal p = -(\<infinity>::ereal)"
   335 | "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
   336 proof goal_cases
   337   case prems: (1 P x)
   338   then obtain a b where "x = (a, b)"
   339     by (cases x) auto
   340   with prems show P
   341    by (cases rule: ereal2_cases[of a b]) auto
   342 qed auto
   343 termination by standard (rule wf_empty)
   344 
   345 lemma Infty_neq_0[simp]:
   346   "(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
   347   "-(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> -(\<infinity>::ereal)"
   348   by (simp_all add: zero_ereal_def)
   349 
   350 lemma ereal_eq_0[simp]:
   351   "ereal r = 0 \<longleftrightarrow> r = 0"
   352   "0 = ereal r \<longleftrightarrow> r = 0"
   353   unfolding zero_ereal_def by simp_all
   354 
   355 lemma ereal_eq_1[simp]:
   356   "ereal r = 1 \<longleftrightarrow> r = 1"
   357   "1 = ereal r \<longleftrightarrow> r = 1"
   358   unfolding one_ereal_def by simp_all
   359 
   360 instance
   361 proof
   362   fix a b c :: ereal
   363   show "0 + a = a"
   364     by (cases a) (simp_all add: zero_ereal_def)
   365   show "a + b = b + a"
   366     by (cases rule: ereal2_cases[of a b]) simp_all
   367   show "a + b + c = a + (b + c)"
   368     by (cases rule: ereal3_cases[of a b c]) simp_all
   369   show "0 \<noteq> (1::ereal)"
   370     by (simp add: one_ereal_def zero_ereal_def)
   371 qed
   372 
   373 end
   374 
   375 lemma ereal_0_plus [simp]: "ereal 0 + x = x"
   376   and plus_ereal_0 [simp]: "x + ereal 0 = x"
   377 by(simp_all add: zero_ereal_def[symmetric])
   378 
   379 instance ereal :: numeral ..
   380 
   381 lemma real_of_ereal_0[simp]: "real (0::ereal) = 0"
   382   unfolding zero_ereal_def by simp
   383 
   384 lemma abs_ereal_zero[simp]: "\<bar>0\<bar> = (0::ereal)"
   385   unfolding zero_ereal_def abs_ereal.simps by simp
   386 
   387 lemma ereal_uminus_zero[simp]: "- 0 = (0::ereal)"
   388   by (simp add: zero_ereal_def)
   389 
   390 lemma ereal_uminus_zero_iff[simp]:
   391   fixes a :: ereal
   392   shows "-a = 0 \<longleftrightarrow> a = 0"
   393   by (cases a) simp_all
   394 
   395 lemma ereal_plus_eq_PInfty[simp]:
   396   fixes a b :: ereal
   397   shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
   398   by (cases rule: ereal2_cases[of a b]) auto
   399 
   400 lemma ereal_plus_eq_MInfty[simp]:
   401   fixes a b :: ereal
   402   shows "a + b = -\<infinity> \<longleftrightarrow> (a = -\<infinity> \<or> b = -\<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>"
   403   by (cases rule: ereal2_cases[of a b]) auto
   404 
   405 lemma ereal_add_cancel_left:
   406   fixes a b :: ereal
   407   assumes "a \<noteq> -\<infinity>"
   408   shows "a + b = a + c \<longleftrightarrow> a = \<infinity> \<or> b = c"
   409   using assms by (cases rule: ereal3_cases[of a b c]) auto
   410 
   411 lemma ereal_add_cancel_right:
   412   fixes a b :: ereal
   413   assumes "a \<noteq> -\<infinity>"
   414   shows "b + a = c + a \<longleftrightarrow> a = \<infinity> \<or> b = c"
   415   using assms by (cases rule: ereal3_cases[of a b c]) auto
   416 
   417 lemma ereal_real: "ereal (real x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)"
   418   by (cases x) simp_all
   419 
   420 lemma real_of_ereal_add:
   421   fixes a b :: ereal
   422   shows "real (a + b) =
   423     (if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real a + real b else 0)"
   424   by (cases rule: ereal2_cases[of a b]) auto
   425 
   426 
   427 subsubsection "Linear order on @{typ ereal}"
   428 
   429 instantiation ereal :: linorder
   430 begin
   431 
   432 function less_ereal
   433 where
   434   "   ereal x < ereal y     \<longleftrightarrow> x < y"
   435 | "(\<infinity>::ereal) < a           \<longleftrightarrow> False"
   436 | "         a < -(\<infinity>::ereal) \<longleftrightarrow> False"
   437 | "ereal x    < \<infinity>           \<longleftrightarrow> True"
   438 | "        -\<infinity> < ereal r     \<longleftrightarrow> True"
   439 | "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
   440 proof goal_cases
   441   case prems: (1 P x)
   442   then obtain a b where "x = (a,b)" by (cases x) auto
   443   with prems show P by (cases rule: ereal2_cases[of a b]) auto
   444 qed simp_all
   445 termination by (relation "{}") simp
   446 
   447 definition "x \<le> (y::ereal) \<longleftrightarrow> x < y \<or> x = y"
   448 
   449 lemma ereal_infty_less[simp]:
   450   fixes x :: ereal
   451   shows "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)"
   452     "-\<infinity> < x \<longleftrightarrow> (x \<noteq> -\<infinity>)"
   453   by (cases x, simp_all) (cases x, simp_all)
   454 
   455 lemma ereal_infty_less_eq[simp]:
   456   fixes x :: ereal
   457   shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>"
   458     and "x \<le> -\<infinity> \<longleftrightarrow> x = -\<infinity>"
   459   by (auto simp add: less_eq_ereal_def)
   460 
   461 lemma ereal_less[simp]:
   462   "ereal r < 0 \<longleftrightarrow> (r < 0)"
   463   "0 < ereal r \<longleftrightarrow> (0 < r)"
   464   "ereal r < 1 \<longleftrightarrow> (r < 1)"
   465   "1 < ereal r \<longleftrightarrow> (1 < r)"
   466   "0 < (\<infinity>::ereal)"
   467   "-(\<infinity>::ereal) < 0"
   468   by (simp_all add: zero_ereal_def one_ereal_def)
   469 
   470 lemma ereal_less_eq[simp]:
   471   "x \<le> (\<infinity>::ereal)"
   472   "-(\<infinity>::ereal) \<le> x"
   473   "ereal r \<le> ereal p \<longleftrightarrow> r \<le> p"
   474   "ereal r \<le> 0 \<longleftrightarrow> r \<le> 0"
   475   "0 \<le> ereal r \<longleftrightarrow> 0 \<le> r"
   476   "ereal r \<le> 1 \<longleftrightarrow> r \<le> 1"
   477   "1 \<le> ereal r \<longleftrightarrow> 1 \<le> r"
   478   by (auto simp add: less_eq_ereal_def zero_ereal_def one_ereal_def)
   479 
   480 lemma ereal_infty_less_eq2:
   481   "a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = (\<infinity>::ereal)"
   482   "a \<le> b \<Longrightarrow> b = -\<infinity> \<Longrightarrow> a = -(\<infinity>::ereal)"
   483   by simp_all
   484 
   485 instance
   486 proof
   487   fix x y z :: ereal
   488   show "x \<le> x"
   489     by (cases x) simp_all
   490   show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
   491     by (cases rule: ereal2_cases[of x y]) auto
   492   show "x \<le> y \<or> y \<le> x "
   493     by (cases rule: ereal2_cases[of x y]) auto
   494   {
   495     assume "x \<le> y" "y \<le> x"
   496     then show "x = y"
   497       by (cases rule: ereal2_cases[of x y]) auto
   498   }
   499   {
   500     assume "x \<le> y" "y \<le> z"
   501     then show "x \<le> z"
   502       by (cases rule: ereal3_cases[of x y z]) auto
   503   }
   504 qed
   505 
   506 end
   507 
   508 lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
   509   using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
   510 
   511 instance ereal :: dense_linorder
   512   by standard (blast dest: ereal_dense2)
   513 
   514 instance ereal :: ordered_ab_semigroup_add
   515 proof
   516   fix a b c :: ereal
   517   assume "a \<le> b"
   518   then show "c + a \<le> c + b"
   519     by (cases rule: ereal3_cases[of a b c]) auto
   520 qed
   521 
   522 lemma real_of_ereal_positive_mono:
   523   fixes x y :: ereal
   524   shows "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> real x \<le> real y"
   525   by (cases rule: ereal2_cases[of x y]) auto
   526 
   527 lemma ereal_MInfty_lessI[intro, simp]:
   528   fixes a :: ereal
   529   shows "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
   530   by (cases a) auto
   531 
   532 lemma ereal_less_PInfty[intro, simp]:
   533   fixes a :: ereal
   534   shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"
   535   by (cases a) auto
   536 
   537 lemma ereal_less_ereal_Ex:
   538   fixes a b :: ereal
   539   shows "x < ereal r \<longleftrightarrow> x = -\<infinity> \<or> (\<exists>p. p < r \<and> x = ereal p)"
   540   by (cases x) auto
   541 
   542 lemma less_PInf_Ex_of_nat: "x \<noteq> \<infinity> \<longleftrightarrow> (\<exists>n::nat. x < ereal (real n))"
   543 proof (cases x)
   544   case (real r)
   545   then show ?thesis
   546     using reals_Archimedean2[of r] by simp
   547 qed simp_all
   548 
   549 lemma ereal_add_mono:
   550   fixes a b c d :: ereal
   551   assumes "a \<le> b"
   552     and "c \<le> d"
   553   shows "a + c \<le> b + d"
   554   using assms
   555   apply (cases a)
   556   apply (cases rule: ereal3_cases[of b c d], auto)
   557   apply (cases rule: ereal3_cases[of b c d], auto)
   558   done
   559 
   560 lemma ereal_minus_le_minus[simp]:
   561   fixes a b :: ereal
   562   shows "- a \<le> - b \<longleftrightarrow> b \<le> a"
   563   by (cases rule: ereal2_cases[of a b]) auto
   564 
   565 lemma ereal_minus_less_minus[simp]:
   566   fixes a b :: ereal
   567   shows "- a < - b \<longleftrightarrow> b < a"
   568   by (cases rule: ereal2_cases[of a b]) auto
   569 
   570 lemma ereal_le_real_iff:
   571   "x \<le> real y \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x \<le> y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x \<le> 0)"
   572   by (cases y) auto
   573 
   574 lemma real_le_ereal_iff:
   575   "real y \<le> x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y \<le> ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 \<le> x)"
   576   by (cases y) auto
   577 
   578 lemma ereal_less_real_iff:
   579   "x < real y \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0)"
   580   by (cases y) auto
   581 
   582 lemma real_less_ereal_iff:
   583   "real y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)"
   584   by (cases y) auto
   585 
   586 lemma real_of_ereal_pos:
   587   fixes x :: ereal
   588   shows "0 \<le> x \<Longrightarrow> 0 \<le> real x" by (cases x) auto
   589 
   590 lemmas real_of_ereal_ord_simps =
   591   ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff
   592 
   593 lemma abs_ereal_ge0[simp]: "0 \<le> x \<Longrightarrow> \<bar>x :: ereal\<bar> = x"
   594   by (cases x) auto
   595 
   596 lemma abs_ereal_less0[simp]: "x < 0 \<Longrightarrow> \<bar>x :: ereal\<bar> = -x"
   597   by (cases x) auto
   598 
   599 lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>"
   600   by (cases x) auto
   601 
   602 lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>"
   603   by (cases x) auto
   604 
   605 lemma abs_real_of_ereal[simp]: "\<bar>real (x :: ereal)\<bar> = real \<bar>x\<bar>"
   606   by (cases x) auto
   607 
   608 lemma zero_less_real_of_ereal:
   609   fixes x :: ereal
   610   shows "0 < real x \<longleftrightarrow> 0 < x \<and> x \<noteq> \<infinity>"
   611   by (cases x) auto
   612 
   613 lemma ereal_0_le_uminus_iff[simp]:
   614   fixes a :: ereal
   615   shows "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   616   by (cases rule: ereal2_cases[of a]) auto
   617 
   618 lemma ereal_uminus_le_0_iff[simp]:
   619   fixes a :: ereal
   620   shows "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   621   by (cases rule: ereal2_cases[of a]) auto
   622 
   623 lemma ereal_add_strict_mono:
   624   fixes a b c d :: ereal
   625   assumes "a \<le> b"
   626     and "0 \<le> a"
   627     and "a \<noteq> \<infinity>"
   628     and "c < d"
   629   shows "a + c < b + d"
   630   using assms
   631   by (cases rule: ereal3_cases[case_product ereal_cases, of a b c d]) auto
   632 
   633 lemma ereal_less_add:
   634   fixes a b c :: ereal
   635   shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"
   636   by (cases rule: ereal2_cases[of b c]) auto
   637 
   638 lemma ereal_add_nonneg_eq_0_iff:
   639   fixes a b :: ereal
   640   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
   641   by (cases a b rule: ereal2_cases) auto
   642 
   643 lemma ereal_uminus_eq_reorder: "- a = b \<longleftrightarrow> a = (-b::ereal)"
   644   by auto
   645 
   646 lemma ereal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < (a::ereal)"
   647   by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
   648 
   649 lemma ereal_less_uminus_reorder: "a < - b \<longleftrightarrow> b < - (a::ereal)"
   650   by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
   651 
   652 lemma ereal_uminus_le_reorder: "- a \<le> b \<longleftrightarrow> -b \<le> (a::ereal)"
   653   by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_le_minus)
   654 
   655 lemmas ereal_uminus_reorder =
   656   ereal_uminus_eq_reorder ereal_uminus_less_reorder ereal_uminus_le_reorder
   657 
   658 lemma ereal_bot:
   659   fixes x :: ereal
   660   assumes "\<And>B. x \<le> ereal B"
   661   shows "x = - \<infinity>"
   662 proof (cases x)
   663   case (real r)
   664   with assms[of "r - 1"] show ?thesis
   665     by auto
   666 next
   667   case PInf
   668   with assms[of 0] show ?thesis
   669     by auto
   670 next
   671   case MInf
   672   then show ?thesis
   673     by simp
   674 qed
   675 
   676 lemma ereal_top:
   677   fixes x :: ereal
   678   assumes "\<And>B. x \<ge> ereal B"
   679   shows "x = \<infinity>"
   680 proof (cases x)
   681   case (real r)
   682   with assms[of "r + 1"] show ?thesis
   683     by auto
   684 next
   685   case MInf
   686   with assms[of 0] show ?thesis
   687     by auto
   688 next
   689   case PInf
   690   then show ?thesis
   691     by simp
   692 qed
   693 
   694 lemma
   695   shows ereal_max[simp]: "ereal (max x y) = max (ereal x) (ereal y)"
   696     and ereal_min[simp]: "ereal (min x y) = min (ereal x) (ereal y)"
   697   by (simp_all add: min_def max_def)
   698 
   699 lemma ereal_max_0: "max 0 (ereal r) = ereal (max 0 r)"
   700   by (auto simp: zero_ereal_def)
   701 
   702 lemma
   703   fixes f :: "nat \<Rightarrow> ereal"
   704   shows ereal_incseq_uminus[simp]: "incseq (\<lambda>x. - f x) \<longleftrightarrow> decseq f"
   705     and ereal_decseq_uminus[simp]: "decseq (\<lambda>x. - f x) \<longleftrightarrow> incseq f"
   706   unfolding decseq_def incseq_def by auto
   707 
   708 lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))"
   709   unfolding incseq_def by auto
   710 
   711 lemma ereal_add_nonneg_nonneg[simp]:
   712   fixes a b :: ereal
   713   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
   714   using add_mono[of 0 a 0 b] by simp
   715 
   716 lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B"
   717   by auto
   718 
   719 lemma incseq_setsumI:
   720   fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
   721   assumes "\<And>i. 0 \<le> f i"
   722   shows "incseq (\<lambda>i. setsum f {..< i})"
   723 proof (intro incseq_SucI)
   724   fix n
   725   have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
   726     using assms by (rule add_left_mono)
   727   then show "setsum f {..< n} \<le> setsum f {..< Suc n}"
   728     by auto
   729 qed
   730 
   731 lemma incseq_setsumI2:
   732   fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
   733   assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
   734   shows "incseq (\<lambda>i. \<Sum>n\<in>A. f n i)"
   735   using assms
   736   unfolding incseq_def by (auto intro: setsum_mono)
   737 
   738 lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
   739 proof (cases "finite A")
   740   case True
   741   then show ?thesis by induct auto
   742 next
   743   case False
   744   then show ?thesis by simp
   745 qed
   746 
   747 lemma setsum_Pinfty:
   748   fixes f :: "'a \<Rightarrow> ereal"
   749   shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
   750 proof safe
   751   assume *: "setsum f P = \<infinity>"
   752   show "finite P"
   753   proof (rule ccontr)
   754     assume "\<not> finite P"
   755     with * show False
   756       by auto
   757   qed
   758   show "\<exists>i\<in>P. f i = \<infinity>"
   759   proof (rule ccontr)
   760     assume "\<not> ?thesis"
   761     then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>"
   762       by auto
   763     with \<open>finite P\<close> have "setsum f P \<noteq> \<infinity>"
   764       by induct auto
   765     with * show False
   766       by auto
   767   qed
   768 next
   769   fix i
   770   assume "finite P" and "i \<in> P" and "f i = \<infinity>"
   771   then show "setsum f P = \<infinity>"
   772   proof induct
   773     case (insert x A)
   774     show ?case using insert by (cases "x = i") auto
   775   qed simp
   776 qed
   777 
   778 lemma setsum_Inf:
   779   fixes f :: "'a \<Rightarrow> ereal"
   780   shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
   781 proof
   782   assume *: "\<bar>setsum f A\<bar> = \<infinity>"
   783   have "finite A"
   784     by (rule ccontr) (insert *, auto)
   785   moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>"
   786   proof (rule ccontr)
   787     assume "\<not> ?thesis"
   788     then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
   789       by auto
   790     from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" ..
   791     with * show False
   792       by auto
   793   qed
   794   ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
   795     by auto
   796 next
   797   assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
   798   then obtain i where "finite A" "i \<in> A" and "\<bar>f i\<bar> = \<infinity>"
   799     by auto
   800   then show "\<bar>setsum f A\<bar> = \<infinity>"
   801   proof induct
   802     case (insert j A)
   803     then show ?case
   804       by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
   805   qed simp
   806 qed
   807 
   808 lemma setsum_real_of_ereal:
   809   fixes f :: "'i \<Rightarrow> ereal"
   810   assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
   811   shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
   812 proof -
   813   have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
   814   proof
   815     fix x
   816     assume "x \<in> S"
   817     from assms[OF this] show "\<exists>r. f x = ereal r"
   818       by (cases "f x") auto
   819   qed
   820   from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" ..
   821   then show ?thesis
   822     by simp
   823 qed
   824 
   825 lemma setsum_ereal_0:
   826   fixes f :: "'a \<Rightarrow> ereal"
   827   assumes "finite A"
   828     and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
   829   shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
   830 proof
   831   assume "setsum f A = 0" with assms show "\<forall>i\<in>A. f i = 0"
   832   proof (induction A)
   833     case (insert a A)
   834     then have "f a = 0 \<and> (\<Sum>a\<in>A. f a) = 0"
   835       by (subst ereal_add_nonneg_eq_0_iff[symmetric]) (simp_all add: setsum_nonneg)
   836     with insert show ?case
   837       by simp
   838   qed simp
   839 qed auto
   840 
   841 subsubsection "Multiplication"
   842 
   843 instantiation ereal :: "{comm_monoid_mult,sgn}"
   844 begin
   845 
   846 function sgn_ereal :: "ereal \<Rightarrow> ereal" where
   847   "sgn (ereal r) = ereal (sgn r)"
   848 | "sgn (\<infinity>::ereal) = 1"
   849 | "sgn (-\<infinity>::ereal) = -1"
   850 by (auto intro: ereal_cases)
   851 termination by standard (rule wf_empty)
   852 
   853 function times_ereal where
   854   "ereal r * ereal p = ereal (r * p)"
   855 | "ereal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)"
   856 | "\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)"
   857 | "ereal r * -\<infinity> = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)"
   858 | "-\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)"
   859 | "(\<infinity>::ereal) * \<infinity> = \<infinity>"
   860 | "-(\<infinity>::ereal) * \<infinity> = -\<infinity>"
   861 | "(\<infinity>::ereal) * -\<infinity> = -\<infinity>"
   862 | "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
   863 proof goal_cases
   864   case prems: (1 P x)
   865   then obtain a b where "x = (a, b)"
   866     by (cases x) auto
   867   with prems show P
   868     by (cases rule: ereal2_cases[of a b]) auto
   869 qed simp_all
   870 termination by (relation "{}") simp
   871 
   872 instance
   873 proof
   874   fix a b c :: ereal
   875   show "1 * a = a"
   876     by (cases a) (simp_all add: one_ereal_def)
   877   show "a * b = b * a"
   878     by (cases rule: ereal2_cases[of a b]) simp_all
   879   show "a * b * c = a * (b * c)"
   880     by (cases rule: ereal3_cases[of a b c])
   881        (simp_all add: zero_ereal_def zero_less_mult_iff)
   882 qed
   883 
   884 end
   885 
   886 lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))"
   887   by (simp add: one_ereal_def zero_ereal_def)
   888 
   889 lemma real_ereal_1[simp]: "real (1::ereal) = 1"
   890   unfolding one_ereal_def by simp
   891 
   892 lemma real_of_ereal_le_1:
   893   fixes a :: ereal
   894   shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
   895   by (cases a) (auto simp: one_ereal_def)
   896 
   897 lemma abs_ereal_one[simp]: "\<bar>1\<bar> = (1::ereal)"
   898   unfolding one_ereal_def by simp
   899 
   900 lemma ereal_mult_zero[simp]:
   901   fixes a :: ereal
   902   shows "a * 0 = 0"
   903   by (cases a) (simp_all add: zero_ereal_def)
   904 
   905 lemma ereal_zero_mult[simp]:
   906   fixes a :: ereal
   907   shows "0 * a = 0"
   908   by (cases a) (simp_all add: zero_ereal_def)
   909 
   910 lemma ereal_m1_less_0[simp]: "-(1::ereal) < 0"
   911   by (simp add: zero_ereal_def one_ereal_def)
   912 
   913 lemma ereal_times[simp]:
   914   "1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1"
   915   "1 \<noteq> -(\<infinity>::ereal)" "-(\<infinity>::ereal) \<noteq> 1"
   916   by (auto simp: one_ereal_def)
   917 
   918 lemma ereal_plus_1[simp]:
   919   "1 + ereal r = ereal (r + 1)"
   920   "ereal r + 1 = ereal (r + 1)"
   921   "1 + -(\<infinity>::ereal) = -\<infinity>"
   922   "-(\<infinity>::ereal) + 1 = -\<infinity>"
   923   unfolding one_ereal_def by auto
   924 
   925 lemma ereal_zero_times[simp]:
   926   fixes a b :: ereal
   927   shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   928   by (cases rule: ereal2_cases[of a b]) auto
   929 
   930 lemma ereal_mult_eq_PInfty[simp]:
   931   "a * b = (\<infinity>::ereal) \<longleftrightarrow>
   932     (a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = -\<infinity>)"
   933   by (cases rule: ereal2_cases[of a b]) auto
   934 
   935 lemma ereal_mult_eq_MInfty[simp]:
   936   "a * b = -(\<infinity>::ereal) \<longleftrightarrow>
   937     (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = -\<infinity>)"
   938   by (cases rule: ereal2_cases[of a b]) auto
   939 
   940 lemma ereal_abs_mult: "\<bar>x * y :: ereal\<bar> = \<bar>x\<bar> * \<bar>y\<bar>"
   941   by (cases x y rule: ereal2_cases) (auto simp: abs_mult)
   942 
   943 lemma ereal_0_less_1[simp]: "0 < (1::ereal)"
   944   by (simp_all add: zero_ereal_def one_ereal_def)
   945 
   946 lemma ereal_mult_minus_left[simp]:
   947   fixes a b :: ereal
   948   shows "-a * b = - (a * b)"
   949   by (cases rule: ereal2_cases[of a b]) auto
   950 
   951 lemma ereal_mult_minus_right[simp]:
   952   fixes a b :: ereal
   953   shows "a * -b = - (a * b)"
   954   by (cases rule: ereal2_cases[of a b]) auto
   955 
   956 lemma ereal_mult_infty[simp]:
   957   "a * (\<infinity>::ereal) = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
   958   by (cases a) auto
   959 
   960 lemma ereal_infty_mult[simp]:
   961   "(\<infinity>::ereal) * a = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
   962   by (cases a) auto
   963 
   964 lemma ereal_mult_strict_right_mono:
   965   assumes "a < b"
   966     and "0 < c"
   967     and "c < (\<infinity>::ereal)"
   968   shows "a * c < b * c"
   969   using assms
   970   by (cases rule: ereal3_cases[of a b c]) (auto simp: zero_le_mult_iff)
   971 
   972 lemma ereal_mult_strict_left_mono:
   973   "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c < (\<infinity>::ereal) \<Longrightarrow> c * a < c * b"
   974   using ereal_mult_strict_right_mono
   975   by (simp add: mult.commute[of c])
   976 
   977 lemma ereal_mult_right_mono:
   978   fixes a b c :: ereal
   979   shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   980   using assms
   981   apply (cases "c = 0")
   982   apply simp
   983   apply (cases rule: ereal3_cases[of a b c])
   984   apply (auto simp: zero_le_mult_iff)
   985   done
   986 
   987 lemma ereal_mult_left_mono:
   988   fixes a b c :: ereal
   989   shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   990   using ereal_mult_right_mono
   991   by (simp add: mult.commute[of c])
   992 
   993 lemma zero_less_one_ereal[simp]: "0 \<le> (1::ereal)"
   994   by (simp add: one_ereal_def zero_ereal_def)
   995 
   996 lemma ereal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * (b :: ereal)"
   997   by (cases rule: ereal2_cases[of a b]) auto
   998 
   999 lemma ereal_right_distrib:
  1000   fixes r a b :: ereal
  1001   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> r * (a + b) = r * a + r * b"
  1002   by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)
  1003 
  1004 lemma ereal_left_distrib:
  1005   fixes r a b :: ereal
  1006   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (a + b) * r = a * r + b * r"
  1007   by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)
  1008 
  1009 lemma ereal_mult_le_0_iff:
  1010   fixes a b :: ereal
  1011   shows "a * b \<le> 0 \<longleftrightarrow> (0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b)"
  1012   by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_le_0_iff)
  1013 
  1014 lemma ereal_zero_le_0_iff:
  1015   fixes a b :: ereal
  1016   shows "0 \<le> a * b \<longleftrightarrow> (0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0)"
  1017   by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_le_mult_iff)
  1018 
  1019 lemma ereal_mult_less_0_iff:
  1020   fixes a b :: ereal
  1021   shows "a * b < 0 \<longleftrightarrow> (0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b)"
  1022   by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_less_0_iff)
  1023 
  1024 lemma ereal_zero_less_0_iff:
  1025   fixes a b :: ereal
  1026   shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)"
  1027   by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff)
  1028 
  1029 lemma ereal_left_mult_cong:
  1030   fixes a b c :: ereal
  1031   shows  "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * d"
  1032   by (cases "c = 0") simp_all
  1033 
  1034 lemma ereal_right_mult_cong: 
  1035   fixes a b c :: ereal
  1036   shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = d * b"
  1037   by (cases "c = 0") simp_all
  1038 
  1039 lemma ereal_distrib:
  1040   fixes a b c :: ereal
  1041   assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>"
  1042     and "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>"
  1043     and "\<bar>c\<bar> \<noteq> \<infinity>"
  1044   shows "(a + b) * c = a * c + b * c"
  1045   using assms
  1046   by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
  1047 
  1048 lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)"
  1049   apply (induct w rule: num_induct)
  1050   apply (simp only: numeral_One one_ereal_def)
  1051   apply (simp only: numeral_inc ereal_plus_1)
  1052   done
  1053 
  1054 lemma setsum_ereal_right_distrib:
  1055   fixes f :: "'a \<Rightarrow> ereal"
  1056   shows "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> r * setsum f A = (\<Sum>n\<in>A. r * f n)"
  1057   by (induct A rule: infinite_finite_induct)  (auto simp: ereal_right_distrib setsum_nonneg)
  1058 
  1059 lemma setsum_ereal_left_distrib:
  1060   "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> setsum f A * r = (\<Sum>n\<in>A. f n * r :: ereal)"
  1061   using setsum_ereal_right_distrib[of A f r] by (simp add: mult_ac)
  1062 
  1063 lemma ereal_le_epsilon:
  1064   fixes x y :: ereal
  1065   assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"
  1066   shows "x \<le> y"
  1067 proof -
  1068   {
  1069     assume a: "\<exists>r. y = ereal r"
  1070     then obtain r where r_def: "y = ereal r"
  1071       by auto
  1072     {
  1073       assume "x = -\<infinity>"
  1074       then have ?thesis by auto
  1075     }
  1076     moreover
  1077     {
  1078       assume "x \<noteq> -\<infinity>"
  1079       then obtain p where p_def: "x = ereal p"
  1080       using a assms[rule_format, of 1]
  1081         by (cases x) auto
  1082       {
  1083         fix e
  1084         have "0 < e \<longrightarrow> p \<le> r + e"
  1085           using assms[rule_format, of "ereal e"] p_def r_def by auto
  1086       }
  1087       then have "p \<le> r"
  1088         apply (subst field_le_epsilon)
  1089         apply auto
  1090         done
  1091       then have ?thesis
  1092         using r_def p_def by auto
  1093     }
  1094     ultimately have ?thesis
  1095       by blast
  1096   }
  1097   moreover
  1098   {
  1099     assume "y = -\<infinity> | y = \<infinity>"
  1100     then have ?thesis
  1101       using assms[rule_format, of 1] by (cases x) auto
  1102   }
  1103   ultimately show ?thesis
  1104     by (cases y) auto
  1105 qed
  1106 
  1107 lemma ereal_le_epsilon2:
  1108   fixes x y :: ereal
  1109   assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + ereal e"
  1110   shows "x \<le> y"
  1111 proof -
  1112   {
  1113     fix e :: ereal
  1114     assume "e > 0"
  1115     {
  1116       assume "e = \<infinity>"
  1117       then have "x \<le> y + e"
  1118         by auto
  1119     }
  1120     moreover
  1121     {
  1122       assume "e \<noteq> \<infinity>"
  1123       then obtain r where "e = ereal r"
  1124         using \<open>e > 0\<close> by (cases e) auto
  1125       then have "x \<le> y + e"
  1126         using assms[rule_format, of r] \<open>e>0\<close> by auto
  1127     }
  1128     ultimately have "x \<le> y + e"
  1129       by blast
  1130   }
  1131   then show ?thesis
  1132     using ereal_le_epsilon by auto
  1133 qed
  1134 
  1135 lemma ereal_le_real:
  1136   fixes x y :: ereal
  1137   assumes "\<forall>z. x \<le> ereal z \<longrightarrow> y \<le> ereal z"
  1138   shows "y \<le> x"
  1139   by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
  1140 
  1141 lemma setprod_ereal_0:
  1142   fixes f :: "'a \<Rightarrow> ereal"
  1143   shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. f i = 0)"
  1144 proof (cases "finite A")
  1145   case True
  1146   then show ?thesis by (induct A) auto
  1147 next
  1148   case False
  1149   then show ?thesis by auto
  1150 qed
  1151 
  1152 lemma setprod_ereal_pos:
  1153   fixes f :: "'a \<Rightarrow> ereal"
  1154   assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
  1155   shows "0 \<le> (\<Prod>i\<in>I. f i)"
  1156 proof (cases "finite I")
  1157   case True
  1158   from this pos show ?thesis
  1159     by induct auto
  1160 next
  1161   case False
  1162   then show ?thesis by simp
  1163 qed
  1164 
  1165 lemma setprod_PInf:
  1166   fixes f :: "'a \<Rightarrow> ereal"
  1167   assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
  1168   shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
  1169 proof (cases "finite I")
  1170   case True
  1171   from this assms show ?thesis
  1172   proof (induct I)
  1173     case (insert i I)
  1174     then have pos: "0 \<le> f i" "0 \<le> setprod f I"
  1175       by (auto intro!: setprod_ereal_pos)
  1176     from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>"
  1177       by auto
  1178     also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
  1179       using setprod_ereal_pos[of I f] pos
  1180       by (cases rule: ereal2_cases[of "f i" "setprod f I"]) auto
  1181     also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
  1182       using insert by (auto simp: setprod_ereal_0)
  1183     finally show ?case .
  1184   qed simp
  1185 next
  1186   case False
  1187   then show ?thesis by simp
  1188 qed
  1189 
  1190 lemma setprod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (setprod f A)"
  1191 proof (cases "finite A")
  1192   case True
  1193   then show ?thesis
  1194     by induct (auto simp: one_ereal_def)
  1195 next
  1196   case False
  1197   then show ?thesis
  1198     by (simp add: one_ereal_def)
  1199 qed
  1200 
  1201 
  1202 subsubsection \<open>Power\<close>
  1203 
  1204 lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)"
  1205   by (induct n) (auto simp: one_ereal_def)
  1206 
  1207 lemma ereal_power_PInf[simp]: "(\<infinity>::ereal) ^ n = (if n = 0 then 1 else \<infinity>)"
  1208   by (induct n) (auto simp: one_ereal_def)
  1209 
  1210 lemma ereal_power_uminus[simp]:
  1211   fixes x :: ereal
  1212   shows "(- x) ^ n = (if even n then x ^ n else - (x^n))"
  1213   by (induct n) (auto simp: one_ereal_def)
  1214 
  1215 lemma ereal_power_numeral[simp]:
  1216   "(numeral num :: ereal) ^ n = ereal (numeral num ^ n)"
  1217   by (induct n) (auto simp: one_ereal_def)
  1218 
  1219 lemma zero_le_power_ereal[simp]:
  1220   fixes a :: ereal
  1221   assumes "0 \<le> a"
  1222   shows "0 \<le> a ^ n"
  1223   using assms by (induct n) (auto simp: ereal_zero_le_0_iff)
  1224 
  1225 
  1226 subsubsection \<open>Subtraction\<close>
  1227 
  1228 lemma ereal_minus_minus_image[simp]:
  1229   fixes S :: "ereal set"
  1230   shows "uminus ` uminus ` S = S"
  1231   by (auto simp: image_iff)
  1232 
  1233 lemma ereal_uminus_lessThan[simp]:
  1234   fixes a :: ereal
  1235   shows "uminus ` {..<a} = {-a<..}"
  1236 proof -
  1237   {
  1238     fix x
  1239     assume "-a < x"
  1240     then have "- x < - (- a)"
  1241       by (simp del: ereal_uminus_uminus)
  1242     then have "- x < a"
  1243       by simp
  1244   }
  1245   then show ?thesis
  1246     by force
  1247 qed
  1248 
  1249 lemma ereal_uminus_greaterThan[simp]: "uminus ` {(a::ereal)<..} = {..<-a}"
  1250   by (metis ereal_uminus_lessThan ereal_uminus_uminus ereal_minus_minus_image)
  1251 
  1252 instantiation ereal :: minus
  1253 begin
  1254 
  1255 definition "x - y = x + -(y::ereal)"
  1256 instance ..
  1257 
  1258 end
  1259 
  1260 lemma ereal_minus[simp]:
  1261   "ereal r - ereal p = ereal (r - p)"
  1262   "-\<infinity> - ereal r = -\<infinity>"
  1263   "ereal r - \<infinity> = -\<infinity>"
  1264   "(\<infinity>::ereal) - x = \<infinity>"
  1265   "-(\<infinity>::ereal) - \<infinity> = -\<infinity>"
  1266   "x - -y = x + y"
  1267   "x - 0 = x"
  1268   "0 - x = -x"
  1269   by (simp_all add: minus_ereal_def)
  1270 
  1271 lemma ereal_x_minus_x[simp]: "x - x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)"
  1272   by (cases x) simp_all
  1273 
  1274 lemma ereal_eq_minus_iff:
  1275   fixes x y z :: ereal
  1276   shows "x = z - y \<longleftrightarrow>
  1277     (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y = z) \<and>
  1278     (y = -\<infinity> \<longrightarrow> x = \<infinity>) \<and>
  1279     (y = \<infinity> \<longrightarrow> z = \<infinity> \<longrightarrow> x = \<infinity>) \<and>
  1280     (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>)"
  1281   by (cases rule: ereal3_cases[of x y z]) auto
  1282 
  1283 lemma ereal_eq_minus:
  1284   fixes x y z :: ereal
  1285   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x = z - y \<longleftrightarrow> x + y = z"
  1286   by (auto simp: ereal_eq_minus_iff)
  1287 
  1288 lemma ereal_less_minus_iff:
  1289   fixes x y z :: ereal
  1290   shows "x < z - y \<longleftrightarrow>
  1291     (y = \<infinity> \<longrightarrow> z = \<infinity> \<and> x \<noteq> \<infinity>) \<and>
  1292     (y = -\<infinity> \<longrightarrow> x \<noteq> \<infinity>) \<and>
  1293     (\<bar>y\<bar> \<noteq> \<infinity>\<longrightarrow> x + y < z)"
  1294   by (cases rule: ereal3_cases[of x y z]) auto
  1295 
  1296 lemma ereal_less_minus:
  1297   fixes x y z :: ereal
  1298   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x < z - y \<longleftrightarrow> x + y < z"
  1299   by (auto simp: ereal_less_minus_iff)
  1300 
  1301 lemma ereal_le_minus_iff:
  1302   fixes x y z :: ereal
  1303   shows "x \<le> z - y \<longleftrightarrow> (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>) \<and> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y \<le> z)"
  1304   by (cases rule: ereal3_cases[of x y z]) auto
  1305 
  1306 lemma ereal_le_minus:
  1307   fixes x y z :: ereal
  1308   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x \<le> z - y \<longleftrightarrow> x + y \<le> z"
  1309   by (auto simp: ereal_le_minus_iff)
  1310 
  1311 lemma ereal_minus_less_iff:
  1312   fixes x y z :: ereal
  1313   shows "x - y < z \<longleftrightarrow> y \<noteq> -\<infinity> \<and> (y = \<infinity> \<longrightarrow> x \<noteq> \<infinity> \<and> z \<noteq> -\<infinity>) \<and> (y \<noteq> \<infinity> \<longrightarrow> x < z + y)"
  1314   by (cases rule: ereal3_cases[of x y z]) auto
  1315 
  1316 lemma ereal_minus_less:
  1317   fixes x y z :: ereal
  1318   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - y < z \<longleftrightarrow> x < z + y"
  1319   by (auto simp: ereal_minus_less_iff)
  1320 
  1321 lemma ereal_minus_le_iff:
  1322   fixes x y z :: ereal
  1323   shows "x - y \<le> z \<longleftrightarrow>
  1324     (y = -\<infinity> \<longrightarrow> z = \<infinity>) \<and>
  1325     (y = \<infinity> \<longrightarrow> x = \<infinity> \<longrightarrow> z = \<infinity>) \<and>
  1326     (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x \<le> z + y)"
  1327   by (cases rule: ereal3_cases[of x y z]) auto
  1328 
  1329 lemma ereal_minus_le:
  1330   fixes x y z :: ereal
  1331   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - y \<le> z \<longleftrightarrow> x \<le> z + y"
  1332   by (auto simp: ereal_minus_le_iff)
  1333 
  1334 lemma ereal_minus_eq_minus_iff:
  1335   fixes a b c :: ereal
  1336   shows "a - b = a - c \<longleftrightarrow>
  1337     b = c \<or> a = \<infinity> \<or> (a = -\<infinity> \<and> b \<noteq> -\<infinity> \<and> c \<noteq> -\<infinity>)"
  1338   by (cases rule: ereal3_cases[of a b c]) auto
  1339 
  1340 lemma ereal_add_le_add_iff:
  1341   fixes a b c :: ereal
  1342   shows "c + a \<le> c + b \<longleftrightarrow>
  1343     a \<le> b \<or> c = \<infinity> \<or> (c = -\<infinity> \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>)"
  1344   by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
  1345 
  1346 lemma ereal_add_le_add_iff2:
  1347   fixes a b c :: ereal
  1348   shows "a + c \<le> b + c \<longleftrightarrow> a \<le> b \<or> c = \<infinity> \<or> (c = -\<infinity> \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>)"
  1349 by(cases rule: ereal3_cases[of a b c])(simp_all add: field_simps)
  1350 
  1351 lemma ereal_mult_le_mult_iff:
  1352   fixes a b c :: ereal
  1353   shows "\<bar>c\<bar> \<noteq> \<infinity> \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1354   by (cases rule: ereal3_cases[of a b c]) (simp_all add: mult_le_cancel_left)
  1355 
  1356 lemma ereal_minus_mono:
  1357   fixes A B C D :: ereal assumes "A \<le> B" "D \<le> C"
  1358   shows "A - C \<le> B - D"
  1359   using assms
  1360   by (cases rule: ereal3_cases[case_product ereal_cases, of A B C D]) simp_all
  1361 
  1362 lemma real_of_ereal_minus:
  1363   fixes a b :: ereal
  1364   shows "real (a - b) = (if \<bar>a\<bar> = \<infinity> \<or> \<bar>b\<bar> = \<infinity> then 0 else real a - real b)"
  1365   by (cases rule: ereal2_cases[of a b]) auto
  1366 
  1367 lemma real_of_ereal_minus': "\<bar>x\<bar> = \<infinity> \<longleftrightarrow> \<bar>y\<bar> = \<infinity> \<Longrightarrow> real x - real y = real (x - y :: ereal)"
  1368 by(subst real_of_ereal_minus) auto
  1369 
  1370 lemma ereal_diff_positive:
  1371   fixes a b :: ereal shows "a \<le> b \<Longrightarrow> 0 \<le> b - a"
  1372   by (cases rule: ereal2_cases[of a b]) auto
  1373 
  1374 lemma ereal_between:
  1375   fixes x e :: ereal
  1376   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
  1377     and "0 < e"
  1378   shows "x - e < x"
  1379     and "x < x + e"
  1380   using assms
  1381   apply (cases x, cases e)
  1382   apply auto
  1383   using assms
  1384   apply (cases x, cases e)
  1385   apply auto
  1386   done
  1387 
  1388 lemma ereal_minus_eq_PInfty_iff:
  1389   fixes x y :: ereal
  1390   shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
  1391   by (cases x y rule: ereal2_cases) simp_all
  1392 
  1393 
  1394 subsubsection \<open>Division\<close>
  1395 
  1396 instantiation ereal :: inverse
  1397 begin
  1398 
  1399 function inverse_ereal where
  1400   "inverse (ereal r) = (if r = 0 then \<infinity> else ereal (inverse r))"
  1401 | "inverse (\<infinity>::ereal) = 0"
  1402 | "inverse (-\<infinity>::ereal) = 0"
  1403   by (auto intro: ereal_cases)
  1404 termination by (relation "{}") simp
  1405 
  1406 definition "x div y = x * inverse (y :: ereal)"
  1407 
  1408 instance ..
  1409 
  1410 end
  1411 
  1412 lemma real_of_ereal_inverse[simp]:
  1413   fixes a :: ereal
  1414   shows "real (inverse a) = 1 / real a"
  1415   by (cases a) (auto simp: inverse_eq_divide)
  1416 
  1417 lemma ereal_inverse[simp]:
  1418   "inverse (0::ereal) = \<infinity>"
  1419   "inverse (1::ereal) = 1"
  1420   by (simp_all add: one_ereal_def zero_ereal_def)
  1421 
  1422 lemma ereal_divide[simp]:
  1423   "ereal r / ereal p = (if p = 0 then ereal r * \<infinity> else ereal (r / p))"
  1424   unfolding divide_ereal_def by (auto simp: divide_real_def)
  1425 
  1426 lemma ereal_divide_same[simp]:
  1427   fixes x :: ereal
  1428   shows "x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)"
  1429   by (cases x) (simp_all add: divide_real_def divide_ereal_def one_ereal_def)
  1430 
  1431 lemma ereal_inv_inv[simp]:
  1432   fixes x :: ereal
  1433   shows "inverse (inverse x) = (if x \<noteq> -\<infinity> then x else \<infinity>)"
  1434   by (cases x) auto
  1435 
  1436 lemma ereal_inverse_minus[simp]:
  1437   fixes x :: ereal
  1438   shows "inverse (- x) = (if x = 0 then \<infinity> else -inverse x)"
  1439   by (cases x) simp_all
  1440 
  1441 lemma ereal_uminus_divide[simp]:
  1442   fixes x y :: ereal
  1443   shows "- x / y = - (x / y)"
  1444   unfolding divide_ereal_def by simp
  1445 
  1446 lemma ereal_divide_Infty[simp]:
  1447   fixes x :: ereal
  1448   shows "x / \<infinity> = 0" "x / -\<infinity> = 0"
  1449   unfolding divide_ereal_def by simp_all
  1450 
  1451 lemma ereal_divide_one[simp]: "x / 1 = (x::ereal)"
  1452   unfolding divide_ereal_def by simp
  1453 
  1454 lemma ereal_divide_ereal[simp]: "\<infinity> / ereal r = (if 0 \<le> r then \<infinity> else -\<infinity>)"
  1455   unfolding divide_ereal_def by simp
  1456 
  1457 lemma ereal_inverse_nonneg_iff: "0 \<le> inverse (x :: ereal) \<longleftrightarrow> 0 \<le> x \<or> x = -\<infinity>"
  1458   by (cases x) auto
  1459 
  1460 lemma zero_le_divide_ereal[simp]:
  1461   fixes a :: ereal
  1462   assumes "0 \<le> a"
  1463     and "0 \<le> b"
  1464   shows "0 \<le> a / b"
  1465   using assms by (cases rule: ereal2_cases[of a b]) (auto simp: zero_le_divide_iff)
  1466 
  1467 lemma ereal_le_divide_pos:
  1468   fixes x y z :: ereal
  1469   shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z"
  1470   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  1471 
  1472 lemma ereal_divide_le_pos:
  1473   fixes x y z :: ereal
  1474   shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y"
  1475   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  1476 
  1477 lemma ereal_le_divide_neg:
  1478   fixes x y z :: ereal
  1479   shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y"
  1480   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  1481 
  1482 lemma ereal_divide_le_neg:
  1483   fixes x y z :: ereal
  1484   shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z"
  1485   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  1486 
  1487 lemma ereal_inverse_antimono_strict:
  1488   fixes x y :: ereal
  1489   shows "0 \<le> x \<Longrightarrow> x < y \<Longrightarrow> inverse y < inverse x"
  1490   by (cases rule: ereal2_cases[of x y]) auto
  1491 
  1492 lemma ereal_inverse_antimono:
  1493   fixes x y :: ereal
  1494   shows "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> inverse y \<le> inverse x"
  1495   by (cases rule: ereal2_cases[of x y]) auto
  1496 
  1497 lemma inverse_inverse_Pinfty_iff[simp]:
  1498   fixes x :: ereal
  1499   shows "inverse x = \<infinity> \<longleftrightarrow> x = 0"
  1500   by (cases x) auto
  1501 
  1502 lemma ereal_inverse_eq_0:
  1503   fixes x :: ereal
  1504   shows "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity>"
  1505   by (cases x) auto
  1506 
  1507 lemma ereal_0_gt_inverse:
  1508   fixes x :: ereal
  1509   shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x"
  1510   by (cases x) auto
  1511 
  1512 lemma ereal_inverse_le_0_iff:
  1513   fixes x :: ereal
  1514   shows "inverse x \<le> 0 \<longleftrightarrow> x < 0 \<or> x = \<infinity>"
  1515   by(cases x) auto
  1516 
  1517 lemma ereal_divide_eq_0_iff: "x / y = 0 \<longleftrightarrow> x = 0 \<or> \<bar>y :: ereal\<bar> = \<infinity>"
  1518 by(cases x y rule: ereal2_cases) simp_all
  1519 
  1520 lemma ereal_mult_less_right:
  1521   fixes a b c :: ereal
  1522   assumes "b * a < c * a"
  1523     and "0 < a"
  1524     and "a < \<infinity>"
  1525   shows "b < c"
  1526   using assms
  1527   by (cases rule: ereal3_cases[of a b c])
  1528      (auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)
  1529 
  1530 lemma ereal_mult_divide: fixes a b :: ereal shows "0 < b \<Longrightarrow> b < \<infinity> \<Longrightarrow> b * (a / b) = a"
  1531   by (cases a b rule: ereal2_cases) auto
  1532 
  1533 lemma ereal_power_divide:
  1534   fixes x y :: ereal
  1535   shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n"
  1536   by (cases rule: ereal2_cases [of x y])
  1537      (auto simp: one_ereal_def zero_ereal_def power_divide zero_le_power_eq)
  1538 
  1539 lemma ereal_le_mult_one_interval:
  1540   fixes x y :: ereal
  1541   assumes y: "y \<noteq> -\<infinity>"
  1542   assumes z: "\<And>z. 0 < z \<Longrightarrow> z < 1 \<Longrightarrow> z * x \<le> y"
  1543   shows "x \<le> y"
  1544 proof (cases x)
  1545   case PInf
  1546   with z[of "1 / 2"] show "x \<le> y"
  1547     by (simp add: one_ereal_def)
  1548 next
  1549   case (real r)
  1550   note r = this
  1551   show "x \<le> y"
  1552   proof (cases y)
  1553     case (real p)
  1554     note p = this
  1555     have "r \<le> p"
  1556     proof (rule field_le_mult_one_interval)
  1557       fix z :: real
  1558       assume "0 < z" and "z < 1"
  1559       with z[of "ereal z"] show "z * r \<le> p"
  1560         using p r by (auto simp: zero_le_mult_iff one_ereal_def)
  1561     qed
  1562     then show "x \<le> y"
  1563       using p r by simp
  1564   qed (insert y, simp_all)
  1565 qed simp
  1566 
  1567 lemma ereal_divide_right_mono[simp]:
  1568   fixes x y z :: ereal
  1569   assumes "x \<le> y"
  1570     and "0 < z"
  1571   shows "x / z \<le> y / z"
  1572   using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono)
  1573 
  1574 lemma ereal_divide_left_mono[simp]:
  1575   fixes x y z :: ereal
  1576   assumes "y \<le> x"
  1577     and "0 < z"
  1578     and "0 < x * y"
  1579   shows "z / x \<le> z / y"
  1580   using assms
  1581   by (cases x y z rule: ereal3_cases)
  1582      (auto intro: divide_left_mono simp: field_simps zero_less_mult_iff mult_less_0_iff split: split_if_asm)
  1583 
  1584 lemma ereal_divide_zero_left[simp]:
  1585   fixes a :: ereal
  1586   shows "0 / a = 0"
  1587   by (cases a) (auto simp: zero_ereal_def)
  1588 
  1589 lemma ereal_times_divide_eq_left[simp]:
  1590   fixes a b c :: ereal
  1591   shows "b / c * a = b * a / c"
  1592   by (cases a b c rule: ereal3_cases) (auto simp: field_simps zero_less_mult_iff mult_less_0_iff)
  1593 
  1594 lemma ereal_times_divide_eq: "a * (b / c :: ereal) = a * b / c"
  1595   by (cases a b c rule: ereal3_cases)
  1596      (auto simp: field_simps zero_less_mult_iff)
  1597 
  1598 subsection "Complete lattice"
  1599 
  1600 instantiation ereal :: lattice
  1601 begin
  1602 
  1603 definition [simp]: "sup x y = (max x y :: ereal)"
  1604 definition [simp]: "inf x y = (min x y :: ereal)"
  1605 instance by standard simp_all
  1606 
  1607 end
  1608 
  1609 instantiation ereal :: complete_lattice
  1610 begin
  1611 
  1612 definition "bot = (-\<infinity>::ereal)"
  1613 definition "top = (\<infinity>::ereal)"
  1614 
  1615 definition "Sup S = (SOME x :: ereal. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z))"
  1616 definition "Inf S = (SOME x :: ereal. (\<forall>y\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x))"
  1617 
  1618 lemma ereal_complete_Sup:
  1619   fixes S :: "ereal set"
  1620   shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
  1621 proof (cases "\<exists>x. \<forall>a\<in>S. a \<le> ereal x")
  1622   case True
  1623   then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y"
  1624     by auto
  1625   then have "\<infinity> \<notin> S"
  1626     by force
  1627   show ?thesis
  1628   proof (cases "S \<noteq> {-\<infinity>} \<and> S \<noteq> {}")
  1629     case True
  1630     with \<open>\<infinity> \<notin> S\<close> obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
  1631       by auto
  1632     obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "\<And>z. (\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z"
  1633     proof (atomize_elim, rule complete_real)
  1634       show "\<exists>x. x \<in> ereal -` S"
  1635         using x by auto
  1636       show "\<exists>z. \<forall>x\<in>ereal -` S. x \<le> z"
  1637         by (auto dest: y intro!: exI[of _ y])
  1638     qed
  1639     show ?thesis
  1640     proof (safe intro!: exI[of _ "ereal s"])
  1641       fix y
  1642       assume "y \<in> S"
  1643       with s \<open>\<infinity> \<notin> S\<close> show "y \<le> ereal s"
  1644         by (cases y) auto
  1645     next
  1646       fix z
  1647       assume "\<forall>y\<in>S. y \<le> z"
  1648       with \<open>S \<noteq> {-\<infinity>} \<and> S \<noteq> {}\<close> show "ereal s \<le> z"
  1649         by (cases z) (auto intro!: s)
  1650     qed
  1651   next
  1652     case False
  1653     then show ?thesis
  1654       by (auto intro!: exI[of _ "-\<infinity>"])
  1655   qed
  1656 next
  1657   case False
  1658   then show ?thesis
  1659     by (fastforce intro!: exI[of _ \<infinity>] ereal_top intro: order_trans dest: less_imp_le simp: not_le)
  1660 qed
  1661 
  1662 lemma ereal_complete_uminus_eq:
  1663   fixes S :: "ereal set"
  1664   shows "(\<forall>y\<in>uminus`S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>uminus`S. y \<le> z) \<longrightarrow> x \<le> z)
  1665      \<longleftrightarrow> (\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -x)"
  1666   by simp (metis ereal_minus_le_minus ereal_uminus_uminus)
  1667 
  1668 lemma ereal_complete_Inf:
  1669   "\<exists>x. (\<forall>y\<in>S::ereal set. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x)"
  1670   using ereal_complete_Sup[of "uminus ` S"]
  1671   unfolding ereal_complete_uminus_eq
  1672   by auto
  1673 
  1674 instance
  1675 proof
  1676   show "Sup {} = (bot::ereal)"
  1677     apply (auto simp: bot_ereal_def Sup_ereal_def)
  1678     apply (rule some1_equality)
  1679     apply (metis ereal_bot ereal_less_eq(2))
  1680     apply (metis ereal_less_eq(2))
  1681     done
  1682   show "Inf {} = (top::ereal)"
  1683     apply (auto simp: top_ereal_def Inf_ereal_def)
  1684     apply (rule some1_equality)
  1685     apply (metis ereal_top ereal_less_eq(1))
  1686     apply (metis ereal_less_eq(1))
  1687     done
  1688 qed (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
  1689   simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
  1690 
  1691 end
  1692 
  1693 instance ereal :: complete_linorder ..
  1694 
  1695 instance ereal :: linear_continuum
  1696 proof
  1697   show "\<exists>a b::ereal. a \<noteq> b"
  1698     using zero_neq_one by blast
  1699 qed
  1700 
  1701 subsubsection "Topological space"
  1702 
  1703 instantiation ereal :: linear_continuum_topology
  1704 begin
  1705 
  1706 definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
  1707   open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
  1708 
  1709 instance
  1710   by standard (simp add: open_ereal_generated)
  1711 
  1712 end
  1713 
  1714 lemma continuous_on_compose': 
  1715   "continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow> f`s \<subseteq> t \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
  1716   using continuous_on_compose[of s f g] continuous_on_subset[of t g "f`s"] by auto
  1717 
  1718 lemma continuous_on_ereal[continuous_intros]:
  1719   assumes f: "continuous_on s f" shows "continuous_on s (\<lambda>x. ereal (f x))"
  1720   by (rule continuous_on_compose'[OF f continuous_onI_mono[of ereal UNIV]]) auto
  1721 
  1722 lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F"
  1723   using isCont_tendsto_compose[of x ereal f F] continuous_on_ereal[of UNIV "\<lambda>x. x"]
  1724   by (simp add: continuous_on_eq_continuous_at)
  1725 
  1726 lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. - f x::ereal) ---> - x) F"
  1727   apply (rule tendsto_compose[where g=uminus])
  1728   apply (auto intro!: order_tendstoI simp: eventually_at_topological)
  1729   apply (rule_tac x="{..< -a}" in exI)
  1730   apply (auto split: ereal.split simp: ereal_less_uminus_reorder) []
  1731   apply (rule_tac x="{- a <..}" in exI)
  1732   apply (auto split: ereal.split simp: ereal_uminus_reorder) []
  1733   done
  1734 
  1735 lemma ereal_Lim_uminus: "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x::ereal) ---> - f0) net"
  1736   using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\<lambda>x. - f x" "- f0" net]
  1737   by auto
  1738 
  1739 lemma ereal_divide_less_iff: "0 < (c::ereal) \<Longrightarrow> c < \<infinity> \<Longrightarrow> a / c < b \<longleftrightarrow> a < b * c"
  1740   by (cases a b c rule: ereal3_cases) (auto simp: field_simps)
  1741 
  1742 lemma ereal_less_divide_iff: "0 < (c::ereal) \<Longrightarrow> c < \<infinity> \<Longrightarrow> a < b / c \<longleftrightarrow> a * c < b"
  1743   by (cases a b c rule: ereal3_cases) (auto simp: field_simps)
  1744 
  1745 lemma tendsto_cmult_ereal[tendsto_intros, simp, intro]:
  1746   assumes c: "\<bar>c\<bar> \<noteq> \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. c * f x::ereal) ---> c * x) F"
  1747 proof -
  1748   { fix c :: ereal assume "0 < c" "c < \<infinity>"
  1749     then have "((\<lambda>x. c * f x::ereal) ---> c * x) F"
  1750       apply (intro tendsto_compose[OF _ f])
  1751       apply (auto intro!: order_tendstoI simp: eventually_at_topological)
  1752       apply (rule_tac x="{a/c <..}" in exI)
  1753       apply (auto split: ereal.split simp: ereal_divide_less_iff mult.commute) []
  1754       apply (rule_tac x="{..< a/c}" in exI)
  1755       apply (auto split: ereal.split simp: ereal_less_divide_iff mult.commute) []
  1756       done }
  1757   note * = this
  1758 
  1759   have "((0 < c \<and> c < \<infinity>) \<or> (-\<infinity> < c \<and> c < 0) \<or> c = 0)"
  1760     using c by (cases c) auto
  1761   then show ?thesis
  1762   proof (elim disjE conjE)
  1763     assume "- \<infinity> < c" "c < 0"
  1764     then have "0 < - c" "- c < \<infinity>"
  1765       by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0])
  1766     then have "((\<lambda>x. (- c) * f x) ---> (- c) * x) F"
  1767       by (rule *)
  1768     from tendsto_uminus_ereal[OF this] show ?thesis 
  1769       by simp
  1770   qed (auto intro!: *)
  1771 qed
  1772 
  1773 lemma tendsto_cmult_ereal_not_0[tendsto_intros, simp, intro]:
  1774   assumes "x \<noteq> 0" and f: "(f ---> x) F" shows "((\<lambda>x. c * f x::ereal) ---> c * x) F"
  1775 proof cases
  1776   assume "\<bar>c\<bar> = \<infinity>"
  1777   show ?thesis
  1778   proof (rule filterlim_cong[THEN iffD1, OF refl refl _ tendsto_const])
  1779     have "0 < x \<or> x < 0"
  1780       using \<open>x \<noteq> 0\<close> by (auto simp add: neq_iff)
  1781     then show "eventually (\<lambda>x'. c * x = c * f x') F"
  1782     proof
  1783       assume "0 < x" from order_tendstoD(1)[OF f this] show ?thesis
  1784         by eventually_elim (insert \<open>0<x\<close> \<open>\<bar>c\<bar> = \<infinity>\<close>, auto)
  1785     next
  1786       assume "x < 0" from order_tendstoD(2)[OF f this] show ?thesis
  1787         by eventually_elim (insert \<open>x<0\<close> \<open>\<bar>c\<bar> = \<infinity>\<close>, auto)
  1788     qed
  1789   qed
  1790 qed (rule tendsto_cmult_ereal[OF _ f])
  1791 
  1792 lemma tendsto_cadd_ereal[tendsto_intros, simp, intro]:
  1793   assumes c: "y \<noteq> - \<infinity>" "x \<noteq> - \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. f x + y::ereal) ---> x + y) F"
  1794   apply (intro tendsto_compose[OF _ f])
  1795   apply (auto intro!: order_tendstoI simp: eventually_at_topological)
  1796   apply (rule_tac x="{a - y <..}" in exI)
  1797   apply (auto split: ereal.split simp: ereal_minus_less_iff c) []
  1798   apply (rule_tac x="{..< a - y}" in exI)
  1799   apply (auto split: ereal.split simp: ereal_less_minus_iff c) []
  1800   done
  1801 
  1802 lemma tendsto_add_left_ereal[tendsto_intros, simp, intro]:
  1803   assumes c: "\<bar>y\<bar> \<noteq> \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. f x + y::ereal) ---> x + y) F"
  1804   apply (intro tendsto_compose[OF _ f])
  1805   apply (auto intro!: order_tendstoI simp: eventually_at_topological)
  1806   apply (rule_tac x="{a - y <..}" in exI)
  1807   apply (insert c, auto split: ereal.split simp: ereal_minus_less_iff) []
  1808   apply (rule_tac x="{..< a - y}" in exI)
  1809   apply (auto split: ereal.split simp: ereal_less_minus_iff c) []
  1810   done
  1811 
  1812 lemma continuous_at_ereal[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. ereal (f x))"
  1813   unfolding continuous_def by auto
  1814 
  1815 lemma ereal_Sup:
  1816   assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
  1817   shows "ereal (Sup A) = (SUP a:A. ereal a)"
  1818 proof (rule continuous_at_Sup_mono)
  1819   obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
  1820     using * by (force simp: bot_ereal_def)
  1821   then show "bdd_above A" "A \<noteq> {}"
  1822     by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
  1823 qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
  1824 
  1825 lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))"
  1826   using ereal_Sup[of "f`A"] by auto
  1827 
  1828 lemma ereal_Inf:
  1829   assumes *: "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
  1830   shows "ereal (Inf A) = (INF a:A. ereal a)"
  1831 proof (rule continuous_at_Inf_mono)
  1832   obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
  1833     using * by (force simp: top_ereal_def)
  1834   then show "bdd_below A" "A \<noteq> {}"
  1835     by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
  1836 qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
  1837 
  1838 lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))"
  1839   using ereal_Inf[of "f`A"] by auto
  1840 
  1841 lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
  1842   by (auto intro!: SUP_eqI
  1843            simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
  1844            intro!: complete_lattice_class.Inf_lower2)
  1845 
  1846 lemma ereal_SUP_uminus_eq:
  1847   fixes f :: "'a \<Rightarrow> ereal"
  1848   shows "(SUP x:S. uminus (f x)) = - (INF x:S. f x)"
  1849   using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
  1850 
  1851 lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
  1852   by (auto intro!: inj_onI)
  1853 
  1854 lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S"
  1855   using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
  1856 
  1857 lemma ereal_INF_uminus_eq:
  1858   fixes f :: "'a \<Rightarrow> ereal"
  1859   shows "(INF x:S. - f x) = - (SUP x:S. f x)"
  1860   using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
  1861 
  1862 lemma ereal_SUP_uminus:
  1863   fixes f :: "'a \<Rightarrow> ereal"
  1864   shows "(SUP i : R. - f i) = - (INF i : R. f i)"
  1865   using ereal_Sup_uminus_image_eq[of "f`R"]
  1866   by (simp add: image_image)
  1867 
  1868 lemma ereal_SUP_not_infty:
  1869   fixes f :: "_ \<Rightarrow> ereal"
  1870   shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>SUPREMUM A f\<bar> \<noteq> \<infinity>"
  1871   using SUP_upper2[of _ A l f] SUP_least[of A f u]
  1872   by (cases "SUPREMUM A f") auto
  1873 
  1874 lemma ereal_INF_not_infty:
  1875   fixes f :: "_ \<Rightarrow> ereal"
  1876   shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>INFIMUM A f\<bar> \<noteq> \<infinity>"
  1877   using INF_lower2[of _ A f u] INF_greatest[of A l f]
  1878   by (cases "INFIMUM A f") auto
  1879 
  1880 lemma ereal_image_uminus_shift:
  1881   fixes X Y :: "ereal set"
  1882   shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
  1883 proof
  1884   assume "uminus ` X = Y"
  1885   then have "uminus ` uminus ` X = uminus ` Y"
  1886     by (simp add: inj_image_eq_iff)
  1887   then show "X = uminus ` Y"
  1888     by (simp add: image_image)
  1889 qed (simp add: image_image)
  1890 
  1891 lemma Sup_eq_MInfty:
  1892   fixes S :: "ereal set"
  1893   shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
  1894   unfolding bot_ereal_def[symmetric] by auto
  1895 
  1896 lemma Inf_eq_PInfty:
  1897   fixes S :: "ereal set"
  1898   shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}"
  1899   using Sup_eq_MInfty[of "uminus`S"]
  1900   unfolding ereal_Sup_uminus_image_eq ereal_image_uminus_shift by simp
  1901 
  1902 lemma Inf_eq_MInfty:
  1903   fixes S :: "ereal set"
  1904   shows "-\<infinity> \<in> S \<Longrightarrow> Inf S = -\<infinity>"
  1905   unfolding bot_ereal_def[symmetric] by auto
  1906 
  1907 lemma Sup_eq_PInfty:
  1908   fixes S :: "ereal set"
  1909   shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
  1910   unfolding top_ereal_def[symmetric] by auto
  1911 
  1912 lemma not_MInfty_nonneg[simp]: "0 \<le> (x::ereal) \<Longrightarrow> x \<noteq> - \<infinity>"
  1913   by auto
  1914 
  1915 lemma Sup_ereal_close:
  1916   fixes e :: ereal
  1917   assumes "0 < e"
  1918     and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}"
  1919   shows "\<exists>x\<in>S. Sup S - e < x"
  1920   using assms by (cases e) (auto intro!: less_Sup_iff[THEN iffD1])
  1921 
  1922 lemma Inf_ereal_close:
  1923   fixes e :: ereal
  1924   assumes "\<bar>Inf X\<bar> \<noteq> \<infinity>"
  1925     and "0 < e"
  1926   shows "\<exists>x\<in>X. x < Inf X + e"
  1927 proof (rule Inf_less_iff[THEN iffD1])
  1928   show "Inf X < Inf X + e"
  1929     using assms by (cases e) auto
  1930 qed
  1931 
  1932 lemma SUP_PInfty:
  1933   "(\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i) \<Longrightarrow> (SUP i:A. f i :: ereal) = \<infinity>"
  1934   unfolding top_ereal_def[symmetric] SUP_eq_top_iff
  1935   by (metis MInfty_neq_PInfty(2) PInfty_neq_ereal(2) less_PInf_Ex_of_nat less_ereal.elims(2) less_le_trans)
  1936 
  1937 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
  1938   by (rule SUP_PInfty) auto
  1939 
  1940 lemma SUP_ereal_add_left:
  1941   assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
  1942   shows "(SUP i:I. f i + c :: ereal) = (SUP i:I. f i) + c"
  1943 proof cases
  1944   assume "(SUP i:I. f i) = - \<infinity>"
  1945   moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
  1946     unfolding Sup_eq_MInfty Sup_image_eq[symmetric] by auto
  1947   ultimately show ?thesis
  1948     by (cases c) (auto simp: \<open>I \<noteq> {}\<close>)
  1949 next
  1950   assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
  1951     unfolding Sup_image_eq[symmetric]
  1952     by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
  1953        (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
  1954 qed
  1955 
  1956 lemma SUP_ereal_add_right:
  1957   fixes c :: ereal
  1958   shows "I \<noteq> {} \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> (SUP i:I. c + f i) = c + (SUP i:I. f i)"
  1959   using SUP_ereal_add_left[of I c f] by (simp add: add.commute)
  1960 
  1961 lemma SUP_ereal_minus_right:
  1962   assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
  1963   shows "(SUP i:I. c - f i :: ereal) = c - (INF i:I. f i)"
  1964   using SUP_ereal_add_right[OF assms, of "\<lambda>i. - f i"]
  1965   by (simp add: ereal_SUP_uminus minus_ereal_def)
  1966 
  1967 lemma SUP_ereal_minus_left:
  1968   assumes "I \<noteq> {}" "c \<noteq> \<infinity>"
  1969   shows "(SUP i:I. f i - c:: ereal) = (SUP i:I. f i) - c"
  1970   using SUP_ereal_add_left[OF \<open>I \<noteq> {}\<close>, of "-c" f] by (simp add: \<open>c \<noteq> \<infinity>\<close> minus_ereal_def)
  1971 
  1972 lemma INF_ereal_minus_right:
  1973   assumes "I \<noteq> {}" and "\<bar>c\<bar> \<noteq> \<infinity>"
  1974   shows "(INF i:I. c - f i) = c - (SUP i:I. f i::ereal)"
  1975 proof -
  1976   { fix b have "(-c) + b = - (c - b)"
  1977       using \<open>\<bar>c\<bar> \<noteq> \<infinity>\<close> by (cases c b rule: ereal2_cases) auto }
  1978   note * = this
  1979   show ?thesis
  1980     using SUP_ereal_add_right[OF \<open>I \<noteq> {}\<close>, of "-c" f] \<open>\<bar>c\<bar> \<noteq> \<infinity>\<close>
  1981     by (auto simp add: * ereal_SUP_uminus_eq)
  1982 qed
  1983 
  1984 lemma SUP_ereal_le_addI:
  1985   fixes f :: "'i \<Rightarrow> ereal"
  1986   assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
  1987   shows "SUPREMUM UNIV f + y \<le> z"
  1988   unfolding SUP_ereal_add_left[OF UNIV_not_empty \<open>y \<noteq> -\<infinity>\<close>, symmetric]
  1989   by (rule SUP_least assms)+
  1990 
  1991 lemma SUP_combine:
  1992   fixes f :: "'a::semilattice_sup \<Rightarrow> 'a::semilattice_sup \<Rightarrow> 'b::complete_lattice"
  1993   assumes mono: "\<And>a b c d. a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> f a c \<le> f b d"
  1994   shows "(SUP i:UNIV. SUP j:UNIV. f i j) = (SUP i. f i i)"
  1995 proof (rule antisym)
  1996   show "(SUP i j. f i j) \<le> (SUP i. f i i)"
  1997     by (rule SUP_least SUP_upper2[where i="sup i j" for i j] UNIV_I mono sup_ge1 sup_ge2)+
  1998   show "(SUP i. f i i) \<le> (SUP i j. f i j)"
  1999     by (rule SUP_least SUP_upper2 UNIV_I mono order_refl)+
  2000 qed
  2001 
  2002 lemma SUP_ereal_add:
  2003   fixes f g :: "nat \<Rightarrow> ereal"
  2004   assumes inc: "incseq f" "incseq g"
  2005     and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
  2006   shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
  2007   apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty])
  2008   apply (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2))
  2009   apply (subst (2) add.commute)
  2010   apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty assms(3)])
  2011   apply (subst (2) add.commute)
  2012   apply (rule SUP_combine[symmetric] ereal_add_mono inc[THEN monoD] | assumption)+
  2013   done
  2014 
  2015 lemma INF_ereal_add:
  2016   fixes f :: "nat \<Rightarrow> ereal"
  2017   assumes "decseq f" "decseq g"
  2018     and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
  2019   shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
  2020 proof -
  2021   have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
  2022     using assms unfolding INF_less_iff by auto
  2023   { fix a b :: ereal assume "a \<noteq> \<infinity>" "b \<noteq> \<infinity>"
  2024     then have "- ((- a) + (- b)) = a + b"
  2025       by (cases a b rule: ereal2_cases) auto }
  2026   note * = this
  2027   have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
  2028     by (simp add: fin *)
  2029   also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
  2030     unfolding ereal_INF_uminus_eq
  2031     using assms INF_less
  2032     by (subst SUP_ereal_add) (auto simp: ereal_SUP_uminus fin *)
  2033   finally show ?thesis .
  2034 qed
  2035 
  2036 lemma SUP_ereal_add_pos:
  2037   fixes f g :: "nat \<Rightarrow> ereal"
  2038   assumes inc: "incseq f" "incseq g"
  2039     and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
  2040   shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
  2041 proof (intro SUP_ereal_add inc)
  2042   fix i
  2043   show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
  2044     using pos[of i] by auto
  2045 qed
  2046 
  2047 lemma SUP_ereal_setsum:
  2048   fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
  2049   assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
  2050     and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
  2051   shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUPREMUM UNIV (f n))"
  2052 proof (cases "finite A")
  2053   case True
  2054   then show ?thesis using assms
  2055     by induct (auto simp: incseq_setsumI2 setsum_nonneg SUP_ereal_add_pos)
  2056 next
  2057   case False
  2058   then show ?thesis by simp
  2059 qed
  2060 
  2061 lemma SUP_ereal_mult_left:
  2062   fixes f :: "'a \<Rightarrow> ereal"
  2063   assumes "I \<noteq> {}"
  2064   assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
  2065   shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
  2066 proof cases
  2067   assume "(SUP i: I. f i) = 0"
  2068   moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
  2069     by (metis SUP_upper f antisym)
  2070   ultimately show ?thesis
  2071     by simp
  2072 next
  2073   assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
  2074     unfolding SUP_def
  2075     by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
  2076        (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
  2077              intro!: ereal_mult_left_mono c)
  2078 qed
  2079 
  2080 lemma countable_approach: 
  2081   fixes x :: ereal
  2082   assumes "x \<noteq> -\<infinity>"
  2083   shows "\<exists>f. incseq f \<and> (\<forall>i::nat. f i < x) \<and> (f ----> x)"
  2084 proof (cases x)
  2085   case (real r)
  2086   moreover have "(\<lambda>n. r - inverse (real (Suc n))) ----> r - 0"
  2087     by (intro tendsto_intros LIMSEQ_inverse_real_of_nat)
  2088   ultimately show ?thesis
  2089     by (intro exI[of _ "\<lambda>n. x - inverse (Suc n)"]) (auto simp: incseq_def)
  2090 next 
  2091   case PInf with LIMSEQ_SUP[of "\<lambda>n::nat. ereal (real n)"] show ?thesis
  2092     by (intro exI[of _ "\<lambda>n. ereal (real n)"]) (auto simp: incseq_def SUP_nat_Infty)
  2093 qed (simp add: assms)
  2094 
  2095 lemma Sup_countable_SUP:
  2096   assumes "A \<noteq> {}"
  2097   shows "\<exists>f::nat \<Rightarrow> ereal. incseq f \<and> range f \<subseteq> A \<and> Sup A = (SUP i. f i)"
  2098 proof cases
  2099   assume "Sup A = -\<infinity>"
  2100   with \<open>A \<noteq> {}\<close> have "A = {-\<infinity>}"
  2101     by (auto simp: Sup_eq_MInfty)
  2102   then show ?thesis
  2103     by (auto intro!: exI[of _ "\<lambda>_. -\<infinity>"] simp: bot_ereal_def)
  2104 next
  2105   assume "Sup A \<noteq> -\<infinity>"
  2106   then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l ----> Sup A"
  2107     by (auto dest: countable_approach)
  2108 
  2109   have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
  2110   proof (rule dependent_nat_choice)
  2111     show "\<exists>x. x \<in> A \<and> l 0 \<le> x"
  2112       using l[of 0] by (auto simp: less_Sup_iff)
  2113   next
  2114     fix x n assume "x \<in> A \<and> l n \<le> x"
  2115     moreover from l[of "Suc n"] obtain y where "y \<in> A" "l (Suc n) < y"
  2116       by (auto simp: less_Sup_iff)
  2117     ultimately show "\<exists>y. (y \<in> A \<and> l (Suc n) \<le> y) \<and> x \<le> y"
  2118       by (auto intro!: exI[of _ "max x y"] split: split_max)
  2119   qed
  2120   then guess f .. note f = this
  2121   then have "range f \<subseteq> A" "incseq f"
  2122     by (auto simp: incseq_Suc_iff)
  2123   moreover
  2124   have "(SUP i. f i) = Sup A"
  2125   proof (rule tendsto_unique)
  2126     show "f ----> (SUP i. f i)"
  2127       by (rule LIMSEQ_SUP \<open>incseq f\<close>)+
  2128     show "f ----> Sup A"
  2129       using l f
  2130       by (intro tendsto_sandwich[OF _ _ l_Sup tendsto_const])
  2131          (auto simp: Sup_upper)
  2132   qed simp
  2133   ultimately show ?thesis
  2134     by auto
  2135 qed
  2136 
  2137 lemma SUP_countable_SUP:
  2138   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
  2139   using Sup_countable_SUP [of "g`A"] by auto
  2140 
  2141 subsection "Relation to @{typ enat}"
  2142 
  2143 definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
  2144 
  2145 declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
  2146 declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
  2147 
  2148 lemma ereal_of_enat_simps[simp]:
  2149   "ereal_of_enat (enat n) = ereal n"
  2150   "ereal_of_enat \<infinity> = \<infinity>"
  2151   by (simp_all add: ereal_of_enat_def)
  2152 
  2153 lemma ereal_of_enat_le_iff[simp]: "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
  2154   by (cases m n rule: enat2_cases) auto
  2155 
  2156 lemma ereal_of_enat_less_iff[simp]: "ereal_of_enat m < ereal_of_enat n \<longleftrightarrow> m < n"
  2157   by (cases m n rule: enat2_cases) auto
  2158 
  2159 lemma numeral_le_ereal_of_enat_iff[simp]: "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
  2160 by (cases n) (auto)
  2161 
  2162 lemma numeral_less_ereal_of_enat_iff[simp]: "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
  2163   by (cases n) auto
  2164 
  2165 lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
  2166   by (cases n) (auto simp: enat_0[symmetric])
  2167 
  2168 lemma ereal_of_enat_gt_zero_cancel_iff[simp]: "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
  2169   by (cases n) (auto simp: enat_0[symmetric])
  2170 
  2171 lemma ereal_of_enat_zero[simp]: "ereal_of_enat 0 = 0"
  2172   by (auto simp: enat_0[symmetric])
  2173 
  2174 lemma ereal_of_enat_inf[simp]: "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
  2175   by (cases n) auto
  2176 
  2177 lemma ereal_of_enat_add: "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
  2178   by (cases m n rule: enat2_cases) auto
  2179 
  2180 lemma ereal_of_enat_sub:
  2181   assumes "n \<le> m"
  2182   shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
  2183   using assms by (cases m n rule: enat2_cases) auto
  2184 
  2185 lemma ereal_of_enat_mult:
  2186   "ereal_of_enat (m * n) = ereal_of_enat m * ereal_of_enat n"
  2187   by (cases m n rule: enat2_cases) auto
  2188 
  2189 lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
  2190 lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
  2191 
  2192 lemma ereal_of_enat_Sup:
  2193   assumes "A \<noteq> {}" shows "ereal_of_enat (Sup A) = (SUP a : A. ereal_of_enat a)"
  2194 proof (intro antisym mono_Sup)
  2195   show "ereal_of_enat (Sup A) \<le> (SUP a : A. ereal_of_enat a)"
  2196   proof cases
  2197     assume "finite A"
  2198     with \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" "ereal_of_enat (Sup A) = ereal_of_enat a"
  2199       using Max_in[of A] by (auto simp: Sup_enat_def simp del: Max_in)
  2200     then show ?thesis
  2201       by (auto intro: SUP_upper)
  2202   next
  2203     assume "\<not> finite A"
  2204     have [simp]: "(SUP a : A. ereal_of_enat a) = top"
  2205       unfolding SUP_eq_top_iff
  2206     proof safe
  2207       fix x :: ereal assume "x < top"
  2208       then obtain n :: nat where "x < n"
  2209         using less_PInf_Ex_of_nat top_ereal_def by auto
  2210       obtain a where "a \<in> A - enat ` {.. n}"
  2211         by (metis \<open>\<not> finite A\<close> all_not_in_conv finite_Diff2 finite_atMost finite_imageI finite.emptyI)
  2212       then have "a \<in> A" "ereal n \<le> ereal_of_enat a"
  2213         by (auto simp: image_iff Ball_def)
  2214            (metis enat_iless enat_ord_simps(1) ereal_of_enat_less_iff ereal_of_enat_simps(1) less_le not_less)
  2215       with \<open>x < n\<close> show "\<exists>i\<in>A. x < ereal_of_enat i"
  2216         by (auto intro!: bexI[of _ a])
  2217     qed
  2218     show ?thesis
  2219       by simp
  2220   qed
  2221 qed (simp add: mono_def)
  2222 
  2223 lemma ereal_of_enat_SUP:
  2224   "A \<noteq> {} \<Longrightarrow> ereal_of_enat (SUP a:A. f a) = (SUP a : A. ereal_of_enat (f a))"
  2225   using ereal_of_enat_Sup[of "f`A"] by auto
  2226 
  2227 subsection "Limits on @{typ ereal}"
  2228 
  2229 lemma open_PInfty: "open A \<Longrightarrow> \<infinity> \<in> A \<Longrightarrow> (\<exists>x. {ereal x<..} \<subseteq> A)"
  2230   unfolding open_ereal_generated
  2231 proof (induct rule: generate_topology.induct)
  2232   case (Int A B)
  2233   then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
  2234     by auto
  2235   with Int show ?case
  2236     by (intro exI[of _ "max x z"]) fastforce
  2237 next
  2238   case (Basis S)
  2239   {
  2240     fix x
  2241     have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t"
  2242       by (cases x) auto
  2243   }
  2244   moreover note Basis
  2245   ultimately show ?case
  2246     by (auto split: ereal.split)
  2247 qed (fastforce simp add: vimage_Union)+
  2248 
  2249 lemma open_MInfty: "open A \<Longrightarrow> -\<infinity> \<in> A \<Longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A)"
  2250   unfolding open_ereal_generated
  2251 proof (induct rule: generate_topology.induct)
  2252   case (Int A B)
  2253   then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
  2254     by auto
  2255   with Int show ?case
  2256     by (intro exI[of _ "min x z"]) fastforce
  2257 next
  2258   case (Basis S)
  2259   {
  2260     fix x
  2261     have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x"
  2262       by (cases x) auto
  2263   }
  2264   moreover note Basis
  2265   ultimately show ?case
  2266     by (auto split: ereal.split)
  2267 qed (fastforce simp add: vimage_Union)+
  2268 
  2269 lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
  2270   by (intro open_vimage continuous_intros)
  2271 
  2272 lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
  2273   unfolding open_generated_order[where 'a=real]
  2274 proof (induct rule: generate_topology.induct)
  2275   case (Basis S)
  2276   moreover {
  2277     fix x
  2278     have "ereal ` {..< x} = { -\<infinity> <..< ereal x }"
  2279       apply auto
  2280       apply (case_tac xa)
  2281       apply auto
  2282       done
  2283   }
  2284   moreover {
  2285     fix x
  2286     have "ereal ` {x <..} = { ereal x <..< \<infinity> }"
  2287       apply auto
  2288       apply (case_tac xa)
  2289       apply auto
  2290       done
  2291   }
  2292   ultimately show ?case
  2293      by auto
  2294 qed (auto simp add: image_Union image_Int)
  2295 
  2296 
  2297 lemma eventually_finite:
  2298   fixes x :: ereal
  2299   assumes "\<bar>x\<bar> \<noteq> \<infinity>" "(f ---> x) F"
  2300   shows "eventually (\<lambda>x. \<bar>f x\<bar> \<noteq> \<infinity>) F"
  2301 proof -
  2302   have "(f ---> ereal (real x)) F"
  2303     using assms by (cases x) auto
  2304   then have "eventually (\<lambda>x. f x \<in> ereal ` UNIV) F"
  2305     by (rule topological_tendstoD) (auto intro: open_ereal)
  2306   also have "(\<lambda>x. f x \<in> ereal ` UNIV) = (\<lambda>x. \<bar>f x\<bar> \<noteq> \<infinity>)"
  2307     by auto
  2308   finally show ?thesis .
  2309 qed
  2310 
  2311 
  2312 lemma open_ereal_def:
  2313   "open A \<longleftrightarrow> open (ereal -` A) \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A)) \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
  2314   (is "open A \<longleftrightarrow> ?rhs")
  2315 proof
  2316   assume "open A"
  2317   then show ?rhs
  2318     using open_PInfty open_MInfty open_ereal_vimage by auto
  2319 next
  2320   assume "?rhs"
  2321   then obtain x y where A: "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..< ereal y} \<subseteq> A"
  2322     by auto
  2323   have *: "A = ereal ` (ereal -` A) \<union> (if \<infinity> \<in> A then {ereal x<..} else {}) \<union> (if -\<infinity> \<in> A then {..< ereal y} else {})"
  2324     using A(2,3) by auto
  2325   from open_ereal[OF A(1)] show "open A"
  2326     by (subst *) (auto simp: open_Un)
  2327 qed
  2328 
  2329 lemma open_PInfty2:
  2330   assumes "open A"
  2331     and "\<infinity> \<in> A"
  2332   obtains x where "{ereal x<..} \<subseteq> A"
  2333   using open_PInfty[OF assms] by auto
  2334 
  2335 lemma open_MInfty2:
  2336   assumes "open A"
  2337     and "-\<infinity> \<in> A"
  2338   obtains x where "{..<ereal x} \<subseteq> A"
  2339   using open_MInfty[OF assms] by auto
  2340 
  2341 lemma ereal_openE:
  2342   assumes "open A"
  2343   obtains x y where "open (ereal -` A)"
  2344     and "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A"
  2345     and "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
  2346   using assms open_ereal_def by auto
  2347 
  2348 lemmas open_ereal_lessThan = open_lessThan[where 'a=ereal]
  2349 lemmas open_ereal_greaterThan = open_greaterThan[where 'a=ereal]
  2350 lemmas ereal_open_greaterThanLessThan = open_greaterThanLessThan[where 'a=ereal]
  2351 lemmas closed_ereal_atLeast = closed_atLeast[where 'a=ereal]
  2352 lemmas closed_ereal_atMost = closed_atMost[where 'a=ereal]
  2353 lemmas closed_ereal_atLeastAtMost = closed_atLeastAtMost[where 'a=ereal]
  2354 lemmas closed_ereal_singleton = closed_singleton[where 'a=ereal]
  2355 
  2356 lemma ereal_open_cont_interval:
  2357   fixes S :: "ereal set"
  2358   assumes "open S"
  2359     and "x \<in> S"
  2360     and "\<bar>x\<bar> \<noteq> \<infinity>"
  2361   obtains e where "e > 0" and "{x-e <..< x+e} \<subseteq> S"
  2362 proof -
  2363   from \<open>open S\<close>
  2364   have "open (ereal -` S)"
  2365     by (rule ereal_openE)
  2366   then obtain e where "e > 0" and e: "\<And>y. dist y (real x) < e \<Longrightarrow> ereal y \<in> S"
  2367     using assms unfolding open_dist by force
  2368   show thesis
  2369   proof (intro that subsetI)
  2370     show "0 < ereal e"
  2371       using \<open>0 < e\<close> by auto
  2372     fix y
  2373     assume "y \<in> {x - ereal e<..<x + ereal e}"
  2374     with assms obtain t where "y = ereal t" "dist t (real x) < e"
  2375       by (cases y) (auto simp: dist_real_def)
  2376     then show "y \<in> S"
  2377       using e[of t] by auto
  2378   qed
  2379 qed
  2380 
  2381 lemma ereal_open_cont_interval2:
  2382   fixes S :: "ereal set"
  2383   assumes "open S"
  2384     and "x \<in> S"
  2385     and x: "\<bar>x\<bar> \<noteq> \<infinity>"
  2386   obtains a b where "a < x" and "x < b" and "{a <..< b} \<subseteq> S"
  2387 proof -
  2388   obtain e where "0 < e" "{x - e<..<x + e} \<subseteq> S"
  2389     using assms by (rule ereal_open_cont_interval)
  2390   with that[of "x - e" "x + e"] ereal_between[OF x, of e]
  2391   show thesis
  2392     by auto
  2393 qed
  2394 
  2395 subsubsection \<open>Convergent sequences\<close>
  2396 
  2397 lemma lim_real_of_ereal[simp]:
  2398   assumes lim: "(f ---> ereal x) net"
  2399   shows "((\<lambda>x. real (f x)) ---> x) net"
  2400 proof (intro topological_tendstoI)
  2401   fix S
  2402   assume "open S" and "x \<in> S"
  2403   then have S: "open S" "ereal x \<in> ereal ` S"
  2404     by (simp_all add: inj_image_mem_iff)
  2405   have "\<forall>x. f x \<in> ereal ` S \<longrightarrow> real (f x) \<in> S"
  2406     by auto
  2407   from this lim[THEN topological_tendstoD, OF open_ereal, OF S]
  2408   show "eventually (\<lambda>x. real (f x) \<in> S) net"
  2409     by (rule eventually_mono)
  2410 qed
  2411 
  2412 lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
  2413   by (auto dest!: lim_real_of_ereal)
  2414 
  2415 lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
  2416 proof -
  2417   {
  2418     fix l :: ereal
  2419     assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
  2420     from this[THEN spec, of "real l"] have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
  2421       by (cases l) (auto elim: eventually_elim1)
  2422   }
  2423   then show ?thesis
  2424     by (auto simp: order_tendsto_iff)
  2425 qed
  2426 
  2427 lemma tendsto_PInfty_eq_at_top:
  2428   "((\<lambda>z. ereal (f z)) ---> \<infinity>) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
  2429   unfolding tendsto_PInfty filterlim_at_top_dense by simp
  2430 
  2431 lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
  2432   unfolding tendsto_def
  2433 proof safe
  2434   fix S :: "ereal set"
  2435   assume "open S" "-\<infinity> \<in> S"
  2436   from open_MInfty[OF this] obtain B where "{..<ereal B} \<subseteq> S" ..
  2437   moreover
  2438   assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
  2439   then have "eventually (\<lambda>z. f z \<in> {..< B}) F"
  2440     by auto
  2441   ultimately show "eventually (\<lambda>z. f z \<in> S) F"
  2442     by (auto elim!: eventually_elim1)
  2443 next
  2444   fix x
  2445   assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
  2446   from this[rule_format, of "{..< ereal x}"] show "eventually (\<lambda>y. f y < ereal x) F"
  2447     by auto
  2448 qed
  2449 
  2450 lemma Lim_PInfty: "f ----> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
  2451   unfolding tendsto_PInfty eventually_sequentially
  2452 proof safe
  2453   fix r
  2454   assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
  2455   then obtain N where "\<forall>n\<ge>N. ereal (r + 1) \<le> f n"
  2456     by blast
  2457   moreover have "ereal r < ereal (r + 1)"
  2458     by auto
  2459   ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
  2460     by (blast intro: less_le_trans)
  2461 qed (blast intro: less_imp_le)
  2462 
  2463 lemma Lim_MInfty: "f ----> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
  2464   unfolding tendsto_MInfty eventually_sequentially
  2465 proof safe
  2466   fix r
  2467   assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
  2468   then obtain N where "\<forall>n\<ge>N. f n \<le> ereal (r - 1)"
  2469     by blast
  2470   moreover have "ereal (r - 1) < ereal r"
  2471     by auto
  2472   ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
  2473     by (blast intro: le_less_trans)
  2474 qed (blast intro: less_imp_le)
  2475 
  2476 lemma Lim_bounded_PInfty: "f ----> l \<Longrightarrow> (\<And>n. f n \<le> ereal B) \<Longrightarrow> l \<noteq> \<infinity>"
  2477   using LIMSEQ_le_const2[of f l "ereal B"] by auto
  2478 
  2479 lemma Lim_bounded_MInfty: "f ----> l \<Longrightarrow> (\<And>n. ereal B \<le> f n) \<Longrightarrow> l \<noteq> -\<infinity>"
  2480   using LIMSEQ_le_const[of f l "ereal B"] by auto
  2481 
  2482 lemma tendsto_explicit:
  2483   "f ----> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
  2484   unfolding tendsto_def eventually_sequentially by auto
  2485 
  2486 lemma Lim_bounded_PInfty2: "f ----> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
  2487   using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
  2488 
  2489 lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
  2490   by (intro LIMSEQ_le_const2) auto
  2491 
  2492 lemma Lim_bounded2_ereal:
  2493   assumes lim:"f ----> (l :: 'a::linorder_topology)"
  2494     and ge: "\<forall>n\<ge>N. f n \<ge> C"
  2495   shows "l \<ge> C"
  2496   using ge
  2497   by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
  2498      (auto simp: eventually_sequentially)
  2499 
  2500 lemma real_of_ereal_mult[simp]:
  2501   fixes a b :: ereal
  2502   shows "real (a * b) = real a * real b"
  2503   by (cases rule: ereal2_cases[of a b]) auto
  2504 
  2505 lemma real_of_ereal_eq_0:
  2506   fixes x :: ereal
  2507   shows "real x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity> \<or> x = 0"
  2508   by (cases x) auto
  2509 
  2510 lemma tendsto_ereal_realD:
  2511   fixes f :: "'a \<Rightarrow> ereal"
  2512   assumes "x \<noteq> 0"
  2513     and tendsto: "((\<lambda>x. ereal (real (f x))) ---> x) net"
  2514   shows "(f ---> x) net"
  2515 proof (intro topological_tendstoI)
  2516   fix S
  2517   assume S: "open S" "x \<in> S"
  2518   with \<open>x \<noteq> 0\<close> have "open (S - {0})" "x \<in> S - {0}"
  2519     by auto
  2520   from tendsto[THEN topological_tendstoD, OF this]
  2521   show "eventually (\<lambda>x. f x \<in> S) net"
  2522     by (rule eventually_rev_mp) (auto simp: ereal_real)
  2523 qed
  2524 
  2525 lemma tendsto_ereal_realI:
  2526   fixes f :: "'a \<Rightarrow> ereal"
  2527   assumes x: "\<bar>x\<bar> \<noteq> \<infinity>" and tendsto: "(f ---> x) net"
  2528   shows "((\<lambda>x. ereal (real (f x))) ---> x) net"
  2529 proof (intro topological_tendstoI)
  2530   fix S
  2531   assume "open S" and "x \<in> S"
  2532   with x have "open (S - {\<infinity>, -\<infinity>})" "x \<in> S - {\<infinity>, -\<infinity>}"
  2533     by auto
  2534   from tendsto[THEN topological_tendstoD, OF this]
  2535   show "eventually (\<lambda>x. ereal (real (f x)) \<in> S) net"
  2536     by (elim eventually_elim1) (auto simp: ereal_real)
  2537 qed
  2538 
  2539 lemma ereal_mult_cancel_left:
  2540   fixes a b c :: ereal
  2541   shows "a * b = a * c \<longleftrightarrow> (\<bar>a\<bar> = \<infinity> \<and> 0 < b * c) \<or> a = 0 \<or> b = c"
  2542   by (cases rule: ereal3_cases[of a b c]) (simp_all add: zero_less_mult_iff)
  2543 
  2544 lemma tendsto_add_ereal:
  2545   fixes x y :: ereal
  2546   assumes x: "\<bar>x\<bar> \<noteq> \<infinity>" and y: "\<bar>y\<bar> \<noteq> \<infinity>"
  2547   assumes f: "(f ---> x) F" and g: "(g ---> y) F"
  2548   shows "((\<lambda>x. f x + g x) ---> x + y) F"
  2549 proof -
  2550   from x obtain r where x': "x = ereal r" by (cases x) auto
  2551   with f have "((\<lambda>i. real (f i)) ---> r) F" by simp
  2552   moreover
  2553   from y obtain p where y': "y = ereal p" by (cases y) auto
  2554   with g have "((\<lambda>i. real (g i)) ---> p) F" by simp
  2555   ultimately have "((\<lambda>i. real (f i) + real (g i)) ---> r + p) F"
  2556     by (rule tendsto_add)
  2557   moreover
  2558   from eventually_finite[OF x f] eventually_finite[OF y g]
  2559   have "eventually (\<lambda>x. f x + g x = ereal (real (f x) + real (g x))) F"
  2560     by eventually_elim auto
  2561   ultimately show ?thesis
  2562     by (simp add: x' y' cong: filterlim_cong)
  2563 qed
  2564 
  2565 lemma ereal_inj_affinity:
  2566   fixes m t :: ereal
  2567   assumes "\<bar>m\<bar> \<noteq> \<infinity>"
  2568     and "m \<noteq> 0"
  2569     and "\<bar>t\<bar> \<noteq> \<infinity>"
  2570   shows "inj_on (\<lambda>x. m * x + t) A"
  2571   using assms
  2572   by (cases rule: ereal2_cases[of m t])
  2573      (auto intro!: inj_onI simp: ereal_add_cancel_right ereal_mult_cancel_left)
  2574 
  2575 lemma ereal_PInfty_eq_plus[simp]:
  2576   fixes a b :: ereal
  2577   shows "\<infinity> = a + b \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
  2578   by (cases rule: ereal2_cases[of a b]) auto
  2579 
  2580 lemma ereal_MInfty_eq_plus[simp]:
  2581   fixes a b :: ereal
  2582   shows "-\<infinity> = a + b \<longleftrightarrow> (a = -\<infinity> \<and> b \<noteq> \<infinity>) \<or> (b = -\<infinity> \<and> a \<noteq> \<infinity>)"
  2583   by (cases rule: ereal2_cases[of a b]) auto
  2584 
  2585 lemma ereal_less_divide_pos:
  2586   fixes x y :: ereal
  2587   shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y < z / x \<longleftrightarrow> x * y < z"
  2588   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  2589 
  2590 lemma ereal_divide_less_pos:
  2591   fixes x y z :: ereal
  2592   shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y / x < z \<longleftrightarrow> y < x * z"
  2593   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  2594 
  2595 lemma ereal_divide_eq:
  2596   fixes a b c :: ereal
  2597   shows "b \<noteq> 0 \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity> \<Longrightarrow> a / b = c \<longleftrightarrow> a = b * c"
  2598   by (cases rule: ereal3_cases[of a b c])
  2599      (simp_all add: field_simps)
  2600 
  2601 lemma ereal_inverse_not_MInfty[simp]: "inverse (a::ereal) \<noteq> -\<infinity>"
  2602   by (cases a) auto
  2603 
  2604 lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
  2605   by (cases x) auto
  2606 
  2607 lemma ereal_real':
  2608   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
  2609   shows "ereal (real x) = x"
  2610   using assms by auto
  2611 
  2612 lemma real_ereal_id: "real \<circ> ereal = id"
  2613 proof -
  2614   {
  2615     fix x
  2616     have "(real o ereal) x = id x"
  2617       by auto
  2618   }
  2619   then show ?thesis
  2620     using ext by blast
  2621 qed
  2622 
  2623 lemma open_image_ereal: "open(UNIV-{ \<infinity> , (-\<infinity> :: ereal)})"
  2624   by (metis range_ereal open_ereal open_UNIV)
  2625 
  2626 lemma ereal_le_distrib:
  2627   fixes a b c :: ereal
  2628   shows "c * (a + b) \<le> c * a + c * b"
  2629   by (cases rule: ereal3_cases[of a b c])
  2630      (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
  2631 
  2632 lemma ereal_pos_distrib:
  2633   fixes a b c :: ereal
  2634   assumes "0 \<le> c"
  2635     and "c \<noteq> \<infinity>"
  2636   shows "c * (a + b) = c * a + c * b"
  2637   using assms
  2638   by (cases rule: ereal3_cases[of a b c])
  2639     (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
  2640 
  2641 lemma ereal_max_mono: "(a::ereal) \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> max a c \<le> max b d"
  2642   by (metis sup_ereal_def sup_mono)
  2643 
  2644 lemma ereal_max_least: "(a::ereal) \<le> x \<Longrightarrow> c \<le> x \<Longrightarrow> max a c \<le> x"
  2645   by (metis sup_ereal_def sup_least)
  2646 
  2647 lemma ereal_LimI_finite:
  2648   fixes x :: ereal
  2649   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
  2650     and "\<And>r. 0 < r \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
  2651   shows "u ----> x"
  2652 proof (rule topological_tendstoI, unfold eventually_sequentially)
  2653   obtain rx where rx: "x = ereal rx"
  2654     using assms by (cases x) auto
  2655   fix S
  2656   assume "open S" and "x \<in> S"
  2657   then have "open (ereal -` S)"
  2658     unfolding open_ereal_def by auto
  2659   with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
  2660     unfolding open_real_def rx by auto
  2661   then obtain n where
  2662     upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
  2663     lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
  2664     using assms(2)[of "ereal r"] by auto
  2665   show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
  2666   proof (safe intro!: exI[of _ n])
  2667     fix N
  2668     assume "n \<le> N"
  2669     from upper[OF this] lower[OF this] assms \<open>0 < r\<close>
  2670     have "u N \<notin> {\<infinity>,(-\<infinity>)}"
  2671       by auto
  2672     then obtain ra where ra_def: "(u N) = ereal ra"
  2673       by (cases "u N") auto
  2674     then have "rx < ra + r" and "ra < rx + r"
  2675       using rx assms \<open>0 < r\<close> lower[OF \<open>n \<le> N\<close>] upper[OF \<open>n \<le> N\<close>]
  2676       by auto
  2677     then have "dist (real (u N)) rx < r"
  2678       using rx ra_def
  2679       by (auto simp: dist_real_def abs_diff_less_iff field_simps)
  2680     from dist[OF this] show "u N \<in> S"
  2681       using \<open>u N  \<notin> {\<infinity>, -\<infinity>}\<close>
  2682       by (auto simp: ereal_real split: split_if_asm)
  2683   qed
  2684 qed
  2685 
  2686 lemma tendsto_obtains_N:
  2687   assumes "f ----> f0"
  2688   assumes "open S"
  2689     and "f0 \<in> S"
  2690   obtains N where "\<forall>n\<ge>N. f n \<in> S"
  2691   using assms using tendsto_def
  2692   using tendsto_explicit[of f f0] assms by auto
  2693 
  2694 lemma ereal_LimI_finite_iff:
  2695   fixes x :: ereal
  2696   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
  2697   shows "u ----> x \<longleftrightarrow> (\<forall>r. 0 < r \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r))"
  2698   (is "?lhs \<longleftrightarrow> ?rhs")
  2699 proof
  2700   assume lim: "u ----> x"
  2701   {
  2702     fix r :: ereal
  2703     assume "r > 0"
  2704     then obtain N where "\<forall>n\<ge>N. u n \<in> {x - r <..< x + r}"
  2705        apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
  2706        using lim ereal_between[of x r] assms \<open>r > 0\<close>
  2707        apply auto
  2708        done
  2709     then have "\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
  2710       using ereal_minus_less[of r x]
  2711       by (cases r) auto
  2712   }
  2713   then show ?rhs
  2714     by auto
  2715 next
  2716   assume ?rhs
  2717   then show "u ----> x"
  2718     using ereal_LimI_finite[of x] assms by auto
  2719 qed
  2720 
  2721 lemma ereal_Limsup_uminus:
  2722   fixes f :: "'a \<Rightarrow> ereal"
  2723   shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
  2724   unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus_eq ..
  2725 
  2726 lemma liminf_bounded_iff:
  2727   fixes x :: "nat \<Rightarrow> ereal"
  2728   shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)"
  2729   (is "?lhs \<longleftrightarrow> ?rhs")
  2730   unfolding le_Liminf_iff eventually_sequentially ..
  2731 
  2732 lemma Liminf_add_le:
  2733   fixes f g :: "_ \<Rightarrow> ereal"
  2734   assumes F: "F \<noteq> bot"
  2735   assumes ev: "eventually (\<lambda>x. 0 \<le> f x) F" "eventually (\<lambda>x. 0 \<le> g x) F"
  2736   shows "Liminf F f + Liminf F g \<le> Liminf F (\<lambda>x. f x + g x)"
  2737   unfolding Liminf_def
  2738 proof (subst SUP_ereal_add_left[symmetric])
  2739   let ?F = "{P. eventually P F}"
  2740   let ?INF = "\<lambda>P g. INFIMUM (Collect P) g"
  2741   show "?F \<noteq> {}"
  2742     by (auto intro: eventually_True)
  2743   show "(SUP P:?F. ?INF P g) \<noteq> - \<infinity>"
  2744     unfolding bot_ereal_def[symmetric] SUP_bot_conv INF_eq_bot_iff
  2745     by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
  2746   have "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. (SUP P':?F. ?INF P f + ?INF P' g))"
  2747   proof (safe intro!: SUP_mono bexI[of _ "\<lambda>x. P x \<and> 0 \<le> f x" for P])
  2748     fix P let ?P' = "\<lambda>x. P x \<and> 0 \<le> f x"
  2749     assume "eventually P F"
  2750     with ev show "eventually ?P' F"
  2751       by eventually_elim auto
  2752     have "?INF P f + (SUP P:?F. ?INF P g) \<le> ?INF ?P' f + (SUP P:?F. ?INF P g)"
  2753       by (intro ereal_add_mono INF_mono) auto
  2754     also have "\<dots> = (SUP P':?F. ?INF ?P' f + ?INF P' g)"
  2755     proof (rule SUP_ereal_add_right[symmetric])
  2756       show "INFIMUM {x. P x \<and> 0 \<le> f x} f \<noteq> - \<infinity>"
  2757         unfolding bot_ereal_def[symmetric] INF_eq_bot_iff
  2758         by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
  2759     qed fact
  2760     finally show "?INF P f + (SUP P:?F. ?INF P g) \<le> (SUP P':?F. ?INF ?P' f + ?INF P' g)" .
  2761   qed
  2762   also have "\<dots> \<le> (SUP P:?F. INF x:Collect P. f x + g x)"
  2763   proof (safe intro!: SUP_least)
  2764     fix P Q assume *: "eventually P F" "eventually Q F"
  2765     show "?INF P f + ?INF Q g \<le> (SUP P:?F. INF x:Collect P. f x + g x)"
  2766     proof (rule SUP_upper2)
  2767       show "(\<lambda>x. P x \<and> Q x) \<in> ?F"
  2768         using * by (auto simp: eventually_conj)
  2769       show "?INF P f + ?INF Q g \<le> (INF x:{x. P x \<and> Q x}. f x + g x)"
  2770         by (intro INF_greatest ereal_add_mono) (auto intro: INF_lower)
  2771     qed
  2772   qed
  2773   finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. INF x:Collect P. f x + g x)" .
  2774 qed
  2775 
  2776 lemma Sup_ereal_mult_right':
  2777   assumes nonempty: "Y \<noteq> {}"
  2778   and x: "x \<ge> 0"
  2779   shows "(SUP i:Y. f i) * ereal x = (SUP i:Y. f i * ereal x)" (is "?lhs = ?rhs")
  2780 proof(cases "x = 0")
  2781   case True thus ?thesis by(auto simp add: nonempty zero_ereal_def[symmetric])
  2782 next
  2783   case False
  2784   show ?thesis
  2785   proof(rule antisym)
  2786     show "?rhs \<le> ?lhs"
  2787       by(rule SUP_least)(simp add: ereal_mult_right_mono SUP_upper x)
  2788   next
  2789     have "?lhs / ereal x = (SUP i:Y. f i) * (ereal x / ereal x)" by(simp only: ereal_times_divide_eq)
  2790     also have "\<dots> = (SUP i:Y. f i)" using False by simp
  2791     also have "\<dots> \<le> ?rhs / x"
  2792     proof(rule SUP_least)
  2793       fix i
  2794       assume "i \<in> Y"
  2795       have "f i = f i * (ereal x / ereal x)" using False by simp
  2796       also have "\<dots> = f i * x / x" by(simp only: ereal_times_divide_eq)
  2797       also from \<open>i \<in> Y\<close> have "f i * x \<le> ?rhs" by(rule SUP_upper)
  2798       hence "f i * x / x \<le> ?rhs / x" using x False by simp
  2799       finally show "f i \<le> ?rhs / x" .
  2800     qed
  2801     finally have "(?lhs / x) * x \<le> (?rhs / x) * x"
  2802       by(rule ereal_mult_right_mono)(simp add: x)
  2803     also have "\<dots> = ?rhs" using False ereal_divide_eq mult.commute by force
  2804     also have "(?lhs / x) * x = ?lhs" using False ereal_divide_eq mult.commute by force
  2805     finally show "?lhs \<le> ?rhs" .
  2806   qed
  2807 qed
  2808 
  2809 lemma sup_continuous_add[order_continuous_intros]:
  2810   fixes f g :: "'a::complete_lattice \<Rightarrow> ereal"
  2811   assumes nn: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x" and cont: "sup_continuous f" "sup_continuous g"
  2812   shows "sup_continuous (\<lambda>x. f x + g x)"
  2813   unfolding sup_continuous_def
  2814 proof safe
  2815   fix M :: "nat \<Rightarrow> 'a" assume "incseq M"
  2816   then show "f (SUP i. M i) + g (SUP i. M i) = (SUP i. f (M i) + g (M i))"
  2817     using SUP_ereal_add_pos[of "\<lambda>i. f (M i)" "\<lambda>i. g (M i)"] nn
  2818       cont[THEN sup_continuous_mono] cont[THEN sup_continuousD]
  2819     by (auto simp: mono_def)
  2820 qed
  2821 
  2822 lemma sup_continuous_mult_right[order_continuous_intros]:
  2823   "0 \<le> c \<Longrightarrow> c < \<infinity> \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x * c :: ereal)"
  2824   by (cases c) (auto simp: sup_continuous_def fun_eq_iff Sup_ereal_mult_right')
  2825 
  2826 lemma sup_continuous_mult_left[order_continuous_intros]:
  2827   "0 \<le> c \<Longrightarrow> c < \<infinity> \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. c * f x :: ereal)"
  2828   using sup_continuous_mult_right[of c f] by (simp add: mult_ac)
  2829 
  2830 lemma sup_continuous_ereal_of_enat[order_continuous_intros]:
  2831   assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. ereal_of_enat (f x))"
  2832   by (rule sup_continuous_compose[OF _ f])
  2833      (auto simp: sup_continuous_def ereal_of_enat_SUP)
  2834 
  2835 subsubsection \<open>Sums\<close>
  2836 
  2837 lemma sums_ereal_positive:
  2838   fixes f :: "nat \<Rightarrow> ereal"
  2839   assumes "\<And>i. 0 \<le> f i"
  2840   shows "f sums (SUP n. \<Sum>i<n. f i)"
  2841 proof -
  2842   have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
  2843     using ereal_add_mono[OF _ assms]
  2844     by (auto intro!: incseq_SucI)
  2845   from LIMSEQ_SUP[OF this]
  2846   show ?thesis unfolding sums_def
  2847     by (simp add: atLeast0LessThan)
  2848 qed
  2849 
  2850 lemma summable_ereal_pos:
  2851   fixes f :: "nat \<Rightarrow> ereal"
  2852   assumes "\<And>i. 0 \<le> f i"
  2853   shows "summable f"
  2854   using sums_ereal_positive[of f, OF assms]
  2855   unfolding summable_def
  2856   by auto
  2857 
  2858 lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
  2859   unfolding sums_def by simp
  2860 
  2861 lemma suminf_ereal_eq_SUP:
  2862   fixes f :: "nat \<Rightarrow> ereal"
  2863   assumes "\<And>i. 0 \<le> f i"
  2864   shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
  2865   using sums_ereal_positive[of f, OF assms, THEN sums_unique]
  2866   by simp
  2867 
  2868 lemma suminf_bound:
  2869   fixes f :: "nat \<Rightarrow> ereal"
  2870   assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
  2871     and pos: "\<And>n. 0 \<le> f n"
  2872   shows "suminf f \<le> x"
  2873 proof (rule Lim_bounded_ereal)
  2874   have "summable f" using pos[THEN summable_ereal_pos] .
  2875   then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
  2876     by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
  2877   show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
  2878     using assms by auto
  2879 qed
  2880 
  2881 lemma suminf_bound_add:
  2882   fixes f :: "nat \<Rightarrow> ereal"
  2883   assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
  2884     and pos: "\<And>n. 0 \<le> f n"
  2885     and "y \<noteq> -\<infinity>"
  2886   shows "suminf f + y \<le> x"
  2887 proof (cases y)
  2888   case (real r)
  2889   then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
  2890     using assms by (simp add: ereal_le_minus)
  2891   then have "(\<Sum> n. f n) \<le> x - y"
  2892     using pos by (rule suminf_bound)
  2893   then show "(\<Sum> n. f n) + y \<le> x"
  2894     using assms real by (simp add: ereal_le_minus)
  2895 qed (insert assms, auto)
  2896 
  2897 lemma suminf_upper:
  2898   fixes f :: "nat \<Rightarrow> ereal"
  2899   assumes "\<And>n. 0 \<le> f n"
  2900   shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
  2901   unfolding suminf_ereal_eq_SUP [OF assms]
  2902   by (auto intro: complete_lattice_class.SUP_upper)
  2903 
  2904 lemma suminf_0_le:
  2905   fixes f :: "nat \<Rightarrow> ereal"
  2906   assumes "\<And>n. 0 \<le> f n"
  2907   shows "0 \<le> (\<Sum>n. f n)"
  2908   using suminf_upper[of f 0, OF assms]
  2909   by simp
  2910 
  2911 lemma suminf_le_pos:
  2912   fixes f g :: "nat \<Rightarrow> ereal"
  2913   assumes "\<And>N. f N \<le> g N"
  2914     and "\<And>N. 0 \<le> f N"
  2915   shows "suminf f \<le> suminf g"
  2916 proof (safe intro!: suminf_bound)
  2917   fix n
  2918   {
  2919     fix N
  2920     have "0 \<le> g N"
  2921       using assms(2,1)[of N] by auto
  2922   }
  2923   have "setsum f {..<n} \<le> setsum g {..<n}"
  2924     using assms by (auto intro: setsum_mono)
  2925   also have "\<dots> \<le> suminf g"
  2926     using \<open>\<And>N. 0 \<le> g N\<close>
  2927     by (rule suminf_upper)
  2928   finally show "setsum f {..<n} \<le> suminf g" .
  2929 qed (rule assms(2))
  2930 
  2931 lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1"
  2932   using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
  2933   by (simp add: one_ereal_def)
  2934 
  2935 lemma suminf_add_ereal:
  2936   fixes f g :: "nat \<Rightarrow> ereal"
  2937   assumes "\<And>i. 0 \<le> f i"
  2938     and "\<And>i. 0 \<le> g i"
  2939   shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
  2940   apply (subst (1 2 3) suminf_ereal_eq_SUP)
  2941   unfolding setsum.distrib
  2942   apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
  2943   done
  2944 
  2945 lemma suminf_cmult_ereal:
  2946   fixes f g :: "nat \<Rightarrow> ereal"
  2947   assumes "\<And>i. 0 \<le> f i"
  2948     and "0 \<le> a"
  2949   shows "(\<Sum>i. a * f i) = a * suminf f"
  2950   by (auto simp: setsum_ereal_right_distrib[symmetric] assms
  2951        ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
  2952        intro!: SUP_ereal_mult_left)
  2953 
  2954 lemma suminf_PInfty:
  2955   fixes f :: "nat \<Rightarrow> ereal"
  2956   assumes "\<And>i. 0 \<le> f i"
  2957     and "suminf f \<noteq> \<infinity>"
  2958   shows "f i \<noteq> \<infinity>"
  2959 proof -
  2960   from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
  2961   have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>"
  2962     by auto
  2963   then show ?thesis
  2964     unfolding setsum_Pinfty by simp
  2965 qed
  2966 
  2967 lemma suminf_PInfty_fun:
  2968   assumes "\<And>i. 0 \<le> f i"
  2969     and "suminf f \<noteq> \<infinity>"
  2970   shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
  2971 proof -
  2972   have "\<forall>i. \<exists>r. f i = ereal r"
  2973   proof
  2974     fix i
  2975     show "\<exists>r. f i = ereal r"
  2976       using suminf_PInfty[OF assms] assms(1)[of i]
  2977       by (cases "f i") auto
  2978   qed
  2979   from choice[OF this] show ?thesis
  2980     by auto
  2981 qed
  2982 
  2983 lemma summable_ereal:
  2984   assumes "\<And>i. 0 \<le> f i"
  2985     and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
  2986   shows "summable f"
  2987 proof -
  2988   have "0 \<le> (\<Sum>i. ereal (f i))"
  2989     using assms by (intro suminf_0_le) auto
  2990   with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
  2991     by (cases "\<Sum>i. ereal (f i)") auto
  2992   from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
  2993   have "summable (\<lambda>x. ereal (f x))"
  2994     using assms by auto
  2995   from summable_sums[OF this]
  2996   have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))"
  2997     by auto
  2998   then show "summable f"
  2999     unfolding r sums_ereal summable_def ..
  3000 qed
  3001 
  3002 lemma suminf_ereal:
  3003   assumes "\<And>i. 0 \<le> f i"
  3004     and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
  3005   shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
  3006 proof (rule sums_unique[symmetric])
  3007   from summable_ereal[OF assms]
  3008   show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
  3009     unfolding sums_ereal
  3010     using assms
  3011     by (intro summable_sums summable_ereal)
  3012 qed
  3013 
  3014 lemma suminf_ereal_minus:
  3015   fixes f g :: "nat \<Rightarrow> ereal"
  3016   assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i"
  3017     and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
  3018   shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
  3019 proof -
  3020   {
  3021     fix i
  3022     have "0 \<le> f i"
  3023       using ord[of i] by auto
  3024   }
  3025   moreover
  3026   from suminf_PInfty_fun[OF \<open>\<And>i. 0 \<le> f i\<close> fin(1)] obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))" ..
  3027   from suminf_PInfty_fun[OF \<open>\<And>i. 0 \<le> g i\<close> fin(2)] obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))" ..
  3028   {
  3029     fix i
  3030     have "0 \<le> f i - g i"
  3031       using ord[of i] by (auto simp: ereal_le_minus_iff)
  3032   }
  3033   moreover
  3034   have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
  3035     using assms by (auto intro!: suminf_le_pos simp: field_simps)
  3036   then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>"
  3037     using fin by auto
  3038   ultimately show ?thesis
  3039     using assms \<open>\<And>i. 0 \<le> f i\<close>
  3040     apply simp
  3041     apply (subst (1 2 3) suminf_ereal)
  3042     apply (auto intro!: suminf_diff[symmetric] summable_ereal)
  3043     done
  3044 qed
  3045 
  3046 lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
  3047 proof -
  3048   have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)"
  3049     by (rule suminf_upper) auto
  3050   then show ?thesis
  3051     by simp
  3052 qed
  3053 
  3054 lemma summable_real_of_ereal:
  3055   fixes f :: "nat \<Rightarrow> ereal"
  3056   assumes f: "\<And>i. 0 \<le> f i"
  3057     and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
  3058   shows "summable (\<lambda>i. real (f i))"
  3059 proof (rule summable_def[THEN iffD2])
  3060   have "0 \<le> (\<Sum>i. f i)"
  3061     using assms by (auto intro: suminf_0_le)
  3062   with fin obtain r where r: "ereal r = (\<Sum>i. f i)"
  3063     by (cases "(\<Sum>i. f i)") auto
  3064   {
  3065     fix i
  3066     have "f i \<noteq> \<infinity>"
  3067       using f by (intro suminf_PInfty[OF _ fin]) auto
  3068     then have "\<bar>f i\<bar> \<noteq> \<infinity>"
  3069       using f[of i] by auto
  3070   }
  3071   note fin = this
  3072   have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
  3073     using f
  3074     by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
  3075   also have "\<dots> = ereal r"
  3076     using fin r by (auto simp: ereal_real)
  3077   finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
  3078     by (auto simp: sums_ereal)
  3079 qed
  3080 
  3081 lemma suminf_SUP_eq:
  3082   fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
  3083   assumes "\<And>i. incseq (\<lambda>n. f n i)"
  3084     and "\<And>n i. 0 \<le> f n i"
  3085   shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
  3086 proof -
  3087   {
  3088     fix n :: nat
  3089     have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
  3090       using assms
  3091       by (auto intro!: SUP_ereal_setsum [symmetric])
  3092   }
  3093   note * = this
  3094   show ?thesis
  3095     using assms
  3096     apply (subst (1 2) suminf_ereal_eq_SUP)
  3097     unfolding *
  3098     apply (auto intro!: SUP_upper2)
  3099     apply (subst SUP_commute)
  3100     apply rule
  3101     done
  3102 qed
  3103 
  3104 lemma suminf_setsum_ereal:
  3105   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
  3106   assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
  3107   shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
  3108 proof (cases "finite A")
  3109   case True
  3110   then show ?thesis
  3111     using nonneg
  3112     by induct (simp_all add: suminf_add_ereal setsum_nonneg)
  3113 next
  3114   case False
  3115   then show ?thesis by simp
  3116 qed
  3117 
  3118 lemma suminf_ereal_eq_0:
  3119   fixes f :: "nat \<Rightarrow> ereal"
  3120   assumes nneg: "\<And>i. 0 \<le> f i"
  3121   shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
  3122 proof
  3123   assume "(\<Sum>i. f i) = 0"
  3124   {
  3125     fix i
  3126     assume "f i \<noteq> 0"
  3127     with nneg have "0 < f i"
  3128       by (auto simp: less_le)
  3129     also have "f i = (\<Sum>j. if j = i then f i else 0)"
  3130       by (subst suminf_finite[where N="{i}"]) auto
  3131     also have "\<dots> \<le> (\<Sum>i. f i)"
  3132       using nneg
  3133       by (auto intro!: suminf_le_pos)
  3134     finally have False
  3135       using \<open>(\<Sum>i. f i) = 0\<close> by auto
  3136   }
  3137   then show "\<forall>i. f i = 0"
  3138     by auto
  3139 qed simp
  3140 
  3141 lemma suminf_ereal_offset_le:
  3142   fixes f :: "nat \<Rightarrow> ereal"
  3143   assumes f: "\<And>i. 0 \<le> f i"
  3144   shows "(\<Sum>i. f (i + k)) \<le> suminf f"
  3145 proof -
  3146   have "(\<lambda>n. \<Sum>i<n. f (i + k)) ----> (\<Sum>i. f (i + k))"
  3147     using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
  3148   moreover have "(\<lambda>n. \<Sum>i<n. f i) ----> (\<Sum>i. f i)"
  3149     using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
  3150   then have "(\<lambda>n. \<Sum>i<n + k. f i) ----> (\<Sum>i. f i)"
  3151     by (rule LIMSEQ_ignore_initial_segment)
  3152   ultimately show ?thesis
  3153   proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
  3154     fix n assume "k \<le> n"
  3155     have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
  3156       by simp
  3157     also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
  3158       by (subst setsum.reindex) auto
  3159     also have "\<dots> \<le> setsum f {..<n + k}"
  3160       by (intro setsum_mono3) (auto simp: f)
  3161     finally show "(\<Sum>i<n. f (i + k)) \<le> setsum f {..<n + k}" .
  3162   qed
  3163 qed
  3164 
  3165 lemma sums_suminf_ereal: "f sums x \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal x"
  3166   by (metis sums_ereal sums_unique)
  3167 
  3168 lemma suminf_ereal': "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal (\<Sum>i. f i)"
  3169   by (metis sums_ereal sums_unique summable_def)
  3170 
  3171 lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
  3172   by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
  3173 
  3174 lemma suminf_ereal_finite_neg:
  3175   assumes "summable f"
  3176   shows "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>"
  3177 proof-
  3178   from assms obtain x where "f sums x" by blast
  3179   hence "(\<lambda>x. ereal (f x)) sums ereal x" by (simp add: sums_ereal)
  3180   from sums_unique[OF this] have "(\<Sum>x. ereal (f x)) = ereal x" ..
  3181   thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
  3182 qed
  3183 
  3184 
  3185 lemma SUP_ereal_add_directed:
  3186   fixes f g :: "'a \<Rightarrow> ereal"
  3187   assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
  3188   assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<le> f k + g k"
  3189   shows "(SUP i:I. f i + g i) = (SUP i:I. f i) + (SUP i:I. g i)"
  3190 proof cases
  3191   assume "I = {}" then show ?thesis
  3192     by (simp add: bot_ereal_def)
  3193 next
  3194   assume "I \<noteq> {}"
  3195   show ?thesis
  3196   proof (rule antisym)
  3197     show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)"
  3198       by (rule SUP_least; intro ereal_add_mono SUP_upper)
  3199   next
  3200     have "bot < (SUP i:I. g i)"
  3201       using \<open>I \<noteq> {}\<close> nonneg(2) by (auto simp: bot_ereal_def less_SUP_iff)
  3202     then have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))"
  3203       by (intro SUP_ereal_add_left[symmetric] \<open>I \<noteq> {}\<close>) auto
  3204     also have "\<dots> = (SUP i:I. (SUP j:I. f i + g j))"
  3205       using nonneg(1) by (intro SUP_cong refl SUP_ereal_add_right[symmetric] \<open>I \<noteq> {}\<close>) auto
  3206     also have "\<dots> \<le> (SUP i:I. f i + g i)"
  3207       using directed by (intro SUP_least) (blast intro: SUP_upper2)
  3208     finally show "(SUP i:I. f i) + (SUP i:I. g i) \<le> (SUP i:I. f i + g i)" .
  3209   qed
  3210 qed
  3211 
  3212 lemma SUP_ereal_setsum_directed:
  3213   fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
  3214   assumes "I \<noteq> {}"
  3215   assumes directed: "\<And>N i j. N \<subseteq> A \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f n i \<le> f n k \<and> f n j \<le> f n k"
  3216   assumes nonneg: "\<And>n i. i \<in> I \<Longrightarrow> n \<in> A \<Longrightarrow> 0 \<le> f n i"
  3217   shows "(SUP i:I. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUP i:I. f n i)"
  3218 proof -
  3219   have "N \<subseteq> A \<Longrightarrow> (SUP i:I. \<Sum>n\<in>N. f n i) = (\<Sum>n\<in>N. SUP i:I. f n i)" for N
  3220   proof (induction N rule: infinite_finite_induct)
  3221     case (insert n N)
  3222     moreover have "(SUP i:I. f n i + (\<Sum>l\<in>N. f l i)) = (SUP i:I. f n i) + (SUP i:I. \<Sum>l\<in>N. f l i)"
  3223     proof (rule SUP_ereal_add_directed)
  3224       fix i assume "i \<in> I" then show "0 \<le> f n i" "0 \<le> (\<Sum>l\<in>N. f l i)"
  3225         using insert by (auto intro!: setsum_nonneg nonneg)
  3226     next
  3227       fix i j assume "i \<in> I" "j \<in> I"
  3228       from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k ..
  3229       then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)" 
  3230         by (intro bexI[of _ k]) (auto intro!: ereal_add_mono setsum_mono)
  3231     qed
  3232     ultimately show ?case
  3233       by simp
  3234   qed (simp_all add: SUP_constant \<open>I \<noteq> {}\<close>)
  3235   from this[of A] show ?thesis by simp
  3236 qed
  3237 
  3238 lemma suminf_SUP_eq_directed:
  3239   fixes f :: "_ \<Rightarrow> nat \<Rightarrow> ereal"
  3240   assumes "I \<noteq> {}"
  3241   assumes directed: "\<And>N i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> finite N \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f i n \<le> f k n \<and> f j n \<le> f k n"
  3242   assumes nonneg: "\<And>n i. 0 \<le> f n i"
  3243   shows "(\<Sum>i. SUP n:I. f n i) = (SUP n:I. \<Sum>i. f n i)"
  3244 proof (subst (1 2) suminf_ereal_eq_SUP)
  3245   show "\<And>n i. 0 \<le> f n i" "\<And>i. 0 \<le> (SUP n:I. f n i)"
  3246     using \<open>I \<noteq> {}\<close> nonneg by (auto intro: SUP_upper2)
  3247   show "(SUP n. \<Sum>i<n. SUP n:I. f n i) = (SUP n:I. SUP j. \<Sum>i<j. f n i)"
  3248     apply (subst SUP_commute)
  3249     apply (subst SUP_ereal_setsum_directed)
  3250     apply (auto intro!: assms simp: finite_subset)
  3251     done
  3252 qed
  3253 
  3254 subsection \<open>More Limits\<close>
  3255 
  3256 lemma convergent_limsup_cl:
  3257   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
  3258   shows "convergent X \<Longrightarrow> limsup X = lim X"
  3259   by (auto simp: convergent_def limI lim_imp_Limsup)
  3260 
  3261 lemma lim_increasing_cl:
  3262   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
  3263   obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
  3264 proof
  3265   show "f ----> (SUP n. f n)"
  3266     using assms
  3267     by (intro increasing_tendsto)
  3268        (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
  3269 qed
  3270 
  3271 lemma lim_decreasing_cl:
  3272   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
  3273   obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
  3274 proof
  3275   show "f ----> (INF n. f n)"
  3276     using assms
  3277     by (intro decreasing_tendsto)
  3278        (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
  3279 qed
  3280 
  3281 lemma compact_complete_linorder:
  3282   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
  3283   shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
  3284 proof -
  3285   obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
  3286     using seq_monosub[of X]
  3287     unfolding comp_def
  3288     by auto
  3289   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)"
  3290     by (auto simp add: monoseq_def)
  3291   then obtain l where "(X \<circ> r) ----> l"
  3292      using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
  3293      by auto
  3294   then show ?thesis
  3295     using \<open>subseq r\<close> by auto
  3296 qed
  3297 
  3298 lemma ereal_dense3:
  3299   fixes x y :: ereal
  3300   shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
  3301 proof (cases x y rule: ereal2_cases, simp_all)
  3302   fix r q :: real
  3303   assume "r < q"
  3304   from Rats_dense_in_real[OF this] show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
  3305     by (fastforce simp: Rats_def)
  3306 next
  3307   fix r :: real
  3308   show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
  3309     using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
  3310     by (auto simp: Rats_def)
  3311 qed
  3312 
  3313 lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
  3314   using continuous_on_eq_continuous_within[of A ereal]
  3315   by (auto intro: continuous_on_ereal continuous_on_id)
  3316 
  3317 lemma ereal_open_uminus:
  3318   fixes S :: "ereal set"
  3319   assumes "open S"
  3320   shows "open (uminus ` S)"
  3321   using \<open>open S\<close>[unfolded open_generated_order]
  3322 proof induct
  3323   have "range uminus = (UNIV :: ereal set)"
  3324     by (auto simp: image_iff ereal_uminus_eq_reorder)
  3325   then show "open (range uminus :: ereal set)"
  3326     by simp
  3327 qed (auto simp add: image_Union image_Int)
  3328 
  3329 lemma ereal_uminus_complement:
  3330   fixes S :: "ereal set"
  3331   shows "uminus ` (- S) = - uminus ` S"
  3332   by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
  3333 
  3334 lemma ereal_closed_uminus:
  3335   fixes S :: "ereal set"
  3336   assumes "closed S"
  3337   shows "closed (uminus ` S)"
  3338   using assms
  3339   unfolding closed_def ereal_uminus_complement[symmetric]
  3340   by (rule ereal_open_uminus)
  3341 
  3342 lemma ereal_open_affinity_pos:
  3343   fixes S :: "ereal set"
  3344   assumes "open S"
  3345     and m: "m \<noteq> \<infinity>" "0 < m"
  3346     and t: "\<bar>t\<bar> \<noteq> \<infinity>"
  3347   shows "open ((\<lambda>x. m * x + t) ` S)"
  3348 proof -
  3349   have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
  3350     using m t
  3351     apply (intro open_vimage \<open>open S\<close>)
  3352     apply (intro continuous_at_imp_continuous_on ballI tendsto_cmult_ereal continuous_at[THEN iffD2]
  3353                  tendsto_ident_at tendsto_add_left_ereal)
  3354     apply auto
  3355     done
  3356   also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
  3357     using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
  3358                        simp del: uminus_ereal.simps)
  3359   also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
  3360     using m t
  3361     by (simp add: set_eq_iff image_iff)
  3362        (metis abs_ereal_less0 abs_ereal_uminus ereal_divide_eq ereal_eq_minus ereal_minus(7,8)
  3363               ereal_minus_less_minus ereal_mult_eq_PInfty ereal_uminus_uminus ereal_zero_mult)
  3364   finally show ?thesis .
  3365 qed
  3366 
  3367 lemma ereal_open_affinity:
  3368   fixes S :: "ereal set"
  3369   assumes "open S"
  3370     and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0"
  3371     and t: "\<bar>t\<bar> \<noteq> \<infinity>"
  3372   shows "open ((\<lambda>x. m * x + t) ` S)"
  3373 proof cases
  3374   assume "0 < m"
  3375   then show ?thesis
  3376     using ereal_open_affinity_pos[OF \<open>open S\<close> _ _ t, of m] m
  3377     by auto
  3378 next
  3379   assume "\<not> 0 < m" then
  3380   have "0 < -m"
  3381     using \<open>m \<noteq> 0\<close>
  3382     by (cases m) auto
  3383   then have m: "-m \<noteq> \<infinity>" "0 < -m"
  3384     using \<open>\<bar>m\<bar> \<noteq> \<infinity>\<close>
  3385     by (auto simp: ereal_uminus_eq_reorder)
  3386   from ereal_open_affinity_pos[OF ereal_open_uminus[OF \<open>open S\<close>] m t] show ?thesis
  3387     unfolding image_image by simp
  3388 qed
  3389 
  3390 lemma open_uminus_iff:
  3391   fixes S :: "ereal set"
  3392   shows "open (uminus ` S) \<longleftrightarrow> open S"
  3393   using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"]
  3394   by auto
  3395 
  3396 lemma ereal_Liminf_uminus:
  3397   fixes f :: "'a \<Rightarrow> ereal"
  3398   shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
  3399   using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
  3400 
  3401 lemma Liminf_PInfty:
  3402   fixes f :: "'a \<Rightarrow> ereal"
  3403   assumes "\<not> trivial_limit net"
  3404   shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
  3405   unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
  3406   using Liminf_le_Limsup[OF assms, of f]
  3407   by auto
  3408 
  3409 lemma Limsup_MInfty:
  3410   fixes f :: "'a \<Rightarrow> ereal"
  3411   assumes "\<not> trivial_limit net"
  3412   shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
  3413   unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
  3414   using Liminf_le_Limsup[OF assms, of f]
  3415   by auto
  3416 
  3417 lemma convergent_ereal:
  3418   fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
  3419   shows "convergent X \<longleftrightarrow> limsup X = liminf X"
  3420   using tendsto_iff_Liminf_eq_Limsup[of sequentially]
  3421   by (auto simp: convergent_def)
  3422 
  3423 lemma limsup_le_liminf_real:
  3424   fixes X :: "nat \<Rightarrow> real" and L :: real
  3425   assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X"
  3426   shows "X ----> L"
  3427 proof -
  3428   from 1 2 have "limsup X \<le> liminf X" by auto
  3429   hence 3: "limsup X = liminf X"  
  3430     apply (subst eq_iff, rule conjI)
  3431     by (rule Liminf_le_Limsup, auto)
  3432   hence 4: "convergent (\<lambda>n. ereal (X n))"
  3433     by (subst convergent_ereal)
  3434   hence "limsup X = lim (\<lambda>n. ereal(X n))"
  3435     by (rule convergent_limsup_cl)
  3436   also from 1 2 3 have "limsup X = L" by auto
  3437   finally have "lim (\<lambda>n. ereal(X n)) = L" ..
  3438   hence "(\<lambda>n. ereal (X n)) ----> L"
  3439     apply (elim subst)
  3440     by (subst convergent_LIMSEQ_iff [symmetric], rule 4) 
  3441   thus ?thesis by simp
  3442 qed
  3443 
  3444 lemma liminf_PInfty:
  3445   fixes X :: "nat \<Rightarrow> ereal"
  3446   shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
  3447   by (metis Liminf_PInfty trivial_limit_sequentially)
  3448 
  3449 lemma limsup_MInfty:
  3450   fixes X :: "nat \<Rightarrow> ereal"
  3451   shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
  3452   by (metis Limsup_MInfty trivial_limit_sequentially)
  3453 
  3454 lemma ereal_lim_mono:
  3455   fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
  3456   assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
  3457     and "X ----> x"
  3458     and "Y ----> y"
  3459   shows "x \<le> y"
  3460   using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
  3461 
  3462 lemma incseq_le_ereal:
  3463   fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
  3464   assumes inc: "incseq X"
  3465     and lim: "X ----> L"
  3466   shows "X N \<le> L"
  3467   using inc
  3468   by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
  3469 
  3470 lemma decseq_ge_ereal:
  3471   assumes dec: "decseq X"
  3472     and lim: "X ----> (L::'a::linorder_topology)"
  3473   shows "X N \<ge> L"
  3474   using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
  3475 
  3476 lemma bounded_abs:
  3477   fixes a :: real
  3478   assumes "a \<le> x"
  3479     and "x \<le> b"
  3480   shows "abs x \<le> max (abs a) (abs b)"
  3481   by (metis abs_less_iff assms leI le_max_iff_disj
  3482     less_eq_real_def less_le_not_le less_minus_iff minus_minus)
  3483 
  3484 lemma ereal_Sup_lim:
  3485   fixes a :: "'a::{complete_linorder,linorder_topology}"
  3486   assumes "\<And>n. b n \<in> s"
  3487     and "b ----> a"
  3488   shows "a \<le> Sup s"
  3489   by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
  3490 
  3491 lemma ereal_Inf_lim:
  3492   fixes a :: "'a::{complete_linorder,linorder_topology}"
  3493   assumes "\<And>n. b n \<in> s"
  3494     and "b ----> a"
  3495   shows "Inf s \<le> a"
  3496   by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
  3497 
  3498 lemma SUP_Lim_ereal:
  3499   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
  3500   assumes inc: "incseq X"
  3501     and l: "X ----> l"
  3502   shows "(SUP n. X n) = l"
  3503   using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
  3504   by simp
  3505 
  3506 lemma INF_Lim_ereal:
  3507   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
  3508   assumes dec: "decseq X"
  3509     and l: "X ----> l"
  3510   shows "(INF n. X n) = l"
  3511   using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
  3512   by simp
  3513 
  3514 lemma SUP_eq_LIMSEQ:
  3515   assumes "mono f"
  3516   shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
  3517 proof
  3518   have inc: "incseq (\<lambda>i. ereal (f i))"
  3519     using \<open>mono f\<close> unfolding mono_def incseq_def by auto
  3520   {
  3521     assume "f ----> x"
  3522     then have "(\<lambda>i. ereal (f i)) ----> ereal x"
  3523       by auto
  3524     from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
  3525   next
  3526     assume "(SUP n. ereal (f n)) = ereal x"
  3527     with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
  3528   }
  3529 qed
  3530 
  3531 lemma liminf_ereal_cminus:
  3532   fixes f :: "nat \<Rightarrow> ereal"
  3533   assumes "c \<noteq> -\<infinity>"
  3534   shows "liminf (\<lambda>x. c - f x) = c - limsup f"
  3535 proof (cases c)
  3536   case PInf
  3537   then show ?thesis
  3538     by (simp add: Liminf_const)
  3539 next
  3540   case (real r)
  3541   then show ?thesis
  3542     unfolding liminf_SUP_INF limsup_INF_SUP
  3543     apply (subst INF_ereal_minus_right)
  3544     apply auto
  3545     apply (subst SUP_ereal_minus_right)
  3546     apply auto
  3547     done
  3548 qed (insert \<open>c \<noteq> -\<infinity>\<close>, simp)
  3549 
  3550 
  3551 subsubsection \<open>Continuity\<close>
  3552 
  3553 lemma continuous_at_of_ereal:
  3554   "\<bar>x0 :: ereal\<bar> \<noteq> \<infinity> \<Longrightarrow> continuous (at x0) real"
  3555   unfolding continuous_at
  3556   by (rule lim_real_of_ereal) (simp add: ereal_real)
  3557 
  3558 lemma nhds_ereal: "nhds (ereal r) = filtermap ereal (nhds r)"
  3559   by (simp add: filtermap_nhds_open_map open_ereal continuous_at_of_ereal)
  3560 
  3561 lemma at_ereal: "at (ereal r) = filtermap ereal (at r)"
  3562   by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
  3563 
  3564 lemma at_left_ereal: "at_left (ereal r) = filtermap ereal (at_left r)"
  3565   by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
  3566 
  3567 lemma at_right_ereal: "at_right (ereal r) = filtermap ereal (at_right r)"
  3568   by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
  3569 
  3570 lemma
  3571   shows at_left_PInf: "at_left \<infinity> = filtermap ereal at_top"
  3572     and at_right_MInf: "at_right (-\<infinity>) = filtermap ereal at_bot"
  3573   unfolding filter_eq_iff eventually_filtermap eventually_at_top_dense eventually_at_bot_dense
  3574     eventually_at_left[OF ereal_less(5)] eventually_at_right[OF ereal_less(6)]
  3575   by (auto simp add: ereal_all_split ereal_ex_split)
  3576 
  3577 lemma ereal_tendsto_simps1:
  3578   "((f \<circ> real) ---> y) (at_left (ereal x)) \<longleftrightarrow> (f ---> y) (at_left x)"
  3579   "((f \<circ> real) ---> y) (at_right (ereal x)) \<longleftrightarrow> (f ---> y) (at_right x)"
  3580   "((f \<circ> real) ---> y) (at_left (\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_top"
  3581   "((f \<circ> real) ---> y) (at_right (-\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_bot"
  3582   unfolding tendsto_compose_filtermap at_left_ereal at_right_ereal at_left_PInf at_right_MInf
  3583   by (auto simp: filtermap_filtermap filtermap_ident)
  3584 
  3585 lemma ereal_tendsto_simps2:
  3586   "((ereal \<circ> f) ---> ereal a) F \<longleftrightarrow> (f ---> a) F"
  3587   "((ereal \<circ> f) ---> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)"
  3588   "((ereal \<circ> f) ---> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)"
  3589   unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
  3590   using lim_ereal by (simp_all add: comp_def)
  3591 
  3592 lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
  3593 
  3594 lemma continuous_at_iff_ereal:
  3595   fixes f :: "'a::t2_space \<Rightarrow> real"
  3596   shows "continuous (at x0 within s) f \<longleftrightarrow> continuous (at x0 within s) (ereal \<circ> f)"
  3597   unfolding continuous_within comp_def lim_ereal ..
  3598 
  3599 lemma continuous_on_iff_ereal:
  3600   fixes f :: "'a::t2_space => real"
  3601   assumes "open A"
  3602   shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)"
  3603   unfolding continuous_on_def comp_def lim_ereal ..
  3604 
  3605 lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real"
  3606   using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
  3607   by auto
  3608 
  3609 lemma continuous_on_iff_real:
  3610   fixes f :: "'a::t2_space \<Rightarrow> ereal"
  3611   assumes *: "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
  3612   shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
  3613 proof -
  3614   have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
  3615     using assms by force
  3616   then have *: "continuous_on (f ` A) real"
  3617     using continuous_on_real by (simp add: continuous_on_subset)
  3618   have **: "continuous_on ((real \<circ> f) ` A) ereal"
  3619     by (intro continuous_on_ereal continuous_on_id)
  3620   {
  3621     assume "continuous_on A f"
  3622     then have "continuous_on A (real \<circ> f)"
  3623       apply (subst continuous_on_compose)
  3624       using *
  3625       apply auto
  3626       done
  3627   }
  3628   moreover
  3629   {
  3630     assume "continuous_on A (real \<circ> f)"
  3631     then have "continuous_on A (ereal \<circ> (real \<circ> f))"
  3632       apply (subst continuous_on_compose)
  3633       using **
  3634       apply auto
  3635       done
  3636     then have "continuous_on A f"
  3637       apply (subst continuous_on_cong[of _ A _ "ereal \<circ> (real \<circ> f)"])
  3638       using assms ereal_real
  3639       apply auto
  3640       done
  3641   }
  3642   ultimately show ?thesis
  3643     by auto
  3644 qed
  3645 
  3646 
  3647 subsubsection \<open>Tests for code generator\<close>
  3648 
  3649 (* A small list of simple arithmetic expressions *)
  3650 
  3651 value "- \<infinity> :: ereal"
  3652 value "\<bar>-\<infinity>\<bar> :: ereal"
  3653 value "4 + 5 / 4 - ereal 2 :: ereal"
  3654 value "ereal 3 < \<infinity>"
  3655 value "real (\<infinity>::ereal) = 0"
  3656 
  3657 end