E-variables, e-processes, numéraires, and the minimax regret

This file defines the objects of Sections 1 and 2 of the paper. The observations X₁, X₂, … take values in a measurable space 𝒳, and a path is a sequence x : ℕ → 𝒳, whose coordinate x i is the observation X_{i+1} of the paper. The first t observations X^t = (X₁, …, X_t) are the coordinates x i with i < t.

• dataFiltration 𝒳: the filtration (ℱ_t)_{t ≥ 0} generated by X, with ℱ₀ trivial;
• IsEVariable 𝔓 t E: E is an e-variable at horizon t for the null 𝔓, that is, E ∈ ℰ_t, the first inequality in eq. (1);
• valueAt E τ: the value E_τ of a process at a time τ with values in {0, 1, …} ∪ {∞}, with E_∞ = limsup_{t → ∞} E_t;
• IsEProcess 𝔓 E: (E_t) is an e-process, the second inequality in eq. (1);
• IsNumeraire 𝔓 Q t E: E is a numéraire at horizon t, the first property in eq. (2);
• eIntegral μ g: the integral of a function g with values in [−∞, ∞];
• ePower Q E: the e-power E_Q(log E) of E;
• regret Q Es E: the regret R_t(E) = E_Q{log(E*_t/E)} of eq. (3), with Es = E*_t;
• minimaxRegret 𝔓 Q Es T: the minimax regret Γ_T of eq. (3);
• FiniteOptimalEPower 𝔓 Q: the standing assumption sup_{E ∈ ℰ_t} E_Q(log E) < ∞ of Section 2;
• eta 𝔓 Es T: the supremum η_T of eq. (4);
• snell P ℱ G N: the Snell envelope of a process by backward induction, and snellEnvelope P Es T the Snell envelope (Λ^P_t)_{0 ≤ t ≤ T} of Section 2;
• marginal P t: the distribution P_t of X^t under P;
• probVectors T: the set Δ_T of probability vectors (ξ₀, …, ξ_T);
• IsTestSupermartingale and IsTestMartingale: test (super)martingales with respect to a filtration, Section 1.

Conventions. E-variables and e-processes take values in [0, ∞], as in the paper. An expectation in [−∞, ∞] is eIntegral, the integral of the positive part minus the integral of the negative part in EReal. It is the expectation of the paper whenever one of the two parts is integrable, which is the convention of Section S1; when both integrals are infinite, its value is ⊥. Ratios are taken in [0, ∞], where 0/0 = 0 and ∞/∞ = 0. Since a numéraire is positive and finite Q-almost surely, these conventions do not affect the regrets.

The data filtration

def LogOptimal.dataFiltration (𝒳 : Type u_2) [MeasurableSpace 𝒳] : MeasureTheory.Filtration ℕ MeasurableSpace.pi

The filtration (ℱ_t)_{t ≥ 0} generated by X = (X_t)_{t ≥ 1} (Section 1): ℱ_t is generated by the first t observations, the coordinates x i with i < t, and ℱ₀ is trivial.

Equations

• LogOptimal.dataFiltration 𝒳 = { seq := fun (t : ℕ) => ⨆ (i : ℕ), ⨆ (_ : i < t), MeasurableSpace.comap (fun (x : ℕ → 𝒳) => x i) inst✝, mono' := ⋯, le' := ⋯ }

theorem LogOptimal.measurable_coord_dataFiltration {𝒳 : Type u_1} [MeasurableSpace 𝒳] {i t : ℕ} (h : i < t) : Measurable fun (x : ℕ → 𝒳) => x i

noncomputable def LogOptimal.marginal {𝒳 : Type u_1} [MeasurableSpace 𝒳] (P : MeasureTheory.Measure (ℕ → 𝒳)) (t : ℕ) : MeasureTheory.Measure (Fin t → 𝒳)

The distribution P_t of X^t = (X₁, …, X_t) under a distribution P of X.

Equations

• LogOptimal.marginal P t = MeasureTheory.Measure.map (fun (x : ℕ → 𝒳) (i : Fin t) => x ↑i) P

E-variables and e-processes

def LogOptimal.IsEVariable {𝒳 : Type u_1} [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (t : ℕ) (E : (ℕ → 𝒳) → ENNReal) : Prop

E is an e-variable at horizon t for the null 𝔓, E ∈ ℰ_t (Section 1): an ℱ_t-measurable random variable with values in [0, ∞] with sup_{P ∈ 𝔓} E_P(E) ≤ 1, the first inequality in eq. (1).

Equations

• LogOptimal.IsEVariable 𝔓 t E = (Measurable E ∧ ∀ P ∈ 𝔓, ∫⁻ (x : ℕ → 𝒳), E x ∂P ≤ 1)

noncomputable def LogOptimal.valueAt {Ω : Type u_2} (E : ℕ → Ω → ENNReal) (τ : Ω → ℕ∞) (x : Ω) : ENNReal

The value E_τ of a process (E_t) at a time τ with values in {0, 1, …} ∪ {∞}, with E_∞ = limsup_{t → ∞} E_t (Section 1).

Equations

• LogOptimal.valueAt E τ x = if h : τ x = ⊤ then Filter.limsup (fun (t : ℕ) => E t x) Filter.atTop else E (WithTop.untop (τ x) h) x

def LogOptimal.IsEProcess {𝒳 : Type u_1} [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (E : ℕ → (ℕ → 𝒳) → ENNReal) : Prop

(E_t)_{t ≥ 0} is an e-process for the null 𝔓 (Section 1): a process adapted to (ℱ_t) with values in [0, ∞] such that sup_{P ∈ 𝔓} E_P(E_τ) ≤ 1 for every stopping time τ of (ℱ_t) with values in {0, 1, …} ∪ {∞}, the second inequality in eq. (1).

Equations

• One or more equations did not get rendered due to their size.

def LogOptimal.IsTestSupermartingale {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (𝔓 : Set (MeasureTheory.Measure Ω)) (ℱ : MeasureTheory.Filtration ℕ mΩ) (M : ℕ → Ω → ℝ) : Prop

A test supermartingale with respect to a filtration ℱ (Section 1): a nonnegative process adapted to ℱ with initial value one that is a supermartingale with respect to ℱ under every null distribution. The adaptedness is stated separately so that it holds also for an empty null.

Equations

• LogOptimal.IsTestSupermartingale 𝔓 ℱ M = (MeasureTheory.StronglyAdapted ℱ M ∧ (∀ (t : ℕ) (ω : Ω), 0 ≤ M t ω) ∧ (∀ (ω : Ω), M 0 ω = 1) ∧ ∀ P ∈ 𝔓, MeasureTheory.Supermartingale M ℱ P)

def LogOptimal.IsTestMartingale {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (𝔓 : Set (MeasureTheory.Measure Ω)) (ℱ : MeasureTheory.Filtration ℕ mΩ) (M : ℕ → Ω → ℝ) : Prop

A test martingale with respect to a filtration ℱ (Section 1): a nonnegative process adapted to ℱ with initial value one that is a martingale with respect to ℱ under every null distribution. The adaptedness is stated separately so that it holds also for an empty null.

Equations

• LogOptimal.IsTestMartingale 𝔓 ℱ M = (MeasureTheory.StronglyAdapted ℱ M ∧ (∀ (t : ℕ) (ω : Ω), 0 ≤ M t ω) ∧ (∀ (ω : Ω), M 0 ω = 1) ∧ ∀ P ∈ 𝔓, MeasureTheory.Martingale M ℱ P)

Expectations in [−∞, ∞], e-powers, and regrets

noncomputable def LogOptimal.eIntegral {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) (g : Ω → EReal) : EReal

The integral of a function g with values in [−∞, ∞]: the integral of its positive part minus the integral of its negative part, in EReal. It is the expectation of Section S1 whenever one of the two parts is integrable.

Equations

• LogOptimal.eIntegral μ g = ↑(∫⁻ (ω : Ω), (g ω).toENNReal ∂μ) - ↑(∫⁻ (ω : Ω), (-g ω).toENNReal ∂μ)

noncomputable def LogOptimal.ePower {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (Q : MeasureTheory.Measure Ω) (E : Ω → ENNReal) : EReal

The e-power E_Q(log E) of a random variable E with values in [0, ∞] (Section 1).

Equations

• LogOptimal.ePower Q E = LogOptimal.eIntegral Q fun (ω : Ω) => (E ω).log

noncomputable def LogOptimal.regret {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (Q : MeasureTheory.Measure Ω) (Es E : Ω → ENNReal) : EReal

The regret R_t(E) = E_Q{log(E*_t/E)} of eq. (3), where Es = E*_t is the numéraire at horizon t. The regret of an e-process (E_t) at t is R_t(E_t) = regret Q (Es t) (E t).

Equations

• LogOptimal.regret Q Es E = LogOptimal.eIntegral Q fun (ω : Ω) => (Es ω / E ω).log

noncomputable def LogOptimal.minimaxRegret {𝒳 : Type u_1} [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal) (T : ℕ) : EReal

The minimax regret Γ_T = inf_{(E_t)} max_{0 ≤ t ≤ T} R_t(E_t) of eq. (3), where the infimum runs over all e-processes (E_t) and Es t = E*_t are the numéraires.

Equations

• LogOptimal.minimaxRegret 𝔓 Q Es T = ⨅ (E : ℕ → (ℕ → 𝒳) → ENNReal), ⨅ (_ : LogOptimal.IsEProcess 𝔓 E), ⨆ (t : ℕ), ⨆ (_ : t ≤ T), LogOptimal.regret Q (Es t) (E t)

Numéraires

def LogOptimal.IsNumeraire {𝒳 : Type u_1} [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (t : ℕ) (Es : (ℕ → 𝒳) → ENNReal) : Prop

Es is a numéraire at horizon t (Larsson, Ramdas and Ruf, 2025, Definition 2.1): an e-variable Es = E*_t ∈ ℰ_t that satisfies the first of the properties in eq. (2), sup_{E ∈ ℰ_t} E_Q(E/E*_t) ≤ 1.

Equations

• LogOptimal.IsNumeraire 𝔓 Q t Es = (LogOptimal.IsEVariable 𝔓 t Es ∧ ∀ (E : (ℕ → 𝒳) → ENNReal), LogOptimal.IsEVariable 𝔓 t E → ∫⁻ (x : ℕ → 𝒳), E x / Es x ∂Q ≤ 1)

def LogOptimal.IsLogOptimal {𝒳 : Type u_1} [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (t : ℕ) (Es : (ℕ → 𝒳) → ENNReal) : Prop

The second property in eq. (2): E_Q(log E*_t) = sup_{E ∈ ℰ_t} E_Q(log E).

Equations

• LogOptimal.IsLogOptimal 𝔓 Q t Es = (LogOptimal.ePower Q Es = ⨆ (E : (ℕ → 𝒳) → ENNReal), ⨆ (_ : LogOptimal.IsEVariable 𝔓 t E), LogOptimal.ePower Q E)

def LogOptimal.IsNumeraireDensity {𝒳 : Type u_1} [MeasurableSpace 𝒳] (Q : MeasureTheory.Measure (ℕ → 𝒳)) (t : ℕ) (Es : (ℕ → 𝒳) → ENNReal) (Ps : MeasureTheory.Measure (Fin t → 𝒳)) : Prop

The third property in eq. (2): E*_t = dQ_t/dP*_t for a sub-probability measure P*_t on 𝒳^t. It is stated as Q_t = P*_t.withDensity e for a measurable e on 𝒳^t with E*_t = e(X^t) Q-almost surely.

Equations

• One or more equations did not get rendered due to their size.

def LogOptimal.FiniteOptimalEPower {𝒳 : Type u_1} [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) : Prop

The standing assumption of Section 2: sup_{E ∈ ℰ_t} E_Q(log E) < ∞ for every t ≥ 0.

Equations

• LogOptimal.FiniteOptimalEPower 𝔓 Q = ∀ (t : ℕ), ⨆ (E : (ℕ → 𝒳) → ENNReal), ⨆ (_ : LogOptimal.IsEVariable 𝔓 t E), LogOptimal.ePower Q E < ⊤

def LogOptimal.probVectors (T : ℕ) : Set (Fin (T + 1) → ℝ)

The set Δ_T of probability vectors (ξ₀, …, ξ_T) (Section 2).

Equations

• LogOptimal.probVectors T = {ξ : Fin (T + 1) → ℝ | (∀ (t : Fin (T + 1)), 0 ≤ ξ t) ∧ ∑ t : Fin (T + 1), ξ t = 1}

The supremum η_T and the Snell envelope

noncomputable def LogOptimal.truncTime {Ω : Type u_2} (τ : Ω → ℕ∞) (T : ℕ) (x : Ω) : ℕ

The time τ ∧ T = min(τ, T), a natural number.

Equations

• LogOptimal.truncTime τ T x = WithTop.untopD T (min (τ x) ↑T)

theorem LogOptimal.coe_truncTime {Ω : Type u_2} (τ : Ω → ℕ∞) (T : ℕ) (x : Ω) : ↑(truncTime τ T x) = min (τ x) ↑T

theorem LogOptimal.truncTime_le {Ω : Type u_2} (τ : Ω → ℕ∞) (T : ℕ) (x : Ω) : truncTime τ T x ≤ T

noncomputable def LogOptimal.eta {𝒳 : Type u_1} [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Es : ℕ → (ℕ → 𝒳) → ENNReal) (T : ℕ) : ENNReal

The supremum η_T = sup_{P ∈ 𝔓} sup_τ E_P(E*_{τ ∧ T}) of eq. (4), where τ ranges over the stopping times of (ℱ_t) and Es t = E*_t are the fixed versions of the numéraires.

Equations

• LogOptimal.eta 𝔓 Es T = ⨆ P ∈ 𝔓, ⨆ (τ : (ℕ → 𝒳) → ℕ∞), ⨆ (_ : MeasureTheory.IsStoppingTime (LogOptimal.dataFiltration 𝒳) τ), ∫⁻ (x : ℕ → 𝒳), Es (LogOptimal.truncTime τ T x) x ∂P

@[irreducible]

noncomputable def LogOptimal.snell {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (ℱ : MeasureTheory.Filtration ℕ mΩ) (G : ℕ → Ω → ℝ) (N : ℕ) : ℕ → Ω → ℝ

The Snell envelope of an adapted process (G_n)_{0 ≤ n ≤ N} under P with respect to a filtration ℱ, defined by backward induction: S_N = G_N and S_n = max{G_n, E_P(S_{n+1} ∣ ℱ_n)} for n < N (Peskir and Shiryaev, 2006, eqs. (1.1.6) and (1.1.7)). For n > N, the value is G_N.

Equations

• LogOptimal.snell P ℱ G N x✝ = if N ≤ x✝ then G N else fun (ω : Ω) => max (G x✝ ω) (P[LogOptimal.snell P ℱ G N (x✝ + 1) | ↑ℱ x✝] ω)

noncomputable def LogOptimal.snellEnvelope {𝒳 : Type u_1} [MeasurableSpace 𝒳] (P : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal) (T : ℕ) : ℕ → (ℕ → 𝒳) → ℝ

The Snell envelope (Λ^P_t)_{0 ≤ t ≤ T} of (E*_{t ∧ T})_{t ≥ 0} under P (Section 2), defined by Λ^P_T = E*_T and Λ^P_t = max{E*_t, E_P(Λ^P_{t+1} ∣ ℱ_t)} for t < T. It takes real values: since E_P(E*_t) ≤ 1, the numéraire E*_t is finite P-almost surely, and its real part (E*_t).toReal is used.

Equations

• LogOptimal.snellEnvelope P Es T = LogOptimal.snell P (LogOptimal.dataFiltration 𝒳) (fun (t : ℕ) (x : ℕ → 𝒳) => (Es t x).toReal) T