Documentation

Mathlib.Probability.Martingale.OptionalSampling

Optional sampling theorem #

If τ is a bounded stopping time and σ is another stopping time, then the value of a martingale f at the stopping time min τ σ is almost everywhere equal to μ[stoppedValue f τ | hσ.measurableSpace].

Main results #

The value of a martingale f at a stopping time τ bounded by n is the conditional expectation of f n with respect to the σ-algebra generated by τ.

The value of a martingale f at a stopping time τ bounded by n is the conditional expectation of f n with respect to the σ-algebra generated by τ.

If τ and σ are two stopping times with σ ≤ τ and τ is bounded, then the value of a martingale f at σ is the conditional expectation of its value at τ with respect to the σ-algebra generated by σ.

If τ and σ are two stopping times with σ ≤ τ and τ is bounded, then the value of a martingale f at σ is the conditional expectation of its value at τ with respect to the σ-algebra generated by σ.

In the following results the index set verifies [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι], which means that it is order-isomorphic to a subset of . ι is equipped with the discrete topology, which is also the order topology, and is a measurable space with the Borel σ-algebra.

Optional Sampling theorem. If τ is a bounded stopping time and σ is another stopping time, then the value of a martingale f at the stopping time min τ σ is almost everywhere equal to the conditional expectation of f stopped at τ with respect to the σ-algebra generated by σ.