Lean module · OFUL
BanditRLProof.OFULGaussianCovarianceMixture
# Positive-definite covariance Gaussian mixture for OFUL This file transports the standard-Gaussian quadratic-exponential identity through the square root of `V0⁻¹`. For a positive-definite prior precision `V0` and a positive-semidefinite Gram matrix `G`, it collects the transformed determinant and quadratic form into the OFUL-facing matrices `V0 + G` and `(V0 + G)⁻¹`.
Module map
Imports
BanditRLProof.OFULGaussianSpectralMixture
Imported by
BanditRLProof, BanditRLProof.OFULGaussianMixtureMeasurability
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.OFUL.inner_toEuclideanCLM_selfAdjoint
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem inner_toEuclideanCLM_selfAdjoint (C : Matrix Feature Feature Real) (hC : C.IsHermitian) (x y : EuclideanSpace Real Feature) : ⟪x, Matrix.toEuclideanCLM (𝕜
theorem
BanditRLProof.OFUL.inner_toEuclideanCLM_congruence
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem inner_toEuclideanCLM_congruence (C G : Matrix Feature Feature Real) (hC : C.IsHermitian) (z : EuclideanSpace Real Feature) : ⟪Matrix.toEuclideanCLM (𝕜
theorem
BanditRLProof.OFUL.integral_exp_inner_sub_quadratic_multivariateGaussian_zero_inv_transformed
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem integral_exp_inner_sub_quadratic_multivariateGaussian_zero_inv_transformed (V0 G : Matrix Feature Feature Real) (hG : G.PosSemidef) (score : EuclideanSpace Real Feature) : let C := CFC.sqrt V0⁻¹ integral (ProbabilityTheory.multivariateGaussian 0 V0⁻¹) (fun z : EuclideanSpace Real Feature => Real.exp (⟪score, z⟫_ℝ - ⟪z, Matrix.toEuclideanCLM (𝕜
theorem
BanditRLProof.OFUL.sqrt_inv_congruence_factorization
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem sqrt_inv_congruence_factorization (V0 G : Matrix Feature Feature Real) (hV0 : V0.PosDef) : let D := CFC.sqrt V0 let C := CFC.sqrt V0⁻¹ D * (1 + C * G * C) * D = V0 + G
theorem
BanditRLProof.OFUL.det_one_add_sqrt_inv_congruence_eq_ratio
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem det_one_add_sqrt_inv_congruence_eq_ratio (V0 G : Matrix Feature Feature Real) (hV0 : V0.PosDef) : let C := CFC.sqrt V0⁻¹ Matrix.det (1 + C * G * C) = Matrix.det (V0 + G) / Matrix.det V0
theorem
BanditRLProof.OFUL.sqrt_inv_congruence_inverse
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sqrt_inv_congruence_inverse (V0 G : Matrix Feature Feature Real) (hV0 : V0.PosDef) : let C := CFC.sqrt V0⁻¹ C * (1 + C * G * C)⁻¹ * C = (V0 + G)⁻¹
theorem
BanditRLProof.OFUL.dotProduct_sqrt_inv_congruence_inverse
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem dotProduct_sqrt_inv_congruence_inverse (V0 G : Matrix Feature Feature Real) (hV0 : V0.PosDef) (score : EuclideanSpace Real Feature) : let C := CFC.sqrt V0⁻¹ (Matrix.toEuclideanCLM (𝕜
theorem
BanditRLProof.OFUL.integral_exp_inner_sub_quadratic_multivariateGaussian_zero_inv_detRatio
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem integral_exp_inner_sub_quadratic_multivariateGaussian_zero_inv_detRatio (V0 G : Matrix Feature Feature Real) (hV0 : V0.PosDef) (hG : G.PosSemidef) (score : EuclideanSpace Real Feature) : integral (ProbabilityTheory.multivariateGaussian 0 V0⁻¹) (fun z : EuclideanSpace Real Feature => Real.exp (⟪score, z⟫_ℝ - ⟪z, Matrix.toEuclideanCLM (𝕜
theorem
BanditRLProof.OFUL.integral_exp_inner_sub_quadratic_multivariateGaussian_zero_inv
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem integral_exp_inner_sub_quadratic_multivariateGaussian_zero_inv (V0 G : Matrix Feature Feature Real) (hV0 : V0.PosDef) (hG : G.PosSemidef) (score : EuclideanSpace Real Feature) : integral (ProbabilityTheory.multivariateGaussian 0 V0⁻¹) (fun z : EuclideanSpace Real Feature => Real.exp (⟪score, z⟫_ℝ - ⟪z, Matrix.toEuclideanCLM (𝕜