Proposition 2: the numéraires of the Gaussian location model

This file proves Proposition 2 of the paper, following its proof in Section S1.4, and the standing assumption of Section 2 for the alternatives Q_μ and for every mixture Q.

• ePower_ofReal_prod_lik: if g_i ∼ N(0, s²) under Q for i ∈ S, then E_Q{log ∏_{i∈S} ℓ(g_i)} = |S|κ, since E{log ℓ(Z)} = −log s − (s^{−2} − 1)s²/2 = κ for Z ∼ N(0, s²);
• ePower_gaussNumeraire_mixAlt, ePower_gaussNumeraire_altDist: E_Q(log E*_t) = (t − 1)κ under Q and under every Q_μ, since Y_i ∼ N(0, s²) there (Lemma S2(iii));
• ePower_likProcess_altDist: E_{Q_μ}{log ∏_{i=1}^t ℓ(X_i − μ)} = tκ;
• ePower_altDist_le_of_isEVariable: the Gibbs inequality E_{Q_μ}(log E) ≤ tκ = KL(Q_{μ,t} ‖ P_{μ,t}) for every E ∈ ℰ_t, with the integrability of (log E)⁺;
• ePower_mixAlt_le_of_isEVariable and finiteOptimalEPower_mixAlt: for every mixture Q with s > 0 and any ρ, sup_{E ∈ ℰ_t} E_Q(log E) ≤ tκ < ∞, by averaging the previous bound over μ ∼ N(0, ρ²), separately for the positive and negative parts of log E;
• isEVariable_gaussNumeraire_null: E*_t ∈ ℰ_t, since E_θ(E*_t) = 1 for every θ;
• isNumeraire_gaussNumeraire_mixAlt: for ρ² ≥ 1 − s², E*_t = ∏_{i=2}^t ℓ(Y_i) is the numéraire at every horizon t ≥ 0;
• setting_mixAlt_of_isNumeraire and setting_gaussNumeraire_mixAlt: the setting of Sections 1 and 2 for the mixture Q, with any numéraires and with the numéraires of Proposition 2;
• prop_numeraire_proof: Proposition 2.

Expectations of log ℓ

theorem LogOptimal.neg_log_sub_mul_sq_eq_kappa {s : ℝ} (hs : 0 < s) : -Real.log s - (s⁻¹ ^ 2 - 1) * 1 ^ 2 * s ^ 2 / 2 = kappa s

theorem LogOptimal.integral_log_lik_mul_gaussianReal {s : ℝ} (hs : 0 < s) (c : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => Real.log (lik s (c * y))) (ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal) ∧ ∫ (y : ℝ), Real.log (lik s (c * y)) ∂ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal = -Real.log s - (s⁻¹ ^ 2 - 1) * c ^ 2 * s ^ 2 / 2

For Z ∼ N(0, s²) and c ∈ ℝ, log ℓ(cZ) is integrable and E{log ℓ(cZ)} = −log s − (s^{−2} − 1)c²s²/2, from log ℓ(y) = −log s − (s^{−2} − 1)y²/2.

theorem LogOptimal.log_ofReal_prod_lik {s : ℝ} (hs : 0 < s) (S : Finset ℕ) (f : ℕ → ℝ) : (ENNReal.ofReal (∏ i ∈ S, lik s (f i))).log = ↑(∑ i ∈ S, Real.log (lik s (f i)))

log ∏_{i∈S} ℓ(f_i) = ∑_{i∈S} log ℓ(f_i), a real number, since ℓ > 0.

theorem LogOptimal.ePower_ofReal_prod_lik {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Q : MeasureTheory.Measure Ω} {s : ℝ} (hs : 0 < s) (S : Finset ℕ) {g : ℕ → Ω → ℝ} (hg : ∀ i ∈ S, Measurable (g i)) (hlaw : ∀ i ∈ S, MeasureTheory.Measure.map (g i) Q = ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal) : MeasureTheory.Integrable (fun (x : Ω) => (ENNReal.ofReal (∏ i ∈ S, lik s (g i x))).log.toReal) Q ∧ ∫ (x : Ω), (ENNReal.ofReal (∏ i ∈ S, lik s (g i x))).log.toReal ∂Q = ↑S.card * kappa s ∧ (ePower Q fun (x : Ω) => ENNReal.ofReal (∏ i ∈ S, lik s (g i x))) = ↑(↑S.card * kappa s)

E-power of a product of likelihood ratios: if g_i ∼ N(0, s²) under Q for every i ∈ S, then log ∏_{i∈S} ℓ(g_i) is Q-integrable with expectation |S|κ.

E-powers of the products of likelihood ratios

theorem LogOptimal.ePower_gaussNumeraire_mixAlt {s : ℝ} (hs : 0 < s) (ρ : ℝ) (t : ℕ) : MeasureTheory.Integrable (fun (x : ℕ → ℝ) => (gaussNumeraire s t x).log.toReal) (mixAlt s ρ) ∧ ∫ (x : ℕ → ℝ), (gaussNumeraire s t x).log.toReal ∂mixAlt s ρ = ↑(t - 1) * kappa s ∧ ePower (mixAlt s ρ) (gaussNumeraire s t) = ↑(↑(t - 1) * kappa s)

E_Q(log E*_t) = (t − 1)κ under the mixture Q (Proposition 2), since the Y_i are N(0, s²) variables under Q.

theorem LogOptimal.ePower_gaussNumeraire_altDist {s : ℝ} (hs : 0 < s) (μ : ℝ) (t : ℕ) : MeasureTheory.Integrable (fun (x : ℕ → ℝ) => (gaussNumeraire s t x).log.toReal) (altDist s μ) ∧ ∫ (x : ℕ → ℝ), (gaussNumeraire s t x).log.toReal ∂altDist s μ = ↑(t - 1) * kappa s ∧ ePower (altDist s μ) (gaussNumeraire s t) = ↑(↑(t - 1) * kappa s)

E_{Q_μ}(log E*_t) = (t − 1)κ under every Q_μ, since the Y_i are N(0, s²) variables under Q_μ.

theorem LogOptimal.altDist_map_coord_sub (s μ : ℝ) (i : ℕ) : MeasureTheory.Measure.map (fun (x : ℕ → ℝ) => x i - μ) (altDist s μ) = ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal

Under Q_μ, X_i − μ ∼ N(0, s²).

theorem LogOptimal.ePower_likProcess_altDist {s : ℝ} (hs : 0 < s) (μ : ℝ) (t : ℕ) : MeasureTheory.Integrable (fun (x : ℕ → ℝ) => (ENNReal.ofReal (likProcess s μ t x)).log.toReal) (altDist s μ) ∧ ∫ (x : ℕ → ℝ), (ENNReal.ofReal (likProcess s μ t x)).log.toReal ∂altDist s μ = ↑t * kappa s ∧ (ePower (altDist s μ) fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)) = ↑(↑t * kappa s)

E_{Q_μ}{log ∏_{i=1}^t ℓ(X_i − μ)} = tκ (Proposition S4(i)), since the X_i − μ are N(0, s²) variables under Q_μ.

The Gibbs inequality and the standing assumption

theorem LogOptimal.likProcess_pos {s : ℝ} (hs : 0 < s) (μ : ℝ) (t : ℕ) (x : ℕ → ℝ) : 0 < likProcess s μ t x

theorem LogOptimal.lintegral_toENNReal_log_ne_top_of_integrable {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Q : MeasureTheory.Measure Ω} {F : Ω → ENNReal} (hF : ∀ᵐ (x : Ω) ∂Q, 0 < F x ∧ F x < ⊤) (hlog : MeasureTheory.Integrable (fun (x : Ω) => (F x).log.toReal) Q) : ∫⁻ (x : Ω), (F x).log.toENNReal ∂Q ≠ ⊤

If 0 < F < ∞ and log F is integrable, then the positive part of log F has a finite integral.

theorem LogOptimal.ePower_altDist_le_of_isEVariable {s : ℝ} (hs : 0 < s) (μ : ℝ) {t : ℕ} {E : (ℕ → ℝ) → ENNReal} (hE : IsEVariable gaussNull t E) : ∫⁻ (x : ℕ → ℝ), (E x).log.toENNReal ∂altDist s μ ≤ ∫⁻ (x : ℕ → ℝ), (ENNReal.ofReal (likProcess s μ t x)).log.toENNReal ∂altDist s μ + 1 ∧ ePower (altDist s μ) E ≤ ↑(↑t * kappa s)

The Gibbs inequality for Q_μ: for every E ∈ ℰ_t, E_{Q_μ}(log E) ≤ tκ, the divergence KL(Q_{μ,t} ‖ P_{μ,t}), since E_{Q_μ}(E/L^μ_t) = E_μ(E) ≤ 1; moreover, E_{Q_μ}{(log E)⁺} ≤ E_{Q_μ}{(log L^μ_t)⁺} + 1.

theorem LogOptimal.lintegral_log_likProcess_altDist (s μ : ℝ) (t : ℕ) : ∫⁻ (x : ℕ → ℝ), (ENNReal.ofReal (likProcess s μ t x)).log.toENNReal ∂altDist s μ = ∫⁻ (x : ℕ → ℝ), (ENNReal.ofReal (likProcess s 0 t x)).log.toENNReal ∂altDist s 0

The positive parts of the logarithms of the likelihood ratios L^μ_t have the same expectation under every Q_μ, by the translation x ↦ x + μ.

noncomputable def LogOptimal.posLogBound (s : ℝ) (t : ℕ) : ENNReal

The uniform bound E_{Q_0}{(log L^0_t)⁺} + 1 on E_{Q_μ}{(log E)⁺} for E ∈ ℰ_t.

Equations

• LogOptimal.posLogBound s t = ∫⁻ (x : ℕ → ℝ), (ENNReal.ofReal (LogOptimal.likProcess s 0 t x)).log.toENNReal ∂LogOptimal.altDist s 0 + 1

theorem LogOptimal.posLogBound_ne_top {s : ℝ} (hs : 0 < s) (t : ℕ) : posLogBound s t ≠ ⊤

theorem LogOptimal.lintegral_pos_log_altDist_le {s : ℝ} (hs : 0 < s) (μ : ℝ) {t : ℕ} {E : (ℕ → ℝ) → ENNReal} (hE : IsEVariable gaussNull t E) : ∫⁻ (x : ℕ → ℝ), (E x).log.toENNReal ∂altDist s μ ≤ posLogBound s t

theorem LogOptimal.lintegral_pos_log_mixAlt_le {s : ℝ} (hs : 0 < s) (ρ : ℝ) {t : ℕ} {E : (ℕ → ℝ) → ENNReal} (hE : IsEVariable gaussNull t E) : ∫⁻ (x : ℕ → ℝ), (E x).log.toENNReal ∂mixAlt s ρ ≤ posLogBound s t

Under the mixture Q, the positive part of log E has expectation at most posLogBound s t for every E ∈ ℰ_t.

theorem LogOptimal.ePower_mixAlt_le_of_isEVariable {s : ℝ} (hs : 0 < s) (ρ : ℝ) {t : ℕ} {E : (ℕ → ℝ) → ENNReal} (hE : IsEVariable gaussNull t E) : ePower (mixAlt s ρ) E ≤ ↑(↑t * kappa s)

The standing assumption for the mixture: for every s > 0, every ρ, and every E ∈ ℰ_t, E_Q(log E) ≤ tκ. The bound E_{Q_μ}(log E) ≤ tκ of the Gibbs inequality holds under every Q_μ, and it is averaged over μ ∼ N(0, ρ²) separately for the positive and negative parts of log E.

theorem LogOptimal.finiteOptimalEPower_altDist {s : ℝ} (hs : 0 < s) (μ : ℝ) : FiniteOptimalEPower gaussNull (altDist s μ)

theorem LogOptimal.finiteOptimalEPower_mixAlt {s : ℝ} (hs : 0 < s) (ρ : ℝ) : FiniteOptimalEPower gaussNull (mixAlt s ρ)

theorem LogOptimal.isProbabilityMeasure_of_mem_gaussNull (P : MeasureTheory.Measure (ℕ → ℝ)) : P ∈ gaussNull → MeasureTheory.IsProbabilityMeasure P

theorem LogOptimal.gaussNull_nonempty : gaussNull.Nonempty

The numéraire of Proposition 2

theorem LogOptimal.gaussNumeraire_eq_helmertVec (s : ℝ) (t : ℕ) (x : ℕ → ℝ) : gaussNumeraire s t x = ENNReal.ofReal (∏ j : Fin (t - 1), lik s (helmertVec t x j))

E*_t is a function of Y^t: E*_t = G(Y^t) with G(u) = ∏_j ℓ(u_j).

theorem LogOptimal.gaussNumeraire_zero (s : ℝ) : gaussNumeraire s 0 = fun (x : ℕ → ℝ) => 1

theorem LogOptimal.measurable_gaussNumeraire_dataFiltration_le (s : ℝ) (t : ℕ) : Measurable (gaussNumeraire s t)

theorem LogOptimal.lintegral_gaussNumeraire_nullDist {s : ℝ} (hs : 0 < s) (θ : ℝ) (t : ℕ) : ∫⁻ (x : ℕ → ℝ), gaussNumeraire s t x ∂nullDist θ = 1

E_θ(E*_t) = 1 for every θ, since Y^t ∼ N(0, 1)^{⊗(t−1)} under P_θ and ∏_j ℓ(u_j) is the density of N(0, s²)^{⊗(t−1)} with respect to N(0, 1)^{⊗(t−1)}.

theorem LogOptimal.isEVariable_gaussNumeraire_null {s : ℝ} (hs : 0 < s) (t : ℕ) : IsEVariable gaussNull t (gaussNumeraire s t)

E*_t ∈ ℰ_t.

theorem LogOptimal.isNumeraire_gaussNumeraire_mixAlt_of_one_le {s ρ : ℝ} (hs : 0 < s) (hρ : 1 - s ^ 2 ≤ ρ ^ 2) {t : ℕ} (ht : 1 ≤ t) : IsNumeraire gaussNull (mixAlt s ρ) t (gaussNumeraire s t) ∧ IsNumeraireDensity (mixAlt s ρ) t (gaussNumeraire s t) ((ProbabilityTheory.gaussianReal 0 (ρ ^ 2 - (1 - s ^ 2) / ↑t).toNNReal).bind fun (θ : ℝ) => marginal (nullDist θ) t)

Proposition 2, numéraire: for ρ² ≥ 1 − s² and t ≥ 1, E*_t = dQ_t/dP*_t with the mixture P*_t = ∫ P_{θ,t} N{0, ρ² − (1 − s²)/t}(dθ) of null distributions, so that E*_t is the numéraire and P*_t the measure in eq. (2).

theorem LogOptimal.isNumeraire_gaussNumeraire_mixAlt {s ρ : ℝ} (hs : 0 < s) (hρ : 1 - s ^ 2 ≤ ρ ^ 2) (t : ℕ) : IsNumeraire gaussNull (mixAlt s ρ) t (gaussNumeraire s t)

Partial result 1: for s > 0 and ρ² ≥ 1 − s², E*_t = ∏_{i=2}^t ℓ(Y_i) is the numéraire of the mixture Q at every horizon t ≥ 0; at t = 0, E*_0 = 1.

theorem LogOptimal.setting_mixAlt_of_isNumeraire {s ρ : ℝ} (hs : 0 < s) {Es : ℕ → (ℕ → ℝ) → ENNReal} (hEs : ∀ (t : ℕ), IsNumeraire gaussNull (mixAlt s ρ) t (Es t)) : Setting gaussNull (mixAlt s ρ) Es

Partial result 2: for s > 0 and every ρ, numéraires of the mixture Q at every horizon give the setting of Sections 1 and 2; the standing assumption follows from sup_{E ∈ ℰ_t} E_Q(log E) ≤ tκ.

theorem LogOptimal.setting_gaussNumeraire_mixAlt {s ρ : ℝ} (hs : 0 < s) (hρ : 1 - s ^ 2 ≤ ρ ^ 2) : Setting gaussNull (mixAlt s ρ) (gaussNumeraire s)

Partial result 1, the setting: for s > 0 and ρ² ≥ 1 − s², the numéraires of Proposition 2 give the setting of Sections 1 and 2.

Proposition 2

theorem LogOptimal.prop_numeraire_proof (s ρ : ℝ) : 0 < s → 0 ≤ ρ → 1 - s ^ 2 ≤ ρ ^ 2 → (∀ (t : ℕ), 1 ≤ t → IsNumeraire gaussNull (mixAlt s ρ) t (gaussNumeraire s t) ∧ IsNumeraireDensity (mixAlt s ρ) t (gaussNumeraire s t) ((ProbabilityTheory.gaussianReal 0 (ρ ^ 2 - (1 - s ^ 2) / ↑t).toNNReal).bind fun (θ : ℝ) => marginal (nullDist θ) t) ∧ ePower (mixAlt s ρ) (gaussNumeraire s t) = ↑((↑t - 1) * kappa s)) ∧ InformationTheory.klDiv (ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal) (ProbabilityTheory.gaussianReal 0 1) = ENNReal.ofReal (kappa s) ∧ IsTestMartingale gaussNull helmertFiltration fun (t : ℕ) (x : ℕ → ℝ) => ∏ i ∈ Finset.Icc 2 t, lik s (helmertY i x)