Lean module · OFUL
BanditRLProof.OFULGaussianMixtureMeasurability
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
Imports
BanditRLProof.OFULGaussianCovarianceMixture
Imported by
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.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.gaussianQuadraticExponentialReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def gaussianQuadraticExponential (score : Omega -> EuclideanSpace Real Feature) (gram : Omega -> Matrix Feature Feature Real) (p : Omega × EuclideanSpace Real Feature) : Real
theorem
BanditRLProof.OFUL.measurable_gaussianQuadraticExponential_dot
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.measurable_gaussianQuadraticExponential_dotReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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))
theorem
BanditRLProof.OFUL.measurable_gaussianQuadraticExponential
Compiled
Joint measurability of the quadratic exponential from measurable random scores and coordinatewise measurable random Gram matrices.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.measurable_gaussianQuadraticExponentialReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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)
def
BanditRLProof.OFUL.gaussianQuadraticExponentialENNReal
Compiled
The nonnegative extended-real surface used by Tonelli.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.gaussianQuadraticExponentialENNRealReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def gaussianQuadraticExponentialENNReal (score : Omega -> EuclideanSpace Real Feature) (gram : Omega -> Matrix Feature Feature Real) (p : Omega × EuclideanSpace Real Feature) : ENNReal
theorem
BanditRLProof.OFUL.measurable_gaussianQuadraticExponentialENNReal
Compiled
Joint measurability of the `ENNReal` Tonelli surface.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.measurable_gaussianQuadraticExponentialENNRealReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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)
theorem
BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_prod
Compiled
Tonelli for the quadratic exponential under an arbitrary `SFinite` parameter law.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_prodReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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
theorem
BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_prod_multivariateGaussian_zero_inv
Compiled
Tonelli specialized to the `N(0, V0⁻¹)` parameter law used by OFUL.
Used in these reading views: Bandit Book
5. OFUL, self-normalized confidence, and stopping times
Canonical node identity
declaration:BanditRLProof.OFUL.lintegral_gaussianQuadraticExponentialENNReal_prod_multivariateGaussian_zero_invReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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