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