src/HOL/Library/Liminf_Limsup.thy
author hoelzl
Wed Mar 16 11:49:56 2016 +0100 (2016-03-16)
changeset 62624 59ceeb6f3079
parent 62343 24106dc44def
child 62975 1d066f6ab25d
permissions -rw-r--r--
generalized some Borel measurable statements to support ennreal
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:
hoelzl@62624
    23
  "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> SUPREMUM A f \<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}"
hoelzl@62624
    28
  shows "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> (SUP i: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}"
hoelzl@51340
    34
  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
    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:
hoelzl@62624
    49
  "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> INFIMUM A f \<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}"
hoelzl@62624
    54
  shows "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i: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}"
hoelzl@51340
    60
  shows "(INF i: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"
hoelzl@54257
    66
  shows "(SUP i : A. SUP j : B. f i j) = (SUP p : 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"
hoelzl@54257
    71
  shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
hoelzl@51340
    72
  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
hoelzl@51340
    73
wenzelm@61585
    74
subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
hoelzl@51340
    75
hoelzl@54261
    76
definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
hoelzl@51340
    77
  "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
hoelzl@51340
    78
hoelzl@54261
    79
definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
hoelzl@51340
    80
  "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
hoelzl@51340
    81
hoelzl@51340
    82
abbreviation "liminf \<equiv> Liminf sequentially"
hoelzl@51340
    83
hoelzl@51340
    84
abbreviation "limsup \<equiv> Limsup sequentially"
hoelzl@51340
    85
hoelzl@51340
    86
lemma Liminf_eqI:
wenzelm@61730
    87
  "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>
haftmann@56218
    88
    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
hoelzl@51340
    89
  unfolding Liminf_def by (auto intro!: SUP_eqI)
hoelzl@51340
    90
hoelzl@51340
    91
lemma Limsup_eqI:
wenzelm@61730
    92
  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>
haftmann@56218
    93
    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
hoelzl@51340
    94
  unfolding Limsup_def by (auto intro!: INF_eqI)
hoelzl@51340
    95
haftmann@56212
    96
lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)"
hoelzl@51340
    97
  unfolding Liminf_def eventually_sequentially
haftmann@56212
    98
  by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono)
hoelzl@51340
    99
haftmann@56212
   100
lemma limsup_INF_SUP: "limsup f = (INF n. SUP m:{n..}. f m)"
hoelzl@51340
   101
  unfolding Limsup_def eventually_sequentially
haftmann@56212
   102
  by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
hoelzl@51340
   103
wenzelm@61730
   104
lemma Limsup_const:
hoelzl@51340
   105
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@54261
   106
  shows "Limsup F (\<lambda>x. c) = c"
hoelzl@51340
   107
proof -
hoelzl@51340
   108
  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
hoelzl@51340
   109
  have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
hoelzl@51340
   110
    using ntriv by (intro SUP_const) (auto simp: eventually_False *)
hoelzl@51340
   111
  then show ?thesis
hoelzl@51340
   112
    unfolding Limsup_def using eventually_True
hoelzl@51340
   113
    by (subst INF_cong[where D="\<lambda>x. c"])
hoelzl@51340
   114
       (auto intro!: INF_const simp del: eventually_True)
hoelzl@51340
   115
qed
hoelzl@51340
   116
hoelzl@51340
   117
lemma Liminf_const:
hoelzl@51340
   118
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@54261
   119
  shows "Liminf F (\<lambda>x. c) = c"
hoelzl@51340
   120
proof -
hoelzl@51340
   121
  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
hoelzl@51340
   122
  have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
hoelzl@51340
   123
    using ntriv by (intro INF_const) (auto simp: eventually_False *)
hoelzl@51340
   124
  then show ?thesis
hoelzl@51340
   125
    unfolding Liminf_def using eventually_True
hoelzl@51340
   126
    by (subst SUP_cong[where D="\<lambda>x. c"])
hoelzl@51340
   127
       (auto intro!: SUP_const simp del: eventually_True)
hoelzl@51340
   128
qed
hoelzl@51340
   129
hoelzl@51340
   130
lemma Liminf_mono:
hoelzl@51340
   131
  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
hoelzl@51340
   132
  shows "Liminf F f \<le> Liminf F g"
hoelzl@51340
   133
  unfolding Liminf_def
hoelzl@51340
   134
proof (safe intro!: SUP_mono)
hoelzl@51340
   135
  fix P assume "eventually P F"
hoelzl@51340
   136
  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
haftmann@56218
   137
  then show "\<exists>Q\<in>{P. eventually P F}. INFIMUM (Collect P) f \<le> INFIMUM (Collect Q) g"
hoelzl@51340
   138
    by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
hoelzl@51340
   139
qed
hoelzl@51340
   140
hoelzl@51340
   141
lemma Liminf_eq:
hoelzl@51340
   142
  assumes "eventually (\<lambda>x. f x = g x) F"
hoelzl@51340
   143
  shows "Liminf F f = Liminf F g"
lp15@61810
   144
  by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
hoelzl@51340
   145
hoelzl@51340
   146
lemma Limsup_mono:
hoelzl@51340
   147
  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
hoelzl@51340
   148
  shows "Limsup F f \<le> Limsup F g"
hoelzl@51340
   149
  unfolding Limsup_def
hoelzl@51340
   150
proof (safe intro!: INF_mono)
hoelzl@51340
   151
  fix P assume "eventually P F"
hoelzl@51340
   152
  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
haftmann@56218
   153
  then show "\<exists>Q\<in>{P. eventually P F}. SUPREMUM (Collect Q) f \<le> SUPREMUM (Collect P) g"
hoelzl@51340
   154
    by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
hoelzl@51340
   155
qed
hoelzl@51340
   156
hoelzl@51340
   157
lemma Limsup_eq:
hoelzl@51340
   158
  assumes "eventually (\<lambda>x. f x = g x) net"
hoelzl@51340
   159
  shows "Limsup net f = Limsup net g"
lp15@61810
   160
  by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
hoelzl@51340
   161
hoelzl@51340
   162
lemma Liminf_le_Limsup:
hoelzl@51340
   163
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   164
  shows "Liminf F f \<le> Limsup F f"
hoelzl@51340
   165
  unfolding Limsup_def Liminf_def
hoelzl@54261
   166
  apply (rule SUP_least)
hoelzl@54261
   167
  apply (rule INF_greatest)
hoelzl@51340
   168
proof safe
hoelzl@51340
   169
  fix P Q assume "eventually P F" "eventually Q F"
hoelzl@51340
   170
  then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
hoelzl@51340
   171
  then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
hoelzl@51340
   172
    using ntriv by (auto simp add: eventually_False)
haftmann@56218
   173
  have "INFIMUM (Collect P) f \<le> INFIMUM (Collect ?C) f"
hoelzl@51340
   174
    by (rule INF_mono) auto
haftmann@56218
   175
  also have "\<dots> \<le> SUPREMUM (Collect ?C) f"
hoelzl@51340
   176
    using not_False by (intro INF_le_SUP) auto
haftmann@56218
   177
  also have "\<dots> \<le> SUPREMUM (Collect Q) f"
hoelzl@51340
   178
    by (rule SUP_mono) auto
haftmann@56218
   179
  finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" .
hoelzl@51340
   180
qed
hoelzl@51340
   181
hoelzl@51340
   182
lemma Liminf_bounded:
hoelzl@51340
   183
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   184
  assumes le: "eventually (\<lambda>n. C \<le> X n) F"
hoelzl@51340
   185
  shows "C \<le> Liminf F X"
hoelzl@51340
   186
  using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
hoelzl@51340
   187
hoelzl@51340
   188
lemma Limsup_bounded:
hoelzl@51340
   189
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   190
  assumes le: "eventually (\<lambda>n. X n \<le> C) F"
hoelzl@51340
   191
  shows "Limsup F X \<le> C"
hoelzl@51340
   192
  using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
hoelzl@51340
   193
hoelzl@61245
   194
lemma le_Limsup:
hoelzl@61245
   195
  assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
hoelzl@61245
   196
  shows "l \<le> Limsup F f"
hoelzl@61245
   197
proof -
hoelzl@61245
   198
  have "l = Limsup F (\<lambda>x. l)"
hoelzl@61245
   199
    using F by (simp add: Limsup_const)
hoelzl@61245
   200
  also have "\<dots> \<le> Limsup F f"
wenzelm@61730
   201
    by (intro Limsup_mono x)
hoelzl@61245
   202
  finally show ?thesis .
hoelzl@61245
   203
qed
hoelzl@61245
   204
hoelzl@51340
   205
lemma le_Liminf_iff:
hoelzl@51340
   206
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
hoelzl@51340
   207
  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
hoelzl@51340
   208
proof -
wenzelm@61730
   209
  have "eventually (\<lambda>x. y < X x) F"
wenzelm@61730
   210
    if "eventually P F" "y < INFIMUM (Collect P) X" for y P
lp15@61810
   211
    using that by (auto elim!: eventually_mono dest: less_INF_D)
hoelzl@51340
   212
  moreover
wenzelm@61730
   213
  have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
wenzelm@61730
   214
    if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
wenzelm@61730
   215
  proof (cases "\<exists>z. y < z \<and> z < C")
wenzelm@61730
   216
    case True
wenzelm@61730
   217
    then obtain z where z: "y < z \<and> z < C" ..
wenzelm@61730
   218
    moreover from z have "z \<le> INFIMUM {x. z < X x} X"
wenzelm@61730
   219
      by (auto intro!: INF_greatest)
wenzelm@61730
   220
    ultimately show ?thesis
wenzelm@61730
   221
      using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
wenzelm@61730
   222
  next
wenzelm@61730
   223
    case False
wenzelm@61730
   224
    then have "C \<le> INFIMUM {x. y < X x} X"
wenzelm@61730
   225
      by (intro INF_greatest) auto
wenzelm@61730
   226
    with \<open>y < C\<close> show ?thesis
wenzelm@61730
   227
      using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
wenzelm@61730
   228
  qed
hoelzl@51340
   229
  ultimately show ?thesis
hoelzl@51340
   230
    unfolding Liminf_def le_SUP_iff by auto
hoelzl@51340
   231
qed
hoelzl@51340
   232
eberlm@62049
   233
lemma Limsup_le_iff:
eberlm@62049
   234
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
eberlm@62049
   235
  shows "C \<ge> Limsup F X \<longleftrightarrow> (\<forall>y>C. eventually (\<lambda>x. y > X x) F)"
eberlm@62049
   236
proof -
eberlm@62049
   237
  { fix y P assume "eventually P F" "y > SUPREMUM (Collect P) X"
eberlm@62049
   238
    then have "eventually (\<lambda>x. y > X x) F"
eberlm@62049
   239
      by (auto elim!: eventually_mono dest: SUP_lessD) }
eberlm@62049
   240
  moreover
eberlm@62049
   241
  { fix y P assume "y > C" and y: "\<forall>y>C. eventually (\<lambda>x. y > X x) F"
eberlm@62049
   242
    have "\<exists>P. eventually P F \<and> y > SUPREMUM (Collect P) X"
eberlm@62049
   243
    proof (cases "\<exists>z. C < z \<and> z < y")
eberlm@62049
   244
      case True
eberlm@62049
   245
      then obtain z where z: "C < z \<and> z < y" ..
eberlm@62049
   246
      moreover from z have "z \<ge> SUPREMUM {x. z > X x} X"
eberlm@62049
   247
        by (auto intro!: SUP_least)
eberlm@62049
   248
      ultimately show ?thesis
eberlm@62049
   249
        using y by (intro exI[of _ "\<lambda>x. z > X x"]) auto
eberlm@62049
   250
    next
eberlm@62049
   251
      case False
eberlm@62049
   252
      then have "C \<ge> SUPREMUM {x. y > X x} X"
eberlm@62049
   253
        by (intro SUP_least) (auto simp: not_less)
eberlm@62049
   254
      with \<open>y > C\<close> show ?thesis
eberlm@62049
   255
        using y by (intro exI[of _ "\<lambda>x. y > X x"]) auto
eberlm@62049
   256
    qed }
eberlm@62049
   257
  ultimately show ?thesis
eberlm@62049
   258
    unfolding Limsup_def INF_le_iff by auto
eberlm@62049
   259
qed
eberlm@62049
   260
eberlm@62049
   261
lemma less_LiminfD:
eberlm@62049
   262
  "y < Liminf F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x > y) F"
eberlm@62049
   263
  using le_Liminf_iff[of "Liminf F f" F f] by simp
eberlm@62049
   264
eberlm@62049
   265
lemma Limsup_lessD:
eberlm@62049
   266
  "y > Limsup F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x < y) F"
eberlm@62049
   267
  using Limsup_le_iff[of F f "Limsup F f"] by simp
eberlm@62049
   268
hoelzl@51340
   269
lemma lim_imp_Liminf:
wenzelm@61730
   270
  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
hoelzl@51340
   271
  assumes ntriv: "\<not> trivial_limit F"
wenzelm@61973
   272
  assumes lim: "(f \<longlongrightarrow> f0) F"
hoelzl@51340
   273
  shows "Liminf F f = f0"
hoelzl@51340
   274
proof (intro Liminf_eqI)
hoelzl@51340
   275
  fix P assume P: "eventually P F"
haftmann@56218
   276
  then have "eventually (\<lambda>x. INFIMUM (Collect P) f \<le> f x) F"
hoelzl@51340
   277
    by eventually_elim (auto intro!: INF_lower)
haftmann@56218
   278
  then show "INFIMUM (Collect P) f \<le> f0"
hoelzl@51340
   279
    by (rule tendsto_le[OF ntriv lim tendsto_const])
hoelzl@51340
   280
next
haftmann@56218
   281
  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y"
hoelzl@51340
   282
  show "f0 \<le> y"
hoelzl@51340
   283
  proof cases
hoelzl@51340
   284
    assume "\<exists>z. y < z \<and> z < f0"
wenzelm@53374
   285
    then obtain z where "y < z \<and> z < f0" ..
haftmann@56218
   286
    moreover have "z \<le> INFIMUM {x. z < f x} f"
hoelzl@51340
   287
      by (rule INF_greatest) simp
hoelzl@51340
   288
    ultimately show ?thesis
hoelzl@51340
   289
      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
hoelzl@51340
   290
  next
hoelzl@51340
   291
    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
hoelzl@51340
   292
    show ?thesis
hoelzl@51340
   293
    proof (rule classical)
hoelzl@51340
   294
      assume "\<not> f0 \<le> y"
hoelzl@51340
   295
      then have "eventually (\<lambda>x. y < f x) F"
hoelzl@51340
   296
        using lim[THEN topological_tendstoD, of "{y <..}"] by auto
hoelzl@51340
   297
      then have "eventually (\<lambda>x. f0 \<le> f x) F"
lp15@61810
   298
        using discrete by (auto elim!: eventually_mono)
haftmann@56218
   299
      then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
hoelzl@51340
   300
        by (rule upper)
haftmann@56218
   301
      moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
hoelzl@51340
   302
        by (intro INF_greatest) simp
hoelzl@51340
   303
      ultimately show "f0 \<le> y" by simp
hoelzl@51340
   304
    qed
hoelzl@51340
   305
  qed
hoelzl@51340
   306
qed
hoelzl@51340
   307
hoelzl@51340
   308
lemma lim_imp_Limsup:
wenzelm@61730
   309
  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
hoelzl@51340
   310
  assumes ntriv: "\<not> trivial_limit F"
wenzelm@61973
   311
  assumes lim: "(f \<longlongrightarrow> f0) F"
hoelzl@51340
   312
  shows "Limsup F f = f0"
hoelzl@51340
   313
proof (intro Limsup_eqI)
hoelzl@51340
   314
  fix P assume P: "eventually P F"
haftmann@56218
   315
  then have "eventually (\<lambda>x. f x \<le> SUPREMUM (Collect P) f) F"
hoelzl@51340
   316
    by eventually_elim (auto intro!: SUP_upper)
haftmann@56218
   317
  then show "f0 \<le> SUPREMUM (Collect P) f"
hoelzl@51340
   318
    by (rule tendsto_le[OF ntriv tendsto_const lim])
hoelzl@51340
   319
next
haftmann@56218
   320
  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f"
hoelzl@51340
   321
  show "y \<le> f0"
wenzelm@53381
   322
  proof (cases "\<exists>z. f0 < z \<and> z < y")
wenzelm@53381
   323
    case True
wenzelm@53381
   324
    then obtain z where "f0 < z \<and> z < y" ..
haftmann@56218
   325
    moreover have "SUPREMUM {x. f x < z} f \<le> z"
hoelzl@51340
   326
      by (rule SUP_least) simp
hoelzl@51340
   327
    ultimately show ?thesis
hoelzl@51340
   328
      using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
hoelzl@51340
   329
  next
wenzelm@53381
   330
    case False
hoelzl@51340
   331
    show ?thesis
hoelzl@51340
   332
    proof (rule classical)
hoelzl@51340
   333
      assume "\<not> y \<le> f0"
hoelzl@51340
   334
      then have "eventually (\<lambda>x. f x < y) F"
hoelzl@51340
   335
        using lim[THEN topological_tendstoD, of "{..< y}"] by auto
hoelzl@51340
   336
      then have "eventually (\<lambda>x. f x \<le> f0) F"
lp15@61810
   337
        using False by (auto elim!: eventually_mono simp: not_less)
haftmann@56218
   338
      then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
hoelzl@51340
   339
        by (rule lower)
haftmann@56218
   340
      moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
hoelzl@51340
   341
        by (intro SUP_least) simp
hoelzl@51340
   342
      ultimately show "y \<le> f0" by simp
hoelzl@51340
   343
    qed
hoelzl@51340
   344
  qed
hoelzl@51340
   345
qed
hoelzl@51340
   346
hoelzl@51340
   347
lemma Liminf_eq_Limsup:
wenzelm@61730
   348
  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
hoelzl@51340
   349
  assumes ntriv: "\<not> trivial_limit F"
hoelzl@51340
   350
    and lim: "Liminf F f = f0" "Limsup F f = f0"
wenzelm@61973
   351
  shows "(f \<longlongrightarrow> f0) F"
hoelzl@51340
   352
proof (rule order_tendstoI)
hoelzl@51340
   353
  fix a assume "f0 < a"
hoelzl@51340
   354
  with assms have "Limsup F f < a" by simp
haftmann@56218
   355
  then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
hoelzl@51340
   356
    unfolding Limsup_def INF_less_iff by auto
hoelzl@51340
   357
  then show "eventually (\<lambda>x. f x < a) F"
lp15@61810
   358
    by (auto elim!: eventually_mono dest: SUP_lessD)
hoelzl@51340
   359
next
hoelzl@51340
   360
  fix a assume "a < f0"
hoelzl@51340
   361
  with assms have "a < Liminf F f" by simp
haftmann@56218
   362
  then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
hoelzl@51340
   363
    unfolding Liminf_def less_SUP_iff by auto
hoelzl@51340
   364
  then show "eventually (\<lambda>x. a < f x) F"
lp15@61810
   365
    by (auto elim!: eventually_mono dest: less_INF_D)
hoelzl@51340
   366
qed
hoelzl@51340
   367
hoelzl@51340
   368
lemma tendsto_iff_Liminf_eq_Limsup:
wenzelm@61730
   369
  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
wenzelm@61973
   370
  shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
hoelzl@51340
   371
  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
hoelzl@51340
   372
hoelzl@51340
   373
lemma liminf_subseq_mono:
hoelzl@51340
   374
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
hoelzl@51340
   375
  assumes "subseq r"
hoelzl@51340
   376
  shows "liminf X \<le> liminf (X \<circ> r) "
hoelzl@51340
   377
proof-
hoelzl@51340
   378
  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
hoelzl@51340
   379
  proof (safe intro!: INF_mono)
hoelzl@51340
   380
    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
wenzelm@60500
   381
      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
hoelzl@51340
   382
  qed
haftmann@56212
   383
  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
hoelzl@51340
   384
qed
hoelzl@51340
   385
hoelzl@51340
   386
lemma limsup_subseq_mono:
hoelzl@51340
   387
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
hoelzl@51340
   388
  assumes "subseq r"
hoelzl@51340
   389
  shows "limsup (X \<circ> r) \<le> limsup X"
hoelzl@51340
   390
proof-
wenzelm@61730
   391
  have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
hoelzl@51340
   392
  proof (safe intro!: SUP_mono)
wenzelm@61730
   393
    fix m :: nat
wenzelm@61730
   394
    assume "n \<le> m"
wenzelm@61730
   395
    then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
wenzelm@60500
   396
      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
hoelzl@51340
   397
  qed
wenzelm@61730
   398
  then show ?thesis
wenzelm@61730
   399
    by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
hoelzl@51340
   400
qed
hoelzl@51340
   401
wenzelm@61730
   402
lemma continuous_on_imp_continuous_within:
wenzelm@61730
   403
  "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
wenzelm@61730
   404
  unfolding continuous_on_eq_continuous_within
wenzelm@61730
   405
  by (auto simp: continuous_within intro: tendsto_within_subset)
hoelzl@61245
   406
eberlm@62049
   407
lemma Liminf_compose_continuous_mono:
eberlm@62049
   408
  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
eberlm@62049
   409
  assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot"
eberlm@62049
   410
  shows "Liminf F (\<lambda>n. f (g n)) = f (Liminf F g)"
eberlm@62049
   411
proof -
eberlm@62049
   412
  { fix P assume "eventually P F"
eberlm@62049
   413
    have "\<exists>x. P x"
eberlm@62049
   414
    proof (rule ccontr)
eberlm@62049
   415
      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
eberlm@62049
   416
        by auto
eberlm@62049
   417
      with \<open>eventually P F\<close> F show False
eberlm@62049
   418
        by auto
eberlm@62049
   419
    qed }
eberlm@62049
   420
  note * = this
eberlm@62049
   421
eberlm@62049
   422
  have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))"
haftmann@62343
   423
    unfolding Liminf_def
eberlm@62049
   424
    by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
eberlm@62049
   425
       (auto intro: eventually_True)
eberlm@62049
   426
  also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
eberlm@62049
   427
    by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
eberlm@62049
   428
       (auto dest!: eventually_happens simp: F)
eberlm@62049
   429
  finally show ?thesis by (auto simp: Liminf_def)
eberlm@62049
   430
qed
eberlm@62049
   431
eberlm@62049
   432
lemma Limsup_compose_continuous_mono:
eberlm@62049
   433
  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
eberlm@62049
   434
  assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot"
eberlm@62049
   435
  shows "Limsup F (\<lambda>n. f (g n)) = f (Limsup F g)"
eberlm@62049
   436
proof -
eberlm@62049
   437
  { fix P assume "eventually P F"
eberlm@62049
   438
    have "\<exists>x. P x"
eberlm@62049
   439
    proof (rule ccontr)
eberlm@62049
   440
      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
eberlm@62049
   441
        by auto
eberlm@62049
   442
      with \<open>eventually P F\<close> F show False
eberlm@62049
   443
        by auto
eberlm@62049
   444
    qed }
eberlm@62049
   445
  note * = this
eberlm@62049
   446
eberlm@62049
   447
  have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))"
haftmann@62343
   448
    unfolding Limsup_def
eberlm@62049
   449
    by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
eberlm@62049
   450
       (auto intro: eventually_True)
eberlm@62049
   451
  also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
eberlm@62049
   452
    by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
eberlm@62049
   453
       (auto dest!: eventually_happens simp: F)
eberlm@62049
   454
  finally show ?thesis by (auto simp: Limsup_def)
eberlm@62049
   455
qed
eberlm@62049
   456
hoelzl@61245
   457
lemma Liminf_compose_continuous_antimono:
wenzelm@61730
   458
  fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}"
wenzelm@61730
   459
  assumes c: "continuous_on UNIV f"
wenzelm@61730
   460
    and am: "antimono f"
wenzelm@61730
   461
    and F: "F \<noteq> bot"
hoelzl@61245
   462
  shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
hoelzl@61245
   463
proof -
wenzelm@61730
   464
  have *: "\<exists>x. P x" if "eventually P F" for P
wenzelm@61730
   465
  proof (rule ccontr)
wenzelm@61730
   466
    assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
wenzelm@61730
   467
      by auto
wenzelm@61730
   468
    with \<open>eventually P F\<close> F show False
wenzelm@61730
   469
      by auto
wenzelm@61730
   470
  qed
hoelzl@61245
   471
  have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
haftmann@62343
   472
    unfolding Limsup_def
hoelzl@61245
   473
    by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
hoelzl@61245
   474
       (auto intro: eventually_True)
hoelzl@61245
   475
  also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
hoelzl@61245
   476
    by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
hoelzl@61245
   477
       (auto dest!: eventually_happens simp: F)
hoelzl@61245
   478
  finally show ?thesis
hoelzl@61245
   479
    by (auto simp: Liminf_def)
hoelzl@61245
   480
qed
eberlm@62049
   481
eberlm@62049
   482
lemma Limsup_compose_continuous_antimono:
eberlm@62049
   483
  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
eberlm@62049
   484
  assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot"
eberlm@62049
   485
  shows "Limsup F (\<lambda>n. f (g n)) = f (Liminf F g)"
eberlm@62049
   486
proof -
eberlm@62049
   487
  { fix P assume "eventually P F"
eberlm@62049
   488
    have "\<exists>x. P x"
eberlm@62049
   489
    proof (rule ccontr)
eberlm@62049
   490
      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
eberlm@62049
   491
        by auto
eberlm@62049
   492
      with \<open>eventually P F\<close> F show False
eberlm@62049
   493
        by auto
eberlm@62049
   494
    qed }
eberlm@62049
   495
  note * = this
eberlm@62049
   496
eberlm@62049
   497
  have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))"
haftmann@62343
   498
    unfolding Liminf_def
eberlm@62049
   499
    by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
eberlm@62049
   500
       (auto intro: eventually_True)
eberlm@62049
   501
  also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
eberlm@62049
   502
    by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
eberlm@62049
   503
       (auto dest!: eventually_happens simp: F)
eberlm@62049
   504
  finally show ?thesis
eberlm@62049
   505
    by (auto simp: Limsup_def)
eberlm@62049
   506
qed
eberlm@62049
   507
eberlm@62049
   508
hoelzl@61880
   509
subsection \<open>More Limits\<close>
hoelzl@61880
   510
hoelzl@61880
   511
lemma convergent_limsup_cl:
hoelzl@61880
   512
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
hoelzl@61880
   513
  shows "convergent X \<Longrightarrow> limsup X = lim X"
hoelzl@61880
   514
  by (auto simp: convergent_def limI lim_imp_Limsup)
hoelzl@61880
   515
hoelzl@61880
   516
lemma convergent_liminf_cl:
hoelzl@61880
   517
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
hoelzl@61880
   518
  shows "convergent X \<Longrightarrow> liminf X = lim X"
hoelzl@61880
   519
  by (auto simp: convergent_def limI lim_imp_Liminf)
hoelzl@61880
   520
hoelzl@61880
   521
lemma lim_increasing_cl:
hoelzl@61880
   522
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
wenzelm@61969
   523
  obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
hoelzl@61880
   524
proof
wenzelm@61969
   525
  show "f \<longlonglongrightarrow> (SUP n. f n)"
hoelzl@61880
   526
    using assms
hoelzl@61880
   527
    by (intro increasing_tendsto)
hoelzl@61880
   528
       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
hoelzl@61880
   529
qed
hoelzl@61880
   530
hoelzl@61880
   531
lemma lim_decreasing_cl:
hoelzl@61880
   532
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
wenzelm@61969
   533
  obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
hoelzl@61880
   534
proof
wenzelm@61969
   535
  show "f \<longlonglongrightarrow> (INF n. f n)"
hoelzl@61880
   536
    using assms
hoelzl@61880
   537
    by (intro decreasing_tendsto)
hoelzl@61880
   538
       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
hoelzl@61880
   539
qed
hoelzl@61880
   540
hoelzl@61880
   541
lemma compact_complete_linorder:
hoelzl@61880
   542
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
wenzelm@61969
   543
  shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
hoelzl@61880
   544
proof -
hoelzl@61880
   545
  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
hoelzl@61880
   546
    using seq_monosub[of X]
hoelzl@61880
   547
    unfolding comp_def
hoelzl@61880
   548
    by auto
hoelzl@61880
   549
  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
   550
    by (auto simp add: monoseq_def)
wenzelm@61969
   551
  then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"
hoelzl@61880
   552
     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
hoelzl@61880
   553
     by auto
hoelzl@61880
   554
  then show ?thesis
hoelzl@61880
   555
    using \<open>subseq r\<close> by auto
hoelzl@61880
   556
qed
hoelzl@61245
   557
hoelzl@51340
   558
end