Randomized stopping times and mixtures of stopped null distributions

This file defines the objects of Section 3 of the paper.

• StoppedPath 𝒳: the space of the pairs (t, x^t) with t ∈ {0, 1, …} ∪ {∞} and x^t ∈ 𝒳^t. A pair is represented by (t, x) with x : ℕ → 𝒳 a whole path, and the σ-algebra is the one under which only x^t is observed: a set A is measurable when, for every t, the set of the paths x with (t, x) ∈ A belongs to ℱ_t (to the product σ-algebra for t = ∞). Two paths with the same first t observations are thus not separated at time t.
• IsRandomizedStoppingTime τ: a measurable map τ : 𝒳^∞ × [0, 1] → {0, 1, …} ∪ {∞} such that τ(·, u) is a stopping time of (ℱ_t) for every u ∈ [0, 1].
• valueAtRandomized E τ: the value E_{τ(X, U)} of a process at a randomized stopping time.
• stoppedLaw P τ: the distribution P^τ of (τ, X^τ) when X ∼ P and U is uniform on [0, 1] and independent of X.
• stoppedAlternative Q T ξ: the distribution Q^ξ with Q^ξ[{t} × B] = ξ_t Q_t(B).
• stoppedMixtures 𝔓: the set ℬ of mixtures P̄ = ∫ P_λ^{τ_λ} π(dλ) of stopped null distributions.

The Kullback–Leibler divergence is InformationTheory.klDiv of Mathlib.

@[instance_reducible]

def LogOptimal.observedSigma (𝒳 : Type u_1) [MeasurableSpace 𝒳] (t : ℕ∞) : MeasurableSpace (ℕ → 𝒳)

The σ-algebra of the observations up to time t ∈ {0, 1, …} ∪ {∞}: ℱ_t for finite t, and the product σ-algebra for t = ∞.

Equations

• LogOptimal.observedSigma 𝒳 t = WithTop.recTopCoe MeasurableSpace.pi (fun (n : ℕ) => ↑(LogOptimal.dataFiltration 𝒳) n) t

def LogOptimal.StoppedPath (𝒳 : Type u_1) : Type u_1

The pairs (t, x^t) of Section 3, represented by pairs (t, x) of a time t ∈ {0, 1, …} ∪ {∞} and a whole path x. The σ-algebra (StoppedPath.instMeasurableSpace) observes only x^t.

Equations

• LogOptimal.StoppedPath 𝒳 = (ℕ∞ × (ℕ → 𝒳))

def LogOptimal.StoppedPath.mk {𝒳 : Type u} (t : ℕ∞) (x : ℕ → 𝒳) : StoppedPath 𝒳

The pair (t, x^t), represented by (t, x).

Equations

• LogOptimal.StoppedPath.mk t x = (t, x)

def LogOptimal.StoppedPath.time {𝒳 : Type u} (p : StoppedPath 𝒳) : ℕ∞

The time t of a pair (t, x^t).

Equations

• p.time = p.1

def LogOptimal.StoppedPath.path {𝒳 : Type u} (p : StoppedPath 𝒳) : ℕ → 𝒳

A path x whose first t observations are x^t, for a pair (t, x^t).

Equations

• p.path = p.2

@[simp]

theorem LogOptimal.StoppedPath.time_mk {𝒳 : Type u} (t : ℕ∞) (x : ℕ → 𝒳) : (mk t x).time = t

@[simp]

theorem LogOptimal.StoppedPath.path_mk {𝒳 : Type u} (t : ℕ∞) (x : ℕ → 𝒳) : (mk t x).path = x

@[instance_reducible]

instance LogOptimal.StoppedPath.instMeasurableSpace {𝒳 : Type u} [MeasurableSpace 𝒳] : MeasurableSpace (StoppedPath 𝒳)

The σ-algebra on the pairs (t, x^t): a set A is measurable when, for every t, the paths x with (t, x) ∈ A form a set of ℱ_t (of the product σ-algebra for t = ∞).

Equations

• One or more equations did not get rendered due to their size.

theorem LogOptimal.StoppedPath.measurableSet_iff {𝒳 : Type u} [MeasurableSpace 𝒳] {A : Set (StoppedPath 𝒳)} : MeasurableSet A ↔ ∀ (t : ℕ∞), MeasurableSet {x : ℕ → 𝒳 | mk t x ∈ A}

theorem LogOptimal.observedSigma_le {𝒳 : Type u} [MeasurableSpace 𝒳] (t : ℕ∞) : observedSigma 𝒳 t ≤ MeasurableSpace.pi

theorem LogOptimal.measurable_mk_coe {𝒳 : Type u} [MeasurableSpace 𝒳] (t : ℕ) : Measurable fun (x : ℕ → 𝒳) => StoppedPath.mk (↑t) x

At a fixed finite time t, the map x ↦ (t, x^t) is measurable.

Randomized stopping times

def LogOptimal.IsRandomizedStoppingTime {𝒳 : Type u} [MeasurableSpace 𝒳] (τ : (ℕ → 𝒳) → ↑unitInterval → ℕ∞) : Prop

A randomized stopping time (Section 3): a measurable map τ : 𝒳^∞ × [0, 1] → {0, 1, …} ∪ {∞} such that τ(·, u) is a stopping time of (ℱ_t) for every u ∈ [0, 1].

Equations

• LogOptimal.IsRandomizedStoppingTime τ = (Measurable (Function.uncurry τ) ∧ ∀ (u : ↑unitInterval), MeasureTheory.IsStoppingTime (LogOptimal.dataFiltration 𝒳) fun (x : ℕ → 𝒳) => τ x u)

noncomputable def LogOptimal.valueAtRandomized {𝒳 : Type u} (E : ℕ → (ℕ → 𝒳) → ENNReal) (τ : (ℕ → 𝒳) → ↑unitInterval → ℕ∞) (p : (ℕ → 𝒳) × ↑unitInterval) : ENNReal

The value E_{τ(X, U)} of a process at a randomized stopping time, as a function of (X, U).

Equations

• LogOptimal.valueAtRandomized E τ p = LogOptimal.valueAt E (fun (x : ℕ → 𝒳) => τ x p.2) p.1

noncomputable def LogOptimal.stoppedLaw {𝒳 : Type u} [MeasurableSpace 𝒳] (P : MeasureTheory.Measure (ℕ → 𝒳)) (τ : (ℕ → 𝒳) → ↑unitInterval → ℕ∞) : MeasureTheory.Measure (StoppedPath 𝒳)

The distribution P^τ of (τ, X^τ) when X ∼ P and U is uniform on [0, 1] and independent of X, with X^τ = (X_t)_{t ≥ 1} on the event {τ = ∞} (Section 3).

Equations

• LogOptimal.stoppedLaw P τ = MeasureTheory.Measure.map (fun (p : (ℕ → 𝒳) × ↑unitInterval) => LogOptimal.StoppedPath.mk (τ p.1 p.2) p.1) (P.prod MeasureTheory.volume)

noncomputable def LogOptimal.stoppedAlternative {𝒳 : Type u} [MeasurableSpace 𝒳] (Q : MeasureTheory.Measure (ℕ → 𝒳)) (T : ℕ) (ξ : Fin (T + 1) → ℝ) : MeasureTheory.Measure (StoppedPath 𝒳)

The distribution Q^ξ on the pairs (t, x^t) with Q^ξ[{t} × B] = ξ_t Q_t(B) for 0 ≤ t ≤ T, for a probability vector ξ ∈ Δ_T (Section 3): the distribution of the path of X ∼ Q stopped at an independent time with distribution ξ.

Equations

• LogOptimal.stoppedAlternative Q T ξ = ∑ t : Fin (T + 1), ENNReal.ofReal (ξ t) • MeasureTheory.Measure.map (fun (x : ℕ → 𝒳) => LogOptimal.StoppedPath.mk (↑↑t) x) Q

def LogOptimal.stoppedMixtures {𝒳 : Type u} [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) : Set (MeasureTheory.Measure (StoppedPath 𝒳))

The set ℬ of mixtures of stopped null distributions (Section 3): the distributions P̄ = ∫ P_λ^{τ_λ} π(dλ), where π is a probability measure on a measurable space, λ ↦ P_λ ∈ 𝔓 is a probability kernel, and (λ, x, u) ↦ τ_λ(x, u) is measurable with τ_λ a randomized stopping time for every λ. The mixture is the distribution of (τ_Λ(X, U), X^{τ_Λ(X, U)}), where Λ ∼ π, X ∼ P_Λ given Λ, and U is uniform on [0, 1] and independent of (Λ, X).

Equations

• One or more equations did not get rendered due to their size.