Objects of the statements

This file defines the objects that appear only in the statements of LogOptimalEProcesses.Paper:

• Setting 𝔓 Q Es: the setting of Sections 1 and 2;

• the measurability of θ ↦ P_θ and μ ↦ Q_μ, and the kernels nullKernel and altKernel s;

• worstCaseMinimaxRegret s Esμ T: the minimax regret in the worst case over μ of Theorem 1, inf_{(E_t)} max_{0 ≤ t ≤ T} sup_{μ ∈ ℝ} R^μ_t(E_t);

• helmertVec t: the vector Y^t = (Y₂, …, Y_t);

• mutualInfo μ f g: the mutual information of two random variables, Proposition S3;

• the objects of the lower-bound proof of Proposition 3(i), Lemmas S4 to S6: the horizons t_k = r^k, the uniform ξ on {t₀, …, t_K}, the stopping rule τ', the randomized stopping time τ, the mixture P̄, the variables W_{jk}, the sets 𝒵_k(y), the functions J_k of eq. (S7), the probabilities p_k, the events A_k, and the constants β, β', and c'.

The setting of Sections 1 and 2

structure LogOptimal.Setting {𝒳 : Type u_1} [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal) : Prop

The setting of Sections 1 and 2: the null distributions and the alternative are probability measures, Es t = E*_t is a numéraire at every horizon t (in the versions fixed in Section 2), and the standing assumption sup_{E ∈ ℰ_t} E_Q(log E) < ∞ holds.

• isProbabilityMeasure_null (P : MeasureTheory.Measure (ℕ → 𝒳)) : P ∈ 𝔓 → MeasureTheory.IsProbabilityMeasure P

  The null distributions are probability measures.

• isProbabilityMeasure_alt : MeasureTheory.IsProbabilityMeasure Q

  The alternative is a probability measure.

• isNumeraire (t : ℕ) : IsNumeraire 𝔓 Q t (Es t)

  E*_t is a numéraire at every horizon t.

• finiteOptimalEPower : FiniteOptimalEPower 𝔓 Q

  The standing assumption of Section 2.

Kernels of null and alternative distributions

instance LogOptimal.instIsProbabilityMeasureForallNatRealNullDist (θ : ℝ) : MeasureTheory.IsProbabilityMeasure (nullDist θ)

instance LogOptimal.instIsProbabilityMeasureForallNatRealAltDist (s μ : ℝ) : MeasureTheory.IsProbabilityMeasure (altDist s μ)

instance LogOptimal.instIsProbabilityMeasureForallNatRealStdGaussSeq : MeasureTheory.IsProbabilityMeasure stdGaussSeq

theorem LogOptimal.infinitePi_gaussianReal_eq_map (μ : ℝ) (v : NNReal) : (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal μ v) = MeasureTheory.Measure.map (fun (z : ℕ → ℝ) (i : ℕ) => μ + z i) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal 0 v)

N(μ, v)^{⊗∞} is the image of N(0, v)^{⊗∞} under the shift by μ of every coordinate.

theorem LogOptimal.measurable_infinitePi_gaussianReal (v : NNReal) : Measurable fun (μ : ℝ) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal μ v

μ ↦ N(μ, v)^{⊗∞} is measurable.

theorem LogOptimal.measurable_nullDist : Measurable nullDist

theorem LogOptimal.measurable_altDist (s : ℝ) : Measurable (altDist s)

noncomputable def LogOptimal.nullKernel : ProbabilityTheory.Kernel ℝ (ℕ → ℝ)

The probability kernel θ ↦ P_θ.

Equations

• LogOptimal.nullKernel = { toFun := LogOptimal.nullDist, measurable' := LogOptimal.measurable_nullDist }

noncomputable def LogOptimal.altKernel (s : ℝ) : ProbabilityTheory.Kernel ℝ (ℕ → ℝ)

The probability kernel μ ↦ Q_μ.

Equations

• LogOptimal.altKernel s = { toFun := LogOptimal.altDist s, measurable' := ⋯ }

instance LogOptimal.instIsMarkovKernelRealForallNatNullKernel : ProbabilityTheory.IsMarkovKernel nullKernel

instance LogOptimal.instIsMarkovKernelRealForallNatAltKernel (s : ℝ) : ProbabilityTheory.IsMarkovKernel (altKernel s)

instance LogOptimal.instIsProbabilityMeasureForallNatRealMixAlt (s ρ : ℝ) : MeasureTheory.IsProbabilityMeasure (mixAlt s ρ)

The minimax regret in the worst case over the location

noncomputable def LogOptimal.worstCaseMinimaxRegret (s : ℝ) (Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal) (T : ℕ) : EReal

The minimax regret in the worst case over μ of Theorem 1, inf_{(E_t)} max_{0 ≤ t ≤ T} sup_{μ ∈ ℝ} R^μ_t(E_t), where the infimum runs over the e-processes for the Gaussian location null and R^μ_t is the regret defined by eqs. (2) and (3) with Q_μ in place of Q, with the numéraires Esμ μ t of Q_μ.

Equations

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

The vector Y^t and mutual information

noncomputable def LogOptimal.helmertVec (t : ℕ) (x : ℕ → ℝ) : Fin (t - 1) → ℝ

The vector Y^t = (Y₂, …, Y_t), indexed by Fin (t - 1).

Equations

• LogOptimal.helmertVec t x i = LogOptimal.helmertY (↑i + 2) x

noncomputable def LogOptimal.mutualInfo {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) (f : Ω → α) (g : Ω → β) : ENNReal

The mutual information I(f; g) of two random variables, the Kullback–Leibler divergence of their joint distribution from the product of their distributions.

Equations

• LogOptimal.mutualInfo μ f g = InformationTheory.klDiv (MeasureTheory.Measure.map (fun (ω : Ω) => (f ω, g ω)) μ) ((MeasureTheory.Measure.map f μ).prod (MeasureTheory.Measure.map g μ))

The objects of Lemmas S4 to S6

noncomputable def LogOptimal.lbWeights (r K T : ℕ) : Fin (T + 1) → ℝ

The uniform ξ ∈ Δ_T on the horizons t_k = r^k, 0 ≤ k ≤ K, of the lower-bound proof of Proposition 3(i).

Equations

• LogOptimal.lbWeights r K T t = if ∃ k ≤ K, ↑t = r ^ k then 1 / (↑K + 1) else 0

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

The standardized running mean Z_t = t^{1/2}(X̄_t − θ).

Equations

• LogOptimal.lbZ θ t x = √↑t * (LogOptimal.runningMean t x - θ)

noncomputable def LogOptimal.lbStoppingRule (r K : ℕ) (c θ : ℝ) (x : ℕ → ℝ) : ℕ∞

The stopping rule τ' of Section S1.6: the first horizon t_k = r^k, k ≤ K, with c ≤ |Z_{t_k}| ≤ c + 1, or ∞ if there is none.

Equations

• LogOptimal.lbStoppingRule r K c θ x = if h : ∃ k ≤ K, c ≤ |LogOptimal.lbZ θ (r ^ k) x| ∧ |LogOptimal.lbZ θ (r ^ k) x| ≤ c + 1 then ↑(r ^ Nat.find h) else ⊤

noncomputable def LogOptimal.lbRandomizedRule (r K : ℕ) (c θ : ℝ) (x : ℕ → ℝ) (u : ↑unitInterval) : ℕ∞

The randomized stopping time τ of Section S1.6: τ = τ' with probability 1/2, and otherwise τ ∼ ξ independent of X. With u uniform on [0, 1], τ = τ' when u < 1/2, and τ = t_k with k = min{K, ⌊(2u − 1)(K + 1)⌋} otherwise, which is uniform on {0, …, K}.

Equations

• LogOptimal.lbRandomizedRule r K c θ x u = if ↑u < 1 / 2 then LogOptimal.lbStoppingRule r K c θ x else ↑(r ^ min K ⌊(2 * ↑u - 1) * (↑K + 1)⌋₊)

noncomputable def LogOptimal.lbMixture (s ρ : ℝ) (r K : ℕ) (c : ℝ) : MeasureTheory.Measure (StoppedPath ℝ)

The mixture P̄ of Section S1.6: the distribution of (τ, X^τ), where θ ∼ N(0, γ²) with γ² = ρ² + s², X ∼ P_θ given θ, and τ is the randomized stopping time lbRandomizedRule.

Equations

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

noncomputable def LogOptimal.lbW (r j k : ℕ) (x : ℕ → ℝ) : ℝ

The variable W_{jk}(y) = t_j^{1/2} ∑_{i = t_j + 1}^{t_k} y_i/{i(i − 1)}^{1/2} of Section S1.6, as a function of the path, with y_i = Y_i.

Equations

• LogOptimal.lbW r j k x = √(↑r ^ j) * ∑ i ∈ Finset.Ioc (r ^ j) (r ^ k), LogOptimal.helmertY i x / √(↑i * (↑i - 1))

noncomputable def LogOptimal.lbZset (r k : ℕ) (c : ℝ) (x : ℕ → ℝ) : Set ℝ

The set 𝒵_k(y) = {z : c ≤ |z| ≤ c + 1} ∖ ⋃_{j < k} {z : c ≤ |(t_j/t_k)^{1/2}z − W_{jk}(y)| ≤ c + 1} of Section S1.6, as a function of the path.

Equations

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

noncomputable def LogOptimal.lbJ (s ρ : ℝ) (r K : ℕ) (c : ℝ) (k : ℕ) (x : ℕ → ℝ) : ℝ

The function J_k of eq. (S7), with t = t_k = r^k, γ² = ρ² + s², and ξ_{t_k} = 1/(K + 1): `J_k(x) = {2φ_{ρ²+s²/t}(x̄_t)}^{-1}{∫{𝒵_k(y)} φ₁(z)φ{γ²}(x̄_t − t^{-1/2}z) dz

• ξ_t φ_{γ²+1/t}(x̄_t)}`.

Equations

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

noncomputable def LogOptimal.lbP (r k : ℕ) (c : ℝ) (x : ℕ → ℝ) : ℝ

The probability p_k(y) = ∫_{𝒵_k(y)} φ₁(z) dz of Lemma S5, as a function of the path.

Equations

• LogOptimal.lbP r k c x = ∫ (z : ℝ) in LogOptimal.lbZset r k c x, ProbabilityTheory.gaussianPDFReal 0 1 z

noncomputable def LogOptimal.lbCPrime (r : ℕ) (c : ℝ) : ℝ

The constant c' = c − (c + 1)r^{-1/2} of Lemma S5.

Equations

• LogOptimal.lbCPrime r c = c - (c + 1) / √↑r

def LogOptimal.lbA (r k : ℕ) (c' : ℝ) : Set (ℕ → ℝ)

The event A_k = {y : max_{j < k} |W_{jk}(y)| < c'} of Lemma S5, as a set of paths.

Equations

• LogOptimal.lbA r k c' = {x : ℕ → ℝ | ∀ j < k, |LogOptimal.lbW r j k x| < c'}

noncomputable def LogOptimal.lbBetaPrime (s ρ : ℝ) : ℝ

The constant β' = ½ log{ρ²/(γ² + 1)} − log 2 of Lemma S5, with γ² = ρ² + s².

Equations

• LogOptimal.lbBetaPrime s ρ = Real.log (ρ ^ 2 / (ρ ^ 2 + s ^ 2 + 1)) / 2 - Real.log 2

noncomputable def LogOptimal.lbBeta (s ρ : ℝ) (K : ℕ) (c : ℝ) : ℝ

The constant β = log(K + 1) + log φ₁(c + 1) + log(ρ/γ) of Lemma S6, with γ = (ρ² + s²)^{1/2}.

Equations

• LogOptimal.lbBeta s ρ K c = Real.log (↑K + 1) + Real.log (ProbabilityTheory.gaussianPDFReal 0 1 (c + 1)) + Real.log (ρ / √(ρ ^ 2 + s ^ 2))