The Gaussian location model

This file defines the objects of Section 4 of the paper and of Sections S1 and S2 of its supplementary material. The observations take values in 𝒳 = ℝ, and the coordinate x i of a path x : ℕ → ℝ is the observation X_{i+1}.

• nullDist θ: the null distribution P_θ = N(θ, 1)^{⊗∞}, and gaussNull the null 𝔓 = {P_θ : θ ∈ ℝ};
• altDist s μ: the alternative Q_μ = N(μ, s²)^{⊗∞}, and mixAlt s ρ the mixture Q = ∫ Q_μ N(0, ρ²)(dμ), where N(0, 0) is the unit mass at zero;
• runningMean t x: the running mean X̄_t = t^{-1} ∑_{i=1}^t X_i;
• helmertY i x: the variable Y_i = {(i − 1)/i}^{1/2}(X_i − X̄_{i−1}) of eq. (7), for i ≥ 2;
• lik s y: the likelihood ratio ℓ = φ_{s²}/φ₁, where φ_v is the density of N(0, v);
• kappa s: κ = (s² − 1 − log s²)/2;
• helmertFiltration: the filtration (𝒢_t) generated by (Y_t)_{t ≥ 2}, with 𝒢₀ and 𝒢₁ trivial;
• gaussNumeraire s t: the numéraire E*_t = ∏_{i=2}^t ℓ(Y_i) of Proposition 2;
• likProcess s θ t: the likelihood ratio L^θ_t = ∏_{i=1}^t ℓ(X_i − θ) of Q_θ against P_θ;
• stdGaussSeq, walk t, walkFiltration, reward s t: the random walk (S_t) with S₀ = 0 and independent N(0, 1) increments, realized on the space of its increments, the filtration generated by (S_t), and the reward h_t of Lemma 2;
• horizon j, blockRatio s j, etaBound s j, mixtureEProcess s: the horizons T_j = ⌈exp(e^j)⌉, the ratios q_j, the bounds u_j, and the e-process of Proposition 3(ii);
• runningMeanProcess s t: the process Ẽ_t = ∏_{i=2}^t ℓ(X_i − X̄_{i−1}) of Proposition S6.

Variances are nonnegative reals in Mathlib's gaussianReal; the variances s² and ρ² are (s ^ 2).toNNReal and (ρ ^ 2).toNNReal.

The null and the alternative

noncomputable def LogOptimal.nullDist (θ : ℝ) : MeasureTheory.Measure (ℕ → ℝ)

The null distribution P_θ = N(θ, 1)^{⊗∞} of Section 4.

Equations

• LogOptimal.nullDist θ = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal θ 1

def LogOptimal.gaussNull : Set (MeasureTheory.Measure (ℕ → ℝ))

The Gaussian location null 𝔓 = {P_θ : θ ∈ ℝ} of Section 4.

Equations

• LogOptimal.gaussNull = Set.range LogOptimal.nullDist

noncomputable def LogOptimal.altDist (s μ : ℝ) : MeasureTheory.Measure (ℕ → ℝ)

The alternative Q_μ = N(μ, s²)^{⊗∞} of Section 4.

Equations

• LogOptimal.altDist s μ = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal μ (s ^ 2).toNNReal

noncomputable def LogOptimal.mixAlt (s ρ : ℝ) : MeasureTheory.Measure (ℕ → ℝ)

The alternative Q = ∫ Q_μ N(0, ρ²)(dμ) of Section 4, where N(0, 0) is the unit mass at zero.

Equations

• LogOptimal.mixAlt s ρ = (ProbabilityTheory.gaussianReal 0 (ρ ^ 2).toNNReal).bind (LogOptimal.altDist s)

The running mean and the variables Y_i

noncomputable def LogOptimal.runningMean (t : ℕ) (x : ℕ → ℝ) : ℝ

The running mean X̄_t = t^{-1} ∑_{i=1}^t X_i.

Equations

• LogOptimal.runningMean t x = (∑ i ∈ Finset.range t, x i) / ↑t

noncomputable def LogOptimal.helmertY (i : ℕ) (x : ℕ → ℝ) : ℝ

The variable Y_i = {(i − 1)/i}^{1/2}(X_i − X̄_{i−1}) of eq. (7), for i ≥ 2.

Equations

• LogOptimal.helmertY i x = √((↑i - 1) / ↑i) * (x (i - 1) - LogOptimal.runningMean (i - 1) x)

theorem LogOptimal.measurable_runningMean (t : ℕ) : Measurable (runningMean t)

theorem LogOptimal.measurable_helmertY (i : ℕ) : Measurable (helmertY i)

noncomputable def LogOptimal.helmertFiltration : MeasureTheory.Filtration ℕ MeasurableSpace.pi

The filtration (𝒢_t)_{t ≥ 0} generated by (Y_t)_{t ≥ 2}, with 𝒢₀ and 𝒢₁ trivial.

Equations

• One or more equations did not get rendered due to their size.

Likelihood ratios and numéraires

noncomputable def LogOptimal.lik (s y : ℝ) : ℝ

The likelihood ratio ℓ = φ_{s²}/φ₁, where φ_v is the density of N(0, v).

Equations

• LogOptimal.lik s y = ProbabilityTheory.gaussianPDFReal 0 (s ^ 2).toNNReal y / ProbabilityTheory.gaussianPDFReal 0 1 y

theorem LogOptimal.measurable_lik (s : ℝ) : Measurable (lik s)

theorem LogOptimal.measurable_gaussianReal_mean (v : NNReal) : Measurable fun (m : ℝ) => ProbabilityTheory.gaussianReal m v

theorem LogOptimal.gaussianReal_bind_gaussianReal (m : ℝ) (a b : NNReal) : ((ProbabilityTheory.gaussianReal m a).bind fun (θ : ℝ) => ProbabilityTheory.gaussianReal θ b) = ProbabilityTheory.gaussianReal m (a + b)

The mixture of N(θ, b) over θ ∼ N(m, a) is N(m, a + b).

noncomputable def LogOptimal.notepCond (s θ : ℝ) (x : ℕ → ℝ) : ℝ

The conditional expectation E_θ(E*_2 ∣ X_1) = {2/(1 + s²)}^{1/2} exp{−(1 − s²)(X_1 − θ)²/(2 + 2s²)} of eq. (S15), as a function of the path.

Equations

• LogOptimal.notepCond s θ x = √(2 / (1 + s ^ 2)) * Real.exp (-((1 - s ^ 2) * (x 0 - θ) ^ 2) / (2 + 2 * s ^ 2))

noncomputable def LogOptimal.kappa (s : ℝ) : ℝ

κ = (s² − 1 − log s²)/2, the Kullback–Leibler divergence of N(0, s²) from N(0, 1).

Equations

• LogOptimal.kappa s = (s ^ 2 - 1 - Real.log (s ^ 2)) / 2

noncomputable def LogOptimal.gaussNumeraire (s : ℝ) (t : ℕ) (x : ℕ → ℝ) : ENNReal

The numéraire E*_t = ∏_{i=2}^t ℓ(Y_i) of Proposition 2, equal to one for t ≤ 1.

Equations

• LogOptimal.gaussNumeraire s t x = ENNReal.ofReal (∏ i ∈ Finset.Icc 2 t, LogOptimal.lik s (LogOptimal.helmertY i x))

noncomputable def LogOptimal.likProcess (s θ : ℝ) (t : ℕ) (x : ℕ → ℝ) : ℝ

The likelihood ratio L^θ_t = ∏_{i=1}^t ℓ(X_i − θ) of Q_θ against P_θ on ℱ_t, with L^θ₀ = 1 (Section 4.2).

Equations

• LogOptimal.likProcess s θ t x = ∏ i ∈ Finset.range t, LogOptimal.lik s (x i - θ)

The random walk of Lemma 2

noncomputable def LogOptimal.stdGaussSeq : MeasureTheory.Measure (ℕ → ℝ)

The distribution N(0, 1)^{⊗∞} of the increments of the random walk (S_t) of Lemma 2.

Equations

• LogOptimal.stdGaussSeq = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal 0 1

def LogOptimal.walk (t : ℕ) (ω : ℕ → ℝ) : ℝ

The random walk S_t = ∑_{i < t} ω_i with S₀ = 0, as a function of its increments ω.

Equations

• LogOptimal.walk t ω = ∑ i ∈ Finset.range t, ω i

theorem LogOptimal.measurable_walk (t : ℕ) : Measurable (walk t)

def LogOptimal.walkFiltration : MeasureTheory.Filtration ℕ MeasurableSpace.pi

The filtration generated by the random walk (S_t)_{t ≥ 0}.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LogOptimal.reward (s : ℝ) (t : ℕ) (ω : ℕ → ℝ) : ℝ

The reward h_t = s exp{(1 − s²)S_t²/(2t)} of Lemma 2, with h₀ = 1.

Equations

• LogOptimal.reward s t ω = if t = 0 then 1 else s * Real.exp ((1 - s ^ 2) * LogOptimal.walk t ω ^ 2 / (2 * ↑t))

The e-process of Proposition 3(ii)

noncomputable def LogOptimal.horizon (j : ℕ) : ℕ

The horizon T_j = ⌈exp(e^j)⌉ of Proposition 3(ii).

Equations

• LogOptimal.horizon j = ⌈Real.exp (Real.exp ↑j)⌉₊

noncomputable def LogOptimal.blockRatio (s : ℝ) (j : ℕ) : ℝ

The ratio q_j = 1 + s²/{(1 − s²)(j + 1)} of Proposition 3(ii).

Equations

• LogOptimal.blockRatio s j = 1 + s ^ 2 / ((1 - s ^ 2) * (↑j + 1))

noncomputable def LogOptimal.etaBound (s : ℝ) (j : ℕ) : ℝ

The bound u_j = {(j + 1)/(s² j)}(2 + 2 log T_j / log q_j)^{1 − s² j/(j + 1)} of Proposition 3(ii).

Equations

• LogOptimal.etaBound s j = (↑j + 1) / (s ^ 2 * ↑j) * (2 + 2 * Real.log ↑(LogOptimal.horizon j) / Real.log (LogOptimal.blockRatio s j)) ^ (1 - s ^ 2 * ↑j / (↑j + 1))

noncomputable def LogOptimal.mixtureEProcess (s : ℝ) (t : ℕ) (x : ℕ → ℝ) : ENNReal

The e-process E_t = ∑_{j ≥ 1} E*_{t ∧ T_j}/{j(j + 1)u_j} of Proposition 3(ii).

Equations

• One or more equations did not get rendered due to their size.

The process with the running mean of Proposition S6

noncomputable def LogOptimal.runningMeanProcess (s : ℝ) (t : ℕ) (x : ℕ → ℝ) : ENNReal

The process Ẽ_t = ∏_{i=2}^t ℓ(X_i − X̄_{i−1}) of Proposition S6.

Equations

• LogOptimal.runningMeanProcess s t x = ENNReal.ofReal (∏ i ∈ Finset.Icc 2 t, LogOptimal.lik s (x (i - 1) - LogOptimal.runningMean (i - 1) x))