BanditRLProof.OFULGaussianSpectralMixture

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

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

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 (𝕜 := Real) A v⟫_ℝ = ∑ i, hA.isHermitian.eigenvalues i * x i ^ 2

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 (𝕜 := Real) A z⟫_ℝ / 2)) = (Finset.univ.prod (fun i => Real.sqrt (1 + hA.isHermitian.eigenvalues i)))⁻¹ * Real.exp (Finset.univ.sum (fun i => ⟪score, hA.isHermitian.eigenvectorBasis i⟫_ℝ ^ 2 / (2 * (1 + hA.isHermitian.eigenvalues i))))

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)

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 (𝕜 := Real) (1 + A)⁻¹ (hA.isHermitian.eigenvectorBasis i) = (1 + hA.isHermitian.eigenvalues i)⁻¹ • hA.isHermitian.eigenvectorBasis i

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))

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 (𝕜 := Real) A z⟫_ℝ / 2)) = (Real.sqrt (Matrix.det (1 + A)))⁻¹ * Real.exp (score ⬝ᵥ (1 + A)⁻¹.mulVec score / 2)