Stochastic intervals

This file defines the stochastic intervals [[σ,τ]], [[σ,τ[[, ]]σ,τ]], ]]σ,τ[[ and the graph [[σ]] (blueprint def:stochasticInterval), and proves that ]]σ,τ]] is an ElementaryPredictableSet for bounded stopping times on ℕ (blueprint lem:elementaryPredictableSet_stochasticInterval, issue https://github.com/RemyDegenne/brownian-motion/issues/440).

For σ, τ : Ω → T ∪ {∞} (modelled as Ω → WithTop ι) over a time domain ι, a stochastic interval is the subset of ι × Ω cut out by comparing the time coordinate with σ and τ. Note these are subsets of ι × Ω, not of WithTop ι × Ω — the time coordinate is a genuine time.

Main definitions

• stochIcc, stochIco, stochIoc, stochIoo — the four stochastic intervals [[σ,τ]], [[σ,τ[[, ]]σ,τ]], ]]σ,τ[[.
• stochGraph — the graph [[σ]] = {(t, ω) | t = σ ω}.

Main results

• stochIoc.exists_elementaryPredictableSet — for stopping times σ, τ with τ bounded by n on ℕ, the interval ]]σ,τ]] is an ElementaryPredictableSet. It decomposes as the finite disjoint union ⋃_{i < n} (i, i+1] × {σ ≤ i < τ} of predictable rectangles, which is exactly the data of an ElementaryPredictableSet. Only τ need be bounded (not σ).

Stochastic intervals (general time domain)

def ProbabilityTheory.stochIcc {ι : Type u_1} {Ω : Type u_2} [Preorder ι] (σ τ : Ω → WithTop ι) : Set (ι × Ω)

The closed stochastic interval [[σ, τ]] = {(t, ω) | σ ω ≤ t ≤ τ ω}.

Equations

• ProbabilityTheory.stochIcc σ τ = {p : ι × Ω | σ p.2 ≤ ↑p.1 ∧ ↑p.1 ≤ τ p.2}

def ProbabilityTheory.stochIco {ι : Type u_1} {Ω : Type u_2} [Preorder ι] (σ τ : Ω → WithTop ι) : Set (ι × Ω)

The right-open stochastic interval [[σ, τ[[ = {(t, ω) | σ ω ≤ t < τ ω}.

Equations

• ProbabilityTheory.stochIco σ τ = {p : ι × Ω | σ p.2 ≤ ↑p.1 ∧ ↑p.1 < τ p.2}

def ProbabilityTheory.stochIoc {ι : Type u_1} {Ω : Type u_2} [Preorder ι] (σ τ : Ω → WithTop ι) : Set (ι × Ω)

The left-open stochastic interval ]]σ, τ]] = {(t, ω) | σ ω < t ≤ τ ω}.

Equations

• ProbabilityTheory.stochIoc σ τ = {p : ι × Ω | σ p.2 < ↑p.1 ∧ ↑p.1 ≤ τ p.2}

def ProbabilityTheory.stochIoo {ι : Type u_1} {Ω : Type u_2} [Preorder ι] (σ τ : Ω → WithTop ι) : Set (ι × Ω)

The open stochastic interval ]]σ, τ[[ = {(t, ω) | σ ω < t < τ ω}.

Equations

• ProbabilityTheory.stochIoo σ τ = {p : ι × Ω | σ p.2 < ↑p.1 ∧ ↑p.1 < τ p.2}

def ProbabilityTheory.stochGraph {ι : Type u_1} {Ω : Type u_2} (σ : Ω → WithTop ι) : Set (ι × Ω)

The graph of a stopping time [[σ]] = {(t, ω) | t = σ ω}.

Equations

• ProbabilityTheory.stochGraph σ = {p : ι × Ω | ↑p.1 = σ p.2}

@[simp]

theorem ProbabilityTheory.mem_stochIcc {ι : Type u_1} {Ω : Type u_2} [Preorder ι] {σ τ : Ω → WithTop ι} {t : ι} {ω : Ω} : (t, ω) ∈ stochIcc σ τ ↔ σ ω ≤ ↑t ∧ ↑t ≤ τ ω

@[simp]

theorem ProbabilityTheory.mem_stochIco {ι : Type u_1} {Ω : Type u_2} [Preorder ι] {σ τ : Ω → WithTop ι} {t : ι} {ω : Ω} : (t, ω) ∈ stochIco σ τ ↔ σ ω ≤ ↑t ∧ ↑t < τ ω

@[simp]

theorem ProbabilityTheory.mem_stochIoc {ι : Type u_1} {Ω : Type u_2} [Preorder ι] {σ τ : Ω → WithTop ι} {t : ι} {ω : Ω} : (t, ω) ∈ stochIoc σ τ ↔ σ ω < ↑t ∧ ↑t ≤ τ ω

@[simp]

theorem ProbabilityTheory.mem_stochIoo {ι : Type u_1} {Ω : Type u_2} [Preorder ι] {σ τ : Ω → WithTop ι} {t : ι} {ω : Ω} : (t, ω) ∈ stochIoo σ τ ↔ σ ω < ↑t ∧ ↑t < τ ω

@[simp]

theorem ProbabilityTheory.mem_stochGraph {ι : Type u_1} {Ω : Type u_2} {σ : Ω → WithTop ι} {t : ι} {ω : Ω} : (t, ω) ∈ stochGraph σ ↔ ↑t = σ ω

theorem ProbabilityTheory.stochGraph_eq_stochIcc {ι : Type u_1} {Ω : Type u_2} [PartialOrder ι] (σ : Ω → WithTop ι) : stochGraph σ = stochIcc σ σ

The graph is the diagonal stochastic interval, [[σ]] = [[σ, σ]].

]]σ,τ]] on ℕ: an elementary predictable set

The blueprint decomposition ]]σ,τ]] = ⋃ₖ (k-1, k] × {σ ≤ k-1 < τ}. We index by the left endpoint i = k - 1, so the building blocks are (i, i+1] × {σ ≤ i < τ} for i : ℕ.

theorem ProbabilityTheory.stochIoc.measurableSet_slice {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ℕ mΩ} {σ τ : Ω → ℕ∞} (hσ : MeasureTheory.IsStoppingTime 𝓕 σ) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) (i : ℕ) : MeasurableSet {ω : Ω | σ ω ≤ ↑i ∧ ↑i < τ ω}

The slice {ω | σ ω ≤ i < τ ω} over the interval (i, i+1]. It is 𝓕 i-measurable for stopping times σ, τ: it is {σ ≤ i} ∩ {τ ≤ i}ᶜ.

theorem ProbabilityTheory.stochIoc.eq_iUnion {Ω : Type u_2} (σ τ : Ω → ℕ∞) : stochIoc σ τ = ⋃ (i : ℕ), Set.Ioc i (i + 1) ×ˢ {ω : Ω | σ ω ≤ ↑i ∧ ↑i < τ ω}

]]σ,τ]] = ⋃ᵢ (i, i+1] × {σ ≤ i < τ} as subsets of ℕ × Ω — a purely arithmetic identity on ℕ∞, valid for any σ, τ.

theorem ProbabilityTheory.stochIoc.exists_elementaryPredictableSet {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ℕ mΩ} {σ τ : Ω → ℕ∞} (hσ : MeasureTheory.IsStoppingTime 𝓕 σ) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) {n : ℕ} (hτn : ∀ (ω : Ω), τ ω ≤ ↑n) : ∃ (S : ElementaryPredictableSet 𝓕), ↑S = stochIoc σ τ

]]σ,τ]] is an elementary predictable set for bounded stopping times on ℕ (blueprint lem:elementaryPredictableSet_stochasticInterval). With τ ≤ n, ]]σ,τ]] = ⋃_{i < n} (i, i+1] × {σ ≤ i < τ} is a finite disjoint union of predictable rectangles, which is exactly the data of an ElementaryPredictableSet.