Lean module · OFUL

BanditRLProof.OFULGaussianEvaluatedMixture

# Evaluated Gaussian mixtures for finite-horizon OFUL scores This module evaluates the inner Gaussian direction integral in the finite-horizon score/variance-Gram mixture and transports the product-space bound to the determinant-ratio inverse-Gram exponential.

Module map

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

Imports

BanditRLProof.OFULFiniteHorizonScoreGram

Imported by

BanditRLProof, BanditRLProof.OFULSelfNormalizedMarkov

Declarations

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

theorem BanditRLProof.OFUL.integrable_exp_inner_sub_quadratic_multivariateGaussian_zero_inv Compiled

The positive-semidefinite Gaussian quadratic exponential is integrable. Fernique supplies a square-exponential envelope for the linear term.

theorem integrable_exp_inner_sub_quadratic_multivariateGaussian_zero_inv [Fintype Feature] [DecidableEq Feature] (V0 G : Matrix Feature Feature Real) (hG : G.PosSemidef) (score : EuclideanSpace Real Feature) : Integrable (fun z : EuclideanSpace Real Feature => Real.exp (⟪score, z⟫_ℝ - ⟪z, Matrix.toEuclideanCLM (𝕜

Source line 23 Chapter context: OFUL

theorem BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_multivariateGaussian_zero_inv Compiled

The `ENNReal` Gaussian direction integral equals the completed-square determinant-ratio expression.

theorem lintegral_gaussianQuadraticExponentialENNReal_multivariateGaussian_zero_inv [Fintype Feature] [DecidableEq Feature] (V0 G : Matrix Feature Feature Real) (hV0 : V0.PosDef) (hG : G.PosSemidef) (score : EuclideanSpace Real Feature) : ∫⁻ z : EuclideanSpace Real Feature, ENNReal.ofReal (Real.exp (⟪score, z⟫_ℝ - ⟪z, Matrix.toEuclideanCLM (𝕜

Source line 103 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHorizonDetRatioInvGramExponential Compiled

The evaluated determinant-ratio inverse-Gram exponential for a finite-horizon score and variance Gram.

noncomputable def finiteHorizonDetRatioInvGramExponential [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (n : Nat) (omega : Omega) : ENNReal

Source line 128 Chapter context: OFUL

theorem BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_finiteHorizon_multivariateGaussian_zero_inv Compiled

Samplewise evaluation of the finite-horizon Gaussian direction integral.

theorem lintegral_gaussianQuadraticExponentialENNReal_finiteHorizon_multivariateGaussian_zero_inv [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (n : Nat) (omega : Omega) : ∫⁻ theta : EuclideanSpace Real Feature, gaussianQuadraticExponentialENNReal (finiteHorizonNoiseScore feature noise n) (finiteHorizonVarianceGram feature varianceProxy n) (omega, theta) ∂ProbabilityTheory.multivariateGaussian 0 V0⁻¹ = finiteHorizonDetRatioInvGramExponential V0 feature noise varianceProxy n omega

Source line 151 Chapter context: OFUL

theorem BanditRLProof.OFUL.measurable_finiteHorizonDetRatioInvGramExponential Compiled

The evaluated finite-horizon mixture is measurable in the sample.

theorem measurable_finiteHorizonDetRatioInvGramExponential [MeasurableSpace Omega] [Fintype Feature] [DecidableEq Feature] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (n : Nat) (hfeature : forall i j, Measurable (fun omega => feature i omega j)) (hnoise : forall i, Measurable (noise i)) : Measurable (finiteHorizonDetRatioInvGramExponential V0 feature noise varianceProxy n)

Source line 180 Chapter context: OFUL

theorem BanditRLProof.OFUL.lintegral_finiteHorizon_detRatio_invGramExponential_le_one Compiled

The evaluated finite-horizon Gaussian mixture has `ENNReal` expectation at most one.

theorem lintegral_finiteHorizon_detRatio_invGramExponential_le_one [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (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) : ∫⁻ omega, finiteHorizonDetRatioInvGramExponential V0 feature noise varianceProxy n omega ∂mu <= 1

Source line 230 Chapter context: OFUL