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