src/HOL/Library/Liminf_Limsup.thy
author hoelzl
Tue Aug 27 16:06:27 2013 +0200 (2013-08-27)
changeset 53216 ad2e09c30aa8
parent 51542 738598beeb26
child 53374 a14d2a854c02
permissions -rw-r--r--
renamed inner_dense_linorder to dense_linorder
hoelzl@51340
     1
(*  Title:      HOL/Library/Liminf_Limsup.thy
hoelzl@51340
     2
    Author:     Johannes Hölzl, TU München
hoelzl@51340
     3
*)
hoelzl@51340
     4
hoelzl@51340
     5
header {* Liminf and Limsup on complete lattices *}
hoelzl@51340
     6
hoelzl@51340
     7
theory Liminf_Limsup
wenzelm@51542
     8
imports Complex_Main
hoelzl@51340
     9
begin
hoelzl@51340
    10
hoelzl@51340
    11
lemma le_Sup_iff_less:
hoelzl@53216
    12
  fixes x :: "'a :: {complete_linorder, dense_linorder}"
hoelzl@51340
    13
  shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
hoelzl@51340
    14
  unfolding le_SUP_iff
hoelzl@51340
    15
  by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
hoelzl@51340
    16
hoelzl@51340
    17
lemma Inf_le_iff_less:
hoelzl@53216
    18
  fixes x :: "'a :: {complete_linorder, dense_linorder}"
hoelzl@51340
    19
  shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
hoelzl@51340
    20
  unfolding INF_le_iff
hoelzl@51340
    21
  by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
hoelzl@51340
    22
hoelzl@51340
    23
lemma SUPR_pair:
hoelzl@51340
    24
  "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
hoelzl@51340
    25
  by (rule antisym) (auto intro!: SUP_least SUP_upper2)
hoelzl@51340
    26
hoelzl@51340
    27
lemma INFI_pair:
hoelzl@51340
    28
  "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
hoelzl@51340
    29
  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
hoelzl@51340
    30
hoelzl@51340
    31
subsubsection {* @{text Liminf} and @{text Limsup} *}
hoelzl@51340
    32
hoelzl@51340
    33
definition
hoelzl@51340
    34
  "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
hoelzl@51340
    35
hoelzl@51340
    36
definition
hoelzl@51340
    37
  "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
hoelzl@51340
    38
hoelzl@51340
    39
abbreviation "liminf \<equiv> Liminf sequentially"
hoelzl@51340
    40
hoelzl@51340
    41
abbreviation "limsup \<equiv> Limsup sequentially"
hoelzl@51340
    42
hoelzl@51340
    43
lemma Liminf_eqI:
hoelzl@51340
    44
  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
hoelzl@51340
    45
    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
hoelzl@51340
    46
  unfolding Liminf_def by (auto intro!: SUP_eqI)
hoelzl@51340
    47
hoelzl@51340
    48
lemma Limsup_eqI:
hoelzl@51340
    49
  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
hoelzl@51340
    50
    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
hoelzl@51340
    51
  unfolding Limsup_def by (auto intro!: INF_eqI)
hoelzl@51340
    52
hoelzl@51340
    53
lemma liminf_SUPR_INFI:
hoelzl@51340
    54
  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
hoelzl@51340
    55
  shows "liminf f = (SUP n. INF m:{n..}. f m)"
hoelzl@51340
    56
  unfolding Liminf_def eventually_sequentially
hoelzl@51340
    57
  by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
hoelzl@51340
    58
hoelzl@51340
    59
lemma limsup_INFI_SUPR:
hoelzl@51340
    60
  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
hoelzl@51340
    61
  shows "limsup f = (INF n. SUP m:{n..}. f m)"
hoelzl@51340
    62
  unfolding Limsup_def eventually_sequentially
hoelzl@51340
    63
  by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
hoelzl@51340
    64
hoelzl@51340
    65
lemma Limsup_const: 
hoelzl@51340
    66
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
    67
  shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
hoelzl@51340
    68
proof -
hoelzl@51340
    69
  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
hoelzl@51340
    70
  have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
hoelzl@51340
    71
    using ntriv by (intro SUP_const) (auto simp: eventually_False *)
hoelzl@51340
    72
  then show ?thesis
hoelzl@51340
    73
    unfolding Limsup_def using eventually_True
hoelzl@51340
    74
    by (subst INF_cong[where D="\<lambda>x. c"])
hoelzl@51340
    75
       (auto intro!: INF_const simp del: eventually_True)
hoelzl@51340
    76
qed
hoelzl@51340
    77
hoelzl@51340
    78
lemma Liminf_const:
hoelzl@51340
    79
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
    80
  shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
hoelzl@51340
    81
proof -
hoelzl@51340
    82
  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
hoelzl@51340
    83
  have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
hoelzl@51340
    84
    using ntriv by (intro INF_const) (auto simp: eventually_False *)
hoelzl@51340
    85
  then show ?thesis
hoelzl@51340
    86
    unfolding Liminf_def using eventually_True
hoelzl@51340
    87
    by (subst SUP_cong[where D="\<lambda>x. c"])
hoelzl@51340
    88
       (auto intro!: SUP_const simp del: eventually_True)
hoelzl@51340
    89
qed
hoelzl@51340
    90
hoelzl@51340
    91
lemma Liminf_mono:
hoelzl@51340
    92
  fixes f g :: "'a => 'b :: complete_lattice"
hoelzl@51340
    93
  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
hoelzl@51340
    94
  shows "Liminf F f \<le> Liminf F g"
hoelzl@51340
    95
  unfolding Liminf_def
hoelzl@51340
    96
proof (safe intro!: SUP_mono)
hoelzl@51340
    97
  fix P assume "eventually P F"
hoelzl@51340
    98
  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
hoelzl@51340
    99
  then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
hoelzl@51340
   100
    by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
hoelzl@51340
   101
qed
hoelzl@51340
   102
hoelzl@51340
   103
lemma Liminf_eq:
hoelzl@51340
   104
  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
hoelzl@51340
   105
  assumes "eventually (\<lambda>x. f x = g x) F"
hoelzl@51340
   106
  shows "Liminf F f = Liminf F g"
hoelzl@51340
   107
  by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
hoelzl@51340
   108
hoelzl@51340
   109
lemma Limsup_mono:
hoelzl@51340
   110
  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
hoelzl@51340
   111
  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
hoelzl@51340
   112
  shows "Limsup F f \<le> Limsup F g"
hoelzl@51340
   113
  unfolding Limsup_def
hoelzl@51340
   114
proof (safe intro!: INF_mono)
hoelzl@51340
   115
  fix P assume "eventually P F"
hoelzl@51340
   116
  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
hoelzl@51340
   117
  then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
hoelzl@51340
   118
    by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
hoelzl@51340
   119
qed
hoelzl@51340
   120
hoelzl@51340
   121
lemma Limsup_eq:
hoelzl@51340
   122
  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
hoelzl@51340
   123
  assumes "eventually (\<lambda>x. f x = g x) net"
hoelzl@51340
   124
  shows "Limsup net f = Limsup net g"
hoelzl@51340
   125
  by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
hoelzl@51340
   126
hoelzl@51340
   127
lemma Liminf_le_Limsup:
hoelzl@51340
   128
  fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
hoelzl@51340
   129
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   130
  shows "Liminf F f \<le> Limsup F f"
hoelzl@51340
   131
  unfolding Limsup_def Liminf_def
hoelzl@51340
   132
  apply (rule complete_lattice_class.SUP_least)
hoelzl@51340
   133
  apply (rule complete_lattice_class.INF_greatest)
hoelzl@51340
   134
proof safe
hoelzl@51340
   135
  fix P Q assume "eventually P F" "eventually Q F"
hoelzl@51340
   136
  then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
hoelzl@51340
   137
  then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
hoelzl@51340
   138
    using ntriv by (auto simp add: eventually_False)
hoelzl@51340
   139
  have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
hoelzl@51340
   140
    by (rule INF_mono) auto
hoelzl@51340
   141
  also have "\<dots> \<le> SUPR (Collect ?C) f"
hoelzl@51340
   142
    using not_False by (intro INF_le_SUP) auto
hoelzl@51340
   143
  also have "\<dots> \<le> SUPR (Collect Q) f"
hoelzl@51340
   144
    by (rule SUP_mono) auto
hoelzl@51340
   145
  finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
hoelzl@51340
   146
qed
hoelzl@51340
   147
hoelzl@51340
   148
lemma Liminf_bounded:
hoelzl@51340
   149
  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
hoelzl@51340
   150
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   151
  assumes le: "eventually (\<lambda>n. C \<le> X n) F"
hoelzl@51340
   152
  shows "C \<le> Liminf F X"
hoelzl@51340
   153
  using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
hoelzl@51340
   154
hoelzl@51340
   155
lemma Limsup_bounded:
hoelzl@51340
   156
  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
hoelzl@51340
   157
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   158
  assumes le: "eventually (\<lambda>n. X n \<le> C) F"
hoelzl@51340
   159
  shows "Limsup F X \<le> C"
hoelzl@51340
   160
  using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
hoelzl@51340
   161
hoelzl@51340
   162
lemma le_Liminf_iff:
hoelzl@51340
   163
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
hoelzl@51340
   164
  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
hoelzl@51340
   165
proof -
hoelzl@51340
   166
  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
hoelzl@51340
   167
    then have "eventually (\<lambda>x. y < X x) F"
hoelzl@51340
   168
      by (auto elim!: eventually_elim1 dest: less_INF_D) }
hoelzl@51340
   169
  moreover
hoelzl@51340
   170
  { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
hoelzl@51340
   171
    have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
hoelzl@51340
   172
    proof cases
hoelzl@51340
   173
      assume "\<exists>z. y < z \<and> z < C"
hoelzl@51340
   174
      then guess z ..
hoelzl@51340
   175
      moreover then have "z \<le> INFI {x. z < X x} X"
hoelzl@51340
   176
        by (auto intro!: INF_greatest)
hoelzl@51340
   177
      ultimately show ?thesis
hoelzl@51340
   178
        using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
hoelzl@51340
   179
    next
hoelzl@51340
   180
      assume "\<not> (\<exists>z. y < z \<and> z < C)"
hoelzl@51340
   181
      then have "C \<le> INFI {x. y < X x} X"
hoelzl@51340
   182
        by (intro INF_greatest) auto
hoelzl@51340
   183
      with `y < C` show ?thesis
hoelzl@51340
   184
        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
hoelzl@51340
   185
    qed }
hoelzl@51340
   186
  ultimately show ?thesis
hoelzl@51340
   187
    unfolding Liminf_def le_SUP_iff by auto
hoelzl@51340
   188
qed
hoelzl@51340
   189
hoelzl@51340
   190
lemma lim_imp_Liminf:
hoelzl@51340
   191
  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
hoelzl@51340
   192
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   193
  assumes lim: "(f ---> f0) F"
hoelzl@51340
   194
  shows "Liminf F f = f0"
hoelzl@51340
   195
proof (intro Liminf_eqI)
hoelzl@51340
   196
  fix P assume P: "eventually P F"
hoelzl@51340
   197
  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
hoelzl@51340
   198
    by eventually_elim (auto intro!: INF_lower)
hoelzl@51340
   199
  then show "INFI (Collect P) f \<le> f0"
hoelzl@51340
   200
    by (rule tendsto_le[OF ntriv lim tendsto_const])
hoelzl@51340
   201
next
hoelzl@51340
   202
  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
hoelzl@51340
   203
  show "f0 \<le> y"
hoelzl@51340
   204
  proof cases
hoelzl@51340
   205
    assume "\<exists>z. y < z \<and> z < f0"
hoelzl@51340
   206
    then guess z ..
hoelzl@51340
   207
    moreover have "z \<le> INFI {x. z < f x} f"
hoelzl@51340
   208
      by (rule INF_greatest) simp
hoelzl@51340
   209
    ultimately show ?thesis
hoelzl@51340
   210
      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
hoelzl@51340
   211
  next
hoelzl@51340
   212
    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
hoelzl@51340
   213
    show ?thesis
hoelzl@51340
   214
    proof (rule classical)
hoelzl@51340
   215
      assume "\<not> f0 \<le> y"
hoelzl@51340
   216
      then have "eventually (\<lambda>x. y < f x) F"
hoelzl@51340
   217
        using lim[THEN topological_tendstoD, of "{y <..}"] by auto
hoelzl@51340
   218
      then have "eventually (\<lambda>x. f0 \<le> f x) F"
hoelzl@51340
   219
        using discrete by (auto elim!: eventually_elim1)
hoelzl@51340
   220
      then have "INFI {x. f0 \<le> f x} f \<le> y"
hoelzl@51340
   221
        by (rule upper)
hoelzl@51340
   222
      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
hoelzl@51340
   223
        by (intro INF_greatest) simp
hoelzl@51340
   224
      ultimately show "f0 \<le> y" by simp
hoelzl@51340
   225
    qed
hoelzl@51340
   226
  qed
hoelzl@51340
   227
qed
hoelzl@51340
   228
hoelzl@51340
   229
lemma lim_imp_Limsup:
hoelzl@51340
   230
  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
hoelzl@51340
   231
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   232
  assumes lim: "(f ---> f0) F"
hoelzl@51340
   233
  shows "Limsup F f = f0"
hoelzl@51340
   234
proof (intro Limsup_eqI)
hoelzl@51340
   235
  fix P assume P: "eventually P F"
hoelzl@51340
   236
  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
hoelzl@51340
   237
    by eventually_elim (auto intro!: SUP_upper)
hoelzl@51340
   238
  then show "f0 \<le> SUPR (Collect P) f"
hoelzl@51340
   239
    by (rule tendsto_le[OF ntriv tendsto_const lim])
hoelzl@51340
   240
next
hoelzl@51340
   241
  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
hoelzl@51340
   242
  show "y \<le> f0"
hoelzl@51340
   243
  proof cases
hoelzl@51340
   244
    assume "\<exists>z. f0 < z \<and> z < y"
hoelzl@51340
   245
    then guess z ..
hoelzl@51340
   246
    moreover have "SUPR {x. f x < z} f \<le> z"
hoelzl@51340
   247
      by (rule SUP_least) simp
hoelzl@51340
   248
    ultimately show ?thesis
hoelzl@51340
   249
      using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
hoelzl@51340
   250
  next
hoelzl@51340
   251
    assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
hoelzl@51340
   252
    show ?thesis
hoelzl@51340
   253
    proof (rule classical)
hoelzl@51340
   254
      assume "\<not> y \<le> f0"
hoelzl@51340
   255
      then have "eventually (\<lambda>x. f x < y) F"
hoelzl@51340
   256
        using lim[THEN topological_tendstoD, of "{..< y}"] by auto
hoelzl@51340
   257
      then have "eventually (\<lambda>x. f x \<le> f0) F"
hoelzl@51340
   258
        using discrete by (auto elim!: eventually_elim1 simp: not_less)
hoelzl@51340
   259
      then have "y \<le> SUPR {x. f x \<le> f0} f"
hoelzl@51340
   260
        by (rule lower)
hoelzl@51340
   261
      moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
hoelzl@51340
   262
        by (intro SUP_least) simp
hoelzl@51340
   263
      ultimately show "y \<le> f0" by simp
hoelzl@51340
   264
    qed
hoelzl@51340
   265
  qed
hoelzl@51340
   266
qed
hoelzl@51340
   267
hoelzl@51340
   268
lemma Liminf_eq_Limsup:
hoelzl@51340
   269
  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
hoelzl@51340
   270
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   271
    and lim: "Liminf F f = f0" "Limsup F f = f0"
hoelzl@51340
   272
  shows "(f ---> f0) F"
hoelzl@51340
   273
proof (rule order_tendstoI)
hoelzl@51340
   274
  fix a assume "f0 < a"
hoelzl@51340
   275
  with assms have "Limsup F f < a" by simp
hoelzl@51340
   276
  then obtain P where "eventually P F" "SUPR (Collect P) f < a"
hoelzl@51340
   277
    unfolding Limsup_def INF_less_iff by auto
hoelzl@51340
   278
  then show "eventually (\<lambda>x. f x < a) F"
hoelzl@51340
   279
    by (auto elim!: eventually_elim1 dest: SUP_lessD)
hoelzl@51340
   280
next
hoelzl@51340
   281
  fix a assume "a < f0"
hoelzl@51340
   282
  with assms have "a < Liminf F f" by simp
hoelzl@51340
   283
  then obtain P where "eventually P F" "a < INFI (Collect P) f"
hoelzl@51340
   284
    unfolding Liminf_def less_SUP_iff by auto
hoelzl@51340
   285
  then show "eventually (\<lambda>x. a < f x) F"
hoelzl@51340
   286
    by (auto elim!: eventually_elim1 dest: less_INF_D)
hoelzl@51340
   287
qed
hoelzl@51340
   288
hoelzl@51340
   289
lemma tendsto_iff_Liminf_eq_Limsup:
hoelzl@51340
   290
  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
hoelzl@51340
   291
  shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
hoelzl@51340
   292
  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
hoelzl@51340
   293
hoelzl@51340
   294
lemma liminf_subseq_mono:
hoelzl@51340
   295
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
hoelzl@51340
   296
  assumes "subseq r"
hoelzl@51340
   297
  shows "liminf X \<le> liminf (X \<circ> r) "
hoelzl@51340
   298
proof-
hoelzl@51340
   299
  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
hoelzl@51340
   300
  proof (safe intro!: INF_mono)
hoelzl@51340
   301
    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
hoelzl@51340
   302
      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
hoelzl@51340
   303
  qed
hoelzl@51340
   304
  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
hoelzl@51340
   305
qed
hoelzl@51340
   306
hoelzl@51340
   307
lemma limsup_subseq_mono:
hoelzl@51340
   308
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
hoelzl@51340
   309
  assumes "subseq r"
hoelzl@51340
   310
  shows "limsup (X \<circ> r) \<le> limsup X"
hoelzl@51340
   311
proof-
hoelzl@51340
   312
  have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
hoelzl@51340
   313
  proof (safe intro!: SUP_mono)
hoelzl@51340
   314
    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
hoelzl@51340
   315
      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
hoelzl@51340
   316
  qed
hoelzl@51340
   317
  then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
hoelzl@51340
   318
qed
hoelzl@51340
   319
hoelzl@51340
   320
end