Gaussian integrals: eqs. (S1) and (S2), the likelihood ratio ℓ, and κ

This file proves the facts on the likelihood ratio ℓ = φ_{s²}/φ₁ of Section 4.1 and of Section S1.1 of the supplementary material, following the paper. With b = s^{-2} − 1:

• lik_eq and log_lik: ℓ(y) = s^{-1} exp(−by²/2) and log ℓ(y) = −log s − by²/2;
• integral_lik_affine: eq. (S1), E{ℓ(m + v^{1/2}Z)} = {s(1 + bv)^{1/2}}^{-1} exp{−bm²/(2 + 2bv)} for Z ∼ N(0, 1), by completing the square;
• integral_lik_add: the case v = 1, E{ℓ(m + Z)} = exp{−(1 − s²)m²/2};
• lik_lt_lik and integral_lik: for s < 1, ℓ(y) decreases in |y|, and E{ℓ(Z)} = 1 (Section 4.1);
• prod_gaussianPDFReal_eq: eq. (S2), ∏_{i=1}^t φ_v(x_i − m) = t^{-1/2} φ_{v/t}(x̄_t − m) ∏_{i=2}^t φ_v(y_i), from Lemma S2(i);
• gaussianReal_zero_eq_withDensity_lik and klDiv_gaussianReal: N(0, s²) has density ℓ with respect to N(0, 1), so that κ = KL{N(0, s²) ‖ N(0, 1)} = E{log ℓ(sZ)} = (s² − 1 − log s²)/2 (Proposition 2);
• eq_S_gauss_proof, eq_S_factor_proof, and sec4_lik_proof: the statements of the paper, and prop_numeraire_klDiv the claim on κ of the statement prop_numeraire.

The likelihood ratio ℓ

theorem LogOptimal.coe_toNNReal_sq (s : ℝ) : ↑(s ^ 2).toNNReal = s ^ 2

theorem LogOptimal.lik_eq {s : ℝ} (hs : 0 < s) (y : ℝ) : lik s y = s⁻¹ * Real.exp (-(s⁻¹ ^ 2 - 1) * y ^ 2 / 2)

ℓ(y) = s^{-1} exp(−by²/2) with b = s^{-2} − 1.

theorem LogOptimal.lik_pos {s : ℝ} (hs : 0 < s) (y : ℝ) : 0 < lik s y

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

log ℓ(y) = −log s − by²/2 with b = s^{-2} − 1 (Section S1.1).

Equation (S1)

theorem LogOptimal.integral_lik_affine {s : ℝ} (hs : 0 < s) (m v : ℝ) (hv : 0 ≤ v) (hbv : 0 < 1 + (s⁻¹ ^ 2 - 1) * v) : ∫ (z : ℝ), lik s (m + √v * z) ∂ProbabilityTheory.gaussianReal 0 1 = (s * √(1 + (s⁻¹ ^ 2 - 1) * v))⁻¹ * Real.exp (-((s⁻¹ ^ 2 - 1) * m ^ 2) / (2 + 2 * (s⁻¹ ^ 2 - 1) * v))

Equation (S1): for m ∈ ℝ, v ≥ 0 with 1 + bv > 0, and Z ∼ N(0, 1), completing the square gives E{ℓ(m + v^{1/2}Z)} = {s(1 + bv)^{1/2}}^{-1} exp{−bm²/(2 + 2bv)}.

theorem LogOptimal.integral_lik_add {s : ℝ} (hs : 0 < s) (m : ℝ) : ∫ (z : ℝ), lik s (m + z) ∂ProbabilityTheory.gaussianReal 0 1 = Real.exp (-((1 - s ^ 2) * m ^ 2) / 2)

Equation (S1) with v = 1: since s(1 + b)^{1/2} = 1 and b/(1 + b) = 1 − s², E{ℓ(m + Z)} = exp{−(1 − s²)m²/2}.

Properties of ℓ (Section 4.1)

theorem LogOptimal.lik_lt_lik {s : ℝ} (hs : 0 < s) (hs1 : s < 1) {y y' : ℝ} (h : |y| < |y'|) : lik s y' < lik s y

For s < 1, ℓ(y) decreases in |y|.

theorem LogOptimal.integral_lik {s : ℝ} (hs : 0 < s) : ∫ (y : ℝ), lik s y ∂ProbabilityTheory.gaussianReal 0 1 = 1

The expectation of ℓ under N(0, 1) is one: E{ℓ(Z)} = ∫ φ_{s²} = 1.

Equation (S2)

theorem LogOptimal.prod_gaussianPDFReal_zero (s : Finset ℕ) (v : NNReal) (f : ℕ → ℝ) : ∏ i ∈ s, ProbabilityTheory.gaussianPDFReal 0 v (f i) = (√(2 * Real.pi * ↑v))⁻¹ ^ s.card * Real.exp ((-∑ i ∈ s, f i ^ 2) / (2 * ↑v))

theorem LogOptimal.prod_gaussianPDFReal_eq {t : ℕ} (ht : 1 ≤ t) (x : ℕ → ℝ) (m : ℝ) {v : NNReal} (hv : 0 < v) : ∏ i ∈ Finset.range t, ProbabilityTheory.gaussianPDFReal 0 v (x i - m) = (√↑t)⁻¹ * ProbabilityTheory.gaussianPDFReal 0 (v / ↑t) (runningMean t x - m) * ∏ i ∈ Finset.Icc 2 t, ProbabilityTheory.gaussianPDFReal 0 v (helmertY i x)

Equation (S2): by Lemma S2(i), for x ∈ ℝ^t, every m ∈ ℝ, and every v > 0, ∏_{i=1}^t φ_v(x_i − m) = t^{-1/2} φ_{v/t}(x̄_t − m) ∏_{i=2}^t φ_v(y_i).

The divergence κ

theorem LogOptimal.gaussianReal_zero_eq_withDensity_lik {s : ℝ} (hs : 0 < s) : ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal = (ProbabilityTheory.gaussianReal 0 1).withDensity fun (y : ℝ) => ENNReal.ofReal (lik s y)

N(0, s²) has density ℓ with respect to N(0, 1).

theorem LogOptimal.integral_sq_gaussianReal (v : NNReal) : ∫ (y : ℝ), y ^ 2 ∂ProbabilityTheory.gaussianReal 0 v = ↑v

theorem LogOptimal.klDiv_gaussianReal {s : ℝ} (hs : 0 < s) : InformationTheory.klDiv (ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal) (ProbabilityTheory.gaussianReal 0 1) = ENNReal.ofReal (kappa s)

κ = KL{N(0, s²) ‖ N(0, 1)} = (s² − 1 − log s²)/2 (Proposition 2).

The statements of the paper

theorem LogOptimal.eq_S_gauss_proof (s : ℝ) : 0 < s → have b := s⁻¹ ^ 2 - 1; (∀ (y : ℝ), Real.log (lik s y) = -Real.log s - b * y ^ 2 / 2) ∧ (∀ (m v : ℝ), 0 ≤ v → 0 < 1 + b * v → ∫ (z : ℝ), lik s (m + √v * z) ∂ProbabilityTheory.gaussianReal 0 1 = (s * √(1 + b * v))⁻¹ * Real.exp (-(b * m ^ 2) / (2 + 2 * b * v))) ∧ ∀ (m : ℝ), ∫ (z : ℝ), lik s (m + z) ∂ProbabilityTheory.gaussianReal 0 1 = Real.exp (-((1 - s ^ 2) * m ^ 2) / 2)

theorem LogOptimal.eq_S_factor_proof (t : ℕ) : 1 ≤ t → ∀ (x : ℕ → ℝ) (m : ℝ) (v : NNReal), 0 < v → ∏ i ∈ Finset.range t, ProbabilityTheory.gaussianPDFReal 0 v (x i - m) = (√↑t)⁻¹ * ProbabilityTheory.gaussianPDFReal 0 (v / ↑t) (runningMean t x - m) * ∏ i ∈ Finset.Icc 2 t, ProbabilityTheory.gaussianPDFReal 0 v (helmertY i x)

theorem LogOptimal.sec4_lik_proof (s : ℝ) : 0 < s → (s < 1 → ∀ (y y' : ℝ), |y| < |y'| → lik s y' < lik s y) ∧ ∫ (y : ℝ), lik s y ∂ProbabilityTheory.gaussianReal 0 1 = 1

theorem LogOptimal.prop_numeraire_klDiv (s : ℝ) : 0 < s → InformationTheory.klDiv (ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal) (ProbabilityTheory.gaussianReal 0 1) = ENNReal.ofReal (kappa s)