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