Lean module · OFUL

BanditRLProof.OFULGaussianSpectralMixture

# Spectral Gaussian mixture identity for OFUL This module transports the compiled independent-coordinate Gaussian quadratic-exponential identity through the orthonormal eigenbasis of a real positive-semidefinite matrix. It then collects the spectral product and coordinate quadratic form as `det (1 + A)` and `(1 + A)⁻¹`.

Module map

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

Imports

BanditRLProof.OFULGaussianMixture

Imported by

BanditRLProof, BanditRLProof.OFULGaussianCovarianceMixture

Declarations

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

theorem BanditRLProof.OFUL.inner_sum_smul_orthonormalBasis Compiled Internal helper

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

private theorem inner_sum_smul_orthonormalBasis (b : OrthonormalBasis Feature Real (EuclideanSpace Real Feature)) (x : Feature -> Real) (i : Feature) : ⟪b i, ∑ j, x j • b j⟫_ℝ = x i

Source line 20 Chapter context: OFUL

theorem BanditRLProof.OFUL.inner_sum_smul_orthonormalBasis_left Compiled Internal helper

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

private theorem inner_sum_smul_orthonormalBasis_left (b : OrthonormalBasis Feature Real (EuclideanSpace Real Feature)) (score : EuclideanSpace Real Feature) (x : Feature -> Real) : ⟪score, ∑ i, x i • b i⟫_ℝ = ∑ i, ⟪score, b i⟫_ℝ * x i

Source line 28 Chapter context: OFUL

theorem BanditRLProof.OFUL.inner_toEuclideanCLM_sum_eigenvectorBasis Compiled Internal helper

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

private theorem inner_toEuclideanCLM_sum_eigenvectorBasis (A : Matrix Feature Feature Real) (hA : A.PosSemidef) (x : Feature -> Real) : let b := hA.isHermitian.eigenvectorBasis let v : EuclideanSpace Real Feature := ∑ i, x i • b i ⟪v, Matrix.toEuclideanCLM (𝕜

Source line 39 Chapter context: OFUL

theorem BanditRLProof.OFUL.integral_exp_inner_sub_quadratic_stdGaussian_eigenvalues Compiled

The standard-Gaussian quadratic-exponential integral in the orthonormal eigenbasis of a positive-semidefinite matrix. This is the explicit spectral-coordinate transport bridge from the diagonal product identity. The following lemmas collect its right-hand side into matrix determinant and inverse-quadratic notation.

theorem integral_exp_inner_sub_quadratic_stdGaussian_eigenvalues (A : Matrix Feature Feature Real) (hA : A.PosSemidef) (score : EuclideanSpace Real Feature) : integral (ProbabilityTheory.stdGaussian (EuclideanSpace Real Feature)) (fun z : EuclideanSpace Real Feature => Real.exp (⟪score, z⟫_ℝ - ⟪z, Matrix.toEuclideanCLM (𝕜

Source line 108 Chapter context: OFUL

theorem BanditRLProof.OFUL.det_one_add_posSemidef_eq_prod_eigenvalues Compiled

The determinant of `1 + A` is the product of one plus the eigenvalues of a real positive-semidefinite matrix.

theorem det_one_add_posSemidef_eq_prod_eigenvalues (A : Matrix Feature Feature Real) (hA : A.PosSemidef) : Matrix.det (1 + A) = Finset.univ.prod (fun i => 1 + hA.isHermitian.eigenvalues i)

Source line 175 Chapter context: OFUL

theorem BanditRLProof.OFUL.toEuclideanCLM_one_add_posSemidef_inv_eigenvectorBasis Compiled Internal helper

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

private theorem toEuclideanCLM_one_add_posSemidef_inv_eigenvectorBasis (A : Matrix Feature Feature Real) (hA : A.PosSemidef) (i : Feature) : Matrix.toEuclideanCLM (𝕜

Source line 233 Chapter context: OFUL

theorem BanditRLProof.OFUL.dotProduct_one_add_posSemidef_inv_mulVec_eq_sum_eigenvalues Compiled

The inverse quadratic form of `1 + A` equals its spectral-coordinate sum.

theorem dotProduct_one_add_posSemidef_inv_mulVec_eq_sum_eigenvalues (A : Matrix Feature Feature Real) (hA : A.PosSemidef) (score : EuclideanSpace Real Feature) : score ⬝ᵥ (1 + A)⁻¹.mulVec score = Finset.univ.sum (fun i => ⟪score, hA.isHermitian.eigenvectorBasis i⟫_ℝ ^ 2 / (1 + hA.isHermitian.eigenvalues i))

Source line 285 Chapter context: OFUL

theorem BanditRLProof.OFUL.integral_exp_inner_sub_quadratic_stdGaussian_det Compiled

Exact standard-Gaussian quadratic-exponential identity for an arbitrary real positive-semidefinite matrix. This closes the orthonormal spectral transport from the diagonal-coordinate Gaussian mixture leaf. Transport from a nonstandard initial covariance and the stochastic Tonelli/Markov assembly remain separate obligations.

theorem integral_exp_inner_sub_quadratic_stdGaussian_det (A : Matrix Feature Feature Real) (hA : A.PosSemidef) (score : EuclideanSpace Real Feature) : integral (ProbabilityTheory.stdGaussian (EuclideanSpace Real Feature)) (fun z : EuclideanSpace Real Feature => Real.exp (⟪score, z⟫_ℝ - ⟪z, Matrix.toEuclideanCLM (𝕜

Source line 351 Chapter context: OFUL