2.10. Bentkus's convex-set theorem
Bentkus's Lyapunov bound for convex sets. There is an absolute constant C>0 with the
following property. Let d,n\in\mathbb N with d>0, let
X_1,\ldots,X_n be independent measurable random vectors in \mathbb R^d such that
\mathbb E X_i=0,
\qquad
\mathbb E\|X_i\|^3<\infty,
and set W=\sum_{i=1}^n X_i. Suppose that the covariance matrix
S=\operatorname{Cov}(W) is positive definite, and let G be a centered Gaussian
random vector with covariance matrix S. Then for every measurable convex set
A\subseteq\mathbb R^d,
\left|\Pr(W\in A)-\Pr(G\in A)\right|
\le
C d^{1/4}\sum_{i=1}^n
\mathbb E\left\|S^{-1/2}X_i\right\|^3.
Lean code for Theorem2.10.1●1 theorem
Associated Lean declarations
-
theoremdefined in ProbabilityApproximation/Bentkus/Induction.leancomplete
theorem ProbabilityTheory.exists_bentkus_convex_set_constant.{u} : ∃ C, 0 < C ∧ ∀ {d n : ℕ}, 0 < d → ∀ {Ω : Type u} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) (S : Matrix (Fin d) (Fin d) ℝ), (∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ) → ProbabilityTheory.iIndepFun X μ → (∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) → S.PosDef → (∀ (x y : EuclideanSpace ℝ (Fin d)), ((ProbabilityTheory.covarianceBilin (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ)) x) y = x.ofLp ⬝ᵥ S.mulVec y.ofLp) → ∀ (A : Set (EuclideanSpace ℝ (Fin d))), MeasurableSet A → Convexity.IsConvexSet ℝ A → |((MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ) A).toReal - ((ProbabilityTheory.multivariateGaussian 0 S) A).toReal| ≤ C * ↑d ^ (1 / 4) * ∑ i, ∫ (ω : Ω), ‖(Matrix.toEuclideanCLM (CFC.sqrt S)⁻¹) (X i ω)‖ ^ 3 ∂μ
theorem ProbabilityTheory.exists_bentkus_convex_set_constant.{u} : ∃ C, 0 < C ∧ ∀ {d n : ℕ}, 0 < d → ∀ {Ω : Type u} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) (S : Matrix (Fin d) (Fin d) ℝ), (∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ) → ProbabilityTheory.iIndepFun X μ → (∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) → S.PosDef → (∀ (x y : EuclideanSpace ℝ (Fin d)), ((ProbabilityTheory.covarianceBilin (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ)) x) y = x.ofLp ⬝ᵥ S.mulVec y.ofLp) → ∀ (A : Set (EuclideanSpace ℝ (Fin d))), MeasurableSet A → Convexity.IsConvexSet ℝ A → |((MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ) A).toReal - ((ProbabilityTheory.multivariateGaussian 0 S) A).toReal| ≤ C * ↑d ^ (1 / 4) * ∑ i, ∫ (ω : Ω), ‖(Matrix.toEuclideanCLM (CFC.sqrt S)⁻¹) (X i ω)‖ ^ 3 ∂μ
Bentkus's multivariate Berry--Esseen theorem for measurable convex sets.
This is Theorem 1.1 and equation (1.1) of Bentkus (2004), printed
pp. 400--401. The matrix S here is the total covariance; S^{-1/2} is the
paper's inverse of the positive covariance square root. The proof first establishes the
standardized replacement estimate and then applies covariance-square-root whitening.