An initial enlargement: Proposition S3 #

This file proves Proposition S3 of the supplementary material and the claim of Section S2.4 on the two suprema of the stopped numéraires, following the paper.

(i) By Lemma S2(ii), X̄_t = X₁ + ∑_{i=2}^t Y_i/{i(i − 1)}^{1/2}, and X̄_t → θ almost surely under P_θ by the strong law of large numbers.

(ii) By Lemma S2(iii), X̄_t ∼ N(θ, 1/t) is independent of Y^t under P_θ, so that X₁ = X̄_t − ∑_{i=2}^t Y_i/{i(i − 1)}^{1/2} has the conditional distribution N[θ − ∑_{i=2}^t Y_i/{i(i − 1)}^{1/2}, 1/t] given Y^t. The mutual information is computed from the density of the joint distribution of (Y^t, X₁) with respect to the product of its marginals, the ratio of the densities of N(θ − ∑_{i=2}^t Y_i/{i(i − 1)}^{1/2}, 1/t) and N(θ, 1): the expectation of its logarithm is ½ log t − t E_θ{(X̄_t − θ)²}/2 + E_θ{(X₁ − θ)²}/2 = ½ log t. The paper obtains this value as the difference between the differential entropies of N(0, 1) and N(0, 1/t).

(iii) Under P_θ, the translated sequence X'_i = X_i + θ' − θ has distribution P_{θ'}, the variables Y_i take the same values at X and at X', and the translation maps the stopping times of (ℱ_t) to stopping times of (ℱ_t).

The two suprema of Section S2.4 follow from Propositions 2 and S3(iii): the numéraires form a test martingale with respect to (𝒢_t), so that optional stopping at the bounded times τ ∧ T gives E_θ(E*_{τ∧T}) = 1 for the stopping times τ of (𝒢_t), and the supremum over the stopping times of (ℱ_t) is the same for every θ, hence equal to η_T.

ae_tendsto_sum_helmertY: Proposition S3(i);
enlargeShift, enlargeKernel, and enlargeDensity: the sum ∑_{i=2}^t y_i/{i(i − 1)}^{1/2}, the conditional distribution of X₁ given Y^t = y, and the density of the distribution of (Y^t, X₁) with respect to the product of the distributions of Y^t and of X₁;
condDistrib_coord_zero_helmertVec and mutualInfo_coord_zero_helmertVec: Proposition S3(ii);
iSup_lintegral_valueAt_eq and isEProcess_gaussNull_iff_exists: Proposition S3(iii);
prop_enlarge_proof and sec_enlarge_suprema_proof: the statements prop_enlarge and sec_enlarge_suprema.

Proposition S3(i) #

source

theorem LogOptimal.ae_tendsto_sum_helmertY (θ : ℝ) :

∀ᵐ (x : ℕ → ℝ) ∂nullDist θ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.Icc 2 n, helmertY i x / √(↑i * (↑i - 1))) Filter.atTop (nhds (θ - x 0))

Proposition S3(i): ∑_{i=2}^n Y_i/{i(i − 1)}^{1/2} → θ − X₁ almost surely under P_θ.

Proposition S3(ii): the conditional distribution of `X₁` given `Y^t` #

source

noncomputable def LogOptimal.enlargeShift (t : ℕ) (y : Fin (t - 1) → ℝ) :

ℝ

The sum g(y) = ∑_{i=2}^t y_i/{i(i − 1)}^{1/2} of Proposition S3(ii), for y = (y₂, …, y_t) indexed by Fin (t - 1), whose coordinate j is y_{j+2}.

Equations

LogOptimal.enlargeShift t y = ∑ i : Fin (t - 1), y i / √((↑↑i + 2) * (↑↑i + 1))

Instances For

source

theorem LogOptimal.measurable_enlargeShift (t : ℕ) :

Measurable (enlargeShift t)

source

noncomputable def LogOptimal.enlargeKernel (θ : ℝ) (t : ℕ) :

ProbabilityTheory.Kernel (Fin (t - 1) → ℝ) ℝ

The kernel y ↦ N(θ, 1/t) pushed forward by a ↦ a − g(y): the conditional distribution of X₁ given Y^t = y under P_θ.

Equations

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

Instances For

source

instance LogOptimal.instIsMarkovKernelForallFinHSubNatOfNatRealEnlargeKernel (θ : ℝ) (t : ℕ) :

ProbabilityTheory.IsMarkovKernel (enlargeKernel θ t)

The kernel y ↦ N(θ − g(y), 1/t) is a Markov kernel.

source

theorem LogOptimal.condDistrib_coord_zero_helmertVec (θ : ℝ) {t : ℕ} (ht : 1 ≤ t) :

∀ᵐ (y : Fin (t - 1) → ℝ) ∂MeasureTheory.Measure.map (helmertVec t) (nullDist θ), (ProbabilityTheory.condDistrib (fun (x : ℕ → ℝ) => x 0) (helmertVec t) (nullDist θ)) y = ProbabilityTheory.gaussianReal (θ - ∑ i : Fin (t - 1), y i / √((↑↑i + 2) * (↑↑i + 1))) (↑t)⁻¹

Proposition S3(ii), conditional distribution: under P_θ, the conditional distribution of X₁ given Y^t is N[θ − ∑_{i=2}^t Y_i/{i(i − 1)}^{1/2}, 1/t].

Proposition S3(ii): the mutual information #

source

noncomputable def LogOptimal.enlargeDensity (θ : ℝ) (t : ℕ) (p : (Fin (t - 1) → ℝ) × ℝ) :

ℝ

The density r(y, a) = φ_{1/t}(a − θ + g(y))/φ₁(a − θ) of the distribution of (Y^t, X₁) under P_θ with respect to the product of the distributions of Y^t and of X₁.

Equations

LogOptimal.enlargeDensity θ t p = ProbabilityTheory.gaussianPDFReal (θ - LogOptimal.enlargeShift t p.1) (↑t)⁻¹ p.2 / ProbabilityTheory.gaussianPDFReal θ 1 p.2

Instances For

source

theorem LogOptimal.mutualInfo_coord_zero_helmertVec (θ : ℝ) {t : ℕ} (ht : 1 ≤ t) :

mutualInfo (nullDist θ) (fun (x : ℕ → ℝ) => x 0) (helmertVec t) = ENNReal.ofReal (Real.log ↑t / 2)

Proposition S3(ii), mutual information: I(X₁; Y^t) = ½ log t under P_θ.

Proposition S3(iii): translation of the observations #

source

theorem LogOptimal.iSup_lintegral_valueAt_eq {E : ℕ → (ℕ → ℝ) → ENNReal} (hE : ∀ (t : ℕ), Measurable (E t)) (θ θ' : ℝ) :

⨆ (τ : (ℕ → ℝ) → ℕ∞), ⨆ (_ : MeasureTheory.IsStoppingTime (dataFiltration ℝ) τ), ∫⁻ (x : ℕ → ℝ), valueAt E τ x ∂nullDist θ = ⨆ (τ : (ℕ → ℝ) → ℕ∞), ⨆ (_ : MeasureTheory.IsStoppingTime (dataFiltration ℝ) τ), ∫⁻ (x : ℕ → ℝ), valueAt E τ x ∂nullDist θ'

Proposition S3(iii): for a process adapted to (𝒢_t), sup_τ E_θ(E_τ) over the stopping times of (ℱ_t) is the same for every θ.

source

theorem LogOptimal.isEProcess_gaussNull_iff_exists {E : ℕ → (ℕ → ℝ) → ENNReal} (hE : ∀ (t : ℕ), Measurable (E t)) :

IsEProcess gaussNull E ↔ ∃ (θ : ℝ), IsEProcess {nullDist θ} E

Proposition S3(iii), last claim: a process adapted to (𝒢_t) is an e-process for the Gaussian null if and only if it is an e-process for {P_θ} for some θ.