Lean module · OFUL

BanditRLProof.OFULFiniteHorizonScoreGram

This module identifies the scalar compensated process from the fixed-direction conditional-MGF theorem with the random score/random-Gram quadratic exponential used by the Gaussian method of mixtures.

Module map

Source: BanditRLProof/OFULFiniteHorizonScoreGram.lean
Teaching chapter: 5. OFUL, self-normalized confidence, and stopping times
Declarations: 14
Placeholders: 0

Imports

BanditRLProof.OFULSelfNormalizedConfidence, BanditRLProof.OFULGaussianMixtureMeasurability

Imported by

BanditRLProof, BanditRLProof.OFULGaussianEvaluatedMixture

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.OFUL.finiteHorizonNoiseScore Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonNoiseScore

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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

Source line 20 Chapter context: OFUL

def BanditRLProof.OFUL.varianceWeightedFeature Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.varianceWeightedFeature

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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

Source line 29 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHorizonVarianceGram Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonVarianceGram

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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

Source line 36 Chapter context: OFUL

theorem BanditRLProof.OFUL.inner_finiteHorizonNoiseScore_eq_sum_projection_mul_noise Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.inner_finiteHorizonNoiseScore_eq_sum_projection_mul_noise

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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)

Source line 45 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHorizonVarianceGram_quadraticForm_eq_sum Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonVarianceGram_quadraticForm_eq_sum

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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)

Source line 71 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHorizonVarianceGram_posSemidef Compiled

The finite-horizon variance Gram is positive semidefinite.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonVarianceGram_posSemidef

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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

Source line 100 Chapter context: OFUL

theorem BanditRLProof.OFUL.measurable_finiteHorizonVarianceGram_apply Compiled

Coordinatewise measurability of the finite-horizon variance Gram.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.measurable_finiteHorizonVarianceGram_apply

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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)

Source line 119 Chapter context: OFUL

theorem BanditRLProof.OFUL.measurable_finiteHorizonNoiseScore Compiled

Measurability of the finite-horizon score from coordinatewise inputs.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.measurable_finiteHorizonNoiseScore

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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)

Source line 135 Chapter context: OFUL

theorem BanditRLProof.OFUL.compensatedScore_eq_inner_sub_varianceGram Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.compensatedScore_eq_inner_sub_varianceGram

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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 (𝕜 := Real) (finiteHorizonVarianceGram feature varianceProxy n omega) theta⟫_Real / 2

Source line 150 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHorizonScoreVarianceGram_hasMGFUpperBoundAt Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.finiteHorizonScoreVarianceGram_hasMGFUpperBoundAt

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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 (𝕜 := Real) (finiteHorizonVarianceGram feature varianceProxy n omega) theta⟫_Real / 2) 1 0 mu

Source line 180 Chapter context: OFUL

theorem BanditRLProof.OFUL.integral_exp_inner_finiteHorizonScore_sub_varianceGram_le_one Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.integral_exp_inner_finiteHorizonScore_sub_varianceGram_le_one

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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 (𝕜 := Real) (finiteHorizonVarianceGram feature varianceProxy n omega) theta⟫_Real / 2) ∂mu <= 1

Source line 257 Chapter context: OFUL

theorem BanditRLProof.OFUL.integral_gaussianQuadraticExponential_finiteHorizon_le_one Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.integral_gaussianQuadraticExponential_finiteHorizon_le_one

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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

Source line 299 Chapter context: OFUL

theorem BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_finiteHorizon_prod_le_one Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_finiteHorizon_prod_le_one

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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

Source line 338 Chapter context: OFUL

theorem BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_finiteHorizon_prod_multivariateGaussian_zero_inv_le_one Compiled

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

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identity

declaration:BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_finiteHorizon_prod_multivariateGaussian_zero_inv_le_one

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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

Source line 456 Chapter context: OFUL