BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · OFUL

BanditRLProof.OFULGaussianCovarianceMixture

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

Declarations
9
Placeholders
0

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.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identitydeclaration:BanditRLProof.OFUL.inner_toEuclideanCLM_selfAdjoint

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

private theorem inner_toEuclideanCLM_selfAdjoint (C : Matrix Feature Feature Real) (hC : C.IsHermitian) (x y : EuclideanSpace Real Feature) : ⟪x, Matrix.toEuclideanCLM (𝕜 := Real) C y⟫_ℝ = ⟪Matrix.toEuclideanCLM (𝕜 := Real) C x, y⟫_ℝ
Source line 20 Chapter context: OFUL
theorem BanditRLProof.OFUL.inner_toEuclideanCLM_congruence 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 identitydeclaration:BanditRLProof.OFUL.inner_toEuclideanCLM_congruence

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

private theorem inner_toEuclideanCLM_congruence (C G : Matrix Feature Feature Real) (hC : C.IsHermitian) (z : EuclideanSpace Real Feature) : ⟪Matrix.toEuclideanCLM (𝕜 := Real) C z, Matrix.toEuclideanCLM (𝕜 := Real) G (Matrix.toEuclideanCLM (𝕜 := Real) C z)⟫_ℝ = ⟪z, Matrix.toEuclideanCLM (𝕜 := Real) (C * G * C) z⟫_ℝ
Source line 35 Chapter context: OFUL
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.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identitydeclaration:BanditRLProof.OFUL.integral_exp_inner_sub_quadratic_multivariateGaussian_zero_inv_transformed

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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 (𝕜 := Real) G z⟫_ℝ / 2)) = (Real.sqrt (Matrix.det (1 + C * G * C)))⁻¹ * Real.exp ((Matrix.toEuclideanCLM (𝕜 := Real) C score) ⬝ᵥ (1 + C * G * C)⁻¹.mulVec (Matrix.toEuclideanCLM (𝕜 := Real) C score) / 2)
Source line 57 Chapter context: OFUL
theorem BanditRLProof.OFUL.sqrt_inv_congruence_factorization 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 identitydeclaration:BanditRLProof.OFUL.sqrt_inv_congruence_factorization

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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
Source line 103 Chapter context: OFUL
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.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identitydeclaration:BanditRLProof.OFUL.det_one_add_sqrt_inv_congruence_eq_ratio

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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
Source line 130 Chapter context: OFUL
theorem BanditRLProof.OFUL.sqrt_inv_congruence_inverse Compiled

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 identitydeclaration:BanditRLProof.OFUL.sqrt_inv_congruence_inverse

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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)⁻¹
Source line 162 Chapter context: OFUL
theorem BanditRLProof.OFUL.dotProduct_sqrt_inv_congruence_inverse Compiled

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 identitydeclaration:BanditRLProof.OFUL.dotProduct_sqrt_inv_congruence_inverse

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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 (𝕜 := Real) C score) ⬝ᵥ (1 + C * G * C)⁻¹.mulVec (Matrix.toEuclideanCLM (𝕜 := Real) C score) = score ⬝ᵥ (V0 + G)⁻¹.mulVec score
Source line 187 Chapter context: OFUL
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.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identitydeclaration:BanditRLProof.OFUL.integral_exp_inner_sub_quadratic_multivariateGaussian_zero_inv_detRatio

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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 (𝕜 := Real) G z⟫_ℝ / 2)) = (Real.sqrt (Matrix.det (V0 + G) / Matrix.det V0))⁻¹ * Real.exp (score ⬝ᵥ (V0 + G)⁻¹.mulVec score / 2)
Source line 222 Chapter context: OFUL
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.

Used in these reading views: Bandit Book

5. OFUL, self-normalized confidence, and stopping times

Canonical node identitydeclaration:BanditRLProof.OFUL.integral_exp_inner_sub_quadratic_multivariateGaussian_zero_inv

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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 (𝕜 := Real) G z⟫_ℝ / 2)) = Real.sqrt (Matrix.det V0 / Matrix.det (V0 + G)) * Real.exp (score ⬝ᵥ (V0 + G)⁻¹.mulVec score / 2)
Source line 240 Chapter context: OFUL