The numéraire and the regret

This file proves the facts on the numéraire of Section 2 of the paper and Lemma S1 (Integrability of the numéraire), with the basic properties of e-variables, e-processes, and the minimax regret on which the later files rely.

• dataFiltration_zero, eq_of_measurable_dataFiltration_zero: ℱ₀ is trivial, so that an ℱ₀-measurable function is constant;
• valueAt_of_eq_coe, valueAt_le_of_forall_le, valueAt_stopped: the value E_τ of a process at a time τ;
• IsEProcess.isEVariable: the value E_t of an e-process at t belongs to ℰ_t;
• FiniteOptimalEPower.nonempty: under the standing assumption, the null is not empty;
• IsNumeraire.ae_pos_lt_top, IsNumeraire.integrable_log, IsNumeraire.isLogOptimal: a numéraire is positive and finite Q-almost surely, with a Q-integrable logarithm, and it is log-optimal (Lemma S1);
• IsNumeraire.regret_eq_sub, IsNumeraire.regret_nonneg: R_t(E) = E_Q(log E*_t) − E_Q(log E) ≥ 0 for E ∈ ℰ_t (Lemma S1), with Jensen's inequality for the logarithm (eIntegral_log_le_log_lintegral);
• IsNumeraire.ae_eq: numéraires are unique up to Q-null sets (Larsson, Ramdas and Ruf, 2025, Section 2);
• Setting.numeraire_zero: E*_0 = 1, since ℱ₀ is trivial;
• lem_regret_proof (Lemma S1) and sec2_numeraire_proof (Section 2);
• minimaxRegret_le_of_isEProcess, minimaxRegret_mono, Setting.minimaxRegret_nonneg: basic bounds on the minimax regret Γ_T.

The data filtration

theorem LogOptimal.dataFiltration_apply {𝒳 : Type u_1} [MeasurableSpace 𝒳] (t : ℕ) : ↑(dataFiltration 𝒳) t = ⨆ (i : ℕ), ⨆ (_ : i < t), MeasurableSpace.comap (fun (x : ℕ → 𝒳) => x i) inst✝

theorem LogOptimal.dataFiltration_zero {𝒳 : Type u_1} [MeasurableSpace 𝒳] : ↑(dataFiltration 𝒳) 0 = ⊥

theorem LogOptimal.eq_of_measurable_dataFiltration_zero {𝒳 : Type u_1} [MeasurableSpace 𝒳] {β : Type u_2} [MeasurableSpace β] [MeasurableSingletonClass β] {f : (ℕ → 𝒳) → β} (hf : Measurable f) (x y : ℕ → 𝒳) : f x = f y

Since ℱ₀ is trivial, an ℱ₀-measurable function is constant.

Values at stopping times

theorem LogOptimal.valueAt_of_eq_coe {Ω : Type u_1} {E : ℕ → Ω → ENNReal} {τ : Ω → ℕ∞} {x : Ω} {n : ℕ} (h : τ x = ↑n) : valueAt E τ x = E n x

theorem LogOptimal.valueAt_of_eq_top {Ω : Type u_1} {E : ℕ → Ω → ENNReal} {τ : Ω → ℕ∞} {x : Ω} (h : τ x = ⊤) : valueAt E τ x = Filter.limsup (fun (t : ℕ) => E t x) Filter.atTop

theorem LogOptimal.valueAt_const {Ω : Type u_1} (E : ℕ → Ω → ENNReal) (t : ℕ) : (valueAt E fun (x : Ω) => ↑t) = E t

theorem LogOptimal.valueAt_le_of_forall_le {Ω : Type u_1} {E : ℕ → Ω → ENNReal} {τ : Ω → ℕ∞} {x : Ω} {c : ENNReal} (h : ∀ (t : ℕ), E t x ≤ c) : valueAt E τ x ≤ c

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

The value at τ of the process (E_{t ∧ T})_{t ≥ 0} stopped at T is E_{τ ∧ T}, also on the event {τ = ∞}.

E-variables and e-processes

theorem LogOptimal.IsEVariable.measurable' {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {t : ℕ} {E : (ℕ → 𝒳) → ENNReal} (hE : IsEVariable 𝔓 t E) : Measurable E

theorem LogOptimal.isEVariable_one {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (t : ℕ) : IsEVariable 𝔓 t fun (x : ℕ → 𝒳) => 1

theorem LogOptimal.IsEProcess.isEVariable {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) (t : ℕ) : IsEVariable 𝔓 t (E t)

Lemma S1 for a numéraire at one horizon

theorem LogOptimal.FiniteOptimalEPower.nonempty {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} [MeasureTheory.IsProbabilityMeasure Q] (h : FiniteOptimalEPower 𝔓 Q) : 𝔓.Nonempty

Under the standing assumption, the null is not empty: otherwise the constant ∞ would be an e-variable with infinite e-power.

theorem LogOptimal.IsNumeraire.lintegral_inv_le_one {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hEs : IsNumeraire 𝔓 Q t Es) : ∫⁻ (x : ℕ → 𝒳), (Es x)⁻¹ ∂Q ≤ 1

Taking E ≡ 1 in the first property in eq. (2) gives E_Q(1/E*_t) ≤ 1.

theorem LogOptimal.IsNumeraire.ae_pos {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hEs : IsNumeraire 𝔓 Q t Es) : ∀ᵐ (x : ℕ → 𝒳) ∂Q, 0 < Es x

theorem LogOptimal.IsNumeraire.lintegral_neg_log_le_one {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hEs : IsNumeraire 𝔓 Q t Es) : ∫⁻ (x : ℕ → 𝒳), (-(Es x).log).toENNReal ∂Q ≤ 1

Since log⁻ x ≤ 1/x, the negative part of log E*_t has Q-expectation at most one.

theorem LogOptimal.IsNumeraire.ePower_lt_top {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} (hfin : FiniteOptimalEPower 𝔓 Q) (hEs : IsNumeraire 𝔓 Q t Es) : ePower Q Es < ⊤

theorem LogOptimal.IsNumeraire.lintegral_log_ne_top {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hfin : FiniteOptimalEPower 𝔓 Q) (hEs : IsNumeraire 𝔓 Q t Es) : ∫⁻ (x : ℕ → 𝒳), (Es x).log.toENNReal ∂Q ≠ ⊤

Since E_Q(log E*_t) is at most the finite supremum of the standing assumption, the positive part of log E*_t is Q-integrable.

theorem LogOptimal.IsNumeraire.integrable_log {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hfin : FiniteOptimalEPower 𝔓 Q) (hEs : IsNumeraire 𝔓 Q t Es) : MeasureTheory.Integrable (fun (x : ℕ → 𝒳) => (Es x).log.toReal) Q

theorem LogOptimal.IsNumeraire.ePower_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hfin : FiniteOptimalEPower 𝔓 Q) (hEs : IsNumeraire 𝔓 Q t Es) : ePower Q Es = ↑(∫ (x : ℕ → 𝒳), (Es x).log.toReal ∂Q)

theorem LogOptimal.IsNumeraire.ae_pos_lt_top {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hfin : FiniteOptimalEPower 𝔓 Q) (hEs : IsNumeraire 𝔓 Q t Es) : ∀ᵐ (x : ℕ → 𝒳) ∂Q, 0 < Es x ∧ Es x < ⊤

theorem LogOptimal.IsNumeraire.eIntegral_log_div_nonpos {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} [MeasureTheory.IsProbabilityMeasure Q] (hEs : IsNumeraire 𝔓 Q t Es) {E : (ℕ → 𝒳) → ENNReal} (hE : IsEVariable 𝔓 t E) : ∫⁻ (x : ℕ → 𝒳), (E x / Es x).log.toENNReal ∂Q ≤ 1 ∧ (eIntegral Q fun (x : ℕ → 𝒳) => (E x / Es x).log) ≤ 0

For E ∈ ℰ_t, the expectation E_Q{log(E/E*_t)} is well defined, since log⁺(E/E*_t) ≤ E/E*_t, and Jensen's inequality gives E_Q{log(E/E*_t)} ≤ log E_Q(E/E*_t) ≤ 0.

theorem LogOptimal.IsNumeraire.regret_eq_neg {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} [MeasureTheory.IsProbabilityMeasure Q] (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hfin : FiniteOptimalEPower 𝔓 Q) (hEs : IsNumeraire 𝔓 Q t Es) {E : (ℕ → 𝒳) → ENNReal} (hE : IsEVariable 𝔓 t E) : (regret Q Es E = -eIntegral Q fun (x : ℕ → 𝒳) => (E x / Es x).log) ∧ ∫⁻ (x : ℕ → 𝒳), (-(Es x / E x).log).toENNReal ∂Q < ⊤

theorem LogOptimal.IsNumeraire.regret_nonneg {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} [MeasureTheory.IsProbabilityMeasure Q] (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hfin : FiniteOptimalEPower 𝔓 Q) (hEs : IsNumeraire 𝔓 Q t Es) {E : (ℕ → 𝒳) → ENNReal} (hE : IsEVariable 𝔓 t E) : 0 ≤ regret Q Es E

The regret of an e-variable is nonnegative, by Jensen's inequality and the numéraire property (Lemma S1).

theorem LogOptimal.IsNumeraire.regret_eq_sub {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} [MeasureTheory.IsProbabilityMeasure Q] (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hfin : FiniteOptimalEPower 𝔓 Q) (hEs : IsNumeraire 𝔓 Q t Es) {E : (ℕ → 𝒳) → ENNReal} (hE : IsEVariable 𝔓 t E) : regret Q Es E = ePower Q Es - ePower Q E

The regret is the loss of e-power relative to the numéraire (Lemma S1): R_t(E) = E_Q(log E*_t) − E_Q(log E), since log E = log E*_t + log(E/E*_t) Q-almost surely with an integrable first term.

theorem LogOptimal.IsNumeraire.isLogOptimal {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} [MeasureTheory.IsProbabilityMeasure Q] (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hfin : FiniteOptimalEPower 𝔓 Q) (hEs : IsNumeraire 𝔓 Q t Es) : IsLogOptimal 𝔓 Q t Es

The second property in eq. (2): the numéraire is log-optimal (Lemma S1).

Uniqueness of the numéraire

theorem LogOptimal.two_le_add_inv (u : ENNReal) : 2 ≤ u + u⁻¹

theorem LogOptimal.eq_one_of_add_inv_eq_two {u : ENNReal} (h : u + u⁻¹ = 2) : u = 1

theorem LogOptimal.IsNumeraire.ae_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} [MeasureTheory.IsProbabilityMeasure Q] {t : ℕ} {Es : (ℕ → 𝒳) → ENNReal} (hEs : IsNumeraire 𝔓 Q t Es) (hfinite : ∀ᵐ (x : ℕ → 𝒳) ∂Q, 0 < Es x ∧ Es x < ⊤) {E : (ℕ → 𝒳) → ENNReal} (hE : IsNumeraire 𝔓 Q t E) : E =ᵐ[Q] Es

Uniqueness of the numéraire (Larsson, Ramdas and Ruf, 2025, Section 2, after Definition 2.1; the uniqueness of the log-optimal e-variable in their Proposition 2.4 follows from it): two numéraires at horizon t are equal Q-almost surely. For U = E/E*_t, the numéraire properties give E_Q(U) ≤ 1 and E_Q(1/U) ≤ 1. Larsson et al. conclude by the equality case of Jensen's inequality; here U + 1/U ≥ 2, with equality only if U = 1, gives U = 1 Q-almost surely.

The setting of Sections 1 and 2

theorem LogOptimal.Setting.nonempty {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) : 𝔓.Nonempty

theorem LogOptimal.Setting.ae_pos_lt_top {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) (t : ℕ) : ∀ᵐ (x : ℕ → 𝒳) ∂Q, 0 < Es t x ∧ Es t x < ⊤

theorem LogOptimal.Setting.regret_nonneg {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) {t : ℕ} {E : (ℕ → 𝒳) → ENNReal} (hE : IsEVariable 𝔓 t E) : 0 ≤ regret Q (Es t) E

theorem LogOptimal.Setting.regret_eq_sub {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) {t : ℕ} {E : (ℕ → 𝒳) → ENNReal} (hE : IsEVariable 𝔓 t E) : regret Q (Es t) E = ePower Q (Es t) - ePower Q E

theorem LogOptimal.Setting.ePower_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) (t : ℕ) : ePower Q (Es t) = ↑(∫ (x : ℕ → 𝒳), (Es t x).log.toReal ∂Q)

theorem LogOptimal.Setting.numeraire_zero {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) (x : ℕ → 𝒳) : Es 0 x = 1

The numéraire E*_0 equals one, since ℱ₀ is trivial (Section 2): a constant c with c ≤ 1 (an e-variable) and 1/c ≤ 1 (the first property in eq. (2) with E ≡ 1).

theorem LogOptimal.Setting.regret_self {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) (t : ℕ) : regret Q (Es t) (Es t) = 0

The regret of E*_t itself is zero.

theorem LogOptimal.Setting.regret_of_ae_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) {t : ℕ} {E : (ℕ → 𝒳) → ENNReal} (hE : E =ᵐ[Q] Es t) : regret Q (Es t) E = 0

An e-variable equal to E*_t Q-almost surely has regret zero.

The minimax regret

theorem LogOptimal.minimaxRegret_le_of_isEProcess {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) {T : ℕ} {c : EReal} (h : ∀ t ≤ T, regret Q (Es t) (E t) ≤ c) : minimaxRegret 𝔓 Q Es T ≤ c

theorem LogOptimal.minimaxRegret_mono {𝒳 : Type u_1} [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal) (T : ℕ) : minimaxRegret 𝔓 Q Es T ≤ minimaxRegret 𝔓 Q Es (T + 1)

Γ_T ≤ Γ_{T+1}, since the maximum in eq. (3) is taken over more horizons for T + 1.

theorem LogOptimal.Setting.minimaxRegret_nonneg {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) (T : ℕ) : 0 ≤ minimaxRegret 𝔓 Q Es T

Γ_T ≥ 0, since every e-process has a nonnegative regret at t = 0 by Lemma S1.

Lemma S1 and the facts on the numéraire of Section 2

theorem LogOptimal.lem_regret_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal) : Setting 𝔓 Q Es → ∀ (t : ℕ), (∀ᵐ (x : ℕ → 𝒳) ∂Q, 0 < Es t x ∧ Es t x < ⊤) ∧ MeasureTheory.Integrable (fun (x : ℕ → 𝒳) => (Es t x).log.toReal) Q ∧ ePower Q (Es t) = ↑(∫ (x : ℕ → 𝒳), (Es t x).log.toReal ∂Q) ∧ IsLogOptimal 𝔓 Q t (Es t) ∧ ∀ (E : (ℕ → 𝒳) → ENNReal), IsEVariable 𝔓 t E → ∫⁻ (x : ℕ → 𝒳), (-(Es t x / E x).log).toENNReal ∂Q < ⊤ ∧ regret Q (Es t) E = ePower Q (Es t) - ePower Q E ∧ 0 ≤ regret Q (Es t) E

theorem LogOptimal.sec2_numeraire_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal) : Setting 𝔓 Q Es → (∀ (t : ℕ), ∀ᵐ (x : ℕ → 𝒳) ∂Q, 0 < Es t x) ∧ (∀ (t : ℕ) (E : (ℕ → 𝒳) → ENNReal), IsNumeraire 𝔓 Q t E → E =ᵐ[Q] Es t) ∧ ∀ (x : ℕ → 𝒳), Es 0 x = 1