/
monotone_convergence.lean
317 lines (245 loc) · 13.5 KB
/
monotone_convergence.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
/-
Copyright (c) 2021 Heather Macbeth. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Heather Macbeth, Yury Kudryashov
-/
import topology.order.basic
/-!
# Bounded monotone sequences converge
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
In this file we prove a few theorems of the form “if the range of a monotone function `f : ι → α`
admits a least upper bound `a`, then `f x` tends to `a` as `x → ∞`”, as well as version of this
statement for (conditionally) complete lattices that use `⨆ x, f x` instead of `is_lub`.
These theorems work for linear orders with order topologies as well as their products (both in terms
of `prod` and in terms of function types). In order to reduce code duplication, we introduce two
typeclasses (one for the property formulated above and one for the dual property), prove theorems
assuming one of these typeclasses, and provide instances for linear orders and their products.
We also prove some "inverse" results: if `f n` is a monotone sequence and `a` is its limit,
then `f n ≤ a` for all `n`.
## Tags
monotone convergence
-/
open filter set function
open_locale filter topology classical
variables {α β : Type*}
/-- We say that `α` is a `Sup_convergence_class` if the following holds. Let `f : ι → α` be a
monotone function, let `a : α` be a least upper bound of `set.range f`. Then `f x` tends to `𝓝 a` as
`x → ∞` (formally, at the filter `filter.at_top`). We require this for `ι = (s : set α)`, `f = coe`
in the definition, then prove it for any `f` in `tendsto_at_top_is_lub`.
This property holds for linear orders with order topology as well as their products. -/
class Sup_convergence_class (α : Type*) [preorder α] [topological_space α] : Prop :=
(tendsto_coe_at_top_is_lub : ∀ (a : α) (s : set α), is_lub s a → tendsto (coe : s → α) at_top (𝓝 a))
/-- We say that `α` is an `Inf_convergence_class` if the following holds. Let `f : ι → α` be a
monotone function, let `a : α` be a greatest lower bound of `set.range f`. Then `f x` tends to `𝓝 a`
as `x → -∞` (formally, at the filter `filter.at_bot`). We require this for `ι = (s : set α)`,
`f = coe` in the definition, then prove it for any `f` in `tendsto_at_bot_is_glb`.
This property holds for linear orders with order topology as well as their products. -/
class Inf_convergence_class (α : Type*) [preorder α] [topological_space α] : Prop :=
(tendsto_coe_at_bot_is_glb : ∀ (a : α) (s : set α), is_glb s a → tendsto (coe : s → α) at_bot (𝓝 a))
instance order_dual.Sup_convergence_class [preorder α] [topological_space α]
[Inf_convergence_class α] : Sup_convergence_class αᵒᵈ :=
⟨‹Inf_convergence_class α›.1⟩
instance order_dual.Inf_convergence_class [preorder α] [topological_space α]
[Sup_convergence_class α] : Inf_convergence_class αᵒᵈ :=
⟨‹Sup_convergence_class α›.1⟩
@[priority 100] -- see Note [lower instance priority]
instance linear_order.Sup_convergence_class [topological_space α] [linear_order α]
[order_topology α] : Sup_convergence_class α :=
begin
refine ⟨λ a s ha, tendsto_order.2 ⟨λ b hb, _, λ b hb, _⟩⟩,
{ rcases ha.exists_between hb with ⟨c, hcs, bc, bca⟩,
lift c to s using hcs,
refine (eventually_ge_at_top c).mono (λ x hx, bc.trans_le hx) },
{ exact eventually_of_forall (λ x, (ha.1 x.2).trans_lt hb) }
end
@[priority 100] -- see Note [lower instance priority]
instance linear_order.Inf_convergence_class [topological_space α] [linear_order α]
[order_topology α] : Inf_convergence_class α :=
show Inf_convergence_class αᵒᵈᵒᵈ, from order_dual.Inf_convergence_class
section
variables {ι : Type*} [preorder ι] [topological_space α]
section is_lub
variables [preorder α] [Sup_convergence_class α] {f : ι → α} {a : α}
lemma tendsto_at_top_is_lub (h_mono : monotone f) (ha : is_lub (set.range f) a) :
tendsto f at_top (𝓝 a) :=
begin
suffices : tendsto (range_factorization f) at_top at_top,
from (Sup_convergence_class.tendsto_coe_at_top_is_lub _ _ ha).comp this,
exact h_mono.range_factorization.tendsto_at_top_at_top (λ b, b.2.imp $ λ a ha, ha.ge)
end
lemma tendsto_at_bot_is_lub (h_anti : antitone f) (ha : is_lub (set.range f) a) :
tendsto f at_bot (𝓝 a) :=
by convert tendsto_at_top_is_lub h_anti.dual_left ha
end is_lub
section is_glb
variables [preorder α] [Inf_convergence_class α] {f : ι → α} {a : α}
lemma tendsto_at_bot_is_glb (h_mono : monotone f) (ha : is_glb (set.range f) a) :
tendsto f at_bot (𝓝 a) :=
by convert tendsto_at_top_is_lub h_mono.dual ha.dual
lemma tendsto_at_top_is_glb (h_anti : antitone f) (ha : is_glb (set.range f) a) :
tendsto f at_top (𝓝 a) :=
by convert tendsto_at_bot_is_lub h_anti.dual ha.dual
end is_glb
section csupr
variables [conditionally_complete_lattice α] [Sup_convergence_class α] {f : ι → α} {a : α}
lemma tendsto_at_top_csupr (h_mono : monotone f) (hbdd : bdd_above $ range f) :
tendsto f at_top (𝓝 (⨆i, f i)) :=
begin
casesI is_empty_or_nonempty ι,
exacts [tendsto_of_is_empty, tendsto_at_top_is_lub h_mono (is_lub_csupr hbdd)]
end
lemma tendsto_at_bot_csupr (h_anti : antitone f) (hbdd : bdd_above $ range f) :
tendsto f at_bot (𝓝 (⨆ i, f i)) :=
by convert tendsto_at_top_csupr h_anti.dual hbdd.dual
end csupr
section cinfi
variables [conditionally_complete_lattice α] [Inf_convergence_class α] {f : ι → α} {a : α}
lemma tendsto_at_bot_cinfi (h_mono : monotone f) (hbdd : bdd_below $ range f) :
tendsto f at_bot (𝓝 (⨅ i, f i)) :=
by convert tendsto_at_top_csupr h_mono.dual hbdd.dual
lemma tendsto_at_top_cinfi (h_anti : antitone f) (hbdd : bdd_below $ range f) :
tendsto f at_top (𝓝 (⨅ i, f i)) :=
by convert tendsto_at_bot_csupr h_anti.dual hbdd.dual
end cinfi
section supr
variables [complete_lattice α] [Sup_convergence_class α] {f : ι → α} {a : α}
lemma tendsto_at_top_supr (h_mono : monotone f) : tendsto f at_top (𝓝 (⨆i, f i)) :=
tendsto_at_top_csupr h_mono (order_top.bdd_above _)
lemma tendsto_at_bot_supr (h_anti : antitone f) :
tendsto f at_bot (𝓝 (⨆i, f i)) :=
tendsto_at_bot_csupr h_anti (order_top.bdd_above _)
end supr
section infi
variables [complete_lattice α] [Inf_convergence_class α] {f : ι → α} {a : α}
lemma tendsto_at_bot_infi (h_mono : monotone f) : tendsto f at_bot (𝓝 (⨅i, f i)) :=
tendsto_at_bot_cinfi h_mono (order_bot.bdd_below _)
lemma tendsto_at_top_infi (h_anti : antitone f) :
tendsto f at_top (𝓝 (⨅i, f i)) :=
tendsto_at_top_cinfi h_anti (order_bot.bdd_below _)
end infi
end
instance [preorder α] [preorder β] [topological_space α] [topological_space β]
[Sup_convergence_class α] [Sup_convergence_class β] : Sup_convergence_class (α × β) :=
begin
constructor,
rintro ⟨a, b⟩ s h,
rw [is_lub_prod, ← range_restrict, ← range_restrict] at h,
have A : tendsto (λ x : s, (x : α × β).1) at_top (𝓝 a),
from tendsto_at_top_is_lub (monotone_fst.restrict s) h.1,
have B : tendsto (λ x : s, (x : α × β).2) at_top (𝓝 b),
from tendsto_at_top_is_lub (monotone_snd.restrict s) h.2,
convert A.prod_mk_nhds B,
ext1 ⟨⟨x, y⟩, h⟩, refl
end
instance [preorder α] [preorder β] [topological_space α] [topological_space β]
[Inf_convergence_class α] [Inf_convergence_class β] : Inf_convergence_class (α × β) :=
show Inf_convergence_class (αᵒᵈ × βᵒᵈ)ᵒᵈ, from order_dual.Inf_convergence_class
instance {ι : Type*} {α : ι → Type*} [Π i, preorder (α i)] [Π i, topological_space (α i)]
[Π i, Sup_convergence_class (α i)] : Sup_convergence_class (Π i, α i) :=
begin
refine ⟨λ f s h, _⟩,
simp only [is_lub_pi, ← range_restrict] at h,
exact tendsto_pi_nhds.2 (λ i, tendsto_at_top_is_lub ((monotone_eval _).restrict _) (h i))
end
instance {ι : Type*} {α : ι → Type*} [Π i, preorder (α i)] [Π i, topological_space (α i)]
[Π i, Inf_convergence_class (α i)] : Inf_convergence_class (Π i, α i) :=
show Inf_convergence_class (Π i, (α i)ᵒᵈ)ᵒᵈ, from order_dual.Inf_convergence_class
instance pi.Sup_convergence_class' {ι : Type*} [preorder α] [topological_space α]
[Sup_convergence_class α] : Sup_convergence_class (ι → α) :=
pi.Sup_convergence_class
instance pi.Inf_convergence_class' {ι : Type*} [preorder α] [topological_space α]
[Inf_convergence_class α] : Inf_convergence_class (ι → α) :=
pi.Inf_convergence_class
lemma tendsto_of_monotone {ι α : Type*} [preorder ι] [topological_space α]
[conditionally_complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) :
tendsto f at_top at_top ∨ (∃ l, tendsto f at_top (𝓝 l)) :=
if H : bdd_above (range f) then or.inr ⟨_, tendsto_at_top_csupr h_mono H⟩
else or.inl $ tendsto_at_top_at_top_of_monotone' h_mono H
lemma tendsto_iff_tendsto_subseq_of_monotone {ι₁ ι₂ α : Type*} [semilattice_sup ι₁] [preorder ι₂]
[nonempty ι₁] [topological_space α] [conditionally_complete_linear_order α] [order_topology α]
[no_max_order α] {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α} (hf : monotone f)
(hg : tendsto φ at_top at_top) :
tendsto f at_top (𝓝 l) ↔ tendsto (f ∘ φ) at_top (𝓝 l) :=
begin
split; intro h,
{ exact h.comp hg },
{ rcases tendsto_of_monotone hf with h' | ⟨l', hl'⟩,
{ exact (not_tendsto_at_top_of_tendsto_nhds h (h'.comp hg)).elim },
{ rwa tendsto_nhds_unique h (hl'.comp hg) } }
end
/-! The next family of results, such as `is_lub_of_tendsto_at_top` and `supr_eq_of_tendsto`, are
converses to the standard fact that bounded monotone functions converge. They state, that if a
monotone function `f` tends to `a` along `filter.at_top`, then that value `a` is a least upper bound
for the range of `f`.
Related theorems above (`is_lub.is_lub_of_tendsto`, `is_glb.is_glb_of_tendsto` etc) cover the case
when `f x` tends to `a` as `x` tends to some point `b` in the domain. -/
lemma monotone.ge_of_tendsto [topological_space α] [preorder α] [order_closed_topology α]
[semilattice_sup β] {f : β → α} {a : α} (hf : monotone f)
(ha : tendsto f at_top (𝓝 a)) (b : β) :
f b ≤ a :=
begin
haveI : nonempty β := nonempty.intro b,
exact ge_of_tendsto ha ((eventually_ge_at_top b).mono (λ _ hxy, hf hxy))
end
lemma monotone.le_of_tendsto [topological_space α] [preorder α] [order_closed_topology α]
[semilattice_inf β] {f : β → α} {a : α} (hf : monotone f)
(ha : tendsto f at_bot (𝓝 a)) (b : β) :
a ≤ f b :=
hf.dual.ge_of_tendsto ha b
lemma antitone.le_of_tendsto [topological_space α] [preorder α] [order_closed_topology α]
[semilattice_sup β] {f : β → α} {a : α} (hf : antitone f)
(ha : tendsto f at_top (𝓝 a)) (b : β) :
a ≤ f b :=
hf.dual_right.ge_of_tendsto ha b
lemma antitone.ge_of_tendsto [topological_space α] [preorder α] [order_closed_topology α]
[semilattice_inf β] {f : β → α} {a : α} (hf : antitone f)
(ha : tendsto f at_bot (𝓝 a)) (b : β) :
f b ≤ a :=
hf.dual_right.le_of_tendsto ha b
lemma is_lub_of_tendsto_at_top [topological_space α] [preorder α] [order_closed_topology α]
[nonempty β] [semilattice_sup β] {f : β → α} {a : α} (hf : monotone f)
(ha : tendsto f at_top (𝓝 a)) :
is_lub (set.range f) a :=
begin
split,
{ rintros _ ⟨b, rfl⟩,
exact hf.ge_of_tendsto ha b },
{ exact λ _ hb, le_of_tendsto' ha (λ x, hb (set.mem_range_self x)) }
end
lemma is_glb_of_tendsto_at_bot [topological_space α] [preorder α] [order_closed_topology α]
[nonempty β] [semilattice_inf β] {f : β → α} {a : α} (hf : monotone f)
(ha : tendsto f at_bot (𝓝 a)) :
is_glb (set.range f) a :=
@is_lub_of_tendsto_at_top αᵒᵈ βᵒᵈ _ _ _ _ _ _ _ hf.dual ha
lemma is_lub_of_tendsto_at_bot [topological_space α] [preorder α] [order_closed_topology α]
[nonempty β] [semilattice_inf β] {f : β → α} {a : α} (hf : antitone f)
(ha : tendsto f at_bot (𝓝 a)) :
is_lub (set.range f) a :=
@is_lub_of_tendsto_at_top α βᵒᵈ _ _ _ _ _ _ _ hf.dual_left ha
lemma is_glb_of_tendsto_at_top [topological_space α] [preorder α] [order_closed_topology α]
[nonempty β] [semilattice_sup β] {f : β → α} {a : α} (hf : antitone f)
(ha : tendsto f at_top (𝓝 a)) :
is_glb (set.range f) a :=
@is_glb_of_tendsto_at_bot α βᵒᵈ _ _ _ _ _ _ _ hf.dual_left ha
lemma supr_eq_of_tendsto {α β} [topological_space α] [complete_linear_order α] [order_topology α]
[nonempty β] [semilattice_sup β] {f : β → α} {a : α} (hf : monotone f) :
tendsto f at_top (𝓝 a) → supr f = a :=
tendsto_nhds_unique (tendsto_at_top_supr hf)
lemma infi_eq_of_tendsto {α} [topological_space α] [complete_linear_order α] [order_topology α]
[nonempty β] [semilattice_sup β] {f : β → α} {a : α} (hf : antitone f) :
tendsto f at_top (𝓝 a) → infi f = a :=
tendsto_nhds_unique (tendsto_at_top_infi hf)
lemma supr_eq_supr_subseq_of_monotone {ι₁ ι₂ α : Type*} [preorder ι₂] [complete_lattice α]
{l : filter ι₁} [l.ne_bot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : monotone f)
(hφ : tendsto φ l at_top) :
(⨆ i, f i) = (⨆ i, f (φ i)) :=
le_antisymm
(supr_mono' $ λ i, exists_imp_exists (λ j (hj : i ≤ φ j), hf hj)
(hφ.eventually $ eventually_ge_at_top i).exists)
(supr_mono' $ λ i, ⟨φ i, le_rfl⟩)
lemma infi_eq_infi_subseq_of_monotone {ι₁ ι₂ α : Type*} [preorder ι₂] [complete_lattice α]
{l : filter ι₁} [l.ne_bot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : monotone f)
(hφ : tendsto φ l at_bot) :
(⨅ i, f i) = (⨅ i, f (φ i)) :=
supr_eq_supr_subseq_of_monotone hf.dual hφ