Martingales #
A family of functions f : ι → α → E
is a martingale with respect to a filtration ℱ
if every
f i
is integrable, f
is adapted with respect to ℱ
and for all i ≤ j
,
μ[f j | ℱ.le i] =ᵐ[μ] f i
. On the other hand, f : ι → α → E
is said to be a supermartingale
with respect to the filtration ℱ
if f i
is integrable, f
is adapted with resepct to ℱ
and for all i ≤ j
, μ[f j | ℱ.le i] ≤ᵐ[μ] f i
. Finally, f : ι → α → E
is said to be a
submartingale with respect to the filtration ℱ
if f i
is integrable, f
is adapted with
resepct to ℱ
and for all i ≤ j
, f i ≤ᵐ[μ] μ[f j | ℱ.le i]
.
The definitions of filtration and adapted can be found in probability_theory.stopping
.
Definitions #
measure_theory.martingale f ℱ μ
:f
is a martingale with respect to filtrationℱ
and measureμ
.measure_theory.supermartingale f ℱ μ
:f
is a supermartingale with respect to filtrationℱ
and measureμ
.measure_theory.submartingale f ℱ μ
:f
is a submartingale with respect to filtrationℱ
and measureμ
.
Results #
measure_theory.martingale_condexp f ℱ μ
: the sequenceλ i, μ[f | ℱ i, ℱ.le i])
is a martingale with respect toℱ
andμ
.
A family of functions f : ι → α → E
is a martingale with respect to a filtration ℱ
if f
is adapted with respect to ℱ
and for all i ≤ j
, μ[f j | ℱ.le i] =ᵐ[μ] f i
.
Equations
- measure_theory.martingale f ℱ μ = (measure_theory.adapted ℱ f ∧ ∀ (i j : ι), i ≤ j → μ[f j|_] =ᵐ[μ] f i)
A family of integrable functions f : ι → α → E
is a supermartingale with respect to a
filtration ℱ
if f
is adapted with respect to ℱ
and for all i ≤ j
,
μ[f j | ℱ.le i] ≤ᵐ[μ] f i
.
Equations
- measure_theory.supermartingale f ℱ μ = (measure_theory.adapted ℱ f ∧ (∀ (i j : ι), i ≤ j → μ[f j|_] ≤ᵐ[μ] f i) ∧ ∀ (i : ι), measure_theory.integrable (f i) μ)
A family of integrable functions f : ι → α → E
is a submartingale with respect to a
filtration ℱ
if f
is adapted with respect to ℱ
and for all i ≤ j
,
f i ≤ᵐ[μ] μ[f j | ℱ.le i]
.
Equations
- measure_theory.submartingale f ℱ μ = (measure_theory.adapted ℱ f ∧ (∀ (i j : ι), i ≤ j → f i ≤ᵐ[μ] (μ[f j|_])) ∧ ∀ (i : ι), measure_theory.integrable (f i) μ)
Given a submartingale f
and bounded stopping times τ
and π
such that τ ≤ π
, the
expectation of stopped_value f τ
is less or equal to the expectation of stopped_value f π
.
This is the forward direction of the optional stopping theorem.