Documentation

LogOptimalEProcesses.EProcess.SimpleNull

A simple null #

This file proves the claim of Section 1 of the paper on a simple null 𝒫 = {P}: under the standing assumption, Q_t is absolutely continuous with respect to P_t, the likelihood ratios E*_t = dQ_t/dP_t of the first t observations are numΓ©raires and form a test martingale with respect to (β„±_t), and Ξ“_T = 0 for every T and every choice of numΓ©raires.

The first t observations #

source
theorem LogOptimal.measurable_pathPrefix {𝒳 : Type u_1} [MeasurableSpace 𝒳] (t : β„•) :
Measurable fun (x : β„• β†’ 𝒳) (i : Fin t) => x ↑i
source
theorem LogOptimal.measurable_pathPrefix_dataFiltration {𝒳 : Type u_1} [MeasurableSpace 𝒳] (t : β„•) :
Measurable fun (x : β„• β†’ 𝒳) (i : Fin t) => x ↑i
source
theorem LogOptimal.dataFiltration_le_comap_pathPrefix {𝒳 : Type u_1} [MeasurableSpace 𝒳] (t : β„•) :
↑(dataFiltration 𝒳) t ≀ MeasurableSpace.comap (fun (x : β„• β†’ 𝒳) (i : Fin t) => x ↑i) MeasurableSpace.pi
source
theorem LogOptimal.marginal_apply_of_measurableSet {𝒳 : Type u_1} [MeasurableSpace 𝒳] (P : MeasureTheory.Measure (β„• β†’ 𝒳)) {t : β„•} {B : Set (Fin t β†’ 𝒳)} (hB : MeasurableSet B) :
(marginal P t) B = P ((fun (x : β„• β†’ 𝒳) (i : Fin t) => x ↑i) ⁻¹' B)
source
theorem LogOptimal.lintegral_marginal_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] (P : MeasureTheory.Measure (β„• β†’ 𝒳)) {t : β„•} {f : (Fin t β†’ 𝒳) β†’ ENNReal} (hf : Measurable f) :
∫⁻ (y : Fin t β†’ 𝒳), f y βˆ‚marginal P t = ∫⁻ (x : β„• β†’ 𝒳), f fun (i : Fin t) => x ↑i βˆ‚P
source
theorem LogOptimal.setLIntegral_marginal_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] (P : MeasureTheory.Measure (β„• β†’ 𝒳)) {t : β„•} {f : (Fin t β†’ 𝒳) β†’ ENNReal} (hf : Measurable f) {B : Set (Fin t β†’ 𝒳)} (hB : MeasurableSet B) :
∫⁻ (y : Fin t β†’ 𝒳) in B, f y βˆ‚marginal P t = ∫⁻ (x : β„• β†’ 𝒳) in (fun (x : β„• β†’ 𝒳) (i : Fin t) => x ↑i) ⁻¹' B, f fun (i : Fin t) => x ↑i βˆ‚P
source
theorem LogOptimal.marginal_isProbabilityMeasure {𝒳 : Type u_1} [MeasurableSpace 𝒳] (P : MeasureTheory.Measure (β„• β†’ 𝒳)) [MeasureTheory.IsProbabilityMeasure P] (t : β„•) :
MeasureTheory.IsProbabilityMeasure (marginal P t)

Likelihood ratios for a simple null #

source
theorem LogOptimal.marginal_absolutelyContinuous {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} [MeasureTheory.IsProbabilityMeasure P] (hfin : FiniteOptimalEPower {P} Q) (t : β„•) :
(marginal Q t).AbsolutelyContinuous (marginal P t)

Under the standing assumption, Q_t is absolutely continuous with respect to P_t, by the argument of the proof of Proposition S1(i): for a set B with P_t(B) = 0 < Q_t(B), the e-variable 1 + ∞ 1(X^t ∈ B) (the paper takes 1 + m 1(X^t ∈ B) and lets m β†’ ∞) would have infinite e-power.

source
theorem LogOptimal.measure_eq_setLIntegral_rnDeriv {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] {t : β„•} (hac : (marginal Q t).AbsolutelyContinuous (marginal P t)) {A : Set (β„• β†’ 𝒳)} (hA : MeasurableSet A) :
Q A = ∫⁻ (x : β„• β†’ 𝒳) in A, (marginal Q t).rnDeriv (marginal P t) fun (i : Fin t) => x ↑i βˆ‚P

The change of measure on β„±_t: Q(A) = E_P{E*_t 1(A)} for A ∈ β„±_t, where E*_t = dQ_t/dP_t.

source
theorem LogOptimal.lintegral_eq_lintegral_mul_rnDeriv {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] {t : β„•} (hac : (marginal Q t).AbsolutelyContinuous (marginal P t)) {H : (β„• β†’ 𝒳) β†’ ENNReal} (hH : Measurable H) :
∫⁻ (x : β„• β†’ 𝒳), H x βˆ‚Q = ∫⁻ (x : β„• β†’ 𝒳), ((marginal Q t).rnDeriv (marginal P t) fun (i : Fin t) => x ↑i) * H x βˆ‚P

The change of measure on β„±_t: E_Q(H) = E_P(E*_t H) for an β„±_t-measurable H β‰₯ 0, where E*_t = dQ_t/dP_t.

source
theorem LogOptimal.measurable_rnDeriv_dataFiltration {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} (t : β„•) :
Measurable fun (x : β„• β†’ 𝒳) => (marginal Q t).rnDeriv (marginal P t) fun (i : Fin t) => x ↑i
source
theorem LogOptimal.measurable_rnDeriv_pathPrefix {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} (t : β„•) :
Measurable fun (x : β„• β†’ 𝒳) => (marginal Q t).rnDeriv (marginal P t) fun (i : Fin t) => x ↑i
source
theorem LogOptimal.lintegral_rnDeriv_marginal {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hfin : FiniteOptimalEPower {P} Q) (t : β„•) :
∫⁻ (x : β„• β†’ 𝒳), (marginal Q t).rnDeriv (marginal P t) fun (i : Fin t) => x ↑i βˆ‚P = 1
source
theorem LogOptimal.isNumeraire_rnDeriv {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hfin : FiniteOptimalEPower {P} Q) (t : β„•) :
IsNumeraire {P} Q t fun (x : β„• β†’ 𝒳) => (marginal Q t).rnDeriv (marginal P t) fun (i : Fin t) => x ↑i

The likelihood ratio E*_t = dQ_t/dP_t is a numΓ©raire at horizon t for the simple null {P}: it is an e-variable, and E_Q(E/E*_t) = E_P{E*_t (E/E*_t)} ≀ E_P(E) ≀ 1 for every E ∈ β„°_t, by the change of measure on β„±_t (Larsson, Ramdas and Ruf, 2025, Example 2.2).

source
theorem LogOptimal.ae_rnDeriv_lt_top {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hfin : FiniteOptimalEPower {P} Q) (t : β„•) :
βˆ€α΅ (x : β„• β†’ 𝒳) βˆ‚P, ((marginal Q t).rnDeriv (marginal P t) fun (i : Fin t) => x ↑i) < ⊀
source
theorem LogOptimal.rnDeriv_marginal_zero {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (x : β„• β†’ 𝒳) :
((marginal Q 0).rnDeriv (marginal P 0) fun (i : Fin 0) => x ↑i) = 1

At t = 0, E*_0 = dQ_0/dP_0 = 1 at every path, since Q_0 = P_0 is the unit mass on the single point of 𝒳^0.

source
theorem LogOptimal.isTestMartingale_rnDeriv {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hfin : FiniteOptimalEPower {P} Q) :
IsTestMartingale {P} (dataFiltration 𝒳) fun (t : β„•) (x : β„• β†’ 𝒳) => ((marginal Q t).rnDeriv (marginal P t) fun (i : Fin t) => x ↑i).toReal

The likelihood ratios E*_t = dQ_t/dP_t form a test martingale with respect to (β„±_t) under P: for A ∈ β„±_t, E_P{E*_{t+1} 1(A)} = Q(A) = E_P{E*_t 1(A)} by the change of measure.

source
theorem LogOptimal.isEProcess_stopped_rnDeriv {𝒳 : Type u_1} [MeasurableSpace 𝒳] {P Q : MeasureTheory.Measure (β„• β†’ 𝒳)} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hfin : FiniteOptimalEPower {P} Q) (T : β„•) :
IsEProcess {P} fun (t : β„•) (x : β„• β†’ 𝒳) => (marginal Q (min t T)).rnDeriv (marginal P (min t T)) fun (i : Fin (min t T)) => x ↑i

The likelihood ratios stopped at T form an e-process: at a stopping time Ο„, their value is E*_{Ο„ ∧ T}, and optional stopping at the bounded time Ο„ ∧ T gives E_P(E*_{Ο„ ∧ T}) ≀ 1.

source
theorem LogOptimal.intro_simple_null_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (P Q : MeasureTheory.Measure (β„• β†’ 𝒳)) :
MeasureTheory.IsProbabilityMeasure P β†’ MeasureTheory.IsProbabilityMeasure Q β†’ FiniteOptimalEPower {P} Q β†’ have Es := fun (t : β„•) (x : β„• β†’ 𝒳) => (marginal Q t).rnDeriv (marginal P t) fun (i : Fin t) => x ↑i; (βˆ€ (t : β„•), (marginal Q t).AbsolutelyContinuous (marginal P t)) ∧ (βˆ€ (t : β„•), IsNumeraire {P} Q t (Es t)) ∧ (IsTestMartingale {P} (dataFiltration 𝒳) fun (t : β„•) (x : β„• β†’ 𝒳) => (Es t x).toReal) ∧ βˆ€ (Es' : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal), (βˆ€ (t : β„•), IsNumeraire {P} Q t (Es' t)) β†’ βˆ€ (T : β„•), minimaxRegret {P} Q Es' T = 0