Lean module · OFUL

BanditRLProof.OFULGaussianMixtureMeasurability

# Joint measurability for the OFUL Gaussian mixture This file packages the random-score/random-Gram quadratic exponential on the product of a sample space and a finite-dimensional Gaussian parameter space. It proves the joint measurable surface needed by Tonelli and exposes both a generic product-measure identity and the `N(0, V0⁻¹)` specialization.

Module map

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

Imports

BanditRLProof.OFULGaussianCovarianceMixture

Imported by

BanditRLProof, BanditRLProof.OFULFiniteHorizonScoreGram

Declarations

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

def BanditRLProof.OFUL.gaussianQuadraticExponential Compiled

The quadratic exponential mixed over the Gaussian direction in OFUL.

noncomputable def gaussianQuadraticExponential (score : Omega -> EuclideanSpace Real Feature) (gram : Omega -> Matrix Feature Feature Real) (p : Omega × EuclideanSpace Real Feature) : Real

Source line 24 Chapter context: OFUL

theorem BanditRLProof.OFUL.measurable_gaussianQuadraticExponential_dot Compiled Internal helper

No declaration docstring is present; use the chapter context and exact statement below.

private theorem measurable_gaussianQuadraticExponential_dot (score : Omega -> EuclideanSpace Real Feature) (gram : Omega -> Matrix Feature Feature Real) (hscore : Measurable score) (hgram : forall i j, Measurable (fun omega => gram omega i j)) : Measurable (fun p : Omega × EuclideanSpace Real Feature => Real.exp ((WithLp.ofLp (score p.1)) ⬝ᵥ (WithLp.ofLp p.2) - (WithLp.ofLp p.2) ⬝ᵥ (gram p.1).mulVec (WithLp.ofLp p.2) / 2))

Source line 33 Chapter context: OFUL

theorem BanditRLProof.OFUL.measurable_gaussianQuadraticExponential Compiled

Joint measurability of the quadratic exponential from measurable random scores and coordinatewise measurable random Gram matrices.

theorem measurable_gaussianQuadraticExponential (score : Omega -> EuclideanSpace Real Feature) (gram : Omega -> Matrix Feature Feature Real) (hscore : Measurable score) (hgram : forall i j, Measurable (fun omega => gram omega i j)) : Measurable (gaussianQuadraticExponential score gram)

Source line 51 Chapter context: OFUL

def BanditRLProof.OFUL.gaussianQuadraticExponentialENNReal Compiled

The nonnegative extended-real surface used by Tonelli.

noncomputable def gaussianQuadraticExponentialENNReal (score : Omega -> EuclideanSpace Real Feature) (gram : Omega -> Matrix Feature Feature Real) (p : Omega × EuclideanSpace Real Feature) : ENNReal

Source line 68 Chapter context: OFUL

theorem BanditRLProof.OFUL.measurable_gaussianQuadraticExponentialENNReal Compiled

Joint measurability of the `ENNReal` Tonelli surface.

theorem measurable_gaussianQuadraticExponentialENNReal (score : Omega -> EuclideanSpace Real Feature) (gram : Omega -> Matrix Feature Feature Real) (hscore : Measurable score) (hgram : forall i j, Measurable (fun omega => gram omega i j)) : Measurable (gaussianQuadraticExponentialENNReal score gram)

Source line 75 Chapter context: OFUL

theorem BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_prod Compiled

Tonelli for the quadratic exponential under an arbitrary `SFinite` parameter law.

theorem lintegral_gaussianQuadraticExponentialENNReal_prod (mu : Measure Omega) (nu : Measure (EuclideanSpace Real Feature)) [SFinite nu] (score : Omega -> EuclideanSpace Real Feature) (gram : Omega -> Matrix Feature Feature Real) (hscore : Measurable score) (hgram : forall i j, Measurable (fun omega => gram omega i j)) : ∫⁻ p, gaussianQuadraticExponentialENNReal score gram p ∂mu.prod nu = ∫⁻ omega, ∫⁻ theta, gaussianQuadraticExponentialENNReal score gram (omega, theta) ∂nu ∂mu

Source line 84 Chapter context: OFUL

theorem BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_prod_multivariateGaussian_zero_inv Compiled

Tonelli specialized to the `N(0, V0⁻¹)` parameter law used by OFUL.

theorem lintegral_gaussianQuadraticExponentialENNReal_prod_multivariateGaussian_zero_inv (mu : Measure Omega) (V0 : Matrix Feature Feature Real) (score : Omega -> EuclideanSpace Real Feature) (gram : Omega -> Matrix Feature Feature Real) (hscore : Measurable score) (hgram : forall i j, Measurable (fun omega => gram omega i j)) : ∫⁻ p, gaussianQuadraticExponentialENNReal score gram p ∂mu.prod (ProbabilityTheory.multivariateGaussian 0 V0⁻¹) = ∫⁻ omega, ∫⁻ theta, gaussianQuadraticExponentialENNReal score gram (omega, theta) ∂ProbabilityTheory.multivariateGaussian 0 V0⁻¹ ∂mu

Source line 99 Chapter context: OFUL