The conditional distribution of Y₂ given X₁

This file proves the claim of Section 4.1 of the paper that, under P_θ and given X₁, the variable Y₂ = (X₂ − X₁)/2^{1/2} is normal with mean (θ − X₁)/2^{1/2} and variance 1/2 (sec4_conditional_Y2_proof).

• helmertY_two: Y₂ = (X₂ − X₁)/2^{1/2}.
• map_pair_nullDist: under P_θ, (X₁, X₂) has distribution N(θ, 1) ⊗ N(θ, 1).
• condY2Kernel θ: the kernel a ↦ N(θ, 1) pushed forward by b ↦ (b − a)/2^{1/2}, which is N{(θ − a)/2^{1/2}, 1/2} (condY2Kernel_apply).
• map_x0_helmertY2: the joint distribution of (X₁, Y₂) is N(θ, 1) ⊗ₘ condY2Kernel θ.

theorem LogOptimal.helmertY_two (x : ℕ → ℝ) : helmertY 2 x = (x 1 - x 0) / √2

theorem LogOptimal.map_pair_nullDist (θ : ℝ) : MeasureTheory.Measure.map (fun (x : ℕ → ℝ) => (x 0, x 1)) (nullDist θ) = (ProbabilityTheory.gaussianReal θ 1).prod (ProbabilityTheory.gaussianReal θ 1)

noncomputable def LogOptimal.condY2Kernel (θ : ℝ) : ProbabilityTheory.Kernel ℝ ℝ

The kernel a ↦ N(θ, 1) pushed forward by b ↦ (b − a)/2^{1/2}: the conditional distribution of Y₂ given X₁ = a under P_θ.

Equations

• LogOptimal.condY2Kernel θ = (ProbabilityTheory.Kernel.id.prod (ProbabilityTheory.Kernel.const ℝ (ProbabilityTheory.gaussianReal θ 1))).map fun (p : ℝ × ℝ) => (p.2 - p.1) / √2

instance LogOptimal.instIsMarkovKernelRealCondY2Kernel (θ : ℝ) : ProbabilityTheory.IsMarkovKernel (condY2Kernel θ)

theorem LogOptimal.condY2Kernel_apply' (θ a : ℝ) : (condY2Kernel θ) a = MeasureTheory.Measure.map (fun (b : ℝ) => (b - a) / √2) (ProbabilityTheory.gaussianReal θ 1)

theorem LogOptimal.condY2Kernel_apply (θ a : ℝ) : (condY2Kernel θ) a = ProbabilityTheory.gaussianReal ((θ - a) / √2) (1 / 2)

theorem LogOptimal.map_x0_helmertY2 (θ : ℝ) : MeasureTheory.Measure.map (fun (x : ℕ → ℝ) => (x 0, helmertY 2 x)) (nullDist θ) = (ProbabilityTheory.gaussianReal θ 1).compProd (condY2Kernel θ)

Under P_θ, the joint distribution of (X₁, Y₂) is N(θ, 1) ⊗ₘ condY2Kernel θ.

theorem LogOptimal.sec4_conditional_Y2_proof (θ : ℝ) : (∀ (x : ℕ → ℝ), helmertY 2 x = (x 1 - x 0) / √2) ∧ ∀ᵐ (x₁ : ℝ) ∂MeasureTheory.Measure.map (fun (x : ℕ → ℝ) => x 0) (nullDist θ), (ProbabilityTheory.condDistrib (helmertY 2) (fun (x : ℕ → ℝ) => x 0) (nullDist θ)) x₁ = ProbabilityTheory.gaussianReal ((θ - x₁) / √2) (1 / 2)