Stopping at the second observation: Proposition S2

This file proves Proposition S2 of the supplementary material and the claims of Section S2.3 that follow it, following the paper. Under P_θ and given X₁, Y₂ = (X₂ − X₁)/2^{1/2} is normal with mean (θ − X₁)/2^{1/2} and variance 1/2 (Section 4.1), and eq. (S1) with v = 1/2 gives eq. (S15), E_θ(E*_2 ∣ X₁) = {2/(1 + s²)}^{1/2} exp{−(1 − s²)(X₁ − θ)²/(2 + 2s²)}. Since E*_0 = E*_1 = 1 and every stopping time τ ≤ 2 of (ℱ_t) satisfies {τ ≤ 1} ∈ ℱ₁, E_θ(E*_τ) = E_θ{1(τ ≤ 1) + 1(τ = 2)E_θ(E*_2 ∣ X₁)} ≤ E_θ[max{1, E_θ(E*_2 ∣ X₁)}], with equality for τ = 1 + 1{E_θ(E*_2 ∣ X₁) > 1}, which gives eq. (S16).

• condExp_gaussNumeraire_two: eq. (S15);
• setLIntegral_gaussNumeraire_two: the defining property of eq. (S15) on the events of ℱ₁, written in [0, ∞];
• lintegral_valueAt_gaussNumeraire: E_θ(E*_τ) = P_θ(τ ≤ 1) + E_θ{1(τ = 2)E_θ(E*_2 ∣ X₁)} for every stopping time τ ≤ 2;
• one_lt_notepCond_iff: the region where E_θ(E*_2 ∣ X₁) exceeds one;
• one_lt_lintegral_max_notepCond: the right-hand side of eq. (S16) exceeds one for s ≠ 1;
• prop_notep_proof: Proposition S2, with the best stopping time 1 + 1{E_θ(E*_2 ∣ X₁) > 1};
• not_isEProcess_gaussNumeraire and marginal_nullDist_two_ac_mixAlt: the numéraires are not an e-process for s ≠ 1, and the null distributions of X² are absolutely continuous with respect to Q₂;
• minimaxRegret_pos_of_converse: Γ_T ≥ Γ₂ > 0 for T ≥ 2, given the setting of Sections 1 and 2 and the converse of Remark 1 (Proposition S1(i)) at T = 2.

Eq. (S15): the conditional expectation of E*_2 given X₁

theorem LogOptimal.condExp_gaussNumeraire_two {s : ℝ} (hs : 0 < s) (θ : ℝ) : (nullDist θ)[fun (x : ℕ → ℝ) => (gaussNumeraire s 2 x).toReal | ↑(dataFiltration ℝ) 1] =ᵐ[nullDist θ] notepCond s θ

Equation (S15): E_θ(E*_2 ∣ X₁) = {2/(1 + s²)}^{1/2} exp{−(1 − s²)(X₁ − θ)²/(2 + 2s²)}, by the conditional distribution of Y₂ given X₁ (Section 4.1) and eq. (S1) with v = 1/2.

theorem LogOptimal.setLIntegral_gaussNumeraire_two {s : ℝ} (hs : 0 < s) (θ : ℝ) {A : Set (ℕ → ℝ)} (hA : MeasurableSet A) : ∫⁻ (x : ℕ → ℝ) in A, gaussNumeraire s 2 x ∂nullDist θ = ∫⁻ (x : ℕ → ℝ) in A, ENNReal.ofReal (notepCond s θ x) ∂nullDist θ

The defining property of eq. (S15) on the events A ∈ ℱ₁, in [0, ∞]: E_θ{1_A E*_2} = E_θ{1_A E_θ(E*_2 ∣ X₁)}.

Stopping times bounded by two

theorem LogOptimal.lintegral_valueAt_gaussNumeraire {s : ℝ} (hs : 0 < s) (θ : ℝ) {τ : (ℕ → ℝ) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration ℝ) τ) (hτ2 : ∀ (x : ℕ → ℝ), τ x ≤ 2) : ∫⁻ (x : ℕ → ℝ), valueAt (gaussNumeraire s) τ x ∂nullDist θ = (nullDist θ) {x : ℕ → ℝ | τ x ≤ 1} + ∫⁻ (x : ℕ → ℝ) in {x : ℕ → ℝ | τ x ≤ 1}ᶜ, ENNReal.ofReal (notepCond s θ x) ∂nullDist θ

The expectation at a stopping time τ ≤ 2: E_θ(E*_τ) = P_θ(τ ≤ 1) + E_θ{1(τ = 2)E_θ(E*_2 ∣ X₁)}, since {τ = 2} = {τ ≤ 1}ᶜ ∈ ℱ₁.

theorem LogOptimal.lintegral_valueAt_gaussNumeraire_le {s : ℝ} (hs : 0 < s) (θ : ℝ) {τ : (ℕ → ℝ) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration ℝ) τ) (hτ2 : ∀ (x : ℕ → ℝ), τ x ≤ 2) : ∫⁻ (x : ℕ → ℝ), valueAt (gaussNumeraire s) τ x ∂nullDist θ ≤ ∫⁻ (x : ℕ → ℝ), max 1 (ENNReal.ofReal (notepCond s θ x)) ∂nullDist θ

Every stopping time τ ≤ 2 satisfies E_θ(E*_τ) ≤ E_θ[max{1, E_θ(E*_2 ∣ X₁)}].

theorem LogOptimal.isStoppingTime_notep (s θ : ℝ) : MeasureTheory.IsStoppingTime (dataFiltration ℝ) fun (x : ℕ → ℝ) => if 1 < notepCond s θ x then 2 else 1

The stopping time τ = 1 + 1{E_θ(E*_2 ∣ X₁) > 1} of Proposition S2.

theorem LogOptimal.lintegral_valueAt_notep {s : ℝ} (hs : 0 < s) (θ : ℝ) : ∫⁻ (x : ℕ → ℝ), valueAt (gaussNumeraire s) (fun (x : ℕ → ℝ) => if 1 < notepCond s θ x then 2 else 1) x ∂nullDist θ = ∫⁻ (x : ℕ → ℝ), max 1 (ENNReal.ofReal (notepCond s θ x)) ∂nullDist θ

The stopping time τ = 1 + 1{E_θ(E*_2 ∣ X₁) > 1} attains E_θ[max{1, E_θ(E*_2 ∣ X₁)}].

The region where E_θ(E*_2 ∣ X₁) exceeds one

theorem LogOptimal.one_lt_notepCond_iff {s : ℝ} (hs : 0 < s) (hs1 : s ≠ 1) (θ : ℝ) (x : ℕ → ℝ) : 1 < notepCond s θ x ↔ if s < 1 then (x 0 - θ) ^ 2 < (1 + s ^ 2) / (1 - s ^ 2) * Real.log (2 / (1 + s ^ 2)) else (1 + s ^ 2) / (1 - s ^ 2) * Real.log (2 / (1 + s ^ 2)) < (x 0 - θ) ^ 2

E_θ(E*_2 ∣ X₁) > 1 exactly when (X₁ − θ)² < {(1 + s²)/(1 − s²)} log{2/(1 + s²)} if s < 1, and when the reverse strict inequality holds if s > 1.

theorem LogOptimal.nullDist_one_lt_notepCond_ne_zero {s : ℝ} (hs : 0 < s) (hs1 : s ≠ 1) (θ : ℝ) : (nullDist θ) {x : ℕ → ℝ | 1 < notepCond s θ x} ≠ 0

For s ≠ 1, the event {E_θ(E*_2 ∣ X₁) > 1} has positive probability under P_θ: it is the event that X₁ lies in a nonempty open set, and N(θ, 1) charges every such set.

theorem LogOptimal.one_lt_lintegral_max_notepCond {s : ℝ} (hs : 0 < s) (hs1 : s ≠ 1) (θ : ℝ) : 1 < ∫⁻ (x : ℕ → ℝ), max 1 (ENNReal.ofReal (notepCond s θ x)) ∂nullDist θ

Equation (S16), positivity: for s ≠ 1, E_θ[max{1, E_θ(E*_2 ∣ X₁)}] > 1, since each of the conditions of one_lt_notepCond_iff holds with positive probability under P_θ.

Proposition S2

theorem LogOptimal.prop_notep_proof (s θ : ℝ) : 0 < s → s ≠ 1 → (nullDist θ)[fun (x : ℕ → ℝ) => (gaussNumeraire s 2 x).toReal | ↑(dataFiltration ℝ) 1] =ᵐ[nullDist θ] notepCond s θ ∧ ⨆ (τ : (ℕ → ℝ) → ℕ∞), ⨆ (_ : MeasureTheory.IsStoppingTime (dataFiltration ℝ) τ ∧ ∀ (x : ℕ → ℝ), τ x ≤ 2), ∫⁻ (x : ℕ → ℝ), valueAt (gaussNumeraire s) τ x ∂nullDist θ = ∫⁻ (x : ℕ → ℝ), max 1 (ENNReal.ofReal (notepCond s θ x)) ∂nullDist θ ∧ 1 < ∫⁻ (x : ℕ → ℝ), max 1 (ENNReal.ofReal (notepCond s θ x)) ∂nullDist θ ∧ have τ := fun (x : ℕ → ℝ) => if 1 < notepCond s θ x then 2 else 1; (MeasureTheory.IsStoppingTime (dataFiltration ℝ) τ ∧ ∀ (x : ℕ → ℝ), τ x ≤ 2) ∧ ∫⁻ (x : ℕ → ℝ), valueAt (gaussNumeraire s) τ x ∂nullDist θ = ∫⁻ (x : ℕ → ℝ), max 1 (ENNReal.ofReal (notepCond s θ x)) ∂nullDist θ

The claims of Section S2.3

theorem LogOptimal.not_isEProcess_gaussNumeraire {s : ℝ} (hs : 0 < s) (hs1 : s ≠ 1) : ¬IsEProcess gaussNull (gaussNumeraire s)

Since the supremum in eq. (S16) exceeds one, the numéraires are not an e-process with respect to (ℱ_t) for s ≠ 1.

theorem LogOptimal.marginal_nullDist_two_ac_altDist (θ μ : ℝ) {s : ℝ} (hs : s ≠ 0) : (marginal (nullDist θ) 2).AbsolutelyContinuous (marginal (altDist s μ) 2)

The distribution of X² under P_θ is absolutely continuous with respect to its distribution under Q_μ, since N(θ, 1) and N(μ, s²) are both equivalent to the Lebesgue measure.

theorem LogOptimal.marginal_nullDist_two_ac_mixAlt (θ : ℝ) {s : ℝ} (hs : s ≠ 0) (ρ : ℝ) : (marginal (nullDist θ) 2).AbsolutelyContinuous (marginal (mixAlt s ρ) 2)

The null distributions of X² are absolutely continuous with respect to Q₂: a set that is Q₂-null is Q_{μ,2}-null for some μ, hence Lebesgue-null.

Positivity of the minimax regret

theorem LogOptimal.minimaxRegret_pos_of_converse {s ρ : ℝ} (hs : 0 < s) (hs1 : s ≠ 1) (hS : Setting gaussNull (mixAlt s ρ) (gaussNumeraire s)) (hconv : minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) 2 = 0 → (∀ P ∈ gaussNull, (marginal P 2).AbsolutelyContinuous (marginal (mixAlt s ρ) 2)) → ∃ (Es' : ℕ → (ℕ → ℝ) → ENNReal), (∀ t ≤ 2, Measurable (Es' t) ∧ Es' t =ᵐ[mixAlt s ρ] gaussNumeraire s t) ∧ IsEProcess gaussNull fun (t : ℕ) => Es' (min t 2)) (T : ℕ) : 2 ≤ T → 0 < minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T

Positivity of the minimax regret (Section S2.3): for s ≠ 1, Γ_T ≥ Γ₂ > 0 for every T ≥ 2, given the setting of Sections 1 and 2 for the Gaussian location model and the converse of Remark 1 (Proposition S1(i)) at T = 2. If Γ₂ = 0, Proposition S1(i) gives versions of E*_0, E*_1, E*_2 that form an e-process when stopped at 2. Since the null distributions of X² are absolutely continuous with respect to Q₂, these versions agree with the numéraires P_θ-almost surely, and the stopping time 1 + 1{E_θ(E*_2 ∣ X₁) > 1} contradicts eq. (S16). Proposition 1 then gives Γ_T ≥ Γ₂.