Densities against mixtures of null distributions, and bounds on e-powers

This file proves the general facts on numéraires and e-powers that the Gaussian results of the paper use.

• marginal_bind: the distribution of X^t under a mixture ∫ P_λ π(dλ) is the mixture of the distributions P_{λ,t};
• lintegral_eq_lintegral_mul_of_marginal_eq: if Q_t has density e with respect to P_t, then E_Q(H) = E_P{e(X^t) H} for every ℱ_t-measurable H ≥ 0;
• isNumeraire_of_marginal_eq_withDensity and sec_methods_mixture_proof: an e-variable E = dQ_t/dP*_t, with P*_t a mixture of null distributions of X^t, is the numéraire, and P*_t is the measure in eq. (2) (Section S4; the proof of Proposition 2 uses the same argument): for every E' ∈ ℰ_t, Fubini's theorem gives E_Q(E'/E) ≤ E_{P*_t}(E') ≤ 1;
• isNumeraire_zero_one: at t = 0, the constant 1 is the numéraire, since ℱ₀ is trivial;
• lintegral_toENNReal_log_le_of_lintegral_div_le_one and ePower_le_of_lintegral_div_le_one: if E_Q(E/F) ≤ 1 for a positive and finite F with an integrable logarithm, then the positive part of log E is Q-integrable and E_Q(log E) ≤ E_Q(log F), by Jensen's inequality, as in the proof of Lemma S1;
• regret_eq_integral_sub_ePower: E_Q{log(E*/E)} = E_Q(log E*) − E_Q(log E) for a positive and finite E* with an integrable logarithm, without the numéraire property;
• eIntegral_bind_le and le_eIntegral_bind: bounds on an expectation under a mixture ∫ Q_a ν(da) from bounds under each Q_a, applied to the positive and negative parts separately.

Mixtures of null distributions

theorem LogOptimal.marginal_bind {𝒳 : Type u_1} [MeasurableSpace 𝒳] {Λ : Type u_2} [MeasurableSpace Λ] (π : MeasureTheory.Measure Λ) {κ : Λ → MeasureTheory.Measure (ℕ → 𝒳)} (hκ : Measurable κ) (t : ℕ) : marginal (π.bind κ) t = π.bind fun (a : Λ) => marginal (κ a) t

The distribution of X^t under a mixture ∫ P_λ π(dλ) is the mixture of the distributions P_{λ,t}.

theorem LogOptimal.lintegral_eq_lintegral_mul_of_marginal_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] {Q P : MeasureTheory.Measure (ℕ → 𝒳)} {t : ℕ} {e : (Fin t → 𝒳) → ENNReal} (he : Measurable e) (hQ : marginal Q t = (marginal P t).withDensity e) {H : (ℕ → 𝒳) → ENNReal} (hH : Measurable H) : ∫⁻ (x : ℕ → 𝒳), H x ∂Q = ∫⁻ (x : ℕ → 𝒳), (e fun (i : Fin t) => x ↑i) * H x ∂P

The change of measure on ℱ_t: if Q_t has density e with respect to P_t, then E_Q(H) = E_P{e(X^t) H} for every ℱ_t-measurable H ≥ 0.

theorem LogOptimal.isNumeraire_of_marginal_eq_withDensity {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Λ : Type u_2} [MeasurableSpace Λ] (π : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure π] {κ : Λ → MeasureTheory.Measure (ℕ → 𝒳)} (hκm : Measurable κ) [∀ (a : Λ), MeasureTheory.IsProbabilityMeasure (κ a)] (hκ : ∀ (a : Λ), κ a ∈ 𝔓) {t : ℕ} {E : (ℕ → 𝒳) → ENNReal} {e : (Fin t → 𝒳) → ENNReal} (hE : IsEVariable 𝔓 t E) (he : Measurable e) (hEe : E =ᵐ[Q] fun (x : ℕ → 𝒳) => e fun (i : Fin t) => x ↑i) (hQ : marginal Q t = (π.bind fun (a : Λ) => marginal (κ a) t).withDensity e) : IsNumeraire 𝔓 Q t E ∧ IsNumeraireDensity Q t E (π.bind fun (a : Λ) => marginal (κ a) t)

A density against a mixture of null distributions (Section S4, and the proof of Proposition 2): an e-variable E with E = e(X^t) Q-almost surely, where e = dQ_t/dP*_t and P*_t = ∫ P_{λ,t} π(dλ) is a mixture of null distributions of X^t, is the numéraire, and P*_t is the measure in eq. (2). For every E' ∈ ℰ_t, the change of measure on ℱ_t and Fubini's theorem give E_Q(E'/E) ≤ ∫ E_{P_λ}(E') π(dλ) ≤ 1.

theorem LogOptimal.isNumeraire_zero_one {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} [MeasureTheory.IsProbabilityMeasure Q] (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hne : 𝔓.Nonempty) : IsNumeraire 𝔓 Q 0 fun (x : ℕ → 𝒳) => 1

At t = 0, the constant 1 is the numéraire, since ℱ₀ is trivial: every E' ∈ ℰ₀ is a constant c, and c = E_P(E') ≤ 1 for a null distribution P.

theorem LogOptimal.sec_methods_mixture_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Λ : Type u) [MeasurableSpace Λ] (π : MeasureTheory.Measure Λ) (κ : ProbabilityTheory.Kernel Λ (ℕ → 𝒳)) : MeasureTheory.IsProbabilityMeasure π → ProbabilityTheory.IsMarkovKernel κ → (∀ (a : Λ), κ a ∈ 𝔓) → ∀ (t : ℕ) (E : (ℕ → 𝒳) → ENNReal) (e : (Fin t → 𝒳) → ENNReal), IsEVariable 𝔓 t E → Measurable e → (E =ᵐ[Q] fun (x : ℕ → 𝒳) => e fun (i : Fin t) => x ↑i) → marginal Q t = (π.bind fun (a : Λ) => marginal (κ a) t).withDensity e → IsNumeraire 𝔓 Q t E ∧ IsNumeraireDensity Q t E (π.bind fun (a : Λ) => marginal (κ a) t)

Section S4, a density against a mixture of null distributions: the general statement sec_methods_mixture.

Bounds on e-powers

theorem LogOptimal.lintegral_toENNReal_log_le_of_lintegral_div_le_one {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Q : MeasureTheory.Measure Ω} {E F : Ω → ENNReal} (hFm : AEMeasurable F Q) (hF : ∀ᵐ (x : Ω) ∂Q, 0 < F x ∧ F x < ⊤) (hdiv : ∫⁻ (x : Ω), E x / F x ∂Q ≤ 1) : ∫⁻ (x : Ω), (E x).log.toENNReal ∂Q ≤ ∫⁻ (x : Ω), (F x).log.toENNReal ∂Q + 1

If E_Q(E/F) ≤ 1 for a positive and finite F, then E_Q{(log E)⁺} ≤ E_Q{(log F)⁺} + 1, since (log E)⁺ ≤ (log F)⁺ + (log(E/F))⁺ and (log(E/F))⁺ ≤ E/F.

theorem LogOptimal.regret_eq_integral_sub_ePower {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Q : MeasureTheory.Measure Ω} {Es E : Ω → ENNReal} (hEs : ∀ᵐ (x : Ω) ∂Q, 0 < Es x ∧ Es x < ⊤) (hlog : MeasureTheory.Integrable (fun (x : Ω) => (Es x).log.toReal) Q) (hE : AEMeasurable E Q) (hpos : ∫⁻ (x : Ω), (E x).log.toENNReal ∂Q ≠ ⊤) : regret Q Es E = ↑(∫ (x : Ω), (Es x).log.toReal ∂Q) - ePower Q E

The regret E_Q{log(E*/E)} = E_Q(log E*) − E_Q(log E) for a positive and finite E* with an integrable logarithm and an E with a Q-integrable positive part of log E, without the numéraire property.

theorem LogOptimal.ePower_le_of_lintegral_div_le_one {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Q : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Q] {E F : Ω → ENNReal} (hE : AEMeasurable E Q) (hFm : AEMeasurable F Q) (hF : ∀ᵐ (x : Ω) ∂Q, 0 < F x ∧ F x < ⊤) (hlog : MeasureTheory.Integrable (fun (x : Ω) => (F x).log.toReal) Q) (hdiv : ∫⁻ (x : Ω), E x / F x ∂Q ≤ 1) : ePower Q E ≤ ↑(∫ (x : Ω), (F x).log.toReal ∂Q)

If E_Q(E/F) ≤ 1 for a positive and finite F with an integrable logarithm, then E_Q(log E) ≤ E_Q(log F): since log E = log F + log(E/F), Jensen's inequality gives E_Q(log E) ≤ E_Q(log F) + log E_Q(E/F) ≤ E_Q(log F).

Expectations under a mixture of alternatives

theorem LogOptimal.eIntegral_bind_le {α : Type u_1} {Ω : Type u_2} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure ν] {κ : α → MeasureTheory.Measure Ω} (hκ : Measurable κ) {f : Ω → EReal} (hf : Measurable f) {A : ENNReal} (hA : A ≠ ⊤) (hpos : ∀ (a : α), ∫⁻ (x : Ω), (f x).toENNReal ∂κ a ≤ A) {c : ℝ} (hc : ∀ (a : α), eIntegral (κ a) f ≤ ↑c) : eIntegral (ν.bind κ) f ≤ ↑c

The expectation under a mixture ∫ Q_a ν(da) of a function f with values in [−∞, ∞] is at most c when it is at most c under each Q_a and the positive parts of f have uniformly bounded expectations.

theorem LogOptimal.le_eIntegral_bind {α : Type u_1} {Ω : Type u_2} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure ν] {κ : α → MeasureTheory.Measure Ω} (hκ : Measurable κ) {f : Ω → EReal} (hf : Measurable f) (hpos : ∫⁻ (x : Ω), (f x).toENNReal ∂ν.bind κ ≠ ⊤) {c : ℝ} (hc : ∀ (a : α), ↑c ≤ eIntegral (κ a) f) : ↑c ≤ eIntegral (ν.bind κ) f

The expectation under a mixture ∫ Q_a ν(da) of a function f with values in [−∞, ∞] is at least c when it is at least c under each Q_a and the positive part of f has a finite expectation under the mixture.