-
Notifications
You must be signed in to change notification settings - Fork 298
/
stopping.lean
294 lines (238 loc) · 10.5 KB
/
stopping.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
/-
Copyright (c) 2021 Kexing Ying. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kexing Ying
-/
import measure_theory.constructions.borel_space
/-!
# Filtration and stopping time
This file defines some standard definition from the theory of stochastic processes including
filtrations and stopping times. These definitions are used to model the amount of information
at a specific time and is the first step in formalizing stochastic processes.
## Main definitions
* `measure_theory.filtration`: a filtration on a measurable space
* `measure_theory.adapted`: a sequence of functions `u` is said to be adapted to a
filtration `f` if at each point in time `i`, `u i` is `f i`-measurable
* `measure_theory.filtration.natural`: the natural filtration with respect to a sequence of
measurable functions is the smallest filtration to which it is adapted to
* `measure_theory.stopping_time`: a stopping time with respect to some filtration `f` is a
function `τ` such that for all `i`, the preimage of `{j | j ≤ i}` along `τ` is
`f i`-measurable
* `measure_theory.stopping_time.measurable_space`: the σ-algebra associated with a stopping time
## Tags
filtration, stopping time, stochastic process
-/
noncomputable theory
open_locale classical measure_theory nnreal ennreal topological_space
namespace measure_theory
/-- A `filtration` on measurable space `α` with σ-algebra `m` is a monotone
sequence of of sub-σ-algebras of `m`. -/
structure filtration {α : Type*} (ι : Type*) [preorder ι] (m : measurable_space α) :=
(seq : ι → measurable_space α)
(mono : monotone seq)
(le : ∀ i : ι, seq i ≤ m)
variables {α β ι : Type*} {m : measurable_space α} [measurable_space β]
open topological_space
section preorder
variables [preorder ι]
instance : has_coe_to_fun (filtration ι m) (λ _, ι → measurable_space α) :=
⟨λ f, f.seq⟩
/-- The constant filtration which is equal to `m` for all `i : ι`. -/
def const_filtration (m : measurable_space α) : filtration ι m :=
⟨λ _, m, monotone_const, λ _, le_rfl⟩
instance : inhabited (filtration ι m) :=
⟨const_filtration m⟩
lemma measurable_set_of_filtration {f : filtration ι m} {s : set α} {i : ι}
(hs : measurable_set[f i] s) : measurable_set[m] s :=
f.le i s hs
/-- A measure is σ-finite with respect to filtration if it is σ-finite with respect
to all the sub-σ-algebra of the filtration. -/
class sigma_finite_filtration (μ : measure α) (f : filtration ι m) : Prop :=
(sigma_finite : ∀ i : ι, sigma_finite (μ.trim (f.le i)))
instance sigma_finite_of_sigma_finite_filtration (μ : measure α) (f : filtration ι m)
[hf : sigma_finite_filtration μ f] (i : ι) :
sigma_finite (μ.trim (f.le i)) :=
by apply hf.sigma_finite -- can't exact here
/-- A sequence of functions `u` is adapted to a filtration `f` if for all `i`,
`u i` is `f i`-measurable. -/
def adapted (f : filtration ι m) (u : ι → α → β) : Prop :=
∀ i : ι, measurable[f i] (u i)
namespace adapted
lemma add [has_add β] [has_measurable_add₂ β] {u v : ι → α → β} {f : filtration ι m}
(hu : adapted f u) (hv : adapted f v) : adapted f (u + v):=
λ i, @measurable.add _ _ _ _ (f i) _ _ _ (hu i) (hv i)
lemma neg [has_neg β] [has_measurable_neg β] {u : ι → α → β} {f : filtration ι m}
(hu : adapted f u) : adapted f (-u) :=
λ i, @measurable.neg _ α _ _ _ (f i) _ (hu i)
lemma smul [has_scalar ℝ β] [has_measurable_smul ℝ β] {u : ι → α → β} {f : filtration ι m}
(c : ℝ) (hu : adapted f u) : adapted f (c • u) :=
λ i, @measurable.const_smul ℝ β α _ _ _ (f i) _ _ (hu i) c
end adapted
variable (β)
lemma adapted_zero [has_zero β] (f : filtration ι m) : adapted f (0 : ι → α → β) :=
λ i, @measurable_zero β α _ (f i) _
variable {β}
namespace filtration
/-- Given a sequence of functions, the natural filtration is the smallest sequence
of σ-algebras such that that sequence of functions is measurable with respect to
the filtration. -/
def natural (u : ι → α → β) (hum : ∀ i, measurable (u i)) : filtration ι m :=
{ seq := λ i, ⨆ j ≤ i, measurable_space.comap (u j) infer_instance,
mono := λ i j hij, bsupr_le_bsupr' $ λ k hk, le_trans hk hij,
le := λ i, bsupr_le (λ j hj s hs, let ⟨t, ht, ht'⟩ := hs in ht' ▸ hum j ht) }
lemma adapted_natural {u : ι → α → β} (hum : ∀ i, measurable[m] (u i)) :
adapted (natural u hum) u :=
λ i, measurable.le (le_bsupr_of_le i (le_refl i) (le_refl _)) (λ s hs, ⟨s, hs, rfl⟩)
end filtration
variables {μ : measure α} {f : filtration ι m}
/-- A stopping time with respect to some filtration `f` is a function
`τ` such that for all `i`, the preimage of `{j | j ≤ i}` along `τ` is measurable
with respect to `f i`.
Intuitively, the stopping time `τ` describes some stopping rule such that at time
`i`, we may determine it with the information we have at time `i`. -/
def is_stopping_time (f : filtration ι m) (τ : α → ι) :=
∀ i : ι, measurable_set[f i] $ {x | τ x ≤ i}
lemma is_stopping_time.measurable_set_eq
{f : filtration ℕ m} {τ : α → ℕ} (hτ : is_stopping_time f τ) (i : ℕ) :
measurable_set[f i] $ {x | τ x = i} :=
begin
cases i,
{ convert (hτ 0),
simp only [set.set_of_eq_eq_singleton, le_zero_iff] },
{ rw (_ : {x | τ x = i + 1} = {x | τ x ≤ i + 1} \ {x | τ x ≤ i}),
{ exact @measurable_set.diff _ (f (i + 1)) _ _ (hτ (i + 1))
(f.mono (nat.le_succ _) _ (hτ i)) },
{ ext, simp only [set.mem_diff, not_le, set.mem_set_of_eq],
split,
{ intro h, simp [h] },
{ rintro ⟨h₁, h₂⟩,
linarith } } }
end
lemma is_stopping_time.measurable_set_eq_le
{f : filtration ℕ m} {τ : α → ℕ} (hτ : is_stopping_time f τ) {i j : ℕ} (hle : i ≤ j) :
measurable_set[f j] $ {x | τ x = i} :=
f.mono hle _ $ hτ.measurable_set_eq i
lemma is_stopping_time_of_measurable_set_eq
{f : filtration ℕ m} {τ : α → ℕ} (hτ : ∀ i, measurable_set[f i] $ {x | τ x = i}) :
is_stopping_time f τ :=
begin
intro i,
rw show {x | τ x ≤ i} = ⋃ k ≤ i, {x | τ x = k}, by { ext, simp },
refine @measurable_set.bUnion _ _ (f i) _ _ (set.countable_encodable _) (λ k hk, _),
exact f.mono hk _ (hτ k),
end
lemma is_stopping_time_const {f : filtration ι m} (i : ι) :
is_stopping_time f (λ x, i) :=
λ j, by simp
end preorder
namespace is_stopping_time
lemma max [linear_order ι] {f : filtration ι m} {τ π : α → ι}
(hτ : is_stopping_time f τ) (hπ : is_stopping_time f π) :
is_stopping_time f (λ x, max (τ x) (π x)) :=
begin
intro i,
simp_rw [max_le_iff, set.set_of_and],
exact @measurable_set.inter _ (f i) _ _ (hτ i) (hπ i),
end
lemma min [linear_order ι] {f : filtration ι m} {τ π : α → ι}
(hτ : is_stopping_time f τ) (hπ : is_stopping_time f π) :
is_stopping_time f (λ x, min (τ x) (π x)) :=
begin
intro i,
simp_rw [min_le_iff, set.set_of_or],
exact @measurable_set.union _ (f i) _ _ (hτ i) (hπ i),
end
lemma add_const
[add_group ι] [preorder ι] [covariant_class ι ι (function.swap (+)) (≤)]
[covariant_class ι ι (+) (≤)]
{f : filtration ι m} {τ : α → ι} (hτ : is_stopping_time f τ) {i : ι} (hi : 0 ≤ i) :
is_stopping_time f (λ x, τ x + i) :=
begin
intro j,
simp_rw [← le_sub_iff_add_le],
exact f.mono (sub_le_self j hi) _ (hτ (j - i)),
end
variables [preorder ι] {f : filtration ι m}
/-- The associated σ-algebra with a stopping time. -/
def measurable_space
{τ : α → ι} (hτ : is_stopping_time f τ) : measurable_space α :=
{ measurable_set' := λ s, ∀ i : ι, measurable_set[f i] (s ∩ {x | τ x ≤ i}),
measurable_set_empty :=
λ i, (set.empty_inter {x | τ x ≤ i}).symm ▸ @measurable_set.empty _ (f i),
measurable_set_compl := λ s hs i,
begin
rw (_ : sᶜ ∩ {x | τ x ≤ i} = (sᶜ ∪ {x | τ x ≤ i}ᶜ) ∩ {x | τ x ≤ i}),
{ refine @measurable_set.inter _ (f i) _ _ _ _,
{ rw ← set.compl_inter,
exact @measurable_set.compl _ _ (f i) (hs i) },
{ exact hτ i} },
{ rw set.union_inter_distrib_right,
simp only [set.compl_inter_self, set.union_empty] }
end,
measurable_set_Union := λ s hs i,
begin
rw forall_swap at hs,
rw set.Union_inter,
exact @measurable_set.Union _ _ (f i) _ _ (hs i),
end }
@[protected]
lemma measurable_set {τ : α → ι} (hτ : is_stopping_time f τ) (s : set α) :
measurable_set[hτ.measurable_space] s ↔
∀ i : ι, measurable_set[f i] (s ∩ {x | τ x ≤ i}) :=
iff.rfl
lemma measurable_space_mono
{τ π : α → ι} (hτ : is_stopping_time f τ) (hπ : is_stopping_time f π) (hle : τ ≤ π) :
hτ.measurable_space ≤ hπ.measurable_space :=
begin
intros s hs i,
rw (_ : s ∩ {x | π x ≤ i} = s ∩ {x | τ x ≤ i} ∩ {x | π x ≤ i}),
{ exact @measurable_set.inter _ (f i) _ _ (hs i) (hπ i) },
{ ext,
simp only [set.mem_inter_eq, iff_self_and, and.congr_left_iff, set.mem_set_of_eq],
intros hle' _,
exact le_trans (hle _) hle' },
end
lemma measurable_space_le [encodable ι] {τ : α → ι} (hτ : is_stopping_time f τ) :
hτ.measurable_space ≤ m :=
begin
intros s hs,
change ∀ i, measurable_set[f i] (s ∩ {x | τ x ≤ i}) at hs,
rw (_ : s = ⋃ i, s ∩ {x | τ x ≤ i}),
{ exact measurable_set.Union (λ i, f.le i _ (hs i)) },
{ ext x, split; rw set.mem_Union,
{ exact λ hx, ⟨τ x, hx, le_refl _⟩ },
{ rintro ⟨_, hx, _⟩,
exact hx } }
end
section nat
lemma measurable_set_eq_const {f : filtration ℕ m}
{τ : α → ℕ} (hτ : is_stopping_time f τ) (i : ℕ) :
measurable_set[hτ.measurable_space] {x | τ x = i} :=
begin
rw hτ.measurable_set,
intro j,
by_cases i ≤ j,
{ rw (_ : {x | τ x = i} ∩ {x | τ x ≤ j} = {x | τ x = i}),
{ exact hτ.measurable_set_eq_le h },
{ ext,
simp only [set.mem_inter_eq, and_iff_left_iff_imp, set.mem_set_of_eq],
rintro rfl,
assumption } },
{ rw (_ : {x | τ x = i} ∩ {x | τ x ≤ j} = ∅),
{ exact @measurable_set.empty _ (f j) },
{ ext,
simp only [set.mem_empty_eq, set.mem_inter_eq, not_and, not_le, set.mem_set_of_eq, iff_false],
rintro rfl,
rwa not_le at h } }
end
lemma measurable {f : filtration ℕ m} {τ : α → ℕ} (hτ : is_stopping_time f τ) :
measurable[hτ.measurable_space] τ :=
begin
refine @measurable_to_encodable ℕ α ⊤ hτ.measurable_space _ τ _,
intro y,
simp_rw [set.preimage, set.mem_singleton_iff],
exact is_stopping_time.measurable_set_eq_const _ _,
end
end nat
end is_stopping_time
end measure_theory