2.10. Bentkus's convex-set theorem🔗

Theorem2.10.1

Statement uses 2

Statement dependency previews

Preview

Theorem 2.3.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagsprincipal-theoremsource-bentkus-2004multivariateconvex-setfidelity-exact

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

theoremdefined in ProbabilityApproximation/Bentkus/Induction.lean

complete

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 associated declaration first proves the standardized replacement theorem and then transports it through covariance-square-root whitening.