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