Skip to content

Commit 397b110

Browse files
kex-ypre-commit-ci-lite[bot]
kex-y
and
pre-commit-ci-lite[bot]
committed
feat(Probability): predictable processes (leanprover-community#30997)
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
1 parent 1b1b028 commit 397b110

3 files changed

Lines changed: 246 additions & 0 deletions

File tree

β€ŽMathlib.leanβ€Ž

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5492,6 +5492,7 @@ import Mathlib.Probability.Process.FiniteDimensionalLaws
54925492
import Mathlib.Probability.Process.HittingTime
54935493
import Mathlib.Probability.Process.Kolmogorov
54945494
import Mathlib.Probability.Process.PartitionFiltration
5495+
import Mathlib.Probability.Process.Predictable
54955496
import Mathlib.Probability.Process.Stopping
54965497
import Mathlib.Probability.ProductMeasure
54975498
import Mathlib.Probability.StrongLaw

β€ŽMathlib/Probability/Martingale/Basic.leanβ€Ž

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: RΓ©my Degenne, Kexing Ying
55
-/
66
import Mathlib.Probability.Notation
77
import Mathlib.Probability.Process.Stopping
8+
import Mathlib.Probability.Process.Predictable
89

910
/-!
1011
# Martingales
@@ -443,6 +444,38 @@ theorem Martingale.eq_zero_of_predictable [SigmaFiniteFiltration ΞΌ 𝒒] {f :
443444
exact ((Germ.coe_eq.mp (congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒒.le _) (hfadp _)
444445
(hfmgle.integrable _))).symm.trans (hfmgle.2 k (k + 1) k.le_succ)).trans ih
445446

447+
section IsPredictable
448+
449+
variable [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
450+
451+
/-- A predictable submartingale is a.e. greater than or equal to its initial state.
452+
453+
In constrast to the non-primed version, this results require second countablility as `Adapted` is
454+
defined using strong measurability while `IsPredictable` only provides measurable. -/
455+
theorem Submartingale.zero_le_of_predictable' [Preorder E] [SigmaFiniteFiltration ΞΌ 𝒒]
456+
{f : β„• β†’ Ξ© β†’ E} (hfmgle : Submartingale f 𝒒 ΞΌ) (hf : IsPredictable 𝒒 f) (n : β„•) :
457+
f 0 ≀ᡐ[ΞΌ] f n :=
458+
zero_le_of_predictable hfmgle (fun _ ↦ (hf.measurable_add_one _).stronglyMeasurable) n
459+
460+
/-- A predictable supermartingale is a.e. less equal than its initial state.
461+
462+
In constrast to the non-primed version, this results require second countablility as `Adapted` is
463+
defined using strong measurability while `IsPredictable` only provides measurable. -/
464+
theorem Supermartingale.le_zero_of_predictable' [Preorder E] [SigmaFiniteFiltration ΞΌ 𝒒]
465+
{f : β„• β†’ Ξ© β†’ E} (hfmgle : Supermartingale f 𝒒 ΞΌ) (hfadp : IsPredictable 𝒒 f)
466+
(n : β„•) : f n ≀ᡐ[ΞΌ] f 0 :=
467+
le_zero_of_predictable hfmgle (fun _ ↦ (hfadp.measurable_add_one _).stronglyMeasurable) n
468+
469+
/-- A predictable martingale is a.e. equal to its initial state.
470+
471+
In constrast to the non-primed version, this results require second countablility as `Adapted` is
472+
defined using strong measurability while `IsPredictable` only provides measurable. -/
473+
theorem Martingale.eq_zero_of_predictable' [SigmaFiniteFiltration ΞΌ 𝒒] {f : β„• β†’ Ξ© β†’ E}
474+
(hfmgle : Martingale f 𝒒 ΞΌ) (hfadp : IsPredictable 𝒒 f) (n : β„•) : f n =ᡐ[ΞΌ] f 0 :=
475+
eq_zero_of_predictable hfmgle (fun _ ↦ (hfadp.measurable_add_one _).stronglyMeasurable) n
476+
477+
end IsPredictable
478+
446479
namespace Submartingale
447480

448481
protected theorem integrable_stoppedValue [LE E] {f : β„• β†’ Ξ© β†’ E} (hf : Submartingale f 𝒒 ΞΌ)

β€ŽMathlib/Probability/Process/Predictable.leanβ€Ž

Lines changed: 212 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,212 @@
1+
/-
2+
Copyright (c) 2025 Kexing Ying. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kexing Ying
5+
-/
6+
import Mathlib.Probability.Process.Adapted
7+
8+
/-!
9+
# Predictable Οƒ-algebra
10+
11+
This file defines the predictable Οƒ-algebra associated to a filtration, as well as the
12+
notion of predictable processes. We prove that predictable processes are progressively measurable
13+
and adapted. We also give an equivalent characterization of predictability for discrete processes.
14+
15+
## Main definitions
16+
17+
* `Filtration.predictable` : The predictable Οƒ-algebra associated to a filtration.
18+
* `IsPredictable` : A process is predictable if it is measurable with respect to the
19+
predictable Οƒ-algebra.
20+
21+
## Main results
22+
23+
* `IsPredictable.progMeasurable` : A predictable process is progressively measurable.
24+
* `isPredictable_iff_measurable_add_one` : `u` is a discrete predictable process iff
25+
`u (n + 1)` is `𝓕 n`-measurable and `u 0` is `𝓕 0`-measurable.
26+
27+
## Tags
28+
29+
predictable, previsible
30+
31+
-/
32+
33+
open Filter Order TopologicalSpace
34+
35+
open scoped MeasureTheory NNReal ENNReal Topology
36+
37+
namespace MeasureTheory
38+
39+
variable {Ξ© ΞΉ : Type*} {m : MeasurableSpace Ξ©} {E : Type*} [TopologicalSpace E]
40+
41+
section
42+
43+
variable [Preorder ΞΉ] [OrderBot ΞΉ]
44+
45+
namespace Filtration
46+
47+
/-- Given a filtration `𝓕`, the predictable Οƒ-algebra is the Οƒ-algebra on `ΞΉ Γ— Ξ©` generated by
48+
sets of the form `(t, ∞) Γ— A` for `t ∈ ΞΉ` and `A ∈ 𝓕 t` and `{βŠ₯} Γ— A` for `A ∈ 𝓕 βŠ₯`. -/
49+
def predictable (𝓕 : Filtration ΞΉ m) : MeasurableSpace (ΞΉ Γ— Ξ©) :=
50+
MeasurableSpace.generateFrom <|
51+
{s | βˆƒ A, MeasurableSet[𝓕 βŠ₯] A ∧ s = {βŠ₯} Γ—Λ’ A} βˆͺ
52+
{s | βˆƒ i A, MeasurableSet[𝓕 i] A ∧ s = Set.Ioi i Γ—Λ’ A}
53+
54+
end Filtration
55+
56+
/-- A process is said to be predictable if it is measurable with respect to the predictable
57+
Οƒ-algebra. -/
58+
def IsPredictable (𝓕 : Filtration ΞΉ m) (u : ΞΉ β†’ Ξ© β†’ E) :=
59+
StronglyMeasurable[𝓕.predictable] <| Function.uncurry u
60+
61+
end
62+
63+
lemma measurableSet_predictable_singleton_bot_prod [LinearOrder ΞΉ] [OrderBot ΞΉ]
64+
{𝓕 : Filtration ΞΉ m} {s : Set Ξ©} (hs : MeasurableSet[𝓕 βŠ₯] s) :
65+
MeasurableSet[𝓕.predictable] <| {βŠ₯} Γ—Λ’ s :=
66+
MeasurableSpace.measurableSet_generateFrom <| Or.inl ⟨s, hs, rfl⟩
67+
68+
lemma measurableSet_predictable_Ioi_prod [LinearOrder ΞΉ] [OrderBot ΞΉ]
69+
{𝓕 : Filtration ΞΉ m} {i : ΞΉ} {s : Set Ξ©} (hs : MeasurableSet[𝓕 i] s) :
70+
MeasurableSet[𝓕.predictable] <| Set.Ioi i Γ—Λ’ s :=
71+
MeasurableSpace.measurableSet_generateFrom <| Or.inr ⟨i, s, hs, rfl⟩
72+
73+
/-- Sets of the form `(i, j] Γ— A` for any `A ∈ 𝓕 i` are measurable with respect to the predictable
74+
Οƒ-algebra. -/
75+
lemma measurableSet_predictable_Ioc_prod [LinearOrder ΞΉ] [OrderBot ΞΉ]
76+
{𝓕 : Filtration ΞΉ m} (i j : ΞΉ) {s : Set Ξ©} (hs : MeasurableSet[𝓕 i] s) :
77+
MeasurableSet[𝓕.predictable] <| Set.Ioc i j Γ—Λ’ s := by
78+
obtain hij | hij := le_total j i
79+
Β· simp [hij]
80+
Β· rw [← Set.Ioi_diff_Ioi, (by simp : (Set.Ioi i \ Set.Ioi j) Γ—Λ’ s
81+
= Set.Ioi i Γ—Λ’ (s \ s) βˆͺ (Set.Ioi i \ Set.Ioi j) Γ—Λ’ s), ← Set.prod_diff_prod]
82+
exact (measurableSet_predictable_Ioi_prod hs).diff
83+
(measurableSet_predictable_Ioi_prod <| 𝓕.mono hij _ hs)
84+
85+
lemma measurableSpace_le_predictable_of_measurableSet [Preorder ΞΉ] [OrderBot ΞΉ]
86+
{𝓕 : Filtration ΞΉ m} {m' : MeasurableSpace (ΞΉ Γ— Ξ©)}
87+
(hm'bot : βˆ€ A, MeasurableSet[𝓕 βŠ₯] A β†’ MeasurableSet[m'] ({βŠ₯} Γ—Λ’ A))
88+
(hm' : βˆ€ i A, MeasurableSet[𝓕 i] A β†’ MeasurableSet[m'] ((Set.Ioi i) Γ—Λ’ A)) :
89+
𝓕.predictable ≀ m' := by
90+
refine MeasurableSpace.generateFrom_le ?_
91+
rintro - (⟨A, hA, rfl⟩ | ⟨i, A, hA, rfl⟩)
92+
Β· exact hm'bot A hA
93+
Β· exact hm' i A hA
94+
95+
namespace IsPredictable
96+
97+
open Filtration
98+
99+
variable [LinearOrder ΞΉ] [OrderBot ΞΉ] [MeasurableSpace ΞΉ] [TopologicalSpace ΞΉ]
100+
[OpensMeasurableSpace ΞΉ] [OrderClosedTopology ΞΉ]
101+
[MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
102+
103+
/-- A predictable process is progressively measurable. -/
104+
lemma progMeasurable {𝓕 : Filtration ΞΉ m} {u : ΞΉ β†’ Ξ© β†’ E} (h𝓕 : IsPredictable 𝓕 u) :
105+
ProgMeasurable 𝓕 u := by
106+
refine fun i ↦ Measurable.stronglyMeasurable ?_
107+
rw [IsPredictable, stronglyMeasurable_iff_measurable, measurable_iff_comap_le] at h𝓕
108+
rw [measurable_iff_comap_le, (by aesop : (fun (p : Set.Iic i Γ— Ξ©) ↦ u (p.1) p.2)
109+
= Function.uncurry u ∘ (fun p ↦ (p.1, p.2))), ← MeasurableSpace.comap_comp]
110+
refine (MeasurableSpace.comap_mono h𝓕).trans <| MeasurableSpace.comap_le_iff_le_map.2 <|
111+
measurableSpace_le_predictable_of_measurableSet ?_ ?_
112+
Β· intros A hA
113+
simp only [MeasurableSpace.map_def,
114+
(by aesop : (fun (p : Set.Iic i Γ— Ξ©) ↦ ((p.1 : ΞΉ), p.2)) ⁻¹' ({βŠ₯} Γ—Λ’ A) = {βŠ₯} Γ—Λ’ A)]
115+
exact (measurableSet_singleton _).prod <| 𝓕.mono bot_le _ hA
116+
Β· intros j A hA
117+
simp only [MeasurableSpace.map_def]
118+
obtain hji | hij := le_total j i
119+
Β· rw [(by grind : (fun (p : Set.Iic i Γ— Ξ©) ↦ ((p.1 : ΞΉ), p.2)) ⁻¹' Set.Ioi j Γ—Λ’ A
120+
= (Subtype.val ⁻¹' (Set.Ioc j i)) Γ—Λ’ A)]
121+
exact (measurable_subtype_coe measurableSet_Ioc).prod (𝓕.mono hji _ hA)
122+
Β· simp [(by grind : (fun (p : Set.Iic i Γ— Ξ©) ↦ ((p.1 : ΞΉ), p.2)) ⁻¹' Set.Ioi j Γ—Λ’ A = βˆ…)]
123+
124+
/-- A predictable process is adapted. -/
125+
lemma adapted {𝓕 : Filtration ΞΉ m} {u : ΞΉ β†’ Ξ© β†’ E} (h𝓕 : IsPredictable 𝓕 u) :
126+
Adapted 𝓕 u :=
127+
h𝓕.progMeasurable.adapted
128+
129+
omit [SecondCountableTopology E] in
130+
lemma measurableSet_prodMk_add_one_of_predictable {𝓕 : Filtration β„• m} {s : Set (β„• Γ— Ξ©)}
131+
(hs : MeasurableSet[𝓕.predictable] s) (n : β„•) :
132+
MeasurableSet[𝓕 n] {Ο‰ | (n + 1, Ο‰) ∈ s} := by
133+
rw [(by aesop : {Ο‰ | (n + 1, Ο‰) ∈ s} = (Prod.mk (Ξ± := Set.singleton (n + 1)) (Ξ² := Ξ©)
134+
⟨n + 1, rfl⟩) ⁻¹' ((fun (p : Set.singleton (n + 1) Γ— Ξ©) ↦ ((p.1 : β„•), p.2)) ⁻¹' s))]
135+
refine measurableSet_preimage (mΞ² := Subtype.instMeasurableSpace.prod (𝓕 n))
136+
measurable_prodMk_left <| measurableSet_preimage ?_ hs
137+
rw [measurable_iff_comap_le, MeasurableSpace.comap_le_iff_le_map]
138+
refine MeasurableSpace.generateFrom_le ?_
139+
rintro - (⟨A, hA, rfl⟩ | ⟨i, A, hA, rfl⟩)
140+
Β· rw [MeasurableSpace.map_def,
141+
(_ : (fun (p : Set.singleton (n + 1) Γ— Ξ©) ↦ ((p.1 : β„•), p.2)) ⁻¹' ({βŠ₯} Γ—Λ’ A) = βˆ…)]
142+
Β· simp
143+
Β· ext p
144+
simp only [Nat.bot_eq_zero, Set.mem_preimage, Set.mem_prod, Set.mem_singleton_iff,
145+
Set.mem_empty_iff_false, iff_false, not_and]
146+
exact fun hp1 ↦ False.elim <| Nat.succ_ne_zero n (hp1 β–Έ p.1.2.symm)
147+
Β· rw [MeasurableSpace.map_def]
148+
obtain hni | hin := lt_or_ge n i
149+
Β· rw [(_ : (fun (p : Set.singleton (n + 1) Γ— Ξ©) ↦ ((p.1 : β„•), p.2)) ⁻¹' (Set.Ioi i Γ—Λ’ A) = βˆ…)]
150+
Β· simp
151+
Β· ext p
152+
simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_empty_iff_false,
153+
iff_false, not_and]
154+
rw [p.1.2]
155+
grind
156+
Β· rw [(_ : (fun (p : Set.singleton (n + 1) Γ— Ξ©) ↦ ((p.1 : β„•), p.2)) ⁻¹' (Set.Ioi i Γ—Λ’ A)
157+
= {⟨n + 1, rfl⟩} Γ—Λ’ A)]
158+
Β· exact MeasurableSet.prod (MeasurableSet.of_subtype_image trivial) (𝓕.mono hin _ hA)
159+
Β· ext p
160+
simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_singleton_iff,
161+
and_congr_left_iff]
162+
intro hp2
163+
rw [p.1.2]
164+
exact ⟨fun _ ↦ by aesop, fun _ ↦ lt_add_one_iff.2 hin⟩
165+
166+
omit [SecondCountableTopology E] in
167+
/-- If `u` is a discrete predictable process, then `u (n + 1)` is `𝓕 n`-measurable. -/
168+
lemma measurable_add_one {𝓕 : Filtration β„• m} {u : β„• β†’ Ξ© β†’ E} (h𝓕 : IsPredictable 𝓕 u) (n : β„•) :
169+
Measurable[𝓕 n] (u (n + 1)) := by
170+
intro s hs
171+
rw [(by aesop : u (n + 1) ⁻¹' s = {Ο‰ | (n + 1, Ο‰) ∈ (Function.uncurry u) ⁻¹' s})]
172+
exact measurableSet_prodMk_add_one_of_predictable (h𝓕.measurable hs) n
173+
174+
end IsPredictable
175+
176+
section
177+
178+
variable [MetrizableSpace E] [MeasurableSpace E] [BorelSpace E]
179+
180+
lemma measurableSet_predictable_singleton_prod
181+
{𝓕 : Filtration β„• m} {n : β„•} {s : Set Ξ©} (hs : MeasurableSet[𝓕 n] s) :
182+
MeasurableSet[𝓕.predictable] <| {n + 1} Γ—Λ’ s := by
183+
rw [(_ : {n + 1} = Set.Ioc n (n + 1))]
184+
Β· exact measurableSet_predictable_Ioc_prod _ _ hs
185+
Β· ext m
186+
simp only [Set.mem_singleton_iff, Set.mem_Ioc]
187+
omega
188+
189+
lemma isPredictable_of_measurable_add_one [SecondCountableTopology E]
190+
{𝓕 : Filtration β„• m} {u : β„• β†’ Ξ© β†’ E}
191+
(hβ‚€ : Measurable[𝓕 0] (u 0)) (h : βˆ€ n, Measurable[𝓕 n] (u (n + 1))) :
192+
IsPredictable 𝓕 u := by
193+
refine Measurable.stronglyMeasurable ?_
194+
intro s hs
195+
rw [(by aesop : Function.uncurry u ⁻¹' s = ⋃ n : β„•, {n} Γ—Λ’ (u n ⁻¹' s))]
196+
refine MeasurableSet.iUnion <| fun n ↦ ?_
197+
obtain (rfl | hn) := n.eq_zero_or_eq_succ_pred
198+
Β· exact MeasurableSpace.measurableSet_generateFrom <| Or.inl ⟨u 0 ⁻¹' s, hβ‚€ hs, rfl⟩
199+
Β· rw [hn]
200+
exact measurableSet_predictable_singleton_prod (h (n - 1) hs)
201+
202+
/-- A discrete process `u` is predictable iff `u (n + 1)` is `𝓕 n`-measurable for all `n` and
203+
`u 0` is `𝓕 0`-measurable. -/
204+
lemma isPredictable_iff_measurable_add_one [SecondCountableTopology E]
205+
{𝓕 : Filtration β„• m} {u : β„• β†’ Ξ© β†’ E} :
206+
IsPredictable 𝓕 u ↔ Measurable[𝓕 0] (u 0) ∧ βˆ€ n, Measurable[𝓕 n] (u (n + 1)) :=
207+
⟨fun h𝓕 ↦ ⟨(h𝓕.adapted 0).measurable, fun n ↦ h𝓕.measurable_add_one (n)⟩,
208+
fun h ↦ isPredictable_of_measurable_add_one h.1 h.2⟩
209+
210+
end
211+
212+
end MeasureTheory

0 commit comments

Comments
Β (0)