Likelihood ratios in the Gaussian location model

This file computes the distributions of X^t under P_θ and Q_μ and the likelihood ratio L^θ_t = ∏_{i=1}^t ℓ(X_i − θ) of Q_θ against P_θ on ℱ_t (Section 4.2 of the paper).

• marginal_infinitePi: the distribution of X^t under N(m, v)^{⊗∞} is N(m, v)^{⊗t}.
• gaussianReal_eq_withDensity_lik: N(θ, s²) has density y ↦ ℓ(y − θ) with respect to N(θ, 1).
• marginal_altDist: Q_{θ,t} has density ∏_{i=1}^t ℓ(x_i − θ) with respect to P_{θ,t}.
• martingale_likProcess: under P_θ, (L^θ_t) is a martingale with respect to (ℱ_t).
• sec4_lik_process_proof and sec_simple_of_isNumeraire: the claims of Section 4.2 on L^θ_t and of Section S2.5 on the measure P*_t of Q_μ and on the mixing variance.

Marginals of product measures

theorem LogOptimal.marginal_infinitePi {𝒳 : Type u_1} [MeasurableSpace 𝒳] (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsProbabilityMeasure ν] (t : ℕ) : marginal (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ν) t = MeasureTheory.Measure.pi fun (x : Fin t) => ν

The likelihood ratio ℓ

theorem LogOptimal.lik_nonneg (s y : ℝ) : 0 ≤ lik s y

theorem LogOptimal.measurable_lik_sub (s θ : ℝ) : Measurable fun (y : ℝ) => ENNReal.ofReal (lik s (y - θ))

theorem LogOptimal.sq_toNNReal_ne_zero {s : ℝ} (hs : s ≠ 0) : (s ^ 2).toNNReal ≠ 0

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

N(θ, s²) has density y ↦ ℓ(y − θ) with respect to N(θ, 1).

theorem LogOptimal.lintegral_lik_sub (s θ : ℝ) (hs : s ≠ 0) : ∫⁻ (y : ℝ), ENNReal.ofReal (lik s (y - θ)) ∂ProbabilityTheory.gaussianReal θ 1 = 1

theorem LogOptimal.lintegral_lik_coord {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (i : ℕ) : ∫⁻ (x : ℕ → ℝ), ENNReal.ofReal (lik s (x i - θ)) ∂nullDist θ = 1

theorem LogOptimal.measurable_lik_coord (s θ : ℝ) (i : ℕ) : Measurable fun (x : ℕ → ℝ) => lik s (x i - θ)

The distributions of X^t

theorem LogOptimal.marginal_altDist {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (t : ℕ) : marginal (altDist s θ) t = (marginal (nullDist θ) t).withDensity fun (y : Fin t → ℝ) => ENNReal.ofReal (∏ i : Fin t, lik s (y i - θ))

The distribution Q_{θ,t} of X^t under Q_θ has density ∏_{i=1}^t ℓ(x_i − θ) with respect to the distribution P_{θ,t} of X^t under P_θ.

The likelihood ratio L^θ_t

theorem LogOptimal.likProcess_nonneg (s θ : ℝ) (t : ℕ) (x : ℕ → ℝ) : 0 ≤ likProcess s θ t x

theorem LogOptimal.likProcess_zero (s θ : ℝ) (x : ℕ → ℝ) : likProcess s θ 0 x = 1

theorem LogOptimal.likProcess_succ (s θ : ℝ) (t : ℕ) (x : ℕ → ℝ) : likProcess s θ (t + 1) x = likProcess s θ t x * lik s (x t - θ)

theorem LogOptimal.stronglyMeasurable_likProcess (s θ : ℝ) (t : ℕ) : MeasureTheory.StronglyMeasurable (likProcess s θ t)

theorem LogOptimal.iIndepFun_coord (θ : ℝ) : ProbabilityTheory.iIndepFun (fun (i : ℕ) (x : ℕ → ℝ) => x i) (nullDist θ)

theorem LogOptimal.lintegral_likProcess {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (t : ℕ) : ∫⁻ (x : ℕ → ℝ), ENNReal.ofReal (likProcess s θ t x) ∂nullDist θ = 1

theorem LogOptimal.integrable_likProcess {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (t : ℕ) : MeasureTheory.Integrable (likProcess s θ t) (nullDist θ)

theorem LogOptimal.indep_coord_dataFiltration (θ : ℝ) (t : ℕ) : ProbabilityTheory.Indep (MeasurableSpace.comap (fun (x : ℕ → ℝ) => x t) inferInstance) (↑(dataFiltration ℝ) t) (nullDist θ)

theorem LogOptimal.martingale_likProcess {s : ℝ} (hs : s ≠ 0) (θ : ℝ) : MeasureTheory.Martingale (likProcess s θ) (dataFiltration ℝ) (nullDist θ)

theorem LogOptimal.sec4_lik_process_proof (s θ : ℝ) : 0 < s → (∀ (t : ℕ), marginal (altDist s θ) t = (marginal (nullDist θ) t).withDensity fun (y : Fin t → ℝ) => ENNReal.ofReal (∏ i : Fin t, lik s (y i - θ))) ∧ (∀ (t : ℕ) (x : ℕ → ℝ), 0 ≤ likProcess s θ t x) ∧ (∀ (x : ℕ → ℝ), likProcess s θ 0 x = 1) ∧ MeasureTheory.Martingale (likProcess s θ) (dataFiltration ℝ) (nullDist θ)

The measure P*_t of Q_μ and the mixing variance

theorem LogOptimal.mixAlt_zero (s : ℝ) : mixAlt s 0 = altDist s 0

theorem LogOptimal.sec_simple_of_isNumeraire (h : ∀ (s μ : ℝ), 0 < s → s ≤ 1 → ∀ (t : ℕ), IsNumeraire gaussNull (altDist s μ) t fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)) : (∀ (s μ : ℝ), 0 < s → s ≤ 1 → ∀ (t : ℕ), (IsNumeraire gaussNull (altDist s μ) t fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)) ∧ IsNumeraireDensity (altDist s μ) t (fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)) (marginal (nullDist μ) t)) ∧ (∀ (s ρ : ℝ), (∀ (t : ℕ), 1 ≤ t → 0 ≤ ρ ^ 2 - (1 - s ^ 2) / ↑t) ↔ 1 - s ^ 2 ≤ ρ ^ 2) ∧ (∀ (s : ℝ), mixAlt s 0 = altDist s 0) ∧ ∀ (s : ℝ), 0 < s → (1 - s ^ 2 ≤ 0 ^ 2 ↔ 1 ≤ s)

The claims of Section S2.5 (sec_simple), given the numéraire property of L^μ_t for s ≤ 1 (Proposition S4(i)).