Sharp Berry-Esseen Bounds for the Log Determinant of a Gaussian Sample Correlation Matrix

Hongru Zhao

math.PR Aug 12, 2026 · v1 math.ST

Read PDF arXiv abstract Code

TL;DR

All theoretical results have exact or proved-equivalent Lean 4 formulations whose declarations and dependencies are kernel-checked.

Abstract

Let $\widehat R$ be the Pearson sample correlation matrix formed from $n$ independent Gaussian observations in $p$ dimensions, and write $m=n-1\ge p$. Under the null correlation $R=I_p$, the classical independent beta product, exact cumulants, and full Fourier inversion yield, along every sequence $p\to\infty$ with $m\ge p$, a uniform first Edgeworth expansion for $\log\det\widehat R$, centered by its exact mean and scaled by its exact standard deviation. The expansion identifies the exact finite dimensional skewness correction and gives the sharp Kolmogorov equivalent $A_{m,p}/\{6\sqrt{2π}V_{m,p}^{3/2}\}$, where $V_{m,p}$ is the exact variance and $A_{m,p}$ is the absolute third cumulant. This equivalent unifies the square, fixed gap, growing gap, proportional, and dilute regimes; in the square regime the error has order $(\log p)^{-3/2}$ with an exact constant. For every positive definite population correlation matrix $R$, we prove a uniform finite sample Berry-Esseen bound that explicitly tracks population dependence. All theoretical results have exact or proved equivalent Lean 4 formulations whose declarations and dependencies are kernel checked.

Problem

For the Pearson sample correlation matrix from n Gaussian observations in p dimensions, one wants sharp normal-approximation error rates for its log determinant. Existing central limit theorems give only qualitative limits or non-sharp constants, and no single normalization covers all dimension/sample-size regimes.

Approach

Under the null R=I_p, an exact independent beta product representation reduces log det to a sum, yielding exact cumulants and a full Fourier-inversion Edgeworth expansion with a sharp Kolmogorov equivalent. For arbitrary positive definite R, a Wiener chaos decomposition separates a Wishart leading term from a nonlinear diagonal standardization remainder to obtain a finite-sample Berry-Esseen bound. All theoretical results are given exact or proved-equivalent Lean 4 formulations that are kernel-checked.

Results

A uniform first Edgeworth expansion and sharp Kolmogorov equivalent are established across square, fixed-gap, growing-gap, proportional, and dilute regimes; the square regime has error of order (log p)^{-3/2} with an exact constant. A uniform finite-sample Berry-Esseen bound tracking population dependence is proved for every positive definite R.

Constraint	Assumptions	Sharp Kolmogorov equivalent
m=p	square hard edge	C_*(log p)^{-3/2}
m-p=d_0	fixed integer d_0>=0	A_{d_0}/{24√π(log p)^{3/2}}
p/m→γ	γ∈(0,1)	C_0(γ)/p
p/m→0	p→∞	2/{3√(2π)p}

Sharp null Kolmogorov equivalents under representative constraints

Papers With

Sharp Berry-Esseen Bounds for the Log Determinant of a Gaussian Sample Correlation Matrix