Lean module · OFUL
BanditRLProof.OFULGaussianMixture
# Gaussian mixture identities for OFUL This module develops the exact Gaussian quadratic-exponential integrals used after the fixed-direction exponential-supermartingale bound. The scalar identity is the normalization step needed before the finite-dimensional spectral/product assembly.
Module map
Imports
BanditRLProof.OFULSelfNormalizedConfidence
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.OFUL.integral_exp_linear_sub_quadratic_gaussianReal_zero_one
Compiled
The exact scalar quadratic-exponential integral under a standard Gaussian. This is the one-coordinate completed-square identity used by the Gaussian method of mixtures. The nonnegative quadratic coefficient is the scalar eigenvalue contract that will arise from a positive-semidefinite Gram matrix.
theorem integral_exp_linear_sub_quadratic_gaussianReal_zero_one (s q : Real) (hq : 0 <= q) : integral (ProbabilityTheory.gaussianReal 0 1) (fun x : Real => Real.exp (s * x - q * x ^ 2 / 2)) = (Real.sqrt (1 + q))⁻¹ * Real.exp (s ^ 2 / (2 * (1 + q)))
theorem
BanditRLProof.OFUL.integral_exp_sum_linear_sub_diagonal_quadratic_pi_gaussianReal
Compiled
Finite independent-coordinate version of the scalar completed-square identity. The right-hand side is deliberately left as a finite product. The following matrix-facing lemmas identify that product with the square-root determinant factor and the exponential term with an inverse-diagonal quadratic form.
theorem integral_exp_sum_linear_sub_diagonal_quadratic_pi_gaussianReal {Feature : Type*} [Fintype Feature] (score quadratic : Feature -> Real) (hquadratic : forall i, 0 <= quadratic i) : integral (Measure.pi (fun _ : Feature => ProbabilityTheory.gaussianReal 0 1)) (fun z : Feature -> Real => Real.exp (Finset.univ.sum (fun i => score i * z i - quadratic i * (z i) ^ 2 / 2))) = Finset.univ.prod (fun i => (Real.sqrt (1 + quadratic i))⁻¹ * Real.exp (score i ^ 2 / (2 * (1 + quadratic i))))
theorem
BanditRLProof.OFUL.integral_exp_sum_linear_sub_diagonal_quadratic_pi_gaussianReal_eq
Compiled
Finite product identity with the normalization and exponential factors collected separately.
theorem integral_exp_sum_linear_sub_diagonal_quadratic_pi_gaussianReal_eq {Feature : Type*} [Fintype Feature] (score quadratic : Feature -> Real) (hquadratic : forall i, 0 <= quadratic i) : integral (Measure.pi (fun _ : Feature => ProbabilityTheory.gaussianReal 0 1)) (fun z : Feature -> Real => Real.exp (Finset.univ.sum (fun i => score i * z i - quadratic i * (z i) ^ 2 / 2))) = (Finset.univ.prod (fun i => Real.sqrt (1 + quadratic i)))⁻¹ * Real.exp (Finset.univ.sum (fun i => score i ^ 2 / (2 * (1 + quadratic i))))
theorem
BanditRLProof.OFUL.integral_exp_sum_linear_sub_diagonal_quadratic_pi_gaussianReal_det
Compiled
Diagonal matrix form of the finite Gaussian quadratic-exponential identity. This is the diagonal-coordinate determinant-ratio and inverse-quadratic expression intended for later transport through a PSD matrix eigenbasis.
theorem integral_exp_sum_linear_sub_diagonal_quadratic_pi_gaussianReal_det {Feature : Type*} [Fintype Feature] [DecidableEq Feature] (score quadratic : Feature -> Real) (hquadratic : forall i, 0 <= quadratic i) : integral (Measure.pi (fun _ : Feature => ProbabilityTheory.gaussianReal 0 1)) (fun z : Feature -> Real => Real.exp (Finset.univ.sum (fun i => score i * z i - quadratic i * (z i) ^ 2 / 2))) = (Real.sqrt (Matrix.det (Matrix.diagonal (fun i : Feature => 1 + quadratic i))))⁻¹ * Real.exp (score ⬝ᵥ ((Matrix.diagonal (fun i : Feature => 1 + quadratic i))⁻¹).mulVec score / 2)