BanditRLProof.OFULFiniteHorizonScoreGram

The finite-horizon martingale score `sum_{i<n} x_i eta_i`.

noncomputable def finiteHorizonNoiseScore [Fintype Feature] (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (n : Nat) (omega : Omega) : EuclideanSpace Real Feature

Feature rescaling whose ordinary Gram is weighted by the variance proxy.

noncomputable def varianceWeightedFeature (feature : Nat -> Omega -> Feature -> Real) (varianceProxy : Nat -> NNReal) (i : Nat) (omega : Omega) (j : Feature) : Real

The finite-horizon variance-weighted Gram `sum_{i<n} c_i x_i x_i^T`.

noncomputable def finiteHorizonVarianceGram [Fintype Feature] (feature : Nat -> Omega -> Feature -> Real) (varianceProxy : Nat -> NNReal) (n : Nat) (omega : Omega) : Matrix Feature Feature Real

The score inner product is the finite sum of projected noise increments.

theorem inner_finiteHorizonNoiseScore_eq_sum_projection_mul_noise [Fintype Feature] (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (n : Nat) (omega : Omega) (theta : EuclideanSpace Real Feature) : ⟪finiteHorizonNoiseScore feature noise n omega, theta⟫_Real = (Finset.range n).sum (fun i => dotProduct (WithLp.ofLp theta) (feature i omega) * noise i omega)

The weighted Gram quadratic form is the variance-weighted projection sum.

theorem finiteHorizonVarianceGram_quadraticForm_eq_sum [Fintype Feature] (feature : Nat -> Omega -> Feature -> Real) (varianceProxy : Nat -> NNReal) (n : Nat) (omega : Omega) (theta : Feature -> Real) : quadraticForm (finiteHorizonVarianceGram feature varianceProxy n omega) theta = (Finset.range n).sum (fun i => (((varianceProxy i : NNReal) : Real)) * (dotProduct theta (feature i omega)) ^ 2)

The finite-horizon variance Gram is positive semidefinite.

theorem finiteHorizonVarianceGram_posSemidef [Fintype Feature] (feature : Nat -> Omega -> Feature -> Real) (varianceProxy : Nat -> NNReal) (n : Nat) (omega : Omega) : (finiteHorizonVarianceGram feature varianceProxy n omega).PosSemidef

Coordinatewise measurability of the finite-horizon variance Gram.

theorem measurable_finiteHorizonVarianceGram_apply [MeasurableSpace Omega] [Fintype Feature] (feature : Nat -> Omega -> Feature -> Real) (varianceProxy : Nat -> NNReal) (n : Nat) (hfeature : forall i j, Measurable (fun omega => feature i omega j)) : forall j k, Measurable (fun omega => finiteHorizonVarianceGram feature varianceProxy n omega j k)

Measurability of the finite-horizon score from coordinatewise inputs.

theorem measurable_finiteHorizonNoiseScore [MeasurableSpace Omega] [Fintype Feature] (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (n : Nat) (hfeature : forall i j, Measurable (fun omega => feature i omega j)) (hnoise : forall i, Measurable (noise i)) : Measurable (finiteHorizonNoiseScore feature noise n)

Pointwise identification of the fixed-direction compensated finite sum with the random score/random-Gram quadratic exponent.

theorem compensatedScore_eq_inner_sub_varianceGram [Fintype Feature] [DecidableEq Feature] (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (n : Nat) (omega : Omega) (theta : EuclideanSpace Real Feature) : (Finset.range (n + 1)).sum (fun t => match t with | 0 => 0 | i + 1 => dotProduct (WithLp.ofLp theta) (feature i omega) * noise i omega - (((varianceProxy i : NNReal) : Real) * (dotProduct (WithLp.ofLp theta) (feature i omega)) ^ 2 / 2)) = ⟪finiteHorizonNoiseScore feature noise n omega, theta⟫_Real - ⟪theta, Matrix.toEuclideanCLM (𝕜

The fixed-direction conditional-MGF endpoint transported to the random finite-horizon score and variance Gram.

theorem finiteHorizonScoreVarianceGram_hasMGFUpperBoundAt [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (theta : EuclideanSpace Real Feature) (projectionBound : Nat -> Real) (hprojection : forall i, StronglyMeasurable[F i] (fun omega => dotProduct (WithLp.ofLp theta) (feature i omega))) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall i, 0 <= projectionBound i) (hprojectionBound : forall i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (varianceProxy i) mu) : Concentration.HasMGFUpperBoundAt (fun omega => ⟪finiteHorizonNoiseScore feature noise n omega, theta⟫_Real - ⟪theta, Matrix.toEuclideanCLM (𝕜

Explicit unit expectation bound for the score/Gram quadratic exponential.

theorem integral_exp_inner_finiteHorizonScore_sub_varianceGram_le_one [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (theta : EuclideanSpace Real Feature) (projectionBound : Nat -> Real) (hprojection : forall i, StronglyMeasurable[F i] (fun omega => dotProduct (WithLp.ofLp theta) (feature i omega))) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall i, 0 <= projectionBound i) (hprojectionBound : forall i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (varianceProxy i) mu) : ∫ omega, Real.exp (⟪finiteHorizonNoiseScore feature noise n omega, theta⟫_Real - ⟪theta, Matrix.toEuclideanCLM (𝕜

The fixed-direction expectation bound on the exact Gaussian-mixture consumer surface.

theorem integral_gaussianQuadraticExponential_finiteHorizon_le_one [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (theta : EuclideanSpace Real Feature) (projectionBound : Nat -> Real) (hprojection : forall i, StronglyMeasurable[F i] (fun omega => dotProduct (WithLp.ofLp theta) (feature i omega))) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall i, 0 <= projectionBound i) (hprojectionBound : forall i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (varianceProxy i) mu) : ∫ omega, gaussianQuadraticExponential (finiteHorizonNoiseScore feature noise n) (finiteHorizonVarianceGram feature varianceProxy n) (omega, theta) ∂mu <= 1

Tonelli transport of all fixed-direction bounds through an arbitrary probability law on Gaussian directions.

theorem lintegral_gaussianQuadraticExponentialENNReal_finiteHorizon_prod_le_one [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (nu : Measure (EuclideanSpace Real Feature)) [IsProbabilityMeasure nu] (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (projectionBound : EuclideanSpace Real Feature -> Nat -> Real) (hfeature : forall i j, StronglyMeasurable[F i] (fun omega => feature i omega j)) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall theta i, 0 <= projectionBound theta i) (hprojectionBound : forall theta i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound theta i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (varianceProxy i) mu) : ∫⁻ p, gaussianQuadraticExponentialENNReal (finiteHorizonNoiseScore feature noise n) (finiteHorizonVarianceGram feature varianceProxy n) p ∂mu.prod nu <= 1

Gaussian-direction specialization of the finite-horizon Tonelli bound.

theorem lintegral_gaussianQuadraticExponentialENNReal_finiteHorizon_prod_multivariateGaussian_zero_inv_le_one [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (V0 : Matrix Feature Feature Real) (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (projectionBound : EuclideanSpace Real Feature -> Nat -> Real) (hfeature : forall i j, StronglyMeasurable[F i] (fun omega => feature i omega j)) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall theta i, 0 <= projectionBound theta i) (hprojectionBound : forall theta i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound theta i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (varianceProxy i) mu) : ∫⁻ p, gaussianQuadraticExponentialENNReal (finiteHorizonNoiseScore feature noise n) (finiteHorizonVarianceGram feature varianceProxy n) p ∂mu.prod (ProbabilityTheory.multivariateGaussian 0 V0⁻¹) <= 1