src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
author hoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51481 ef949192e5d6
parent 51475 ebf9d4fd00ba
child 51530 609914f0934a
permissions -rw-r--r--
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
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@51351
    14
lemma convergent_limsup_cl:
hoelzl@51351
    15
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
hoelzl@51351
    16
  shows "convergent X \<Longrightarrow> limsup X = lim X"
hoelzl@51351
    17
  by (auto simp: convergent_def limI lim_imp_Limsup)
hoelzl@51351
    18
hoelzl@51351
    19
lemma lim_increasing_cl:
hoelzl@51351
    20
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
hoelzl@51351
    21
  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
hoelzl@51351
    22
proof
hoelzl@51351
    23
  show "f ----> (SUP n. f n)"
hoelzl@51351
    24
    using assms
hoelzl@51351
    25
    by (intro increasing_tendsto)
hoelzl@51351
    26
       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
hoelzl@51351
    27
qed
hoelzl@51351
    28
hoelzl@51351
    29
lemma lim_decreasing_cl:
hoelzl@51351
    30
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
hoelzl@51351
    31
  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
hoelzl@51351
    32
proof
hoelzl@51351
    33
  show "f ----> (INF n. f n)"
hoelzl@51351
    34
    using assms
hoelzl@51351
    35
    by (intro decreasing_tendsto)
hoelzl@51351
    36
       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
hoelzl@51351
    37
qed
hoelzl@51351
    38
hoelzl@51351
    39
lemma compact_complete_linorder:
hoelzl@51351
    40
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
hoelzl@51351
    41
  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
hoelzl@51351
    42
proof -
hoelzl@51351
    43
  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
hoelzl@51351
    44
    using seq_monosub[of X] unfolding comp_def by auto
hoelzl@51351
    45
  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@51351
    46
    by (auto simp add: monoseq_def)
hoelzl@51351
    47
  then obtain l where "(X\<circ>r) ----> l"
hoelzl@51351
    48
     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"] by auto
hoelzl@51351
    49
  then show ?thesis using `subseq r` by auto
hoelzl@51351
    50
qed
hoelzl@51351
    51
hoelzl@51351
    52
lemma compact_UNIV: "compact (UNIV :: 'a::{complete_linorder, linorder_topology, second_countable_topology} set)"
hoelzl@51351
    53
  using compact_complete_linorder
hoelzl@51351
    54
  by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def)
hoelzl@51351
    55
hoelzl@51351
    56
lemma compact_eq_closed:
hoelzl@51351
    57
  fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set"
hoelzl@51351
    58
  shows "compact S \<longleftrightarrow> closed S"
hoelzl@51351
    59
  using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed by auto
hoelzl@51351
    60
hoelzl@51351
    61
lemma closed_contains_Sup_cl:
hoelzl@51351
    62
  fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set"
hoelzl@51351
    63
  assumes "closed S" "S \<noteq> {}" shows "Sup S \<in> S"
hoelzl@51351
    64
proof -
hoelzl@51351
    65
  from compact_eq_closed[of S] compact_attains_sup[of S] assms
hoelzl@51351
    66
  obtain s where "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto
hoelzl@51351
    67
  moreover then have "Sup S = s"
hoelzl@51351
    68
    by (auto intro!: Sup_eqI)
hoelzl@51351
    69
  ultimately show ?thesis
hoelzl@51351
    70
    by simp
hoelzl@51351
    71
qed
hoelzl@51351
    72
hoelzl@51351
    73
lemma closed_contains_Inf_cl:
hoelzl@51351
    74
  fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set"
hoelzl@51351
    75
  assumes "closed S" "S \<noteq> {}" shows "Inf S \<in> S"
hoelzl@51351
    76
proof -
hoelzl@51351
    77
  from compact_eq_closed[of S] compact_attains_inf[of S] assms
hoelzl@51351
    78
  obtain s where "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
hoelzl@51351
    79
  moreover then have "Inf S = s"
hoelzl@51351
    80
    by (auto intro!: Inf_eqI)
hoelzl@51351
    81
  ultimately show ?thesis
hoelzl@51351
    82
    by simp
hoelzl@51351
    83
qed
hoelzl@51351
    84
hoelzl@51351
    85
lemma ereal_dense3: 
hoelzl@51351
    86
  fixes x y :: ereal shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
hoelzl@51351
    87
proof (cases x y rule: ereal2_cases, simp_all)
hoelzl@51351
    88
  fix r q :: real assume "r < q"
hoelzl@51351
    89
  from Rats_dense_in_real[OF this]
hoelzl@51351
    90
  show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
hoelzl@51351
    91
    by (fastforce simp: Rats_def)
hoelzl@51351
    92
next
hoelzl@51351
    93
  fix r :: real show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
hoelzl@51351
    94
    using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
hoelzl@51351
    95
    by (auto simp: Rats_def)
hoelzl@51351
    96
qed
hoelzl@51351
    97
hoelzl@51351
    98
instance ereal :: second_countable_topology
hoelzl@51351
    99
proof (default, intro exI conjI)
hoelzl@51351
   100
  let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
hoelzl@51351
   101
  show "countable ?B" by (auto intro: countable_rat)
hoelzl@51351
   102
  show "open = generate_topology ?B"
hoelzl@51351
   103
  proof (intro ext iffI)
hoelzl@51351
   104
    fix S :: "ereal set" assume "open S"
hoelzl@51351
   105
    then show "generate_topology ?B S"
hoelzl@51351
   106
      unfolding open_generated_order
hoelzl@51351
   107
    proof induct
hoelzl@51351
   108
      case (Basis b)
hoelzl@51351
   109
      then obtain e where "b = {..< e} \<or> b = {e <..}" by auto
hoelzl@51351
   110
      moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}"
hoelzl@51351
   111
        by (auto dest: ereal_dense3
hoelzl@51351
   112
                 simp del: ex_simps
hoelzl@51351
   113
                 simp add: ex_simps[symmetric] conj_commute Rats_def image_iff)
hoelzl@51351
   114
      ultimately show ?case
hoelzl@51351
   115
        by (auto intro: generate_topology.intros)
hoelzl@51351
   116
    qed (auto intro: generate_topology.intros)
hoelzl@51351
   117
  next
hoelzl@51351
   118
    fix S assume "generate_topology ?B S" then show "open S" by induct auto
hoelzl@51351
   119
  qed
hoelzl@51351
   120
qed
hoelzl@51351
   121
hoelzl@43920
   122
lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
hoelzl@43920
   123
  unfolding continuous_on_topological open_ereal_def by auto
hoelzl@41980
   124
hoelzl@43920
   125
lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal"
hoelzl@41980
   126
  using continuous_on_eq_continuous_at[of UNIV] by auto
hoelzl@41980
   127
hoelzl@43920
   128
lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
hoelzl@41980
   129
  using continuous_on_eq_continuous_within[of A] by auto
hoelzl@41980
   130
hoelzl@43920
   131
lemma ereal_open_uminus:
hoelzl@43920
   132
  fixes S :: "ereal set"
hoelzl@51340
   133
  assumes "open S" shows "open (uminus ` S)"
hoelzl@51340
   134
  using `open S`[unfolded open_generated_order]
hoelzl@51340
   135
proof induct
hoelzl@51340
   136
  have "range uminus = (UNIV :: ereal set)"
hoelzl@51340
   137
    by (auto simp: image_iff ereal_uminus_eq_reorder)
hoelzl@51340
   138
  then show "open (range uminus :: ereal set)" by simp
hoelzl@51340
   139
qed (auto simp add: image_Union image_Int)
hoelzl@41980
   140
hoelzl@43920
   141
lemma ereal_uminus_complement:
hoelzl@43920
   142
  fixes S :: "ereal set"
hoelzl@41980
   143
  shows "uminus ` (- S) = - uminus ` S"
hoelzl@41980
   144
  by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
hoelzl@41980
   145
hoelzl@43920
   146
lemma ereal_closed_uminus:
hoelzl@43920
   147
  fixes S :: "ereal set"
hoelzl@41980
   148
  assumes "closed S"
hoelzl@41980
   149
  shows "closed (uminus ` S)"
hoelzl@51340
   150
  using assms unfolding closed_def ereal_uminus_complement[symmetric] by (rule ereal_open_uminus)
hoelzl@41980
   151
hoelzl@43920
   152
lemma ereal_open_closed_aux:
hoelzl@43920
   153
  fixes S :: "ereal set"
hoelzl@41980
   154
  assumes "open S" "closed S"
wenzelm@49664
   155
    and S: "(-\<infinity>) ~: S"
hoelzl@41980
   156
  shows "S = {}"
wenzelm@49664
   157
proof (rule ccontr)
hoelzl@41980
   158
  assume "S ~= {}"
hoelzl@51351
   159
  then have *: "(Inf S):S" by (metis assms(2) closed_contains_Inf_cl)
wenzelm@49664
   160
  { assume "Inf S=(-\<infinity>)"
wenzelm@49664
   161
    then have False using * assms(3) by auto }
hoelzl@41980
   162
  moreover
wenzelm@49664
   163
  { assume "Inf S=\<infinity>"
wenzelm@49664
   164
    then have "S={\<infinity>}" by (metis Inf_eq_PInfty `S ~= {}`)
wenzelm@49664
   165
    then have False by (metis assms(1) not_open_singleton) }
hoelzl@41980
   166
  moreover
hoelzl@41980
   167
  { assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
hoelzl@43920
   168
    from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this
hoelzl@41980
   169
    then obtain b where b_def: "Inf S-e<b & b<Inf S"
hoelzl@51329
   170
      using fin ereal_between[of "Inf S" e] dense[of "Inf S-e"] by auto
wenzelm@49664
   171
    then have "b: {Inf S-e <..< Inf S+e}" using e fin ereal_between[of "Inf S" e]
noschinl@44918
   172
      by auto
wenzelm@49664
   173
    then have "b:S" using e by auto
wenzelm@49664
   174
    then have False using b_def by (metis complete_lattice_class.Inf_lower leD)
hoelzl@41980
   175
  } ultimately show False by auto
hoelzl@41980
   176
qed
hoelzl@41980
   177
hoelzl@43920
   178
lemma ereal_open_closed:
hoelzl@43920
   179
  fixes S :: "ereal set"
hoelzl@41980
   180
  shows "(open S & closed S) <-> (S = {} | S = UNIV)"
wenzelm@49664
   181
proof -
wenzelm@49664
   182
  { assume lhs: "open S & closed S"
wenzelm@49664
   183
    { assume "(-\<infinity>) ~: S"
wenzelm@49664
   184
      then have "S={}" using lhs ereal_open_closed_aux by auto }
wenzelm@49664
   185
    moreover
wenzelm@49664
   186
    { assume "(-\<infinity>) : S"
wenzelm@49664
   187
      then have "(- S)={}" using lhs ereal_open_closed_aux[of "-S"] by auto }
wenzelm@49664
   188
    ultimately have "S = {} | S = UNIV" by auto
wenzelm@49664
   189
  } then show ?thesis by auto
hoelzl@41980
   190
qed
hoelzl@41980
   191
hoelzl@43920
   192
lemma ereal_open_affinity_pos:
hoelzl@43923
   193
  fixes S :: "ereal set"
hoelzl@41980
   194
  assumes "open S" and m: "m \<noteq> \<infinity>" "0 < m" and t: "\<bar>t\<bar> \<noteq> \<infinity>"
hoelzl@41980
   195
  shows "open ((\<lambda>x. m * x + t) ` S)"
hoelzl@41980
   196
proof -
hoelzl@43920
   197
  obtain r where r[simp]: "m = ereal r" using m by (cases m) auto
hoelzl@43920
   198
  obtain p where p[simp]: "t = ereal p" using t by auto
hoelzl@41980
   199
  have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0" using m by auto
hoelzl@43920
   200
  from `open S`[THEN ereal_openE] guess l u . note T = this
hoelzl@41980
   201
  let ?f = "(\<lambda>x. m * x + t)"
wenzelm@49664
   202
  show ?thesis
wenzelm@49664
   203
    unfolding open_ereal_def
hoelzl@41980
   204
  proof (intro conjI impI exI subsetI)
hoelzl@43920
   205
    have "ereal -` ?f ` S = (\<lambda>x. r * x + p) ` (ereal -` S)"
hoelzl@41980
   206
    proof safe
wenzelm@49664
   207
      fix x y
wenzelm@49664
   208
      assume "ereal y = m * x + t" "x \<in> S"
hoelzl@43920
   209
      then show "y \<in> (\<lambda>x. r * x + p) ` ereal -` S"
hoelzl@41980
   210
        using `r \<noteq> 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm)
hoelzl@41980
   211
    qed force
hoelzl@43920
   212
    then show "open (ereal -` ?f ` S)"
hoelzl@41980
   213
      using open_affinity[OF T(1) `r \<noteq> 0`] by (auto simp: ac_simps)
hoelzl@41980
   214
  next
wenzelm@49664
   215
    assume "\<infinity> \<in> ?f`S"
wenzelm@49664
   216
    with `0 < r` have "\<infinity> \<in> S" by auto
wenzelm@49664
   217
    fix x
wenzelm@49664
   218
    assume "x \<in> {ereal (r * l + p)<..}"
hoelzl@43920
   219
    then have [simp]: "ereal (r * l + p) < x" by auto
hoelzl@41980
   220
    show "x \<in> ?f`S"
hoelzl@41980
   221
    proof (rule image_eqI)
hoelzl@41980
   222
      show "x = m * ((x - t) / m) + t"
hoelzl@43920
   223
        using m t by (cases rule: ereal3_cases[of m x t]) auto
hoelzl@43920
   224
      have "ereal l < (x - t)/m"
hoelzl@43920
   225
        using m t by (simp add: ereal_less_divide_pos ereal_less_minus)
hoelzl@41980
   226
      then show "(x - t)/m \<in> S" using T(2)[OF `\<infinity> \<in> S`] by auto
hoelzl@41980
   227
    qed
hoelzl@41980
   228
  next
hoelzl@41980
   229
    assume "-\<infinity> \<in> ?f`S" with `0 < r` have "-\<infinity> \<in> S" by auto
hoelzl@43920
   230
    fix x assume "x \<in> {..<ereal (r * u + p)}"
hoelzl@43920
   231
    then have [simp]: "x < ereal (r * u + p)" by auto
hoelzl@41980
   232
    show "x \<in> ?f`S"
hoelzl@41980
   233
    proof (rule image_eqI)
hoelzl@41980
   234
      show "x = m * ((x - t) / m) + t"
hoelzl@43920
   235
        using m t by (cases rule: ereal3_cases[of m x t]) auto
hoelzl@43920
   236
      have "(x - t)/m < ereal u"
hoelzl@43920
   237
        using m t by (simp add: ereal_divide_less_pos ereal_minus_less)
hoelzl@41980
   238
      then show "(x - t)/m \<in> S" using T(3)[OF `-\<infinity> \<in> S`] by auto
hoelzl@41980
   239
    qed
hoelzl@41980
   240
  qed
hoelzl@41980
   241
qed
hoelzl@41980
   242
hoelzl@43920
   243
lemma ereal_open_affinity:
hoelzl@43923
   244
  fixes S :: "ereal set"
wenzelm@49664
   245
  assumes "open S"
wenzelm@49664
   246
    and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0"
wenzelm@49664
   247
    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
hoelzl@41980
   248
  shows "open ((\<lambda>x. m * x + t) ` S)"
hoelzl@41980
   249
proof cases
wenzelm@49664
   250
  assume "0 < m"
wenzelm@49664
   251
  then show ?thesis
hoelzl@43920
   252
    using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m by auto
hoelzl@41980
   253
next
hoelzl@41980
   254
  assume "\<not> 0 < m" then
hoelzl@41980
   255
  have "0 < -m" using `m \<noteq> 0` by (cases m) auto
hoelzl@41980
   256
  then have m: "-m \<noteq> \<infinity>" "0 < -m" using `\<bar>m\<bar> \<noteq> \<infinity>`
hoelzl@43920
   257
    by (auto simp: ereal_uminus_eq_reorder)
hoelzl@43920
   258
  from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t]
hoelzl@41980
   259
  show ?thesis unfolding image_image by simp
hoelzl@41980
   260
qed
hoelzl@41980
   261
hoelzl@43920
   262
lemma ereal_lim_mult:
hoelzl@43920
   263
  fixes X :: "'a \<Rightarrow> ereal"
wenzelm@49664
   264
  assumes lim: "(X ---> L) net"
wenzelm@49664
   265
    and a: "\<bar>a\<bar> \<noteq> \<infinity>"
hoelzl@41980
   266
  shows "((\<lambda>i. a * X i) ---> a * L) net"
hoelzl@41980
   267
proof cases
hoelzl@41980
   268
  assume "a \<noteq> 0"
hoelzl@41980
   269
  show ?thesis
hoelzl@41980
   270
  proof (rule topological_tendstoI)
wenzelm@49664
   271
    fix S
wenzelm@49664
   272
    assume "open S" "a * L \<in> S"
hoelzl@41980
   273
    have "a * L / a = L"
hoelzl@43920
   274
      using `a \<noteq> 0` a by (cases rule: ereal2_cases[of a L]) auto
hoelzl@41980
   275
    then have L: "L \<in> ((\<lambda>x. x / a) ` S)"
hoelzl@41980
   276
      using `a * L \<in> S` by (force simp: image_iff)
hoelzl@41980
   277
    moreover have "open ((\<lambda>x. x / a) ` S)"
hoelzl@43920
   278
      using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a
hoelzl@43920
   279
      by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps)
hoelzl@41980
   280
    note * = lim[THEN topological_tendstoD, OF this L]
wenzelm@49664
   281
    { fix x
wenzelm@49664
   282
      from a `a \<noteq> 0` have "a * (x / a) = x"
hoelzl@43920
   283
        by (cases rule: ereal2_cases[of a x]) auto }
hoelzl@41980
   284
    note this[simp]
hoelzl@41980
   285
    show "eventually (\<lambda>x. a * X x \<in> S) net"
hoelzl@41980
   286
      by (rule eventually_mono[OF _ *]) auto
hoelzl@41980
   287
  qed
noschinl@44918
   288
qed auto
hoelzl@41980
   289
hoelzl@43920
   290
lemma ereal_lim_uminus:
wenzelm@49664
   291
  fixes X :: "'a \<Rightarrow> ereal"
wenzelm@49664
   292
  shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net"
hoelzl@43920
   293
  using ereal_lim_mult[of X L net "ereal (-1)"]
wenzelm@49664
   294
    ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"]
hoelzl@41980
   295
  by (auto simp add: algebra_simps)
hoelzl@41980
   296
hoelzl@43923
   297
lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
hoelzl@41980
   298
proof
hoelzl@41980
   299
  assume "x = -\<infinity>" then have "{x..} = UNIV" by auto
hoelzl@41980
   300
  then show "open {x..}" by auto
hoelzl@41980
   301
next
hoelzl@41980
   302
  assume "open {x..}"
hoelzl@41980
   303
  then have "open {x..} \<and> closed {x..}" by auto
hoelzl@43920
   304
  then have "{x..} = UNIV" unfolding ereal_open_closed by auto
hoelzl@43920
   305
  then show "x = -\<infinity>" by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
hoelzl@41980
   306
qed
hoelzl@41980
   307
hoelzl@43920
   308
lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)"
hoelzl@43920
   309
  using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto
hoelzl@41980
   310
hoelzl@43920
   311
lemma ereal_Liminf_uminus:
hoelzl@43920
   312
  fixes f :: "'a => ereal"
hoelzl@41980
   313
  shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)"
hoelzl@43920
   314
  using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
hoelzl@41980
   315
hoelzl@43920
   316
lemma ereal_Lim_uminus:
wenzelm@49664
   317
  fixes f :: "'a \<Rightarrow> ereal"
wenzelm@49664
   318
  shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net"
hoelzl@41980
   319
  using
hoelzl@43920
   320
    ereal_lim_mult[of f f0 net "- 1"]
hoelzl@43920
   321
    ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
hoelzl@43920
   322
  by (auto simp: ereal_uminus_reorder)
hoelzl@41980
   323
hoelzl@41980
   324
lemma Liminf_PInfty:
hoelzl@43920
   325
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@41980
   326
  assumes "\<not> trivial_limit net"
hoelzl@41980
   327
  shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
hoelzl@51351
   328
  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] using Liminf_le_Limsup[OF assms, of f] by auto
hoelzl@41980
   329
hoelzl@41980
   330
lemma Limsup_MInfty:
hoelzl@43920
   331
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@41980
   332
  assumes "\<not> trivial_limit net"
hoelzl@41980
   333
  shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
hoelzl@51351
   334
  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] using Liminf_le_Limsup[OF assms, of f] by auto
hoelzl@41980
   335
hoelzl@50104
   336
lemma convergent_ereal:
hoelzl@51351
   337
  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
hoelzl@50104
   338
  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
hoelzl@51340
   339
  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
hoelzl@50104
   340
  by (auto simp: convergent_def)
hoelzl@50104
   341
hoelzl@41980
   342
lemma liminf_PInfty:
hoelzl@51351
   343
  fixes X :: "nat \<Rightarrow> ereal"
hoelzl@51351
   344
  shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
wenzelm@49664
   345
  by (metis Liminf_PInfty trivial_limit_sequentially)
hoelzl@41980
   346
hoelzl@41980
   347
lemma limsup_MInfty:
hoelzl@51351
   348
  fixes X :: "nat \<Rightarrow> ereal"
hoelzl@51351
   349
  shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
wenzelm@49664
   350
  by (metis Limsup_MInfty trivial_limit_sequentially)
hoelzl@41980
   351
hoelzl@43920
   352
lemma ereal_lim_mono:
hoelzl@51351
   353
  fixes X Y :: "nat => 'a::linorder_topology"
hoelzl@41980
   354
  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
wenzelm@49664
   355
    and "X ----> x" "Y ----> y"
hoelzl@41980
   356
  shows "x <= y"
hoelzl@51000
   357
  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
hoelzl@41980
   358
hoelzl@43920
   359
lemma incseq_le_ereal:
hoelzl@51351
   360
  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
hoelzl@41980
   361
  assumes inc: "incseq X" and lim: "X ----> L"
hoelzl@41980
   362
  shows "X N \<le> L"
wenzelm@49664
   363
  using inc by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
hoelzl@41980
   364
wenzelm@49664
   365
lemma decseq_ge_ereal:
wenzelm@49664
   366
  assumes dec: "decseq X"
hoelzl@51351
   367
    and lim: "X ----> (L::'a::linorder_topology)"
wenzelm@49664
   368
  shows "X N >= L"
wenzelm@49664
   369
  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
hoelzl@41980
   370
hoelzl@41980
   371
lemma bounded_abs:
hoelzl@41980
   372
  assumes "(a::real)<=x" "x<=b"
hoelzl@41980
   373
  shows "abs x <= max (abs a) (abs b)"
wenzelm@49664
   374
  by (metis abs_less_iff assms leI le_max_iff_disj
wenzelm@49664
   375
    less_eq_real_def less_le_not_le less_minus_iff minus_minus)
hoelzl@41980
   376
hoelzl@43920
   377
lemma ereal_Sup_lim:
hoelzl@51351
   378
  assumes "\<And>n. b n \<in> s" "b ----> (a::'a::{complete_linorder, linorder_topology})"
hoelzl@41980
   379
  shows "a \<le> Sup s"
wenzelm@49664
   380
  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
hoelzl@41980
   381
hoelzl@43920
   382
lemma ereal_Inf_lim:
hoelzl@51351
   383
  assumes "\<And>n. b n \<in> s" "b ----> (a::'a::{complete_linorder, linorder_topology})"
hoelzl@41980
   384
  shows "Inf s \<le> a"
wenzelm@49664
   385
  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
hoelzl@41980
   386
hoelzl@43920
   387
lemma SUP_Lim_ereal:
hoelzl@51000
   388
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
hoelzl@51351
   389
  assumes inc: "incseq X" and l: "X ----> l" shows "(SUP n. X n) = l"
hoelzl@51000
   390
  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] by simp
hoelzl@41980
   391
hoelzl@51351
   392
lemma INF_Lim_ereal:
hoelzl@51351
   393
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
hoelzl@51351
   394
  assumes dec: "decseq X" and l: "X ----> l" shows "(INF n. X n) = l"
hoelzl@51351
   395
  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l] by simp
hoelzl@41980
   396
hoelzl@41980
   397
lemma SUP_eq_LIMSEQ:
hoelzl@41980
   398
  assumes "mono f"
hoelzl@43920
   399
  shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
hoelzl@41980
   400
proof
hoelzl@43920
   401
  have inc: "incseq (\<lambda>i. ereal (f i))"
hoelzl@41980
   402
    using `mono f` unfolding mono_def incseq_def by auto
hoelzl@41980
   403
  { assume "f ----> x"
wenzelm@49664
   404
    then have "(\<lambda>i. ereal (f i)) ----> ereal x" by auto
wenzelm@49664
   405
    from SUP_Lim_ereal[OF inc this]
wenzelm@49664
   406
    show "(SUP n. ereal (f n)) = ereal x" . }
hoelzl@43920
   407
  { assume "(SUP n. ereal (f n)) = ereal x"
hoelzl@51000
   408
    with LIMSEQ_SUP[OF inc]
hoelzl@41980
   409
    show "f ----> x" by auto }
hoelzl@41980
   410
qed
hoelzl@41980
   411
hoelzl@43920
   412
lemma liminf_ereal_cminus:
wenzelm@49664
   413
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   414
  assumes "c \<noteq> -\<infinity>"
hoelzl@42950
   415
  shows "liminf (\<lambda>x. c - f x) = c - limsup f"
hoelzl@42950
   416
proof (cases c)
wenzelm@49664
   417
  case PInf
wenzelm@49664
   418
  then show ?thesis by (simp add: Liminf_const)
hoelzl@42950
   419
next
wenzelm@49664
   420
  case (real r)
wenzelm@49664
   421
  then show ?thesis
hoelzl@42950
   422
    unfolding liminf_SUPR_INFI limsup_INFI_SUPR
hoelzl@43920
   423
    apply (subst INFI_ereal_cminus)
hoelzl@42950
   424
    apply auto
hoelzl@43920
   425
    apply (subst SUPR_ereal_cminus)
hoelzl@42950
   426
    apply auto
hoelzl@42950
   427
    done
hoelzl@42950
   428
qed (insert `c \<noteq> -\<infinity>`, simp)
hoelzl@42950
   429
wenzelm@49664
   430
hoelzl@41980
   431
subsubsection {* Continuity *}
hoelzl@41980
   432
hoelzl@43920
   433
lemma continuous_at_of_ereal:
hoelzl@43920
   434
  fixes x0 :: ereal
hoelzl@41980
   435
  assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
hoelzl@41980
   436
  shows "continuous (at x0) real"
wenzelm@49664
   437
proof -
wenzelm@49664
   438
  { fix T
wenzelm@49664
   439
    assume T_def: "open T & real x0 : T"
wenzelm@49664
   440
    def S == "ereal ` T"
wenzelm@49664
   441
    then have "ereal (real x0) : S" using T_def by auto
wenzelm@49664
   442
    then have "x0 : S" using assms ereal_real by auto
wenzelm@49664
   443
    moreover have "open S" using open_ereal S_def T_def by auto
wenzelm@49664
   444
    moreover have "ALL y:S. real y : T" using S_def T_def by auto
wenzelm@49664
   445
    ultimately have "EX S. x0 : S & open S & (ALL y:S. real y : T)" by auto
wenzelm@49664
   446
  }
wenzelm@49664
   447
  then show ?thesis unfolding continuous_at_open by blast
hoelzl@41980
   448
qed
hoelzl@41980
   449
hoelzl@41980
   450
hoelzl@43920
   451
lemma continuous_at_iff_ereal:
wenzelm@49664
   452
  fixes f :: "'a::t2_space => real"
wenzelm@49664
   453
  shows "continuous (at x0) f <-> continuous (at x0) (ereal o f)"
wenzelm@49664
   454
proof -
wenzelm@49664
   455
  { assume "continuous (at x0) f"
wenzelm@49664
   456
    then have "continuous (at x0) (ereal o f)"
wenzelm@49664
   457
      using continuous_at_ereal continuous_at_compose[of x0 f ereal] by auto
wenzelm@49664
   458
  }
wenzelm@49664
   459
  moreover
wenzelm@49664
   460
  { assume "continuous (at x0) (ereal o f)"
wenzelm@49664
   461
    then have "continuous (at x0) (real o (ereal o f))"
wenzelm@49664
   462
      using continuous_at_of_ereal by (intro continuous_at_compose[of x0 "ereal o f"]) auto
wenzelm@49664
   463
    moreover have "real o (ereal o f) = f" using real_ereal_id by (simp add: o_assoc)
wenzelm@49664
   464
    ultimately have "continuous (at x0) f" by auto
wenzelm@49664
   465
  } ultimately show ?thesis by auto
hoelzl@41980
   466
qed
hoelzl@41980
   467
hoelzl@41980
   468
hoelzl@43920
   469
lemma continuous_on_iff_ereal:
wenzelm@49664
   470
  fixes f :: "'a::t2_space => real"
wenzelm@49664
   471
  fixes A assumes "open A"
wenzelm@49664
   472
  shows "continuous_on A f <-> continuous_on A (ereal o f)"
hoelzl@51481
   473
  using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong)
hoelzl@41980
   474
hoelzl@41980
   475
hoelzl@43923
   476
lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>::ereal)}) real"
wenzelm@49664
   477
  using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal by auto
hoelzl@41980
   478
hoelzl@41980
   479
hoelzl@41980
   480
lemma continuous_on_iff_real:
hoelzl@43920
   481
  fixes f :: "'a::t2_space => ereal"
hoelzl@41980
   482
  assumes "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
hoelzl@41980
   483
  shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
wenzelm@49664
   484
proof -
hoelzl@41980
   485
  have "f ` A <= UNIV-{\<infinity>,(-\<infinity>)}" using assms by force
wenzelm@49664
   486
  then have *: "continuous_on (f ` A) real"
wenzelm@49664
   487
    using continuous_on_real by (simp add: continuous_on_subset)
wenzelm@49664
   488
  have **: "continuous_on ((real o f) ` A) ereal"
wenzelm@49664
   489
    using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real o f) ` A"] by blast
wenzelm@49664
   490
  { assume "continuous_on A f"
wenzelm@49664
   491
    then have "continuous_on A (real o f)"
wenzelm@49664
   492
      apply (subst continuous_on_compose)
wenzelm@49664
   493
      using * apply auto
wenzelm@49664
   494
      done
wenzelm@49664
   495
  }
wenzelm@49664
   496
  moreover
wenzelm@49664
   497
  { assume "continuous_on A (real o f)"
wenzelm@49664
   498
    then have "continuous_on A (ereal o (real o f))"
wenzelm@49664
   499
      apply (subst continuous_on_compose)
wenzelm@49664
   500
      using ** apply auto
wenzelm@49664
   501
      done
wenzelm@49664
   502
    then have "continuous_on A f"
wenzelm@49664
   503
      apply (subst continuous_on_eq[of A "ereal o (real o f)" f])
wenzelm@49664
   504
      using assms ereal_real apply auto
wenzelm@49664
   505
      done
wenzelm@49664
   506
  }
wenzelm@49664
   507
  ultimately show ?thesis by auto
hoelzl@41980
   508
qed
hoelzl@41980
   509
hoelzl@41980
   510
hoelzl@41980
   511
lemma continuous_at_const:
hoelzl@43920
   512
  fixes f :: "'a::t2_space => ereal"
hoelzl@41980
   513
  assumes "ALL x. (f x = C)"
hoelzl@41980
   514
  shows "ALL x. continuous (at x) f"
wenzelm@49664
   515
  unfolding continuous_at_open using assms t1_space by auto
hoelzl@41980
   516
hoelzl@41980
   517
hoelzl@41980
   518
lemma mono_closed_real:
hoelzl@41980
   519
  fixes S :: "real set"
hoelzl@41980
   520
  assumes mono: "ALL y z. y:S & y<=z --> z:S"
wenzelm@49664
   521
    and "closed S"
hoelzl@41980
   522
  shows "S = {} | S = UNIV | (EX a. S = {a ..})"
wenzelm@49664
   523
proof -
wenzelm@49664
   524
  { assume "S ~= {}"
wenzelm@49664
   525
    { assume ex: "EX B. ALL x:S. B<=x"
hoelzl@51475
   526
      then have *: "ALL x:S. Inf S <= x" using cInf_lower_EX[of _ S] ex by metis
wenzelm@49664
   527
      then have "Inf S : S" apply (subst closed_contains_Inf) using ex `S ~= {}` `closed S` by auto
wenzelm@49664
   528
      then have "ALL x. (Inf S <= x <-> x:S)" using mono[rule_format, of "Inf S"] * by auto
wenzelm@49664
   529
      then have "S = {Inf S ..}" by auto
wenzelm@49664
   530
      then have "EX a. S = {a ..}" by auto
wenzelm@49664
   531
    }
wenzelm@49664
   532
    moreover
wenzelm@49664
   533
    { assume "~(EX B. ALL x:S. B<=x)"
wenzelm@49664
   534
      then have nex: "ALL B. EX x:S. x<B" by (simp add: not_le)
wenzelm@49664
   535
      { fix y
wenzelm@49664
   536
        obtain x where "x:S & x < y" using nex by auto
wenzelm@49664
   537
        then have "y:S" using mono[rule_format, of x y] by auto
wenzelm@49664
   538
      } then have "S = UNIV" by auto
wenzelm@49664
   539
    }
wenzelm@49664
   540
    ultimately have "S = UNIV | (EX a. S = {a ..})" by blast
wenzelm@49664
   541
  } then show ?thesis by blast
hoelzl@41980
   542
qed
hoelzl@41980
   543
hoelzl@41980
   544
hoelzl@43920
   545
lemma mono_closed_ereal:
hoelzl@41980
   546
  fixes S :: "real set"
hoelzl@41980
   547
  assumes mono: "ALL y z. y:S & y<=z --> z:S"
wenzelm@49664
   548
    and "closed S"
hoelzl@43920
   549
  shows "EX a. S = {x. a <= ereal x}"
wenzelm@49664
   550
proof -
wenzelm@49664
   551
  { assume "S = {}"
wenzelm@49664
   552
    then have ?thesis apply(rule_tac x=PInfty in exI) by auto }
wenzelm@49664
   553
  moreover
wenzelm@49664
   554
  { assume "S = UNIV"
wenzelm@49664
   555
    then have ?thesis apply(rule_tac x="-\<infinity>" in exI) by auto }
wenzelm@49664
   556
  moreover
wenzelm@49664
   557
  { assume "EX a. S = {a ..}"
wenzelm@49664
   558
    then obtain a where "S={a ..}" by auto
wenzelm@49664
   559
    then have ?thesis apply(rule_tac x="ereal a" in exI) by auto
wenzelm@49664
   560
  }
wenzelm@49664
   561
  ultimately show ?thesis using mono_closed_real[of S] assms by auto
hoelzl@41980
   562
qed
hoelzl@41980
   563
hoelzl@41980
   564
subsection {* Sums *}
hoelzl@41980
   565
wenzelm@49664
   566
lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
hoelzl@41980
   567
proof cases
wenzelm@49664
   568
  assume "finite A"
wenzelm@49664
   569
  then show ?thesis by induct auto
hoelzl@41980
   570
qed simp
hoelzl@41980
   571
hoelzl@43923
   572
lemma setsum_Pinfty:
hoelzl@43923
   573
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@43923
   574
  shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))"
hoelzl@41980
   575
proof safe
hoelzl@41980
   576
  assume *: "setsum f P = \<infinity>"
hoelzl@41980
   577
  show "finite P"
hoelzl@41980
   578
  proof (rule ccontr) assume "infinite P" with * show False by auto qed
hoelzl@41980
   579
  show "\<exists>i\<in>P. f i = \<infinity>"
hoelzl@41980
   580
  proof (rule ccontr)
hoelzl@41980
   581
    assume "\<not> ?thesis" then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>" by auto
hoelzl@41980
   582
    from `finite P` this have "setsum f P \<noteq> \<infinity>"
hoelzl@41980
   583
      by induct auto
hoelzl@41980
   584
    with * show False by auto
hoelzl@41980
   585
  qed
hoelzl@41980
   586
next
hoelzl@41980
   587
  fix i assume "finite P" "i \<in> P" "f i = \<infinity>"
wenzelm@49664
   588
  then show "setsum f P = \<infinity>"
hoelzl@41980
   589
  proof induct
hoelzl@41980
   590
    case (insert x A)
hoelzl@41980
   591
    show ?case using insert by (cases "x = i") auto
hoelzl@41980
   592
  qed simp
hoelzl@41980
   593
qed
hoelzl@41980
   594
hoelzl@41980
   595
lemma setsum_Inf:
hoelzl@43923
   596
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@41980
   597
  shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>))"
hoelzl@41980
   598
proof
hoelzl@41980
   599
  assume *: "\<bar>setsum f A\<bar> = \<infinity>"
hoelzl@41980
   600
  have "finite A" by (rule ccontr) (insert *, auto)
hoelzl@41980
   601
  moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>"
hoelzl@41980
   602
  proof (rule ccontr)
hoelzl@43920
   603
    assume "\<not> ?thesis" then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto
hoelzl@41980
   604
    from bchoice[OF this] guess r ..
huffman@44142
   605
    with * show False by auto
hoelzl@41980
   606
  qed
hoelzl@41980
   607
  ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" by auto
hoelzl@41980
   608
next
hoelzl@41980
   609
  assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
hoelzl@41980
   610
  then obtain i where "finite A" "i \<in> A" "\<bar>f i\<bar> = \<infinity>" by auto
hoelzl@41980
   611
  then show "\<bar>setsum f A\<bar> = \<infinity>"
hoelzl@41980
   612
  proof induct
hoelzl@41980
   613
    case (insert j A) then show ?case
hoelzl@43920
   614
      by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
hoelzl@41980
   615
  qed simp
hoelzl@41980
   616
qed
hoelzl@41980
   617
hoelzl@43920
   618
lemma setsum_real_of_ereal:
hoelzl@43923
   619
  fixes f :: "'i \<Rightarrow> ereal"
hoelzl@41980
   620
  assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
hoelzl@41980
   621
  shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
hoelzl@41980
   622
proof -
hoelzl@43920
   623
  have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
hoelzl@41980
   624
  proof
hoelzl@41980
   625
    fix x assume "x \<in> S"
hoelzl@43920
   626
    from assms[OF this] show "\<exists>r. f x = ereal r" by (cases "f x") auto
hoelzl@41980
   627
  qed
hoelzl@41980
   628
  from bchoice[OF this] guess r ..
hoelzl@41980
   629
  then show ?thesis by simp
hoelzl@41980
   630
qed
hoelzl@41980
   631
hoelzl@43920
   632
lemma setsum_ereal_0:
hoelzl@43920
   633
  fixes f :: "'a \<Rightarrow> ereal" assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
hoelzl@41980
   634
  shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
hoelzl@41980
   635
proof
hoelzl@41980
   636
  assume *: "(\<Sum>x\<in>A. f x) = 0"
hoelzl@41980
   637
  then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>" by auto
hoelzl@41980
   638
  then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>" using assms by (force simp: setsum_Pinfty)
hoelzl@43920
   639
  then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto
hoelzl@41980
   640
  from bchoice[OF this] * assms show "\<forall>i\<in>A. f i = 0"
hoelzl@41980
   641
    using setsum_nonneg_eq_0_iff[of A "\<lambda>i. real (f i)"] by auto
hoelzl@41980
   642
qed (rule setsum_0')
hoelzl@41980
   643
hoelzl@41980
   644
hoelzl@43920
   645
lemma setsum_ereal_right_distrib:
wenzelm@49664
   646
  fixes f :: "'a \<Rightarrow> ereal"
wenzelm@49664
   647
  assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
hoelzl@41980
   648
  shows "r * setsum f A = (\<Sum>n\<in>A. r * f n)"
hoelzl@41980
   649
proof cases
wenzelm@49664
   650
  assume "finite A"
wenzelm@49664
   651
  then show ?thesis using assms
hoelzl@43920
   652
    by induct (auto simp: ereal_right_distrib setsum_nonneg)
hoelzl@41980
   653
qed simp
hoelzl@41980
   654
hoelzl@43920
   655
lemma sums_ereal_positive:
wenzelm@49664
   656
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   657
  assumes "\<And>i. 0 \<le> f i"
wenzelm@49664
   658
  shows "f sums (SUP n. \<Sum>i<n. f i)"
hoelzl@41980
   659
proof -
hoelzl@41980
   660
  have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
hoelzl@43920
   661
    using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)
hoelzl@51000
   662
  from LIMSEQ_SUP[OF this]
hoelzl@41980
   663
  show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)
hoelzl@41980
   664
qed
hoelzl@41980
   665
hoelzl@43920
   666
lemma summable_ereal_pos:
wenzelm@49664
   667
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   668
  assumes "\<And>i. 0 \<le> f i"
wenzelm@49664
   669
  shows "summable f"
hoelzl@43920
   670
  using sums_ereal_positive[of f, OF assms] unfolding summable_def by auto
hoelzl@41980
   671
hoelzl@43920
   672
lemma suminf_ereal_eq_SUPR:
wenzelm@49664
   673
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   674
  assumes "\<And>i. 0 \<le> f i"
hoelzl@41980
   675
  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
hoelzl@43920
   676
  using sums_ereal_positive[of f, OF assms, THEN sums_unique] by simp
hoelzl@41980
   677
wenzelm@49664
   678
lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
hoelzl@41980
   679
  unfolding sums_def by simp
hoelzl@41980
   680
hoelzl@41980
   681
lemma suminf_bound:
hoelzl@43920
   682
  fixes f :: "nat \<Rightarrow> ereal"
hoelzl@41980
   683
  assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x" and pos: "\<And>n. 0 \<le> f n"
hoelzl@41980
   684
  shows "suminf f \<le> x"
hoelzl@43920
   685
proof (rule Lim_bounded_ereal)
hoelzl@43920
   686
  have "summable f" using pos[THEN summable_ereal_pos] .
hoelzl@41980
   687
  then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
hoelzl@41980
   688
    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
hoelzl@41980
   689
  show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
hoelzl@41980
   690
    using assms by auto
hoelzl@41980
   691
qed
hoelzl@41980
   692
hoelzl@41980
   693
lemma suminf_bound_add:
hoelzl@43920
   694
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   695
  assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
wenzelm@49664
   696
    and pos: "\<And>n. 0 \<le> f n"
wenzelm@49664
   697
    and "y \<noteq> -\<infinity>"
hoelzl@41980
   698
  shows "suminf f + y \<le> x"
hoelzl@41980
   699
proof (cases y)
wenzelm@49664
   700
  case (real r)
wenzelm@49664
   701
  then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
hoelzl@43920
   702
    using assms by (simp add: ereal_le_minus)
hoelzl@41980
   703
  then have "(\<Sum> n. f n) \<le> x - y" using pos by (rule suminf_bound)
hoelzl@41980
   704
  then show "(\<Sum> n. f n) + y \<le> x"
hoelzl@43920
   705
    using assms real by (simp add: ereal_le_minus)
hoelzl@41980
   706
qed (insert assms, auto)
hoelzl@41980
   707
hoelzl@41980
   708
lemma suminf_upper:
wenzelm@49664
   709
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   710
  assumes "\<And>n. 0 \<le> f n"
hoelzl@41980
   711
  shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
hoelzl@44928
   712
  unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
huffman@45031
   713
  by (auto intro: complete_lattice_class.Sup_upper)
hoelzl@41980
   714
hoelzl@41980
   715
lemma suminf_0_le:
wenzelm@49664
   716
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   717
  assumes "\<And>n. 0 \<le> f n"
hoelzl@41980
   718
  shows "0 \<le> (\<Sum>n. f n)"
hoelzl@41980
   719
  using suminf_upper[of f 0, OF assms] by simp
hoelzl@41980
   720
hoelzl@41980
   721
lemma suminf_le_pos:
hoelzl@43920
   722
  fixes f g :: "nat \<Rightarrow> ereal"
hoelzl@41980
   723
  assumes "\<And>N. f N \<le> g N" "\<And>N. 0 \<le> f N"
hoelzl@41980
   724
  shows "suminf f \<le> suminf g"
hoelzl@41980
   725
proof (safe intro!: suminf_bound)
wenzelm@49664
   726
  fix n
wenzelm@49664
   727
  { fix N have "0 \<le> g N" using assms(2,1)[of N] by auto }
wenzelm@49664
   728
  have "setsum f {..<n} \<le> setsum g {..<n}"
wenzelm@49664
   729
    using assms by (auto intro: setsum_mono)
hoelzl@41980
   730
  also have "... \<le> suminf g" using `\<And>N. 0 \<le> g N` by (rule suminf_upper)
hoelzl@41980
   731
  finally show "setsum f {..<n} \<le> suminf g" .
hoelzl@41980
   732
qed (rule assms(2))
hoelzl@41980
   733
hoelzl@43920
   734
lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal)^Suc n) = 1"
hoelzl@43920
   735
  using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
hoelzl@43920
   736
  by (simp add: one_ereal_def)
hoelzl@41980
   737
hoelzl@43920
   738
lemma suminf_add_ereal:
hoelzl@43920
   739
  fixes f g :: "nat \<Rightarrow> ereal"
hoelzl@41980
   740
  assumes "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
hoelzl@41980
   741
  shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
hoelzl@43920
   742
  apply (subst (1 2 3) suminf_ereal_eq_SUPR)
hoelzl@41980
   743
  unfolding setsum_addf
wenzelm@49664
   744
  apply (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
wenzelm@49664
   745
  done
hoelzl@41980
   746
hoelzl@43920
   747
lemma suminf_cmult_ereal:
hoelzl@43920
   748
  fixes f g :: "nat \<Rightarrow> ereal"
hoelzl@41980
   749
  assumes "\<And>i. 0 \<le> f i" "0 \<le> a"
hoelzl@41980
   750
  shows "(\<Sum>i. a * f i) = a * suminf f"
hoelzl@43920
   751
  by (auto simp: setsum_ereal_right_distrib[symmetric] assms
hoelzl@43920
   752
                 ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR
hoelzl@43920
   753
           intro!: SUPR_ereal_cmult )
hoelzl@41980
   754
hoelzl@41980
   755
lemma suminf_PInfty:
hoelzl@43923
   756
  fixes f :: "nat \<Rightarrow> ereal"
hoelzl@41980
   757
  assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>"
hoelzl@41980
   758
  shows "f i \<noteq> \<infinity>"
hoelzl@41980
   759
proof -
hoelzl@41980
   760
  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
hoelzl@41980
   761
  have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>" by auto
wenzelm@49664
   762
  then show ?thesis unfolding setsum_Pinfty by simp
hoelzl@41980
   763
qed
hoelzl@41980
   764
hoelzl@41980
   765
lemma suminf_PInfty_fun:
hoelzl@41980
   766
  assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>"
hoelzl@43920
   767
  shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
hoelzl@41980
   768
proof -
hoelzl@43920
   769
  have "\<forall>i. \<exists>r. f i = ereal r"
hoelzl@41980
   770
  proof
hoelzl@43920
   771
    fix i show "\<exists>r. f i = ereal r"
hoelzl@41980
   772
      using suminf_PInfty[OF assms] assms(1)[of i] by (cases "f i") auto
hoelzl@41980
   773
  qed
hoelzl@41980
   774
  from choice[OF this] show ?thesis by auto
hoelzl@41980
   775
qed
hoelzl@41980
   776
hoelzl@43920
   777
lemma summable_ereal:
hoelzl@43920
   778
  assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
hoelzl@41980
   779
  shows "summable f"
hoelzl@41980
   780
proof -
hoelzl@43920
   781
  have "0 \<le> (\<Sum>i. ereal (f i))"
hoelzl@41980
   782
    using assms by (intro suminf_0_le) auto
hoelzl@43920
   783
  with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
hoelzl@43920
   784
    by (cases "\<Sum>i. ereal (f i)") auto
hoelzl@43920
   785
  from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
hoelzl@43920
   786
  have "summable (\<lambda>x. ereal (f x))" using assms by auto
hoelzl@41980
   787
  from summable_sums[OF this]
hoelzl@43920
   788
  have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))" by auto
hoelzl@41980
   789
  then show "summable f"
hoelzl@43920
   790
    unfolding r sums_ereal summable_def ..
hoelzl@41980
   791
qed
hoelzl@41980
   792
hoelzl@43920
   793
lemma suminf_ereal:
hoelzl@43920
   794
  assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
hoelzl@43920
   795
  shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
hoelzl@41980
   796
proof (rule sums_unique[symmetric])
hoelzl@43920
   797
  from summable_ereal[OF assms]
hoelzl@43920
   798
  show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
hoelzl@43920
   799
    unfolding sums_ereal using assms by (intro summable_sums summable_ereal)
hoelzl@41980
   800
qed
hoelzl@41980
   801
hoelzl@43920
   802
lemma suminf_ereal_minus:
hoelzl@43920
   803
  fixes f g :: "nat \<Rightarrow> ereal"
hoelzl@41980
   804
  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
   805
  shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
hoelzl@41980
   806
proof -
hoelzl@41980
   807
  { fix i have "0 \<le> f i" using ord[of i] by auto }
hoelzl@41980
   808
  moreover
hoelzl@41980
   809
  from suminf_PInfty_fun[OF `\<And>i. 0 \<le> f i` fin(1)] guess f' .. note this[simp]
hoelzl@41980
   810
  from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] guess g' .. note this[simp]
hoelzl@43920
   811
  { fix i have "0 \<le> f i - g i" using ord[of i] by (auto simp: ereal_le_minus_iff) }
hoelzl@41980
   812
  moreover
hoelzl@41980
   813
  have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
hoelzl@41980
   814
    using assms by (auto intro!: suminf_le_pos simp: field_simps)
hoelzl@41980
   815
  then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>" using fin by auto
hoelzl@41980
   816
  ultimately show ?thesis using assms `\<And>i. 0 \<le> f i`
hoelzl@41980
   817
    apply simp
wenzelm@49664
   818
    apply (subst (1 2 3) suminf_ereal)
wenzelm@49664
   819
    apply (auto intro!: suminf_diff[symmetric] summable_ereal)
wenzelm@49664
   820
    done
hoelzl@41980
   821
qed
hoelzl@41980
   822
wenzelm@49664
   823
lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
hoelzl@41980
   824
proof -
hoelzl@43923
   825
  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)" by (rule suminf_upper) auto
hoelzl@41980
   826
  then show ?thesis by simp
hoelzl@41980
   827
qed
hoelzl@41980
   828
hoelzl@43920
   829
lemma summable_real_of_ereal:
hoelzl@43923
   830
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   831
  assumes f: "\<And>i. 0 \<le> f i"
wenzelm@49664
   832
    and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
hoelzl@41980
   833
  shows "summable (\<lambda>i. real (f i))"
hoelzl@41980
   834
proof (rule summable_def[THEN iffD2])
hoelzl@41980
   835
  have "0 \<le> (\<Sum>i. f i)" using assms by (auto intro: suminf_0_le)
hoelzl@43920
   836
  with fin obtain r where r: "ereal r = (\<Sum>i. f i)" by (cases "(\<Sum>i. f i)") auto
hoelzl@41980
   837
  { fix i have "f i \<noteq> \<infinity>" using f by (intro suminf_PInfty[OF _ fin]) auto
hoelzl@41980
   838
    then have "\<bar>f i\<bar> \<noteq> \<infinity>" using f[of i] by auto }
hoelzl@41980
   839
  note fin = this
hoelzl@43920
   840
  have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
hoelzl@43920
   841
    using f by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
hoelzl@43920
   842
  also have "\<dots> = ereal r" using fin r by (auto simp: ereal_real)
hoelzl@43920
   843
  finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" by (auto simp: sums_ereal)
hoelzl@41980
   844
qed
hoelzl@41980
   845
hoelzl@42950
   846
lemma suminf_SUP_eq:
hoelzl@43920
   847
  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
hoelzl@42950
   848
  assumes "\<And>i. incseq (\<lambda>n. f n i)" "\<And>n i. 0 \<le> f n i"
hoelzl@42950
   849
  shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
hoelzl@42950
   850
proof -
hoelzl@42950
   851
  { fix n :: nat
hoelzl@42950
   852
    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
hoelzl@43920
   853
      using assms by (auto intro!: SUPR_ereal_setsum[symmetric]) }
hoelzl@42950
   854
  note * = this
hoelzl@42950
   855
  show ?thesis using assms
hoelzl@43920
   856
    apply (subst (1 2) suminf_ereal_eq_SUPR)
hoelzl@42950
   857
    unfolding *
hoelzl@44928
   858
    apply (auto intro!: SUP_upper2)
wenzelm@49664
   859
    apply (subst SUP_commute)
wenzelm@49664
   860
    apply rule
wenzelm@49664
   861
    done
hoelzl@42950
   862
qed
hoelzl@42950
   863
hoelzl@47761
   864
lemma suminf_setsum_ereal:
hoelzl@47761
   865
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
hoelzl@47761
   866
  assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
hoelzl@47761
   867
  shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
hoelzl@47761
   868
proof cases
wenzelm@49664
   869
  assume "finite A"
wenzelm@49664
   870
  then show ?thesis using nonneg
hoelzl@47761
   871
    by induct (simp_all add: suminf_add_ereal setsum_nonneg)
hoelzl@47761
   872
qed simp
hoelzl@47761
   873
hoelzl@50104
   874
lemma suminf_ereal_eq_0:
hoelzl@50104
   875
  fixes f :: "nat \<Rightarrow> ereal"
hoelzl@50104
   876
  assumes nneg: "\<And>i. 0 \<le> f i"
hoelzl@50104
   877
  shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
hoelzl@50104
   878
proof
hoelzl@50104
   879
  assume "(\<Sum>i. f i) = 0"
hoelzl@50104
   880
  { fix i assume "f i \<noteq> 0"
hoelzl@50104
   881
    with nneg have "0 < f i" by (auto simp: less_le)
hoelzl@50104
   882
    also have "f i = (\<Sum>j. if j = i then f i else 0)"
hoelzl@50104
   883
      by (subst suminf_finite[where N="{i}"]) auto
hoelzl@50104
   884
    also have "\<dots> \<le> (\<Sum>i. f i)"
hoelzl@50104
   885
      using nneg by (auto intro!: suminf_le_pos)
hoelzl@50104
   886
    finally have False using `(\<Sum>i. f i) = 0` by auto }
hoelzl@50104
   887
  then show "\<forall>i. f i = 0" by auto
hoelzl@50104
   888
qed simp
hoelzl@50104
   889
hoelzl@51340
   890
lemma Liminf_within:
hoelzl@51340
   891
  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
hoelzl@51340
   892
  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
hoelzl@51340
   893
  unfolding Liminf_def eventually_within
hoelzl@51340
   894
proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
hoelzl@51340
   895
  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
hoelzl@51340
   896
  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
hoelzl@51340
   897
    by (auto simp: zero_less_dist_iff dist_commute)
hoelzl@51340
   898
  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
hoelzl@51340
   899
    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
hoelzl@51340
   900
next
hoelzl@51340
   901
  fix d :: real assume "0 < d"
hoelzl@51340
   902
  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
hoelzl@51340
   903
    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
hoelzl@51340
   904
    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
hoelzl@51340
   905
       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
hoelzl@51340
   906
qed
hoelzl@51340
   907
hoelzl@51340
   908
lemma Limsup_within:
hoelzl@51340
   909
  fixes f :: "'a::metric_space => 'b::complete_lattice"
hoelzl@51340
   910
  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
hoelzl@51340
   911
  unfolding Limsup_def eventually_within
hoelzl@51340
   912
proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
hoelzl@51340
   913
  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
hoelzl@51340
   914
  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
hoelzl@51340
   915
    by (auto simp: zero_less_dist_iff dist_commute)
hoelzl@51340
   916
  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
hoelzl@51340
   917
    by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
hoelzl@51340
   918
next
hoelzl@51340
   919
  fix d :: real assume "0 < d"
hoelzl@51340
   920
  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
hoelzl@51340
   921
    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
hoelzl@51340
   922
    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
hoelzl@51340
   923
       (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
hoelzl@51340
   924
qed
hoelzl@51340
   925
hoelzl@51340
   926
lemma Liminf_at:
hoelzl@51340
   927
  fixes f :: "'a::metric_space => _"
hoelzl@51340
   928
  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
hoelzl@51340
   929
  using Liminf_within[of x UNIV f] by simp
hoelzl@51340
   930
hoelzl@51340
   931
lemma Limsup_at:
hoelzl@51340
   932
  fixes f :: "'a::metric_space => _"
hoelzl@51340
   933
  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
hoelzl@51340
   934
  using Limsup_within[of x UNIV f] by simp
hoelzl@51340
   935
hoelzl@51340
   936
lemma min_Liminf_at:
hoelzl@51340
   937
  fixes f :: "'a::metric_space => 'b::complete_linorder"
hoelzl@51340
   938
  shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
hoelzl@51340
   939
  unfolding inf_min[symmetric] Liminf_at
hoelzl@51340
   940
  apply (subst inf_commute)
hoelzl@51340
   941
  apply (subst SUP_inf)
hoelzl@51340
   942
  apply (intro SUP_cong[OF refl])
hoelzl@51340
   943
  apply (cut_tac A="ball x b - {x}" and B="{x}" and M=f in INF_union)
hoelzl@51340
   944
  apply (simp add: INF_def del: inf_ereal_def)
hoelzl@51340
   945
  done
hoelzl@51340
   946
hoelzl@51340
   947
subsection {* monoset *}
hoelzl@51340
   948
hoelzl@51340
   949
definition (in order) mono_set:
hoelzl@51340
   950
  "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
hoelzl@51340
   951
hoelzl@51340
   952
lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
hoelzl@51340
   953
lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
hoelzl@51340
   954
lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
hoelzl@51340
   955
lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
hoelzl@51340
   956
hoelzl@51340
   957
lemma (in complete_linorder) mono_set_iff:
hoelzl@51340
   958
  fixes S :: "'a set"
hoelzl@51340
   959
  defines "a \<equiv> Inf S"
hoelzl@51340
   960
  shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
hoelzl@51340
   961
proof
hoelzl@51340
   962
  assume "mono_set S"
hoelzl@51340
   963
  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
hoelzl@51340
   964
  show ?c
hoelzl@51340
   965
  proof cases
hoelzl@51340
   966
    assume "a \<in> S"
hoelzl@51340
   967
    show ?c
hoelzl@51340
   968
      using mono[OF _ `a \<in> S`]
hoelzl@51340
   969
      by (auto intro: Inf_lower simp: a_def)
hoelzl@51340
   970
  next
hoelzl@51340
   971
    assume "a \<notin> S"
hoelzl@51340
   972
    have "S = {a <..}"
hoelzl@51340
   973
    proof safe
hoelzl@51340
   974
      fix x assume "x \<in> S"
hoelzl@51340
   975
      then have "a \<le> x" unfolding a_def by (rule Inf_lower)
hoelzl@51340
   976
      then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
hoelzl@51340
   977
    next
hoelzl@51340
   978
      fix x assume "a < x"
hoelzl@51340
   979
      then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
hoelzl@51340
   980
      with mono[of y x] show "x \<in> S" by auto
hoelzl@51340
   981
    qed
hoelzl@51340
   982
    then show ?c ..
hoelzl@51340
   983
  qed
hoelzl@51340
   984
qed auto
hoelzl@51340
   985
hoelzl@51340
   986
lemma ereal_open_mono_set:
hoelzl@51340
   987
  fixes S :: "ereal set"
hoelzl@51340
   988
  shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})"
hoelzl@51340
   989
  by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
hoelzl@51340
   990
    ereal_open_closed mono_set_iff open_ereal_greaterThan)
hoelzl@51340
   991
hoelzl@51340
   992
lemma ereal_closed_mono_set:
hoelzl@51340
   993
  fixes S :: "ereal set"
hoelzl@51340
   994
  shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
hoelzl@51340
   995
  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
hoelzl@51340
   996
    ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
hoelzl@51340
   997
hoelzl@51340
   998
lemma ereal_Liminf_Sup_monoset:
hoelzl@51340
   999
  fixes f :: "'a => ereal"
hoelzl@51340
  1000
  shows "Liminf net f =
hoelzl@51340
  1001
    Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
hoelzl@51340
  1002
    (is "_ = Sup ?A")
hoelzl@51340
  1003
proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
hoelzl@51340
  1004
  fix P assume P: "eventually P net"
hoelzl@51340
  1005
  fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
hoelzl@51340
  1006
  { fix x assume "P x"
hoelzl@51340
  1007
    then have "INFI (Collect P) f \<le> f x"
hoelzl@51340
  1008
      by (intro complete_lattice_class.INF_lower) simp
hoelzl@51340
  1009
    with S have "f x \<in> S"
hoelzl@51340
  1010
      by (simp add: mono_set) }
hoelzl@51340
  1011
  with P show "eventually (\<lambda>x. f x \<in> S) net"
hoelzl@51340
  1012
    by (auto elim: eventually_elim1)
hoelzl@51340
  1013
next
hoelzl@51340
  1014
  fix y l
hoelzl@51340
  1015
  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
hoelzl@51340
  1016
  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
hoelzl@51340
  1017
  show "l \<le> y"
hoelzl@51340
  1018
  proof (rule dense_le)
hoelzl@51340
  1019
    fix B assume "B < l"
hoelzl@51340
  1020
    then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
hoelzl@51340
  1021
      by (intro S[rule_format]) auto
hoelzl@51340
  1022
    then have "INFI {x. B < f x} f \<le> y"
hoelzl@51340
  1023
      using P by auto
hoelzl@51340
  1024
    moreover have "B \<le> INFI {x. B < f x} f"
hoelzl@51340
  1025
      by (intro INF_greatest) auto
hoelzl@51340
  1026
    ultimately show "B \<le> y"
hoelzl@51340
  1027
      by simp
hoelzl@51340
  1028
  qed
hoelzl@51340
  1029
qed
hoelzl@51340
  1030
hoelzl@51340
  1031
lemma ereal_Limsup_Inf_monoset:
hoelzl@51340
  1032
  fixes f :: "'a => ereal"
hoelzl@51340
  1033
  shows "Limsup net f =
hoelzl@51340
  1034
    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@51340
  1035
    (is "_ = Inf ?A")
hoelzl@51340
  1036
proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
hoelzl@51340
  1037
  fix P assume P: "eventually P net"
hoelzl@51340
  1038
  fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
hoelzl@51340
  1039
  { fix x assume "P x"
hoelzl@51340
  1040
    then have "f x \<le> SUPR (Collect P) f"
hoelzl@51340
  1041
      by (intro complete_lattice_class.SUP_upper) simp
hoelzl@51340
  1042
    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
hoelzl@51340
  1043
    have "f x \<in> S"
hoelzl@51340
  1044
      by (simp add: inj_image_mem_iff) }
hoelzl@51340
  1045
  with P show "eventually (\<lambda>x. f x \<in> S) net"
hoelzl@51340
  1046
    by (auto elim: eventually_elim1)
hoelzl@51340
  1047
next
hoelzl@51340
  1048
  fix y l
hoelzl@51340
  1049
  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
hoelzl@51340
  1050
  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
hoelzl@51340
  1051
  show "y \<le> l"
hoelzl@51340
  1052
  proof (rule dense_ge)
hoelzl@51340
  1053
    fix B assume "l < B"
hoelzl@51340
  1054
    then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
hoelzl@51340
  1055
      by (intro S[rule_format]) auto
hoelzl@51340
  1056
    then have "y \<le> SUPR {x. f x < B} f"
hoelzl@51340
  1057
      using P by auto
hoelzl@51340
  1058
    moreover have "SUPR {x. f x < B} f \<le> B"
hoelzl@51340
  1059
      by (intro SUP_least) auto
hoelzl@51340
  1060
    ultimately show "y \<le> B"
hoelzl@51340
  1061
      by simp
hoelzl@51340
  1062
  qed
hoelzl@51340
  1063
qed
hoelzl@51340
  1064
hoelzl@51340
  1065
lemma liminf_bounded_open:
hoelzl@51340
  1066
  fixes x :: "nat \<Rightarrow> ereal"
hoelzl@51340
  1067
  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@51340
  1068
  (is "_ \<longleftrightarrow> ?P x0")
hoelzl@51340
  1069
proof
hoelzl@51340
  1070
  assume "?P x0"
hoelzl@51340
  1071
  then show "x0 \<le> liminf x"
hoelzl@51340
  1072
    unfolding ereal_Liminf_Sup_monoset eventually_sequentially
hoelzl@51340
  1073
    by (intro complete_lattice_class.Sup_upper) auto
hoelzl@51340
  1074
next
hoelzl@51340
  1075
  assume "x0 \<le> liminf x"
hoelzl@51340
  1076
  { fix S :: "ereal set"
hoelzl@51340
  1077
    assume om: "open S & mono_set S & x0:S"
hoelzl@51340
  1078
    { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }
hoelzl@51340
  1079
    moreover
hoelzl@51340
  1080
    { assume "~(S=UNIV)"
hoelzl@51340
  1081
      then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
hoelzl@51340
  1082
      then have "B<x0" using om by auto
hoelzl@51340
  1083
      then have "EX N. ALL n>=N. x n : S"
hoelzl@51340
  1084
        unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
hoelzl@51340
  1085
    }
hoelzl@51340
  1086
    ultimately have "EX N. (ALL n>=N. x n : S)" by auto
hoelzl@51340
  1087
  }
hoelzl@51340
  1088
  then show "?P x0" by auto
hoelzl@51340
  1089
qed
hoelzl@51340
  1090
huffman@44125
  1091
end