高斯样本相关矩阵对数行列式的精确Berry-Esseen界
Sharp Berry-Esseen Bounds for the Log Determinant of a Gaussian Sample Correlation Matrix
浏览论文内容
中文总结 AI 辅助
该研究针对高斯样本相关矩阵对数行列式，推导了零相关下的埃奇沃思展开式与统一的Kolmogorov等价式，还证明了正定总体相关矩阵下的有限样本Berry-Esseen界，且相关结果有Lean 4等价公式并经内核验证。
中文摘要 AI 辅助
设$\boldsymbol{\tilde{R}}$为从$p$维$n$个独立高斯观测值构成的Pearson样本相关矩阵，记$m=n-1\boldsymbol{\tilde{R}}I_p$。在零相关条件$R=I_p$下，经典独立贝塔乘积、精确累积量及全傅里叶逆变换，结合每一条满足$m\boldsymbol{\tilde{R}}p$的序列$p\to\boldsymbol{\tilde{R}}$，给出了以其精确均值为中心、以精确标准差为尺度的$\boldsymbol{\tilde{R}}\boldsymbol{\tilde{R}}\boldsymbol{\tilde{R}}$的一致一阶埃奇沃思展开式。该展开式确定了精确的有限维偏度校正，并给出了精确的Kolmogorov等价式$A_{m,p}/6\boldsymbol{\tilde{R}}2\boldsymbol{\tilde{R}}V_{m,p}^{3/2}$，其中$V_{m,p}$为精确方差，$A_{m,p}$为绝对三阶累积量。该等价式统一了平方、固定间隙、增长间隙、比例及稀疏 regime；在平方 regime 中，误差阶为$(\boldsymbol{\tilde{R}}p)^{-3/2}$且带有精确常数。对于每个正定总体相关矩阵$R$，我们证明了一致有限样本Berry-Esseen界，其明确跟踪总体依赖性。所有理论结果均有精确或已证明等价的Lean 4公式，其声明和依赖关系经内核检查。
英文摘要
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.
