Test supermartingales and Ville's inequality

This file proves that test supermartingales with respect to (ℱ_t) are e-processes (Section 1 of the paper), and Ville's inequality for e-processes and test supermartingales.

• integral_stoppedValue_le_of_supermartingale: optional stopping at bounded times, E_P(M_σ) ≤ E_P(M_0) for a supermartingale and a bounded stopping time σ;
• lintegral_valueAt_le_of_supermartingale: E_P(M_τ) ≤ E_P(M_0) for a nonnegative supermartingale at every stopping time τ with values in {0, 1, …} ∪ {∞}, with M_∞ = limsup_t M_t, by optional stopping at the bounded times τ ∧ n, the almost sure convergence of (M_n) (Doob's convergence theorem), and Fatou's lemma;
• IsTestSupermartingale.isEProcess and intro_test_supermartingale_proof: a test supermartingale with respect to (ℱ_t) is an e-process;
• IsEProcess.measure_exists_ge_le and IsTestSupermartingale.measure_exists_ge_le: Ville's inequality P(∃ t, M_t ≥ c) ≤ 1/c, from the e-process property at the hitting time of [c, ∞].

Truncated times

theorem LogOptimal.untopA_min_eq_truncTime {Ω : Type u_1} (τ : Ω → ℕ∞) (T : ℕ) (x : Ω) : WithTop.untopA (min (τ x) ↑T) = truncTime τ T x

theorem LogOptimal.truncTime_of_eq_coe {Ω : Type u_1} {τ : Ω → ℕ∞} {x : Ω} {k T : ℕ} (h : τ x = ↑k) (hk : k ≤ T) : truncTime τ T x = k

Nonnegative supermartingales at stopping times

theorem LogOptimal.integral_stoppedValue_le_of_supermartingale {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {ℱ : MeasureTheory.Filtration ℕ mΩ} {M : ℕ → Ω → ℝ} (hM : MeasureTheory.Supermartingale M ℱ P) {σ : Ω → ℕ∞} (hσ : MeasureTheory.IsStoppingTime ℱ σ) {N : ℕ} (hbdd : ∀ (ω : Ω), σ ω ≤ ↑N) : ∫ (ω : Ω), MeasureTheory.stoppedValue M σ ω ∂P ≤ ∫ (ω : Ω), M 0 ω ∂P

Optional stopping at bounded times for a supermartingale: E_P(M_σ) ≤ E_P(M_0) for every stopping time σ bounded by N.

theorem LogOptimal.stoppedValue_min_eq {Ω : Type u_1} (M : ℕ → Ω → ℝ) (τ : Ω → ℕ∞) (n : ℕ) : (MeasureTheory.stoppedValue M fun (ω : Ω) => min (τ ω) ↑n) = fun (ω : Ω) => M (truncTime τ n ω) ω

theorem LogOptimal.lintegral_truncTime_le_of_supermartingale {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {ℱ : MeasureTheory.Filtration ℕ mΩ} {M : ℕ → Ω → ℝ} (hM : MeasureTheory.Supermartingale M ℱ P) (hnn : ∀ (t : ℕ) (ω : Ω), 0 ≤ M t ω) {τ : Ω → ℕ∞} (hτ : MeasureTheory.IsStoppingTime ℱ τ) (n : ℕ) : ∫⁻ (ω : Ω), ENNReal.ofReal (M (truncTime τ n ω) ω) ∂P ≤ ENNReal.ofReal (∫ (ω : Ω), M 0 ω ∂P)

Optional stopping at the bounded time τ ∧ n for a nonnegative supermartingale: E_P(M_{τ ∧ n}) ≤ E_P(M_0), written in [0, ∞].

theorem LogOptimal.lintegral_valueAt_le_of_supermartingale {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {ℱ : MeasureTheory.Filtration ℕ mΩ} {M : ℕ → Ω → ℝ} (hM : MeasureTheory.Supermartingale M ℱ P) (hnn : ∀ (t : ℕ) (ω : Ω), 0 ≤ M t ω) {τ : Ω → ℕ∞} (hτ : MeasureTheory.IsStoppingTime ℱ τ) : ∫⁻ (ω : Ω), valueAt (fun (t : ℕ) (ω : Ω) => ENNReal.ofReal (M t ω)) τ ω ∂P ≤ ENNReal.ofReal (∫ (ω : Ω), M 0 ω ∂P)

A nonnegative supermartingale M satisfies E_P(M_τ) ≤ E_P(M_0) at every stopping time τ with values in {0, 1, …} ∪ {∞}, with M_∞ = limsup_t M_t: optional stopping at the bounded times τ ∧ n, the almost sure convergence of (M_n) (Doob's convergence theorem), so that M_{τ ∧ n} → M_τ almost surely, and Fatou's lemma.

Test supermartingales are e-processes

theorem LogOptimal.IsTestSupermartingale.isEProcess {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) {M : ℕ → (ℕ → 𝒳) → ℝ} (hM : IsTestSupermartingale 𝔓 (dataFiltration 𝒳) M) : IsEProcess 𝔓 fun (t : ℕ) (x : ℕ → 𝒳) => ENNReal.ofReal (M t x)

Test supermartingales with respect to (ℱ_t) are e-processes (Section 1): the process is adapted, and E_P(M_τ) ≤ E_P(M_0) = 1 at every stopping time τ by lintegral_valueAt_le_of_supermartingale.

theorem LogOptimal.IsEProcess.measure_exists_ge_le {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) {P : MeasureTheory.Measure (ℕ → 𝒳)} (hP : P ∈ 𝔓) (c : ENNReal) : P {x : ℕ → 𝒳 | ∃ (t : ℕ), c ≤ E t x} ≤ c⁻¹

Ville's inequality for e-processes: for an e-process (E_t), a null distribution P, and c ∈ [0, ∞], P(∃ t, E_t ≥ c) ≤ 1/c. It follows from the e-process property at the hitting time τ of [c, ∞], since E_τ ≥ c on the event {∃ t, E_t ≥ c}.

theorem LogOptimal.IsTestSupermartingale.measure_exists_ge_le {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) {M : ℕ → (ℕ → 𝒳) → ℝ} (hM : IsTestSupermartingale 𝔓 (dataFiltration 𝒳) M) {P : MeasureTheory.Measure (ℕ → 𝒳)} (hP : P ∈ 𝔓) {c : ℝ} (hc : 0 < c) : P {x : ℕ → 𝒳 | ∃ (t : ℕ), c ≤ M t x} ≤ ENNReal.ofReal (1 / c)

Ville's inequality for test supermartingales with respect to (ℱ_t): for every null distribution P and every c > 0, P(∃ t, M_t ≥ c) ≤ 1/c.

theorem LogOptimal.intro_test_supermartingale_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) : (∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) → ∀ (M : ℕ → (ℕ → 𝒳) → ℝ), IsTestSupermartingale 𝔓 (dataFiltration 𝒳) M → IsEProcess 𝔓 fun (t : ℕ) (x : ℕ → 𝒳) => ENNReal.ofReal (M t x)