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