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