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