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