MeasureTheory.Submartingale.expected_stoppedValue_mono
theorem MeasureTheory.Submartingale.expected_stoppedValue_mono :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} {τ π : Ω → ℕ} [inst : MeasureTheory.SigmaFiniteFiltration μ 𝒢],
MeasureTheory.Submartingale f 𝒢 μ →
MeasureTheory.IsStoppingTime 𝒢 τ →
MeasureTheory.IsStoppingTime 𝒢 π →
τ ≤ π →
∀ {N : ℕ},
(∀ (ω : Ω), π ω ≤ N) →
∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ
This theorem, known as the forward direction of the optional stopping theorem, states that for a given submartingale `f` and two bounded stopping times `τ` and `π` (where `τ` is less than or equal to `π`), the expected value of the function `f` stopped at time `τ` is less than or equal to the expected value of the function `f` stopped at time `π`. This result is valid for any natural number `N` such that `π ω` is less than or equal to `N` for all `ω`. The theorem is particularly significant in the context of stochastic processes and their related filtration systems.
More concisely: For a submartingale `f` and bounded stopping times `τ` and `π` with `τ ≤ π` and `π ω ≤ N` for some natural number `N`, we have the inequality `E[f?_τ] ≤ E[f?_π]`.
|
MeasureTheory.Submartingale.stoppedProcess
theorem MeasureTheory.Submartingale.stoppedProcess :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} {τ : Ω → ℕ} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Submartingale f 𝒢 μ →
MeasureTheory.IsStoppingTime 𝒢 τ → MeasureTheory.Submartingale (MeasureTheory.stoppedProcess f τ) 𝒢 μ
This theorem states that, for a given measurable space `Ω`, filtration `𝒢`, measure `μ`, a function `f` from natural numbers `ℕ` to `Ω` to real numbers `ℝ`, and a stopping time `τ`, if `μ` is a finite measure and `f` is a submartingale with respect to `𝒢` and `μ`, then the stopped process of `f` with respect to the stopping time `τ` is also a submartingale with respect to the same `𝒢` and `μ`. In other words, it asserts that stopping a submartingale does not change its submartingale property.
More concisely: If `μ` is a finite measure, `𝒢` is a filtration on a measurable space `Ω`, `f` is a submartingale with respect to `𝒢` and `μ`, and `τ` is a stopping time, then the stopped process `f` at `τ` is also a submartingale with respect to `𝒢` and `μ`.
|
MeasureTheory.submartingale_iff_expected_stoppedValue_mono
theorem MeasureTheory.submartingale_iff_expected_stoppedValue_mono :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Adapted 𝒢 f →
(∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
(MeasureTheory.Submartingale f 𝒢 μ ↔
∀ (τ π : Ω → ℕ),
MeasureTheory.IsStoppingTime 𝒢 τ →
MeasureTheory.IsStoppingTime 𝒢 π →
τ ≤ π →
(∃ N, ∀ (x : Ω), π x ≤ N) →
∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤
∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ)
**The Optional Stopping Theorem** or the Fair Game Theorem states that an adapted integrable process `f`, is a submartingale if and only if for all bounded stopping times `τ` and `π` such that `τ` is less than or equal to `π`, the expected value of the stopped value of `f` at `τ` is less than or equal to the expected value of its stopped value at `π`. Here, an adapted process is a sequence of functions associated with a filtration such that each function is measurable with respect to the associated level of the filtration. A stopping time is a rule for stopping an iterative process based on the information available at the current step. The stopped value of a function with respect to a stopping time is the value of the function at the stopping time.
More concisely: An adapted integrable process `f` is a submartingale if and only if for all bounded stopping times `τ` and `π` with `τ ≤ π`, we have the expectation property: `ℱ-ℙ(τ < ∞) * ⅆℱ τ[f] ≤ ⅆℱ π[f]`, where `ℱ` is the filtration, `ℙ` is the probability measure, and `ⅆℱ` denotes expectation under `ℙ` conditioned on `ℱ`.
|
MeasureTheory.submartingale_of_expected_stoppedValue_mono
theorem MeasureTheory.submartingale_of_expected_stoppedValue_mono :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Adapted 𝒢 f →
(∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
(∀ (τ π : Ω → ℕ),
MeasureTheory.IsStoppingTime 𝒢 τ →
MeasureTheory.IsStoppingTime 𝒢 π →
τ ≤ π →
(∃ N, ∀ (ω : Ω), π ω ≤ N) →
∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ) →
MeasureTheory.Submartingale f 𝒢 μ
This theorem is a converse of the optional stopping theorem. It states that if a process `f` is adapted to a filtration `𝒢` and is integrable, then `f` is a submartingale if the expected value of its stopped values is non-decreasing with respect to the stopping times. Specifically, for any two bounded stopping times `τ` and `π` with `τ` less than or equal to `π`, the expected value of the stopped value of `f` at `τ` is less than or equal to the expected value of its stopped value at `π`.
More concisely: If `f` is an adapted, integrable process in a filtration `𝒢`, then `f` is a submartingale if for all bounded stopping times `τ` and `π` with `τ ≤ π`, we have `�� EXPECTED [f X_τ] ≤ �� EXPECTED [f X_π]`, where `X` denotes the process `f` under consideration.
|
MeasureTheory.maximal_ineq
theorem MeasureTheory.maximal_ineq :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Submartingale f 𝒢 μ →
0 ≤ f →
∀ {ε : NNReal} (n : ℕ),
ε • ↑↑μ {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω} ≤
ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω}, f n ω ∂μ)
This is a statement of Doob's maximal inequality in the context of measure theory. Given a measurable space `Ω`, a measure `μ` on that space, and a filtration `𝒢` indexed by the natural numbers, if `f` is a submartingale with respect to `Ω`, `μ`, and `𝒢` and `f` is nonnegative, then for all nonnegative real numbers `ε` and natural numbers `n`, the measure of the set of `ω` in `Ω` where `ε` is less than or equal to the supremum of `f k ω` for `k` less than or equal to `n` multiplied by `ε` is less than or equal to the integral over the same set of `f n ω`. Note that the supremum is taken over the finiteset of natural numbers less than or equal to `n`.
More concisely: For any measure space `(Ω, μ)`, filtration `𝒢`, and submartingale `f` with respect to `(Ω, μ, 𝒢)` that is nonnegative, for all `ε > 0` and `n ∈ ℕ`, the measure of the set where `ε` is less than the supremum of `f` over the first `n` steps times `ε` is no greater than the integral over this set of `f` at the `n`-th step.
|