src/HOL/Library/Liminf_Limsup.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69861 62e47f06d22c
child 70378 ebd108578ab1
permissions -rw-r--r--
improved code equations taken over from AFP
hoelzl@51340
     1
(*  Title:      HOL/Library/Liminf_Limsup.thy
hoelzl@51340
     2
    Author:     Johannes Hölzl, TU München
eberlm@62049
     3
    Author:     Manuel Eberl, TU München
hoelzl@51340
     4
*)
hoelzl@51340
     5
hoelzl@62624
     6
section \<open>Liminf and Limsup on conditionally complete lattices\<close>
hoelzl@51340
     7
hoelzl@51340
     8
theory Liminf_Limsup
wenzelm@51542
     9
imports Complex_Main
hoelzl@51340
    10
begin
hoelzl@51340
    11
hoelzl@62624
    12
lemma (in conditionally_complete_linorder) le_cSup_iff:
hoelzl@62624
    13
  assumes "A \<noteq> {}" "bdd_above A"
hoelzl@62624
    14
  shows "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
hoelzl@62624
    15
proof safe
hoelzl@62624
    16
  fix y assume "x \<le> Sup A" "y < x"
hoelzl@62624
    17
  then have "y < Sup A" by auto
hoelzl@62624
    18
  then show "\<exists>a\<in>A. y < a"
hoelzl@62624
    19
    unfolding less_cSup_iff[OF assms] .
hoelzl@62624
    20
qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] cSup_upper assms)
hoelzl@62624
    21
hoelzl@62624
    22
lemma (in conditionally_complete_linorder) le_cSUP_iff:
haftmann@69313
    23
  "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> Sup (f ` A) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
hoelzl@62624
    24
  using le_cSup_iff [of "f ` A"] by simp
hoelzl@62624
    25
hoelzl@62624
    26
lemma le_cSup_iff_less:
hoelzl@62624
    27
  fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
haftmann@69260
    28
  shows "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> (SUP i\<in>A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)"
hoelzl@62624
    29
  by (simp add: le_cSUP_iff)
hoelzl@62624
    30
     (blast intro: less_imp_le less_trans less_le_trans dest: dense)
hoelzl@62624
    31
hoelzl@51340
    32
lemma le_Sup_iff_less:
hoelzl@53216
    33
  fixes x :: "'a :: {complete_linorder, dense_linorder}"
haftmann@69260
    34
  shows "x \<le> (SUP i\<in>A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
hoelzl@51340
    35
  unfolding le_SUP_iff
hoelzl@51340
    36
  by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
hoelzl@51340
    37
hoelzl@62624
    38
lemma (in conditionally_complete_linorder) cInf_le_iff:
hoelzl@62624
    39
  assumes "A \<noteq> {}" "bdd_below A"
hoelzl@62624
    40
  shows "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
hoelzl@62624
    41
proof safe
hoelzl@62624
    42
  fix y assume "x \<ge> Inf A" "y > x"
hoelzl@62624
    43
  then have "y > Inf A" by auto
hoelzl@62624
    44
  then show "\<exists>a\<in>A. y > a"
hoelzl@62624
    45
    unfolding cInf_less_iff[OF assms] .
hoelzl@62624
    46
qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] cInf_lower assms)
hoelzl@62624
    47
hoelzl@62624
    48
lemma (in conditionally_complete_linorder) cINF_le_iff:
haftmann@69313
    49
  "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> Inf (f ` A) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
hoelzl@62624
    50
  using cInf_le_iff [of "f ` A"] by simp
hoelzl@62624
    51
hoelzl@62624
    52
lemma cInf_le_iff_less:
hoelzl@62624
    53
  fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
haftmann@69260
    54
  shows "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i\<in>A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
hoelzl@62624
    55
  by (simp add: cINF_le_iff)
hoelzl@62624
    56
     (blast intro: less_imp_le less_trans le_less_trans dest: dense)
hoelzl@62624
    57
hoelzl@51340
    58
lemma Inf_le_iff_less:
hoelzl@53216
    59
  fixes x :: "'a :: {complete_linorder, dense_linorder}"
haftmann@69260
    60
  shows "(INF i\<in>A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
hoelzl@51340
    61
  unfolding INF_le_iff
hoelzl@51340
    62
  by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
hoelzl@51340
    63
haftmann@56212
    64
lemma SUP_pair:
hoelzl@54257
    65
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
haftmann@69260
    66
  shows "(SUP i \<in> A. SUP j \<in> B. f i j) = (SUP p \<in> A \<times> B. f (fst p) (snd p))"
hoelzl@51340
    67
  by (rule antisym) (auto intro!: SUP_least SUP_upper2)
hoelzl@51340
    68
haftmann@56212
    69
lemma INF_pair:
hoelzl@54257
    70
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
haftmann@69260
    71
  shows "(INF i \<in> A. INF j \<in> B. f i j) = (INF p \<in> A \<times> B. f (fst p) (snd p))"
hoelzl@51340
    72
  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
hoelzl@51340
    73
eberlm@68860
    74
lemma INF_Sigma:
eberlm@68860
    75
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
haftmann@69260
    76
  shows "(INF i \<in> A. INF j \<in> B i. f i j) = (INF p \<in> Sigma A B. f (fst p) (snd p))"
eberlm@68860
    77
  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
eberlm@68860
    78
wenzelm@61585
    79
subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
hoelzl@51340
    80
hoelzl@54261
    81
definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
haftmann@69260
    82
  "Liminf F f = (SUP P\<in>{P. eventually P F}. INF x\<in>{x. P x}. f x)"
hoelzl@51340
    83
hoelzl@54261
    84
definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
haftmann@69260
    85
  "Limsup F f = (INF P\<in>{P. eventually P F}. SUP x\<in>{x. P x}. f x)"
hoelzl@51340
    86
hoelzl@51340
    87
abbreviation "liminf \<equiv> Liminf sequentially"
hoelzl@51340
    88
hoelzl@51340
    89
abbreviation "limsup \<equiv> Limsup sequentially"
hoelzl@51340
    90
hoelzl@51340
    91
lemma Liminf_eqI:
haftmann@69313
    92
  "(\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> x) \<Longrightarrow>
haftmann@69313
    93
    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
hoelzl@51340
    94
  unfolding Liminf_def by (auto intro!: SUP_eqI)
hoelzl@51340
    95
hoelzl@51340
    96
lemma Limsup_eqI:
haftmann@69313
    97
  "(\<And>P. eventually P F \<Longrightarrow> x \<le> Sup (f ` (Collect P))) \<Longrightarrow>
haftmann@69313
    98
    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
hoelzl@51340
    99
  unfolding Limsup_def by (auto intro!: INF_eqI)
hoelzl@51340
   100
haftmann@69260
   101
lemma liminf_SUP_INF: "liminf f = (SUP n. INF m\<in>{n..}. f m)"
hoelzl@51340
   102
  unfolding Liminf_def eventually_sequentially
haftmann@56212
   103
  by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono)
hoelzl@51340
   104
haftmann@69260
   105
lemma limsup_INF_SUP: "limsup f = (INF n. SUP m\<in>{n..}. f m)"
hoelzl@51340
   106
  unfolding Limsup_def eventually_sequentially
haftmann@56212
   107
  by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
hoelzl@51340
   108
wenzelm@61730
   109
lemma Limsup_const:
hoelzl@51340
   110
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@54261
   111
  shows "Limsup F (\<lambda>x. c) = c"
hoelzl@51340
   112
proof -
hoelzl@51340
   113
  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
haftmann@69260
   114
  have "\<And>P. eventually P F \<Longrightarrow> (SUP x \<in> {x. P x}. c) = c"
hoelzl@51340
   115
    using ntriv by (intro SUP_const) (auto simp: eventually_False *)
hoelzl@51340
   116
  then show ?thesis
haftmann@69661
   117
    apply (auto simp add: Limsup_def)
haftmann@69661
   118
    apply (rule INF_const)
haftmann@69661
   119
    apply auto
haftmann@69661
   120
    using eventually_True apply blast
haftmann@69661
   121
    done
hoelzl@51340
   122
qed
hoelzl@51340
   123
hoelzl@51340
   124
lemma Liminf_const:
hoelzl@51340
   125
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@54261
   126
  shows "Liminf F (\<lambda>x. c) = c"
hoelzl@51340
   127
proof -
hoelzl@51340
   128
  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
haftmann@69260
   129
  have "\<And>P. eventually P F \<Longrightarrow> (INF x \<in> {x. P x}. c) = c"
hoelzl@51340
   130
    using ntriv by (intro INF_const) (auto simp: eventually_False *)
hoelzl@51340
   131
  then show ?thesis
haftmann@69661
   132
    apply (auto simp add: Liminf_def)
haftmann@69661
   133
    apply (rule SUP_const)
haftmann@69661
   134
    apply auto
haftmann@69661
   135
    using eventually_True apply blast
haftmann@69661
   136
    done
hoelzl@51340
   137
qed
hoelzl@51340
   138
hoelzl@51340
   139
lemma Liminf_mono:
hoelzl@51340
   140
  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
hoelzl@51340
   141
  shows "Liminf F f \<le> Liminf F g"
hoelzl@51340
   142
  unfolding Liminf_def
hoelzl@51340
   143
proof (safe intro!: SUP_mono)
hoelzl@51340
   144
  fix P assume "eventually P F"
hoelzl@51340
   145
  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
haftmann@69313
   146
  then show "\<exists>Q\<in>{P. eventually P F}. Inf (f ` (Collect P)) \<le> Inf (g ` (Collect Q))"
hoelzl@51340
   147
    by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
hoelzl@51340
   148
qed
hoelzl@51340
   149
hoelzl@51340
   150
lemma Liminf_eq:
hoelzl@51340
   151
  assumes "eventually (\<lambda>x. f x = g x) F"
hoelzl@51340
   152
  shows "Liminf F f = Liminf F g"
lp15@61810
   153
  by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
hoelzl@51340
   154
hoelzl@51340
   155
lemma Limsup_mono:
hoelzl@51340
   156
  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
hoelzl@51340
   157
  shows "Limsup F f \<le> Limsup F g"
hoelzl@51340
   158
  unfolding Limsup_def
hoelzl@51340
   159
proof (safe intro!: INF_mono)
hoelzl@51340
   160
  fix P assume "eventually P F"
hoelzl@51340
   161
  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
haftmann@69313
   162
  then show "\<exists>Q\<in>{P. eventually P F}. Sup (f ` (Collect Q)) \<le> Sup (g ` (Collect P))"
hoelzl@51340
   163
    by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
hoelzl@51340
   164
qed
hoelzl@51340
   165
hoelzl@51340
   166
lemma Limsup_eq:
hoelzl@51340
   167
  assumes "eventually (\<lambda>x. f x = g x) net"
hoelzl@51340
   168
  shows "Limsup net f = Limsup net g"
lp15@61810
   169
  by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
hoelzl@51340
   170
immler@63895
   171
lemma Liminf_bot[simp]: "Liminf bot f = top"
immler@63895
   172
  unfolding Liminf_def top_unique[symmetric]
immler@63895
   173
  by (rule SUP_upper2[where i="\<lambda>x. False"]) simp_all
immler@63895
   174
immler@63895
   175
lemma Limsup_bot[simp]: "Limsup bot f = bot"
immler@63895
   176
  unfolding Limsup_def bot_unique[symmetric]
immler@63895
   177
  by (rule INF_lower2[where i="\<lambda>x. False"]) simp_all
immler@63895
   178
hoelzl@51340
   179
lemma Liminf_le_Limsup:
hoelzl@51340
   180
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   181
  shows "Liminf F f \<le> Limsup F f"
hoelzl@51340
   182
  unfolding Limsup_def Liminf_def
hoelzl@54261
   183
  apply (rule SUP_least)
hoelzl@54261
   184
  apply (rule INF_greatest)
hoelzl@51340
   185
proof safe
hoelzl@51340
   186
  fix P Q assume "eventually P F" "eventually Q F"
hoelzl@51340
   187
  then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
hoelzl@51340
   188
  then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
hoelzl@51340
   189
    using ntriv by (auto simp add: eventually_False)
haftmann@69313
   190
  have "Inf (f ` (Collect P)) \<le> Inf (f ` (Collect ?C))"
hoelzl@51340
   191
    by (rule INF_mono) auto
haftmann@69313
   192
  also have "\<dots> \<le> Sup (f ` (Collect ?C))"
hoelzl@51340
   193
    using not_False by (intro INF_le_SUP) auto
haftmann@69313
   194
  also have "\<dots> \<le> Sup (f ` (Collect Q))"
hoelzl@51340
   195
    by (rule SUP_mono) auto
haftmann@69313
   196
  finally show "Inf (f ` (Collect P)) \<le> Sup (f ` (Collect Q))" .
hoelzl@51340
   197
qed
hoelzl@51340
   198
hoelzl@51340
   199
lemma Liminf_bounded:
hoelzl@51340
   200
  assumes le: "eventually (\<lambda>n. C \<le> X n) F"
hoelzl@51340
   201
  shows "C \<le> Liminf F X"
immler@63895
   202
  using Liminf_mono[OF le] Liminf_const[of F C]
immler@63895
   203
  by (cases "F = bot") simp_all
hoelzl@51340
   204
hoelzl@51340
   205
lemma Limsup_bounded:
hoelzl@51340
   206
  assumes le: "eventually (\<lambda>n. X n \<le> C) F"
hoelzl@51340
   207
  shows "Limsup F X \<le> C"
immler@63895
   208
  using Limsup_mono[OF le] Limsup_const[of F C]
immler@63895
   209
  by (cases "F = bot") simp_all
hoelzl@51340
   210
hoelzl@61245
   211
lemma le_Limsup:
hoelzl@61245
   212
  assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
hoelzl@61245
   213
  shows "l \<le> Limsup F f"
eberlm@68860
   214
  using F Liminf_bounded[of l f F] Liminf_le_Limsup[of F f] order.trans x by blast
immler@63895
   215
immler@63895
   216
lemma Liminf_le:
immler@63895
   217
  assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. f x \<le> l"
immler@63895
   218
  shows "Liminf F f \<le> l"
immler@63895
   219
  using F Liminf_le_Limsup Limsup_bounded order.trans x by blast
hoelzl@61245
   220
hoelzl@51340
   221
lemma le_Liminf_iff:
hoelzl@51340
   222
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
hoelzl@51340
   223
  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
hoelzl@51340
   224
proof -
wenzelm@61730
   225
  have "eventually (\<lambda>x. y < X x) F"
haftmann@69313
   226
    if "eventually P F" "y < Inf (X ` (Collect P))" for y P
lp15@61810
   227
    using that by (auto elim!: eventually_mono dest: less_INF_D)
hoelzl@51340
   228
  moreover
haftmann@69313
   229
  have "\<exists>P. eventually P F \<and> y < Inf (X ` (Collect P))"
wenzelm@61730
   230
    if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
wenzelm@61730
   231
  proof (cases "\<exists>z. y < z \<and> z < C")
wenzelm@61730
   232
    case True
wenzelm@61730
   233
    then obtain z where z: "y < z \<and> z < C" ..
haftmann@69313
   234
    moreover from z have "z \<le> Inf (X ` {x. z < X x})"
wenzelm@61730
   235
      by (auto intro!: INF_greatest)
wenzelm@61730
   236
    ultimately show ?thesis
wenzelm@61730
   237
      using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
wenzelm@61730
   238
  next
wenzelm@61730
   239
    case False
haftmann@69313
   240
    then have "C \<le> Inf (X ` {x. y < X x})"
wenzelm@61730
   241
      by (intro INF_greatest) auto
wenzelm@61730
   242
    with \<open>y < C\<close> show ?thesis
wenzelm@61730
   243
      using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
wenzelm@61730
   244
  qed
hoelzl@51340
   245
  ultimately show ?thesis
hoelzl@51340
   246
    unfolding Liminf_def le_SUP_iff by auto
hoelzl@51340
   247
qed
hoelzl@51340
   248
eberlm@62049
   249
lemma Limsup_le_iff:
eberlm@62049
   250
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
eberlm@62049
   251
  shows "C \<ge> Limsup F X \<longleftrightarrow> (\<forall>y>C. eventually (\<lambda>x. y > X x) F)"
eberlm@62049
   252
proof -
haftmann@69313
   253
  { fix y P assume "eventually P F" "y > Sup (X ` (Collect P))"
eberlm@62049
   254
    then have "eventually (\<lambda>x. y > X x) F"
eberlm@62049
   255
      by (auto elim!: eventually_mono dest: SUP_lessD) }
eberlm@62049
   256
  moreover
eberlm@62049
   257
  { fix y P assume "y > C" and y: "\<forall>y>C. eventually (\<lambda>x. y > X x) F"
haftmann@69313
   258
    have "\<exists>P. eventually P F \<and> y > Sup (X ` (Collect P))"
eberlm@62049
   259
    proof (cases "\<exists>z. C < z \<and> z < y")
eberlm@62049
   260
      case True
eberlm@62049
   261
      then obtain z where z: "C < z \<and> z < y" ..
haftmann@69313
   262
      moreover from z have "z \<ge> Sup (X ` {x. X x < z})"
eberlm@62049
   263
        by (auto intro!: SUP_least)
eberlm@62049
   264
      ultimately show ?thesis
eberlm@62049
   265
        using y by (intro exI[of _ "\<lambda>x. z > X x"]) auto
eberlm@62049
   266
    next
eberlm@62049
   267
      case False
haftmann@69313
   268
      then have "C \<ge> Sup (X ` {x. X x < y})"
eberlm@62049
   269
        by (intro SUP_least) (auto simp: not_less)
eberlm@62049
   270
      with \<open>y > C\<close> show ?thesis
eberlm@62049
   271
        using y by (intro exI[of _ "\<lambda>x. y > X x"]) auto
eberlm@62049
   272
    qed }
eberlm@62049
   273
  ultimately show ?thesis
eberlm@62049
   274
    unfolding Limsup_def INF_le_iff by auto
eberlm@62049
   275
qed
eberlm@62049
   276
eberlm@62049
   277
lemma less_LiminfD:
eberlm@62049
   278
  "y < Liminf F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x > y) F"
eberlm@62049
   279
  using le_Liminf_iff[of "Liminf F f" F f] by simp
eberlm@62049
   280
eberlm@62049
   281
lemma Limsup_lessD:
eberlm@62049
   282
  "y > Limsup F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x < y) F"
eberlm@62049
   283
  using Limsup_le_iff[of F f "Limsup F f"] by simp
eberlm@62049
   284
hoelzl@51340
   285
lemma lim_imp_Liminf:
wenzelm@61730
   286
  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
hoelzl@51340
   287
  assumes ntriv: "\<not> trivial_limit F"
wenzelm@61973
   288
  assumes lim: "(f \<longlongrightarrow> f0) F"
hoelzl@51340
   289
  shows "Liminf F f = f0"
hoelzl@51340
   290
proof (intro Liminf_eqI)
hoelzl@51340
   291
  fix P assume P: "eventually P F"
haftmann@69313
   292
  then have "eventually (\<lambda>x. Inf (f ` (Collect P)) \<le> f x) F"
hoelzl@51340
   293
    by eventually_elim (auto intro!: INF_lower)
haftmann@69313
   294
  then show "Inf (f ` (Collect P)) \<le> f0"
hoelzl@51340
   295
    by (rule tendsto_le[OF ntriv lim tendsto_const])
hoelzl@51340
   296
next
haftmann@69313
   297
  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y"
hoelzl@51340
   298
  show "f0 \<le> y"
hoelzl@51340
   299
  proof cases
hoelzl@51340
   300
    assume "\<exists>z. y < z \<and> z < f0"
wenzelm@53374
   301
    then obtain z where "y < z \<and> z < f0" ..
haftmann@69313
   302
    moreover have "z \<le> Inf (f ` {x. z < f x})"
hoelzl@51340
   303
      by (rule INF_greatest) simp
hoelzl@51340
   304
    ultimately show ?thesis
hoelzl@51340
   305
      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
hoelzl@51340
   306
  next
hoelzl@51340
   307
    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
hoelzl@51340
   308
    show ?thesis
hoelzl@51340
   309
    proof (rule classical)
hoelzl@51340
   310
      assume "\<not> f0 \<le> y"
hoelzl@51340
   311
      then have "eventually (\<lambda>x. y < f x) F"
hoelzl@51340
   312
        using lim[THEN topological_tendstoD, of "{y <..}"] by auto
hoelzl@51340
   313
      then have "eventually (\<lambda>x. f0 \<le> f x) F"
lp15@61810
   314
        using discrete by (auto elim!: eventually_mono)
haftmann@69313
   315
      then have "Inf (f ` {x. f0 \<le> f x}) \<le> y"
hoelzl@51340
   316
        by (rule upper)
haftmann@69313
   317
      moreover have "f0 \<le> Inf (f ` {x. f0 \<le> f x})"
hoelzl@51340
   318
        by (intro INF_greatest) simp
hoelzl@51340
   319
      ultimately show "f0 \<le> y" by simp
hoelzl@51340
   320
    qed
hoelzl@51340
   321
  qed
hoelzl@51340
   322
qed
hoelzl@51340
   323
hoelzl@51340
   324
lemma lim_imp_Limsup:
wenzelm@61730
   325
  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
hoelzl@51340
   326
  assumes ntriv: "\<not> trivial_limit F"
wenzelm@61973
   327
  assumes lim: "(f \<longlongrightarrow> f0) F"
hoelzl@51340
   328
  shows "Limsup F f = f0"
hoelzl@51340
   329
proof (intro Limsup_eqI)
hoelzl@51340
   330
  fix P assume P: "eventually P F"
haftmann@69313
   331
  then have "eventually (\<lambda>x. f x \<le> Sup (f ` (Collect P))) F"
hoelzl@51340
   332
    by eventually_elim (auto intro!: SUP_upper)
haftmann@69313
   333
  then show "f0 \<le> Sup (f ` (Collect P))"
hoelzl@51340
   334
    by (rule tendsto_le[OF ntriv tendsto_const lim])
hoelzl@51340
   335
next
haftmann@69313
   336
  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))"
hoelzl@51340
   337
  show "y \<le> f0"
wenzelm@53381
   338
  proof (cases "\<exists>z. f0 < z \<and> z < y")
wenzelm@53381
   339
    case True
wenzelm@53381
   340
    then obtain z where "f0 < z \<and> z < y" ..
haftmann@69313
   341
    moreover have "Sup (f ` {x. f x < z}) \<le> z"
hoelzl@51340
   342
      by (rule SUP_least) simp
hoelzl@51340
   343
    ultimately show ?thesis
hoelzl@51340
   344
      using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
hoelzl@51340
   345
  next
wenzelm@53381
   346
    case False
hoelzl@51340
   347
    show ?thesis
hoelzl@51340
   348
    proof (rule classical)
hoelzl@51340
   349
      assume "\<not> y \<le> f0"
hoelzl@51340
   350
      then have "eventually (\<lambda>x. f x < y) F"
hoelzl@51340
   351
        using lim[THEN topological_tendstoD, of "{..< y}"] by auto
hoelzl@51340
   352
      then have "eventually (\<lambda>x. f x \<le> f0) F"
lp15@61810
   353
        using False by (auto elim!: eventually_mono simp: not_less)
haftmann@69313
   354
      then have "y \<le> Sup (f ` {x. f x \<le> f0})"
hoelzl@51340
   355
        by (rule lower)
haftmann@69313
   356
      moreover have "Sup (f ` {x. f x \<le> f0}) \<le> f0"
hoelzl@51340
   357
        by (intro SUP_least) simp
hoelzl@51340
   358
      ultimately show "y \<le> f0" by simp
hoelzl@51340
   359
    qed
hoelzl@51340
   360
  qed
hoelzl@51340
   361
qed
hoelzl@51340
   362
hoelzl@51340
   363
lemma Liminf_eq_Limsup:
wenzelm@61730
   364
  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
hoelzl@51340
   365
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   366
    and lim: "Liminf F f = f0" "Limsup F f = f0"
wenzelm@61973
   367
  shows "(f \<longlongrightarrow> f0) F"
hoelzl@51340
   368
proof (rule order_tendstoI)
hoelzl@51340
   369
  fix a assume "f0 < a"
hoelzl@51340
   370
  with assms have "Limsup F f < a" by simp
haftmann@69313
   371
  then obtain P where "eventually P F" "Sup (f ` (Collect P)) < a"
hoelzl@51340
   372
    unfolding Limsup_def INF_less_iff by auto
hoelzl@51340
   373
  then show "eventually (\<lambda>x. f x < a) F"
lp15@61810
   374
    by (auto elim!: eventually_mono dest: SUP_lessD)
hoelzl@51340
   375
next
hoelzl@51340
   376
  fix a assume "a < f0"
hoelzl@51340
   377
  with assms have "a < Liminf F f" by simp
haftmann@69313
   378
  then obtain P where "eventually P F" "a < Inf (f ` (Collect P))"
hoelzl@51340
   379
    unfolding Liminf_def less_SUP_iff by auto
hoelzl@51340
   380
  then show "eventually (\<lambda>x. a < f x) F"
lp15@61810
   381
    by (auto elim!: eventually_mono dest: less_INF_D)
hoelzl@51340
   382
qed
hoelzl@51340
   383
hoelzl@51340
   384
lemma tendsto_iff_Liminf_eq_Limsup:
wenzelm@61730
   385
  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
wenzelm@61973
   386
  shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
hoelzl@51340
   387
  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
hoelzl@51340
   388
hoelzl@51340
   389
lemma liminf_subseq_mono:
hoelzl@51340
   390
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
eberlm@66447
   391
  assumes "strict_mono r"
hoelzl@51340
   392
  shows "liminf X \<le> liminf (X \<circ> r) "
hoelzl@51340
   393
proof-
haftmann@69260
   394
  have "\<And>n. (INF m\<in>{n..}. X m) \<le> (INF m\<in>{n..}. (X \<circ> r) m)"
hoelzl@51340
   395
  proof (safe intro!: INF_mono)
hoelzl@51340
   396
    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
eberlm@66447
   397
      using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
hoelzl@51340
   398
  qed
haftmann@56212
   399
  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
hoelzl@51340
   400
qed
hoelzl@51340
   401
hoelzl@51340
   402
lemma limsup_subseq_mono:
hoelzl@51340
   403
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
eberlm@66447
   404
  assumes "strict_mono r"
hoelzl@51340
   405
  shows "limsup (X \<circ> r) \<le> limsup X"
hoelzl@51340
   406
proof-
haftmann@69260
   407
  have "(SUP m\<in>{n..}. (X \<circ> r) m) \<le> (SUP m\<in>{n..}. X m)" for n
hoelzl@51340
   408
  proof (safe intro!: SUP_mono)
wenzelm@61730
   409
    fix m :: nat
wenzelm@61730
   410
    assume "n \<le> m"
wenzelm@61730
   411
    then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
eberlm@66447
   412
      using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
hoelzl@51340
   413
  qed
wenzelm@61730
   414
  then show ?thesis
wenzelm@61730
   415
    by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
hoelzl@51340
   416
qed
hoelzl@51340
   417
wenzelm@61730
   418
lemma continuous_on_imp_continuous_within:
wenzelm@61730
   419
  "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
wenzelm@61730
   420
  unfolding continuous_on_eq_continuous_within
wenzelm@61730
   421
  by (auto simp: continuous_within intro: tendsto_within_subset)
hoelzl@61245
   422
eberlm@62049
   423
lemma Liminf_compose_continuous_mono:
eberlm@62049
   424
  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
eberlm@62049
   425
  assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot"
eberlm@62049
   426
  shows "Liminf F (\<lambda>n. f (g n)) = f (Liminf F g)"
eberlm@62049
   427
proof -
eberlm@62049
   428
  { fix P assume "eventually P F"
eberlm@62049
   429
    have "\<exists>x. P x"
eberlm@62049
   430
    proof (rule ccontr)
eberlm@62049
   431
      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
eberlm@62049
   432
        by auto
eberlm@62049
   433
      with \<open>eventually P F\<close> F show False
eberlm@62049
   434
        by auto
eberlm@62049
   435
    qed }
eberlm@62049
   436
  note * = this
eberlm@62049
   437
haftmann@69861
   438
  have "f (SUP P\<in>{P. eventually P F}. Inf (g ` Collect P)) =
haftmann@69861
   439
    Sup (f ` (\<lambda>P. Inf (g ` Collect P)) ` {P. eventually P F})"
haftmann@69861
   440
    using am continuous_on_imp_continuous_within [OF c]
haftmann@69861
   441
    by (rule continuous_at_Sup_mono) (auto intro: eventually_True)
haftmann@69861
   442
  then have "f (Liminf F g) = (SUP P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
haftmann@69861
   443
    by (simp add: Liminf_def image_comp)
haftmann@69313
   444
  also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
haftmann@69661
   445
    using * continuous_at_Inf_mono [OF am continuous_on_imp_continuous_within [OF c]]
haftmann@69661
   446
    by auto 
haftmann@69861
   447
  finally show ?thesis by (auto simp: Liminf_def image_comp)
eberlm@62049
   448
qed
eberlm@62049
   449
eberlm@62049
   450
lemma Limsup_compose_continuous_mono:
eberlm@62049
   451
  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
eberlm@62049
   452
  assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot"
eberlm@62049
   453
  shows "Limsup F (\<lambda>n. f (g n)) = f (Limsup F g)"
eberlm@62049
   454
proof -
eberlm@62049
   455
  { fix P assume "eventually P F"
eberlm@62049
   456
    have "\<exists>x. P x"
eberlm@62049
   457
    proof (rule ccontr)
eberlm@62049
   458
      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
eberlm@62049
   459
        by auto
eberlm@62049
   460
      with \<open>eventually P F\<close> F show False
eberlm@62049
   461
        by auto
eberlm@62049
   462
    qed }
eberlm@62049
   463
  note * = this
eberlm@62049
   464
haftmann@69861
   465
  have "f (INF P\<in>{P. eventually P F}. Sup (g ` Collect P)) =
haftmann@69861
   466
    Inf (f ` (\<lambda>P. Sup (g ` Collect P)) ` {P. eventually P F})"
haftmann@69861
   467
    using am continuous_on_imp_continuous_within [OF c]
haftmann@69861
   468
    by (rule continuous_at_Inf_mono) (auto intro: eventually_True)
haftmann@69861
   469
  then have "f (Limsup F g) = (INF P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
haftmann@69861
   470
    by (simp add: Limsup_def image_comp)
haftmann@69313
   471
  also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
haftmann@69661
   472
    using * continuous_at_Sup_mono [OF am continuous_on_imp_continuous_within [OF c]]
haftmann@69661
   473
    by auto
haftmann@69861
   474
  finally show ?thesis by (auto simp: Limsup_def image_comp)
eberlm@62049
   475
qed
eberlm@62049
   476
hoelzl@61245
   477
lemma Liminf_compose_continuous_antimono:
wenzelm@61730
   478
  fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}"
wenzelm@61730
   479
  assumes c: "continuous_on UNIV f"
wenzelm@61730
   480
    and am: "antimono f"
wenzelm@61730
   481
    and F: "F \<noteq> bot"
hoelzl@61245
   482
  shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
hoelzl@61245
   483
proof -
wenzelm@61730
   484
  have *: "\<exists>x. P x" if "eventually P F" for P
wenzelm@61730
   485
  proof (rule ccontr)
wenzelm@61730
   486
    assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
wenzelm@61730
   487
      by auto
wenzelm@61730
   488
    with \<open>eventually P F\<close> F show False
wenzelm@61730
   489
      by auto
wenzelm@61730
   490
  qed
haftmann@69861
   491
haftmann@69861
   492
  have "f (INF P\<in>{P. eventually P F}. Sup (g ` Collect P)) =
haftmann@69861
   493
    Sup (f ` (\<lambda>P. Sup (g ` Collect P)) ` {P. eventually P F})"
haftmann@69861
   494
    using am continuous_on_imp_continuous_within [OF c]
haftmann@69861
   495
    by (rule continuous_at_Inf_antimono) (auto intro: eventually_True)
haftmann@69861
   496
  then have "f (Limsup F g) = (SUP P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
haftmann@69861
   497
    by (simp add: Limsup_def image_comp)
haftmann@69313
   498
  also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
haftmann@69661
   499
    using * continuous_at_Sup_antimono [OF am continuous_on_imp_continuous_within [OF c]]
haftmann@69661
   500
    by auto
hoelzl@61245
   501
  finally show ?thesis
haftmann@69861
   502
    by (auto simp: Liminf_def image_comp)
hoelzl@61245
   503
qed
eberlm@62049
   504
eberlm@62049
   505
lemma Limsup_compose_continuous_antimono:
eberlm@62049
   506
  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
eberlm@62049
   507
  assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot"
eberlm@62049
   508
  shows "Limsup F (\<lambda>n. f (g n)) = f (Liminf F g)"
eberlm@62049
   509
proof -
eberlm@62049
   510
  { fix P assume "eventually P F"
eberlm@62049
   511
    have "\<exists>x. P x"
eberlm@62049
   512
    proof (rule ccontr)
eberlm@62049
   513
      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
eberlm@62049
   514
        by auto
eberlm@62049
   515
      with \<open>eventually P F\<close> F show False
eberlm@62049
   516
        by auto
eberlm@62049
   517
    qed }
eberlm@62049
   518
  note * = this
eberlm@62049
   519
haftmann@69861
   520
  have "f (SUP P\<in>{P. eventually P F}. Inf (g ` Collect P)) =
haftmann@69861
   521
    Inf (f ` (\<lambda>P. Inf (g ` Collect P)) ` {P. eventually P F})"
haftmann@69861
   522
    using am continuous_on_imp_continuous_within [OF c]
haftmann@69861
   523
    by (rule continuous_at_Sup_antimono) (auto intro: eventually_True)
haftmann@69861
   524
  then have "f (Liminf F g) = (INF P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
haftmann@69861
   525
    by (simp add: Liminf_def image_comp)
haftmann@69313
   526
  also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
haftmann@69661
   527
    using * continuous_at_Inf_antimono [OF am continuous_on_imp_continuous_within [OF c]]
haftmann@69661
   528
    by auto
eberlm@62049
   529
  finally show ?thesis
haftmann@69861
   530
    by (auto simp: Limsup_def image_comp)
eberlm@62049
   531
qed
eberlm@62049
   532
immler@63895
   533
lemma Liminf_filtermap_le: "Liminf (filtermap f F) g \<le> Liminf F (\<lambda>x. g (f x))"
immler@63895
   534
  apply (cases "F = bot", simp)
immler@63895
   535
  by (subst Liminf_def)
immler@63895
   536
    (auto simp add: INF_lower Liminf_bounded eventually_filtermap eventually_mono intro!: SUP_least)
immler@63895
   537
immler@63895
   538
lemma Limsup_filtermap_ge: "Limsup (filtermap f F) g \<ge> Limsup F (\<lambda>x. g (f x))"
immler@63895
   539
  apply (cases "F = bot", simp)
immler@63895
   540
  by (subst Limsup_def)
immler@63895
   541
    (auto simp add: SUP_upper Limsup_bounded eventually_filtermap eventually_mono intro!: INF_greatest)
immler@63895
   542
haftmann@69260
   543
lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x\<in>Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x"
immler@63895
   544
  by (auto intro!: SUP_least simp: Liminf_def)
immler@63895
   545
haftmann@69260
   546
lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x\<in>Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x"
immler@63895
   547
  by (auto intro!: INF_greatest simp: Limsup_def)
immler@63895
   548
immler@63895
   549
lemma Liminf_filtermap_ge: "inj f \<Longrightarrow> Liminf (filtermap f F) g \<ge> Liminf F (\<lambda>x. g (f x))"
immler@63895
   550
  apply (cases "F = bot", simp)
immler@63895
   551
  apply (rule Liminf_least)
immler@63895
   552
  subgoal for P
immler@63895
   553
    by (auto simp: eventually_filtermap the_inv_f_f
immler@63895
   554
        intro!: Liminf_bounded INF_lower2 eventually_mono[of P])
immler@63895
   555
  done
immler@63895
   556
immler@63895
   557
lemma Limsup_filtermap_le: "inj f \<Longrightarrow> Limsup (filtermap f F) g \<le> Limsup F (\<lambda>x. g (f x))"
immler@63895
   558
  apply (cases "F = bot", simp)
immler@63895
   559
  apply (rule Limsup_greatest)
immler@63895
   560
  subgoal for P
immler@63895
   561
    by (auto simp: eventually_filtermap the_inv_f_f
immler@63895
   562
        intro!: Limsup_bounded SUP_upper2 eventually_mono[of P])
immler@63895
   563
  done
immler@63895
   564
immler@63895
   565
lemma Liminf_filtermap_eq: "inj f \<Longrightarrow> Liminf (filtermap f F) g = Liminf F (\<lambda>x. g (f x))"
immler@63895
   566
  using Liminf_filtermap_le[of f F g] Liminf_filtermap_ge[of f F g]
immler@63895
   567
  by simp
immler@63895
   568
immler@63895
   569
lemma Limsup_filtermap_eq: "inj f \<Longrightarrow> Limsup (filtermap f F) g = Limsup F (\<lambda>x. g (f x))"
immler@63895
   570
  using Limsup_filtermap_le[of f F g] Limsup_filtermap_ge[of F g f]
immler@63895
   571
  by simp
immler@63895
   572
eberlm@62049
   573
hoelzl@61880
   574
subsection \<open>More Limits\<close>
hoelzl@61880
   575
hoelzl@61880
   576
lemma convergent_limsup_cl:
hoelzl@61880
   577
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
hoelzl@61880
   578
  shows "convergent X \<Longrightarrow> limsup X = lim X"
hoelzl@61880
   579
  by (auto simp: convergent_def limI lim_imp_Limsup)
hoelzl@61880
   580
hoelzl@61880
   581
lemma convergent_liminf_cl:
hoelzl@61880
   582
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
hoelzl@61880
   583
  shows "convergent X \<Longrightarrow> liminf X = lim X"
hoelzl@61880
   584
  by (auto simp: convergent_def limI lim_imp_Liminf)
hoelzl@61880
   585
hoelzl@61880
   586
lemma lim_increasing_cl:
hoelzl@61880
   587
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
wenzelm@61969
   588
  obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
hoelzl@61880
   589
proof
wenzelm@61969
   590
  show "f \<longlonglongrightarrow> (SUP n. f n)"
hoelzl@61880
   591
    using assms
hoelzl@61880
   592
    by (intro increasing_tendsto)
hoelzl@61880
   593
       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
hoelzl@61880
   594
qed
hoelzl@61880
   595
hoelzl@61880
   596
lemma lim_decreasing_cl:
hoelzl@61880
   597
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
wenzelm@61969
   598
  obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
hoelzl@61880
   599
proof
wenzelm@61969
   600
  show "f \<longlonglongrightarrow> (INF n. f n)"
hoelzl@61880
   601
    using assms
hoelzl@61880
   602
    by (intro decreasing_tendsto)
hoelzl@61880
   603
       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
hoelzl@61880
   604
qed
hoelzl@61880
   605
hoelzl@61880
   606
lemma compact_complete_linorder:
hoelzl@61880
   607
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
eberlm@66447
   608
  shows "\<exists>l r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
hoelzl@61880
   609
proof -
eberlm@66447
   610
  obtain r where "strict_mono r" and mono: "monoseq (X \<circ> r)"
hoelzl@61880
   611
    using seq_monosub[of X]
hoelzl@61880
   612
    unfolding comp_def
hoelzl@61880
   613
    by auto
hoelzl@61880
   614
  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@61880
   615
    by (auto simp add: monoseq_def)
wenzelm@61969
   616
  then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"
hoelzl@61880
   617
     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
hoelzl@61880
   618
     by auto
hoelzl@61880
   619
  then show ?thesis
eberlm@66447
   620
    using \<open>strict_mono r\<close> by auto
hoelzl@61880
   621
qed
hoelzl@61245
   622
hoelzl@62975
   623
lemma tendsto_Limsup:
hoelzl@62975
   624
  fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
hoelzl@62975
   625
  shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Limsup F f) F"
hoelzl@62975
   626
  by (subst tendsto_iff_Liminf_eq_Limsup) auto
hoelzl@62975
   627
hoelzl@62975
   628
lemma tendsto_Liminf:
hoelzl@62975
   629
  fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
hoelzl@62975
   630
  shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Liminf F f) F"
hoelzl@62975
   631
  by (subst tendsto_iff_Liminf_eq_Limsup) auto
hoelzl@62975
   632
hoelzl@51340
   633
end