src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
author haftmann
Sun Mar 16 18:09:04 2014 +0100 (2014-03-16)
changeset 56166 9a241bc276cd
parent 55522 23d2cbac6dce
child 56212 3253aaf73a01
permissions -rw-r--r--
normalising simp rules for compound operators
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:
wenzelm@53788
    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"
wenzelm@53788
    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"
wenzelm@53788
    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:
wenzelm@53788
    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)"
wenzelm@53788
    44
    using seq_monosub[of X]
wenzelm@53788
    45
    unfolding comp_def
wenzelm@53788
    46
    by auto
hoelzl@51351
    47
  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
    48
    by (auto simp add: monoseq_def)
wenzelm@53788
    49
  then obtain l where "(X \<circ> r) ----> l"
wenzelm@53788
    50
     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
wenzelm@53788
    51
     by auto
wenzelm@53788
    52
  then show ?thesis
wenzelm@53788
    53
    using `subseq r` by auto
hoelzl@51351
    54
qed
hoelzl@51351
    55
wenzelm@53788
    56
lemma compact_UNIV:
wenzelm@53788
    57
  "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)"
hoelzl@51351
    58
  using compact_complete_linorder
hoelzl@51351
    59
  by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def)
hoelzl@51351
    60
hoelzl@51351
    61
lemma compact_eq_closed:
wenzelm@53788
    62
  fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
hoelzl@51351
    63
  shows "compact S \<longleftrightarrow> closed S"
wenzelm@53788
    64
  using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed
wenzelm@53788
    65
  by auto
hoelzl@51351
    66
hoelzl@51351
    67
lemma closed_contains_Sup_cl:
wenzelm@53788
    68
  fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
wenzelm@53788
    69
  assumes "closed S"
wenzelm@53788
    70
    and "S \<noteq> {}"
wenzelm@53788
    71
  shows "Sup S \<in> S"
hoelzl@51351
    72
proof -
hoelzl@51351
    73
  from compact_eq_closed[of S] compact_attains_sup[of S] assms
wenzelm@53788
    74
  obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s"
wenzelm@53788
    75
    by auto
wenzelm@53374
    76
  then have "Sup S = s"
hoelzl@51351
    77
    by (auto intro!: Sup_eqI)
wenzelm@53374
    78
  with S show ?thesis
hoelzl@51351
    79
    by simp
hoelzl@51351
    80
qed
hoelzl@51351
    81
hoelzl@51351
    82
lemma closed_contains_Inf_cl:
wenzelm@53788
    83
  fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
wenzelm@53788
    84
  assumes "closed S"
wenzelm@53788
    85
    and "S \<noteq> {}"
wenzelm@53788
    86
  shows "Inf S \<in> S"
hoelzl@51351
    87
proof -
hoelzl@51351
    88
  from compact_eq_closed[of S] compact_attains_inf[of S] assms
wenzelm@53788
    89
  obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t"
wenzelm@53788
    90
    by auto
wenzelm@53374
    91
  then have "Inf S = s"
hoelzl@51351
    92
    by (auto intro!: Inf_eqI)
wenzelm@53374
    93
  with S show ?thesis
hoelzl@51351
    94
    by simp
hoelzl@51351
    95
qed
hoelzl@51351
    96
wenzelm@53788
    97
lemma ereal_dense3:
wenzelm@53788
    98
  fixes x y :: ereal
wenzelm@53788
    99
  shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
hoelzl@51351
   100
proof (cases x y rule: ereal2_cases, simp_all)
wenzelm@53788
   101
  fix r q :: real
wenzelm@53788
   102
  assume "r < q"
wenzelm@53788
   103
  from Rats_dense_in_real[OF this] show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
hoelzl@51351
   104
    by (fastforce simp: Rats_def)
hoelzl@51351
   105
next
wenzelm@53788
   106
  fix r :: real
wenzelm@53788
   107
  show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
hoelzl@51351
   108
    using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
hoelzl@51351
   109
    by (auto simp: Rats_def)
hoelzl@51351
   110
qed
hoelzl@51351
   111
hoelzl@51351
   112
instance ereal :: second_countable_topology
hoelzl@51351
   113
proof (default, intro exI conjI)
hoelzl@51351
   114
  let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
wenzelm@53788
   115
  show "countable ?B"
wenzelm@53788
   116
    by (auto intro: countable_rat)
hoelzl@51351
   117
  show "open = generate_topology ?B"
hoelzl@51351
   118
  proof (intro ext iffI)
wenzelm@53788
   119
    fix S :: "ereal set"
wenzelm@53788
   120
    assume "open S"
hoelzl@51351
   121
    then show "generate_topology ?B S"
hoelzl@51351
   122
      unfolding open_generated_order
hoelzl@51351
   123
    proof induct
hoelzl@51351
   124
      case (Basis b)
wenzelm@53788
   125
      then obtain e where "b = {..<e} \<or> b = {e<..}"
wenzelm@53788
   126
        by auto
hoelzl@51351
   127
      moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}"
hoelzl@51351
   128
        by (auto dest: ereal_dense3
hoelzl@51351
   129
                 simp del: ex_simps
hoelzl@51351
   130
                 simp add: ex_simps[symmetric] conj_commute Rats_def image_iff)
hoelzl@51351
   131
      ultimately show ?case
hoelzl@51351
   132
        by (auto intro: generate_topology.intros)
hoelzl@51351
   133
    qed (auto intro: generate_topology.intros)
hoelzl@51351
   134
  next
wenzelm@53788
   135
    fix S
wenzelm@53788
   136
    assume "generate_topology ?B S"
wenzelm@53788
   137
    then show "open S"
wenzelm@53788
   138
      by induct auto
hoelzl@51351
   139
  qed
hoelzl@51351
   140
qed
hoelzl@51351
   141
hoelzl@43920
   142
lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
wenzelm@53788
   143
  unfolding continuous_on_topological open_ereal_def
wenzelm@53788
   144
  by auto
hoelzl@41980
   145
hoelzl@43920
   146
lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal"
wenzelm@53788
   147
  using continuous_on_eq_continuous_at[of UNIV]
wenzelm@53788
   148
  by auto
hoelzl@41980
   149
hoelzl@43920
   150
lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
wenzelm@53788
   151
  using continuous_on_eq_continuous_within[of A]
wenzelm@53788
   152
  by auto
hoelzl@41980
   153
hoelzl@43920
   154
lemma ereal_open_uminus:
hoelzl@43920
   155
  fixes S :: "ereal set"
wenzelm@53788
   156
  assumes "open S"
wenzelm@53788
   157
  shows "open (uminus ` S)"
hoelzl@51340
   158
  using `open S`[unfolded open_generated_order]
hoelzl@51340
   159
proof induct
hoelzl@51340
   160
  have "range uminus = (UNIV :: ereal set)"
hoelzl@51340
   161
    by (auto simp: image_iff ereal_uminus_eq_reorder)
wenzelm@53788
   162
  then show "open (range uminus :: ereal set)"
wenzelm@53788
   163
    by simp
hoelzl@51340
   164
qed (auto simp add: image_Union image_Int)
hoelzl@41980
   165
hoelzl@43920
   166
lemma ereal_uminus_complement:
hoelzl@43920
   167
  fixes S :: "ereal set"
hoelzl@41980
   168
  shows "uminus ` (- S) = - uminus ` S"
hoelzl@41980
   169
  by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
hoelzl@41980
   170
hoelzl@43920
   171
lemma ereal_closed_uminus:
hoelzl@43920
   172
  fixes S :: "ereal set"
hoelzl@41980
   173
  assumes "closed S"
hoelzl@41980
   174
  shows "closed (uminus ` S)"
wenzelm@53788
   175
  using assms
wenzelm@53788
   176
  unfolding closed_def ereal_uminus_complement[symmetric]
wenzelm@53788
   177
  by (rule ereal_open_uminus)
hoelzl@41980
   178
hoelzl@43920
   179
lemma ereal_open_closed_aux:
hoelzl@43920
   180
  fixes S :: "ereal set"
wenzelm@53788
   181
  assumes "open S"
wenzelm@53788
   182
    and "closed S"
wenzelm@53788
   183
    and S: "(-\<infinity>) \<notin> S"
hoelzl@41980
   184
  shows "S = {}"
wenzelm@49664
   185
proof (rule ccontr)
wenzelm@53788
   186
  assume "\<not> ?thesis"
wenzelm@53788
   187
  then have *: "Inf S \<in> S"
wenzelm@53788
   188
    by (metis assms(2) closed_contains_Inf_cl)
wenzelm@53788
   189
  {
wenzelm@53788
   190
    assume "Inf S = -\<infinity>"
wenzelm@53788
   191
    then have False
wenzelm@53788
   192
      using * assms(3) by auto
wenzelm@53788
   193
  }
hoelzl@41980
   194
  moreover
wenzelm@53788
   195
  {
wenzelm@53788
   196
    assume "Inf S = \<infinity>"
wenzelm@53788
   197
    then have "S = {\<infinity>}"
wenzelm@53788
   198
      by (metis Inf_eq_PInfty `S \<noteq> {}`)
wenzelm@53788
   199
    then have False
wenzelm@53788
   200
      by (metis assms(1) not_open_singleton)
wenzelm@53788
   201
  }
hoelzl@41980
   202
  moreover
wenzelm@53788
   203
  {
wenzelm@53788
   204
    assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
wenzelm@53788
   205
    from ereal_open_cont_interval[OF assms(1) * fin]
wenzelm@53788
   206
    obtain e where e: "e > 0" "{Inf S - e<..<Inf S + e} \<subseteq> S" .
wenzelm@53788
   207
    then obtain b where b: "Inf S - e < b" "b < Inf S"
wenzelm@53788
   208
      using fin ereal_between[of "Inf S" e] dense[of "Inf S - e"]
noschinl@44918
   209
      by auto
wenzelm@53788
   210
    then have "b: {Inf S - e <..< Inf S + e}"
wenzelm@53788
   211
      using e fin ereal_between[of "Inf S" e]
wenzelm@53788
   212
      by auto
wenzelm@53788
   213
    then have "b \<in> S"
wenzelm@53788
   214
      using e by auto
wenzelm@53788
   215
    then have False
wenzelm@53788
   216
      using b by (metis complete_lattice_class.Inf_lower leD)
wenzelm@53788
   217
  }
wenzelm@53788
   218
  ultimately show False
wenzelm@53788
   219
    by auto
hoelzl@41980
   220
qed
hoelzl@41980
   221
hoelzl@43920
   222
lemma ereal_open_closed:
hoelzl@43920
   223
  fixes S :: "ereal set"
wenzelm@53788
   224
  shows "open S \<and> closed S \<longleftrightarrow> S = {} \<or> S = UNIV"
wenzelm@49664
   225
proof -
wenzelm@53788
   226
  {
wenzelm@53788
   227
    assume lhs: "open S \<and> closed S"
wenzelm@53788
   228
    {
wenzelm@53788
   229
      assume "-\<infinity> \<notin> S"
wenzelm@53788
   230
      then have "S = {}"
wenzelm@53788
   231
        using lhs ereal_open_closed_aux by auto
wenzelm@53788
   232
    }
wenzelm@49664
   233
    moreover
wenzelm@53788
   234
    {
wenzelm@53788
   235
      assume "-\<infinity> \<in> S"
wenzelm@53788
   236
      then have "- S = {}"
wenzelm@53788
   237
        using lhs ereal_open_closed_aux[of "-S"] by auto
wenzelm@53788
   238
    }
wenzelm@53788
   239
    ultimately have "S = {} \<or> S = UNIV"
wenzelm@53788
   240
      by auto
wenzelm@53788
   241
  }
wenzelm@53788
   242
  then show ?thesis
wenzelm@53788
   243
    by auto
hoelzl@41980
   244
qed
hoelzl@41980
   245
hoelzl@43920
   246
lemma ereal_open_affinity_pos:
hoelzl@43923
   247
  fixes S :: "ereal set"
wenzelm@53788
   248
  assumes "open S"
wenzelm@53788
   249
    and m: "m \<noteq> \<infinity>" "0 < m"
wenzelm@53788
   250
    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
hoelzl@41980
   251
  shows "open ((\<lambda>x. m * x + t) ` S)"
hoelzl@41980
   252
proof -
wenzelm@53788
   253
  obtain r where r[simp]: "m = ereal r"
wenzelm@53788
   254
    using m by (cases m) auto
wenzelm@53788
   255
  obtain p where p[simp]: "t = ereal p"
wenzelm@53788
   256
    using t by auto
wenzelm@53788
   257
  have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0"
wenzelm@53788
   258
    using m by auto
wenzelm@55522
   259
  from `open S` [THEN ereal_openE]
wenzelm@55522
   260
  obtain l u where T:
wenzelm@55522
   261
      "open (ereal -` S)"
wenzelm@55522
   262
      "\<infinity> \<in> S \<Longrightarrow> {ereal l<..} \<subseteq> S"
wenzelm@55522
   263
      "- \<infinity> \<in> S \<Longrightarrow> {..<ereal u} \<subseteq> S"
wenzelm@55522
   264
    by blast
hoelzl@41980
   265
  let ?f = "(\<lambda>x. m * x + t)"
wenzelm@49664
   266
  show ?thesis
wenzelm@49664
   267
    unfolding open_ereal_def
hoelzl@41980
   268
  proof (intro conjI impI exI subsetI)
hoelzl@43920
   269
    have "ereal -` ?f ` S = (\<lambda>x. r * x + p) ` (ereal -` S)"
hoelzl@41980
   270
    proof safe
wenzelm@49664
   271
      fix x y
wenzelm@49664
   272
      assume "ereal y = m * x + t" "x \<in> S"
hoelzl@43920
   273
      then show "y \<in> (\<lambda>x. r * x + p) ` ereal -` S"
hoelzl@41980
   274
        using `r \<noteq> 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm)
hoelzl@41980
   275
    qed force
hoelzl@43920
   276
    then show "open (ereal -` ?f ` S)"
wenzelm@53788
   277
      using open_affinity[OF T(1) `r \<noteq> 0`]
wenzelm@53788
   278
      by (auto simp: ac_simps)
hoelzl@41980
   279
  next
wenzelm@49664
   280
    assume "\<infinity> \<in> ?f`S"
wenzelm@53788
   281
    with `0 < r` have "\<infinity> \<in> S"
wenzelm@53788
   282
      by auto
wenzelm@49664
   283
    fix x
wenzelm@49664
   284
    assume "x \<in> {ereal (r * l + p)<..}"
wenzelm@53788
   285
    then have [simp]: "ereal (r * l + p) < x"
wenzelm@53788
   286
      by auto
hoelzl@41980
   287
    show "x \<in> ?f`S"
hoelzl@41980
   288
    proof (rule image_eqI)
hoelzl@41980
   289
      show "x = m * ((x - t) / m) + t"
wenzelm@53788
   290
        using m t
wenzelm@53788
   291
        by (cases rule: ereal3_cases[of m x t]) auto
wenzelm@53788
   292
      have "ereal l < (x - t) / m"
wenzelm@53788
   293
        using m t
wenzelm@53788
   294
        by (simp add: ereal_less_divide_pos ereal_less_minus)
wenzelm@53788
   295
      then show "(x - t) / m \<in> S"
wenzelm@53788
   296
        using T(2)[OF `\<infinity> \<in> S`] by auto
hoelzl@41980
   297
    qed
hoelzl@41980
   298
  next
wenzelm@53788
   299
    assume "-\<infinity> \<in> ?f ` S"
wenzelm@53788
   300
    with `0 < r` have "-\<infinity> \<in> S"
wenzelm@53788
   301
      by auto
hoelzl@43920
   302
    fix x assume "x \<in> {..<ereal (r * u + p)}"
wenzelm@53788
   303
    then have [simp]: "x < ereal (r * u + p)"
wenzelm@53788
   304
      by auto
hoelzl@41980
   305
    show "x \<in> ?f`S"
hoelzl@41980
   306
    proof (rule image_eqI)
hoelzl@41980
   307
      show "x = m * ((x - t) / m) + t"
wenzelm@53788
   308
        using m t
wenzelm@53788
   309
        by (cases rule: ereal3_cases[of m x t]) auto
hoelzl@43920
   310
      have "(x - t)/m < ereal u"
wenzelm@53788
   311
        using m t
wenzelm@53788
   312
        by (simp add: ereal_divide_less_pos ereal_minus_less)
wenzelm@53788
   313
      then show "(x - t)/m \<in> S"
wenzelm@53788
   314
        using T(3)[OF `-\<infinity> \<in> S`]
wenzelm@53788
   315
        by auto
hoelzl@41980
   316
    qed
hoelzl@41980
   317
  qed
hoelzl@41980
   318
qed
hoelzl@41980
   319
hoelzl@43920
   320
lemma ereal_open_affinity:
hoelzl@43923
   321
  fixes S :: "ereal set"
wenzelm@49664
   322
  assumes "open S"
wenzelm@49664
   323
    and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0"
wenzelm@49664
   324
    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
hoelzl@41980
   325
  shows "open ((\<lambda>x. m * x + t) ` S)"
hoelzl@41980
   326
proof cases
wenzelm@49664
   327
  assume "0 < m"
wenzelm@49664
   328
  then show ?thesis
wenzelm@53788
   329
    using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m
wenzelm@53788
   330
    by auto
hoelzl@41980
   331
next
hoelzl@41980
   332
  assume "\<not> 0 < m" then
wenzelm@53788
   333
  have "0 < -m"
wenzelm@53788
   334
    using `m \<noteq> 0`
wenzelm@53788
   335
    by (cases m) auto
wenzelm@53788
   336
  then have m: "-m \<noteq> \<infinity>" "0 < -m"
wenzelm@53788
   337
    using `\<bar>m\<bar> \<noteq> \<infinity>`
hoelzl@43920
   338
    by (auto simp: ereal_uminus_eq_reorder)
wenzelm@53788
   339
  from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t] show ?thesis
wenzelm@53788
   340
    unfolding image_image by simp
hoelzl@41980
   341
qed
hoelzl@41980
   342
hoelzl@43920
   343
lemma ereal_lim_mult:
hoelzl@43920
   344
  fixes X :: "'a \<Rightarrow> ereal"
wenzelm@49664
   345
  assumes lim: "(X ---> L) net"
wenzelm@49664
   346
    and a: "\<bar>a\<bar> \<noteq> \<infinity>"
hoelzl@41980
   347
  shows "((\<lambda>i. a * X i) ---> a * L) net"
hoelzl@41980
   348
proof cases
hoelzl@41980
   349
  assume "a \<noteq> 0"
hoelzl@41980
   350
  show ?thesis
hoelzl@41980
   351
  proof (rule topological_tendstoI)
wenzelm@49664
   352
    fix S
wenzelm@53788
   353
    assume "open S" and "a * L \<in> S"
hoelzl@41980
   354
    have "a * L / a = L"
wenzelm@53788
   355
      using `a \<noteq> 0` a
wenzelm@53788
   356
      by (cases rule: ereal2_cases[of a L]) auto
hoelzl@41980
   357
    then have L: "L \<in> ((\<lambda>x. x / a) ` S)"
wenzelm@53788
   358
      using `a * L \<in> S`
wenzelm@53788
   359
      by (force simp: image_iff)
hoelzl@41980
   360
    moreover have "open ((\<lambda>x. x / a) ` S)"
hoelzl@43920
   361
      using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a
hoelzl@43920
   362
      by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps)
hoelzl@41980
   363
    note * = lim[THEN topological_tendstoD, OF this L]
wenzelm@53788
   364
    {
wenzelm@53788
   365
      fix x
wenzelm@49664
   366
      from a `a \<noteq> 0` have "a * (x / a) = x"
wenzelm@53788
   367
        by (cases rule: ereal2_cases[of a x]) auto
wenzelm@53788
   368
    }
hoelzl@41980
   369
    note this[simp]
hoelzl@41980
   370
    show "eventually (\<lambda>x. a * X x \<in> S) net"
hoelzl@41980
   371
      by (rule eventually_mono[OF _ *]) auto
hoelzl@41980
   372
  qed
noschinl@44918
   373
qed auto
hoelzl@41980
   374
hoelzl@43920
   375
lemma ereal_lim_uminus:
wenzelm@49664
   376
  fixes X :: "'a \<Rightarrow> ereal"
wenzelm@53788
   377
  shows "((\<lambda>i. - X i) ---> - L) net \<longleftrightarrow> (X ---> L) net"
hoelzl@43920
   378
  using ereal_lim_mult[of X L net "ereal (-1)"]
wenzelm@49664
   379
    ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"]
hoelzl@41980
   380
  by (auto simp add: algebra_simps)
hoelzl@41980
   381
wenzelm@53788
   382
lemma ereal_open_atLeast:
wenzelm@53788
   383
  fixes x :: ereal
wenzelm@53788
   384
  shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
hoelzl@41980
   385
proof
wenzelm@53788
   386
  assume "x = -\<infinity>"
wenzelm@53788
   387
  then have "{x..} = UNIV"
wenzelm@53788
   388
    by auto
wenzelm@53788
   389
  then show "open {x..}"
wenzelm@53788
   390
    by auto
hoelzl@41980
   391
next
hoelzl@41980
   392
  assume "open {x..}"
wenzelm@53788
   393
  then have "open {x..} \<and> closed {x..}"
wenzelm@53788
   394
    by auto
wenzelm@53788
   395
  then have "{x..} = UNIV"
wenzelm@53788
   396
    unfolding ereal_open_closed by auto
wenzelm@53788
   397
  then show "x = -\<infinity>"
wenzelm@53788
   398
    by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
hoelzl@41980
   399
qed
hoelzl@41980
   400
wenzelm@53788
   401
lemma open_uminus_iff:
wenzelm@53788
   402
  fixes S :: "ereal set"
wenzelm@53788
   403
  shows "open (uminus ` S) \<longleftrightarrow> open S"
wenzelm@53788
   404
  using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"]
wenzelm@53788
   405
  by auto
hoelzl@41980
   406
hoelzl@43920
   407
lemma ereal_Liminf_uminus:
wenzelm@53788
   408
  fixes f :: "'a \<Rightarrow> ereal"
wenzelm@53788
   409
  shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
hoelzl@43920
   410
  using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
hoelzl@41980
   411
hoelzl@43920
   412
lemma ereal_Lim_uminus:
wenzelm@49664
   413
  fixes f :: "'a \<Rightarrow> ereal"
wenzelm@49664
   414
  shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net"
hoelzl@41980
   415
  using
hoelzl@43920
   416
    ereal_lim_mult[of f f0 net "- 1"]
hoelzl@43920
   417
    ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
hoelzl@43920
   418
  by (auto simp: ereal_uminus_reorder)
hoelzl@41980
   419
hoelzl@41980
   420
lemma Liminf_PInfty:
hoelzl@43920
   421
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@41980
   422
  assumes "\<not> trivial_limit net"
hoelzl@41980
   423
  shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
wenzelm@53788
   424
  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
wenzelm@53788
   425
  using Liminf_le_Limsup[OF assms, of f]
wenzelm@53788
   426
  by auto
hoelzl@41980
   427
hoelzl@41980
   428
lemma Limsup_MInfty:
hoelzl@43920
   429
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@41980
   430
  assumes "\<not> trivial_limit net"
hoelzl@41980
   431
  shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
wenzelm@53788
   432
  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
wenzelm@53788
   433
  using Liminf_le_Limsup[OF assms, of f]
wenzelm@53788
   434
  by auto
hoelzl@41980
   435
hoelzl@50104
   436
lemma convergent_ereal:
wenzelm@53788
   437
  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
hoelzl@50104
   438
  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
hoelzl@51340
   439
  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
hoelzl@50104
   440
  by (auto simp: convergent_def)
hoelzl@50104
   441
hoelzl@41980
   442
lemma liminf_PInfty:
hoelzl@51351
   443
  fixes X :: "nat \<Rightarrow> ereal"
hoelzl@51351
   444
  shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
wenzelm@49664
   445
  by (metis Liminf_PInfty trivial_limit_sequentially)
hoelzl@41980
   446
hoelzl@41980
   447
lemma limsup_MInfty:
hoelzl@51351
   448
  fixes X :: "nat \<Rightarrow> ereal"
hoelzl@51351
   449
  shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
wenzelm@49664
   450
  by (metis Limsup_MInfty trivial_limit_sequentially)
hoelzl@41980
   451
hoelzl@43920
   452
lemma ereal_lim_mono:
wenzelm@53788
   453
  fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
wenzelm@53788
   454
  assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
wenzelm@53788
   455
    and "X ----> x"
wenzelm@53788
   456
    and "Y ----> y"
wenzelm@53788
   457
  shows "x \<le> y"
hoelzl@51000
   458
  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
hoelzl@41980
   459
hoelzl@43920
   460
lemma incseq_le_ereal:
hoelzl@51351
   461
  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
wenzelm@53788
   462
  assumes inc: "incseq X"
wenzelm@53788
   463
    and lim: "X ----> L"
hoelzl@41980
   464
  shows "X N \<le> L"
wenzelm@53788
   465
  using inc
wenzelm@53788
   466
  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
hoelzl@41980
   467
wenzelm@49664
   468
lemma decseq_ge_ereal:
wenzelm@49664
   469
  assumes dec: "decseq X"
hoelzl@51351
   470
    and lim: "X ----> (L::'a::linorder_topology)"
wenzelm@53788
   471
  shows "X N \<ge> L"
wenzelm@49664
   472
  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
hoelzl@41980
   473
hoelzl@41980
   474
lemma bounded_abs:
wenzelm@53788
   475
  fixes a :: real
wenzelm@53788
   476
  assumes "a \<le> x"
wenzelm@53788
   477
    and "x \<le> b"
wenzelm@53788
   478
  shows "abs x \<le> max (abs a) (abs b)"
wenzelm@49664
   479
  by (metis abs_less_iff assms leI le_max_iff_disj
wenzelm@49664
   480
    less_eq_real_def less_le_not_le less_minus_iff minus_minus)
hoelzl@41980
   481
hoelzl@43920
   482
lemma ereal_Sup_lim:
wenzelm@53788
   483
  fixes a :: "'a::{complete_linorder,linorder_topology}"
wenzelm@53788
   484
  assumes "\<And>n. b n \<in> s"
wenzelm@53788
   485
    and "b ----> a"
hoelzl@41980
   486
  shows "a \<le> Sup s"
wenzelm@49664
   487
  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
hoelzl@41980
   488
hoelzl@43920
   489
lemma ereal_Inf_lim:
wenzelm@53788
   490
  fixes a :: "'a::{complete_linorder,linorder_topology}"
wenzelm@53788
   491
  assumes "\<And>n. b n \<in> s"
wenzelm@53788
   492
    and "b ----> a"
hoelzl@41980
   493
  shows "Inf s \<le> a"
wenzelm@49664
   494
  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
hoelzl@41980
   495
hoelzl@43920
   496
lemma SUP_Lim_ereal:
wenzelm@53788
   497
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
wenzelm@53788
   498
  assumes inc: "incseq X"
wenzelm@53788
   499
    and l: "X ----> l"
wenzelm@53788
   500
  shows "(SUP n. X n) = l"
wenzelm@53788
   501
  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
wenzelm@53788
   502
  by simp
hoelzl@41980
   503
hoelzl@51351
   504
lemma INF_Lim_ereal:
wenzelm@53788
   505
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
wenzelm@53788
   506
  assumes dec: "decseq X"
wenzelm@53788
   507
    and l: "X ----> l"
wenzelm@53788
   508
  shows "(INF n. X n) = l"
wenzelm@53788
   509
  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
wenzelm@53788
   510
  by simp
hoelzl@41980
   511
hoelzl@41980
   512
lemma SUP_eq_LIMSEQ:
hoelzl@41980
   513
  assumes "mono f"
hoelzl@43920
   514
  shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
hoelzl@41980
   515
proof
hoelzl@43920
   516
  have inc: "incseq (\<lambda>i. ereal (f i))"
hoelzl@41980
   517
    using `mono f` unfolding mono_def incseq_def by auto
wenzelm@53788
   518
  {
wenzelm@53788
   519
    assume "f ----> x"
wenzelm@53788
   520
    then have "(\<lambda>i. ereal (f i)) ----> ereal x"
wenzelm@53788
   521
      by auto
wenzelm@53788
   522
    from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
wenzelm@53788
   523
  next
wenzelm@53788
   524
    assume "(SUP n. ereal (f n)) = ereal x"
wenzelm@53788
   525
    with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
wenzelm@53788
   526
  }
hoelzl@41980
   527
qed
hoelzl@41980
   528
hoelzl@43920
   529
lemma liminf_ereal_cminus:
wenzelm@49664
   530
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   531
  assumes "c \<noteq> -\<infinity>"
hoelzl@42950
   532
  shows "liminf (\<lambda>x. c - f x) = c - limsup f"
hoelzl@42950
   533
proof (cases c)
wenzelm@49664
   534
  case PInf
wenzelm@53788
   535
  then show ?thesis
wenzelm@53788
   536
    by (simp add: Liminf_const)
hoelzl@42950
   537
next
wenzelm@49664
   538
  case (real r)
wenzelm@49664
   539
  then show ?thesis
hoelzl@42950
   540
    unfolding liminf_SUPR_INFI limsup_INFI_SUPR
hoelzl@43920
   541
    apply (subst INFI_ereal_cminus)
hoelzl@42950
   542
    apply auto
hoelzl@43920
   543
    apply (subst SUPR_ereal_cminus)
hoelzl@42950
   544
    apply auto
hoelzl@42950
   545
    done
hoelzl@42950
   546
qed (insert `c \<noteq> -\<infinity>`, simp)
hoelzl@42950
   547
wenzelm@49664
   548
hoelzl@41980
   549
subsubsection {* Continuity *}
hoelzl@41980
   550
hoelzl@43920
   551
lemma continuous_at_of_ereal:
hoelzl@43920
   552
  fixes x0 :: ereal
hoelzl@41980
   553
  assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
hoelzl@41980
   554
  shows "continuous (at x0) real"
wenzelm@49664
   555
proof -
wenzelm@53788
   556
  {
wenzelm@53788
   557
    fix T
wenzelm@53788
   558
    assume T: "open T" "real x0 \<in> T"
wenzelm@53788
   559
    def S \<equiv> "ereal ` T"
wenzelm@53788
   560
    then have "ereal (real x0) \<in> S"
wenzelm@53788
   561
      using T by auto
wenzelm@53788
   562
    then have "x0 \<in> S"
wenzelm@53788
   563
      using assms ereal_real by auto
wenzelm@53788
   564
    moreover have "open S"
wenzelm@53788
   565
      using open_ereal S_def T by auto
wenzelm@53788
   566
    moreover have "\<forall>y\<in>S. real y \<in> T"
wenzelm@53788
   567
      using S_def T by auto
wenzelm@53788
   568
    ultimately have "\<exists>S. x0 \<in> S \<and> open S \<and> (\<forall>y\<in>S. real y \<in> T)"
wenzelm@53788
   569
      by auto
wenzelm@49664
   570
  }
wenzelm@53788
   571
  then show ?thesis
wenzelm@53788
   572
    unfolding continuous_at_open by blast
hoelzl@41980
   573
qed
hoelzl@41980
   574
hoelzl@43920
   575
lemma continuous_at_iff_ereal:
wenzelm@53788
   576
  fixes f :: "'a::t2_space \<Rightarrow> real"
wenzelm@53788
   577
  shows "continuous (at x0) f \<longleftrightarrow> continuous (at x0) (ereal \<circ> f)"
wenzelm@49664
   578
proof -
wenzelm@53788
   579
  {
wenzelm@53788
   580
    assume "continuous (at x0) f"
wenzelm@53788
   581
    then have "continuous (at x0) (ereal \<circ> f)"
wenzelm@53788
   582
      using continuous_at_ereal continuous_at_compose[of x0 f ereal]
wenzelm@53788
   583
      by auto
wenzelm@49664
   584
  }
wenzelm@49664
   585
  moreover
wenzelm@53788
   586
  {
wenzelm@53788
   587
    assume "continuous (at x0) (ereal \<circ> f)"
wenzelm@53788
   588
    then have "continuous (at x0) (real \<circ> (ereal \<circ> f))"
wenzelm@53788
   589
      using continuous_at_of_ereal
wenzelm@53788
   590
      by (intro continuous_at_compose[of x0 "ereal \<circ> f"]) auto
wenzelm@53788
   591
    moreover have "real \<circ> (ereal \<circ> f) = f"
wenzelm@53788
   592
      using real_ereal_id by (simp add: o_assoc)
wenzelm@53788
   593
    ultimately have "continuous (at x0) f"
wenzelm@53788
   594
      by auto
wenzelm@53788
   595
  }
wenzelm@53788
   596
  ultimately show ?thesis
wenzelm@53788
   597
    by auto
hoelzl@41980
   598
qed
hoelzl@41980
   599
hoelzl@41980
   600
hoelzl@43920
   601
lemma continuous_on_iff_ereal:
wenzelm@49664
   602
  fixes f :: "'a::t2_space => real"
wenzelm@53788
   603
  assumes "open A"
wenzelm@53788
   604
  shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)"
wenzelm@53788
   605
  using continuous_at_iff_ereal assms
wenzelm@53788
   606
  by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong)
hoelzl@41980
   607
wenzelm@53788
   608
lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real"
wenzelm@53788
   609
  using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
wenzelm@53788
   610
  by auto
hoelzl@41980
   611
hoelzl@41980
   612
lemma continuous_on_iff_real:
wenzelm@53788
   613
  fixes f :: "'a::t2_space \<Rightarrow> ereal"
hoelzl@41980
   614
  assumes "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
hoelzl@41980
   615
  shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
wenzelm@49664
   616
proof -
wenzelm@53788
   617
  have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
wenzelm@53788
   618
    using assms by force
wenzelm@49664
   619
  then have *: "continuous_on (f ` A) real"
wenzelm@49664
   620
    using continuous_on_real by (simp add: continuous_on_subset)
wenzelm@53788
   621
  have **: "continuous_on ((real \<circ> f) ` A) ereal"
wenzelm@53788
   622
    using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real \<circ> f) ` A"]
wenzelm@53788
   623
    by blast
wenzelm@53788
   624
  {
wenzelm@53788
   625
    assume "continuous_on A f"
wenzelm@53788
   626
    then have "continuous_on A (real \<circ> f)"
wenzelm@49664
   627
      apply (subst continuous_on_compose)
wenzelm@53788
   628
      using *
wenzelm@53788
   629
      apply auto
wenzelm@49664
   630
      done
wenzelm@49664
   631
  }
wenzelm@49664
   632
  moreover
wenzelm@53788
   633
  {
wenzelm@53788
   634
    assume "continuous_on A (real \<circ> f)"
wenzelm@53788
   635
    then have "continuous_on A (ereal \<circ> (real \<circ> f))"
wenzelm@49664
   636
      apply (subst continuous_on_compose)
wenzelm@53788
   637
      using **
wenzelm@53788
   638
      apply auto
wenzelm@49664
   639
      done
wenzelm@49664
   640
    then have "continuous_on A f"
wenzelm@53788
   641
      apply (subst continuous_on_eq[of A "ereal \<circ> (real \<circ> f)" f])
wenzelm@53788
   642
      using assms ereal_real
wenzelm@53788
   643
      apply auto
wenzelm@49664
   644
      done
wenzelm@49664
   645
  }
wenzelm@53788
   646
  ultimately show ?thesis
wenzelm@53788
   647
    by auto
hoelzl@41980
   648
qed
hoelzl@41980
   649
hoelzl@41980
   650
lemma continuous_at_const:
wenzelm@53788
   651
  fixes f :: "'a::t2_space \<Rightarrow> ereal"
wenzelm@53788
   652
  assumes "\<forall>x. f x = C"
wenzelm@53788
   653
  shows "\<forall>x. continuous (at x) f"
wenzelm@53788
   654
  unfolding continuous_at_open
wenzelm@53788
   655
  using assms t1_space
wenzelm@53788
   656
  by auto
hoelzl@41980
   657
hoelzl@41980
   658
lemma mono_closed_real:
hoelzl@41980
   659
  fixes S :: "real set"
wenzelm@53788
   660
  assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
wenzelm@49664
   661
    and "closed S"
wenzelm@53788
   662
  shows "S = {} \<or> S = UNIV \<or> (\<exists>a. S = {a..})"
wenzelm@49664
   663
proof -
wenzelm@53788
   664
  {
wenzelm@53788
   665
    assume "S \<noteq> {}"
wenzelm@53788
   666
    { assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x"
wenzelm@53788
   667
      then have *: "\<forall>x\<in>S. Inf S \<le> x"
hoelzl@54258
   668
        using cInf_lower[of _ S] ex by (metis bdd_below_def)
wenzelm@53788
   669
      then have "Inf S \<in> S"
wenzelm@53788
   670
        apply (subst closed_contains_Inf)
wenzelm@53788
   671
        using ex `S \<noteq> {}` `closed S`
wenzelm@53788
   672
        apply auto
wenzelm@53788
   673
        done
wenzelm@53788
   674
      then have "\<forall>x. Inf S \<le> x \<longleftrightarrow> x \<in> S"
wenzelm@53788
   675
        using mono[rule_format, of "Inf S"] *
wenzelm@53788
   676
        by auto
wenzelm@53788
   677
      then have "S = {Inf S ..}"
wenzelm@53788
   678
        by auto
wenzelm@53788
   679
      then have "\<exists>a. S = {a ..}"
wenzelm@53788
   680
        by auto
wenzelm@49664
   681
    }
wenzelm@49664
   682
    moreover
wenzelm@53788
   683
    {
wenzelm@53788
   684
      assume "\<not> (\<exists>B. \<forall>x\<in>S. B \<le> x)"
wenzelm@53788
   685
      then have nex: "\<forall>B. \<exists>x\<in>S. x < B"
wenzelm@53788
   686
        by (simp add: not_le)
wenzelm@53788
   687
      {
wenzelm@53788
   688
        fix y
wenzelm@53788
   689
        obtain x where "x\<in>S" and "x < y"
wenzelm@53788
   690
          using nex by auto
wenzelm@53788
   691
        then have "y \<in> S"
wenzelm@53788
   692
          using mono[rule_format, of x y] by auto
wenzelm@53788
   693
      }
wenzelm@53788
   694
      then have "S = UNIV"
wenzelm@53788
   695
        by auto
wenzelm@49664
   696
    }
wenzelm@53788
   697
    ultimately have "S = UNIV \<or> (\<exists>a. S = {a ..})"
wenzelm@53788
   698
      by blast
wenzelm@53788
   699
  }
wenzelm@53788
   700
  then show ?thesis
wenzelm@53788
   701
    by blast
hoelzl@41980
   702
qed
hoelzl@41980
   703
hoelzl@43920
   704
lemma mono_closed_ereal:
hoelzl@41980
   705
  fixes S :: "real set"
wenzelm@53788
   706
  assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
wenzelm@49664
   707
    and "closed S"
wenzelm@53788
   708
  shows "\<exists>a. S = {x. a \<le> ereal x}"
wenzelm@49664
   709
proof -
wenzelm@53788
   710
  {
wenzelm@53788
   711
    assume "S = {}"
wenzelm@53788
   712
    then have ?thesis
wenzelm@53788
   713
      apply (rule_tac x=PInfty in exI)
wenzelm@53788
   714
      apply auto
wenzelm@53788
   715
      done
wenzelm@53788
   716
  }
wenzelm@49664
   717
  moreover
wenzelm@53788
   718
  {
wenzelm@53788
   719
    assume "S = UNIV"
wenzelm@53788
   720
    then have ?thesis
wenzelm@53788
   721
      apply (rule_tac x="-\<infinity>" in exI)
wenzelm@53788
   722
      apply auto
wenzelm@53788
   723
      done
wenzelm@53788
   724
  }
wenzelm@49664
   725
  moreover
wenzelm@53788
   726
  {
wenzelm@53788
   727
    assume "\<exists>a. S = {a ..}"
wenzelm@53788
   728
    then obtain a where "S = {a ..}"
wenzelm@53788
   729
      by auto
wenzelm@53788
   730
    then have ?thesis
wenzelm@53788
   731
      apply (rule_tac x="ereal a" in exI)
wenzelm@53788
   732
      apply auto
wenzelm@53788
   733
      done
wenzelm@49664
   734
  }
wenzelm@53788
   735
  ultimately show ?thesis
wenzelm@53788
   736
    using mono_closed_real[of S] assms by auto
hoelzl@41980
   737
qed
hoelzl@41980
   738
wenzelm@53788
   739
hoelzl@41980
   740
subsection {* Sums *}
hoelzl@41980
   741
wenzelm@49664
   742
lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
wenzelm@53788
   743
proof (cases "finite A")
wenzelm@53788
   744
  case True
wenzelm@49664
   745
  then show ?thesis by induct auto
wenzelm@53788
   746
next
wenzelm@53788
   747
  case False
wenzelm@53788
   748
  then show ?thesis by simp
wenzelm@53788
   749
qed
hoelzl@41980
   750
hoelzl@43923
   751
lemma setsum_Pinfty:
hoelzl@43923
   752
  fixes f :: "'a \<Rightarrow> ereal"
wenzelm@53788
   753
  shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
hoelzl@41980
   754
proof safe
hoelzl@41980
   755
  assume *: "setsum f P = \<infinity>"
hoelzl@41980
   756
  show "finite P"
wenzelm@53788
   757
  proof (rule ccontr)
wenzelm@53788
   758
    assume "infinite P"
wenzelm@53788
   759
    with * show False
wenzelm@53788
   760
      by auto
wenzelm@53788
   761
  qed
hoelzl@41980
   762
  show "\<exists>i\<in>P. f i = \<infinity>"
hoelzl@41980
   763
  proof (rule ccontr)
wenzelm@53788
   764
    assume "\<not> ?thesis"
wenzelm@53788
   765
    then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>"
wenzelm@53788
   766
      by auto
wenzelm@53788
   767
    with `finite P` have "setsum f P \<noteq> \<infinity>"
hoelzl@41980
   768
      by induct auto
wenzelm@53788
   769
    with * show False
wenzelm@53788
   770
      by auto
hoelzl@41980
   771
  qed
hoelzl@41980
   772
next
wenzelm@53788
   773
  fix i
wenzelm@53788
   774
  assume "finite P" and "i \<in> P" and "f i = \<infinity>"
wenzelm@49664
   775
  then show "setsum f P = \<infinity>"
hoelzl@41980
   776
  proof induct
hoelzl@41980
   777
    case (insert x A)
hoelzl@41980
   778
    show ?case using insert by (cases "x = i") auto
hoelzl@41980
   779
  qed simp
hoelzl@41980
   780
qed
hoelzl@41980
   781
hoelzl@41980
   782
lemma setsum_Inf:
hoelzl@43923
   783
  fixes f :: "'a \<Rightarrow> ereal"
wenzelm@53788
   784
  shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
hoelzl@41980
   785
proof
hoelzl@41980
   786
  assume *: "\<bar>setsum f A\<bar> = \<infinity>"
wenzelm@53788
   787
  have "finite A"
wenzelm@53788
   788
    by (rule ccontr) (insert *, auto)
hoelzl@41980
   789
  moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>"
hoelzl@41980
   790
  proof (rule ccontr)
wenzelm@53788
   791
    assume "\<not> ?thesis"
wenzelm@53788
   792
    then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
wenzelm@53788
   793
      by auto
wenzelm@53788
   794
    from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" ..
wenzelm@53788
   795
    with * show False
wenzelm@53788
   796
      by auto
hoelzl@41980
   797
  qed
wenzelm@53788
   798
  ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
wenzelm@53788
   799
    by auto
hoelzl@41980
   800
next
hoelzl@41980
   801
  assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
wenzelm@53788
   802
  then obtain i where "finite A" "i \<in> A" and "\<bar>f i\<bar> = \<infinity>"
wenzelm@53788
   803
    by auto
hoelzl@41980
   804
  then show "\<bar>setsum f A\<bar> = \<infinity>"
hoelzl@41980
   805
  proof induct
wenzelm@53788
   806
    case (insert j A)
wenzelm@53788
   807
    then show ?case
hoelzl@43920
   808
      by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
hoelzl@41980
   809
  qed simp
hoelzl@41980
   810
qed
hoelzl@41980
   811
hoelzl@43920
   812
lemma setsum_real_of_ereal:
hoelzl@43923
   813
  fixes f :: "'i \<Rightarrow> ereal"
hoelzl@41980
   814
  assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
hoelzl@41980
   815
  shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
hoelzl@41980
   816
proof -
hoelzl@43920
   817
  have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
hoelzl@41980
   818
  proof
wenzelm@53788
   819
    fix x
wenzelm@53788
   820
    assume "x \<in> S"
wenzelm@53788
   821
    from assms[OF this] show "\<exists>r. f x = ereal r"
wenzelm@53788
   822
      by (cases "f x") auto
hoelzl@41980
   823
  qed
wenzelm@53788
   824
  from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" ..
wenzelm@53788
   825
  then show ?thesis
wenzelm@53788
   826
    by simp
hoelzl@41980
   827
qed
hoelzl@41980
   828
hoelzl@43920
   829
lemma setsum_ereal_0:
wenzelm@53788
   830
  fixes f :: "'a \<Rightarrow> ereal"
wenzelm@53788
   831
  assumes "finite A"
wenzelm@53788
   832
    and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
hoelzl@41980
   833
  shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
hoelzl@41980
   834
proof
hoelzl@41980
   835
  assume *: "(\<Sum>x\<in>A. f x) = 0"
wenzelm@53788
   836
  then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>"
wenzelm@53788
   837
    by auto
wenzelm@53788
   838
  then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>"
wenzelm@53788
   839
    using assms by (force simp: setsum_Pinfty)
wenzelm@53788
   840
  then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
wenzelm@53788
   841
    by auto
hoelzl@41980
   842
  from bchoice[OF this] * assms show "\<forall>i\<in>A. f i = 0"
hoelzl@41980
   843
    using setsum_nonneg_eq_0_iff[of A "\<lambda>i. real (f i)"] by auto
hoelzl@41980
   844
qed (rule setsum_0')
hoelzl@41980
   845
hoelzl@43920
   846
lemma setsum_ereal_right_distrib:
wenzelm@49664
   847
  fixes f :: "'a \<Rightarrow> ereal"
wenzelm@49664
   848
  assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
hoelzl@41980
   849
  shows "r * setsum f A = (\<Sum>n\<in>A. r * f n)"
hoelzl@41980
   850
proof cases
wenzelm@49664
   851
  assume "finite A"
wenzelm@49664
   852
  then show ?thesis using assms
hoelzl@43920
   853
    by induct (auto simp: ereal_right_distrib setsum_nonneg)
hoelzl@41980
   854
qed simp
hoelzl@41980
   855
hoelzl@43920
   856
lemma sums_ereal_positive:
wenzelm@49664
   857
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   858
  assumes "\<And>i. 0 \<le> f i"
wenzelm@49664
   859
  shows "f sums (SUP n. \<Sum>i<n. f i)"
hoelzl@41980
   860
proof -
hoelzl@41980
   861
  have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
wenzelm@53788
   862
    using ereal_add_mono[OF _ assms]
wenzelm@53788
   863
    by (auto intro!: incseq_SucI)
hoelzl@51000
   864
  from LIMSEQ_SUP[OF this]
wenzelm@53788
   865
  show ?thesis unfolding sums_def
wenzelm@53788
   866
    by (simp add: atLeast0LessThan)
hoelzl@41980
   867
qed
hoelzl@41980
   868
hoelzl@43920
   869
lemma summable_ereal_pos:
wenzelm@49664
   870
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   871
  assumes "\<And>i. 0 \<le> f i"
wenzelm@49664
   872
  shows "summable f"
wenzelm@53788
   873
  using sums_ereal_positive[of f, OF assms]
wenzelm@53788
   874
  unfolding summable_def
wenzelm@53788
   875
  by auto
hoelzl@41980
   876
hoelzl@43920
   877
lemma suminf_ereal_eq_SUPR:
wenzelm@49664
   878
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   879
  assumes "\<And>i. 0 \<le> f i"
hoelzl@41980
   880
  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
wenzelm@53788
   881
  using sums_ereal_positive[of f, OF assms, THEN sums_unique]
wenzelm@53788
   882
  by simp
hoelzl@41980
   883
wenzelm@49664
   884
lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
hoelzl@41980
   885
  unfolding sums_def by simp
hoelzl@41980
   886
hoelzl@41980
   887
lemma suminf_bound:
hoelzl@43920
   888
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@53788
   889
  assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
wenzelm@53788
   890
    and pos: "\<And>n. 0 \<le> f n"
hoelzl@41980
   891
  shows "suminf f \<le> x"
hoelzl@43920
   892
proof (rule Lim_bounded_ereal)
hoelzl@43920
   893
  have "summable f" using pos[THEN summable_ereal_pos] .
hoelzl@41980
   894
  then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
hoelzl@41980
   895
    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
hoelzl@41980
   896
  show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
hoelzl@41980
   897
    using assms by auto
hoelzl@41980
   898
qed
hoelzl@41980
   899
hoelzl@41980
   900
lemma suminf_bound_add:
hoelzl@43920
   901
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   902
  assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
wenzelm@49664
   903
    and pos: "\<And>n. 0 \<le> f n"
wenzelm@49664
   904
    and "y \<noteq> -\<infinity>"
hoelzl@41980
   905
  shows "suminf f + y \<le> x"
hoelzl@41980
   906
proof (cases y)
wenzelm@49664
   907
  case (real r)
wenzelm@49664
   908
  then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
hoelzl@43920
   909
    using assms by (simp add: ereal_le_minus)
wenzelm@53788
   910
  then have "(\<Sum> n. f n) \<le> x - y"
wenzelm@53788
   911
    using pos by (rule suminf_bound)
hoelzl@41980
   912
  then show "(\<Sum> n. f n) + y \<le> x"
hoelzl@43920
   913
    using assms real by (simp add: ereal_le_minus)
hoelzl@41980
   914
qed (insert assms, auto)
hoelzl@41980
   915
hoelzl@41980
   916
lemma suminf_upper:
wenzelm@49664
   917
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   918
  assumes "\<And>n. 0 \<le> f n"
hoelzl@41980
   919
  shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
haftmann@56166
   920
  unfolding suminf_ereal_eq_SUPR[OF assms]
haftmann@56166
   921
  by (auto intro: complete_lattice_class.SUP_upper)
hoelzl@41980
   922
hoelzl@41980
   923
lemma suminf_0_le:
wenzelm@49664
   924
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
   925
  assumes "\<And>n. 0 \<le> f n"
hoelzl@41980
   926
  shows "0 \<le> (\<Sum>n. f n)"
wenzelm@53788
   927
  using suminf_upper[of f 0, OF assms]
wenzelm@53788
   928
  by simp
hoelzl@41980
   929
hoelzl@41980
   930
lemma suminf_le_pos:
hoelzl@43920
   931
  fixes f g :: "nat \<Rightarrow> ereal"
wenzelm@53788
   932
  assumes "\<And>N. f N \<le> g N"
wenzelm@53788
   933
    and "\<And>N. 0 \<le> f N"
hoelzl@41980
   934
  shows "suminf f \<le> suminf g"
hoelzl@41980
   935
proof (safe intro!: suminf_bound)
wenzelm@49664
   936
  fix n
wenzelm@53788
   937
  {
wenzelm@53788
   938
    fix N
wenzelm@53788
   939
    have "0 \<le> g N"
wenzelm@53788
   940
      using assms(2,1)[of N] by auto
wenzelm@53788
   941
  }
wenzelm@49664
   942
  have "setsum f {..<n} \<le> setsum g {..<n}"
wenzelm@49664
   943
    using assms by (auto intro: setsum_mono)
wenzelm@53788
   944
  also have "\<dots> \<le> suminf g"
wenzelm@53788
   945
    using `\<And>N. 0 \<le> g N`
wenzelm@53788
   946
    by (rule suminf_upper)
hoelzl@41980
   947
  finally show "setsum f {..<n} \<le> suminf g" .
hoelzl@41980
   948
qed (rule assms(2))
hoelzl@41980
   949
wenzelm@53788
   950
lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1"
hoelzl@43920
   951
  using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
hoelzl@43920
   952
  by (simp add: one_ereal_def)
hoelzl@41980
   953
hoelzl@43920
   954
lemma suminf_add_ereal:
hoelzl@43920
   955
  fixes f g :: "nat \<Rightarrow> ereal"
wenzelm@53788
   956
  assumes "\<And>i. 0 \<le> f i"
wenzelm@53788
   957
    and "\<And>i. 0 \<le> g i"
hoelzl@41980
   958
  shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
hoelzl@43920
   959
  apply (subst (1 2 3) suminf_ereal_eq_SUPR)
hoelzl@41980
   960
  unfolding setsum_addf
wenzelm@49664
   961
  apply (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
wenzelm@49664
   962
  done
hoelzl@41980
   963
hoelzl@43920
   964
lemma suminf_cmult_ereal:
hoelzl@43920
   965
  fixes f g :: "nat \<Rightarrow> ereal"
wenzelm@53788
   966
  assumes "\<And>i. 0 \<le> f i"
wenzelm@53788
   967
    and "0 \<le> a"
hoelzl@41980
   968
  shows "(\<Sum>i. a * f i) = a * suminf f"
hoelzl@43920
   969
  by (auto simp: setsum_ereal_right_distrib[symmetric] assms
wenzelm@53788
   970
       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR
wenzelm@53788
   971
       intro!: SUPR_ereal_cmult )
hoelzl@41980
   972
hoelzl@41980
   973
lemma suminf_PInfty:
hoelzl@43923
   974
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@53788
   975
  assumes "\<And>i. 0 \<le> f i"
wenzelm@53788
   976
    and "suminf f \<noteq> \<infinity>"
hoelzl@41980
   977
  shows "f i \<noteq> \<infinity>"
hoelzl@41980
   978
proof -
hoelzl@41980
   979
  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
wenzelm@53788
   980
  have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>"
wenzelm@53788
   981
    by auto
wenzelm@53788
   982
  then show ?thesis
wenzelm@53788
   983
    unfolding setsum_Pinfty by simp
hoelzl@41980
   984
qed
hoelzl@41980
   985
hoelzl@41980
   986
lemma suminf_PInfty_fun:
wenzelm@53788
   987
  assumes "\<And>i. 0 \<le> f i"
wenzelm@53788
   988
    and "suminf f \<noteq> \<infinity>"
hoelzl@43920
   989
  shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
hoelzl@41980
   990
proof -
hoelzl@43920
   991
  have "\<forall>i. \<exists>r. f i = ereal r"
hoelzl@41980
   992
  proof
wenzelm@53788
   993
    fix i
wenzelm@53788
   994
    show "\<exists>r. f i = ereal r"
wenzelm@53788
   995
      using suminf_PInfty[OF assms] assms(1)[of i]
wenzelm@53788
   996
      by (cases "f i") auto
hoelzl@41980
   997
  qed
wenzelm@53788
   998
  from choice[OF this] show ?thesis
wenzelm@53788
   999
    by auto
hoelzl@41980
  1000
qed
hoelzl@41980
  1001
hoelzl@43920
  1002
lemma summable_ereal:
wenzelm@53788
  1003
  assumes "\<And>i. 0 \<le> f i"
wenzelm@53788
  1004
    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
hoelzl@41980
  1005
  shows "summable f"
hoelzl@41980
  1006
proof -
hoelzl@43920
  1007
  have "0 \<le> (\<Sum>i. ereal (f i))"
hoelzl@41980
  1008
    using assms by (intro suminf_0_le) auto
hoelzl@43920
  1009
  with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
hoelzl@43920
  1010
    by (cases "\<Sum>i. ereal (f i)") auto
hoelzl@43920
  1011
  from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
wenzelm@53788
  1012
  have "summable (\<lambda>x. ereal (f x))"
wenzelm@53788
  1013
    using assms by auto
hoelzl@41980
  1014
  from summable_sums[OF this]
wenzelm@53788
  1015
  have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))"
wenzelm@53788
  1016
    by auto
hoelzl@41980
  1017
  then show "summable f"
hoelzl@43920
  1018
    unfolding r sums_ereal summable_def ..
hoelzl@41980
  1019
qed
hoelzl@41980
  1020
hoelzl@43920
  1021
lemma suminf_ereal:
wenzelm@53788
  1022
  assumes "\<And>i. 0 \<le> f i"
wenzelm@53788
  1023
    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
hoelzl@43920
  1024
  shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
hoelzl@41980
  1025
proof (rule sums_unique[symmetric])
hoelzl@43920
  1026
  from summable_ereal[OF assms]
hoelzl@43920
  1027
  show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
wenzelm@53788
  1028
    unfolding sums_ereal
wenzelm@53788
  1029
    using assms
wenzelm@53788
  1030
    by (intro summable_sums summable_ereal)
hoelzl@41980
  1031
qed
hoelzl@41980
  1032
hoelzl@43920
  1033
lemma suminf_ereal_minus:
hoelzl@43920
  1034
  fixes f g :: "nat \<Rightarrow> ereal"
wenzelm@53788
  1035
  assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i"
wenzelm@53788
  1036
    and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
hoelzl@41980
  1037
  shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
hoelzl@41980
  1038
proof -
wenzelm@53788
  1039
  {
wenzelm@53788
  1040
    fix i
wenzelm@53788
  1041
    have "0 \<le> f i"
wenzelm@53788
  1042
      using ord[of i] by auto
wenzelm@53788
  1043
  }
hoelzl@41980
  1044
  moreover
wenzelm@53788
  1045
  from suminf_PInfty_fun[OF `\<And>i. 0 \<le> f i` fin(1)] obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))" ..
wenzelm@53788
  1046
  from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))" ..
wenzelm@53788
  1047
  {
wenzelm@53788
  1048
    fix i
wenzelm@53788
  1049
    have "0 \<le> f i - g i"
wenzelm@53788
  1050
      using ord[of i] by (auto simp: ereal_le_minus_iff)
wenzelm@53788
  1051
  }
hoelzl@41980
  1052
  moreover
hoelzl@41980
  1053
  have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
hoelzl@41980
  1054
    using assms by (auto intro!: suminf_le_pos simp: field_simps)
wenzelm@53788
  1055
  then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>"
wenzelm@53788
  1056
    using fin by auto
wenzelm@53788
  1057
  ultimately show ?thesis
wenzelm@53788
  1058
    using assms `\<And>i. 0 \<le> f i`
hoelzl@41980
  1059
    apply simp
wenzelm@49664
  1060
    apply (subst (1 2 3) suminf_ereal)
wenzelm@49664
  1061
    apply (auto intro!: suminf_diff[symmetric] summable_ereal)
wenzelm@49664
  1062
    done
hoelzl@41980
  1063
qed
hoelzl@41980
  1064
wenzelm@49664
  1065
lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
hoelzl@41980
  1066
proof -
wenzelm@53788
  1067
  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)"
wenzelm@53788
  1068
    by (rule suminf_upper) auto
wenzelm@53788
  1069
  then show ?thesis
wenzelm@53788
  1070
    by simp
hoelzl@41980
  1071
qed
hoelzl@41980
  1072
hoelzl@43920
  1073
lemma summable_real_of_ereal:
hoelzl@43923
  1074
  fixes f :: "nat \<Rightarrow> ereal"
wenzelm@49664
  1075
  assumes f: "\<And>i. 0 \<le> f i"
wenzelm@49664
  1076
    and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
hoelzl@41980
  1077
  shows "summable (\<lambda>i. real (f i))"
hoelzl@41980
  1078
proof (rule summable_def[THEN iffD2])
wenzelm@53788
  1079
  have "0 \<le> (\<Sum>i. f i)"
wenzelm@53788
  1080
    using assms by (auto intro: suminf_0_le)
wenzelm@53788
  1081
  with fin obtain r where r: "ereal r = (\<Sum>i. f i)"
wenzelm@53788
  1082
    by (cases "(\<Sum>i. f i)") auto
wenzelm@53788
  1083
  {
wenzelm@53788
  1084
    fix i
wenzelm@53788
  1085
    have "f i \<noteq> \<infinity>"
wenzelm@53788
  1086
      using f by (intro suminf_PInfty[OF _ fin]) auto
wenzelm@53788
  1087
    then have "\<bar>f i\<bar> \<noteq> \<infinity>"
wenzelm@53788
  1088
      using f[of i] by auto
wenzelm@53788
  1089
  }
hoelzl@41980
  1090
  note fin = this
hoelzl@43920
  1091
  have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
wenzelm@53788
  1092
    using f
wenzelm@53788
  1093
    by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
wenzelm@53788
  1094
  also have "\<dots> = ereal r"
wenzelm@53788
  1095
    using fin r by (auto simp: ereal_real)
wenzelm@53788
  1096
  finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
wenzelm@53788
  1097
    by (auto simp: sums_ereal)
hoelzl@41980
  1098
qed
hoelzl@41980
  1099
hoelzl@42950
  1100
lemma suminf_SUP_eq:
hoelzl@43920
  1101
  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
wenzelm@53788
  1102
  assumes "\<And>i. incseq (\<lambda>n. f n i)"
wenzelm@53788
  1103
    and "\<And>n i. 0 \<le> f n i"
hoelzl@42950
  1104
  shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
hoelzl@42950
  1105
proof -
wenzelm@53788
  1106
  {
wenzelm@53788
  1107
    fix n :: nat
hoelzl@42950
  1108
    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
wenzelm@53788
  1109
      using assms
wenzelm@53788
  1110
      by (auto intro!: SUPR_ereal_setsum[symmetric])
wenzelm@53788
  1111
  }
hoelzl@42950
  1112
  note * = this
wenzelm@53788
  1113
  show ?thesis
wenzelm@53788
  1114
    using assms
hoelzl@43920
  1115
    apply (subst (1 2) suminf_ereal_eq_SUPR)
hoelzl@42950
  1116
    unfolding *
hoelzl@44928
  1117
    apply (auto intro!: SUP_upper2)
wenzelm@49664
  1118
    apply (subst SUP_commute)
wenzelm@49664
  1119
    apply rule
wenzelm@49664
  1120
    done
hoelzl@42950
  1121
qed
hoelzl@42950
  1122
hoelzl@47761
  1123
lemma suminf_setsum_ereal:
hoelzl@47761
  1124
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
hoelzl@47761
  1125
  assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
hoelzl@47761
  1126
  shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
wenzelm@53788
  1127
proof (cases "finite A")
wenzelm@53788
  1128
  case True
wenzelm@53788
  1129
  then show ?thesis
wenzelm@53788
  1130
    using nonneg
hoelzl@47761
  1131
    by induct (simp_all add: suminf_add_ereal setsum_nonneg)
wenzelm@53788
  1132
next
wenzelm@53788
  1133
  case False
wenzelm@53788
  1134
  then show ?thesis by simp
wenzelm@53788
  1135
qed
hoelzl@47761
  1136
hoelzl@50104
  1137
lemma suminf_ereal_eq_0:
hoelzl@50104
  1138
  fixes f :: "nat \<Rightarrow> ereal"
hoelzl@50104
  1139
  assumes nneg: "\<And>i. 0 \<le> f i"
hoelzl@50104
  1140
  shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
hoelzl@50104
  1141
proof
hoelzl@50104
  1142
  assume "(\<Sum>i. f i) = 0"
wenzelm@53788
  1143
  {
wenzelm@53788
  1144
    fix i
wenzelm@53788
  1145
    assume "f i \<noteq> 0"
wenzelm@53788
  1146
    with nneg have "0 < f i"
wenzelm@53788
  1147
      by (auto simp: less_le)
hoelzl@50104
  1148
    also have "f i = (\<Sum>j. if j = i then f i else 0)"
hoelzl@50104
  1149
      by (subst suminf_finite[where N="{i}"]) auto
hoelzl@50104
  1150
    also have "\<dots> \<le> (\<Sum>i. f i)"
wenzelm@53788
  1151
      using nneg
wenzelm@53788
  1152
      by (auto intro!: suminf_le_pos)
wenzelm@53788
  1153
    finally have False
wenzelm@53788
  1154
      using `(\<Sum>i. f i) = 0` by auto
wenzelm@53788
  1155
  }
wenzelm@53788
  1156
  then show "\<forall>i. f i = 0"
wenzelm@53788
  1157
    by auto
hoelzl@50104
  1158
qed simp
hoelzl@50104
  1159
hoelzl@51340
  1160
lemma Liminf_within:
hoelzl@51340
  1161
  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
hoelzl@51340
  1162
  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
hoelzl@51641
  1163
  unfolding Liminf_def eventually_at
hoelzl@51340
  1164
proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
wenzelm@53788
  1165
  fix P d
wenzelm@53788
  1166
  assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
hoelzl@51340
  1167
  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
hoelzl@51340
  1168
    by (auto simp: zero_less_dist_iff dist_commute)
hoelzl@51340
  1169
  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
hoelzl@51340
  1170
    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
hoelzl@51340
  1171
next
wenzelm@53788
  1172
  fix d :: real
wenzelm@53788
  1173
  assume "0 < d"
hoelzl@51641
  1174
  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
hoelzl@51340
  1175
    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
hoelzl@51340
  1176
    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
hoelzl@51340
  1177
       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
hoelzl@51340
  1178
qed
hoelzl@51340
  1179
hoelzl@51340
  1180
lemma Limsup_within:
wenzelm@53788
  1181
  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
hoelzl@51340
  1182
  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
hoelzl@51641
  1183
  unfolding Limsup_def eventually_at
hoelzl@51340
  1184
proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
wenzelm@53788
  1185
  fix P d
wenzelm@53788
  1186
  assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
hoelzl@51340
  1187
  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
hoelzl@51340
  1188
    by (auto simp: zero_less_dist_iff dist_commute)
hoelzl@51340
  1189
  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
hoelzl@51340
  1190
    by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
hoelzl@51340
  1191
next
wenzelm@53788
  1192
  fix d :: real
wenzelm@53788
  1193
  assume "0 < d"
hoelzl@51641
  1194
  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
hoelzl@51340
  1195
    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
hoelzl@51340
  1196
    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
hoelzl@51340
  1197
       (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
hoelzl@51340
  1198
qed
hoelzl@51340
  1199
hoelzl@51340
  1200
lemma Liminf_at:
hoelzl@54257
  1201
  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
hoelzl@51340
  1202
  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
hoelzl@51340
  1203
  using Liminf_within[of x UNIV f] by simp
hoelzl@51340
  1204
hoelzl@51340
  1205
lemma Limsup_at:
hoelzl@54257
  1206
  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
hoelzl@51340
  1207
  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
hoelzl@51340
  1208
  using Limsup_within[of x UNIV f] by simp
hoelzl@51340
  1209
hoelzl@51340
  1210
lemma min_Liminf_at:
wenzelm@53788
  1211
  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_linorder"
hoelzl@51340
  1212
  shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
hoelzl@51340
  1213
  unfolding inf_min[symmetric] Liminf_at
hoelzl@51340
  1214
  apply (subst inf_commute)
hoelzl@51340
  1215
  apply (subst SUP_inf)
hoelzl@51340
  1216
  apply (intro SUP_cong[OF refl])
hoelzl@54260
  1217
  apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
haftmann@56166
  1218
  apply (drule sym)
haftmann@56166
  1219
  apply auto
haftmann@56166
  1220
  by (metis INF_absorb centre_in_ball)
hoelzl@51340
  1221
wenzelm@53788
  1222
hoelzl@51340
  1223
subsection {* monoset *}
hoelzl@51340
  1224
hoelzl@51340
  1225
definition (in order) mono_set:
hoelzl@51340
  1226
  "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
hoelzl@51340
  1227
hoelzl@51340
  1228
lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
hoelzl@51340
  1229
lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
hoelzl@51340
  1230
lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
hoelzl@51340
  1231
lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
hoelzl@51340
  1232
hoelzl@51340
  1233
lemma (in complete_linorder) mono_set_iff:
hoelzl@51340
  1234
  fixes S :: "'a set"
hoelzl@51340
  1235
  defines "a \<equiv> Inf S"
wenzelm@53788
  1236
  shows "mono_set S \<longleftrightarrow> S = {a <..} \<or> S = {a..}" (is "_ = ?c")
hoelzl@51340
  1237
proof
hoelzl@51340
  1238
  assume "mono_set S"
wenzelm@53788
  1239
  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S"
wenzelm@53788
  1240
    by (auto simp: mono_set)
hoelzl@51340
  1241
  show ?c
hoelzl@51340
  1242
  proof cases
hoelzl@51340
  1243
    assume "a \<in> S"
hoelzl@51340
  1244
    show ?c
hoelzl@51340
  1245
      using mono[OF _ `a \<in> S`]
hoelzl@51340
  1246
      by (auto intro: Inf_lower simp: a_def)
hoelzl@51340
  1247
  next
hoelzl@51340
  1248
    assume "a \<notin> S"
hoelzl@51340
  1249
    have "S = {a <..}"
hoelzl@51340
  1250
    proof safe
hoelzl@51340
  1251
      fix x assume "x \<in> S"
wenzelm@53788
  1252
      then have "a \<le> x"
wenzelm@53788
  1253
        unfolding a_def by (rule Inf_lower)
wenzelm@53788
  1254
      then show "a < x"
wenzelm@53788
  1255
        using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
hoelzl@51340
  1256
    next
hoelzl@51340
  1257
      fix x assume "a < x"
wenzelm@53788
  1258
      then obtain y where "y < x" "y \<in> S"
wenzelm@53788
  1259
        unfolding a_def Inf_less_iff ..
wenzelm@53788
  1260
      with mono[of y x] show "x \<in> S"
wenzelm@53788
  1261
        by auto
hoelzl@51340
  1262
    qed
hoelzl@51340
  1263
    then show ?c ..
hoelzl@51340
  1264
  qed
hoelzl@51340
  1265
qed auto
hoelzl@51340
  1266
hoelzl@51340
  1267
lemma ereal_open_mono_set:
hoelzl@51340
  1268
  fixes S :: "ereal set"
wenzelm@53788
  1269
  shows "open S \<and> mono_set S \<longleftrightarrow> S = UNIV \<or> S = {Inf S <..}"
hoelzl@51340
  1270
  by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
hoelzl@51340
  1271
    ereal_open_closed mono_set_iff open_ereal_greaterThan)
hoelzl@51340
  1272
hoelzl@51340
  1273
lemma ereal_closed_mono_set:
hoelzl@51340
  1274
  fixes S :: "ereal set"
wenzelm@53788
  1275
  shows "closed S \<and> mono_set S \<longleftrightarrow> S = {} \<or> S = {Inf S ..}"
hoelzl@51340
  1276
  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
hoelzl@51340
  1277
    ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
hoelzl@51340
  1278
hoelzl@51340
  1279
lemma ereal_Liminf_Sup_monoset:
wenzelm@53788
  1280
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@51340
  1281
  shows "Liminf net f =
hoelzl@51340
  1282
    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
  1283
    (is "_ = Sup ?A")
hoelzl@51340
  1284
proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
wenzelm@53788
  1285
  fix P
wenzelm@53788
  1286
  assume P: "eventually P net"
wenzelm@53788
  1287
  fix S
wenzelm@53788
  1288
  assume S: "mono_set S" "INFI (Collect P) f \<in> S"
wenzelm@53788
  1289
  {
wenzelm@53788
  1290
    fix x
wenzelm@53788
  1291
    assume "P x"
hoelzl@51340
  1292
    then have "INFI (Collect P) f \<le> f x"
hoelzl@51340
  1293
      by (intro complete_lattice_class.INF_lower) simp
hoelzl@51340
  1294
    with S have "f x \<in> S"
wenzelm@53788
  1295
      by (simp add: mono_set)
wenzelm@53788
  1296
  }
hoelzl@51340
  1297
  with P show "eventually (\<lambda>x. f x \<in> S) net"
hoelzl@51340
  1298
    by (auto elim: eventually_elim1)
hoelzl@51340
  1299
next
hoelzl@51340
  1300
  fix y l
hoelzl@51340
  1301
  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
  1302
  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
hoelzl@51340
  1303
  show "l \<le> y"
hoelzl@51340
  1304
  proof (rule dense_le)
wenzelm@53788
  1305
    fix B
wenzelm@53788
  1306
    assume "B < l"
hoelzl@51340
  1307
    then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
hoelzl@51340
  1308
      by (intro S[rule_format]) auto
hoelzl@51340
  1309
    then have "INFI {x. B < f x} f \<le> y"
hoelzl@51340
  1310
      using P by auto
hoelzl@51340
  1311
    moreover have "B \<le> INFI {x. B < f x} f"
hoelzl@51340
  1312
      by (intro INF_greatest) auto
hoelzl@51340
  1313
    ultimately show "B \<le> y"
hoelzl@51340
  1314
      by simp
hoelzl@51340
  1315
  qed
hoelzl@51340
  1316
qed
hoelzl@51340
  1317
hoelzl@51340
  1318
lemma ereal_Limsup_Inf_monoset:
wenzelm@53788
  1319
  fixes f :: "'a \<Rightarrow> ereal"
hoelzl@51340
  1320
  shows "Limsup net f =
hoelzl@51340
  1321
    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
  1322
    (is "_ = Inf ?A")
hoelzl@51340
  1323
proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
wenzelm@53788
  1324
  fix P
wenzelm@53788
  1325
  assume P: "eventually P net"
wenzelm@53788
  1326
  fix S
wenzelm@53788
  1327
  assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
wenzelm@53788
  1328
  {
wenzelm@53788
  1329
    fix x
wenzelm@53788
  1330
    assume "P x"
hoelzl@51340
  1331
    then have "f x \<le> SUPR (Collect P) f"
hoelzl@51340
  1332
      by (intro complete_lattice_class.SUP_upper) simp
hoelzl@51340
  1333
    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
hoelzl@51340
  1334
    have "f x \<in> S"
hoelzl@51340
  1335
      by (simp add: inj_image_mem_iff) }
hoelzl@51340
  1336
  with P show "eventually (\<lambda>x. f x \<in> S) net"
hoelzl@51340
  1337
    by (auto elim: eventually_elim1)
hoelzl@51340
  1338
next
hoelzl@51340
  1339
  fix y l
hoelzl@51340
  1340
  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
  1341
  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
hoelzl@51340
  1342
  show "y \<le> l"
hoelzl@51340
  1343
  proof (rule dense_ge)
wenzelm@53788
  1344
    fix B
wenzelm@53788
  1345
    assume "l < B"
hoelzl@51340
  1346
    then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
hoelzl@51340
  1347
      by (intro S[rule_format]) auto
hoelzl@51340
  1348
    then have "y \<le> SUPR {x. f x < B} f"
hoelzl@51340
  1349
      using P by auto
hoelzl@51340
  1350
    moreover have "SUPR {x. f x < B} f \<le> B"
hoelzl@51340
  1351
      by (intro SUP_least) auto
hoelzl@51340
  1352
    ultimately show "y \<le> B"
hoelzl@51340
  1353
      by simp
hoelzl@51340
  1354
  qed
hoelzl@51340
  1355
qed
hoelzl@51340
  1356
hoelzl@51340
  1357
lemma liminf_bounded_open:
hoelzl@51340
  1358
  fixes x :: "nat \<Rightarrow> ereal"
hoelzl@51340
  1359
  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
  1360
  (is "_ \<longleftrightarrow> ?P x0")
hoelzl@51340
  1361
proof
hoelzl@51340
  1362
  assume "?P x0"
hoelzl@51340
  1363
  then show "x0 \<le> liminf x"
hoelzl@51340
  1364
    unfolding ereal_Liminf_Sup_monoset eventually_sequentially
hoelzl@51340
  1365
    by (intro complete_lattice_class.Sup_upper) auto
hoelzl@51340
  1366
next
hoelzl@51340
  1367
  assume "x0 \<le> liminf x"
wenzelm@53788
  1368
  {
wenzelm@53788
  1369
    fix S :: "ereal set"
wenzelm@53788
  1370
    assume om: "open S" "mono_set S" "x0 \<in> S"
wenzelm@53788
  1371
    {
wenzelm@53788
  1372
      assume "S = UNIV"
wenzelm@53788
  1373
      then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
wenzelm@53788
  1374
        by auto
wenzelm@53788
  1375
    }
hoelzl@51340
  1376
    moreover
wenzelm@53788
  1377
    {
wenzelm@53788
  1378
      assume "S \<noteq> UNIV"
wenzelm@53788
  1379
      then obtain B where B: "S = {B<..}"
wenzelm@53788
  1380
        using om ereal_open_mono_set by auto
wenzelm@53788
  1381
      then have "B < x0"
wenzelm@53788
  1382
        using om by auto
wenzelm@53788
  1383
      then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
wenzelm@53788
  1384
        unfolding B
wenzelm@53788
  1385
        using `x0 \<le> liminf x` liminf_bounded_iff
wenzelm@53788
  1386
        by auto
hoelzl@51340
  1387
    }
wenzelm@53788
  1388
    ultimately have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
wenzelm@53788
  1389
      by auto
hoelzl@51340
  1390
  }
wenzelm@53788
  1391
  then show "?P x0"
wenzelm@53788
  1392
    by auto
hoelzl@51340
  1393
qed
hoelzl@51340
  1394
huffman@44125
  1395
end