src/HOL/Library/Extended_Nonnegative_Real.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 65687 a68973661472 child 66936 cf8d8fc23891 permissions -rw-r--r--
executable domain membership checks
```     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 Indicator_Function
```
```     9 begin
```
```    10
```
```    11 lemma ereal_ineq_diff_add:
```
```    12   assumes "b \<noteq> (-\<infinity>::ereal)" "a \<ge> b"
```
```    13   shows "a = b + (a-b)"
```
```    14 by (metis add.commute assms(1) assms(2) ereal_eq_minus_iff ereal_minus_le_iff ereal_plus_eq_PInfty)
```
```    15
```
```    16 lemma Limsup_const_add:
```
```    17   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
```
```    18   shows "F \<noteq> bot \<Longrightarrow> Limsup F (\<lambda>x. c + f x) = c + Limsup F f"
```
```    19   by (rule Limsup_compose_continuous_mono)
```
```    20      (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
```
```    21
```
```    22 lemma Liminf_const_add:
```
```    23   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
```
```    24   shows "F \<noteq> bot \<Longrightarrow> Liminf F (\<lambda>x. c + f x) = c + Liminf F f"
```
```    25   by (rule Liminf_compose_continuous_mono)
```
```    26      (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
```
```    27
```
```    28 lemma Liminf_add_const:
```
```    29   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
```
```    30   shows "F \<noteq> bot \<Longrightarrow> Liminf F (\<lambda>x. f x + c) = Liminf F f + c"
```
```    31   by (rule Liminf_compose_continuous_mono)
```
```    32      (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
```
```    33
```
```    34 lemma sums_offset:
```
```    35   fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
```
```    36   assumes "(\<lambda>n. f (n + i)) sums l" shows "f sums (l + (\<Sum>j<i. f j))"
```
```    37 proof  -
```
```    38   have "(\<lambda>k. (\<Sum>n<k. f (n + i)) + (\<Sum>j<i. f j)) \<longlonglongrightarrow> l + (\<Sum>j<i. f j)"
```
```    39     using assms by (auto intro!: tendsto_add simp: sums_def)
```
```    40   moreover
```
```    41   { fix k :: nat
```
```    42     have "(\<Sum>j<k + i. f j) = (\<Sum>j=i..<k + i. f j) + (\<Sum>j=0..<i. f j)"
```
```    43       by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
```
```    44     also have "(\<Sum>j=i..<k + i. f j) = (\<Sum>j\<in>(\<lambda>n. n + i)`{0..<k}. f j)"
```
```    45       unfolding image_add_atLeastLessThan by simp
```
```    46     finally have "(\<Sum>j<k + i. f j) = (\<Sum>n<k. f (n + i)) + (\<Sum>j<i. f j)"
```
```    47       by (auto simp: inj_on_def atLeast0LessThan sum.reindex) }
```
```    48   ultimately have "(\<lambda>k. (\<Sum>n<k + i. f n)) \<longlonglongrightarrow> l + (\<Sum>j<i. f j)"
```
```    49     by simp
```
```    50   then show ?thesis
```
```    51     unfolding sums_def by (rule LIMSEQ_offset)
```
```    52 qed
```
```    53
```
```    54 lemma suminf_offset:
```
```    55   fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
```
```    56   shows "summable (\<lambda>j. f (j + i)) \<Longrightarrow> suminf f = (\<Sum>j. f (j + i)) + (\<Sum>j<i. f j)"
```
```    57   by (intro sums_unique[symmetric] sums_offset summable_sums)
```
```    58
```
```    59 lemma eventually_at_left_1: "(\<And>z::real. 0 < z \<Longrightarrow> z < 1 \<Longrightarrow> P z) \<Longrightarrow> eventually P (at_left 1)"
```
```    60   by (subst eventually_at_left[of 0]) (auto intro: exI[of _ 0])
```
```    61
```
```    62 lemma mult_eq_1:
```
```    63   fixes a b :: "'a :: {ordered_semiring, comm_monoid_mult}"
```
```    64   shows "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b = 1 \<longleftrightarrow> (a = 1 \<and> b = 1)"
```
```    65   by (metis mult.left_neutral eq_iff mult.commute mult_right_mono)
```
```    66
```
```    67 lemma ereal_add_diff_cancel:
```
```    68   fixes a b :: ereal
```
```    69   shows "\<bar>b\<bar> \<noteq> \<infinity> \<Longrightarrow> (a + b) - b = a"
```
```    70   by (cases a b rule: ereal2_cases) auto
```
```    71
```
```    72 lemma add_top:
```
```    73   fixes x :: "'a::{order_top, ordered_comm_monoid_add}"
```
```    74   shows "0 \<le> x \<Longrightarrow> x + top = top"
```
```    75   by (intro top_le add_increasing order_refl)
```
```    76
```
```    77 lemma top_add:
```
```    78   fixes x :: "'a::{order_top, ordered_comm_monoid_add}"
```
```    79   shows "0 \<le> x \<Longrightarrow> top + x = top"
```
```    80   by (intro top_le add_increasing2 order_refl)
```
```    81
```
```    82 lemma le_lfp: "mono f \<Longrightarrow> x \<le> lfp f \<Longrightarrow> f x \<le> lfp f"
```
```    83   by (subst lfp_unfold) (auto dest: monoD)
```
```    84
```
```    85 lemma lfp_transfer:
```
```    86   assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and mg: "mono g"
```
```    87   assumes bot: "\<alpha> bot \<le> lfp g" and eq: "\<And>x. x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
```
```    88   shows "\<alpha> (lfp f) = lfp g"
```
```    89 proof (rule antisym)
```
```    90   note mf = sup_continuous_mono[OF f]
```
```    91   have f_le_lfp: "(f ^^ i) bot \<le> lfp f" for i
```
```    92     by (induction i) (auto intro: le_lfp mf)
```
```    93
```
```    94   have "\<alpha> ((f ^^ i) bot) \<le> lfp g" for i
```
```    95     by (induction i) (auto simp: bot eq f_le_lfp intro!: le_lfp mg)
```
```    96   then show "\<alpha> (lfp f) \<le> lfp g"
```
```    97     unfolding sup_continuous_lfp[OF f]
```
```    98     by (subst \<alpha>[THEN sup_continuousD])
```
```    99        (auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least)
```
```   100
```
```   101   show "lfp g \<le> \<alpha> (lfp f)"
```
```   102     by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_fixpoint[OF mf])
```
```   103 qed
```
```   104
```
```   105 lemma sup_continuous_applyD: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x h)"
```
```   106   using sup_continuous_apply[THEN sup_continuous_compose] .
```
```   107
```
```   108 lemma sup_continuous_SUP[order_continuous_intros]:
```
```   109   fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
```
```   110   assumes M: "\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)"
```
```   111   shows  "sup_continuous (SUP i:I. M i)"
```
```   112   unfolding sup_continuous_def by (auto simp add: sup_continuousD[OF M] intro: SUP_commute)
```
```   113
```
```   114 lemma sup_continuous_apply_SUP[order_continuous_intros]:
```
```   115   fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
```
```   116   shows "(\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)) \<Longrightarrow> sup_continuous (\<lambda>x. SUP i:I. M i x)"
```
```   117   unfolding SUP_apply[symmetric] by (rule sup_continuous_SUP)
```
```   118
```
```   119 lemma sup_continuous_lfp'[order_continuous_intros]:
```
```   120   assumes 1: "sup_continuous f"
```
```   121   assumes 2: "\<And>g. sup_continuous g \<Longrightarrow> sup_continuous (f g)"
```
```   122   shows "sup_continuous (lfp f)"
```
```   123 proof -
```
```   124   have "sup_continuous ((f ^^ i) bot)" for i
```
```   125   proof (induction i)
```
```   126     case (Suc i) then show ?case
```
```   127       by (auto intro!: 2)
```
```   128   qed (simp add: bot_fun_def sup_continuous_const)
```
```   129   then show ?thesis
```
```   130     unfolding sup_continuous_lfp[OF 1] by (intro order_continuous_intros)
```
```   131 qed
```
```   132
```
```   133 lemma sup_continuous_lfp''[order_continuous_intros]:
```
```   134   assumes 1: "\<And>s. sup_continuous (f s)"
```
```   135   assumes 2: "\<And>g. sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>s. f s (g s))"
```
```   136   shows "sup_continuous (\<lambda>x. lfp (f x))"
```
```   137 proof -
```
```   138   have "sup_continuous (\<lambda>x. (f x ^^ i) bot)" for i
```
```   139   proof (induction i)
```
```   140     case (Suc i) then show ?case
```
```   141       by (auto intro!: 2)
```
```   142   qed (simp add: bot_fun_def sup_continuous_const)
```
```   143   then show ?thesis
```
```   144     unfolding sup_continuous_lfp[OF 1] by (intro order_continuous_intros)
```
```   145 qed
```
```   146
```
```   147 lemma mono_INF_fun:
```
```   148     "(\<And>x y. mono (F x y)) \<Longrightarrow> mono (\<lambda>z x. INF y : X x. F x y z :: 'a :: complete_lattice)"
```
```   149   by (auto intro!: INF_mono[OF bexI] simp: le_fun_def mono_def)
```
```   150
```
```   151 lemma continuous_on_max:
```
```   152   fixes f g :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
```
```   153   shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. max (f x) (g x))"
```
```   154   by (auto simp: continuous_on_def intro!: tendsto_max)
```
```   155
```
```   156 lemma continuous_on_cmult_ereal:
```
```   157   "\<bar>c::ereal\<bar> \<noteq> \<infinity> \<Longrightarrow> continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. c * f x)"
```
```   158   using tendsto_cmult_ereal[of c f "f x" "at x within A" for x]
```
```   159   by (auto simp: continuous_on_def simp del: tendsto_cmult_ereal)
```
```   160
```
```   161 context linordered_nonzero_semiring
```
```   162 begin
```
```   163
```
```   164 lemma of_nat_nonneg [simp]: "0 \<le> of_nat n"
```
```   165   by (induct n) simp_all
```
```   166
```
```   167 lemma of_nat_mono[simp]: "i \<le> j \<Longrightarrow> of_nat i \<le> of_nat j"
```
```   168   by (auto simp add: le_iff_add intro!: add_increasing2)
```
```   169
```
```   170 end
```
```   171
```
```   172 lemma real_of_nat_Sup:
```
```   173   assumes "A \<noteq> {}" "bdd_above A"
```
```   174   shows "of_nat (Sup A) = (SUP a:A. of_nat a :: real)"
```
```   175 proof (intro antisym)
```
```   176   show "(SUP a:A. of_nat a::real) \<le> of_nat (Sup A)"
```
```   177     using assms by (intro cSUP_least of_nat_mono) (auto intro: cSup_upper)
```
```   178   have "Sup A \<in> A"
```
```   179     unfolding Sup_nat_def using assms by (intro Max_in) (auto simp: bdd_above_nat)
```
```   180   then show "of_nat (Sup A) \<le> (SUP a:A. of_nat a::real)"
```
```   181     by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
```
```   182 qed
```
```   183
```
```   184 (*These generalise their counterparts in Nat.linordered_semidom_class*)
```
```   185 lemma of_nat_less[simp]:
```
```   186   "m < n \<Longrightarrow> of_nat m < (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0})"
```
```   187   by (auto simp: less_le)
```
```   188
```
```   189 lemma of_nat_le_iff[simp]:
```
```   190   "of_nat m \<le> (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0}) \<longleftrightarrow> m \<le> n"
```
```   191 proof (safe intro!: of_nat_mono)
```
```   192   assume "of_nat m \<le> (of_nat n::'a)" then show "m \<le> n"
```
```   193   proof (intro leI notI)
```
```   194     assume "n < m" from less_le_trans[OF of_nat_less[OF this] \<open>of_nat m \<le> of_nat n\<close>] show False
```
```   195       by blast
```
```   196   qed
```
```   197 qed
```
```   198
```
```   199 lemma (in complete_lattice) SUP_sup_const1:
```
```   200   "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup c (f i)) = sup c (SUP i:I. f i)"
```
```   201   using SUP_sup_distrib[of "\<lambda>_. c" I f] by simp
```
```   202
```
```   203 lemma (in complete_lattice) SUP_sup_const2:
```
```   204   "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup (f i) c) = sup (SUP i:I. f i) c"
```
```   205   using SUP_sup_distrib[of f I "\<lambda>_. c"] by simp
```
```   206
```
```   207 lemma one_less_of_natD:
```
```   208   "(1::'a::linordered_semidom) < of_nat n \<Longrightarrow> 1 < n"
```
```   209   using zero_le_one[where 'a='a]
```
```   210   apply (cases n)
```
```   211   apply simp
```
```   212   subgoal for n'
```
```   213     apply (cases n')
```
```   214     apply simp
```
```   215     apply simp
```
```   216     done
```
```   217   done
```
```   218
```
```   219 lemma sum_le_suminf:
```
```   220   fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
```
```   221   shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> sum f I \<le> suminf f"
```
```   222   by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
```
```   223
```
```   224 lemma suminf_eq_SUP_real:
```
```   225   assumes X: "summable X" "\<And>i. 0 \<le> X i" shows "suminf X = (SUP i. \<Sum>n<i. X n::real)"
```
```   226   by (intro LIMSEQ_unique[OF summable_LIMSEQ] X LIMSEQ_incseq_SUP)
```
```   227      (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono2)
```
```   228
```
```   229 subsection \<open>Defining the extended non-negative reals\<close>
```
```   230
```
```   231 text \<open>Basic definitions and type class setup\<close>
```
```   232
```
```   233 typedef ennreal = "{x :: ereal. 0 \<le> x}"
```
```   234   morphisms enn2ereal e2ennreal'
```
```   235   by auto
```
```   236
```
```   237 definition "e2ennreal x = e2ennreal' (max 0 x)"
```
```   238
```
```   239 lemma enn2ereal_range: "e2ennreal ` {0..} = UNIV"
```
```   240 proof -
```
```   241   have "\<exists>y\<ge>0. x = e2ennreal y" for x
```
```   242     by (cases x) (auto simp: e2ennreal_def max_absorb2)
```
```   243   then show ?thesis
```
```   244     by (auto simp: image_iff Bex_def)
```
```   245 qed
```
```   246
```
```   247 lemma type_definition_ennreal': "type_definition enn2ereal e2ennreal {x. 0 \<le> x}"
```
```   248   using type_definition_ennreal
```
```   249   by (auto simp: type_definition_def e2ennreal_def max_absorb2)
```
```   250
```
```   251 setup_lifting type_definition_ennreal'
```
```   252
```
```   253 declare [[coercion e2ennreal]]
```
```   254
```
```   255 instantiation ennreal :: complete_linorder
```
```   256 begin
```
```   257
```
```   258 lift_definition top_ennreal :: ennreal is top by (rule top_greatest)
```
```   259 lift_definition bot_ennreal :: ennreal is 0 by (rule order_refl)
```
```   260 lift_definition sup_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is sup by (rule le_supI1)
```
```   261 lift_definition inf_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is inf by (rule le_infI)
```
```   262
```
```   263 lift_definition Inf_ennreal :: "ennreal set \<Rightarrow> ennreal" is "Inf"
```
```   264   by (rule Inf_greatest)
```
```   265
```
```   266 lift_definition Sup_ennreal :: "ennreal set \<Rightarrow> ennreal" is "sup 0 \<circ> Sup"
```
```   267   by auto
```
```   268
```
```   269 lift_definition less_eq_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op \<le>" .
```
```   270 lift_definition less_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op <" .
```
```   271
```
```   272 instance
```
```   273   by standard
```
```   274      (transfer ; auto simp: Inf_lower Inf_greatest Sup_upper Sup_least le_max_iff_disj max.absorb1)+
```
```   275
```
```   276 end
```
```   277
```
```   278 lemma pcr_ennreal_enn2ereal[simp]: "pcr_ennreal (enn2ereal x) x"
```
```   279   by (simp add: ennreal.pcr_cr_eq cr_ennreal_def)
```
```   280
```
```   281 lemma rel_fun_eq_pcr_ennreal: "rel_fun op = pcr_ennreal f g \<longleftrightarrow> f = enn2ereal \<circ> g"
```
```   282   by (auto simp: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)
```
```   283
```
```   284 instantiation ennreal :: infinity
```
```   285 begin
```
```   286
```
```   287 definition infinity_ennreal :: ennreal
```
```   288 where
```
```   289   [simp]: "\<infinity> = (top::ennreal)"
```
```   290
```
```   291 instance ..
```
```   292
```
```   293 end
```
```   294
```
```   295 instantiation ennreal :: "{semiring_1_no_zero_divisors, comm_semiring_1}"
```
```   296 begin
```
```   297
```
```   298 lift_definition one_ennreal :: ennreal is 1 by simp
```
```   299 lift_definition zero_ennreal :: ennreal is 0 by simp
```
```   300 lift_definition plus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "op +" by simp
```
```   301 lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "op *" by simp
```
```   302
```
```   303 instance
```
```   304   by standard (transfer; auto simp: field_simps ereal_right_distrib)+
```
```   305
```
```   306 end
```
```   307
```
```   308 instantiation ennreal :: minus
```
```   309 begin
```
```   310
```
```   311 lift_definition minus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "\<lambda>a b. max 0 (a - b)"
```
```   312   by simp
```
```   313
```
```   314 instance ..
```
```   315
```
```   316 end
```
```   317
```
```   318 instance ennreal :: numeral ..
```
```   319
```
```   320 instantiation ennreal :: inverse
```
```   321 begin
```
```   322
```
```   323 lift_definition inverse_ennreal :: "ennreal \<Rightarrow> ennreal" is inverse
```
```   324   by (rule inverse_ereal_ge0I)
```
```   325
```
```   326 definition divide_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal"
```
```   327   where "x div y = x * inverse (y :: ennreal)"
```
```   328
```
```   329 instance ..
```
```   330
```
```   331 end
```
```   332
```
```   333 lemma ennreal_zero_less_one: "0 < (1::ennreal)" \<comment> \<open>TODO: remove \<close>
```
```   334   by transfer auto
```
```   335
```
```   336 instance ennreal :: dioid
```
```   337 proof (standard; transfer)
```
```   338   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)"
```
```   339     unfolding ereal_ex_split Bex_def
```
```   340     by (cases a b rule: ereal2_cases) (auto intro!: exI[of _ "real_of_ereal (b - a)"])
```
```   341 qed
```
```   342
```
```   343 instance ennreal :: ordered_comm_semiring
```
```   344   by standard
```
```   345      (transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+
```
```   346
```
```   347 instance ennreal :: linordered_nonzero_semiring
```
```   348   proof qed (transfer; simp)
```
```   349
```
```   350 instance ennreal :: strict_ordered_ab_semigroup_add
```
```   351 proof
```
```   352   fix a b c d :: ennreal show "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
```
```   353     by transfer (auto intro!: ereal_add_strict_mono)
```
```   354 qed
```
```   355
```
```   356 declare [[coercion "of_nat :: nat \<Rightarrow> ennreal"]]
```
```   357
```
```   358 lemma e2ennreal_neg: "x \<le> 0 \<Longrightarrow> e2ennreal x = 0"
```
```   359   unfolding zero_ennreal_def e2ennreal_def by (simp add: max_absorb1)
```
```   360
```
```   361 lemma e2ennreal_mono: "x \<le> y \<Longrightarrow> e2ennreal x \<le> e2ennreal y"
```
```   362   by (cases "0 \<le> x" "0 \<le> y" rule: bool.exhaust[case_product bool.exhaust])
```
```   363      (auto simp: e2ennreal_neg less_eq_ennreal.abs_eq eq_onp_def)
```
```   364
```
```   365 lemma enn2ereal_nonneg[simp]: "0 \<le> enn2ereal x"
```
```   366   using ennreal.enn2ereal[of x] by simp
```
```   367
```
```   368 lemma ereal_ennreal_cases:
```
```   369   obtains b where "0 \<le> a" "a = enn2ereal b" | "a < 0"
```
```   370   using e2ennreal'_inverse[of a, symmetric] by (cases "0 \<le> a") (auto intro: enn2ereal_nonneg)
```
```   371
```
```   372 lemma rel_fun_liminf[transfer_rule]: "rel_fun (rel_fun op = pcr_ennreal) pcr_ennreal liminf liminf"
```
```   373 proof -
```
```   374   have "rel_fun (rel_fun op = pcr_ennreal) pcr_ennreal (\<lambda>x. sup 0 (liminf x)) liminf"
```
```   375     unfolding liminf_SUP_INF[abs_def] by (transfer_prover_start, transfer_step+; simp)
```
```   376   then show ?thesis
```
```   377     apply (subst (asm) (2) rel_fun_def)
```
```   378     apply (subst (2) rel_fun_def)
```
```   379     apply (auto simp: comp_def max.absorb2 Liminf_bounded rel_fun_eq_pcr_ennreal)
```
```   380     done
```
```   381 qed
```
```   382
```
```   383 lemma rel_fun_limsup[transfer_rule]: "rel_fun (rel_fun op = pcr_ennreal) pcr_ennreal limsup limsup"
```
```   384 proof -
```
```   385   have "rel_fun (rel_fun op = pcr_ennreal) pcr_ennreal (\<lambda>x. INF n. sup 0 (SUP i:{n..}. x i)) limsup"
```
```   386     unfolding limsup_INF_SUP[abs_def] by (transfer_prover_start, transfer_step+; simp)
```
```   387   then show ?thesis
```
```   388     unfolding limsup_INF_SUP[abs_def]
```
```   389     apply (subst (asm) (2) rel_fun_def)
```
```   390     apply (subst (2) rel_fun_def)
```
```   391     apply (auto simp: comp_def max.absorb2 Sup_upper2 rel_fun_eq_pcr_ennreal)
```
```   392     apply (subst (asm) max.absorb2)
```
```   393     apply (rule SUP_upper2)
```
```   394     apply auto
```
```   395     done
```
```   396 qed
```
```   397
```
```   398 lemma sum_enn2ereal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. enn2ereal (f i)) = enn2ereal (sum f I)"
```
```   399   by (induction I rule: infinite_finite_induct) (auto simp: sum_nonneg zero_ennreal.rep_eq plus_ennreal.rep_eq)
```
```   400
```
```   401 lemma transfer_e2ennreal_sum [transfer_rule]:
```
```   402   "rel_fun (rel_fun op = pcr_ennreal) (rel_fun op = pcr_ennreal) sum sum"
```
```   403   by (auto intro!: rel_funI simp: rel_fun_eq_pcr_ennreal comp_def)
```
```   404
```
```   405 lemma enn2ereal_of_nat[simp]: "enn2ereal (of_nat n) = ereal n"
```
```   406   by (induction n) (auto simp: zero_ennreal.rep_eq one_ennreal.rep_eq plus_ennreal.rep_eq)
```
```   407
```
```   408 lemma enn2ereal_numeral[simp]: "enn2ereal (numeral a) = numeral a"
```
```   409   apply (subst of_nat_numeral[of a, symmetric])
```
```   410   apply (subst enn2ereal_of_nat)
```
```   411   apply simp
```
```   412   done
```
```   413
```
```   414 lemma transfer_numeral[transfer_rule]: "pcr_ennreal (numeral a) (numeral a)"
```
```   415   unfolding cr_ennreal_def pcr_ennreal_def by auto
```
```   416
```
```   417 subsection \<open>Cancellation simprocs\<close>
```
```   418
```
```   419 lemma ennreal_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::ennreal) \<or> b = c"
```
```   420   unfolding infinity_ennreal_def by transfer (simp add: top_ereal_def ereal_add_cancel_left)
```
```   421
```
```   422 lemma ennreal_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::ennreal) \<or> b \<le> c"
```
```   423   unfolding infinity_ennreal_def by transfer (simp add: ereal_add_le_add_iff top_ereal_def disj_commute)
```
```   424
```
```   425 lemma ereal_add_left_cancel_less:
```
```   426   fixes a b c :: ereal
```
```   427   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a + b < a + c \<longleftrightarrow> a \<noteq> \<infinity> \<and> b < c"
```
```   428   by (cases a b c rule: ereal3_cases) auto
```
```   429
```
```   430 lemma ennreal_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::ennreal) \<and> b < c"
```
```   431   unfolding infinity_ennreal_def
```
```   432   by transfer (simp add: top_ereal_def ereal_add_left_cancel_less)
```
```   433
```
```   434 ML \<open>
```
```   435 structure Cancel_Ennreal_Common =
```
```   436 struct
```
```   437   (* copied from src/HOL/Tools/nat_numeral_simprocs.ML *)
```
```   438   fun find_first_t _    _ []         = raise TERM("find_first_t", [])
```
```   439     | find_first_t past u (t::terms) =
```
```   440           if u aconv t then (rev past @ terms)
```
```   441           else find_first_t (t::past) u terms
```
```   442
```
```   443   fun dest_summing (Const (@{const_name Groups.plus}, _) \$ t \$ u, ts) =
```
```   444         dest_summing (t, dest_summing (u, ts))
```
```   445     | dest_summing (t, ts) = t :: ts
```
```   446
```
```   447   val mk_sum = Arith_Data.long_mk_sum
```
```   448   fun dest_sum t = dest_summing (t, [])
```
```   449   val find_first = find_first_t []
```
```   450   val trans_tac = Numeral_Simprocs.trans_tac
```
```   451   val norm_ss =
```
```   452     simpset_of (put_simpset HOL_basic_ss @{context}
```
```   453       addsimps @{thms ac_simps add_0_left add_0_right})
```
```   454   fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
```
```   455   fun simplify_meta_eq ctxt cancel_th th =
```
```   456     Arith_Data.simplify_meta_eq [] ctxt
```
```   457       ([th, cancel_th] MRS trans)
```
```   458   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
```
```   459 end
```
```   460
```
```   461 structure Eq_Ennreal_Cancel = ExtractCommonTermFun
```
```   462 (open Cancel_Ennreal_Common
```
```   463   val mk_bal = HOLogic.mk_eq
```
```   464   val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} @{typ ennreal}
```
```   465   fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel}
```
```   466 )
```
```   467
```
```   468 structure Le_Ennreal_Cancel = ExtractCommonTermFun
```
```   469 (open Cancel_Ennreal_Common
```
```   470   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
```
```   471   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} @{typ ennreal}
```
```   472   fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel_le}
```
```   473 )
```
```   474
```
```   475 structure Less_Ennreal_Cancel = ExtractCommonTermFun
```
```   476 (open Cancel_Ennreal_Common
```
```   477   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
```
```   478   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} @{typ ennreal}
```
```   479   fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel_less}
```
```   480 )
```
```   481 \<close>
```
```   482
```
```   483 simproc_setup ennreal_eq_cancel
```
```   484   ("(l::ennreal) + m = n" | "(l::ennreal) = m + n") =
```
```   485   \<open>fn phi => fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
```
```   486
```
```   487 simproc_setup ennreal_le_cancel
```
```   488   ("(l::ennreal) + m \<le> n" | "(l::ennreal) \<le> m + n") =
```
```   489   \<open>fn phi => fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
```
```   490
```
```   491 simproc_setup ennreal_less_cancel
```
```   492   ("(l::ennreal) + m < n" | "(l::ennreal) < m + n") =
```
```   493   \<open>fn phi => fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
```
```   494
```
```   495
```
```   496 subsection \<open>Order with top\<close>
```
```   497
```
```   498 lemma ennreal_zero_less_top[simp]: "0 < (top::ennreal)"
```
```   499   by transfer (simp add: top_ereal_def)
```
```   500
```
```   501 lemma ennreal_one_less_top[simp]: "1 < (top::ennreal)"
```
```   502   by transfer (simp add: top_ereal_def)
```
```   503
```
```   504 lemma ennreal_zero_neq_top[simp]: "0 \<noteq> (top::ennreal)"
```
```   505   by transfer (simp add: top_ereal_def)
```
```   506
```
```   507 lemma ennreal_top_neq_zero[simp]: "(top::ennreal) \<noteq> 0"
```
```   508   by transfer (simp add: top_ereal_def)
```
```   509
```
```   510 lemma ennreal_top_neq_one[simp]: "top \<noteq> (1::ennreal)"
```
```   511   by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
```
```   512
```
```   513 lemma ennreal_one_neq_top[simp]: "1 \<noteq> (top::ennreal)"
```
```   514   by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
```
```   515
```
```   516 lemma ennreal_add_less_top[simp]:
```
```   517   fixes a b :: ennreal
```
```   518   shows "a + b < top \<longleftrightarrow> a < top \<and> b < top"
```
```   519   by transfer (auto simp: top_ereal_def)
```
```   520
```
```   521 lemma ennreal_add_eq_top[simp]:
```
```   522   fixes a b :: ennreal
```
```   523   shows "a + b = top \<longleftrightarrow> a = top \<or> b = top"
```
```   524   by transfer (auto simp: top_ereal_def)
```
```   525
```
```   526 lemma ennreal_sum_less_top[simp]:
```
```   527   fixes f :: "'a \<Rightarrow> ennreal"
```
```   528   shows "finite I \<Longrightarrow> (\<Sum>i\<in>I. f i) < top \<longleftrightarrow> (\<forall>i\<in>I. f i < top)"
```
```   529   by (induction I rule: finite_induct) auto
```
```   530
```
```   531 lemma ennreal_sum_eq_top[simp]:
```
```   532   fixes f :: "'a \<Rightarrow> ennreal"
```
```   533   shows "finite I \<Longrightarrow> (\<Sum>i\<in>I. f i) = top \<longleftrightarrow> (\<exists>i\<in>I. f i = top)"
```
```   534   by (induction I rule: finite_induct) auto
```
```   535
```
```   536 lemma ennreal_mult_eq_top_iff:
```
```   537   fixes a b :: ennreal
```
```   538   shows "a * b = top \<longleftrightarrow> (a = top \<and> b \<noteq> 0) \<or> (b = top \<and> a \<noteq> 0)"
```
```   539   by transfer (auto simp: top_ereal_def)
```
```   540
```
```   541 lemma ennreal_top_eq_mult_iff:
```
```   542   fixes a b :: ennreal
```
```   543   shows "top = a * b \<longleftrightarrow> (a = top \<and> b \<noteq> 0) \<or> (b = top \<and> a \<noteq> 0)"
```
```   544   using ennreal_mult_eq_top_iff[of a b] by auto
```
```   545
```
```   546 lemma ennreal_mult_less_top:
```
```   547   fixes a b :: ennreal
```
```   548   shows "a * b < top \<longleftrightarrow> (a = 0 \<or> b = 0 \<or> (a < top \<and> b < top))"
```
```   549   by transfer (auto simp add: top_ereal_def)
```
```   550
```
```   551 lemma top_power_ennreal: "top ^ n = (if n = 0 then 1 else top :: ennreal)"
```
```   552   by (induction n) (simp_all add: ennreal_mult_eq_top_iff)
```
```   553
```
```   554 lemma ennreal_prod_eq_0[simp]:
```
```   555   fixes f :: "'a \<Rightarrow> ennreal"
```
```   556   shows "(prod f A = 0) = (finite A \<and> (\<exists>i\<in>A. f i = 0))"
```
```   557   by (induction A rule: infinite_finite_induct) auto
```
```   558
```
```   559 lemma ennreal_prod_eq_top:
```
```   560   fixes f :: "'a \<Rightarrow> ennreal"
```
```   561   shows "(\<Prod>i\<in>I. f i) = top \<longleftrightarrow> (finite I \<and> ((\<forall>i\<in>I. f i \<noteq> 0) \<and> (\<exists>i\<in>I. f i = top)))"
```
```   562   by (induction I rule: infinite_finite_induct) (auto simp: ennreal_mult_eq_top_iff)
```
```   563
```
```   564 lemma ennreal_top_mult: "top * a = (if a = 0 then 0 else top :: ennreal)"
```
```   565   by (simp add: ennreal_mult_eq_top_iff)
```
```   566
```
```   567 lemma ennreal_mult_top: "a * top = (if a = 0 then 0 else top :: ennreal)"
```
```   568   by (simp add: ennreal_mult_eq_top_iff)
```
```   569
```
```   570 lemma enn2ereal_eq_top_iff[simp]: "enn2ereal x = \<infinity> \<longleftrightarrow> x = top"
```
```   571   by transfer (simp add: top_ereal_def)
```
```   572
```
```   573 lemma enn2ereal_top: "enn2ereal top = \<infinity>"
```
```   574   by transfer (simp add: top_ereal_def)
```
```   575
```
```   576 lemma e2ennreal_infty: "e2ennreal \<infinity> = top"
```
```   577   by (simp add: top_ennreal.abs_eq top_ereal_def)
```
```   578
```
```   579 lemma ennreal_top_minus[simp]: "top - x = (top::ennreal)"
```
```   580   by transfer (auto simp: top_ereal_def max_def)
```
```   581
```
```   582 lemma minus_top_ennreal: "x - top = (if x = top then top else 0:: ennreal)"
```
```   583   apply transfer
```
```   584   subgoal for x
```
```   585     by (cases x) (auto simp: top_ereal_def max_def)
```
```   586   done
```
```   587
```
```   588 lemma bot_ennreal: "bot = (0::ennreal)"
```
```   589   by transfer rule
```
```   590
```
```   591 lemma ennreal_of_nat_neq_top[simp]: "of_nat i \<noteq> (top::ennreal)"
```
```   592   by (induction i) auto
```
```   593
```
```   594 lemma numeral_eq_of_nat: "(numeral a::ennreal) = of_nat (numeral a)"
```
```   595   by simp
```
```   596
```
```   597 lemma of_nat_less_top: "of_nat i < (top::ennreal)"
```
```   598   using less_le_trans[of "of_nat i" "of_nat (Suc i)" "top::ennreal"]
```
```   599   by simp
```
```   600
```
```   601 lemma top_neq_numeral[simp]: "top \<noteq> (numeral i::ennreal)"
```
```   602   using of_nat_less_top[of "numeral i"] by simp
```
```   603
```
```   604 lemma ennreal_numeral_less_top[simp]: "numeral i < (top::ennreal)"
```
```   605   using of_nat_less_top[of "numeral i"] by simp
```
```   606
```
```   607 lemma ennreal_add_bot[simp]: "bot + x = (x::ennreal)"
```
```   608   by transfer simp
```
```   609
```
```   610 instance ennreal :: semiring_char_0
```
```   611 proof (standard, safe intro!: linorder_injI)
```
```   612   have *: "1 + of_nat k \<noteq> (0::ennreal)" for k
```
```   613     using add_pos_nonneg[OF zero_less_one, of "of_nat k :: ennreal"] by auto
```
```   614   fix x y :: nat assume "x < y" "of_nat x = (of_nat y::ennreal)" then show False
```
```   615     by (auto simp add: less_iff_Suc_add *)
```
```   616 qed
```
```   617
```
```   618 subsection \<open>Arithmetic\<close>
```
```   619
```
```   620 lemma ennreal_minus_zero[simp]: "a - (0::ennreal) = a"
```
```   621   by transfer (auto simp: max_def)
```
```   622
```
```   623 lemma ennreal_add_diff_cancel_right[simp]:
```
```   624   fixes x y z :: ennreal shows "y \<noteq> top \<Longrightarrow> (x + y) - y = x"
```
```   625   apply transfer
```
```   626   subgoal for x y
```
```   627     apply (cases x y rule: ereal2_cases)
```
```   628     apply (auto split: split_max simp: top_ereal_def)
```
```   629     done
```
```   630   done
```
```   631
```
```   632 lemma ennreal_add_diff_cancel_left[simp]:
```
```   633   fixes x y z :: ennreal shows "y \<noteq> top \<Longrightarrow> (y + x) - y = x"
```
```   634   by (simp add: add.commute)
```
```   635
```
```   636 lemma
```
```   637   fixes a b :: ennreal
```
```   638   shows "a - b = 0 \<Longrightarrow> a \<le> b"
```
```   639   apply transfer
```
```   640   subgoal for a b
```
```   641     apply (cases a b rule: ereal2_cases)
```
```   642     apply (auto simp: not_le max_def split: if_splits)
```
```   643     done
```
```   644   done
```
```   645
```
```   646 lemma ennreal_minus_cancel:
```
```   647   fixes a b c :: ennreal
```
```   648   shows "c \<noteq> top \<Longrightarrow> a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a = c - b \<Longrightarrow> a = b"
```
```   649   apply transfer
```
```   650   subgoal for a b c
```
```   651     by (cases a b c rule: ereal3_cases)
```
```   652        (auto simp: top_ereal_def max_def split: if_splits)
```
```   653   done
```
```   654
```
```   655 lemma sup_const_add_ennreal:
```
```   656   fixes a b c :: "ennreal"
```
```   657   shows "sup (c + a) (c + b) = c + sup a b"
```
```   658   apply transfer
```
```   659   subgoal for a b c
```
```   660     apply (cases a b c rule: ereal3_cases)
```
```   661     apply (auto simp: ereal_max[symmetric] simp del: ereal_max)
```
```   662     apply (auto simp: top_ereal_def[symmetric] sup_ereal_def[symmetric]
```
```   663                 simp del: sup_ereal_def)
```
```   664     apply (auto simp add: top_ereal_def)
```
```   665     done
```
```   666   done
```
```   667
```
```   668 lemma ennreal_diff_add_assoc:
```
```   669   fixes a b c :: ennreal
```
```   670   shows "a \<le> b \<Longrightarrow> c + b - a = c + (b - a)"
```
```   671   apply transfer
```
```   672   subgoal for a b c
```
```   673     by (cases a b c rule: ereal3_cases) (auto simp: field_simps max_absorb2)
```
```   674   done
```
```   675
```
```   676 lemma mult_divide_eq_ennreal:
```
```   677   fixes a b :: ennreal
```
```   678   shows "b \<noteq> 0 \<Longrightarrow> b \<noteq> top \<Longrightarrow> (a * b) / b = a"
```
```   679   unfolding divide_ennreal_def
```
```   680   apply transfer
```
```   681   apply (subst mult.assoc)
```
```   682   apply (simp add: top_ereal_def divide_ereal_def[symmetric])
```
```   683   done
```
```   684
```
```   685 lemma divide_mult_eq: "a \<noteq> 0 \<Longrightarrow> a \<noteq> \<infinity> \<Longrightarrow> x * a / (b * a) = x / (b::ennreal)"
```
```   686   unfolding divide_ennreal_def infinity_ennreal_def
```
```   687   apply transfer
```
```   688   subgoal for a b c
```
```   689     apply (cases a b c rule: ereal3_cases)
```
```   690     apply (auto simp: top_ereal_def)
```
```   691     done
```
```   692   done
```
```   693
```
```   694 lemma ennreal_mult_divide_eq:
```
```   695   fixes a b :: ennreal
```
```   696   shows "b \<noteq> 0 \<Longrightarrow> b \<noteq> top \<Longrightarrow> (a * b) / b = a"
```
```   697   unfolding divide_ennreal_def
```
```   698   apply transfer
```
```   699   apply (subst mult.assoc)
```
```   700   apply (simp add: top_ereal_def divide_ereal_def[symmetric])
```
```   701   done
```
```   702
```
```   703 lemma ennreal_add_diff_cancel:
```
```   704   fixes a b :: ennreal
```
```   705   shows "b \<noteq> \<infinity> \<Longrightarrow> (a + b) - b = a"
```
```   706   unfolding infinity_ennreal_def
```
```   707   by transfer (simp add: max_absorb2 top_ereal_def ereal_add_diff_cancel)
```
```   708
```
```   709 lemma ennreal_minus_eq_0:
```
```   710   "a - b = 0 \<Longrightarrow> a \<le> (b::ennreal)"
```
```   711   apply transfer
```
```   712   subgoal for a b
```
```   713     apply (cases a b rule: ereal2_cases)
```
```   714     apply (auto simp: zero_ereal_def ereal_max[symmetric] max.absorb2 simp del: ereal_max)
```
```   715     done
```
```   716   done
```
```   717
```
```   718 lemma ennreal_mono_minus_cancel:
```
```   719   fixes a b c :: ennreal
```
```   720   shows "a - b \<le> a - c \<Longrightarrow> a < top \<Longrightarrow> b \<le> a \<Longrightarrow> c \<le> a \<Longrightarrow> c \<le> b"
```
```   721   by transfer
```
```   722      (auto simp add: max.absorb2 ereal_diff_positive top_ereal_def dest: ereal_mono_minus_cancel)
```
```   723
```
```   724 lemma ennreal_mono_minus:
```
```   725   fixes a b c :: ennreal
```
```   726   shows "c \<le> b \<Longrightarrow> a - b \<le> a - c"
```
```   727   apply transfer
```
```   728   apply (rule max.mono)
```
```   729   apply simp
```
```   730   subgoal for a b c
```
```   731     by (cases a b c rule: ereal3_cases) auto
```
```   732   done
```
```   733
```
```   734 lemma ennreal_minus_pos_iff:
```
```   735   fixes a b :: ennreal
```
```   736   shows "a < top \<or> b < top \<Longrightarrow> 0 < a - b \<Longrightarrow> b < a"
```
```   737   apply transfer
```
```   738   subgoal for a b
```
```   739     by (cases a b rule: ereal2_cases) (auto simp: less_max_iff_disj)
```
```   740   done
```
```   741
```
```   742 lemma ennreal_inverse_top[simp]: "inverse top = (0::ennreal)"
```
```   743   by transfer (simp add: top_ereal_def ereal_inverse_eq_0)
```
```   744
```
```   745 lemma ennreal_inverse_zero[simp]: "inverse 0 = (top::ennreal)"
```
```   746   by transfer (simp add: top_ereal_def ereal_inverse_eq_0)
```
```   747
```
```   748 lemma ennreal_top_divide: "top / (x::ennreal) = (if x = top then 0 else top)"
```
```   749   unfolding divide_ennreal_def
```
```   750   by transfer (simp add: top_ereal_def ereal_inverse_eq_0 ereal_0_gt_inverse)
```
```   751
```
```   752 lemma ennreal_zero_divide[simp]: "0 / (x::ennreal) = 0"
```
```   753   by (simp add: divide_ennreal_def)
```
```   754
```
```   755 lemma ennreal_divide_zero[simp]: "x / (0::ennreal) = (if x = 0 then 0 else top)"
```
```   756   by (simp add: divide_ennreal_def ennreal_mult_top)
```
```   757
```
```   758 lemma ennreal_divide_top[simp]: "x / (top::ennreal) = 0"
```
```   759   by (simp add: divide_ennreal_def ennreal_top_mult)
```
```   760
```
```   761 lemma ennreal_times_divide: "a * (b / c) = a * b / (c::ennreal)"
```
```   762   unfolding divide_ennreal_def
```
```   763   by transfer (simp add: divide_ereal_def[symmetric] ereal_times_divide_eq)
```
```   764
```
```   765 lemma ennreal_zero_less_divide: "0 < a / b \<longleftrightarrow> (0 < a \<and> b < (top::ennreal))"
```
```   766   unfolding divide_ennreal_def
```
```   767   by transfer (auto simp: ereal_zero_less_0_iff top_ereal_def ereal_0_gt_inverse)
```
```   768
```
```   769 lemma divide_right_mono_ennreal:
```
```   770   fixes a b c :: ennreal
```
```   771   shows "a \<le> b \<Longrightarrow> a / c \<le> b / c"
```
```   772   unfolding divide_ennreal_def by (intro mult_mono) auto
```
```   773
```
```   774 lemma ennreal_mult_strict_right_mono: "(a::ennreal) < c \<Longrightarrow> 0 < b \<Longrightarrow> b < top \<Longrightarrow> a * b < c * b"
```
```   775   by transfer (auto intro!: ereal_mult_strict_right_mono)
```
```   776
```
```   777 lemma ennreal_indicator_less[simp]:
```
```   778   "indicator A x \<le> (indicator B x::ennreal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
```
```   779   by (simp add: indicator_def not_le)
```
```   780
```
```   781 lemma ennreal_inverse_positive: "0 < inverse x \<longleftrightarrow> (x::ennreal) \<noteq> top"
```
```   782   by transfer (simp add: ereal_0_gt_inverse top_ereal_def)
```
```   783
```
```   784 lemma ennreal_inverse_mult': "((0 < b \<or> a < top) \<and> (0 < a \<or> b < top)) \<Longrightarrow> inverse (a * b::ennreal) = inverse a * inverse b"
```
```   785   apply transfer
```
```   786   subgoal for a b
```
```   787     by (cases a b rule: ereal2_cases) (auto simp: top_ereal_def)
```
```   788   done
```
```   789
```
```   790 lemma ennreal_inverse_mult: "a < top \<Longrightarrow> b < top \<Longrightarrow> inverse (a * b::ennreal) = inverse a * inverse b"
```
```   791   apply transfer
```
```   792   subgoal for a b
```
```   793     by (cases a b rule: ereal2_cases) (auto simp: top_ereal_def)
```
```   794   done
```
```   795
```
```   796 lemma ennreal_inverse_1[simp]: "inverse (1::ennreal) = 1"
```
```   797   by transfer simp
```
```   798
```
```   799 lemma ennreal_inverse_eq_0_iff[simp]: "inverse (a::ennreal) = 0 \<longleftrightarrow> a = top"
```
```   800   by transfer (simp add: ereal_inverse_eq_0 top_ereal_def)
```
```   801
```
```   802 lemma ennreal_inverse_eq_top_iff[simp]: "inverse (a::ennreal) = top \<longleftrightarrow> a = 0"
```
```   803   by transfer (simp add: top_ereal_def)
```
```   804
```
```   805 lemma ennreal_divide_eq_0_iff[simp]: "(a::ennreal) / b = 0 \<longleftrightarrow> (a = 0 \<or> b = top)"
```
```   806   by (simp add: divide_ennreal_def)
```
```   807
```
```   808 lemma ennreal_divide_eq_top_iff: "(a::ennreal) / b = top \<longleftrightarrow> ((a \<noteq> 0 \<and> b = 0) \<or> (a = top \<and> b \<noteq> top))"
```
```   809   by (auto simp add: divide_ennreal_def ennreal_mult_eq_top_iff)
```
```   810
```
```   811 lemma one_divide_one_divide_ennreal[simp]: "1 / (1 / c) = (c::ennreal)"
```
```   812   including ennreal.lifting
```
```   813   unfolding divide_ennreal_def
```
```   814   by transfer auto
```
```   815
```
```   816 lemma ennreal_mult_left_cong:
```
```   817   "((a::ennreal) \<noteq> 0 \<Longrightarrow> b = c) \<Longrightarrow> a * b = a * c"
```
```   818   by (cases "a = 0") simp_all
```
```   819
```
```   820 lemma ennreal_mult_right_cong:
```
```   821   "((a::ennreal) \<noteq> 0 \<Longrightarrow> b = c) \<Longrightarrow> b * a = c * a"
```
```   822   by (cases "a = 0") simp_all
```
```   823
```
```   824 lemma ennreal_zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < (b::ennreal)"
```
```   825   by transfer (auto simp add: ereal_zero_less_0_iff le_less)
```
```   826
```
```   827 lemma less_diff_eq_ennreal:
```
```   828   fixes a b c :: ennreal
```
```   829   shows "b < top \<or> c < top \<Longrightarrow> a < b - c \<longleftrightarrow> a + c < b"
```
```   830   apply transfer
```
```   831   subgoal for a b c
```
```   832     by (cases a b c rule: ereal3_cases) (auto split: split_max)
```
```   833   done
```
```   834
```
```   835 lemma diff_add_cancel_ennreal:
```
```   836   fixes a b :: ennreal shows "a \<le> b \<Longrightarrow> b - a + a = b"
```
```   837   unfolding infinity_ennreal_def
```
```   838   apply transfer
```
```   839   subgoal for a b
```
```   840     by (cases a b rule: ereal2_cases) (auto simp: max_absorb2)
```
```   841   done
```
```   842
```
```   843 lemma ennreal_diff_self[simp]: "a \<noteq> top \<Longrightarrow> a - a = (0::ennreal)"
```
```   844   by transfer (simp add: top_ereal_def)
```
```   845
```
```   846 lemma ennreal_minus_mono:
```
```   847   fixes a b c :: ennreal
```
```   848   shows "a \<le> c \<Longrightarrow> d \<le> b \<Longrightarrow> a - b \<le> c - d"
```
```   849   apply transfer
```
```   850   apply (rule max.mono)
```
```   851   apply simp
```
```   852   subgoal for a b c d
```
```   853     by (cases a b c d rule: ereal3_cases[case_product ereal_cases]) auto
```
```   854   done
```
```   855
```
```   856 lemma ennreal_minus_eq_top[simp]: "a - (b::ennreal) = top \<longleftrightarrow> a = top"
```
```   857   by transfer (auto simp: top_ereal_def max.absorb2 ereal_minus_eq_PInfty_iff split: split_max)
```
```   858
```
```   859 lemma ennreal_divide_self[simp]: "a \<noteq> 0 \<Longrightarrow> a < top \<Longrightarrow> a / a = (1::ennreal)"
```
```   860   unfolding divide_ennreal_def
```
```   861   apply transfer
```
```   862   subgoal for a
```
```   863     by (cases a) (auto simp: top_ereal_def)
```
```   864   done
```
```   865
```
```   866 subsection \<open>Coercion from @{typ real} to @{typ ennreal}\<close>
```
```   867
```
```   868 lift_definition ennreal :: "real \<Rightarrow> ennreal" is "sup 0 \<circ> ereal"
```
```   869   by simp
```
```   870
```
```   871 declare [[coercion ennreal]]
```
```   872
```
```   873 lemma ennreal_cong: "x = y \<Longrightarrow> ennreal x = ennreal y" by simp
```
```   874
```
```   875 lemma ennreal_cases[cases type: ennreal]:
```
```   876   fixes x :: ennreal
```
```   877   obtains (real) r :: real where "0 \<le> r" "x = ennreal r" | (top) "x = top"
```
```   878   apply transfer
```
```   879   subgoal for x thesis
```
```   880     by (cases x) (auto simp: max.absorb2 top_ereal_def)
```
```   881   done
```
```   882
```
```   883 lemmas ennreal2_cases = ennreal_cases[case_product ennreal_cases]
```
```   884 lemmas ennreal3_cases = ennreal_cases[case_product ennreal2_cases]
```
```   885
```
```   886 lemma ennreal_neq_top[simp]: "ennreal r \<noteq> top"
```
```   887   by transfer (simp add: top_ereal_def zero_ereal_def ereal_max[symmetric] del: ereal_max)
```
```   888
```
```   889 lemma top_neq_ennreal[simp]: "top \<noteq> ennreal r"
```
```   890   using ennreal_neq_top[of r] by (auto simp del: ennreal_neq_top)
```
```   891
```
```   892 lemma ennreal_less_top[simp]: "ennreal x < top"
```
```   893   by transfer (simp add: top_ereal_def max_def)
```
```   894
```
```   895 lemma ennreal_neg: "x \<le> 0 \<Longrightarrow> ennreal x = 0"
```
```   896   by transfer (simp add: max.absorb1)
```
```   897
```
```   898 lemma ennreal_inj[simp]:
```
```   899   "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal a = ennreal b \<longleftrightarrow> a = b"
```
```   900   by (transfer fixing: a b) (auto simp: max_absorb2)
```
```   901
```
```   902 lemma ennreal_le_iff[simp]: "0 \<le> y \<Longrightarrow> ennreal x \<le> ennreal y \<longleftrightarrow> x \<le> y"
```
```   903   by (auto simp: ennreal_def zero_ereal_def less_eq_ennreal.abs_eq eq_onp_def split: split_max)
```
```   904
```
```   905 lemma le_ennreal_iff: "0 \<le> r \<Longrightarrow> x \<le> ennreal r \<longleftrightarrow> (\<exists>q\<ge>0. x = ennreal q \<and> q \<le> r)"
```
```   906   by (cases x) (auto simp: top_unique)
```
```   907
```
```   908 lemma ennreal_less_iff: "0 \<le> r \<Longrightarrow> ennreal r < ennreal q \<longleftrightarrow> r < q"
```
```   909   unfolding not_le[symmetric] by auto
```
```   910
```
```   911 lemma ennreal_eq_zero_iff[simp]: "0 \<le> x \<Longrightarrow> ennreal x = 0 \<longleftrightarrow> x = 0"
```
```   912   by transfer (auto simp: max_absorb2)
```
```   913
```
```   914 lemma ennreal_less_zero_iff[simp]: "0 < ennreal x \<longleftrightarrow> 0 < x"
```
```   915   by transfer (auto simp: max_def)
```
```   916
```
```   917 lemma ennreal_lessI: "0 < q \<Longrightarrow> r < q \<Longrightarrow> ennreal r < ennreal q"
```
```   918   by (cases "0 \<le> r") (auto simp: ennreal_less_iff ennreal_neg)
```
```   919
```
```   920 lemma ennreal_leI: "x \<le> y \<Longrightarrow> ennreal x \<le> ennreal y"
```
```   921   by (cases "0 \<le> y") (auto simp: ennreal_neg)
```
```   922
```
```   923 lemma enn2ereal_ennreal[simp]: "0 \<le> x \<Longrightarrow> enn2ereal (ennreal x) = x"
```
```   924   by transfer (simp add: max_absorb2)
```
```   925
```
```   926 lemma e2ennreal_enn2ereal[simp]: "e2ennreal (enn2ereal x) = x"
```
```   927   by (simp add: e2ennreal_def max_absorb2 ennreal.enn2ereal_inverse)
```
```   928
```
```   929 lemma ennreal_0[simp]: "ennreal 0 = 0"
```
```   930   by (simp add: ennreal_def max.absorb1 zero_ennreal.abs_eq)
```
```   931
```
```   932 lemma ennreal_1[simp]: "ennreal 1 = 1"
```
```   933   by transfer (simp add: max_absorb2)
```
```   934
```
```   935 lemma ennreal_eq_0_iff: "ennreal x = 0 \<longleftrightarrow> x \<le> 0"
```
```   936   by (cases "0 \<le> x") (auto simp: ennreal_neg)
```
```   937
```
```   938 lemma ennreal_le_iff2: "ennreal x \<le> ennreal y \<longleftrightarrow> ((0 \<le> y \<and> x \<le> y) \<or> (x \<le> 0 \<and> y \<le> 0))"
```
```   939   by (cases "0 \<le> y") (auto simp: ennreal_eq_0_iff ennreal_neg)
```
```   940
```
```   941 lemma ennreal_eq_1[simp]: "ennreal x = 1 \<longleftrightarrow> x = 1"
```
```   942   by (cases "0 \<le> x")
```
```   943      (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
```
```   944
```
```   945 lemma ennreal_le_1[simp]: "ennreal x \<le> 1 \<longleftrightarrow> x \<le> 1"
```
```   946   by (cases "0 \<le> x")
```
```   947      (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
```
```   948
```
```   949 lemma ennreal_ge_1[simp]: "ennreal x \<ge> 1 \<longleftrightarrow> x \<ge> 1"
```
```   950   by (cases "0 \<le> x")
```
```   951      (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
```
```   952
```
```   953 lemma one_less_ennreal[simp]: "1 < ennreal x \<longleftrightarrow> 1 < x"
```
```   954   by transfer (auto simp: max.absorb2 less_max_iff_disj)
```
```   955
```
```   956 lemma ennreal_plus[simp]:
```
```   957   "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a + b) = ennreal a + ennreal b"
```
```   958   by (transfer fixing: a b) (auto simp: max_absorb2)
```
```   959
```
```   960 lemma sum_ennreal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. ennreal (f i)) = ennreal (sum f I)"
```
```   961   by (induction I rule: infinite_finite_induct) (auto simp: sum_nonneg)
```
```   962
```
```   963 lemma sum_list_ennreal[simp]:
```
```   964   assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<ge> 0"
```
```   965   shows   "sum_list (map (\<lambda>x. ennreal (f x)) xs) = ennreal (sum_list (map f xs))"
```
```   966 using assms
```
```   967 proof (induction xs)
```
```   968   case (Cons x xs)
```
```   969   from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (sum_list (map f xs))"
```
```   970     by simp
```
```   971   also from Cons.prems have "\<dots> = ennreal (f x + sum_list (map f xs))"
```
```   972     by (intro ennreal_plus [symmetric] sum_list_nonneg) auto
```
```   973   finally show ?case by simp
```
```   974 qed simp_all
```
```   975
```
```   976 lemma ennreal_of_nat_eq_real_of_nat: "of_nat i = ennreal (of_nat i)"
```
```   977   by (induction i) simp_all
```
```   978
```
```   979 lemma of_nat_le_ennreal_iff[simp]: "0 \<le> r \<Longrightarrow> of_nat i \<le> ennreal r \<longleftrightarrow> of_nat i \<le> r"
```
```   980   by (simp add: ennreal_of_nat_eq_real_of_nat)
```
```   981
```
```   982 lemma ennreal_le_of_nat_iff[simp]: "ennreal r \<le> of_nat i \<longleftrightarrow> r \<le> of_nat i"
```
```   983   by (simp add: ennreal_of_nat_eq_real_of_nat)
```
```   984
```
```   985 lemma ennreal_indicator: "ennreal (indicator A x) = indicator A x"
```
```   986   by (auto split: split_indicator)
```
```   987
```
```   988 lemma ennreal_numeral[simp]: "ennreal (numeral n) = numeral n"
```
```   989   using ennreal_of_nat_eq_real_of_nat[of "numeral n"] by simp
```
```   990
```
```   991 lemma min_ennreal: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> min (ennreal x) (ennreal y) = ennreal (min x y)"
```
```   992   by (auto split: split_min)
```
```   993
```
```   994 lemma ennreal_half[simp]: "ennreal (1/2) = inverse 2"
```
```   995   by transfer (simp add: max.absorb2)
```
```   996
```
```   997 lemma ennreal_minus: "0 \<le> q \<Longrightarrow> ennreal r - ennreal q = ennreal (r - q)"
```
```   998   by transfer
```
```   999      (simp add: max.absorb2 zero_ereal_def ereal_max[symmetric] del: ereal_max)
```
```  1000
```
```  1001 lemma ennreal_minus_top[simp]: "ennreal a - top = 0"
```
```  1002   by (simp add: minus_top_ennreal)
```
```  1003
```
```  1004 lemma ennreal_mult: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"
```
```  1005   by transfer (simp add: max_absorb2)
```
```  1006
```
```  1007 lemma ennreal_mult': "0 \<le> a \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"
```
```  1008   by (cases "0 \<le> b") (auto simp: ennreal_mult ennreal_neg mult_nonneg_nonpos)
```
```  1009
```
```  1010 lemma indicator_mult_ennreal: "indicator A x * ennreal r = ennreal (indicator A x * r)"
```
```  1011   by (simp split: split_indicator)
```
```  1012
```
```  1013 lemma ennreal_mult'': "0 \<le> b \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"
```
```  1014   by (cases "0 \<le> a") (auto simp: ennreal_mult ennreal_neg mult_nonpos_nonneg)
```
```  1015
```
```  1016 lemma numeral_mult_ennreal: "0 \<le> x \<Longrightarrow> numeral b * ennreal x = ennreal (numeral b * x)"
```
```  1017   by (simp add: ennreal_mult)
```
```  1018
```
```  1019 lemma ennreal_power: "0 \<le> r \<Longrightarrow> ennreal r ^ n = ennreal (r ^ n)"
```
```  1020   by (induction n) (auto simp: ennreal_mult)
```
```  1021
```
```  1022 lemma power_eq_top_ennreal: "x ^ n = top \<longleftrightarrow> (n \<noteq> 0 \<and> (x::ennreal) = top)"
```
```  1023   by (cases x rule: ennreal_cases)
```
```  1024      (auto simp: ennreal_power top_power_ennreal)
```
```  1025
```
```  1026 lemma inverse_ennreal: "0 < r \<Longrightarrow> inverse (ennreal r) = ennreal (inverse r)"
```
```  1027   by transfer (simp add: max.absorb2)
```
```  1028
```
```  1029 lemma divide_ennreal: "0 \<le> r \<Longrightarrow> 0 < q \<Longrightarrow> ennreal r / ennreal q = ennreal (r / q)"
```
```  1030   by (simp add: divide_ennreal_def inverse_ennreal ennreal_mult[symmetric] inverse_eq_divide)
```
```  1031
```
```  1032 lemma ennreal_inverse_power: "inverse (x ^ n :: ennreal) = inverse x ^ n"
```
```  1033 proof (cases x rule: ennreal_cases)
```
```  1034   case top with power_eq_top_ennreal[of x n] show ?thesis
```
```  1035     by (cases "n = 0") auto
```
```  1036 next
```
```  1037   case (real r) then show ?thesis
```
```  1038   proof cases
```
```  1039     assume "x = 0" then show ?thesis
```
```  1040       using power_eq_top_ennreal[of top "n - 1"]
```
```  1041       by (cases n) (auto simp: ennreal_top_mult)
```
```  1042   next
```
```  1043     assume "x \<noteq> 0"
```
```  1044     with real have "0 < r" by auto
```
```  1045     with real show ?thesis
```
```  1046       by (induction n)
```
```  1047          (auto simp add: ennreal_power ennreal_mult[symmetric] inverse_ennreal)
```
```  1048   qed
```
```  1049 qed
```
```  1050
```
```  1051 lemma ennreal_divide_numeral: "0 \<le> x \<Longrightarrow> ennreal x / numeral b = ennreal (x / numeral b)"
```
```  1052   by (subst divide_ennreal[symmetric]) auto
```
```  1053
```
```  1054 lemma prod_ennreal: "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Prod>i\<in>A. ennreal (f i)) = ennreal (prod f A)"
```
```  1055   by (induction A rule: infinite_finite_induct)
```
```  1056      (auto simp: ennreal_mult prod_nonneg)
```
```  1057
```
```  1058 lemma mult_right_ennreal_cancel: "a * ennreal c = b * ennreal c \<longleftrightarrow> (a = b \<or> c \<le> 0)"
```
```  1059   apply (cases "0 \<le> c")
```
```  1060   apply (cases a b rule: ennreal2_cases)
```
```  1061   apply (auto simp: ennreal_mult[symmetric] ennreal_neg ennreal_top_mult)
```
```  1062   done
```
```  1063
```
```  1064 lemma ennreal_le_epsilon:
```
```  1065   "(\<And>e::real. y < top \<Longrightarrow> 0 < e \<Longrightarrow> x \<le> y + ennreal e) \<Longrightarrow> x \<le> y"
```
```  1066   apply (cases y rule: ennreal_cases)
```
```  1067   apply (cases x rule: ennreal_cases)
```
```  1068   apply (auto simp del: ennreal_plus simp add: top_unique ennreal_plus[symmetric]
```
```  1069     intro: zero_less_one field_le_epsilon)
```
```  1070   done
```
```  1071
```
```  1072 lemma ennreal_rat_dense:
```
```  1073   fixes x y :: ennreal
```
```  1074   shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
```
```  1075 proof transfer
```
```  1076   fix x y :: ereal assume xy: "0 \<le> x" "0 \<le> y" "x < y"
```
```  1077   moreover
```
```  1078   from ereal_dense3[OF \<open>x < y\<close>]
```
```  1079   obtain r where r: "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
```
```  1080     by auto
```
```  1081   then have "0 \<le> r"
```
```  1082     using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto
```
```  1083   with r show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y"
```
```  1084     by (intro exI[of _ r]) (auto simp: max_absorb2)
```
```  1085 qed
```
```  1086
```
```  1087 lemma ennreal_Ex_less_of_nat: "(x::ennreal) < top \<Longrightarrow> \<exists>n. x < of_nat n"
```
```  1088   by (cases x rule: ennreal_cases)
```
```  1089      (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_less_iff reals_Archimedean2)
```
```  1090
```
```  1091 subsection \<open>Coercion from @{typ ennreal} to @{typ real}\<close>
```
```  1092
```
```  1093 definition "enn2real x = real_of_ereal (enn2ereal x)"
```
```  1094
```
```  1095 lemma enn2real_nonneg[simp]: "0 \<le> enn2real x"
```
```  1096   by (auto simp: enn2real_def intro!: real_of_ereal_pos enn2ereal_nonneg)
```
```  1097
```
```  1098 lemma enn2real_mono: "a \<le> b \<Longrightarrow> b < top \<Longrightarrow> enn2real a \<le> enn2real b"
```
```  1099   by (auto simp add: enn2real_def less_eq_ennreal.rep_eq intro!: real_of_ereal_positive_mono enn2ereal_nonneg)
```
```  1100
```
```  1101 lemma enn2real_of_nat[simp]: "enn2real (of_nat n) = n"
```
```  1102   by (auto simp: enn2real_def)
```
```  1103
```
```  1104 lemma enn2real_ennreal[simp]: "0 \<le> r \<Longrightarrow> enn2real (ennreal r) = r"
```
```  1105   by (simp add: enn2real_def)
```
```  1106
```
```  1107 lemma ennreal_enn2real[simp]: "r < top \<Longrightarrow> ennreal (enn2real r) = r"
```
```  1108   by (cases r rule: ennreal_cases) auto
```
```  1109
```
```  1110 lemma real_of_ereal_enn2ereal[simp]: "real_of_ereal (enn2ereal x) = enn2real x"
```
```  1111   by (simp add: enn2real_def)
```
```  1112
```
```  1113 lemma enn2real_top[simp]: "enn2real top = 0"
```
```  1114   unfolding enn2real_def top_ennreal.rep_eq top_ereal_def by simp
```
```  1115
```
```  1116 lemma enn2real_0[simp]: "enn2real 0 = 0"
```
```  1117   unfolding enn2real_def zero_ennreal.rep_eq by simp
```
```  1118
```
```  1119 lemma enn2real_1[simp]: "enn2real 1 = 1"
```
```  1120   unfolding enn2real_def one_ennreal.rep_eq by simp
```
```  1121
```
```  1122 lemma enn2real_numeral[simp]: "enn2real (numeral n) = (numeral n)"
```
```  1123   unfolding enn2real_def by simp
```
```  1124
```
```  1125 lemma enn2real_mult: "enn2real (a * b) = enn2real a * enn2real b"
```
```  1126   unfolding enn2real_def
```
```  1127   by (simp del: real_of_ereal_enn2ereal add: times_ennreal.rep_eq)
```
```  1128
```
```  1129 lemma enn2real_leI: "0 \<le> B \<Longrightarrow> x \<le> ennreal B \<Longrightarrow> enn2real x \<le> B"
```
```  1130   by (cases x rule: ennreal_cases) (auto simp: top_unique)
```
```  1131
```
```  1132 lemma enn2real_positive_iff: "0 < enn2real x \<longleftrightarrow> (0 < x \<and> x < top)"
```
```  1133   by (cases x rule: ennreal_cases) auto
```
```  1134
```
```  1135 lemma enn2real_eq_1_iff[simp]: "enn2real x = 1 \<longleftrightarrow> x = 1"
```
```  1136   by (cases x) auto
```
```  1137
```
```  1138 subsection \<open>Coercion from @{typ enat} to @{typ ennreal}\<close>
```
```  1139
```
```  1140
```
```  1141 definition ennreal_of_enat :: "enat \<Rightarrow> ennreal"
```
```  1142 where
```
```  1143   "ennreal_of_enat n = (case n of \<infinity> \<Rightarrow> top | enat n \<Rightarrow> of_nat n)"
```
```  1144
```
```  1145 declare [[coercion ennreal_of_enat]]
```
```  1146 declare [[coercion "of_nat :: nat \<Rightarrow> ennreal"]]
```
```  1147
```
```  1148 lemma ennreal_of_enat_infty[simp]: "ennreal_of_enat \<infinity> = \<infinity>"
```
```  1149   by (simp add: ennreal_of_enat_def)
```
```  1150
```
```  1151 lemma ennreal_of_enat_enat[simp]: "ennreal_of_enat (enat n) = of_nat n"
```
```  1152   by (simp add: ennreal_of_enat_def)
```
```  1153
```
```  1154 lemma ennreal_of_enat_0[simp]: "ennreal_of_enat 0 = 0"
```
```  1155   using ennreal_of_enat_enat[of 0] unfolding enat_0 by simp
```
```  1156
```
```  1157 lemma ennreal_of_enat_1[simp]: "ennreal_of_enat 1 = 1"
```
```  1158   using ennreal_of_enat_enat[of 1] unfolding enat_1 by simp
```
```  1159
```
```  1160 lemma ennreal_top_neq_of_nat[simp]: "(top::ennreal) \<noteq> of_nat i"
```
```  1161   using ennreal_of_nat_neq_top[of i] by metis
```
```  1162
```
```  1163 lemma ennreal_of_enat_inj[simp]: "ennreal_of_enat i = ennreal_of_enat j \<longleftrightarrow> i = j"
```
```  1164   by (cases i j rule: enat.exhaust[case_product enat.exhaust]) auto
```
```  1165
```
```  1166 lemma ennreal_of_enat_le_iff[simp]: "ennreal_of_enat m \<le> ennreal_of_enat n \<longleftrightarrow> m \<le> n"
```
```  1167   by (auto simp: ennreal_of_enat_def top_unique split: enat.split)
```
```  1168
```
```  1169 lemma of_nat_less_ennreal_of_nat[simp]: "of_nat n \<le> ennreal_of_enat x \<longleftrightarrow> of_nat n \<le> x"
```
```  1170   by (cases x) (auto simp: of_nat_eq_enat)
```
```  1171
```
```  1172 lemma ennreal_of_enat_Sup: "ennreal_of_enat (Sup X) = (SUP x:X. ennreal_of_enat x)"
```
```  1173 proof -
```
```  1174   have "ennreal_of_enat (Sup X) \<le> (SUP x : X. ennreal_of_enat x)"
```
```  1175     unfolding Sup_enat_def
```
```  1176   proof (clarsimp, intro conjI impI)
```
```  1177     fix x assume "finite X" "X \<noteq> {}"
```
```  1178     then show "ennreal_of_enat (Max X) \<le> (SUP x : X. ennreal_of_enat x)"
```
```  1179       by (intro SUP_upper Max_in)
```
```  1180   next
```
```  1181     assume "infinite X" "X \<noteq> {}"
```
```  1182     have "\<exists>y\<in>X. r < ennreal_of_enat y" if r: "r < top" for r
```
```  1183     proof -
```
```  1184       from ennreal_Ex_less_of_nat[OF r] guess n .. note n = this
```
```  1185       have "\<not> (X \<subseteq> enat ` {.. n})"
```
```  1186         using \<open>infinite X\<close> by (auto dest: finite_subset)
```
```  1187       then obtain x where x: "x \<in> X" "x \<notin> enat ` {..n}"
```
```  1188         by blast
```
```  1189       then have "of_nat n \<le> x"
```
```  1190         by (cases x) (auto simp: of_nat_eq_enat)
```
```  1191       with x show ?thesis
```
```  1192         by (auto intro!: bexI[of _ x] less_le_trans[OF n])
```
```  1193     qed
```
```  1194     then have "(SUP x : X. ennreal_of_enat x) = top"
```
```  1195       by simp
```
```  1196     then show "top \<le> (SUP x : X. ennreal_of_enat x)"
```
```  1197       unfolding top_unique by simp
```
```  1198   qed
```
```  1199   then show ?thesis
```
```  1200     by (auto intro!: antisym Sup_least intro: Sup_upper)
```
```  1201 qed
```
```  1202
```
```  1203 lemma ennreal_of_enat_eSuc[simp]: "ennreal_of_enat (eSuc x) = 1 + ennreal_of_enat x"
```
```  1204   by (cases x) (auto simp: eSuc_enat)
```
```  1205
```
```  1206 subsection \<open>Topology on @{typ ennreal}\<close>
```
```  1207
```
```  1208 lemma enn2ereal_Iio: "enn2ereal -` {..<a} = (if 0 \<le> a then {..< e2ennreal a} else {})"
```
```  1209   using enn2ereal_nonneg
```
```  1210   by (cases a rule: ereal_ennreal_cases)
```
```  1211      (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
```
```  1212            simp del: enn2ereal_nonneg
```
```  1213            intro: le_less_trans less_imp_le)
```
```  1214
```
```  1215 lemma enn2ereal_Ioi: "enn2ereal -` {a <..} = (if 0 \<le> a then {e2ennreal a <..} else UNIV)"
```
```  1216   by (cases a rule: ereal_ennreal_cases)
```
```  1217      (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
```
```  1218            intro: less_le_trans)
```
```  1219
```
```  1220 instantiation ennreal :: linear_continuum_topology
```
```  1221 begin
```
```  1222
```
```  1223 definition open_ennreal :: "ennreal set \<Rightarrow> bool"
```
```  1224   where "(open :: ennreal set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
```
```  1225
```
```  1226 instance
```
```  1227 proof
```
```  1228   show "\<exists>a b::ennreal. a \<noteq> b"
```
```  1229     using zero_neq_one by (intro exI)
```
```  1230   show "\<And>x y::ennreal. x < y \<Longrightarrow> \<exists>z>x. z < y"
```
```  1231   proof transfer
```
```  1232     fix x y :: ereal assume "0 \<le> x" and *: "x < y"
```
```  1233     moreover from dense[OF *] guess z ..
```
```  1234     ultimately show "\<exists>z\<in>Collect (op \<le> 0). x < z \<and> z < y"
```
```  1235       by (intro bexI[of _ z]) auto
```
```  1236   qed
```
```  1237 qed (rule open_ennreal_def)
```
```  1238
```
```  1239 end
```
```  1240
```
```  1241 lemma continuous_on_e2ennreal: "continuous_on A e2ennreal"
```
```  1242 proof (rule continuous_on_subset)
```
```  1243   show "continuous_on ({0..} \<union> {..0}) e2ennreal"
```
```  1244   proof (rule continuous_on_closed_Un)
```
```  1245     show "continuous_on {0 ..} e2ennreal"
```
```  1246       by (rule continuous_onI_mono)
```
```  1247          (auto simp add: less_eq_ennreal.abs_eq eq_onp_def enn2ereal_range)
```
```  1248     show "continuous_on {.. 0} e2ennreal"
```
```  1249       by (subst continuous_on_cong[OF refl, of _ _ "\<lambda>_. 0"])
```
```  1250          (auto simp add: e2ennreal_neg continuous_on_const)
```
```  1251   qed auto
```
```  1252   show "A \<subseteq> {0..} \<union> {..0::ereal}"
```
```  1253     by auto
```
```  1254 qed
```
```  1255
```
```  1256 lemma continuous_at_e2ennreal: "continuous (at x within A) e2ennreal"
```
```  1257   by (rule continuous_on_imp_continuous_within[OF continuous_on_e2ennreal, of _ UNIV]) auto
```
```  1258
```
```  1259 lemma continuous_on_enn2ereal: "continuous_on UNIV enn2ereal"
```
```  1260   by (rule continuous_on_generate_topology[OF open_generated_order])
```
```  1261      (auto simp add: enn2ereal_Iio enn2ereal_Ioi)
```
```  1262
```
```  1263 lemma continuous_at_enn2ereal: "continuous (at x within A) enn2ereal"
```
```  1264   by (rule continuous_on_imp_continuous_within[OF continuous_on_enn2ereal]) auto
```
```  1265
```
```  1266 lemma sup_continuous_e2ennreal[order_continuous_intros]:
```
```  1267   assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. e2ennreal (f x))"
```
```  1268   apply (rule sup_continuous_compose[OF _ f])
```
```  1269   apply (rule continuous_at_left_imp_sup_continuous)
```
```  1270   apply (auto simp: mono_def e2ennreal_mono continuous_at_e2ennreal)
```
```  1271   done
```
```  1272
```
```  1273 lemma sup_continuous_enn2ereal[order_continuous_intros]:
```
```  1274   assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. enn2ereal (f x))"
```
```  1275   apply (rule sup_continuous_compose[OF _ f])
```
```  1276   apply (rule continuous_at_left_imp_sup_continuous)
```
```  1277   apply (simp_all add: mono_def less_eq_ennreal.rep_eq continuous_at_enn2ereal)
```
```  1278   done
```
```  1279
```
```  1280 lemma sup_continuous_mult_left_ennreal':
```
```  1281   fixes c :: "ennreal"
```
```  1282   shows "sup_continuous (\<lambda>x. c * x)"
```
```  1283   unfolding sup_continuous_def
```
```  1284   by transfer (auto simp: SUP_ereal_mult_left max.absorb2 SUP_upper2)
```
```  1285
```
```  1286 lemma sup_continuous_mult_left_ennreal[order_continuous_intros]:
```
```  1287   "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. c * f x :: ennreal)"
```
```  1288   by (rule sup_continuous_compose[OF sup_continuous_mult_left_ennreal'])
```
```  1289
```
```  1290 lemma sup_continuous_mult_right_ennreal[order_continuous_intros]:
```
```  1291   "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x * c :: ennreal)"
```
```  1292   using sup_continuous_mult_left_ennreal[of f c] by (simp add: mult.commute)
```
```  1293
```
```  1294 lemma sup_continuous_divide_ennreal[order_continuous_intros]:
```
```  1295   fixes f g :: "'a::complete_lattice \<Rightarrow> ennreal"
```
```  1296   shows "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x / c)"
```
```  1297   unfolding divide_ennreal_def by (rule sup_continuous_mult_right_ennreal)
```
```  1298
```
```  1299 lemma transfer_enn2ereal_continuous_on [transfer_rule]:
```
```  1300   "rel_fun (op =) (rel_fun (rel_fun op = pcr_ennreal) op =) continuous_on continuous_on"
```
```  1301 proof -
```
```  1302   have "continuous_on A f" if "continuous_on A (\<lambda>x. enn2ereal (f x))" for A and f :: "'a \<Rightarrow> ennreal"
```
```  1303     using continuous_on_compose2[OF continuous_on_e2ennreal[of "{0..}"] that]
```
```  1304     by (auto simp: ennreal.enn2ereal_inverse subset_eq e2ennreal_def max_absorb2)
```
```  1305   moreover
```
```  1306   have "continuous_on A (\<lambda>x. enn2ereal (f x))" if "continuous_on A f" for A and f :: "'a \<Rightarrow> ennreal"
```
```  1307     using continuous_on_compose2[OF continuous_on_enn2ereal that] by auto
```
```  1308   ultimately
```
```  1309   show ?thesis
```
```  1310     by (auto simp add: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)
```
```  1311 qed
```
```  1312
```
```  1313 lemma transfer_sup_continuous[transfer_rule]:
```
```  1314   "(rel_fun (rel_fun (op =) pcr_ennreal) op =) sup_continuous sup_continuous"
```
```  1315 proof (safe intro!: rel_funI dest!: rel_fun_eq_pcr_ennreal[THEN iffD1])
```
```  1316   show "sup_continuous (enn2ereal \<circ> f) \<Longrightarrow> sup_continuous f" for f :: "'a \<Rightarrow> _"
```
```  1317     using sup_continuous_e2ennreal[of "enn2ereal \<circ> f"] by simp
```
```  1318   show "sup_continuous f \<Longrightarrow> sup_continuous (enn2ereal \<circ> f)" for f :: "'a \<Rightarrow> _"
```
```  1319     using sup_continuous_enn2ereal[of f] by (simp add: comp_def)
```
```  1320 qed
```
```  1321
```
```  1322 lemma continuous_on_ennreal[tendsto_intros]:
```
```  1323   "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. ennreal (f x))"
```
```  1324   by transfer (auto intro!: continuous_on_max continuous_on_const continuous_on_ereal)
```
```  1325
```
```  1326 lemma tendsto_ennrealD:
```
```  1327   assumes lim: "((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F"
```
```  1328   assumes *: "\<forall>\<^sub>F x in F. 0 \<le> f x" and x: "0 \<le> x"
```
```  1329   shows "(f \<longlongrightarrow> x) F"
```
```  1330   using continuous_on_tendsto_compose[OF continuous_on_enn2ereal lim]
```
```  1331   apply simp
```
```  1332   apply (subst (asm) tendsto_cong)
```
```  1333   using *
```
```  1334   apply eventually_elim
```
```  1335   apply (auto simp: max_absorb2 \<open>0 \<le> x\<close>)
```
```  1336   done
```
```  1337
```
```  1338 lemma tendsto_ennreal_iff[simp]:
```
```  1339   "\<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"
```
```  1340   by (auto dest: tendsto_ennrealD)
```
```  1341      (auto simp: ennreal_def
```
```  1342            intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)
```
```  1343
```
```  1344 lemma tendsto_enn2ereal_iff[simp]: "((\<lambda>i. enn2ereal (f i)) \<longlongrightarrow> enn2ereal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
```
```  1345   using continuous_on_enn2ereal[THEN continuous_on_tendsto_compose, of f x F]
```
```  1346     continuous_on_e2ennreal[THEN continuous_on_tendsto_compose, of "\<lambda>x. enn2ereal (f x)" "enn2ereal x" F UNIV]
```
```  1347   by auto
```
```  1348
```
```  1349 lemma continuous_on_add_ennreal:
```
```  1350   fixes f g :: "'a::topological_space \<Rightarrow> ennreal"
```
```  1351   shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x + g x)"
```
```  1352   by (transfer fixing: A) (auto intro!: tendsto_add_ereal_nonneg simp: continuous_on_def)
```
```  1353
```
```  1354 lemma continuous_on_inverse_ennreal[continuous_intros]:
```
```  1355   fixes f :: "'a::topological_space \<Rightarrow> ennreal"
```
```  1356   shows "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))"
```
```  1357 proof (transfer fixing: A)
```
```  1358   show "pred_fun top  (op \<le> 0) f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))" if "continuous_on A f"
```
```  1359     for f :: "'a \<Rightarrow> ereal"
```
```  1360     using continuous_on_compose2[OF continuous_on_inverse_ereal that] by (auto simp: subset_eq)
```
```  1361 qed
```
```  1362
```
```  1363 instance ennreal :: topological_comm_monoid_add
```
```  1364 proof
```
```  1365   show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)" for a b :: ennreal
```
```  1366     using continuous_on_add_ennreal[of UNIV fst snd]
```
```  1367     using tendsto_at_iff_tendsto_nhds[symmetric, of "\<lambda>x::(ennreal \<times> ennreal). fst x + snd x"]
```
```  1368     by (auto simp: continuous_on_eq_continuous_at)
```
```  1369        (simp add: isCont_def nhds_prod[symmetric])
```
```  1370 qed
```
```  1371
```
```  1372 lemma sup_continuous_add_ennreal[order_continuous_intros]:
```
```  1373   fixes f g :: "'a::complete_lattice \<Rightarrow> ennreal"
```
```  1374   shows "sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. f x + g x)"
```
```  1375   by transfer (auto intro!: sup_continuous_add)
```
```  1376
```
```  1377 lemma ennreal_suminf_lessD: "(\<Sum>i. f i :: ennreal) < x \<Longrightarrow> f i < x"
```
```  1378   using le_less_trans[OF sum_le_suminf[OF summableI, of "{i}" f]] by simp
```
```  1379
```
```  1380 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"
```
```  1381   unfolding sums_def by (simp add: always_eventually sum_nonneg)
```
```  1382
```
```  1383 lemma summable_suminf_not_top: "(\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top \<Longrightarrow> summable f"
```
```  1384   using summable_sums[OF summableI, of "\<lambda>i. ennreal (f i)"]
```
```  1385   by (cases "\<Sum>i. ennreal (f i)" rule: ennreal_cases)
```
```  1386      (auto simp: summable_def)
```
```  1387
```
```  1388 lemma suminf_ennreal[simp]:
```
```  1389   "(\<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)"
```
```  1390   by (rule sums_unique[symmetric]) (simp add: summable_suminf_not_top suminf_nonneg summable_sums)
```
```  1391
```
```  1392 lemma sums_enn2ereal[simp]: "(\<lambda>i. enn2ereal (f i)) sums enn2ereal x \<longleftrightarrow> f sums x"
```
```  1393   unfolding sums_def by (simp add: always_eventually sum_nonneg)
```
```  1394
```
```  1395 lemma suminf_enn2ereal[simp]: "(\<Sum>i. enn2ereal (f i)) = enn2ereal (suminf f)"
```
```  1396   by (rule sums_unique[symmetric]) (simp add: summable_sums)
```
```  1397
```
```  1398 lemma transfer_e2ennreal_suminf [transfer_rule]: "rel_fun (rel_fun op = pcr_ennreal) pcr_ennreal suminf suminf"
```
```  1399   by (auto simp: rel_funI rel_fun_eq_pcr_ennreal comp_def)
```
```  1400
```
```  1401 lemma ennreal_suminf_cmult[simp]: "(\<Sum>i. r * f i) = r * (\<Sum>i. f i::ennreal)"
```
```  1402   by transfer (auto intro!: suminf_cmult_ereal)
```
```  1403
```
```  1404 lemma ennreal_suminf_multc[simp]: "(\<Sum>i. f i * r) = (\<Sum>i. f i::ennreal) * r"
```
```  1405   using ennreal_suminf_cmult[of r f] by (simp add: ac_simps)
```
```  1406
```
```  1407 lemma ennreal_suminf_divide[simp]: "(\<Sum>i. f i / r) = (\<Sum>i. f i::ennreal) / r"
```
```  1408   by (simp add: divide_ennreal_def)
```
```  1409
```
```  1410 lemma ennreal_suminf_neq_top: "summable f \<Longrightarrow> (\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top"
```
```  1411   using sums_ennreal[of f "suminf f"]
```
```  1412   by (simp add: suminf_nonneg sums_unique[symmetric] summable_sums_iff[symmetric] del: sums_ennreal)
```
```  1413
```
```  1414 lemma suminf_ennreal_eq:
```
```  1415   "(\<And>i. 0 \<le> f i) \<Longrightarrow> f sums x \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal x"
```
```  1416   using suminf_nonneg[of f] sums_unique[of f x]
```
```  1417   by (intro sums_unique[symmetric]) (auto simp: summable_sums_iff)
```
```  1418
```
```  1419 lemma ennreal_suminf_bound_add:
```
```  1420   fixes f :: "nat \<Rightarrow> ennreal"
```
```  1421   shows "(\<And>N. (\<Sum>n<N. f n) + y \<le> x) \<Longrightarrow> suminf f + y \<le> x"
```
```  1422   by transfer (auto intro!: suminf_bound_add)
```
```  1423
```
```  1424 lemma ennreal_suminf_SUP_eq_directed:
```
```  1425   fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
```
```  1426   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"
```
```  1427   shows "(\<Sum>n. SUP i:I. f i n) = (SUP i:I. \<Sum>n. f i n)"
```
```  1428 proof cases
```
```  1429   assume "I \<noteq> {}"
```
```  1430   then obtain i where "i \<in> I" by auto
```
```  1431   from * show ?thesis
```
```  1432     by (transfer fixing: I)
```
```  1433        (auto simp: max_absorb2 SUP_upper2[OF \<open>i \<in> I\<close>] suminf_nonneg summable_ereal_pos \<open>I \<noteq> {}\<close>
```
```  1434              intro!: suminf_SUP_eq_directed)
```
```  1435 qed (simp add: bot_ennreal)
```
```  1436
```
```  1437 lemma INF_ennreal_add_const:
```
```  1438   fixes f g :: "nat \<Rightarrow> ennreal"
```
```  1439   shows "(INF i. f i + c) = (INF i. f i) + c"
```
```  1440   using continuous_at_Inf_mono[of "\<lambda>x. x + c" "f`UNIV"]
```
```  1441   using continuous_add[of "at_right (Inf (range f))", of "\<lambda>x. x" "\<lambda>x. c"]
```
```  1442   by (auto simp: mono_def)
```
```  1443
```
```  1444 lemma INF_ennreal_const_add:
```
```  1445   fixes f g :: "nat \<Rightarrow> ennreal"
```
```  1446   shows "(INF i. c + f i) = c + (INF i. f i)"
```
```  1447   using INF_ennreal_add_const[of f c] by (simp add: ac_simps)
```
```  1448
```
```  1449 lemma SUP_mult_left_ennreal: "c * (SUP i:I. f i) = (SUP i:I. c * f i ::ennreal)"
```
```  1450 proof cases
```
```  1451   assume "I \<noteq> {}" then show ?thesis
```
```  1452     by transfer (auto simp add: SUP_ereal_mult_left max_absorb2 SUP_upper2)
```
```  1453 qed (simp add: bot_ennreal)
```
```  1454
```
```  1455 lemma SUP_mult_right_ennreal: "(SUP i:I. f i) * c = (SUP i:I. f i * c ::ennreal)"
```
```  1456   using SUP_mult_left_ennreal by (simp add: mult.commute)
```
```  1457
```
```  1458 lemma SUP_divide_ennreal: "(SUP i:I. f i) / c = (SUP i:I. f i / c ::ennreal)"
```
```  1459   using SUP_mult_right_ennreal by (simp add: divide_ennreal_def)
```
```  1460
```
```  1461 lemma ennreal_SUP_of_nat_eq_top: "(SUP x. of_nat x :: ennreal) = top"
```
```  1462 proof (intro antisym top_greatest le_SUP_iff[THEN iffD2] allI impI)
```
```  1463   fix y :: ennreal assume "y < top"
```
```  1464   then obtain r where "y = ennreal r"
```
```  1465     by (cases y rule: ennreal_cases) auto
```
```  1466   then show "\<exists>i\<in>UNIV. y < of_nat i"
```
```  1467     using reals_Archimedean2[of "max 1 r"] zero_less_one
```
```  1468     by (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_def less_ennreal.abs_eq eq_onp_def max.absorb2
```
```  1469              dest!: one_less_of_natD intro: less_trans)
```
```  1470 qed
```
```  1471
```
```  1472 lemma ennreal_SUP_eq_top:
```
```  1473   fixes f :: "'a \<Rightarrow> ennreal"
```
```  1474   assumes "\<And>n. \<exists>i\<in>I. of_nat n \<le> f i"
```
```  1475   shows "(SUP i : I. f i) = top"
```
```  1476 proof -
```
```  1477   have "(SUP x. of_nat x :: ennreal) \<le> (SUP i : I. f i)"
```
```  1478     using assms by (auto intro!: SUP_least intro: SUP_upper2)
```
```  1479   then show ?thesis
```
```  1480     by (auto simp: ennreal_SUP_of_nat_eq_top top_unique)
```
```  1481 qed
```
```  1482
```
```  1483 lemma ennreal_INF_const_minus:
```
```  1484   fixes f :: "'a \<Rightarrow> ennreal"
```
```  1485   shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
```
```  1486   by (transfer fixing: I)
```
```  1487      (simp add: sup_max[symmetric] SUP_sup_const1 SUP_ereal_minus_right del: sup_ereal_def)
```
```  1488
```
```  1489 lemma of_nat_Sup_ennreal:
```
```  1490   assumes "A \<noteq> {}" "bdd_above A"
```
```  1491   shows "of_nat (Sup A) = (SUP a:A. of_nat a :: ennreal)"
```
```  1492 proof (intro antisym)
```
```  1493   show "(SUP a:A. of_nat a::ennreal) \<le> of_nat (Sup A)"
```
```  1494     by (intro SUP_least of_nat_mono) (auto intro: cSup_upper assms)
```
```  1495   have "Sup A \<in> A"
```
```  1496     unfolding Sup_nat_def using assms by (intro Max_in) (auto simp: bdd_above_nat)
```
```  1497   then show "of_nat (Sup A) \<le> (SUP a:A. of_nat a::ennreal)"
```
```  1498     by (intro SUP_upper)
```
```  1499 qed
```
```  1500
```
```  1501 lemma ennreal_tendsto_const_minus:
```
```  1502   fixes g :: "'a \<Rightarrow> ennreal"
```
```  1503   assumes ae: "\<forall>\<^sub>F x in F. g x \<le> c"
```
```  1504   assumes g: "((\<lambda>x. c - g x) \<longlongrightarrow> 0) F"
```
```  1505   shows "(g \<longlongrightarrow> c) F"
```
```  1506 proof (cases c rule: ennreal_cases)
```
```  1507   case top with tendsto_unique[OF _ g, of "top"] show ?thesis
```
```  1508     by (cases "F = bot") auto
```
```  1509 next
```
```  1510   case (real r)
```
```  1511   then have "\<forall>x. \<exists>q\<ge>0. g x \<le> c \<longrightarrow> (g x = ennreal q \<and> q \<le> r)"
```
```  1512     by (auto simp: le_ennreal_iff)
```
```  1513   then obtain f where *: "0 \<le> f x" "g x = ennreal (f x)" "f x \<le> r" if "g x \<le> c" for x
```
```  1514     by metis
```
```  1515   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"
```
```  1516   proof eventually_elim
```
```  1517     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"
```
```  1518       by (auto simp: real ennreal_minus)
```
```  1519   qed
```
```  1520   with g have "((\<lambda>x. ennreal (r - f x)) \<longlongrightarrow> ennreal 0) F"
```
```  1521     by (auto simp add: tendsto_cong eventually_conj_iff)
```
```  1522   with ae2 have "((\<lambda>x. r - f x) \<longlongrightarrow> 0) F"
```
```  1523     by (subst (asm) tendsto_ennreal_iff) (auto elim: eventually_mono)
```
```  1524   then have "(f \<longlongrightarrow> r) F"
```
```  1525     by (rule Lim_transform2[OF tendsto_const])
```
```  1526   with ae2 have "((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal r) F"
```
```  1527     by (subst tendsto_ennreal_iff) (auto elim: eventually_mono simp: real)
```
```  1528   with ae2 show ?thesis
```
```  1529     by (auto simp: real tendsto_cong eventually_conj_iff)
```
```  1530 qed
```
```  1531
```
```  1532 lemma ennreal_SUP_add:
```
```  1533   fixes f g :: "nat \<Rightarrow> ennreal"
```
```  1534   shows "incseq f \<Longrightarrow> incseq g \<Longrightarrow> (SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
```
```  1535   unfolding incseq_def le_fun_def
```
```  1536   by transfer
```
```  1537      (simp add: SUP_ereal_add incseq_def le_fun_def max_absorb2 SUP_upper2)
```
```  1538
```
```  1539 lemma ennreal_SUP_sum:
```
```  1540   fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
```
```  1541   shows "(\<And>i. i \<in> I \<Longrightarrow> incseq (f i)) \<Longrightarrow> (SUP n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. SUP n. f i n)"
```
```  1542   unfolding incseq_def
```
```  1543   by transfer
```
```  1544      (simp add: SUP_ereal_sum incseq_def SUP_upper2 max_absorb2 sum_nonneg)
```
```  1545
```
```  1546 lemma ennreal_liminf_minus:
```
```  1547   fixes f :: "nat \<Rightarrow> ennreal"
```
```  1548   shows "(\<And>n. f n \<le> c) \<Longrightarrow> liminf (\<lambda>n. c - f n) = c - limsup f"
```
```  1549   apply transfer
```
```  1550   apply (simp add: ereal_diff_positive max.absorb2 liminf_ereal_cminus)
```
```  1551   apply (subst max.absorb2)
```
```  1552   apply (rule ereal_diff_positive)
```
```  1553   apply (rule Limsup_bounded)
```
```  1554   apply auto
```
```  1555   done
```
```  1556
```
```  1557 lemma ennreal_continuous_on_cmult:
```
```  1558   "(c::ennreal) < top \<Longrightarrow> continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. c * f x)"
```
```  1559   by (transfer fixing: A) (auto intro: continuous_on_cmult_ereal)
```
```  1560
```
```  1561 lemma ennreal_tendsto_cmult:
```
```  1562   "(c::ennreal) < top \<Longrightarrow> (f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. c * f x) \<longlongrightarrow> c * x) F"
```
```  1563   by (rule continuous_on_tendsto_compose[where g=f, OF ennreal_continuous_on_cmult, where s=UNIV])
```
```  1564      (auto simp: continuous_on_id)
```
```  1565
```
```  1566 lemma tendsto_ennrealI[intro, simp]:
```
```  1567   "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F"
```
```  1568   by (auto simp: ennreal_def
```
```  1569            intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)
```
```  1570
```
```  1571 lemma ennreal_suminf_minus:
```
```  1572   fixes f g :: "nat \<Rightarrow> ennreal"
```
```  1573   shows "(\<And>i. g i \<le> f i) \<Longrightarrow> suminf f \<noteq> top \<Longrightarrow> suminf g \<noteq> top \<Longrightarrow> (\<Sum>i. f i - g i) = suminf f - suminf g"
```
```  1574   by transfer
```
```  1575      (auto simp add: max.absorb2 ereal_diff_positive suminf_le_pos top_ereal_def intro!: suminf_ereal_minus)
```
```  1576
```
```  1577 lemma ennreal_Sup_countable_SUP:
```
```  1578   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. incseq f \<and> range f \<subseteq> A \<and> Sup A = (SUP i. f i)"
```
```  1579   unfolding incseq_def
```
```  1580   apply transfer
```
```  1581   subgoal for A
```
```  1582     using Sup_countable_SUP[of A]
```
```  1583     apply (clarsimp simp add: incseq_def[symmetric] SUP_upper2 max.absorb2 image_subset_iff Sup_upper2 cong: conj_cong)
```
```  1584     subgoal for f
```
```  1585       by (intro exI[of _ f]) auto
```
```  1586     done
```
```  1587   done
```
```  1588
```
```  1589 lemma ennreal_Inf_countable_INF:
```
```  1590   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. decseq f \<and> range f \<subseteq> A \<and> Inf A = (INF i. f i)"
```
```  1591   including ennreal.lifting
```
```  1592   unfolding decseq_def
```
```  1593   apply transfer
```
```  1594   subgoal for A
```
```  1595     using Inf_countable_INF[of A]
```
```  1596     apply (clarsimp simp add: decseq_def[symmetric])
```
```  1597     subgoal for f
```
```  1598       by (intro exI[of _ f]) auto
```
```  1599     done
```
```  1600   done
```
```  1601
```
```  1602 lemma ennreal_SUP_countable_SUP:
```
```  1603   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
```
```  1604   using ennreal_Sup_countable_SUP [of "g`A"] by auto
```
```  1605
```
```  1606 lemma of_nat_tendsto_top_ennreal: "(\<lambda>n::nat. of_nat n :: ennreal) \<longlonglongrightarrow> top"
```
```  1607   using LIMSEQ_SUP[of "of_nat :: nat \<Rightarrow> ennreal"]
```
```  1608   by (simp add: ennreal_SUP_of_nat_eq_top incseq_def)
```
```  1609
```
```  1610 lemma SUP_sup_continuous_ennreal:
```
```  1611   fixes f :: "ennreal \<Rightarrow> 'a::complete_lattice"
```
```  1612   assumes f: "sup_continuous f" and "I \<noteq> {}"
```
```  1613   shows "(SUP i:I. f (g i)) = f (SUP i:I. g i)"
```
```  1614 proof (rule antisym)
```
```  1615   show "(SUP i:I. f (g i)) \<le> f (SUP i:I. g i)"
```
```  1616     by (rule mono_SUP[OF sup_continuous_mono[OF f]])
```
```  1617   from ennreal_Sup_countable_SUP[of "g`I"] \<open>I \<noteq> {}\<close>
```
```  1618   obtain M :: "nat \<Rightarrow> ennreal" where "incseq M" and M: "range M \<subseteq> g ` I" and eq: "(SUP i : I. g i) = (SUP i. M i)"
```
```  1619     by auto
```
```  1620   have "f (SUP i : I. g i) = (SUP i : range M. f i)"
```
```  1621     unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by simp
```
```  1622   also have "\<dots> \<le> (SUP i : I. f (g i))"
```
```  1623     by (insert M, drule SUP_subset_mono) auto
```
```  1624   finally show "f (SUP i : I. g i) \<le> (SUP i : I. f (g i))" .
```
```  1625 qed
```
```  1626
```
```  1627 lemma ennreal_suminf_SUP_eq:
```
```  1628   fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ennreal"
```
```  1629   shows "(\<And>i. incseq (\<lambda>n. f n i)) \<Longrightarrow> (\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
```
```  1630   apply (rule ennreal_suminf_SUP_eq_directed)
```
```  1631   subgoal for N n j
```
```  1632     by (auto simp: incseq_def intro!:exI[of _ "max n j"])
```
```  1633   done
```
```  1634
```
```  1635 lemma ennreal_SUP_add_left:
```
```  1636   fixes c :: ennreal
```
```  1637   shows "I \<noteq> {} \<Longrightarrow> (SUP i:I. f i + c) = (SUP i:I. f i) + c"
```
```  1638   apply transfer
```
```  1639   apply (simp add: SUP_ereal_add_left)
```
```  1640   apply (subst (1 2) max.absorb2)
```
```  1641   apply (auto intro: SUP_upper2 ereal_add_nonneg_nonneg)
```
```  1642   done
```
```  1643
```
```  1644 lemma ennreal_SUP_const_minus: (* TODO: rename: ennreal_SUP_const_minus *)
```
```  1645   fixes f :: "'a \<Rightarrow> ennreal"
```
```  1646   shows "I \<noteq> {} \<Longrightarrow> c < top \<Longrightarrow> (INF x:I. c - f x) = c - (SUP x:I. f x)"
```
```  1647   apply (transfer fixing: I)
```
```  1648   unfolding ex_in_conv[symmetric]
```
```  1649   apply (auto simp add: sup_max[symmetric] SUP_upper2 sup_absorb2
```
```  1650               simp del: sup_ereal_def)
```
```  1651   apply (subst INF_ereal_minus_right[symmetric])
```
```  1652   apply (auto simp del: sup_ereal_def simp add: sup_INF)
```
```  1653   done
```
```  1654
```
```  1655 subsection \<open>Approximation lemmas\<close>
```
```  1656
```
```  1657 lemma INF_approx_ennreal:
```
```  1658   fixes x::ennreal and e::real
```
```  1659   assumes "e > 0"
```
```  1660   assumes INF: "x = (INF i : A. f i)"
```
```  1661   assumes "x \<noteq> \<infinity>"
```
```  1662   shows "\<exists>i \<in> A. f i < x + e"
```
```  1663 proof -
```
```  1664   have "(INF i : A. f i) < x + e"
```
```  1665     unfolding INF[symmetric] using \<open>0<e\<close> \<open>x \<noteq> \<infinity>\<close> by (cases x) auto
```
```  1666   then show ?thesis
```
```  1667     unfolding INF_less_iff .
```
```  1668 qed
```
```  1669
```
```  1670 lemma SUP_approx_ennreal:
```
```  1671   fixes x::ennreal and e::real
```
```  1672   assumes "e > 0" "A \<noteq> {}"
```
```  1673   assumes SUP: "x = (SUP i : A. f i)"
```
```  1674   assumes "x \<noteq> \<infinity>"
```
```  1675   shows "\<exists>i \<in> A. x < f i + e"
```
```  1676 proof -
```
```  1677   have "x < x + e"
```
```  1678     using \<open>0<e\<close> \<open>x \<noteq> \<infinity>\<close> by (cases x) auto
```
```  1679   also have "x + e = (SUP i : A. f i + e)"
```
```  1680     unfolding SUP ennreal_SUP_add_left[OF \<open>A \<noteq> {}\<close>] ..
```
```  1681   finally show ?thesis
```
```  1682     unfolding less_SUP_iff .
```
```  1683 qed
```
```  1684
```
```  1685 lemma ennreal_approx_SUP:
```
```  1686   fixes x::ennreal
```
```  1687   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
```
```  1688   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
```
```  1689   shows "x = (SUP i : A. f i)"
```
```  1690 proof (rule antisym)
```
```  1691   show "x \<le> (SUP i:A. f i)"
```
```  1692   proof (rule ennreal_le_epsilon)
```
```  1693     fix e :: real assume "0 < e"
```
```  1694     from approx[OF this] guess i ..
```
```  1695     then have "x \<le> f i + e"
```
```  1696       by simp
```
```  1697     also have "\<dots> \<le> (SUP i:A. f i) + e"
```
```  1698       by (intro add_mono \<open>i \<in> A\<close> SUP_upper order_refl)
```
```  1699     finally show "x \<le> (SUP i:A. f i) + e" .
```
```  1700   qed
```
```  1701 qed (intro SUP_least f_bound)
```
```  1702
```
```  1703 lemma ennreal_approx_INF:
```
```  1704   fixes x::ennreal
```
```  1705   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
```
```  1706   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
```
```  1707   shows "x = (INF i : A. f i)"
```
```  1708 proof (rule antisym)
```
```  1709   show "(INF i:A. f i) \<le> x"
```
```  1710   proof (rule ennreal_le_epsilon)
```
```  1711     fix e :: real assume "0 < e"
```
```  1712     from approx[OF this] guess i .. note i = this
```
```  1713     then have "(INF i:A. f i) \<le> f i"
```
```  1714       by (intro INF_lower)
```
```  1715     also have "\<dots> \<le> x + e"
```
```  1716       by fact
```
```  1717     finally show "(INF i:A. f i) \<le> x + e" .
```
```  1718   qed
```
```  1719 qed (intro INF_greatest f_bound)
```
```  1720
```
```  1721 lemma ennreal_approx_unit:
```
```  1722   "(\<And>a::ennreal. 0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * z \<le> y) \<Longrightarrow> z \<le> y"
```
```  1723   apply (subst SUP_mult_right_ennreal[of "\<lambda>x. x" "{0 <..< 1}" z, simplified])
```
```  1724   apply (rule SUP_least)
```
```  1725   apply auto
```
```  1726   done
```
```  1727
```
```  1728 lemma suminf_ennreal2:
```
```  1729   "(\<And>i. 0 \<le> f i) \<Longrightarrow> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal (\<Sum>i. f i)"
```
```  1730   using suminf_ennreal_eq by blast
```
```  1731
```
```  1732 lemma less_top_ennreal: "x < top \<longleftrightarrow> (\<exists>r\<ge>0. x = ennreal r)"
```
```  1733   by (cases x) auto
```
```  1734
```
```  1735 lemma tendsto_top_iff_ennreal:
```
```  1736   fixes f :: "'a \<Rightarrow> ennreal"
```
```  1737   shows "(f \<longlongrightarrow> top) F \<longleftrightarrow> (\<forall>l\<ge>0. eventually (\<lambda>x. ennreal l < f x) F)"
```
```  1738   by (auto simp: less_top_ennreal order_tendsto_iff )
```
```  1739
```
```  1740 lemma ennreal_tendsto_top_eq_at_top:
```
```  1741   "((\<lambda>z. ennreal (f z)) \<longlongrightarrow> top) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
```
```  1742   unfolding filterlim_at_top_dense tendsto_top_iff_ennreal
```
```  1743   apply (auto simp: ennreal_less_iff)
```
```  1744   subgoal for y
```
```  1745     by (auto elim!: eventually_mono allE[of _ "max 0 y"])
```
```  1746   done
```
```  1747
```
```  1748 lemma tendsto_0_if_Limsup_eq_0_ennreal:
```
```  1749   fixes f :: "_ \<Rightarrow> ennreal"
```
```  1750   shows "Limsup F f = 0 \<Longrightarrow> (f \<longlongrightarrow> 0) F"
```
```  1751   using Liminf_le_Limsup[of F f] tendsto_iff_Liminf_eq_Limsup[of F f 0]
```
```  1752   by (cases "F = bot") auto
```
```  1753
```
```  1754 lemma diff_le_self_ennreal[simp]: "a - b \<le> (a::ennreal)"
```
```  1755   by (cases a b rule: ennreal2_cases) (auto simp: ennreal_minus)
```
```  1756
```
```  1757 lemma ennreal_ineq_diff_add: "b \<le> a \<Longrightarrow> a = b + (a - b::ennreal)"
```
```  1758   by transfer (auto simp: ereal_diff_positive max.absorb2 ereal_ineq_diff_add)
```
```  1759
```
```  1760 lemma ennreal_mult_strict_left_mono: "(a::ennreal) < c \<Longrightarrow> 0 < b \<Longrightarrow> b < top \<Longrightarrow> b * a < b * c"
```
```  1761   by transfer (auto intro!: ereal_mult_strict_left_mono)
```
```  1762
```
```  1763 lemma ennreal_between: "0 < e \<Longrightarrow> 0 < x \<Longrightarrow> x < top \<Longrightarrow> x - e < (x::ennreal)"
```
```  1764   by transfer (auto intro!: ereal_between)
```
```  1765
```
```  1766 lemma minus_less_iff_ennreal: "b < top \<Longrightarrow> b \<le> a \<Longrightarrow> a - b < c \<longleftrightarrow> a < c + (b::ennreal)"
```
```  1767   by transfer
```
```  1768      (auto simp: top_ereal_def ereal_minus_less le_less)
```
```  1769
```
```  1770 lemma tendsto_zero_ennreal:
```
```  1771   assumes ev: "\<And>r. 0 < r \<Longrightarrow> \<forall>\<^sub>F x in F. f x < ennreal r"
```
```  1772   shows "(f \<longlongrightarrow> 0) F"
```
```  1773 proof (rule order_tendstoI)
```
```  1774   fix e::ennreal assume "e > 0"
```
```  1775   obtain e'::real where "e' > 0" "ennreal e' < e"
```
```  1776     using \<open>0 < e\<close> dense[of 0 "if e = top then 1 else (enn2real e)"]
```
```  1777     by (cases e) (auto simp: ennreal_less_iff)
```
```  1778   from ev[OF \<open>e' > 0\<close>] show "\<forall>\<^sub>F x in F. f x < e"
```
```  1779     by eventually_elim (insert \<open>ennreal e' < e\<close>, auto)
```
```  1780 qed simp
```
```  1781
```
```  1782 lifting_update ennreal.lifting
```
```  1783 lifting_forget ennreal.lifting
```
```  1784
```
```  1785
```
```  1786 subsection \<open>@{typ ennreal} theorems\<close>
```
```  1787
```
```  1788 lemma neq_top_trans: fixes x y :: ennreal shows "\<lbrakk> y \<noteq> top; x \<le> y \<rbrakk> \<Longrightarrow> x \<noteq> top"
```
```  1789 by (auto simp: top_unique)
```
```  1790
```
```  1791 lemma diff_diff_ennreal: fixes a b :: ennreal shows "a \<le> b \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> b - (b - a) = a"
```
```  1792   by (cases a b rule: ennreal2_cases)
```
```  1793      (auto simp: ennreal_minus top_unique)
```
```  1794
```
```  1795 lemma ennreal_less_one_iff[simp]: "ennreal x < 1 \<longleftrightarrow> x < 1"
```
```  1796   by (cases "0 \<le> x")
```
```  1797      (auto simp: ennreal_neg ennreal_1[symmetric] ennreal_less_iff simp del: ennreal_1)
```
```  1798
```
```  1799 lemma SUP_const_minus_ennreal:
```
```  1800   fixes f :: "'a \<Rightarrow> ennreal" shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
```
```  1801   including ennreal.lifting
```
```  1802   by (transfer fixing: I)
```
```  1803      (simp add: sup_ereal_def[symmetric] SUP_sup_distrib[symmetric] SUP_ereal_minus_right
```
```  1804            del: sup_ereal_def)
```
```  1805
```
```  1806 lemma zero_minus_ennreal[simp]: "0 - (a::ennreal) = 0"
```
```  1807   including ennreal.lifting
```
```  1808   by transfer (simp split: split_max)
```
```  1809
```
```  1810 lemma diff_diff_commute_ennreal:
```
```  1811   fixes a b c :: ennreal shows "a - b - c = a - c - b"
```
```  1812   by (cases a b c rule: ennreal3_cases) (simp_all add: ennreal_minus field_simps)
```
```  1813
```
```  1814 lemma diff_gr0_ennreal: "b < (a::ennreal) \<Longrightarrow> 0 < a - b"
```
```  1815   including ennreal.lifting by transfer (auto simp: ereal_diff_gr0 ereal_diff_positive split: split_max)
```
```  1816
```
```  1817 lemma divide_le_posI_ennreal:
```
```  1818   fixes x y z :: ennreal
```
```  1819   shows "x > 0 \<Longrightarrow> z \<le> x * y \<Longrightarrow> z / x \<le> y"
```
```  1820   by (cases x y z rule: ennreal3_cases)
```
```  1821      (auto simp: divide_ennreal ennreal_mult[symmetric] field_simps top_unique)
```
```  1822
```
```  1823 lemma add_diff_eq_ennreal:
```
```  1824   fixes x y z :: ennreal
```
```  1825   shows "z \<le> y \<Longrightarrow> x + (y - z) = x + y - z"
```
```  1826   including ennreal.lifting
```
```  1827   by transfer
```
```  1828      (insert ereal_add_mono[of 0], auto simp add: ereal_diff_positive max.absorb2 add_diff_eq_ereal)
```
```  1829
```
```  1830 lemma add_diff_inverse_ennreal:
```
```  1831   fixes x y :: ennreal shows "x \<le> y \<Longrightarrow> x + (y - x) = y"
```
```  1832   by (cases x) (simp_all add: top_unique add_diff_eq_ennreal)
```
```  1833
```
```  1834 lemma add_diff_eq_iff_ennreal[simp]:
```
```  1835   fixes x y :: ennreal shows "x + (y - x) = y \<longleftrightarrow> x \<le> y"
```
```  1836 proof
```
```  1837   assume *: "x + (y - x) = y" show "x \<le> y"
```
```  1838     by (subst *[symmetric]) simp
```
```  1839 qed (simp add: add_diff_inverse_ennreal)
```
```  1840
```
```  1841 lemma add_diff_le_ennreal: "a + b - c \<le> a + (b - c::ennreal)"
```
```  1842   apply (cases a b c rule: ennreal3_cases)
```
```  1843   subgoal for a' b' c'
```
```  1844     by (cases "0 \<le> b' - c'")
```
```  1845        (simp_all add: ennreal_minus ennreal_plus[symmetric] top_add ennreal_neg
```
```  1846                  del: ennreal_plus)
```
```  1847   apply (simp_all add: top_add ennreal_plus[symmetric] del: ennreal_plus)
```
```  1848   done
```
```  1849
```
```  1850 lemma diff_eq_0_ennreal: "a < top \<Longrightarrow> a \<le> b \<Longrightarrow> a - b = (0::ennreal)"
```
```  1851   using ennreal_minus_pos_iff gr_zeroI not_less by blast
```
```  1852
```
```  1853 lemma diff_diff_ennreal': fixes x y z :: ennreal shows "z \<le> y \<Longrightarrow> y - z \<le> x \<Longrightarrow> x - (y - z) = x + z - y"
```
```  1854   by (cases x; cases y; cases z)
```
```  1855      (auto simp add: top_add add_top minus_top_ennreal ennreal_minus ennreal_plus[symmetric] top_unique
```
```  1856            simp del: ennreal_plus)
```
```  1857
```
```  1858 lemma diff_diff_ennreal'': fixes x y z :: ennreal
```
```  1859   shows "z \<le> y \<Longrightarrow> x - (y - z) = (if y - z \<le> x then x + z - y else 0)"
```
```  1860   by (cases x; cases y; cases z)
```
```  1861      (auto simp add: top_add add_top minus_top_ennreal ennreal_minus ennreal_plus[symmetric] top_unique ennreal_neg
```
```  1862            simp del: ennreal_plus)
```
```  1863
```
```  1864 lemma power_less_top_ennreal: fixes x :: ennreal shows "x ^ n < top \<longleftrightarrow> x < top \<or> n = 0"
```
```  1865   using power_eq_top_ennreal[of x n] by (auto simp: less_top)
```
```  1866
```
```  1867 lemma ennreal_divide_times: "(a / b) * c = a * (c / b :: ennreal)"
```
```  1868   by (simp add: mult.commute ennreal_times_divide)
```
```  1869
```
```  1870 lemma diff_less_top_ennreal: "a - b < top \<longleftrightarrow>  a < (top :: ennreal)"
```
```  1871   by (cases a; cases b) (auto simp: ennreal_minus)
```
```  1872
```
```  1873 lemma divide_less_ennreal: "b \<noteq> 0 \<Longrightarrow> b < top \<Longrightarrow> a / b < c \<longleftrightarrow> a < (c * b :: ennreal)"
```
```  1874   by (cases a; cases b; cases c)
```
```  1875      (auto simp: divide_ennreal ennreal_mult[symmetric] ennreal_less_iff field_simps ennreal_top_mult ennreal_top_divide)
```
```  1876
```
```  1877 lemma one_less_numeral[simp]: "1 < (numeral n::ennreal) \<longleftrightarrow> (num.One < n)"
```
```  1878   by (simp del: ennreal_1 ennreal_numeral add: ennreal_1[symmetric] ennreal_numeral[symmetric] ennreal_less_iff)
```
```  1879
```
```  1880 lemma divide_eq_1_ennreal: "a / b = (1::ennreal) \<longleftrightarrow> (b \<noteq> top \<and> b \<noteq> 0 \<and> b = a)"
```
```  1881   by (cases a ; cases b; cases "b = 0") (auto simp: ennreal_top_divide divide_ennreal split: if_split_asm)
```
```  1882
```
```  1883 lemma ennreal_mult_cancel_left: "(a * b = a * c) = (a = top \<and> b \<noteq> 0 \<and> c \<noteq> 0 \<or> a = 0 \<or> b = (c::ennreal))"
```
```  1884   by (cases a; cases b; cases c) (auto simp: ennreal_mult[symmetric] ennreal_mult_top ennreal_top_mult)
```
```  1885
```
```  1886 lemma ennreal_minus_if: "ennreal a - ennreal b = ennreal (if 0 \<le> b then (if b \<le> a then a - b else 0) else a)"
```
```  1887   by (auto simp: ennreal_minus ennreal_neg)
```
```  1888
```
```  1889 lemma ennreal_plus_if: "ennreal a + ennreal b = ennreal (if 0 \<le> a then (if 0 \<le> b then a + b else a) else b)"
```
```  1890   by (auto simp: ennreal_neg)
```
```  1891
```
```  1892 lemma power_le_one_iff: "0 \<le> (a::real) \<Longrightarrow> a ^ n \<le> 1 \<longleftrightarrow> (n = 0 \<or> a \<le> 1)"
```
```  1893   by (metis (mono_tags, hide_lams) le_less neq0_conv not_le one_le_power power_0 power_eq_imp_eq_base power_le_one zero_le_one)
```
```  1894
```
```  1895 lemma ennreal_diff_le_mono_left: "a \<le> b \<Longrightarrow> a - c \<le> (b::ennreal)"
```
```  1896   using ennreal_mono_minus[of 0 c a, THEN order_trans, of b] by simp
```
```  1897
```
```  1898 lemma ennreal_minus_le_iff: "a - b \<le> c \<longleftrightarrow> (a \<le> b + (c::ennreal) \<and> (a = top \<and> b = top \<longrightarrow> c = top))"
```
```  1899   by (cases a; cases b; cases c)
```
```  1900      (auto simp: top_unique top_add add_top ennreal_minus ennreal_plus[symmetric]
```
```  1901            simp del: ennreal_plus)
```
```  1902
```
```  1903 lemma ennreal_le_minus_iff: "a \<le> b - c \<longleftrightarrow> (a + c \<le> (b::ennreal) \<or> (a = 0 \<and> b \<le> c))"
```
```  1904   by (cases a; cases b; cases c)
```
```  1905      (auto simp: top_unique top_add add_top ennreal_minus ennreal_plus[symmetric] ennreal_le_iff2
```
```  1906            simp del: ennreal_plus)
```
```  1907
```
```  1908 lemma diff_add_eq_diff_diff_swap_ennreal: "x - (y + z :: ennreal) = x - y - z"
```
```  1909   by (cases x; cases y; cases z)
```
```  1910      (auto simp: ennreal_plus[symmetric] ennreal_minus_if add_top top_add simp del: ennreal_plus)
```
```  1911
```
```  1912 lemma diff_add_assoc2_ennreal: "b \<le> a \<Longrightarrow> (a - b + c::ennreal) = a + c - b"
```
```  1913   by (cases a; cases b; cases c)
```
```  1914      (auto simp add: ennreal_minus_if ennreal_plus_if add_top top_add top_unique simp del: ennreal_plus)
```
```  1915
```
```  1916 lemma diff_gt_0_iff_gt_ennreal: "0 < a - b \<longleftrightarrow> (a = top \<and> b = top \<or> b < (a::ennreal))"
```
```  1917   by (cases a; cases b) (auto simp: ennreal_minus_if ennreal_less_iff)
```
```  1918
```
```  1919 lemma diff_eq_0_iff_ennreal: "(a - b::ennreal) = 0 \<longleftrightarrow> (a < top \<and> a \<le> b)"
```
```  1920   by (cases a) (auto simp: ennreal_minus_eq_0 diff_eq_0_ennreal)
```
```  1921
```
```  1922 lemma add_diff_self_ennreal: "a + (b - a::ennreal) = (if a \<le> b then b else a)"
```
```  1923   by (auto simp: diff_eq_0_iff_ennreal less_top)
```
```  1924
```
```  1925 lemma diff_add_self_ennreal: "(b - a + a::ennreal) = (if a \<le> b then b else a)"
```
```  1926   by (auto simp: diff_add_cancel_ennreal diff_eq_0_iff_ennreal less_top)
```
```  1927
```
```  1928 lemma ennreal_minus_cancel_iff:
```
```  1929   fixes a b c :: ennreal
```
```  1930   shows "a - b = a - c \<longleftrightarrow> (b = c \<or> (a \<le> b \<and> a \<le> c) \<or> a = top)"
```
```  1931   by (cases a; cases b; cases c) (auto simp: ennreal_minus_if)
```
```  1932
```
```  1933 lemma SUP_diff_ennreal:
```
```  1934   "c < top \<Longrightarrow> (SUP i:I. f i - c :: ennreal) = (SUP i:I. f i) - c"
```
```  1935   by (auto intro!: SUP_eqI ennreal_minus_mono SUP_least intro: SUP_upper
```
```  1936            simp: ennreal_minus_cancel_iff ennreal_minus_le_iff less_top[symmetric])
```
```  1937
```
```  1938 lemma ennreal_SUP_add_right:
```
```  1939   fixes c :: ennreal shows "I \<noteq> {} \<Longrightarrow> c + (SUP i:I. f i) = (SUP i:I. c + f i)"
```
```  1940   using ennreal_SUP_add_left[of I f c] by (simp add: add.commute)
```
```  1941
```
```  1942 lemma SUP_add_directed_ennreal:
```
```  1943   fixes f g :: "_ \<Rightarrow> ennreal"
```
```  1944   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"
```
```  1945   shows "(SUP i:I. f i + g i) = (SUP i:I. f i) + (SUP i:I. g i)"
```
```  1946 proof cases
```
```  1947   assume "I = {}" then show ?thesis
```
```  1948     by (simp add: bot_ereal_def)
```
```  1949 next
```
```  1950   assume "I \<noteq> {}"
```
```  1951   show ?thesis
```
```  1952   proof (rule antisym)
```
```  1953     show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)"
```
```  1954       by (rule SUP_least; intro add_mono SUP_upper)
```
```  1955   next
```
```  1956     have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))"
```
```  1957       by (intro ennreal_SUP_add_left[symmetric] \<open>I \<noteq> {}\<close>)
```
```  1958     also have "\<dots> = (SUP i:I. (SUP j:I. f i + g j))"
```
```  1959       by (intro SUP_cong refl ennreal_SUP_add_right \<open>I \<noteq> {}\<close>)
```
```  1960     also have "\<dots> \<le> (SUP i:I. f i + g i)"
```
```  1961       using directed by (intro SUP_least) (blast intro: SUP_upper2)
```
```  1962     finally show "(SUP i:I. f i) + (SUP i:I. g i) \<le> (SUP i:I. f i + g i)" .
```
```  1963   qed
```
```  1964 qed
```
```  1965
```
```  1966 lemma enn2real_eq_0_iff: "enn2real x = 0 \<longleftrightarrow> x = 0 \<or> x = top"
```
```  1967   by (cases x) auto
```
```  1968
```
```  1969 lemma (in -) continuous_on_diff_ereal:
```
```  1970   "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>) \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> \<bar>g x\<bar> \<noteq> \<infinity>) \<Longrightarrow> continuous_on A (\<lambda>z. f z - g z::ereal)"
```
```  1971   apply (auto simp: continuous_on_def)
```
```  1972   apply (intro tendsto_diff_ereal)
```
```  1973   apply metis+
```
```  1974   done
```
```  1975
```
```  1976 lemma (in -) continuous_on_diff_ennreal:
```
```  1977   "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> top) \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x \<noteq> top) \<Longrightarrow> continuous_on A (\<lambda>z. f z - g z::ennreal)"
```
```  1978   including ennreal.lifting
```
```  1979 proof (transfer fixing: A, simp add: top_ereal_def)
```
```  1980   fix f g :: "'a \<Rightarrow> ereal" assume "\<forall>x. 0 \<le> f x" "\<forall>x. 0 \<le> g x" "continuous_on A f" "continuous_on A g"
```
```  1981   moreover assume "f x \<noteq> \<infinity>" "g x \<noteq> \<infinity>" if "x \<in> A" for x
```
```  1982   ultimately show "continuous_on A (\<lambda>z. max 0 (f z - g z))"
```
```  1983     by (intro continuous_on_max continuous_on_const continuous_on_diff_ereal) auto
```
```  1984 qed
```
```  1985
```
```  1986 lemma (in -) tendsto_diff_ennreal:
```
```  1987   "(f \<longlongrightarrow> x) F \<Longrightarrow> (g \<longlongrightarrow> y) F \<Longrightarrow> x \<noteq> top \<Longrightarrow> y \<noteq> top \<Longrightarrow> ((\<lambda>z. f z - g z::ennreal) \<longlongrightarrow> x - y) F"
```
```  1988   using continuous_on_tendsto_compose[where f="\<lambda>x. fst x - snd x::ennreal" and s="{(x, y). x \<noteq> top \<and> y \<noteq> top}" and g="\<lambda>x. (f x, g x)" and l="(x, y)" and F="F",
```
```  1989     OF continuous_on_diff_ennreal]
```
```  1990   by (auto simp: tendsto_Pair eventually_conj_iff less_top order_tendstoD continuous_on_fst continuous_on_snd continuous_on_id)
```
```  1991
```
```  1992 end
```