Randomized stopping times and stopped distributions

This file proves the claims of Section 3 of the paper on the objects of Duality/Defs.lean.

• The maps x ↦ (t, x^t) and (t, x) ↦ (t, x^t) are measurable (StoppedPath.measurable_mk, StoppedPath.measurable_mk_prod), and so is the value (t, x) ↦ E_t(x) of an adapted process, with E_∞ = limsup_t E_t (measurable_valueAt_prod).
• By Fubini's theorem, randomization preserves the second inequality in eq. (1) (sec3_randomized_proof).
• Q^ξ[{t} × B] = ξ_t Q_t(B), and Q^ξ is the distribution of the path of X ∼ Q stopped at an independent time with distribution ξ (sec3_stopped_alternative_proof).
• The Bayesian mixtures of stopped null distributions, with stopping times that are not randomized, belong to ℬ (sec3_bayes_mixtures_proof).

theorem LogOptimal.StoppedPath.measurable_mk_top {𝒳 : Type u_1} [MeasurableSpace 𝒳] : Measurable fun (x : ℕ → 𝒳) => mk ⊤ x

theorem LogOptimal.StoppedPath.measurable_mk {𝒳 : Type u_1} [MeasurableSpace 𝒳] (t : ℕ∞) : Measurable fun (x : ℕ → 𝒳) => mk t x

At a fixed time t ∈ {0, 1, …} ∪ {∞}, the map x ↦ (t, x^t) is measurable.

theorem LogOptimal.StoppedPath.measurable_mk_prod {𝒳 : Type u_1} [MeasurableSpace 𝒳] : Measurable fun (p : ℕ∞ × (ℕ → 𝒳)) => mk p.1 p.2

theorem LogOptimal.StoppedPath.measurableSet_time_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] {t : ℕ} {B : Set (ℕ → 𝒳)} (hB : MeasurableSet B) : MeasurableSet {p : StoppedPath 𝒳 | p.time = ↑t ∧ p.path ∈ B}

noncomputable def LogOptimal.valueAtPair {𝒳 : Type u_1} (E : ℕ → (ℕ → 𝒳) → ENNReal) (p : ℕ∞ × (ℕ → 𝒳)) : ENNReal

The map (t, x) ↦ E_t(x) on ({0, 1, …} ∪ {∞}) × 𝒳^∞, with E_∞ = limsup_t E_t, so that E_τ(x) is its value at (τ(x), x).

Equations

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

theorem LogOptimal.valueAt_eq_valueAtPair {𝒳 : Type u_1} (E : ℕ → (ℕ → 𝒳) → ENNReal) (τ : (ℕ → 𝒳) → ℕ∞) (x : ℕ → 𝒳) : valueAt E τ x = valueAtPair E (τ x, x)

theorem LogOptimal.measurable_valueAtPair {𝒳 : Type u_1} [MeasurableSpace 𝒳] {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : ∀ (t : ℕ), Measurable (E t)) : Measurable (valueAtPair E)

theorem LogOptimal.measurable_valueAtRandomized {𝒳 : Type u_1} [MeasurableSpace 𝒳] {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : ∀ (t : ℕ), Measurable (E t)) {τ : (ℕ → 𝒳) → ↑unitInterval → ℕ∞} (hτ : Measurable (Function.uncurry τ)) : Measurable (valueAtRandomized E τ)

theorem LogOptimal.lintegral_valueAtRandomized_le_one {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) {P : MeasureTheory.Measure (ℕ → 𝒳)} [MeasureTheory.SFinite P] (hP : P ∈ 𝔓) {τ : (ℕ → 𝒳) → ↑unitInterval → ℕ∞} (hτ : IsRandomizedStoppingTime τ) : ∫⁻ (p : (ℕ → 𝒳) × ↑unitInterval), valueAtRandomized E τ p ∂P.prod MeasureTheory.volume ≤ 1

Randomization preserves validity (Section 3): by Fubini's theorem, E_P{E_{τ(X,U)}} ≤ 1 for every e-process (E_t), every P ∈ 𝔓, and every randomized stopping time τ.

theorem LogOptimal.sec3_randomized_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) : (∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) → ∀ (E : ℕ → (ℕ → 𝒳) → ENNReal), IsEProcess 𝔓 E → ∀ P ∈ 𝔓, ∀ (τ : (ℕ → 𝒳) → ↑unitInterval → ℕ∞), IsRandomizedStoppingTime τ → ∫⁻ (p : (ℕ → 𝒳) × ↑unitInterval), valueAtRandomized E τ p ∂P.prod MeasureTheory.volume ≤ 1

The stopped alternative

theorem LogOptimal.stoppedAlternative_apply {𝒳 : Type u_1} [MeasurableSpace 𝒳] (Q : MeasureTheory.Measure (ℕ → 𝒳)) (T : ℕ) (ξ : Fin (T + 1) → ℝ) {A : Set (StoppedPath 𝒳)} (hA : MeasurableSet A) : (stoppedAlternative Q T ξ) A = ∑ t : Fin (T + 1), ENNReal.ofReal (ξ t) * Q {x : ℕ → 𝒳 | StoppedPath.mk (↑↑t) x ∈ A}

theorem LogOptimal.sec3_stopped_alternative_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (Q : MeasureTheory.Measure (ℕ → 𝒳)) : MeasureTheory.IsProbabilityMeasure Q → ∀ (T : ℕ), ∀ ξ ∈ probVectors T, (∀ (t : Fin (T + 1)) (B : Set (ℕ → 𝒳)), MeasurableSet B → (stoppedAlternative Q T ξ) {p : StoppedPath 𝒳 | p.time = ↑↑t ∧ p.path ∈ B} = ENNReal.ofReal (ξ t) * Q B) ∧ stoppedAlternative Q T ξ = MeasureTheory.Measure.map (fun (p : ℕ∞ × (ℕ → 𝒳)) => StoppedPath.mk p.1 p.2) ((∑ t : Fin (T + 1), ENNReal.ofReal (ξ t) • MeasureTheory.Measure.dirac ↑↑t).prod Q)

Bayesian mixtures of stopped null distributions

theorem LogOptimal.sec3_bayes_mixtures_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Λ : Type u) [MeasurableSpace Λ] (π : MeasureTheory.Measure Λ) (κ : ProbabilityTheory.Kernel Λ (ℕ → 𝒳)) (σ : Λ → (ℕ → 𝒳) → ℕ∞) : MeasureTheory.IsProbabilityMeasure π → ProbabilityTheory.IsMarkovKernel κ → (∀ (a : Λ), κ a ∈ 𝔓) → (Measurable fun (p : Λ × (ℕ → 𝒳)) => σ p.1 p.2) → (∀ (a : Λ), MeasureTheory.IsStoppingTime (dataFiltration 𝒳) (σ a)) → MeasureTheory.Measure.map (fun (p : Λ × (ℕ → 𝒳)) => StoppedPath.mk (σ p.1 p.2) p.2) (π.compProd κ) ∈ stoppedMixtures 𝔓