structure
TextbookMartingale
{Ω : Type u_1}
{ι : Type u_2}
[Preorder ι]
{m0 : MeasurableSpace Ω}
(f : ι → Ω → ℝ)
(ℱ : MeasureTheory.Filtration ι m0)
(μ : MeasureTheory.Measure Ω)
:
Textbook definition of a real-valued martingale with respect to a filtration ℱ
and measure μ (Lecture 29, "Martingales"): a process f : ι → Ω → ℝ is a
martingale if it is adapted to ℱ, each f i is integrable, and the
conditional expectation satisfies E[f j | ℱ i] = f i almost surely whenever
i ≤ j.
- adapted : MeasureTheory.StronglyAdapted ℱ f
- integrable (i : ι) : MeasureTheory.Integrable (f i) μ