Operations on e-processes

This file collects operations on e-processes that preserve the second inequality in eq. (1) of the paper, and proves three claims that follow from them.

• measurable_stoppingTime_enat, measurable_eval_truncTime: a stopping time of a filtration indexed by ℕ is measurable, and so is x ↦ E_{τ(x) ∧ T}(x) for an adapted (E_t);
• valueAt_mono_process, IsEProcess.of_le: an adapted process dominated by an e-process is an e-process;
• IsEProcess.lintegral_truncTime_le_one, IsEProcess.stopped: E_P(E_{τ∧T}) ≤ 1, so that the process (E_{t∧T})_{t≥0} stopped at T is an e-process;
• IsEProcess.stopped_add: a combination a E_{t∧T} + b F_{t∧T} of two e-processes stopped at T, with a + b ≤ 1, is an e-process;
• isEProcess_stopped_of_tendsto: by Fatou's lemma, a limit of e-processes at the horizons t ≤ T, stopped at T, is an e-process (the last step of the proof of Proposition S1(i));
• intro_markov_proof: rejection at level α as soon as an e-process reaches 1/α (Section 1);
• sec_eta_monotone_proof: η_T is nondecreasing in T, since τ ∧ T is a stopping time (Example S1);
• sec_methods_snell_proof: a process stopped at T is an e-process if and only if, for each null distribution, some supermartingale up to T dominates it with initial value at most one (Section S4), from Peskir and Shiryaev (2006, Theorem 1.2).

Measurability at stopping times

theorem LogOptimal.measurable_stoppingTime_enat {Ω : Type u_1} {m : MeasurableSpace Ω} {f : MeasureTheory.Filtration ℕ m} {τ : Ω → ℕ∞} (hτ : MeasureTheory.IsStoppingTime f τ) : Measurable τ

A stopping time of a filtration indexed by ℕ, with values in {0, 1, …} ∪ {∞}, is measurable.

theorem LogOptimal.measurable_eval_truncTime {𝒳 : Type u_1} [MeasurableSpace 𝒳] {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : ∀ (t : ℕ), Measurable (E t)) {τ : (ℕ → 𝒳) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration 𝒳) τ) (T : ℕ) : Measurable fun (x : ℕ → 𝒳) => E (truncTime τ T x) x

For an adapted process (E_t) and a stopping time τ, the value x ↦ E_{τ(x) ∧ T}(x) is measurable.

Dominated, stopped, and combined e-processes

theorem LogOptimal.valueAt_mono_process {Ω : Type u_2} {E F : ℕ → Ω → ENNReal} (h : ∀ (t : ℕ) (x : Ω), F t x ≤ E t x) (τ : Ω → ℕ∞) (x : Ω) : valueAt F τ x ≤ valueAt E τ x

The value E_τ is monotone in the process, also on the event {τ = ∞}.

theorem LogOptimal.IsEProcess.of_le {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {E F : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) (hF : ∀ (t : ℕ), Measurable (F t)) (h : ∀ (t : ℕ) (x : ℕ → 𝒳), F t x ≤ E t x) : IsEProcess 𝔓 F

An adapted process dominated by an e-process is an e-process.

theorem LogOptimal.valueAt_min_eq_truncTime {Ω : Type u_2} (E : ℕ → Ω → ENNReal) (τ : Ω → ℕ∞) (T : ℕ) (x : Ω) : valueAt E (fun (x : Ω) => min (τ x) ↑T) x = E (truncTime τ T x) x

The value of a process at the time τ ∧ T is E_{τ∧T}.

theorem LogOptimal.IsEProcess.lintegral_truncTime_le_one {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) {P : MeasureTheory.Measure (ℕ → 𝒳)} (hP : P ∈ 𝔓) {τ : (ℕ → 𝒳) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration 𝒳) τ) (T : ℕ) : ∫⁻ (x : ℕ → 𝒳), E (truncTime τ T x) x ∂P ≤ 1

E_P(E_{τ∧T}) ≤ 1 for an e-process (E_t), a null distribution P, and a stopping time τ, since τ ∧ T is a stopping time.

theorem LogOptimal.IsEProcess.stopped {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) (T : ℕ) : IsEProcess 𝔓 fun (t : ℕ) => E (min t T)

The process (E_{t∧T})_{t≥0} stopped at T is an e-process, with the same values at t ≤ T.

theorem LogOptimal.IsEProcess.stopped_add {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {E F : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) (hF : IsEProcess 𝔓 F) (T : ℕ) {a b : ENNReal} (hab : a + b ≤ 1) : IsEProcess 𝔓 fun (t : ℕ) (x : ℕ → 𝒳) => a * E (min t T) x + b * F (min t T) x

For two e-processes (E_t) and (F_t) and a + b ≤ 1, the process (a E_{t∧T} + b F_{t∧T})_{t≥0} is an e-process.

theorem LogOptimal.isEProcess_stopped_of_tendsto {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {T : ℕ} {G : ℕ → (ℕ → 𝒳) → ENNReal} (hG : ∀ (t : ℕ), Measurable (G t)) {F : ℕ → ℕ → (ℕ → 𝒳) → ENNReal} (hF : ∀ (n : ℕ), IsEProcess 𝔓 (F n)) (hconv : ∀ P ∈ 𝔓, ∀ᵐ (x : ℕ → 𝒳) ∂P, ∀ t ≤ T, Filter.Tendsto (fun (n : ℕ) => F n t x) Filter.atTop (nhds (G t x))) : IsEProcess 𝔓 fun (t : ℕ) => G (min t T)

Limits of e-processes (the last step of the proof of Proposition S1(i)): if e-processes (F^n_t) converge to an adapted (G_t) at every t ≤ T, almost surely under every null distribution, then (G_{t∧T})_{t≥0} is an e-process, by Fatou's lemma at the stopping times τ ∧ T.

Section S4: e-processes stopped at T and dominating supermartingales

theorem LogOptimal.supermartingale_stopped_of_le {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P : MeasureTheory.Measure (ℕ → 𝒳)} [MeasureTheory.IsProbabilityMeasure P] {T : ℕ} {Ψ : ℕ → (ℕ → 𝒳) → ℝ} (hΨ : MeasureTheory.Adapted (dataFiltration 𝒳) Ψ) (hint : ∀ (t : ℕ), MeasureTheory.Integrable (Ψ t) P) (hsup : ∀ t < T, P[Ψ (t + 1) | ↑(dataFiltration 𝒳) t] ≤ᵐ[P] Ψ t) : MeasureTheory.Supermartingale (fun (t : ℕ) => Ψ (min t T)) (dataFiltration 𝒳) P

A process that is a supermartingale up to T, stopped at T, is a supermartingale.

Rejection at level α, the monotonicity of η_T, and Section S4

theorem LogOptimal.intro_markov_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) : (∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) → ∀ (E : ℕ → (ℕ → 𝒳) → ENNReal), IsEProcess 𝔓 E → ∀ (α : ℝ), 0 < α → ∀ P ∈ 𝔓, P {x : ℕ → 𝒳 | ∃ (t : ℕ), ENNReal.ofReal (1 / α) ≤ E t x} ≤ ENNReal.ofReal α

theorem LogOptimal.sec_eta_monotone_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Es : ℕ → (ℕ → 𝒳) → ENNReal) : Monotone (eta 𝔓 Es)

theorem LogOptimal.sec_methods_snell_proof : PeskirShiryaevTheorem12 → ∀ (𝒳 : Type u) [inst : MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))), (∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) → ∀ (T : ℕ) (E : ℕ → (ℕ → 𝒳) → NNReal), (∀ (t : ℕ), Measurable (E t)) → (∀ (t : ℕ), E t = E (min t T)) → ((IsEProcess 𝔓 fun (t : ℕ) (x : ℕ → 𝒳) => ↑(E t x)) ↔ ∀ P ∈ 𝔓, ∃ (Ψ : ℕ → (ℕ → 𝒳) → ℝ), MeasureTheory.Adapted (dataFiltration 𝒳) Ψ ∧ (∀ (t : ℕ), MeasureTheory.Integrable (Ψ t) P) ∧ (∀ t < T, P[Ψ (t + 1) | ↑(dataFiltration 𝒳) t] ≤ᵐ[P] Ψ t) ∧ (∀ t ≤ T, (fun (x : ℕ → 𝒳) => ↑(E t x)) ≤ᵐ[P] Ψ t) ∧ ∀ (x : ℕ → 𝒳), Ψ 0 x ≤ 1)