src/HOL/Library/Extended_Nonnegative_Real.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 62378 85ed00c1fe7c
child 62623 dbc62f86a1a9
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (*  Title:      HOL/Library/Extended_Nonnegative_Real.thy
     2     Author:     Johannes Hölzl
     3 *)
     4 
     5 subsection \<open>The type of non-negative extended real numbers\<close>
     6 
     7 theory Extended_Nonnegative_Real
     8   imports Extended_Real
     9 begin
    10 
    11 context linordered_nonzero_semiring
    12 begin
    13 
    14 lemma of_nat_nonneg [simp]: "0 \<le> of_nat n"
    15   by (induct n) simp_all
    16 
    17 lemma of_nat_mono[simp]: "i \<le> j \<Longrightarrow> of_nat i \<le> of_nat j"
    18   by (auto simp add: le_iff_add intro!: add_increasing2)
    19 
    20 end
    21 
    22 lemma of_nat_less[simp]:
    23   "i < j \<Longrightarrow> of_nat i < (of_nat j::'a::{linordered_nonzero_semiring, semiring_char_0})"
    24   by (auto simp: less_le)
    25 
    26 lemma of_nat_le_iff[simp]:
    27   "of_nat i \<le> (of_nat j::'a::{linordered_nonzero_semiring, semiring_char_0}) \<longleftrightarrow> i \<le> j"
    28 proof (safe intro!: of_nat_mono)
    29   assume "of_nat i \<le> (of_nat j::'a)" then show "i \<le> j"
    30   proof (intro leI notI)
    31     assume "j < i" from less_le_trans[OF of_nat_less[OF this] \<open>of_nat i \<le> of_nat j\<close>] show False
    32       by blast
    33   qed
    34 qed
    35 
    36 lemma (in complete_lattice) SUP_sup_const1:
    37   "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup c (f i)) = sup c (SUP i:I. f i)"
    38   using SUP_sup_distrib[of "\<lambda>_. c" I f] by simp
    39 
    40 lemma (in complete_lattice) SUP_sup_const2:
    41   "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup (f i) c) = sup (SUP i:I. f i) c"
    42   using SUP_sup_distrib[of f I "\<lambda>_. c"] by simp
    43 
    44 lemma one_less_of_natD:
    45   "(1::'a::linordered_semidom) < of_nat n \<Longrightarrow> 1 < n"
    46   using zero_le_one[where 'a='a]
    47   apply (cases n)
    48   apply simp
    49   subgoal for n'
    50     apply (cases n')
    51     apply simp
    52     apply simp
    53     done
    54   done
    55 
    56 lemma setsum_le_suminf:
    57   fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    58   shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> setsum f I \<le> suminf f"
    59   by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
    60 
    61 typedef ennreal = "{x :: ereal. 0 \<le> x}"
    62   morphisms enn2ereal e2ennreal'
    63   by auto
    64 
    65 definition "e2ennreal x = e2ennreal' (max 0 x)"
    66 
    67 lemma type_definition_ennreal': "type_definition enn2ereal e2ennreal {x. 0 \<le> x}"
    68   using type_definition_ennreal
    69   by (auto simp: type_definition_def e2ennreal_def max_absorb2)
    70 
    71 setup_lifting type_definition_ennreal'
    72 
    73 lift_definition ennreal :: "real \<Rightarrow> ennreal" is "sup 0 \<circ> ereal"
    74   by simp
    75 
    76 declare [[coercion ennreal]]
    77 declare [[coercion e2ennreal]]
    78 
    79 instantiation ennreal :: complete_linorder
    80 begin
    81 
    82 lift_definition top_ennreal :: ennreal is top by (rule top_greatest)
    83 lift_definition bot_ennreal :: ennreal is 0 by (rule order_refl)
    84 lift_definition sup_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is sup by (rule le_supI1)
    85 lift_definition inf_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is inf by (rule le_infI)
    86 
    87 lift_definition Inf_ennreal :: "ennreal set \<Rightarrow> ennreal" is "Inf"
    88   by (rule Inf_greatest)
    89 
    90 lift_definition Sup_ennreal :: "ennreal set \<Rightarrow> ennreal" is "sup 0 \<circ> Sup"
    91   by auto
    92 
    93 lift_definition less_eq_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op \<le>" .
    94 lift_definition less_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op <" .
    95 
    96 instance
    97   by standard
    98      (transfer ; auto simp: Inf_lower Inf_greatest Sup_upper Sup_least le_max_iff_disj max.absorb1)+
    99 
   100 end
   101 
   102 lemma ennreal_cases:
   103   fixes x :: ennreal
   104   obtains (real) r :: real where "0 \<le> r" "x = ennreal r" | (top) "x = top"
   105   apply transfer
   106   subgoal for x thesis
   107     by (cases x) (auto simp: max.absorb2 top_ereal_def)
   108   done
   109 
   110 instantiation ennreal :: infinity
   111 begin
   112 
   113 definition infinity_ennreal :: ennreal
   114 where
   115   [simp]: "\<infinity> = (top::ennreal)"
   116 
   117 instance ..
   118 
   119 end
   120 
   121 instantiation ennreal :: "{semiring_1_no_zero_divisors, comm_semiring_1}"
   122 begin
   123 
   124 lift_definition one_ennreal :: ennreal is 1 by simp
   125 lift_definition zero_ennreal :: ennreal is 0 by simp
   126 lift_definition plus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "op +" by simp
   127 lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "op *" by simp
   128 
   129 instance
   130   by standard (transfer; auto simp: field_simps ereal_right_distrib)+
   131 
   132 end
   133 
   134 instantiation ennreal :: minus
   135 begin
   136 
   137 lift_definition minus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "\<lambda>a b. max 0 (a - b)"
   138   by simp
   139 
   140 instance ..
   141 
   142 end
   143 
   144 instance ennreal :: numeral ..
   145 
   146 instantiation ennreal :: inverse
   147 begin
   148 
   149 lift_definition inverse_ennreal :: "ennreal \<Rightarrow> ennreal" is inverse
   150   by (rule inverse_ereal_ge0I)
   151 
   152 definition divide_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal"
   153   where "x div y = x * inverse (y :: ennreal)"
   154 
   155 instance ..
   156 
   157 end
   158 
   159 lemma ennreal_zero_less_one: "0 < (1::ennreal)"
   160   by transfer auto
   161 
   162 instance ennreal :: dioid
   163 proof (standard; transfer)
   164   fix a b :: ereal assume "0 \<le> a" "0 \<le> b" then show "(a \<le> b) = (\<exists>c\<in>Collect (op \<le> 0). b = a + c)"
   165     unfolding ereal_ex_split Bex_def
   166     by (cases a b rule: ereal2_cases) (auto intro!: exI[of _ "real_of_ereal (b - a)"])
   167 qed
   168 
   169 instance ennreal :: ordered_comm_semiring
   170   by standard
   171      (transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+
   172 
   173 instance ennreal :: linordered_nonzero_semiring
   174   proof qed (transfer; simp)
   175 
   176 declare [[coercion "of_nat :: nat \<Rightarrow> ennreal"]]
   177 
   178 lemma e2ennreal_neg: "x \<le> 0 \<Longrightarrow> e2ennreal x = 0"
   179   unfolding zero_ennreal_def e2ennreal_def by (simp add: max_absorb1)
   180 
   181 lemma e2ennreal_mono: "x \<le> y \<Longrightarrow> e2ennreal x \<le> e2ennreal y"
   182   by (cases "0 \<le> x" "0 \<le> y" rule: bool.exhaust[case_product bool.exhaust])
   183      (auto simp: e2ennreal_neg less_eq_ennreal.abs_eq eq_onp_def)
   184 
   185 subsection \<open>Cancellation simprocs\<close>
   186 
   187 lemma ennreal_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::ennreal) \<or> b = c"
   188   unfolding infinity_ennreal_def by transfer (simp add: top_ereal_def ereal_add_cancel_left)
   189 
   190 lemma ennreal_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::ennreal) \<or> b \<le> c"
   191   unfolding infinity_ennreal_def by transfer (simp add: ereal_add_le_add_iff top_ereal_def disj_commute)
   192 
   193 lemma ereal_add_left_cancel_less:
   194   fixes a b c :: ereal
   195   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a + b < a + c \<longleftrightarrow> a \<noteq> \<infinity> \<and> b < c"
   196   by (cases a b c rule: ereal3_cases) auto
   197 
   198 lemma ennreal_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::ennreal) \<and> b < c"
   199   unfolding infinity_ennreal_def
   200   by transfer (simp add: top_ereal_def ereal_add_left_cancel_less)
   201 
   202 ML \<open>
   203 structure Cancel_Ennreal_Common =
   204 struct
   205   (* copied from src/HOL/Tools/nat_numeral_simprocs.ML *)
   206   fun find_first_t _    _ []         = raise TERM("find_first_t", [])
   207     | find_first_t past u (t::terms) =
   208           if u aconv t then (rev past @ terms)
   209           else find_first_t (t::past) u terms
   210 
   211   fun dest_summing (Const (@{const_name Groups.plus}, _) $ t $ u, ts) =
   212         dest_summing (t, dest_summing (u, ts))
   213     | dest_summing (t, ts) = t :: ts
   214 
   215   val mk_sum = Arith_Data.long_mk_sum
   216   fun dest_sum t = dest_summing (t, [])
   217   val find_first = find_first_t []
   218   val trans_tac = Numeral_Simprocs.trans_tac
   219   val norm_ss =
   220     simpset_of (put_simpset HOL_basic_ss @{context}
   221       addsimps @{thms ac_simps add_0_left add_0_right})
   222   fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   223   fun simplify_meta_eq ctxt cancel_th th =
   224     Arith_Data.simplify_meta_eq [] ctxt
   225       ([th, cancel_th] MRS trans)
   226   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
   227 end
   228 
   229 structure Eq_Ennreal_Cancel = ExtractCommonTermFun
   230 (open Cancel_Ennreal_Common
   231   val mk_bal = HOLogic.mk_eq
   232   val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} @{typ ennreal}
   233   fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel}
   234 )
   235 
   236 structure Le_Ennreal_Cancel = ExtractCommonTermFun
   237 (open Cancel_Ennreal_Common
   238   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   239   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} @{typ ennreal}
   240   fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel_le}
   241 )
   242 
   243 structure Less_Ennreal_Cancel = ExtractCommonTermFun
   244 (open Cancel_Ennreal_Common
   245   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
   246   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} @{typ ennreal}
   247   fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel_less}
   248 )
   249 \<close>
   250 
   251 simproc_setup ennreal_eq_cancel
   252   ("(l::ennreal) + m = n" | "(l::ennreal) = m + n") =
   253   \<open>fn phi => fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
   254 
   255 simproc_setup ennreal_le_cancel
   256   ("(l::ennreal) + m \<le> n" | "(l::ennreal) \<le> m + n") =
   257   \<open>fn phi => fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
   258 
   259 simproc_setup ennreal_less_cancel
   260   ("(l::ennreal) + m < n" | "(l::ennreal) < m + n") =
   261   \<open>fn phi => fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
   262 
   263 instantiation ennreal :: linear_continuum_topology
   264 begin
   265 
   266 definition open_ennreal :: "ennreal set \<Rightarrow> bool"
   267   where "(open :: ennreal set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
   268 
   269 instance
   270 proof
   271   show "\<exists>a b::ennreal. a \<noteq> b"
   272     using zero_neq_one by (intro exI)
   273   show "\<And>x y::ennreal. x < y \<Longrightarrow> \<exists>z>x. z < y"
   274   proof transfer
   275     fix x y :: ereal assume "0 \<le> x" "x < y"
   276     moreover from dense[OF this(2)] guess z ..
   277     ultimately show "\<exists>z\<in>Collect (op \<le> 0). x < z \<and> z < y"
   278       by (intro bexI[of _ z]) auto
   279   qed
   280 qed (rule open_ennreal_def)
   281 
   282 end
   283 
   284 lemma ennreal_rat_dense:
   285   fixes x y :: ennreal
   286   shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
   287 proof transfer
   288   fix x y :: ereal assume xy: "0 \<le> x" "0 \<le> y" "x < y"
   289   moreover
   290   from ereal_dense3[OF \<open>x < y\<close>]
   291   obtain r where "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
   292     by auto
   293   moreover then have "0 \<le> r"
   294     using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto
   295   ultimately show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y"
   296     by (intro exI[of _ r]) (auto simp: max_absorb2)
   297 qed
   298 
   299 lemma enn2ereal_range: "e2ennreal ` {0..} = UNIV"
   300 proof -
   301   have "\<exists>y\<ge>0. x = e2ennreal y" for x
   302     by (cases x) (auto simp: e2ennreal_def max_absorb2)
   303   then show ?thesis
   304     by (auto simp: image_iff Bex_def)
   305 qed
   306 
   307 lemma enn2ereal_nonneg: "0 \<le> enn2ereal x"
   308   using ennreal.enn2ereal[of x] by simp
   309 
   310 lemma ereal_ennreal_cases:
   311   obtains b where "0 \<le> a" "a = enn2ereal b" | "a < 0"
   312   using e2ennreal'_inverse[of a, symmetric] by (cases "0 \<le> a") (auto intro: enn2ereal_nonneg)
   313 
   314 lemma enn2ereal_Iio: "enn2ereal -` {..<a} = (if 0 \<le> a then {..< e2ennreal a} else {})"
   315   using enn2ereal_nonneg
   316   by (cases a rule: ereal_ennreal_cases)
   317      (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
   318            intro: le_less_trans less_imp_le)
   319 
   320 lemma enn2ereal_Ioi: "enn2ereal -` {a <..} = (if 0 \<le> a then {e2ennreal a <..} else UNIV)"
   321   using enn2ereal_nonneg
   322   by (cases a rule: ereal_ennreal_cases)
   323      (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
   324            intro: less_le_trans)
   325 
   326 lemma continuous_on_e2ennreal: "continuous_on A e2ennreal"
   327 proof (rule continuous_on_subset)
   328   show "continuous_on ({0..} \<union> {..0}) e2ennreal"
   329   proof (rule continuous_on_closed_Un)
   330     show "continuous_on {0 ..} e2ennreal"
   331       by (rule continuous_onI_mono)
   332          (auto simp add: less_eq_ennreal.abs_eq eq_onp_def enn2ereal_range)
   333     show "continuous_on {.. 0} e2ennreal"
   334       by (subst continuous_on_cong[OF refl, of _ _ "\<lambda>_. 0"])
   335          (auto simp add: e2ennreal_neg continuous_on_const)
   336   qed auto
   337   show "A \<subseteq> {0..} \<union> {..0::ereal}"
   338     by auto
   339 qed
   340 
   341 lemma continuous_at_e2ennreal: "continuous (at x within A) e2ennreal"
   342   by (rule continuous_on_imp_continuous_within[OF continuous_on_e2ennreal, of _ UNIV]) auto
   343 
   344 lemma continuous_on_enn2ereal: "continuous_on UNIV enn2ereal"
   345   by (rule continuous_on_generate_topology[OF open_generated_order])
   346      (auto simp add: enn2ereal_Iio enn2ereal_Ioi)
   347 
   348 lemma continuous_at_enn2ereal: "continuous (at x within A) enn2ereal"
   349   by (rule continuous_on_imp_continuous_within[OF continuous_on_enn2ereal]) auto
   350 
   351 lemma transfer_enn2ereal_continuous_on [transfer_rule]:
   352   "rel_fun (op =) (rel_fun (rel_fun op = pcr_ennreal) op =) continuous_on continuous_on"
   353 proof -
   354   have "continuous_on A f" if "continuous_on A (\<lambda>x. enn2ereal (f x))" for A and f :: "'a \<Rightarrow> ennreal"
   355     using continuous_on_compose2[OF continuous_on_e2ennreal[of "{0..}"] that]
   356     by (auto simp: ennreal.enn2ereal_inverse subset_eq enn2ereal_nonneg e2ennreal_def max_absorb2)
   357   moreover
   358   have "continuous_on A (\<lambda>x. enn2ereal (f x))" if "continuous_on A f" for A and f :: "'a \<Rightarrow> ennreal"
   359     using continuous_on_compose2[OF continuous_on_enn2ereal that] by auto
   360   ultimately
   361   show ?thesis
   362     by (auto simp add: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)
   363 qed
   364 
   365 lemma continuous_on_add_ennreal[continuous_intros]:
   366   fixes f g :: "'a::topological_space \<Rightarrow> ennreal"
   367   shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x + g x)"
   368   by (transfer fixing: A) (auto intro!: tendsto_add_ereal_nonneg simp: continuous_on_def)
   369 
   370 lemma continuous_on_inverse_ennreal[continuous_intros]:
   371   fixes f :: "'a::topological_space \<Rightarrow> ennreal"
   372   shows "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))"
   373 proof (transfer fixing: A)
   374   show "pred_fun (\<lambda>_. True)  (op \<le> 0) f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))" if "continuous_on A f"
   375     for f :: "'a \<Rightarrow> ereal"
   376     using continuous_on_compose2[OF continuous_on_inverse_ereal that] by (auto simp: subset_eq)
   377 qed
   378 
   379 instance ennreal :: topological_comm_monoid_add
   380 proof
   381   show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)" for a b :: ennreal
   382     using continuous_on_add_ennreal[of UNIV fst snd]
   383     using tendsto_at_iff_tendsto_nhds[symmetric, of "\<lambda>x::(ennreal \<times> ennreal). fst x + snd x"]
   384     by (auto simp: continuous_on_eq_continuous_at)
   385        (simp add: isCont_def nhds_prod[symmetric])
   386 qed
   387 
   388 lemma ennreal_zero_less_top[simp]: "0 < (top::ennreal)"
   389   by transfer (simp add: top_ereal_def)
   390 
   391 lemma ennreal_one_less_top[simp]: "1 < (top::ennreal)"
   392   by transfer (simp add: top_ereal_def)
   393 
   394 lemma ennreal_zero_neq_top[simp]: "0 \<noteq> (top::ennreal)"
   395   by transfer (simp add: top_ereal_def)
   396 
   397 lemma ennreal_top_neq_zero[simp]: "(top::ennreal) \<noteq> 0"
   398   by transfer (simp add: top_ereal_def)
   399 
   400 lemma ennreal_top_neq_one[simp]: "top \<noteq> (1::ennreal)"
   401   by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
   402 
   403 lemma ennreal_one_neq_top[simp]: "1 \<noteq> (top::ennreal)"
   404   by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
   405 
   406 lemma ennreal_add_less_top[simp]:
   407   fixes a b :: ennreal
   408   shows "a + b < top \<longleftrightarrow> a < top \<and> b < top"
   409   by transfer (auto simp: top_ereal_def)
   410 
   411 lemma ennreal_add_eq_top[simp]:
   412   fixes a b :: ennreal
   413   shows "a + b = top \<longleftrightarrow> a = top \<or> b = top"
   414   by transfer (auto simp: top_ereal_def)
   415 
   416 lemma ennreal_setsum_less_top[simp]:
   417   fixes f :: "'a \<Rightarrow> ennreal"
   418   shows "finite I \<Longrightarrow> (\<Sum>i\<in>I. f i) < top \<longleftrightarrow> (\<forall>i\<in>I. f i < top)"
   419   by (induction I rule: finite_induct) auto
   420 
   421 lemma ennreal_setsum_eq_top[simp]:
   422   fixes f :: "'a \<Rightarrow> ennreal"
   423   shows "finite I \<Longrightarrow> (\<Sum>i\<in>I. f i) = top \<longleftrightarrow> (\<exists>i\<in>I. f i = top)"
   424   by (induction I rule: finite_induct) auto
   425 
   426 lemma enn2ereal_eq_top_iff[simp]: "enn2ereal x = \<infinity> \<longleftrightarrow> x = top"
   427   by transfer (simp add: top_ereal_def)
   428 
   429 lemma ennreal_top_top: "top - top = (top::ennreal)"
   430   by transfer (auto simp: top_ereal_def max_def)
   431 
   432 lemma ennreal_minus_zero[simp]: "a - (0::ennreal) = a"
   433   by transfer (auto simp: max_def)
   434 
   435 lemma ennreal_add_diff_cancel_right[simp]:
   436   fixes x y z :: ennreal shows "y \<noteq> top \<Longrightarrow> (x + y) - y = x"
   437   apply transfer
   438   subgoal for x y
   439     apply (cases x y rule: ereal2_cases)
   440     apply (auto split: split_max simp: top_ereal_def)
   441     done
   442   done
   443 
   444 lemma ennreal_add_diff_cancel_left[simp]:
   445   fixes x y z :: ennreal shows "y \<noteq> top \<Longrightarrow> (y + x) - y = x"
   446   by (simp add: add.commute)
   447 
   448 lemma
   449   fixes a b :: ennreal
   450   shows "a - b = 0 \<Longrightarrow> a \<le> b"
   451   apply transfer
   452   subgoal for a b
   453     apply (cases a b rule: ereal2_cases)
   454     apply (auto simp: not_le max_def split: if_splits)
   455     done
   456   done
   457 
   458 lemma ennreal_minus_cancel:
   459   fixes a b c :: ennreal
   460   shows "c \<noteq> top \<Longrightarrow> a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a = c - b \<Longrightarrow> a = b"
   461   apply transfer
   462   subgoal for a b c
   463     by (cases a b c rule: ereal3_cases)
   464        (auto simp: top_ereal_def max_def split: if_splits)
   465   done
   466 
   467 lemma enn2ereal_ennreal[simp]: "0 \<le> x \<Longrightarrow> enn2ereal (ennreal x) = x"
   468   by transfer (simp add: max_absorb2)
   469 
   470 lemma tendsto_ennrealD:
   471   assumes lim: "((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F"
   472   assumes *: "\<forall>\<^sub>F x in F. 0 \<le> f x" and x: "0 \<le> x"
   473   shows "(f \<longlongrightarrow> x) F"
   474   using continuous_on_tendsto_compose[OF continuous_on_enn2ereal lim]
   475   apply simp
   476   apply (subst (asm) tendsto_cong)
   477   using *
   478   apply eventually_elim
   479   apply (auto simp: max_absorb2 \<open>0 \<le> x\<close>)
   480   done
   481 
   482 lemma tendsto_ennreal_iff[simp]:
   483   "\<forall>\<^sub>F x in F. 0 \<le> f x \<Longrightarrow> 0 \<le> x \<Longrightarrow> ((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
   484   by (auto dest: tendsto_ennrealD)
   485      (auto simp: ennreal_def
   486            intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)
   487 
   488 lemma ennreal_zero[simp]: "ennreal 0 = 0"
   489   by (simp add: ennreal_def max.absorb1 zero_ennreal.abs_eq)
   490 
   491 lemma ennreal_plus[simp]:
   492   "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a + b) = ennreal a + ennreal b"
   493   by (transfer fixing: a b) (auto simp: max_absorb2)
   494 
   495 lemma ennreal_inj[simp]:
   496   "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal a = ennreal b \<longleftrightarrow> a = b"
   497   by (transfer fixing: a b) (auto simp: max_absorb2)
   498 
   499 lemma ennreal_le_iff[simp]: "0 \<le> y \<Longrightarrow> ennreal x \<le> ennreal y \<longleftrightarrow> x \<le> y"
   500   by (auto simp: ennreal_def zero_ereal_def less_eq_ennreal.abs_eq eq_onp_def split: split_max)
   501 
   502 lemma setsum_ennreal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. ennreal (f i)) = ennreal (setsum f I)"
   503   by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg)
   504 
   505 lemma sums_ennreal[simp]: "(\<And>i. 0 \<le> f i) \<Longrightarrow> 0 \<le> x \<Longrightarrow> (\<lambda>i. ennreal (f i)) sums ennreal x \<longleftrightarrow> f sums x"
   506   unfolding sums_def by (simp add: always_eventually setsum_nonneg)
   507 
   508 lemma summable_suminf_not_top: "(\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top \<Longrightarrow> summable f"
   509   using summable_sums[OF summableI, of "\<lambda>i. ennreal (f i)"]
   510   by (cases "\<Sum>i. ennreal (f i)" rule: ennreal_cases)
   511      (auto simp: summable_def)
   512 
   513 lemma suminf_ennreal[simp]:
   514   "(\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal (\<Sum>i. f i)"
   515   by (rule sums_unique[symmetric]) (simp add: summable_suminf_not_top suminf_nonneg summable_sums)
   516 
   517 lemma suminf_less_top: "(\<Sum>i. f i :: ennreal) < top \<Longrightarrow> f i < top"
   518   using le_less_trans[OF setsum_le_suminf[OF summableI, of "{i}" f]] by simp
   519 
   520 lemma add_top:
   521   fixes x :: "'a::{order_top, ordered_comm_monoid_add}"
   522   shows "0 \<le> x \<Longrightarrow> x + top = top"
   523   by (intro top_le add_increasing order_refl)
   524 
   525 lemma top_add:
   526   fixes x :: "'a::{order_top, ordered_comm_monoid_add}"
   527   shows "0 \<le> x \<Longrightarrow> top + x = top"
   528   by (intro top_le add_increasing2 order_refl)
   529 
   530 lemma enn2ereal_top: "enn2ereal top = \<infinity>"
   531   by transfer (simp add: top_ereal_def)
   532 
   533 lemma e2ennreal_infty: "e2ennreal \<infinity> = top"
   534   by (simp add: top_ennreal.abs_eq top_ereal_def)
   535 
   536 lemma sup_const_add_ennreal:
   537   fixes a b c :: "ennreal"
   538   shows "sup (c + a) (c + b) = c + sup a b"
   539   apply transfer
   540   subgoal for a b c
   541     apply (cases a b c rule: ereal3_cases)
   542     apply (auto simp: ereal_max[symmetric] simp del: ereal_max)
   543     apply (auto simp: top_ereal_def[symmetric] sup_ereal_def[symmetric]
   544                 simp del: sup_ereal_def)
   545     apply (auto simp add: top_ereal_def)
   546     done
   547   done
   548 
   549 lemma bot_ennreal: "bot = (0::ennreal)"
   550   by transfer rule
   551 
   552 lemma le_lfp: "mono f \<Longrightarrow> x \<le> lfp f \<Longrightarrow> f x \<le> lfp f"
   553   by (subst lfp_unfold) (auto dest: monoD)
   554 
   555 lemma lfp_transfer:
   556   assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and mg: "mono g"
   557   assumes bot: "\<alpha> bot \<le> lfp g" and eq: "\<And>x. x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
   558   shows "\<alpha> (lfp f) = lfp g"
   559 proof (rule antisym)
   560   note mf = sup_continuous_mono[OF f]
   561   have f_le_lfp: "(f ^^ i) bot \<le> lfp f" for i
   562     by (induction i) (auto intro: le_lfp mf)
   563 
   564   have "\<alpha> ((f ^^ i) bot) \<le> lfp g" for i
   565     by (induction i) (auto simp: bot eq f_le_lfp intro!: le_lfp mg)
   566   then show "\<alpha> (lfp f) \<le> lfp g"
   567     unfolding sup_continuous_lfp[OF f]
   568     by (subst \<alpha>[THEN sup_continuousD])
   569        (auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least)
   570 
   571   show "lfp g \<le> \<alpha> (lfp f)"
   572     by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_unfold[OF mf, symmetric])
   573 qed
   574 
   575 lemma sup_continuous_applyD: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x h)"
   576   using sup_continuous_apply[THEN sup_continuous_compose] .
   577 
   578 lemma INF_ennreal_add_const:
   579   fixes f g :: "nat \<Rightarrow> ennreal"
   580   shows "(INF i. f i + c) = (INF i. f i) + c"
   581   using continuous_at_Inf_mono[of "\<lambda>x. x + c" "f`UNIV"]
   582   using continuous_add[of "at_right (Inf (range f))", of "\<lambda>x. x" "\<lambda>x. c"]
   583   by (auto simp: mono_def)
   584 
   585 lemma INF_ennreal_const_add:
   586   fixes f g :: "nat \<Rightarrow> ennreal"
   587   shows "(INF i. c + f i) = c + (INF i. f i)"
   588   using INF_ennreal_add_const[of f c] by (simp add: ac_simps)
   589 
   590 lemma sup_continuous_e2ennreal[order_continuous_intros]:
   591   assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. e2ennreal (f x))"
   592   apply (rule sup_continuous_compose[OF _ f])
   593   apply (rule continuous_at_left_imp_sup_continuous)
   594   apply (auto simp: mono_def e2ennreal_mono continuous_at_e2ennreal)
   595   done
   596 
   597 lemma sup_continuous_enn2ereal[order_continuous_intros]:
   598   assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. enn2ereal (f x))"
   599   apply (rule sup_continuous_compose[OF _ f])
   600   apply (rule continuous_at_left_imp_sup_continuous)
   601   apply (simp_all add: mono_def less_eq_ennreal.rep_eq continuous_at_enn2ereal)
   602   done
   603 
   604 lemma ennreal_1[simp]: "ennreal 1 = 1"
   605   by transfer (simp add: max_absorb2)
   606 
   607 lemma ennreal_of_nat_eq_real_of_nat: "of_nat i = ennreal (of_nat i)"
   608   by (induction i) simp_all
   609 
   610 lemma ennreal_SUP_of_nat_eq_top: "(SUP x. of_nat x :: ennreal) = top"
   611 proof (intro antisym top_greatest le_SUP_iff[THEN iffD2] allI impI)
   612   fix y :: ennreal assume "y < top"
   613   then obtain r where "y = ennreal r"
   614     by (cases y rule: ennreal_cases) auto
   615   then show "\<exists>i\<in>UNIV. y < of_nat i"
   616     using ex_less_of_nat[of "max 1 r"] zero_less_one
   617     by (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_def less_ennreal.abs_eq eq_onp_def max.absorb2
   618              dest!: one_less_of_natD intro: less_trans)
   619 qed
   620 
   621 lemma ennreal_SUP_eq_top:
   622   fixes f :: "'a \<Rightarrow> ennreal"
   623   assumes "\<And>n. \<exists>i\<in>I. of_nat n \<le> f i"
   624   shows "(SUP i : I. f i) = top"
   625 proof -
   626   have "(SUP x. of_nat x :: ennreal) \<le> (SUP i : I. f i)"
   627     using assms by (auto intro!: SUP_least intro: SUP_upper2)
   628   then show ?thesis
   629     by (auto simp: ennreal_SUP_of_nat_eq_top top_unique)
   630 qed
   631 
   632 lemma sup_continuous_SUP[order_continuous_intros]:
   633   fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
   634   assumes M: "\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)"
   635   shows  "sup_continuous (SUP i:I. M i)"
   636   unfolding sup_continuous_def by (auto simp add: sup_continuousD[OF M] intro: SUP_commute)
   637 
   638 lemma sup_continuous_apply_SUP[order_continuous_intros]:
   639   fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
   640   shows "(\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)) \<Longrightarrow> sup_continuous (\<lambda>x. SUP i:I. M i x)"
   641   unfolding SUP_apply[symmetric] by (rule sup_continuous_SUP)
   642 
   643 lemma sup_continuous_lfp'[order_continuous_intros]:
   644   assumes 1: "sup_continuous f"
   645   assumes 2: "\<And>g. sup_continuous g \<Longrightarrow> sup_continuous (f g)"
   646   shows "sup_continuous (lfp f)"
   647 proof -
   648   have "sup_continuous ((f ^^ i) bot)" for i
   649   proof (induction i)
   650     case (Suc i) then show ?case
   651       by (auto intro!: 2)
   652   qed (simp add: bot_fun_def sup_continuous_const)
   653   then show ?thesis
   654     unfolding sup_continuous_lfp[OF 1] by (intro order_continuous_intros)
   655 qed
   656 
   657 lemma sup_continuous_lfp''[order_continuous_intros]:
   658   assumes 1: "\<And>s. sup_continuous (f s)"
   659   assumes 2: "\<And>g. sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>s. f s (g s))"
   660   shows "sup_continuous (\<lambda>x. lfp (f x))"
   661 proof -
   662   have "sup_continuous (\<lambda>x. (f x ^^ i) bot)" for i
   663   proof (induction i)
   664     case (Suc i) then show ?case
   665       by (auto intro!: 2)
   666   qed (simp add: bot_fun_def sup_continuous_const)
   667   then show ?thesis
   668     unfolding sup_continuous_lfp[OF 1] by (intro order_continuous_intros)
   669 qed
   670 
   671 lemma ennreal_INF_const_minus:
   672   fixes f :: "'a \<Rightarrow> ennreal"
   673   shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
   674   by (transfer fixing: I)
   675      (simp add: sup_max[symmetric] SUP_sup_const1 SUP_ereal_minus_right del: sup_ereal_def)
   676 
   677 lemma ennreal_diff_add_assoc:
   678   fixes a b c :: ennreal
   679   shows "a \<le> b \<Longrightarrow> c + b - a = c + (b - a)"
   680   apply transfer
   681   subgoal for a b c
   682     apply (cases a b c rule: ereal3_cases)
   683     apply (auto simp: field_simps max_absorb2)
   684     done
   685   done
   686 
   687 lemma ennreal_top_minus[simp]:
   688   fixes c :: ennreal
   689   shows "top - c = top"
   690   by transfer (auto simp: top_ereal_def max_absorb2)
   691 
   692 lemma le_ennreal_iff:
   693   "0 \<le> r \<Longrightarrow> x \<le> ennreal r \<longleftrightarrow> (\<exists>q\<ge>0. x = ennreal q \<and> q \<le> r)"
   694   apply (transfer fixing: r)
   695   subgoal for x
   696     by (cases x) (auto simp: max_absorb2 cong: conj_cong)
   697   done
   698 
   699 lemma ennreal_minus: "0 \<le> q \<Longrightarrow> q \<le> r \<Longrightarrow> ennreal r - ennreal q = ennreal (r - q)"
   700   by transfer (simp add: max_absorb2)
   701 
   702 lemma ennreal_tendsto_const_minus:
   703   fixes g :: "'a \<Rightarrow> ennreal"
   704   assumes ae: "\<forall>\<^sub>F x in F. g x \<le> c"
   705   assumes g: "((\<lambda>x. c - g x) \<longlongrightarrow> 0) F"
   706   shows "(g \<longlongrightarrow> c) F"
   707 proof (cases c rule: ennreal_cases)
   708   case top with tendsto_unique[OF _ g, of "top"] show ?thesis
   709     by (cases "F = bot") auto
   710 next
   711   case (real r)
   712   then have "\<forall>x. \<exists>q\<ge>0. g x \<le> c \<longrightarrow> (g x = ennreal q \<and> q \<le> r)"
   713     by (auto simp: le_ennreal_iff)
   714   then obtain f where *: "\<And>x. g x \<le> c \<Longrightarrow> 0 \<le> f x" "\<And>x. g x \<le> c \<Longrightarrow> g x = ennreal (f x)" "\<And>x. g x \<le> c \<Longrightarrow> f x \<le> r"
   715     by metis
   716   from ae have ae2: "\<forall>\<^sub>F x in F. c - g x = ennreal (r - f x) \<and> f x \<le> r \<and> g x = ennreal (f x) \<and> 0 \<le> f x"
   717   proof eventually_elim
   718     fix x assume "g x \<le> c" with *[of x] \<open>0 \<le> r\<close> show "c - g x = ennreal (r - f x) \<and> f x \<le> r \<and> g x = ennreal (f x) \<and> 0 \<le> f x"
   719       by (auto simp: real ennreal_minus)
   720   qed
   721   with g have "((\<lambda>x. ennreal (r - f x)) \<longlongrightarrow> ennreal 0) F"
   722     by (auto simp add: tendsto_cong eventually_conj_iff)
   723   with ae2 have "((\<lambda>x. r - f x) \<longlongrightarrow> 0) F"
   724     by (subst (asm) tendsto_ennreal_iff) (auto elim: eventually_mono)
   725   then have "(f \<longlongrightarrow> r) F"
   726     by (rule Lim_transform2[OF tendsto_const])
   727   with ae2 have "((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal r) F"
   728     by (subst tendsto_ennreal_iff) (auto elim: eventually_mono simp: real)
   729   with ae2 show ?thesis
   730     by (auto simp: real tendsto_cong eventually_conj_iff)
   731 qed
   732 
   733 lemma ereal_add_diff_cancel:
   734   fixes a b :: ereal
   735   shows "\<bar>b\<bar> \<noteq> \<infinity> \<Longrightarrow> (a + b) - b = a"
   736   by (cases a b rule: ereal2_cases) auto
   737 
   738 lemma ennreal_add_diff_cancel:
   739   fixes a b :: ennreal
   740   shows "b \<noteq> \<infinity> \<Longrightarrow> (a + b) - b = a"
   741   unfolding infinity_ennreal_def
   742   by transfer (simp add: max_absorb2 top_ereal_def ereal_add_diff_cancel)
   743 
   744 lemma ennreal_mult_eq_top_iff:
   745   fixes a b :: ennreal
   746   shows "a * b = top \<longleftrightarrow> (a = top \<and> b \<noteq> 0) \<or> (b = top \<and> a \<noteq> 0)"
   747   by transfer (auto simp: top_ereal_def)
   748 
   749 lemma ennreal_top_eq_mult_iff:
   750   fixes a b :: ennreal
   751   shows "top = a * b \<longleftrightarrow> (a = top \<and> b \<noteq> 0) \<or> (b = top \<and> a \<noteq> 0)"
   752   using ennreal_mult_eq_top_iff[of a b] by auto
   753 
   754 lemma ennreal_mult: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"
   755   by transfer (simp add: max_absorb2)
   756 
   757 lemma setsum_enn2ereal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. enn2ereal (f i)) = enn2ereal (setsum f I)"
   758   by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg zero_ennreal.rep_eq plus_ennreal.rep_eq)
   759 
   760 lemma e2ennreal_enn2ereal[simp]: "e2ennreal (enn2ereal x) = x"
   761   by (simp add: e2ennreal_def max_absorb2 enn2ereal_nonneg ennreal.enn2ereal_inverse)
   762 
   763 lemma tendsto_enn2ereal_iff[simp]: "((\<lambda>i. enn2ereal (f i)) \<longlongrightarrow> enn2ereal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
   764   using continuous_on_enn2ereal[THEN continuous_on_tendsto_compose, of f x F]
   765     continuous_on_e2ennreal[THEN continuous_on_tendsto_compose, of "\<lambda>x. enn2ereal (f x)" "enn2ereal x" F UNIV]
   766   by auto
   767 
   768 lemma sums_enn2ereal[simp]: "(\<lambda>i. enn2ereal (f i)) sums enn2ereal x \<longleftrightarrow> f sums x"
   769   unfolding sums_def by (simp add: always_eventually setsum_nonneg setsum_enn2ereal)
   770 
   771 lemma suminf_enn2real[simp]: "(\<Sum>i. enn2ereal (f i)) = enn2ereal (suminf f)"
   772   by (rule sums_unique[symmetric]) (simp add: summable_sums)
   773 
   774 lemma pcr_ennreal_enn2ereal[simp]: "pcr_ennreal (enn2ereal x) x"
   775   by (simp add: ennreal.pcr_cr_eq cr_ennreal_def)
   776 
   777 lemma rel_fun_eq_pcr_ennreal: "rel_fun op = pcr_ennreal f g \<longleftrightarrow> f = enn2ereal \<circ> g"
   778   by (auto simp: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)
   779 
   780 lemma transfer_e2ennreal_suminf [transfer_rule]: "rel_fun (rel_fun op = pcr_ennreal) pcr_ennreal suminf suminf"
   781   by (auto simp: rel_funI rel_fun_eq_pcr_ennreal comp_def)
   782 
   783 lemma ennreal_suminf_cmult[simp]: "(\<Sum>i. r * f i) = r * (\<Sum>i. f i::ennreal)"
   784   by transfer (auto intro!: suminf_cmult_ereal)
   785 
   786 lemma ennreal_suminf_SUP_eq_directed:
   787   fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
   788   assumes *: "\<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"
   789   shows "(\<Sum>n. SUP i:I. f i n) = (SUP i:I. \<Sum>n. f i n)"
   790 proof cases
   791   assume "I \<noteq> {}"
   792   then obtain i where "i \<in> I" by auto
   793   from * show ?thesis
   794     by (transfer fixing: I)
   795        (auto simp: max_absorb2 SUP_upper2[OF \<open>i \<in> I\<close>] suminf_nonneg summable_ereal_pos \<open>I \<noteq> {}\<close>
   796              intro!: suminf_SUP_eq_directed)
   797 qed (simp add: bot_ennreal)
   798 
   799 lemma ennreal_eq_zero_iff[simp]: "0 \<le> x \<Longrightarrow> ennreal x = 0 \<longleftrightarrow> x = 0"
   800   by transfer (auto simp: max_absorb2)
   801 
   802 lemma ennreal_neq_top[simp]: "ennreal r \<noteq> top"
   803   by transfer (simp add: top_ereal_def zero_ereal_def ereal_max[symmetric] del: ereal_max)
   804 
   805 lemma ennreal_of_nat_neq_top[simp]: "of_nat i \<noteq> (top::ennreal)"
   806   by (induction i) auto
   807 
   808 lemma ennreal_suminf_neq_top: "summable f \<Longrightarrow> (\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top"
   809   using sums_ennreal[of f "suminf f"]
   810   by (simp add: suminf_nonneg sums_unique[symmetric] summable_sums_iff[symmetric] del: sums_ennreal)
   811 
   812 instance ennreal :: semiring_char_0
   813 proof (standard, safe intro!: linorder_injI)
   814   have *: "1 + of_nat k \<noteq> (0::ennreal)" for k
   815     using add_pos_nonneg[OF zero_less_one, of "of_nat k :: ennreal"] by auto
   816   fix x y :: nat assume "x < y" "of_nat x = (of_nat y::ennreal)" then show False
   817     by (auto simp add: less_iff_Suc_add *)
   818 qed
   819 
   820 lemma ennreal_suminf_lessD: "(\<Sum>i. f i :: ennreal) < x \<Longrightarrow> f i < x"
   821   using le_less_trans[OF setsum_le_suminf[OF summableI, of "{i}" f]] by simp
   822 
   823 lemma ennreal_less_top[simp]: "ennreal x < top"
   824   by transfer (simp add: top_ereal_def max_def)
   825 
   826 lemma ennreal_le_epsilon:
   827   "(\<And>e::real. y < top \<Longrightarrow> 0 < e \<Longrightarrow> x \<le> y + ennreal e) \<Longrightarrow> x \<le> y"
   828   apply (cases y rule: ennreal_cases)
   829   apply (cases x rule: ennreal_cases)
   830   apply (auto simp del: ennreal_plus simp add: top_unique ennreal_plus[symmetric]
   831     intro: zero_less_one field_le_epsilon)
   832   done
   833 
   834 lemma ennreal_less_zero_iff[simp]: "0 < ennreal x \<longleftrightarrow> 0 < x"
   835   by transfer (auto simp: max_def)
   836 
   837 lemma suminf_ennreal_eq:
   838   "(\<And>i. 0 \<le> f i) \<Longrightarrow> f sums x \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal x"
   839   using suminf_nonneg[of f] sums_unique[of f x]
   840   by (intro sums_unique[symmetric]) (auto simp: summable_sums_iff)
   841 
   842 lemma transfer_e2ennreal_sumset [transfer_rule]:
   843   "rel_fun (rel_fun op = pcr_ennreal) (rel_fun op = pcr_ennreal) setsum setsum"
   844   by (auto intro!: rel_funI simp: rel_fun_eq_pcr_ennreal comp_def)
   845 
   846 lemma ennreal_suminf_bound_add:
   847   fixes f :: "nat \<Rightarrow> ennreal"
   848   shows "(\<And>N. (\<Sum>n<N. f n) + y \<le> x) \<Longrightarrow> suminf f + y \<le> x"
   849   by transfer (auto intro!: suminf_bound_add)
   850 
   851 end