Ville's inequality in an arbitrary filtration

This file extends Ville's inequality of EProcess/Supermartingale.lean from the data filtration (ℱ_t) to an arbitrary filtration. Section 5 of the paper applies it to the filtration (𝒢_t) generated by the variables Y_i, with respect to which the conditional e-variables form a test martingale.

• mul_measure_exists_ge_le_of_supermartingale: for a nonnegative supermartingale (M_t) with respect to a filtration 𝒢 and for c ∈ [0, ∞], c P(∃ t, M_t ≥ c) ≤ E_P(M_0), from the bound E_P(M_τ) ≤ E_P(M_0) of lintegral_valueAt_le_of_supermartingale at the hitting time τ of [c, ∞], a stopping time of 𝒢;
• IsTestSupermartingale.measure_exists_ge_le_of_filtration: Ville's inequality P(∃ t, M_t ≥ c) ≤ 1/c for a test supermartingale with respect to any filtration.

noncomputable def LogOptimal.hittingTimeGe {Ω : Type u_1} (E : ℕ → Ω → ENNReal) (c : ENNReal) (ω : Ω) : ℕ∞

The hitting time of [c, ∞] by a process (E_t) with values in [0, ∞]: the first t with E_t ≥ c, or ∞ if there is none.

Equations

• LogOptimal.hittingTimeGe E c ω = if h : ∃ (t : ℕ), c ≤ E t ω then ↑(Nat.find h) else ⊤

theorem LogOptimal.isStoppingTime_hittingTimeGe {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {𝒢 : MeasureTheory.Filtration ℕ mΩ} {E : ℕ → Ω → ENNReal} (hE : ∀ (t : ℕ), Measurable (E t)) (c : ENNReal) : MeasureTheory.IsStoppingTime 𝒢 (hittingTimeGe E c)

The hitting time of [c, ∞] by an adapted process is a stopping time.

theorem LogOptimal.indicator_le_valueAt_hittingTimeGe {Ω : Type u_1} (E : ℕ → Ω → ENNReal) (c : ENNReal) (ω : Ω) : {ω : Ω | ∃ (t : ℕ), c ≤ E t ω}.indicator (fun (x : Ω) => c) ω ≤ valueAt E (hittingTimeGe E c) ω

At its hitting time of [c, ∞], a process takes a value at least c on the event {∃ t, E_t ≥ c}.

theorem LogOptimal.mul_measure_exists_ge_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 ω) (c : ENNReal) : c * P {ω : Ω | ∃ (t : ℕ), c ≤ ENNReal.ofReal (M t ω)} ≤ ENNReal.ofReal (∫ (ω : Ω), M 0 ω ∂P)

Ville's inequality for a nonnegative supermartingale (M_t) with respect to any filtration 𝒢: c P(∃ t, M_t ≥ c) ≤ E_P(M_0) for every c ∈ [0, ∞].

theorem LogOptimal.IsTestSupermartingale.measure_exists_ge_le_of_filtration {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {𝒢 : MeasureTheory.Filtration ℕ mΩ} {M : ℕ → Ω → ℝ} {𝔓 : Set (MeasureTheory.Measure Ω)} (hM : IsTestSupermartingale 𝔓 𝒢 M) (hP : P ∈ 𝔓) {c : ℝ} (hc : 0 < c) : P {ω : Ω | ∃ (t : ℕ), ENNReal.ofReal c ≤ ENNReal.ofReal (M t ω)} ≤ ENNReal.ofReal (1 / c)

Ville's inequality for a test supermartingale with respect to any filtration 𝒢: for every null distribution P and every c > 0, P(∃ t, M_t ≥ c) ≤ 1/c.