src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
author huffman
Fri Aug 12 09:17:24 2011 -0700 (2011-08-12)
changeset 44170 510ac30f44c0
parent 44167 e81d676d598e
child 44571 bd91b77c4cd6
permissions -rw-r--r--
make Multivariate_Analysis work with separate set type
wenzelm@41983
     1
(*  Title:      HOL/Multivariate_Analysis/Extended_Real_Limits.thy
wenzelm@41983
     2
    Author:     Johannes Hölzl, TU München
wenzelm@41983
     3
    Author:     Robert Himmelmann, TU München
wenzelm@41983
     4
    Author:     Armin Heller, TU München
wenzelm@41983
     5
    Author:     Bogdan Grechuk, University of Edinburgh
wenzelm@41983
     6
*)
hoelzl@41980
     7
hoelzl@41980
     8
header {* Limits on the Extended real number line *}
hoelzl@41980
     9
hoelzl@41980
    10
theory Extended_Real_Limits
hoelzl@43920
    11
  imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real"
hoelzl@41980
    12
begin
hoelzl@41980
    13
hoelzl@43920
    14
lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
hoelzl@43920
    15
  unfolding continuous_on_topological open_ereal_def by auto
hoelzl@41980
    16
hoelzl@43920
    17
lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal"
hoelzl@41980
    18
  using continuous_on_eq_continuous_at[of UNIV] by auto
hoelzl@41980
    19
hoelzl@43920
    20
lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
hoelzl@41980
    21
  using continuous_on_eq_continuous_within[of A] by auto
hoelzl@41980
    22
hoelzl@43920
    23
lemma ereal_open_uminus:
hoelzl@43920
    24
  fixes S :: "ereal set"
hoelzl@41980
    25
  assumes "open S"
hoelzl@41980
    26
  shows "open (uminus ` S)"
hoelzl@43920
    27
  unfolding open_ereal_def
hoelzl@41980
    28
proof (intro conjI impI)
hoelzl@43920
    29
  obtain x y where S: "open (ereal -` S)"
hoelzl@43920
    30
    "\<infinity> \<in> S \<Longrightarrow> {ereal x<..} \<subseteq> S" "-\<infinity> \<in> S \<Longrightarrow> {..< ereal y} \<subseteq> S"
hoelzl@43920
    31
    using `open S` unfolding open_ereal_def by auto
hoelzl@43920
    32
  have "ereal -` uminus ` S = uminus ` (ereal -` S)"
hoelzl@41980
    33
  proof safe
hoelzl@43920
    34
    fix x y assume "ereal x = - y" "y \<in> S"
hoelzl@43920
    35
    then show "x \<in> uminus ` ereal -` S" by (cases y) auto
hoelzl@41980
    36
  next
hoelzl@43920
    37
    fix x assume "ereal x \<in> S"
hoelzl@43920
    38
    then show "- x \<in> ereal -` uminus ` S"
hoelzl@43920
    39
      by (auto intro: image_eqI[of _ _ "ereal x"])
hoelzl@41980
    40
  qed
hoelzl@43920
    41
  then show "open (ereal -` uminus ` S)"
hoelzl@41980
    42
    using S by (auto intro: open_negations)
hoelzl@41980
    43
  { assume "\<infinity> \<in> uminus ` S"
hoelzl@43920
    44
    then have "-\<infinity> \<in> S" by (metis image_iff ereal_uminus_uminus)
hoelzl@43920
    45
    then have "uminus ` {..<ereal y} \<subseteq> uminus ` S" using S by (intro image_mono) auto
hoelzl@43920
    46
    then show "\<exists>x. {ereal x<..} \<subseteq> uminus ` S" using ereal_uminus_lessThan by auto }
hoelzl@41980
    47
  { assume "-\<infinity> \<in> uminus ` S"
hoelzl@43920
    48
    then have "\<infinity> : S" by (metis image_iff ereal_uminus_uminus)
hoelzl@43920
    49
    then have "uminus ` {ereal x<..} <= uminus ` S" using S by (intro image_mono) auto
hoelzl@43920
    50
    then show "\<exists>y. {..<ereal y} <= uminus ` S" using ereal_uminus_greaterThan by auto }
hoelzl@41980
    51
qed
hoelzl@41980
    52
hoelzl@43920
    53
lemma ereal_uminus_complement:
hoelzl@43920
    54
  fixes S :: "ereal set"
hoelzl@41980
    55
  shows "uminus ` (- S) = - uminus ` S"
hoelzl@41980
    56
  by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
hoelzl@41980
    57
hoelzl@43920
    58
lemma ereal_closed_uminus:
hoelzl@43920
    59
  fixes S :: "ereal set"
hoelzl@41980
    60
  assumes "closed S"
hoelzl@41980
    61
  shows "closed (uminus ` S)"
hoelzl@41980
    62
using assms unfolding closed_def
hoelzl@43920
    63
using ereal_open_uminus[of "- S"] ereal_uminus_complement by auto
hoelzl@41980
    64
hoelzl@43920
    65
lemma not_open_ereal_singleton:
hoelzl@43920
    66
  "\<not> (open {a :: ereal})"
hoelzl@41980
    67
proof(rule ccontr)
hoelzl@41980
    68
  assume "\<not> \<not> open {a}" hence a: "open {a}" by auto
hoelzl@41980
    69
  show False
hoelzl@41980
    70
  proof (cases a)
hoelzl@41980
    71
    case MInf
hoelzl@43920
    72
    then obtain y where "{..<ereal y} <= {a}" using a open_MInfty2[of "{a}"] by auto
hoelzl@43920
    73
    hence "ereal(y - 1):{a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
hoelzl@41980
    74
    then show False using `a=(-\<infinity>)` by auto
hoelzl@41980
    75
  next
hoelzl@41980
    76
    case PInf
hoelzl@43920
    77
    then obtain y where "{ereal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto
hoelzl@43920
    78
    hence "ereal(y+1):{a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
hoelzl@41980
    79
    then show False using `a=\<infinity>` by auto
hoelzl@41980
    80
  next
hoelzl@41980
    81
    case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
hoelzl@43920
    82
    from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
hoelzl@41980
    83
    then obtain b where b_def: "a<b & b<a+e"
hoelzl@43920
    84
      using fin ereal_between ereal_dense[of a "a+e"] by auto
hoelzl@43920
    85
    then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
hoelzl@41980
    86
    then show False using b_def e by auto
hoelzl@41980
    87
  qed
hoelzl@41980
    88
qed
hoelzl@41980
    89
hoelzl@43920
    90
lemma ereal_closed_contains_Inf:
hoelzl@43920
    91
  fixes S :: "ereal set"
hoelzl@41980
    92
  assumes "closed S" "S ~= {}"
hoelzl@41980
    93
  shows "Inf S : S"
hoelzl@41980
    94
proof(rule ccontr)
hoelzl@41980
    95
  assume "Inf S \<notin> S" hence a: "open (-S)" "Inf S:(- S)" using assms by auto
hoelzl@41980
    96
  show False
hoelzl@41980
    97
  proof (cases "Inf S")
hoelzl@41980
    98
    case MInf hence "(-\<infinity>) : - S" using a by auto
hoelzl@43920
    99
    then obtain y where "{..<ereal y} <= (-S)" using a open_MInfty2[of "- S"] by auto
hoelzl@43920
   100
    hence "ereal y <= Inf S" by (metis Compl_anti_mono Compl_lessThan atLeast_iff
hoelzl@41980
   101
      complete_lattice_class.Inf_greatest double_complement set_rev_mp)
hoelzl@41980
   102
    then show False using MInf by auto
hoelzl@41980
   103
  next
hoelzl@41980
   104
    case PInf then have "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))
huffman@44170
   105
    then show False using `Inf S ~: S` by simp
hoelzl@41980
   106
  next
hoelzl@41980
   107
    case (real r) then have fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" by simp
hoelzl@43920
   108
    from ereal_open_cont_interval[OF a this] guess e . note e = this
hoelzl@41980
   109
    { fix x assume "x:S" hence "x>=Inf S" by (rule complete_lattice_class.Inf_lower)
hoelzl@43920
   110
      hence *: "x>Inf S-e" using e by (metis fin ereal_between(1) order_less_le_trans)
hoelzl@41980
   111
      { assume "x<Inf S+e" hence "x:{Inf S-e <..< Inf S+e}" using * by auto
hoelzl@41980
   112
        hence False using e `x:S` by auto
hoelzl@41980
   113
      } hence "x>=Inf S+e" by (metis linorder_le_less_linear)
hoelzl@41980
   114
    } hence "Inf S + e <= Inf S" by (metis le_Inf_iff)
hoelzl@41980
   115
    then show False using real e by (cases e) auto
hoelzl@41980
   116
  qed
hoelzl@41980
   117
qed
hoelzl@41980
   118
hoelzl@43920
   119
lemma ereal_closed_contains_Sup:
hoelzl@43920
   120
  fixes S :: "ereal set"
hoelzl@41980
   121
  assumes "closed S" "S ~= {}"
hoelzl@41980
   122
  shows "Sup S : S"
hoelzl@41980
   123
proof-
hoelzl@43920
   124
  have "closed (uminus ` S)" by (metis assms(1) ereal_closed_uminus)
hoelzl@43920
   125
  hence "Inf (uminus ` S) : uminus ` S" using assms ereal_closed_contains_Inf[of "uminus ` S"] by auto
hoelzl@43920
   126
  hence "- Sup S : uminus ` S" using ereal_Sup_uminus_image_eq[of "uminus ` S"] by (auto simp: image_image)
hoelzl@43920
   127
  thus ?thesis by (metis imageI ereal_uminus_uminus ereal_minus_minus_image)
hoelzl@41980
   128
qed
hoelzl@41980
   129
hoelzl@43920
   130
lemma ereal_open_closed_aux:
hoelzl@43920
   131
  fixes S :: "ereal set"
hoelzl@41980
   132
  assumes "open S" "closed S"
hoelzl@41980
   133
  assumes S: "(-\<infinity>) ~: S"
hoelzl@41980
   134
  shows "S = {}"
hoelzl@41980
   135
proof(rule ccontr)
hoelzl@41980
   136
  assume "S ~= {}"
hoelzl@43920
   137
  hence *: "(Inf S):S" by (metis assms(2) ereal_closed_contains_Inf)
hoelzl@41980
   138
  { assume "Inf S=(-\<infinity>)" hence False using * assms(3) by auto }
hoelzl@41980
   139
  moreover
hoelzl@41980
   140
  { assume "Inf S=\<infinity>" hence "S={\<infinity>}" by (metis Inf_eq_PInfty `S ~= {}`)
hoelzl@43920
   141
    hence False by (metis assms(1) not_open_ereal_singleton) }
hoelzl@41980
   142
  moreover
hoelzl@41980
   143
  { assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
hoelzl@43920
   144
    from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this
hoelzl@41980
   145
    then obtain b where b_def: "Inf S-e<b & b<Inf S"
hoelzl@43920
   146
      using fin ereal_between[of "Inf S" e] ereal_dense[of "Inf S-e"] by auto
hoelzl@43920
   147
    hence "b: {Inf S-e <..< Inf S+e}" using e fin ereal_between[of "Inf S" e] by auto
hoelzl@41980
   148
    hence "b:S" using e by auto
hoelzl@41980
   149
    hence False using b_def by (metis complete_lattice_class.Inf_lower leD)
hoelzl@41980
   150
  } ultimately show False by auto
hoelzl@41980
   151
qed
hoelzl@41980
   152
hoelzl@43920
   153
lemma ereal_open_closed:
hoelzl@43920
   154
  fixes S :: "ereal set"
hoelzl@41980
   155
  shows "(open S & closed S) <-> (S = {} | S = UNIV)"
hoelzl@41980
   156
proof-
hoelzl@41980
   157
{ assume lhs: "open S & closed S"
hoelzl@43920
   158
  { assume "(-\<infinity>) ~: S" hence "S={}" using lhs ereal_open_closed_aux by auto }
hoelzl@41980
   159
  moreover
hoelzl@43920
   160
  { assume "(-\<infinity>) : S" hence "(- S)={}" using lhs ereal_open_closed_aux[of "-S"] by auto }
hoelzl@41980
   161
  ultimately have "S = {} | S = UNIV" by auto
hoelzl@41980
   162
} thus ?thesis by auto
hoelzl@41980
   163
qed
hoelzl@41980
   164
hoelzl@43920
   165
lemma ereal_open_affinity_pos:
hoelzl@43923
   166
  fixes S :: "ereal set"
hoelzl@41980
   167
  assumes "open S" and m: "m \<noteq> \<infinity>" "0 < m" and t: "\<bar>t\<bar> \<noteq> \<infinity>"
hoelzl@41980
   168
  shows "open ((\<lambda>x. m * x + t) ` S)"
hoelzl@41980
   169
proof -
hoelzl@43920
   170
  obtain r where r[simp]: "m = ereal r" using m by (cases m) auto
hoelzl@43920
   171
  obtain p where p[simp]: "t = ereal p" using t by auto
hoelzl@41980
   172
  have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0" using m by auto
hoelzl@43920
   173
  from `open S`[THEN ereal_openE] guess l u . note T = this
hoelzl@41980
   174
  let ?f = "(\<lambda>x. m * x + t)"
hoelzl@43920
   175
  show ?thesis unfolding open_ereal_def
hoelzl@41980
   176
  proof (intro conjI impI exI subsetI)
hoelzl@43920
   177
    have "ereal -` ?f ` S = (\<lambda>x. r * x + p) ` (ereal -` S)"
hoelzl@41980
   178
    proof safe
hoelzl@43920
   179
      fix x y assume "ereal y = m * x + t" "x \<in> S"
hoelzl@43920
   180
      then show "y \<in> (\<lambda>x. r * x + p) ` ereal -` S"
hoelzl@41980
   181
        using `r \<noteq> 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm)
hoelzl@41980
   182
    qed force
hoelzl@43920
   183
    then show "open (ereal -` ?f ` S)"
hoelzl@41980
   184
      using open_affinity[OF T(1) `r \<noteq> 0`] by (auto simp: ac_simps)
hoelzl@41980
   185
  next
hoelzl@41980
   186
    assume "\<infinity> \<in> ?f`S" with `0 < r` have "\<infinity> \<in> S" by auto
hoelzl@43920
   187
    fix x assume "x \<in> {ereal (r * l + p)<..}"
hoelzl@43920
   188
    then have [simp]: "ereal (r * l + p) < x" by auto
hoelzl@41980
   189
    show "x \<in> ?f`S"
hoelzl@41980
   190
    proof (rule image_eqI)
hoelzl@41980
   191
      show "x = m * ((x - t) / m) + t"
hoelzl@43920
   192
        using m t by (cases rule: ereal3_cases[of m x t]) auto
hoelzl@43920
   193
      have "ereal l < (x - t)/m"
hoelzl@43920
   194
        using m t by (simp add: ereal_less_divide_pos ereal_less_minus)
hoelzl@41980
   195
      then show "(x - t)/m \<in> S" using T(2)[OF `\<infinity> \<in> S`] by auto
hoelzl@41980
   196
    qed
hoelzl@41980
   197
  next
hoelzl@41980
   198
    assume "-\<infinity> \<in> ?f`S" with `0 < r` have "-\<infinity> \<in> S" by auto
hoelzl@43920
   199
    fix x assume "x \<in> {..<ereal (r * u + p)}"
hoelzl@43920
   200
    then have [simp]: "x < ereal (r * u + p)" by auto
hoelzl@41980
   201
    show "x \<in> ?f`S"
hoelzl@41980
   202
    proof (rule image_eqI)
hoelzl@41980
   203
      show "x = m * ((x - t) / m) + t"
hoelzl@43920
   204
        using m t by (cases rule: ereal3_cases[of m x t]) auto
hoelzl@43920
   205
      have "(x - t)/m < ereal u"
hoelzl@43920
   206
        using m t by (simp add: ereal_divide_less_pos ereal_minus_less)
hoelzl@41980
   207
      then show "(x - t)/m \<in> S" using T(3)[OF `-\<infinity> \<in> S`] by auto
hoelzl@41980
   208
    qed
hoelzl@41980
   209
  qed
hoelzl@41980
   210
qed
hoelzl@41980
   211
hoelzl@43920
   212
lemma ereal_open_affinity:
hoelzl@43923
   213
  fixes S :: "ereal set"
hoelzl@41980
   214
  assumes "open S" and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" and t: "\<bar>t\<bar> \<noteq> \<infinity>"
hoelzl@41980
   215
  shows "open ((\<lambda>x. m * x + t) ` S)"
hoelzl@41980
   216
proof cases
hoelzl@41980
   217
  assume "0 < m" then show ?thesis
hoelzl@43920
   218
    using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m by auto
hoelzl@41980
   219
next
hoelzl@41980
   220
  assume "\<not> 0 < m" then
hoelzl@41980
   221
  have "0 < -m" using `m \<noteq> 0` by (cases m) auto
hoelzl@41980
   222
  then have m: "-m \<noteq> \<infinity>" "0 < -m" using `\<bar>m\<bar> \<noteq> \<infinity>`
hoelzl@43920
   223
    by (auto simp: ereal_uminus_eq_reorder)
hoelzl@43920
   224
  from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t]
hoelzl@41980
   225
  show ?thesis unfolding image_image by simp
hoelzl@41980
   226
qed
hoelzl@41980
   227
hoelzl@43920
   228
lemma ereal_lim_mult:
hoelzl@43920
   229
  fixes X :: "'a \<Rightarrow> ereal"
hoelzl@41980
   230
  assumes lim: "(X ---> L) net" and a: "\<bar>a\<bar> \<noteq> \<infinity>"
hoelzl@41980
   231
  shows "((\<lambda>i. a * X i) ---> a * L) net"
hoelzl@41980
   232
proof cases
hoelzl@41980
   233
  assume "a \<noteq> 0"
hoelzl@41980
   234
  show ?thesis
hoelzl@41980
   235
  proof (rule topological_tendstoI)
hoelzl@41980
   236
    fix S assume "open S" "a * L \<in> S"
hoelzl@41980
   237
    have "a * L / a = L"
hoelzl@43920
   238
      using `a \<noteq> 0` a by (cases rule: ereal2_cases[of a L]) auto
hoelzl@41980
   239
    then have L: "L \<in> ((\<lambda>x. x / a) ` S)"
hoelzl@41980
   240
      using `a * L \<in> S` by (force simp: image_iff)
hoelzl@41980
   241
    moreover have "open ((\<lambda>x. x / a) ` S)"
hoelzl@43920
   242
      using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a
hoelzl@43920
   243
      by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps)
hoelzl@41980
   244
    note * = lim[THEN topological_tendstoD, OF this L]
hoelzl@41980
   245
    { fix x from a `a \<noteq> 0` have "a * (x / a) = x"
hoelzl@43920
   246
        by (cases rule: ereal2_cases[of a x]) auto }
hoelzl@41980
   247
    note this[simp]
hoelzl@41980
   248
    show "eventually (\<lambda>x. a * X x \<in> S) net"
hoelzl@41980
   249
      by (rule eventually_mono[OF _ *]) auto
hoelzl@41980
   250
  qed
huffman@44125
   251
qed (auto intro: tendsto_const)
hoelzl@41980
   252
hoelzl@43920
   253
lemma ereal_lim_uminus:
hoelzl@43920
   254
  fixes X :: "'a \<Rightarrow> ereal" shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net"
hoelzl@43920
   255
  using ereal_lim_mult[of X L net "ereal (-1)"]
hoelzl@43920
   256
        ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"]
hoelzl@41980
   257
  by (auto simp add: algebra_simps)
hoelzl@41980
   258
hoelzl@43920
   259
lemma Lim_bounded2_ereal:
hoelzl@43920
   260
  assumes lim:"f ----> (l :: ereal)"
hoelzl@41980
   261
  and ge: "ALL n>=N. f n >= C"
hoelzl@41980
   262
  shows "l>=C"
hoelzl@41980
   263
proof-
hoelzl@41980
   264
def g == "(%i. -(f i))"
hoelzl@43920
   265
{ fix n assume "n>=N" hence "g n <= -C" using assms ereal_minus_le_minus g_def by auto }
hoelzl@41980
   266
hence "ALL n>=N. g n <= -C" by auto
hoelzl@43920
   267
moreover have limg: "g ----> (-l)" using g_def ereal_lim_uminus lim by auto
hoelzl@43920
   268
ultimately have "-l <= -C" using Lim_bounded_ereal[of g "-l" _ "-C"] by auto
hoelzl@43920
   269
from this show ?thesis using ereal_minus_le_minus by auto
hoelzl@41980
   270
qed
hoelzl@41980
   271
hoelzl@41980
   272
hoelzl@43923
   273
lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
hoelzl@41980
   274
proof
hoelzl@41980
   275
  assume "x = -\<infinity>" then have "{x..} = UNIV" by auto
hoelzl@41980
   276
  then show "open {x..}" by auto
hoelzl@41980
   277
next
hoelzl@41980
   278
  assume "open {x..}"
hoelzl@41980
   279
  then have "open {x..} \<and> closed {x..}" by auto
hoelzl@43920
   280
  then have "{x..} = UNIV" unfolding ereal_open_closed by auto
hoelzl@43920
   281
  then show "x = -\<infinity>" by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
hoelzl@41980
   282
qed
hoelzl@41980
   283
hoelzl@43920
   284
lemma ereal_open_mono_set:
hoelzl@43920
   285
  fixes S :: "ereal set"
hoelzl@41980
   286
  defines "a \<equiv> Inf S"
huffman@44170
   287
  shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})"
hoelzl@43920
   288
  by (metis Inf_UNIV a_def atLeast_eq_UNIV_iff ereal_open_atLeast
hoelzl@43920
   289
            ereal_open_closed mono_set_iff open_ereal_greaterThan)
hoelzl@41980
   290
hoelzl@43920
   291
lemma ereal_closed_mono_set:
hoelzl@43920
   292
  fixes S :: "ereal set"
huffman@44170
   293
  shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
hoelzl@43920
   294
  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
hoelzl@43920
   295
            ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
hoelzl@41980
   296
hoelzl@43920
   297
lemma ereal_Liminf_Sup_monoset:
hoelzl@43920
   298
  fixes f :: "'a => ereal"
huffman@44170
   299
  shows "Liminf net f = Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
hoelzl@41980
   300
  unfolding Liminf_Sup
hoelzl@41980
   301
proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
huffman@44170
   302
  fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono_set S" "l \<in> S"
hoelzl@41980
   303
  then have "S = UNIV \<or> S = {Inf S <..}"
hoelzl@43920
   304
    using ereal_open_mono_set[of S] by auto
hoelzl@41980
   305
  then show "eventually (\<lambda>x. f x \<in> S) net"
hoelzl@41980
   306
  proof
hoelzl@41980
   307
    assume S: "S = {Inf S<..}"
hoelzl@41980
   308
    then have "Inf S < l" using `l \<in> S` by auto
hoelzl@41980
   309
    then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto
hoelzl@41980
   310
    then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
hoelzl@41980
   311
  qed auto
hoelzl@41980
   312
next
huffman@44170
   313
  fix l y assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "y < l"
hoelzl@41980
   314
  have "eventually  (\<lambda>x. f x \<in> {y <..}) net"
hoelzl@41980
   315
    using `y < l` by (intro S[rule_format]) auto
hoelzl@41980
   316
  then show "eventually (\<lambda>x. y < f x) net" by auto
hoelzl@41980
   317
qed
hoelzl@41980
   318
hoelzl@43920
   319
lemma ereal_Limsup_Inf_monoset:
hoelzl@43920
   320
  fixes f :: "'a => ereal"
huffman@44170
   321
  shows "Limsup net f = Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
hoelzl@41980
   322
  unfolding Limsup_Inf
hoelzl@41980
   323
proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
huffman@44170
   324
  fix l S assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono_set (uminus`S)" "l \<in> S"
huffman@44170
   325
  then have "open (uminus`S) \<and> mono_set (uminus`S)" by (simp add: ereal_open_uminus)
hoelzl@41980
   326
  then have "S = UNIV \<or> S = {..< Sup S}"
hoelzl@43920
   327
    unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp
hoelzl@41980
   328
  then show "eventually (\<lambda>x. f x \<in> S) net"
hoelzl@41980
   329
  proof
hoelzl@41980
   330
    assume S: "S = {..< Sup S}"
hoelzl@41980
   331
    then have "l < Sup S" using `l \<in> S` by auto
hoelzl@41980
   332
    then have "eventually (\<lambda>x. f x < Sup S) net" using ev by auto
hoelzl@41980
   333
    then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
hoelzl@41980
   334
  qed auto
hoelzl@41980
   335
next
huffman@44170
   336
  fix l y assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "l < y"
hoelzl@41980
   337
  have "eventually  (\<lambda>x. f x \<in> {..< y}) net"
hoelzl@41980
   338
    using `l < y` by (intro S[rule_format]) auto
hoelzl@41980
   339
  then show "eventually (\<lambda>x. f x < y) net" by auto
hoelzl@41980
   340
qed
hoelzl@41980
   341
hoelzl@41980
   342
hoelzl@43920
   343
lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)"
hoelzl@43920
   344
  using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto
hoelzl@41980
   345
hoelzl@43920
   346
lemma ereal_Limsup_uminus:
hoelzl@43920
   347
  fixes f :: "'a => ereal"
hoelzl@41980
   348
  shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
hoelzl@41980
   349
proof -
hoelzl@43920
   350
  { fix P l have "(\<exists>x. (l::ereal) = -x \<and> P x) \<longleftrightarrow> P (-l)" by (auto intro!: exI[of _ "-l"]) }
hoelzl@41980
   351
  note Ex_cancel = this
hoelzl@43920
   352
  { fix P :: "ereal set \<Rightarrow> bool" have "(\<forall>S. P S) \<longleftrightarrow> (\<forall>S. P (uminus`S))"
hoelzl@41980
   353
      apply auto by (erule_tac x="uminus`S" in allE) (auto simp: image_image) }
hoelzl@41980
   354
  note add_uminus_image = this
hoelzl@43920
   355
  { fix x S have "(x::ereal) \<in> uminus`S \<longleftrightarrow> -x\<in>S" by (auto intro!: image_eqI[of _ _ "-x"]) }
hoelzl@41980
   356
  note remove_uminus_image = this
hoelzl@41980
   357
  show ?thesis
hoelzl@43920
   358
    unfolding ereal_Limsup_Inf_monoset ereal_Liminf_Sup_monoset
hoelzl@43920
   359
    unfolding ereal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel
hoelzl@41980
   360
    by (subst add_uminus_image) (simp add: open_uminus_iff remove_uminus_image)
hoelzl@41980
   361
qed
hoelzl@41980
   362
hoelzl@43920
   363
lemma ereal_Liminf_uminus:
hoelzl@43920
   364
  fixes f :: "'a => ereal"
hoelzl@41980
   365
  shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)"
hoelzl@43920
   366
  using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
hoelzl@41980
   367
hoelzl@43920
   368
lemma ereal_Lim_uminus:
hoelzl@43920
   369
  fixes f :: "'a \<Rightarrow> ereal" shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net"
hoelzl@41980
   370
  using
hoelzl@43920
   371
    ereal_lim_mult[of f f0 net "- 1"]
hoelzl@43920
   372
    ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
hoelzl@43920
   373
  by (auto simp: ereal_uminus_reorder)
hoelzl@41980
   374
hoelzl@41980
   375
lemma lim_imp_Limsup:
hoelzl@43920
   376
  fixes f :: "'a => ereal"
hoelzl@41980
   377
  assumes "\<not> trivial_limit net"
hoelzl@41980
   378
  assumes lim: "(f ---> f0) net"
hoelzl@41980
   379
  shows "Limsup net f = f0"
hoelzl@43920
   380
  using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]
hoelzl@43920
   381
     ereal_Liminf_uminus[of net f] assms by simp
hoelzl@41980
   382
hoelzl@41980
   383
lemma Liminf_PInfty:
hoelzl@43920
   384
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@41980
   385
  assumes "\<not> trivial_limit net"
hoelzl@41980
   386
  shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
hoelzl@41980
   387
proof (intro lim_imp_Liminf iffI assms)
hoelzl@41980
   388
  assume rhs: "Liminf net f = \<infinity>"
hoelzl@43923
   389
  { fix S :: "ereal set" assume "open S & \<infinity> : S"
hoelzl@43920
   390
    then obtain m where "{ereal m<..} <= S" using open_PInfty2 by auto
hoelzl@43920
   391
    moreover have "eventually (\<lambda>x. f x \<in> {ereal m<..}) net"
hoelzl@43920
   392
      using rhs unfolding Liminf_Sup top_ereal_def[symmetric] Sup_eq_top_iff
hoelzl@43920
   393
      by (auto elim!: allE[where x="ereal m"] simp: top_ereal_def)
hoelzl@41980
   394
    ultimately have "eventually (%x. f x : S) net" apply (subst eventually_mono) by auto
hoelzl@41980
   395
  } then show "(f ---> \<infinity>) net" unfolding tendsto_def by auto
hoelzl@41980
   396
qed
hoelzl@41980
   397
hoelzl@41980
   398
lemma Limsup_MInfty:
hoelzl@43920
   399
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@41980
   400
  assumes "\<not> trivial_limit net"
hoelzl@41980
   401
  shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
hoelzl@43920
   402
  using assms ereal_Lim_uminus[of f "-\<infinity>"] Liminf_PInfty[of _ "\<lambda>x. - (f x)"]
hoelzl@43920
   403
        ereal_Liminf_uminus[of _ f] by (auto simp: ereal_uminus_eq_reorder)
hoelzl@41980
   404
hoelzl@43920
   405
lemma ereal_Liminf_eq_Limsup:
hoelzl@43920
   406
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@41980
   407
  assumes ntriv: "\<not> trivial_limit net"
hoelzl@41980
   408
  assumes lim: "Liminf net f = f0" "Limsup net f = f0"
hoelzl@41980
   409
  shows "(f ---> f0) net"
hoelzl@41980
   410
proof (cases f0)
hoelzl@41980
   411
  case PInf then show ?thesis using Liminf_PInfty[OF ntriv] lim by auto
hoelzl@41980
   412
next
hoelzl@41980
   413
  case MInf then show ?thesis using Limsup_MInfty[OF ntriv] lim by auto
hoelzl@41980
   414
next
hoelzl@41980
   415
  case (real r)
hoelzl@41980
   416
  show "(f ---> f0) net"
hoelzl@41980
   417
  proof (rule topological_tendstoI)
hoelzl@41980
   418
    fix S assume "open S""f0 \<in> S"
hoelzl@41980
   419
    then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
hoelzl@43920
   420
      using ereal_open_cont_interval2[of S f0] real lim by auto
hoelzl@41980
   421
    then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
hoelzl@41980
   422
      unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff
huffman@44142
   423
      by (auto intro!: eventually_conj)
hoelzl@41980
   424
    with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
hoelzl@41980
   425
      by (rule_tac eventually_mono) auto
hoelzl@41980
   426
  qed
hoelzl@41980
   427
qed
hoelzl@41980
   428
hoelzl@43920
   429
lemma ereal_Liminf_eq_Limsup_iff:
hoelzl@43920
   430
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@41980
   431
  assumes "\<not> trivial_limit net"
hoelzl@41980
   432
  shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
hoelzl@43920
   433
  by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
hoelzl@41980
   434
hoelzl@41980
   435
lemma limsup_INFI_SUPR:
hoelzl@43920
   436
  fixes f :: "nat \<Rightarrow> ereal"
hoelzl@41980
   437
  shows "limsup f = (INF n. SUP m:{n..}. f m)"
hoelzl@43920
   438
  using ereal_Limsup_uminus[of sequentially "\<lambda>x. - f x"]
hoelzl@43920
   439
  by (simp add: liminf_SUPR_INFI ereal_INFI_uminus ereal_SUPR_uminus)
hoelzl@41980
   440
hoelzl@41980
   441
lemma liminf_PInfty:
hoelzl@43920
   442
  fixes X :: "nat => ereal"
hoelzl@41980
   443
  shows "X ----> \<infinity> <-> liminf X = \<infinity>"
hoelzl@41980
   444
by (metis Liminf_PInfty trivial_limit_sequentially)
hoelzl@41980
   445
hoelzl@41980
   446
lemma limsup_MInfty:
hoelzl@43920
   447
  fixes X :: "nat => ereal"
hoelzl@41980
   448
  shows "X ----> (-\<infinity>) <-> limsup X = (-\<infinity>)"
hoelzl@41980
   449
by (metis Limsup_MInfty trivial_limit_sequentially)
hoelzl@41980
   450
hoelzl@43920
   451
lemma ereal_lim_mono:
hoelzl@43920
   452
  fixes X Y :: "nat => ereal"
hoelzl@41980
   453
  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
hoelzl@41980
   454
  assumes "X ----> x" "Y ----> y"
hoelzl@41980
   455
  shows "x <= y"
hoelzl@43920
   456
  by (metis ereal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)
hoelzl@41980
   457
hoelzl@43920
   458
lemma incseq_le_ereal:
hoelzl@43920
   459
  fixes X :: "nat \<Rightarrow> ereal"
hoelzl@41980
   460
  assumes inc: "incseq X" and lim: "X ----> L"
hoelzl@41980
   461
  shows "X N \<le> L"
hoelzl@41980
   462
  using inc
huffman@44125
   463
  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
hoelzl@41980
   464
hoelzl@43920
   465
lemma decseq_ge_ereal: assumes dec: "decseq X"
hoelzl@43920
   466
  and lim: "X ----> (L::ereal)" shows "X N >= L"
hoelzl@41980
   467
  using dec
huffman@44125
   468
  by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
hoelzl@41980
   469
hoelzl@41980
   470
lemma liminf_bounded_open:
hoelzl@43920
   471
  fixes x :: "nat \<Rightarrow> ereal"
huffman@44170
   472
  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))" 
hoelzl@41980
   473
  (is "_ \<longleftrightarrow> ?P x0")
hoelzl@41980
   474
proof
hoelzl@41980
   475
  assume "?P x0" then show "x0 \<le> liminf x"
hoelzl@43920
   476
    unfolding ereal_Liminf_Sup_monoset eventually_sequentially
hoelzl@41980
   477
    by (intro complete_lattice_class.Sup_upper) auto
hoelzl@41980
   478
next
hoelzl@41980
   479
  assume "x0 \<le> liminf x"
huffman@44170
   480
  { fix S :: "ereal set" assume om: "open S & mono_set S & x0:S"
hoelzl@41980
   481
    { assume "S = UNIV" hence "EX N. (ALL n>=N. x n : S)" by auto }
hoelzl@41980
   482
    moreover
hoelzl@41980
   483
    { assume "~(S=UNIV)"
hoelzl@43920
   484
      then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
hoelzl@41980
   485
      hence "B<x0" using om by auto
hoelzl@41980
   486
      hence "EX N. ALL n>=N. x n : S" unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
hoelzl@41980
   487
    } ultimately have "EX N. (ALL n>=N. x n : S)" by auto
hoelzl@41980
   488
  } then show "?P x0" by auto
hoelzl@41980
   489
qed
hoelzl@41980
   490
hoelzl@41980
   491
lemma limsup_subseq_mono:
hoelzl@43920
   492
  fixes X :: "nat \<Rightarrow> ereal"
hoelzl@41980
   493
  assumes "subseq r"
hoelzl@41980
   494
  shows "limsup (X \<circ> r) \<le> limsup X"
hoelzl@41980
   495
proof-
hoelzl@41980
   496
  have "(\<lambda>n. - X n) \<circ> r = (\<lambda>n. - (X \<circ> r) n)" by (simp add: fun_eq_iff)
hoelzl@41980
   497
  then have "- limsup X \<le> - limsup (X \<circ> r)"
hoelzl@41980
   498
     using liminf_subseq_mono[of r "(%n. - X n)"]
hoelzl@43920
   499
       ereal_Liminf_uminus[of sequentially X]
hoelzl@43920
   500
       ereal_Liminf_uminus[of sequentially "X o r"] assms by auto
hoelzl@41980
   501
  then show ?thesis by auto
hoelzl@41980
   502
qed
hoelzl@41980
   503
hoelzl@41980
   504
lemma bounded_abs:
hoelzl@41980
   505
  assumes "(a::real)<=x" "x<=b"
hoelzl@41980
   506
  shows "abs x <= max (abs a) (abs b)"
hoelzl@41980
   507
by (metis abs_less_iff assms leI le_max_iff_disj less_eq_real_def less_le_not_le less_minus_iff minus_minus)
hoelzl@41980
   508
hoelzl@41980
   509
lemma bounded_increasing_convergent2: fixes f::"nat => real"
hoelzl@41980
   510
  assumes "ALL n. f n <= B"  "ALL n m. n>=m --> f n >= f m"
hoelzl@41980
   511
  shows "EX l. (f ---> l) sequentially"
hoelzl@41980
   512
proof-
hoelzl@41980
   513
def N == "max (abs (f 0)) (abs B)"
hoelzl@41980
   514
{ fix n have "abs (f n) <= N" unfolding N_def apply (subst bounded_abs) using assms by auto }
hoelzl@41980
   515
hence "bounded {f n| n::nat. True}" unfolding bounded_real by auto
hoelzl@41980
   516
from this show ?thesis apply(rule Topology_Euclidean_Space.bounded_increasing_convergent)
hoelzl@41980
   517
   using assms by auto
hoelzl@41980
   518
qed
hoelzl@43920
   519
lemma lim_ereal_increasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
hoelzl@43920
   520
  obtains l where "f ----> (l::ereal)"
hoelzl@41980
   521
proof(cases "f = (\<lambda>x. - \<infinity>)")
huffman@44125
   522
  case True then show thesis using tendsto_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
hoelzl@41980
   523
next
hoelzl@41980
   524
  case False
hoelzl@41980
   525
  from this obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
hoelzl@41980
   526
  have "ALL n>=N. f n >= f N" using assms by auto
hoelzl@41980
   527
  hence minf: "ALL n>=N. f n > (-\<infinity>)" using N_def by auto
hoelzl@41980
   528
  def Y == "(%n. (if n>=N then f n else f N))"
hoelzl@41980
   529
  hence incy: "!!n m. n>=m ==> Y n >= Y m" using assms by auto
hoelzl@41980
   530
  from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto
hoelzl@41980
   531
  show thesis
hoelzl@43920
   532
  proof(cases "EX B. ALL n. f n < ereal B")
hoelzl@41980
   533
    case False thus thesis apply- apply(rule that[of \<infinity>]) unfolding Lim_PInfty not_ex not_all
hoelzl@41980
   534
    apply safe apply(erule_tac x=B in allE,safe) apply(rule_tac x=x in exI,safe)
hoelzl@41980
   535
    apply(rule order_trans[OF _ assms[rule_format]]) by auto
hoelzl@41980
   536
  next case True then guess B ..
hoelzl@43920
   537
    hence "ALL n. Y n < ereal B" using Y_def by auto note B = this[rule_format]
hoelzl@41980
   538
    { fix n have "Y n < \<infinity>" using B[of n] apply (subst less_le_trans) by auto
hoelzl@41980
   539
      hence "Y n ~= \<infinity> & Y n ~= (-\<infinity>)" using minfy by auto
hoelzl@41980
   540
    } hence *: "ALL n. \<bar>Y n\<bar> \<noteq> \<infinity>" by auto
hoelzl@41980
   541
    { fix n have "real (Y n) < B" proof- case goal1 thus ?case
hoelzl@43920
   542
        using B[of n] apply-apply(subst(asm) ereal_real'[THEN sym]) defer defer
hoelzl@43920
   543
        unfolding ereal_less using * by auto
hoelzl@41980
   544
      qed
hoelzl@41980
   545
    }
hoelzl@41980
   546
    hence B': "ALL n. (real (Y n) <= B)" using less_imp_le by auto
hoelzl@41980
   547
    have "EX l. (%n. real (Y n)) ----> l"
hoelzl@41980
   548
      apply(rule bounded_increasing_convergent2)
hoelzl@41980
   549
    proof safe show "!!n. real (Y n) <= B" using B' by auto
hoelzl@41980
   550
      fix n m::nat assume "n<=m"
hoelzl@43920
   551
      hence "ereal (real (Y n)) <= ereal (real (Y m))"
hoelzl@43920
   552
        using incy[rule_format,of n m] apply(subst ereal_real)+
hoelzl@41980
   553
        using *[rule_format, of n] *[rule_format, of m] by auto
hoelzl@41980
   554
      thus "real (Y n) <= real (Y m)" by auto
hoelzl@41980
   555
    qed then guess l .. note l=this
hoelzl@43920
   556
    have "Y ----> ereal l" using l apply-apply(subst(asm) lim_ereal[THEN sym])
hoelzl@43920
   557
    unfolding ereal_real using * by auto
hoelzl@43920
   558
    thus thesis apply-apply(rule that[of "ereal l"])
hoelzl@41980
   559
       apply (subst tail_same_limit[of Y _ N]) using Y_def by auto
hoelzl@41980
   560
  qed
hoelzl@41980
   561
qed
hoelzl@41980
   562
hoelzl@43920
   563
lemma lim_ereal_decreasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n <= f m"
hoelzl@43920
   564
  obtains l where "f ----> (l::ereal)"
hoelzl@41980
   565
proof -
hoelzl@43920
   566
  from lim_ereal_increasing[of "\<lambda>x. - f x"] assms
hoelzl@41980
   567
  obtain l where "(\<lambda>x. - f x) ----> l" by auto
hoelzl@43920
   568
  from ereal_lim_mult[OF this, of "- 1"] show thesis
hoelzl@43920
   569
    by (intro that[of "-l"]) (simp add: ereal_uminus_eq_reorder)
hoelzl@41980
   570
qed
hoelzl@41980
   571
hoelzl@43920
   572
lemma compact_ereal:
hoelzl@43920
   573
  fixes X :: "nat \<Rightarrow> ereal"
hoelzl@41980
   574
  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
hoelzl@41980
   575
proof -
hoelzl@41980
   576
  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
hoelzl@41980
   577
    using seq_monosub[of X] unfolding comp_def by auto
hoelzl@41980
   578
  then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
hoelzl@41980
   579
    by (auto simp add: monoseq_def)
hoelzl@41980
   580
  then obtain l where "(X\<circ>r) ----> l"
hoelzl@43920
   581
     using lim_ereal_increasing[of "X \<circ> r"] lim_ereal_decreasing[of "X \<circ> r"] by auto
hoelzl@41980
   582
  then show ?thesis using `subseq r` by auto
hoelzl@41980
   583
qed
hoelzl@41980
   584
hoelzl@43920
   585
lemma ereal_Sup_lim:
hoelzl@43920
   586
  assumes "\<And>n. b n \<in> s" "b ----> (a::ereal)"
hoelzl@41980
   587
  shows "a \<le> Sup s"
hoelzl@43920
   588
by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
hoelzl@41980
   589
hoelzl@43920
   590
lemma ereal_Inf_lim:
hoelzl@43920
   591
  assumes "\<And>n. b n \<in> s" "b ----> (a::ereal)"
hoelzl@41980
   592
  shows "Inf s \<le> a"
hoelzl@43920
   593
by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
hoelzl@41980
   594
hoelzl@43920
   595
lemma SUP_Lim_ereal:
hoelzl@43920
   596
  fixes X :: "nat \<Rightarrow> ereal" assumes "incseq X" "X ----> l" shows "(SUP n. X n) = l"
hoelzl@43920
   597
proof (rule ereal_SUPI)
hoelzl@41980
   598
  fix n from assms show "X n \<le> l"
hoelzl@43920
   599
    by (intro incseq_le_ereal) (simp add: incseq_def)
hoelzl@41980
   600
next
hoelzl@41980
   601
  fix y assume "\<And>n. n \<in> UNIV \<Longrightarrow> X n \<le> y"
hoelzl@43920
   602
  with ereal_Sup_lim[OF _ `X ----> l`, of "{..y}"]
hoelzl@41980
   603
  show "l \<le> y" by auto
hoelzl@41980
   604
qed
hoelzl@41980
   605
hoelzl@43920
   606
lemma LIMSEQ_ereal_SUPR:
hoelzl@43920
   607
  fixes X :: "nat \<Rightarrow> ereal" assumes "incseq X" shows "X ----> (SUP n. X n)"
hoelzl@43920
   608
proof (rule lim_ereal_increasing)
hoelzl@41980
   609
  fix n m :: nat assume "m \<le> n" then show "X m \<le> X n"
hoelzl@41980
   610
    using `incseq X` by (simp add: incseq_def)
hoelzl@41980
   611
next
hoelzl@41980
   612
  fix l assume "X ----> l"
hoelzl@43920
   613
  with SUP_Lim_ereal[of X, OF assms this] show ?thesis by simp
hoelzl@41980
   614
qed
hoelzl@41980
   615
hoelzl@43920
   616
lemma INF_Lim_ereal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::ereal)"
hoelzl@43920
   617
  using SUP_Lim_ereal[of "\<lambda>i. - X i" "- l"]
hoelzl@43920
   618
  by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
hoelzl@41980
   619
hoelzl@43920
   620
lemma LIMSEQ_ereal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: ereal)"
hoelzl@43920
   621
  using LIMSEQ_ereal_SUPR[of "\<lambda>i. - X i"]
hoelzl@43920
   622
  by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
hoelzl@41980
   623
hoelzl@41980
   624
lemma SUP_eq_LIMSEQ:
hoelzl@41980
   625
  assumes "mono f"
hoelzl@43920
   626
  shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
hoelzl@41980
   627
proof
hoelzl@43920
   628
  have inc: "incseq (\<lambda>i. ereal (f i))"
hoelzl@41980
   629
    using `mono f` unfolding mono_def incseq_def by auto
hoelzl@41980
   630
  { assume "f ----> x"
hoelzl@43920
   631
   then have "(\<lambda>i. ereal (f i)) ----> ereal x" by auto
hoelzl@43920
   632
   from SUP_Lim_ereal[OF inc this]
hoelzl@43920
   633
   show "(SUP n. ereal (f n)) = ereal x" . }
hoelzl@43920
   634
  { assume "(SUP n. ereal (f n)) = ereal x"
hoelzl@43920
   635
    with LIMSEQ_ereal_SUPR[OF inc]
hoelzl@41980
   636
    show "f ----> x" by auto }
hoelzl@41980
   637
qed
hoelzl@41980
   638
hoelzl@41980
   639
lemma Liminf_within:
hoelzl@43920
   640
  fixes f :: "'a::metric_space => ereal"
hoelzl@41980
   641
  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
hoelzl@41980
   642
proof-
hoelzl@41980
   643
let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
huffman@44170
   644
{ fix T assume T_def: "open T & mono_set T & ?l:T"
hoelzl@41980
   645
  have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
hoelzl@41980
   646
  proof-
hoelzl@41980
   647
  { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
hoelzl@41980
   648
  moreover
hoelzl@41980
   649
  { assume "~(T=UNIV)"
hoelzl@43920
   650
    then obtain B where "T={B<..}" using T_def ereal_open_mono_set[of T] by auto
hoelzl@41980
   651
    hence "B<?l" using T_def by auto
hoelzl@41980
   652
    then obtain d where d_def: "0<d & B<(INF y:(S Int ball x d - {x}). f y)"
hoelzl@41980
   653
      unfolding less_SUP_iff by auto
hoelzl@41980
   654
    { fix y assume "y:S & 0 < dist y x & dist y x < d"
hoelzl@41980
   655
      hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
hoelzl@41980
   656
      hence "f y:T" using d_def INF_leI[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
hoelzl@41980
   657
    } hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
hoelzl@41980
   658
  } ultimately show ?thesis by auto
hoelzl@41980
   659
  qed
hoelzl@41980
   660
}
hoelzl@41980
   661
moreover
hoelzl@41980
   662
{ fix z
huffman@44170
   663
  assume a: "ALL T. open T --> mono_set T --> z : T -->
hoelzl@41980
   664
     (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
hoelzl@41980
   665
  { fix B assume "B<z"
hoelzl@41980
   666
    then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
hoelzl@41980
   667
       using a[rule_format, of "{B<..}"] mono_greaterThan by auto
hoelzl@41980
   668
    { fix y assume "y:(S Int ball x d - {x})"
hoelzl@41980
   669
      hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
hoelzl@41980
   670
         by (metis dist_eq_0_iff real_less_def zero_le_dist)
hoelzl@41980
   671
      hence "B <= f y" using d_def by auto
hoelzl@41980
   672
    } hence "B <= INFI (S Int ball x d - {x}) f" apply (subst le_INFI) by auto
hoelzl@41980
   673
    also have "...<=?l" apply (subst le_SUPI) using d_def by auto
hoelzl@41980
   674
    finally have "B<=?l" by auto
hoelzl@43920
   675
  } hence "z <= ?l" using ereal_le_ereal[of z "?l"] by auto
hoelzl@41980
   676
}
hoelzl@43920
   677
ultimately show ?thesis unfolding ereal_Liminf_Sup_monoset eventually_within
hoelzl@43920
   678
   apply (subst ereal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e - {x}) f)"]) by auto
hoelzl@41980
   679
qed
hoelzl@41980
   680
hoelzl@41980
   681
lemma Limsup_within:
hoelzl@43920
   682
  fixes f :: "'a::metric_space => ereal"
hoelzl@41980
   683
  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
hoelzl@41980
   684
proof-
hoelzl@41980
   685
let ?l="(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
huffman@44170
   686
{ fix T assume T_def: "open T & mono_set (uminus ` T) & ?l:T"
hoelzl@41980
   687
  have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
hoelzl@41980
   688
  proof-
hoelzl@41980
   689
  { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
hoelzl@41980
   690
  moreover
hoelzl@41980
   691
  { assume "~(T=UNIV)" hence "~(uminus ` T = UNIV)"
hoelzl@43920
   692
       by (metis Int_UNIV_right Int_absorb1 image_mono ereal_minus_minus_image subset_UNIV)
hoelzl@43920
   693
    hence "uminus ` T = {Inf (uminus ` T)<..}" using T_def ereal_open_mono_set[of "uminus ` T"]
hoelzl@43920
   694
       ereal_open_uminus[of T] by auto
hoelzl@41980
   695
    then obtain B where "T={..<B}"
hoelzl@43920
   696
      unfolding ereal_Inf_uminus_image_eq ereal_uminus_lessThan[symmetric]
hoelzl@43920
   697
      unfolding inj_image_eq_iff[OF ereal_inj_on_uminus] by simp
hoelzl@41980
   698
    hence "?l<B" using T_def by auto
hoelzl@41980
   699
    then obtain d where d_def: "0<d & (SUP y:(S Int ball x d - {x}). f y)<B"
hoelzl@41980
   700
      unfolding INF_less_iff by auto
hoelzl@41980
   701
    { fix y assume "y:S & 0 < dist y x & dist y x < d"
hoelzl@41980
   702
      hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
hoelzl@41980
   703
      hence "f y:T" using d_def le_SUPI[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
hoelzl@41980
   704
    } hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
hoelzl@41980
   705
  } ultimately show ?thesis by auto
hoelzl@41980
   706
  qed
hoelzl@41980
   707
}
hoelzl@41980
   708
moreover
hoelzl@41980
   709
{ fix z
huffman@44170
   710
  assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T -->
hoelzl@41980
   711
     (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
hoelzl@41980
   712
  { fix B assume "z<B"
hoelzl@41980
   713
    then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"
hoelzl@41980
   714
       using a[rule_format, of "{..<B}"] by auto
hoelzl@41980
   715
    { fix y assume "y:(S Int ball x d - {x})"
hoelzl@41980
   716
      hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
hoelzl@41980
   717
         by (metis dist_eq_0_iff real_less_def zero_le_dist)
hoelzl@41980
   718
      hence "f y <= B" using d_def by auto
hoelzl@41980
   719
    } hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_leI) by auto
hoelzl@41980
   720
    moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_leI) using d_def by auto
hoelzl@41980
   721
    ultimately have "?l<=B" by auto
hoelzl@43920
   722
  } hence "?l <= z" using ereal_ge_ereal[of z "?l"] by auto
hoelzl@41980
   723
}
hoelzl@43920
   724
ultimately show ?thesis unfolding ereal_Limsup_Inf_monoset eventually_within
hoelzl@43920
   725
   apply (subst ereal_InfI) by auto
hoelzl@41980
   726
qed
hoelzl@41980
   727
hoelzl@41980
   728
hoelzl@41980
   729
lemma Liminf_within_UNIV:
hoelzl@43920
   730
  fixes f :: "'a::metric_space => ereal"
hoelzl@41980
   731
  shows "Liminf (at x) f = Liminf (at x within UNIV) f"
hoelzl@41980
   732
by (metis within_UNIV)
hoelzl@41980
   733
hoelzl@41980
   734
hoelzl@41980
   735
lemma Liminf_at:
hoelzl@43920
   736
  fixes f :: "'a::metric_space => ereal"
hoelzl@41980
   737
  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
hoelzl@41980
   738
using Liminf_within[of x UNIV f] Liminf_within_UNIV[of x f] by auto
hoelzl@41980
   739
hoelzl@41980
   740
hoelzl@41980
   741
lemma Limsup_within_UNIV:
hoelzl@43920
   742
  fixes f :: "'a::metric_space => ereal"
hoelzl@41980
   743
  shows "Limsup (at x) f = Limsup (at x within UNIV) f"
hoelzl@41980
   744
by (metis within_UNIV)
hoelzl@41980
   745
hoelzl@41980
   746
hoelzl@41980
   747
lemma Limsup_at:
hoelzl@43920
   748
  fixes f :: "'a::metric_space => ereal"
hoelzl@41980
   749
  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
hoelzl@41980
   750
using Limsup_within[of x UNIV f] Limsup_within_UNIV[of x f] by auto
hoelzl@41980
   751
hoelzl@41980
   752
lemma Lim_within_constant:
hoelzl@41980
   753
  fixes f :: "'a::metric_space => 'b::topological_space"
hoelzl@41980
   754
  assumes "ALL y:S. f y = C"
hoelzl@41980
   755
  shows "(f ---> C) (at x within S)"
hoelzl@41980
   756
unfolding tendsto_def eventually_within
hoelzl@41980
   757
by (metis assms(1) linorder_le_less_linear n_not_Suc_n real_of_nat_le_zero_cancel_iff)
hoelzl@41980
   758
hoelzl@41980
   759
lemma Liminf_within_constant:
hoelzl@43920
   760
  fixes f :: "'a::metric_space => ereal"
hoelzl@41980
   761
  assumes "ALL y:S. f y = C"
hoelzl@41980
   762
  assumes "~trivial_limit (at x within S)"
hoelzl@41980
   763
  shows "Liminf (at x within S) f = C"
hoelzl@41980
   764
by (metis Lim_within_constant assms lim_imp_Liminf)
hoelzl@41980
   765
hoelzl@41980
   766
lemma Limsup_within_constant:
hoelzl@43920
   767
  fixes f :: "'a::metric_space => ereal"
hoelzl@41980
   768
  assumes "ALL y:S. f y = C"
hoelzl@41980
   769
  assumes "~trivial_limit (at x within S)"
hoelzl@41980
   770
  shows "Limsup (at x within S) f = C"
hoelzl@41980
   771
by (metis Lim_within_constant assms lim_imp_Limsup)
hoelzl@41980
   772
hoelzl@41980
   773
lemma islimpt_punctured:
hoelzl@41980
   774
"x islimpt S = x islimpt (S-{x})"
hoelzl@41980
   775
unfolding islimpt_def by blast
hoelzl@41980
   776
hoelzl@41980
   777
hoelzl@41980
   778
lemma islimpt_in_closure:
hoelzl@41980
   779
"(x islimpt S) = (x:closure(S-{x}))"
hoelzl@41980
   780
unfolding closure_def using islimpt_punctured by blast
hoelzl@41980
   781
hoelzl@41980
   782
hoelzl@41980
   783
lemma not_trivial_limit_within:
hoelzl@41980
   784
  "~trivial_limit (at x within S) = (x:closure(S-{x}))"
hoelzl@41980
   785
using islimpt_in_closure by (metis trivial_limit_within)
hoelzl@41980
   786
hoelzl@41980
   787
hoelzl@41980
   788
lemma not_trivial_limit_within_ball:
hoelzl@41980
   789
  "(~trivial_limit (at x within S)) = (ALL e>0. S Int ball x e - {x} ~= {})"
hoelzl@41980
   790
  (is "?lhs = ?rhs")
hoelzl@41980
   791
proof-
hoelzl@41980
   792
{ assume "?lhs"
hoelzl@41980
   793
  { fix e :: real assume "e>0"
hoelzl@41980
   794
    then obtain y where "y:(S-{x}) & dist y x < e"
hoelzl@41980
   795
       using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
hoelzl@41980
   796
    hence "y : (S Int ball x e - {x})" unfolding ball_def by (simp add: dist_commute)
hoelzl@41980
   797
    hence "S Int ball x e - {x} ~= {}" by blast
hoelzl@41980
   798
  } hence "?rhs" by auto
hoelzl@41980
   799
}
hoelzl@41980
   800
moreover
hoelzl@41980
   801
{ assume "?rhs"
hoelzl@41980
   802
  { fix e :: real assume "e>0"
hoelzl@41980
   803
    then obtain y where "y : (S Int ball x e - {x})" using `?rhs` by blast
hoelzl@41980
   804
    hence "y:(S-{x}) & dist y x < e" unfolding ball_def by (simp add: dist_commute)
hoelzl@41980
   805
    hence "EX y:(S-{x}). dist y x < e" by auto
hoelzl@41980
   806
  } hence "?lhs" using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
hoelzl@41980
   807
} ultimately show ?thesis by auto
hoelzl@41980
   808
qed
hoelzl@41980
   809
hoelzl@43920
   810
lemma liminf_ereal_cminus:
hoelzl@43920
   811
  fixes f :: "nat \<Rightarrow> ereal" assumes "c \<noteq> -\<infinity>"
hoelzl@42950
   812
  shows "liminf (\<lambda>x. c - f x) = c - limsup f"
hoelzl@42950
   813
proof (cases c)
hoelzl@42950
   814
  case PInf then show ?thesis by (simp add: Liminf_const)
hoelzl@42950
   815
next
hoelzl@42950
   816
  case (real r) then show ?thesis
hoelzl@42950
   817
    unfolding liminf_SUPR_INFI limsup_INFI_SUPR
hoelzl@43920
   818
    apply (subst INFI_ereal_cminus)
hoelzl@42950
   819
    apply auto
hoelzl@43920
   820
    apply (subst SUPR_ereal_cminus)
hoelzl@42950
   821
    apply auto
hoelzl@42950
   822
    done
hoelzl@42950
   823
qed (insert `c \<noteq> -\<infinity>`, simp)
hoelzl@42950
   824
hoelzl@41980
   825
subsubsection {* Continuity *}
hoelzl@41980
   826
hoelzl@41980
   827
lemma continuous_imp_tendsto:
hoelzl@41980
   828
  assumes "continuous (at x0) f"
hoelzl@41980
   829
  assumes "x ----> x0"
hoelzl@41980
   830
  shows "(f o x) ----> (f x0)"
hoelzl@41980
   831
proof-
hoelzl@41980
   832
{ fix S assume "open S & (f x0):S"
hoelzl@41980
   833
  from this obtain T where T_def: "open T & x0 : T & (ALL x:T. f x : S)"
hoelzl@41980
   834
     using assms continuous_at_open by metis
hoelzl@41980
   835
  hence "(EX N. ALL n>=N. x n : T)" using assms tendsto_explicit T_def by auto
hoelzl@41980
   836
  hence "(EX N. ALL n>=N. f(x n) : S)" using T_def by auto
hoelzl@41980
   837
} from this show ?thesis using tendsto_explicit[of "f o x" "f x0"] by auto
hoelzl@41980
   838
qed
hoelzl@41980
   839
hoelzl@41980
   840
hoelzl@41980
   841
lemma continuous_at_sequentially2:
hoelzl@41980
   842
fixes f :: "'a::metric_space => 'b:: topological_space"
hoelzl@41980
   843
shows "continuous (at x0) f <-> (ALL x. (x ----> x0) --> (f o x) ----> (f x0))"
hoelzl@41980
   844
proof-
hoelzl@41980
   845
{ assume "~(continuous (at x0) f)"
hoelzl@41980
   846
  from this obtain T where T_def:
hoelzl@41980
   847
     "open T & f x0 : T & (ALL S. (open S & x0 : S) --> (EX x':S. f x' ~: T))"
hoelzl@41980
   848
     using continuous_at_open[of x0 f] by metis
hoelzl@41980
   849
  def X == "{x'. f x' ~: T}" hence "x0 islimpt X" unfolding islimpt_def using T_def by auto
hoelzl@41980
   850
  from this obtain x where x_def: "(ALL n. x n : X) & x ----> x0"
hoelzl@41980
   851
     using islimpt_sequential[of x0 X] by auto
hoelzl@41980
   852
  hence "~(f o x) ----> (f x0)" unfolding tendsto_explicit using X_def T_def by auto
hoelzl@41980
   853
  hence "EX x. x ----> x0 & (~(f o x) ----> (f x0))" using x_def by auto
hoelzl@41980
   854
}
hoelzl@41980
   855
from this show ?thesis using continuous_imp_tendsto by auto
hoelzl@41980
   856
qed
hoelzl@41980
   857
hoelzl@43920
   858
lemma continuous_at_of_ereal:
hoelzl@43920
   859
  fixes x0 :: ereal
hoelzl@41980
   860
  assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
hoelzl@41980
   861
  shows "continuous (at x0) real"
hoelzl@41980
   862
proof-
hoelzl@41980
   863
{ fix T assume T_def: "open T & real x0 : T"
hoelzl@43920
   864
  def S == "ereal ` T"
hoelzl@43920
   865
  hence "ereal (real x0) : S" using T_def by auto
hoelzl@43920
   866
  hence "x0 : S" using assms ereal_real by auto
hoelzl@43920
   867
  moreover have "open S" using open_ereal S_def T_def by auto
hoelzl@41980
   868
  moreover have "ALL y:S. real y : T" using S_def T_def by auto
hoelzl@41980
   869
  ultimately have "EX S. x0 : S & open S & (ALL y:S. real y : T)" by auto
hoelzl@41980
   870
} from this show ?thesis unfolding continuous_at_open by blast
hoelzl@41980
   871
qed
hoelzl@41980
   872
hoelzl@41980
   873
hoelzl@43920
   874
lemma continuous_at_iff_ereal:
hoelzl@41980
   875
fixes f :: "'a::t2_space => real"
hoelzl@43920
   876
shows "continuous (at x0) f <-> continuous (at x0) (ereal o f)"
hoelzl@41980
   877
proof-
hoelzl@43920
   878
{ assume "continuous (at x0) f" hence "continuous (at x0) (ereal o f)"
hoelzl@43920
   879
     using continuous_at_ereal continuous_at_compose[of x0 f ereal] by auto
hoelzl@41980
   880
}
hoelzl@41980
   881
moreover
hoelzl@43920
   882
{ assume "continuous (at x0) (ereal o f)"
hoelzl@43920
   883
  hence "continuous (at x0) (real o (ereal o f))"
hoelzl@43920
   884
     using continuous_at_of_ereal by (intro continuous_at_compose[of x0 "ereal o f"]) auto
hoelzl@43920
   885
  moreover have "real o (ereal o f) = f" using real_ereal_id by (simp add: o_assoc)
hoelzl@41980
   886
  ultimately have "continuous (at x0) f" by auto
hoelzl@41980
   887
} ultimately show ?thesis by auto
hoelzl@41980
   888
qed
hoelzl@41980
   889
hoelzl@41980
   890
hoelzl@43920
   891
lemma continuous_on_iff_ereal:
hoelzl@41980
   892
fixes f :: "'a::t2_space => real"
hoelzl@41980
   893
fixes A assumes "open A"
hoelzl@43920
   894
shows "continuous_on A f <-> continuous_on A (ereal o f)"
hoelzl@43920
   895
   using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at)
hoelzl@41980
   896
hoelzl@41980
   897
hoelzl@43923
   898
lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>::ereal)}) real"
hoelzl@43920
   899
   using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal by auto
hoelzl@41980
   900
hoelzl@41980
   901
hoelzl@41980
   902
lemma continuous_on_iff_real:
hoelzl@43920
   903
  fixes f :: "'a::t2_space => ereal"
hoelzl@41980
   904
  assumes "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
hoelzl@41980
   905
  shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
hoelzl@41980
   906
proof-
hoelzl@41980
   907
  have "f ` A <= UNIV-{\<infinity>,(-\<infinity>)}" using assms by force
hoelzl@41980
   908
  hence *: "continuous_on (f ` A) real"
hoelzl@41980
   909
     using continuous_on_real by (simp add: continuous_on_subset)
hoelzl@43920
   910
have **: "continuous_on ((real o f) ` A) ereal"
hoelzl@43920
   911
   using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real o f) ` A"] by blast
hoelzl@41980
   912
{ assume "continuous_on A f" hence "continuous_on A (real o f)"
hoelzl@41980
   913
  apply (subst continuous_on_compose) using * by auto
hoelzl@41980
   914
}
hoelzl@41980
   915
moreover
hoelzl@41980
   916
{ assume "continuous_on A (real o f)"
hoelzl@43920
   917
  hence "continuous_on A (ereal o (real o f))"
hoelzl@41980
   918
     apply (subst continuous_on_compose) using ** by auto
hoelzl@41980
   919
  hence "continuous_on A f"
hoelzl@43920
   920
     apply (subst continuous_on_eq[of A "ereal o (real o f)" f])
hoelzl@43920
   921
     using assms ereal_real by auto
hoelzl@41980
   922
}
hoelzl@41980
   923
ultimately show ?thesis by auto
hoelzl@41980
   924
qed
hoelzl@41980
   925
hoelzl@41980
   926
hoelzl@41980
   927
lemma continuous_at_const:
hoelzl@43920
   928
  fixes f :: "'a::t2_space => ereal"
hoelzl@41980
   929
  assumes "ALL x. (f x = C)"
hoelzl@41980
   930
  shows "ALL x. continuous (at x) f"
hoelzl@41980
   931
unfolding continuous_at_open using assms t1_space by auto
hoelzl@41980
   932
hoelzl@41980
   933
hoelzl@41980
   934
lemma closure_contains_Inf:
hoelzl@41980
   935
  fixes S :: "real set"
hoelzl@41980
   936
  assumes "S ~= {}" "EX B. ALL x:S. B<=x"
hoelzl@41980
   937
  shows "Inf S : closure S"
hoelzl@41980
   938
proof-
hoelzl@41980
   939
have *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] assms by metis
hoelzl@41980
   940
{ fix e assume "e>(0 :: real)"
hoelzl@41980
   941
  from this obtain x where x_def: "x:S & x < Inf S + e" using Inf_close `S ~= {}` by auto
hoelzl@41980
   942
  moreover hence "x > Inf S - e" using * by auto
hoelzl@41980
   943
  ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
hoelzl@41980
   944
  hence "EX x:S. abs (x - Inf S) < e" using x_def by auto
hoelzl@41980
   945
} from this show ?thesis apply (subst closure_approachable) unfolding dist_norm by auto
hoelzl@41980
   946
qed
hoelzl@41980
   947
hoelzl@41980
   948
hoelzl@41980
   949
lemma closed_contains_Inf:
hoelzl@41980
   950
  fixes S :: "real set"
hoelzl@41980
   951
  assumes "S ~= {}" "EX B. ALL x:S. B<=x"
hoelzl@41980
   952
  assumes "closed S"
hoelzl@41980
   953
  shows "Inf S : S"
hoelzl@41980
   954
by (metis closure_contains_Inf closure_closed assms)
hoelzl@41980
   955
hoelzl@41980
   956
hoelzl@41980
   957
lemma mono_closed_real:
hoelzl@41980
   958
  fixes S :: "real set"
hoelzl@41980
   959
  assumes mono: "ALL y z. y:S & y<=z --> z:S"
hoelzl@41980
   960
  assumes "closed S"
hoelzl@41980
   961
  shows "S = {} | S = UNIV | (EX a. S = {a ..})"
hoelzl@41980
   962
proof-
hoelzl@41980
   963
{ assume "S ~= {}"
hoelzl@41980
   964
  { assume ex: "EX B. ALL x:S. B<=x"
hoelzl@41980
   965
    hence *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] ex by metis
hoelzl@41980
   966
    hence "Inf S : S" apply (subst closed_contains_Inf) using ex `S ~= {}` `closed S` by auto
hoelzl@41980
   967
    hence "ALL x. (Inf S <= x <-> x:S)" using mono[rule_format, of "Inf S"] * by auto
hoelzl@41980
   968
    hence "S = {Inf S ..}" by auto
hoelzl@41980
   969
    hence "EX a. S = {a ..}" by auto
hoelzl@41980
   970
  }
hoelzl@41980
   971
  moreover
hoelzl@41980
   972
  { assume "~(EX B. ALL x:S. B<=x)"
hoelzl@41980
   973
    hence nex: "ALL B. EX x:S. x<B" by (simp add: not_le)
hoelzl@41980
   974
    { fix y obtain x where "x:S & x < y" using nex by auto
hoelzl@41980
   975
      hence "y:S" using mono[rule_format, of x y] by auto
hoelzl@41980
   976
    } hence "S = UNIV" by auto
hoelzl@41980
   977
  } ultimately have "S = UNIV | (EX a. S = {a ..})" by blast
hoelzl@41980
   978
} from this show ?thesis by blast
hoelzl@41980
   979
qed
hoelzl@41980
   980
hoelzl@41980
   981
hoelzl@43920
   982
lemma mono_closed_ereal:
hoelzl@41980
   983
  fixes S :: "real set"
hoelzl@41980
   984
  assumes mono: "ALL y z. y:S & y<=z --> z:S"
hoelzl@41980
   985
  assumes "closed S"
hoelzl@43920
   986
  shows "EX a. S = {x. a <= ereal x}"
hoelzl@41980
   987
proof-
hoelzl@41980
   988
{ assume "S = {}" hence ?thesis apply(rule_tac x=PInfty in exI) by auto }
hoelzl@41980
   989
moreover
hoelzl@41980
   990
{ assume "S = UNIV" hence ?thesis apply(rule_tac x="-\<infinity>" in exI) by auto }
hoelzl@41980
   991
moreover
hoelzl@41980
   992
{ assume "EX a. S = {a ..}"
hoelzl@41980
   993
  from this obtain a where "S={a ..}" by auto
hoelzl@43920
   994
  hence ?thesis apply(rule_tac x="ereal a" in exI) by auto
hoelzl@41980
   995
} ultimately show ?thesis using mono_closed_real[of S] assms by auto
hoelzl@41980
   996
qed
hoelzl@41980
   997
hoelzl@41980
   998
subsection {* Sums *}
hoelzl@41980
   999
hoelzl@43920
  1000
lemma setsum_ereal[simp]:
hoelzl@43920
  1001
  "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
hoelzl@41980
  1002
proof cases
hoelzl@41980
  1003
  assume "finite A" then show ?thesis by induct auto
hoelzl@41980
  1004
qed simp
hoelzl@41980
  1005
hoelzl@43923
  1006
lemma setsum_Pinfty:
hoelzl@43923
  1007
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@43923
  1008
  shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))"
hoelzl@41980
  1009
proof safe
hoelzl@41980
  1010
  assume *: "setsum f P = \<infinity>"
hoelzl@41980
  1011
  show "finite P"
hoelzl@41980
  1012
  proof (rule ccontr) assume "infinite P" with * show False by auto qed
hoelzl@41980
  1013
  show "\<exists>i\<in>P. f i = \<infinity>"
hoelzl@41980
  1014
  proof (rule ccontr)
hoelzl@41980
  1015
    assume "\<not> ?thesis" then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>" by auto
hoelzl@41980
  1016
    from `finite P` this have "setsum f P \<noteq> \<infinity>"
hoelzl@41980
  1017
      by induct auto
hoelzl@41980
  1018
    with * show False by auto
hoelzl@41980
  1019
  qed
hoelzl@41980
  1020
next
hoelzl@41980
  1021
  fix i assume "finite P" "i \<in> P" "f i = \<infinity>"
hoelzl@41980
  1022
  thus "setsum f P = \<infinity>"
hoelzl@41980
  1023
  proof induct
hoelzl@41980
  1024
    case (insert x A)
hoelzl@41980
  1025
    show ?case using insert by (cases "x = i") auto
hoelzl@41980
  1026
  qed simp
hoelzl@41980
  1027
qed
hoelzl@41980
  1028
hoelzl@41980
  1029
lemma setsum_Inf:
hoelzl@43923
  1030
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@41980
  1031
  shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>))"
hoelzl@41980
  1032
proof
hoelzl@41980
  1033
  assume *: "\<bar>setsum f A\<bar> = \<infinity>"
hoelzl@41980
  1034
  have "finite A" by (rule ccontr) (insert *, auto)
hoelzl@41980
  1035
  moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>"
hoelzl@41980
  1036
  proof (rule ccontr)
hoelzl@43920
  1037
    assume "\<not> ?thesis" then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto
hoelzl@41980
  1038
    from bchoice[OF this] guess r ..
huffman@44142
  1039
    with * show False by auto
hoelzl@41980
  1040
  qed
hoelzl@41980
  1041
  ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" by auto
hoelzl@41980
  1042
next
hoelzl@41980
  1043
  assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
hoelzl@41980
  1044
  then obtain i where "finite A" "i \<in> A" "\<bar>f i\<bar> = \<infinity>" by auto
hoelzl@41980
  1045
  then show "\<bar>setsum f A\<bar> = \<infinity>"
hoelzl@41980
  1046
  proof induct
hoelzl@41980
  1047
    case (insert j A) then show ?case
hoelzl@43920
  1048
      by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
hoelzl@41980
  1049
  qed simp
hoelzl@41980
  1050
qed
hoelzl@41980
  1051
hoelzl@43920
  1052
lemma setsum_real_of_ereal:
hoelzl@43923
  1053
  fixes f :: "'i \<Rightarrow> ereal"
hoelzl@41980
  1054
  assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
hoelzl@41980
  1055
  shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
hoelzl@41980
  1056
proof -
hoelzl@43920
  1057
  have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
hoelzl@41980
  1058
  proof
hoelzl@41980
  1059
    fix x assume "x \<in> S"
hoelzl@43920
  1060
    from assms[OF this] show "\<exists>r. f x = ereal r" by (cases "f x") auto
hoelzl@41980
  1061
  qed
hoelzl@41980
  1062
  from bchoice[OF this] guess r ..
hoelzl@41980
  1063
  then show ?thesis by simp
hoelzl@41980
  1064
qed
hoelzl@41980
  1065
hoelzl@43920
  1066
lemma setsum_ereal_0:
hoelzl@43920
  1067
  fixes f :: "'a \<Rightarrow> ereal" assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
hoelzl@41980
  1068
  shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
hoelzl@41980
  1069
proof
hoelzl@41980
  1070
  assume *: "(\<Sum>x\<in>A. f x) = 0"
hoelzl@41980
  1071
  then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>" by auto
hoelzl@41980
  1072
  then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>" using assms by (force simp: setsum_Pinfty)
hoelzl@43920
  1073
  then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto
hoelzl@41980
  1074
  from bchoice[OF this] * assms show "\<forall>i\<in>A. f i = 0"
hoelzl@41980
  1075
    using setsum_nonneg_eq_0_iff[of A "\<lambda>i. real (f i)"] by auto
hoelzl@41980
  1076
qed (rule setsum_0')
hoelzl@41980
  1077
hoelzl@41980
  1078
hoelzl@43920
  1079
lemma setsum_ereal_right_distrib:
hoelzl@43920
  1080
  fixes f :: "'a \<Rightarrow> ereal" assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
hoelzl@41980
  1081
  shows "r * setsum f A = (\<Sum>n\<in>A. r * f n)"
hoelzl@41980
  1082
proof cases
hoelzl@41980
  1083
  assume "finite A" then show ?thesis using assms
hoelzl@43920
  1084
    by induct (auto simp: ereal_right_distrib setsum_nonneg)
hoelzl@41980
  1085
qed simp
hoelzl@41980
  1086
hoelzl@43920
  1087
lemma sums_ereal_positive:
hoelzl@43920
  1088
  fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" shows "f sums (SUP n. \<Sum>i<n. f i)"
hoelzl@41980
  1089
proof -
hoelzl@41980
  1090
  have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
hoelzl@43920
  1091
    using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)
hoelzl@43920
  1092
  from LIMSEQ_ereal_SUPR[OF this]
hoelzl@41980
  1093
  show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)
hoelzl@41980
  1094
qed
hoelzl@41980
  1095
hoelzl@43920
  1096
lemma summable_ereal_pos:
hoelzl@43920
  1097
  fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" shows "summable f"
hoelzl@43920
  1098
  using sums_ereal_positive[of f, OF assms] unfolding summable_def by auto
hoelzl@41980
  1099
hoelzl@43920
  1100
lemma suminf_ereal_eq_SUPR:
hoelzl@43920
  1101
  fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i"
hoelzl@41980
  1102
  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
hoelzl@43920
  1103
  using sums_ereal_positive[of f, OF assms, THEN sums_unique] by simp
hoelzl@41980
  1104
hoelzl@43920
  1105
lemma sums_ereal:
hoelzl@43920
  1106
  "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
hoelzl@41980
  1107
  unfolding sums_def by simp
hoelzl@41980
  1108
hoelzl@41980
  1109
lemma suminf_bound:
hoelzl@43920
  1110
  fixes f :: "nat \<Rightarrow> ereal"
hoelzl@41980
  1111
  assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x" and pos: "\<And>n. 0 \<le> f n"
hoelzl@41980
  1112
  shows "suminf f \<le> x"
hoelzl@43920
  1113
proof (rule Lim_bounded_ereal)
hoelzl@43920
  1114
  have "summable f" using pos[THEN summable_ereal_pos] .
hoelzl@41980
  1115
  then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
hoelzl@41980
  1116
    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
hoelzl@41980
  1117
  show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
hoelzl@41980
  1118
    using assms by auto
hoelzl@41980
  1119
qed
hoelzl@41980
  1120
hoelzl@41980
  1121
lemma suminf_bound_add:
hoelzl@43920
  1122
  fixes f :: "nat \<Rightarrow> ereal"
hoelzl@41980
  1123
  assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x" and pos: "\<And>n. 0 \<le> f n" and "y \<noteq> -\<infinity>"
hoelzl@41980
  1124
  shows "suminf f + y \<le> x"
hoelzl@41980
  1125
proof (cases y)
hoelzl@41980
  1126
  case (real r) then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
hoelzl@43920
  1127
    using assms by (simp add: ereal_le_minus)
hoelzl@41980
  1128
  then have "(\<Sum> n. f n) \<le> x - y" using pos by (rule suminf_bound)
hoelzl@41980
  1129
  then show "(\<Sum> n. f n) + y \<le> x"
hoelzl@43920
  1130
    using assms real by (simp add: ereal_le_minus)
hoelzl@41980
  1131
qed (insert assms, auto)
hoelzl@41980
  1132
hoelzl@41980
  1133
lemma sums_finite:
hoelzl@41980
  1134
  assumes "\<forall>N\<ge>n. f N = 0"
hoelzl@41980
  1135
  shows "f sums (\<Sum>N<n. f N)"
hoelzl@41980
  1136
proof -
hoelzl@41980
  1137
  { fix i have "(\<Sum>N<i + n. f N) = (\<Sum>N<n. f N)"
hoelzl@41980
  1138
      by (induct i) (insert assms, auto) }
hoelzl@41980
  1139
  note this[simp]
hoelzl@41980
  1140
  show ?thesis unfolding sums_def
huffman@44125
  1141
    by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan intro: tendsto_const)
hoelzl@41980
  1142
qed
hoelzl@41980
  1143
hoelzl@41980
  1144
lemma suminf_finite:
hoelzl@41980
  1145
  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,t2_space}" assumes "\<forall>N\<ge>n. f N = 0"
hoelzl@41980
  1146
  shows "suminf f = (\<Sum>N<n. f N)"
hoelzl@41980
  1147
  using sums_finite[OF assms, THEN sums_unique] by simp
hoelzl@41980
  1148
hoelzl@41980
  1149
lemma suminf_upper:
hoelzl@43920
  1150
  fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
hoelzl@41980
  1151
  shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
hoelzl@43920
  1152
  unfolding suminf_ereal_eq_SUPR[OF assms] SUPR_def
hoelzl@41980
  1153
  by (auto intro: complete_lattice_class.Sup_upper image_eqI)
hoelzl@41980
  1154
hoelzl@41980
  1155
lemma suminf_0_le:
hoelzl@43920
  1156
  fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
hoelzl@41980
  1157
  shows "0 \<le> (\<Sum>n. f n)"
hoelzl@41980
  1158
  using suminf_upper[of f 0, OF assms] by simp
hoelzl@41980
  1159
hoelzl@41980
  1160
lemma suminf_le_pos:
hoelzl@43920
  1161
  fixes f g :: "nat \<Rightarrow> ereal"
hoelzl@41980
  1162
  assumes "\<And>N. f N \<le> g N" "\<And>N. 0 \<le> f N"
hoelzl@41980
  1163
  shows "suminf f \<le> suminf g"
hoelzl@41980
  1164
proof (safe intro!: suminf_bound)
hoelzl@41980
  1165
  fix n { fix N have "0 \<le> g N" using assms(2,1)[of N] by auto }
hoelzl@41980
  1166
  have "setsum f {..<n} \<le> setsum g {..<n}" using assms by (auto intro: setsum_mono)
hoelzl@41980
  1167
  also have "... \<le> suminf g" using `\<And>N. 0 \<le> g N` by (rule suminf_upper)
hoelzl@41980
  1168
  finally show "setsum f {..<n} \<le> suminf g" .
hoelzl@41980
  1169
qed (rule assms(2))
hoelzl@41980
  1170
hoelzl@43920
  1171
lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal)^Suc n) = 1"
hoelzl@43920
  1172
  using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
hoelzl@43920
  1173
  by (simp add: one_ereal_def)
hoelzl@41980
  1174
hoelzl@43920
  1175
lemma suminf_add_ereal:
hoelzl@43920
  1176
  fixes f g :: "nat \<Rightarrow> ereal"
hoelzl@41980
  1177
  assumes "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
hoelzl@41980
  1178
  shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
hoelzl@43920
  1179
  apply (subst (1 2 3) suminf_ereal_eq_SUPR)
hoelzl@41980
  1180
  unfolding setsum_addf
hoelzl@43920
  1181
  by (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
hoelzl@41980
  1182
hoelzl@43920
  1183
lemma suminf_cmult_ereal:
hoelzl@43920
  1184
  fixes f g :: "nat \<Rightarrow> ereal"
hoelzl@41980
  1185
  assumes "\<And>i. 0 \<le> f i" "0 \<le> a"
hoelzl@41980
  1186
  shows "(\<Sum>i. a * f i) = a * suminf f"
hoelzl@43920
  1187
  by (auto simp: setsum_ereal_right_distrib[symmetric] assms
hoelzl@43920
  1188
                 ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR
hoelzl@43920
  1189
           intro!: SUPR_ereal_cmult )
hoelzl@41980
  1190
hoelzl@41980
  1191
lemma suminf_PInfty:
hoelzl@43923
  1192
  fixes f :: "nat \<Rightarrow> ereal"
hoelzl@41980
  1193
  assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>"
hoelzl@41980
  1194
  shows "f i \<noteq> \<infinity>"
hoelzl@41980
  1195
proof -
hoelzl@41980
  1196
  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
hoelzl@41980
  1197
  have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>" by auto
hoelzl@41980
  1198
  then show ?thesis
hoelzl@41980
  1199
    unfolding setsum_Pinfty by simp
hoelzl@41980
  1200
qed
hoelzl@41980
  1201
hoelzl@41980
  1202
lemma suminf_PInfty_fun:
hoelzl@41980
  1203
  assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>"
hoelzl@43920
  1204
  shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
hoelzl@41980
  1205
proof -
hoelzl@43920
  1206
  have "\<forall>i. \<exists>r. f i = ereal r"
hoelzl@41980
  1207
  proof
hoelzl@43920
  1208
    fix i show "\<exists>r. f i = ereal r"
hoelzl@41980
  1209
      using suminf_PInfty[OF assms] assms(1)[of i] by (cases "f i") auto
hoelzl@41980
  1210
  qed
hoelzl@41980
  1211
  from choice[OF this] show ?thesis by auto
hoelzl@41980
  1212
qed
hoelzl@41980
  1213
hoelzl@43920
  1214
lemma summable_ereal:
hoelzl@43920
  1215
  assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
hoelzl@41980
  1216
  shows "summable f"
hoelzl@41980
  1217
proof -
hoelzl@43920
  1218
  have "0 \<le> (\<Sum>i. ereal (f i))"
hoelzl@41980
  1219
    using assms by (intro suminf_0_le) auto
hoelzl@43920
  1220
  with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
hoelzl@43920
  1221
    by (cases "\<Sum>i. ereal (f i)") auto
hoelzl@43920
  1222
  from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
hoelzl@43920
  1223
  have "summable (\<lambda>x. ereal (f x))" using assms by auto
hoelzl@41980
  1224
  from summable_sums[OF this]
hoelzl@43920
  1225
  have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))" by auto
hoelzl@41980
  1226
  then show "summable f"
hoelzl@43920
  1227
    unfolding r sums_ereal summable_def ..
hoelzl@41980
  1228
qed
hoelzl@41980
  1229
hoelzl@43920
  1230
lemma suminf_ereal:
hoelzl@43920
  1231
  assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
hoelzl@43920
  1232
  shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
hoelzl@41980
  1233
proof (rule sums_unique[symmetric])
hoelzl@43920
  1234
  from summable_ereal[OF assms]
hoelzl@43920
  1235
  show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
hoelzl@43920
  1236
    unfolding sums_ereal using assms by (intro summable_sums summable_ereal)
hoelzl@41980
  1237
qed
hoelzl@41980
  1238
hoelzl@43920
  1239
lemma suminf_ereal_minus:
hoelzl@43920
  1240
  fixes f g :: "nat \<Rightarrow> ereal"
hoelzl@41980
  1241
  assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i" and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
hoelzl@41980
  1242
  shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
hoelzl@41980
  1243
proof -
hoelzl@41980
  1244
  { fix i have "0 \<le> f i" using ord[of i] by auto }
hoelzl@41980
  1245
  moreover
hoelzl@41980
  1246
  from suminf_PInfty_fun[OF `\<And>i. 0 \<le> f i` fin(1)] guess f' .. note this[simp]
hoelzl@41980
  1247
  from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] guess g' .. note this[simp]
hoelzl@43920
  1248
  { fix i have "0 \<le> f i - g i" using ord[of i] by (auto simp: ereal_le_minus_iff) }
hoelzl@41980
  1249
  moreover
hoelzl@41980
  1250
  have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
hoelzl@41980
  1251
    using assms by (auto intro!: suminf_le_pos simp: field_simps)
hoelzl@41980
  1252
  then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>" using fin by auto
hoelzl@41980
  1253
  ultimately show ?thesis using assms `\<And>i. 0 \<le> f i`
hoelzl@41980
  1254
    apply simp
hoelzl@43920
  1255
    by (subst (1 2 3) suminf_ereal)
hoelzl@43920
  1256
       (auto intro!: suminf_diff[symmetric] summable_ereal)
hoelzl@41980
  1257
qed
hoelzl@41980
  1258
hoelzl@43920
  1259
lemma suminf_ereal_PInf[simp]:
hoelzl@43923
  1260
  "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
hoelzl@41980
  1261
proof -
hoelzl@43923
  1262
  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)" by (rule suminf_upper) auto
hoelzl@41980
  1263
  then show ?thesis by simp
hoelzl@41980
  1264
qed
hoelzl@41980
  1265
hoelzl@43920
  1266
lemma summable_real_of_ereal:
hoelzl@43923
  1267
  fixes f :: "nat \<Rightarrow> ereal"
hoelzl@41980
  1268
  assumes f: "\<And>i. 0 \<le> f i" and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
hoelzl@41980
  1269
  shows "summable (\<lambda>i. real (f i))"
hoelzl@41980
  1270
proof (rule summable_def[THEN iffD2])
hoelzl@41980
  1271
  have "0 \<le> (\<Sum>i. f i)" using assms by (auto intro: suminf_0_le)
hoelzl@43920
  1272
  with fin obtain r where r: "ereal r = (\<Sum>i. f i)" by (cases "(\<Sum>i. f i)") auto
hoelzl@41980
  1273
  { fix i have "f i \<noteq> \<infinity>" using f by (intro suminf_PInfty[OF _ fin]) auto
hoelzl@41980
  1274
    then have "\<bar>f i\<bar> \<noteq> \<infinity>" using f[of i] by auto }
hoelzl@41980
  1275
  note fin = this
hoelzl@43920
  1276
  have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
hoelzl@43920
  1277
    using f by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
hoelzl@43920
  1278
  also have "\<dots> = ereal r" using fin r by (auto simp: ereal_real)
hoelzl@43920
  1279
  finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" by (auto simp: sums_ereal)
hoelzl@41980
  1280
qed
hoelzl@41980
  1281
hoelzl@42950
  1282
lemma suminf_SUP_eq:
hoelzl@43920
  1283
  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
hoelzl@42950
  1284
  assumes "\<And>i. incseq (\<lambda>n. f n i)" "\<And>n i. 0 \<le> f n i"
hoelzl@42950
  1285
  shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
hoelzl@42950
  1286
proof -
hoelzl@42950
  1287
  { fix n :: nat
hoelzl@42950
  1288
    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
hoelzl@43920
  1289
      using assms by (auto intro!: SUPR_ereal_setsum[symmetric]) }
hoelzl@42950
  1290
  note * = this
hoelzl@42950
  1291
  show ?thesis using assms
hoelzl@43920
  1292
    apply (subst (1 2) suminf_ereal_eq_SUPR)
hoelzl@42950
  1293
    unfolding *
hoelzl@42950
  1294
    apply (auto intro!: le_SUPI2)
hoelzl@42950
  1295
    apply (subst SUP_commute) ..
hoelzl@42950
  1296
qed
hoelzl@42950
  1297
huffman@44125
  1298
end