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