Berry–Esseen Bounds for Independent Sums

2.7. Gaussian density calculus🔗

Lemma2.7.1
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 2.7.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbentkusanalysisintegration-by-partssource-bentkus-2004fidelity-schwartz-exact

Derivative integral against a Lipschitz function. Let E be a finite-dimensional real normed vector space with a Haar measure \lambda, let p:E\to\mathbb R be a Schwartz function, and suppose that f:E\to\mathbb R is a-Lipschitz. Then, for every h\in E, \left|\int_E f(y)\,Dp(y)[h]\,d\lambda(y)\right| \le a\|h\|\int_{\operatorname{tsupp}f}|p(y)|\,d\lambda(y).

Lean code for Lemma2.7.1●1 theorem
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianIntegrationByParts.lean
    complete
    theorem ProbabilityTheory.bentkus_lipschitz_schwartz_integral_fderiv_bound.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E → ℝ}
  {C : NNReal} (hf : LipschitzWith C f) (p : SchwartzMap E ℝ) (v : E) :
  |∫ (x : E), f x * (fderiv ℝ (⇑p) x) v ∂μ| ≤
    ↑C * ‖v‖ * ∫ (x : E) in tsupport f, |p x| ∂μ
    theorem ProbabilityTheory.bentkus_lipschitz_schwartz_integral_fderiv_bound.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  [BorelSpace E] [FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] {f : E → ℝ}
  {C : NNReal} (hf : LipschitzWith C f)
  (p : SchwartzMap E ℝ) (v : E) :
  |∫ (x : E),
        f x * (fderiv ℝ (⇑p) x) v ∂μ| ≤
    ↑C * ‖v‖ *
      ∫ (x : E) in tsupport f, |p x| ∂μ
    Bentkus's Lemma 2.3: a directional derivative may be transferred from a rapidly decaying
smooth function to a merely Lipschitz factor at the cost of restricting the absolute-value
integral to the topological support of that factor.

The Haar measure represents Lebesgue measure on the finite-dimensional real space.  The statement
is invariant under its arbitrary positive normalization.

This is Bentkus (2004), Lemma 2.3, equations (2.3)--(2.4), printed pp. 402--403. The paper's hypothesis that p and all of its derivatives decay faster than every inverse power is represented exactly by the Schwartz class; the formal theorem follows the paper's difference-quotient argument and does not assume that the Lipschitz factor is differentiable.

Theorem2.7.2
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 2.7.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbentkusgaussian-analysisdensity-derivativessource-bentkus-2004fidelity-explicit-absolute-constant

Gaussian density derivatives and the cubic-contraction bound. Let E be a finite-dimensional real inner-product space, let m=\dim E, and set \rho(x)=(2\pi)^{-m/2}e^{-\|x\|^2/2}. Its first three directional Fréchet derivatives are \begin{aligned} D\rho(x)[h] &=-\langle x,h\rangle\rho(x),\\ D^2\rho(x)[h,k] &=(\langle x,h\rangle\langle x,k\rangle-\langle h,k\rangle)\rho(x),\\ D^3\rho(x)[h,k,l] &=\bigl(-\langle x,h\rangle\langle x,k\rangle\langle x,l\rangle +\langle h,k\rangle\langle x,l\rangle +\langle h,l\rangle\langle x,k\rangle +\langle k,l\rangle\langle x,h\rangle\bigr)\rho(x). \end{aligned} In particular, D^3\rho(x)[w,w,g]=\rho(x)H_{w,g}(x), where H_{w,g}(x)=2\langle w,g\rangle\langle x,w\rangle +\|w\|^2\langle x,g\rangle -\langle x,g\rangle\langle x,w\rangle^2. The contraction H_{w,g} is integrable under the standard Gaussian law \gamma_E. Writing m_4=\int_{\mathbb R}t^4\,dN(0,1)(t), one has the dimension-free estimate \int_E|H_{w,g}(x)|\,d\gamma_E(x) \le(3+\sqrt{m_4})\,\|w\|^2\|g\|.

Lean code for Theorem2.7.2●19 declarations
  • defdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    def ProbabilityTheory.standardGaussianDensityNormalization.{u_2}
  (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] : ℝ
    def ProbabilityTheory.standardGaussianDensityNormalization.{u_2}
  (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] : ℝ
    The normalizing constant `(2π)⁻^(dim E / 2)` for the standard Gaussian density.
  • defdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    def ProbabilityTheory.standardGaussianDensity.{u_2} (E : Type u_2)
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (x : E) : ℝ
    def ProbabilityTheory.standardGaussianDensity.{u_2}
  (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x : E) : ℝ
    The standard Gaussian Lebesgue density on a finite-dimensional real inner-product space.
  • defdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    def ProbabilityTheory.standardGaussianDensityD1.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (x h : E) : ℝ
    def ProbabilityTheory.standardGaussianDensityD1.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x h : E) : ℝ
    The first derivative of the standard Gaussian density, contracted with one direction.
  • defdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    def ProbabilityTheory.standardGaussianDensityD2.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (x h k : E) : ℝ
    def ProbabilityTheory.standardGaussianDensityD2.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x h k : E) : ℝ
    The second derivative of the standard Gaussian density, contracted with two directions.
  • defdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    def ProbabilityTheory.standardGaussianDensityD3.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (x h k l : E) : ℝ
    def ProbabilityTheory.standardGaussianDensityD3.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x h k l : E) :
  ℝ
    The third derivative of the standard Gaussian density, contracted with three directions.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.hasFDerivAt_standardGaussianDensity.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x : E) :
  HasFDerivAt (ProbabilityTheory.standardGaussianDensity E)
    (-ProbabilityTheory.standardGaussianDensity E x • (innerSL ℝ) x) x
    theorem ProbabilityTheory.hasFDerivAt_standardGaussianDensity.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x : E) :
  HasFDerivAt
    (ProbabilityTheory.standardGaussianDensity
      E)
    (-ProbabilityTheory.standardGaussianDensity
          E x •
      (innerSL ℝ) x)
    x
    The exact Fréchet derivative of the standard Gaussian density.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.fderiv_standardGaussianDensity_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x h : E) :
  (fderiv ℝ (ProbabilityTheory.standardGaussianDensity E) x) h =
    ProbabilityTheory.standardGaussianDensityD1 x h
    theorem ProbabilityTheory.fderiv_standardGaussianDensity_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x h : E) :
  (fderiv ℝ
        (ProbabilityTheory.standardGaussianDensity
          E)
        x)
      h =
    ProbabilityTheory.standardGaussianDensityD1
      x h
    Contracting the Fréchet derivative gives the first directional formula.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.fderiv_standardGaussianDensityD1_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x h k : E) :
  (fderiv ℝ (fun y => ProbabilityTheory.standardGaussianDensityD1 y h)
        x)
      k =
    ProbabilityTheory.standardGaussianDensityD2 x h k
    theorem ProbabilityTheory.fderiv_standardGaussianDensityD1_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x h k : E) :
  (fderiv ℝ
        (fun y =>
          ProbabilityTheory.standardGaussianDensityD1
            y h)
        x)
      k =
    ProbabilityTheory.standardGaussianDensityD2
      x h k
    The derivative of the first contraction is the second contraction.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.fderiv_standardGaussianDensityD2_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x h k l : E) :
  (fderiv ℝ (fun y => ProbabilityTheory.standardGaussianDensityD2 y h k)
        x)
      l =
    ProbabilityTheory.standardGaussianDensityD3 x h k l
    theorem ProbabilityTheory.fderiv_standardGaussianDensityD2_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x h k l : E) :
  (fderiv ℝ
        (fun y =>
          ProbabilityTheory.standardGaussianDensityD2
            y h k)
        x)
      l =
    ProbabilityTheory.standardGaussianDensityD3
      x h k l
    The derivative of the second contraction is the third contraction.
  • defdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    def ProbabilityTheory.gaussianThirdHermiteContraction.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x w g : E) : ℝ
    def ProbabilityTheory.gaussianThirdHermiteContraction.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (x w g : E) : ℝ
    The cubic Hermite contraction in Bentkus (2004), equation (3.21).
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.standardGaussianDensityD3_sameDirection.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x w g : E) :
  ProbabilityTheory.standardGaussianDensityD3 x w w g =
    ProbabilityTheory.standardGaussianDensity E x *
      ProbabilityTheory.gaussianThirdHermiteContraction x w g
    theorem ProbabilityTheory.standardGaussianDensityD3_sameDirection.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x w g : E) :
  ProbabilityTheory.standardGaussianDensityD3
      x w w g =
    ProbabilityTheory.standardGaussianDensity
        E x *
      ProbabilityTheory.gaussianThirdHermiteContraction
        x w g
    The twice-equal-direction third derivative is exactly Bentkus's formula (3.21).
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.fderiv_standardGaussianDensityD2_sameDirection.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x w g : E) :
  (fderiv ℝ (fun y => ProbabilityTheory.standardGaussianDensityD2 y w w)
        x)
      g =
    ProbabilityTheory.standardGaussianDensity E x *
      ProbabilityTheory.gaussianThirdHermiteContraction x w g
    theorem ProbabilityTheory.fderiv_standardGaussianDensityD2_sameDirection.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (x w g : E) :
  (fderiv ℝ
        (fun y =>
          ProbabilityTheory.standardGaussianDensityD2
            y w w)
        x)
      g =
    ProbabilityTheory.standardGaussianDensity
        E x *
      ProbabilityTheory.gaussianThirdHermiteContraction
        x w g
    Equation (3.21) as a third directional Fréchet-derivative identity.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.integrable_gaussianThirdHermiteContraction_stdGaussian.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (w g : E) :
  MeasureTheory.Integrable
    (fun x => ProbabilityTheory.gaussianThirdHermiteContraction x w g)
    (ProbabilityTheory.stdGaussian E)
    theorem ProbabilityTheory.integrable_gaussianThirdHermiteContraction_stdGaussian.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (w g : E) :
  MeasureTheory.Integrable
    (fun x =>
      ProbabilityTheory.gaussianThirdHermiteContraction
        x w g)
    (ProbabilityTheory.stdGaussian E)
    The cubic Hermite contraction in Bentkus's equation (3.21) is integrable under standard
Gaussian measure.
  • defdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    def ProbabilityTheory.standardGaussianFourthMoment : ℝ
    def ProbabilityTheory.standardGaussianFourthMoment :
  ℝ
    The universal fourth moment used in the dimension-free bound for the cubic contraction.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.standardGaussianFourthMoment_nonneg :
  0 ≤ ProbabilityTheory.standardGaussianFourthMoment
    theorem ProbabilityTheory.standardGaussianFourthMoment_nonneg :
  0 ≤
    ProbabilityTheory.standardGaussianFourthMoment
    The universal fourth moment is nonnegative.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.integral_inner_pow_four_stdGaussian.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (v : E) :
  ∫ (x : E), inner ℝ v x ^ 4 ∂ProbabilityTheory.stdGaussian E =
    ‖v‖ ^ 4 * ProbabilityTheory.standardGaussianFourthMoment
    theorem ProbabilityTheory.integral_inner_pow_four_stdGaussian.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (v : E) :
  ∫ (x : E),
      inner ℝ v x ^
        4 ∂ProbabilityTheory.stdGaussian
        E =
    ‖v‖ ^ 4 *
      ProbabilityTheory.standardGaussianFourthMoment
    A linear functional of a standard Gaussian has the expected fourth-moment scaling.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.integral_inner_sq_stdGaussian.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (v : E) :
  ∫ (x : E), inner ℝ v x ^ 2 ∂ProbabilityTheory.stdGaussian E = ‖v‖ ^ 2
    theorem ProbabilityTheory.integral_inner_sq_stdGaussian.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (v : E) :
  ∫ (x : E),
      inner ℝ v x ^
        2 ∂ProbabilityTheory.stdGaussian
        E =
    ‖v‖ ^ 2
    A linear functional of a standard Gaussian has second moment equal to its squared norm.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.integral_abs_inner_stdGaussian_le_norm.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (v : E) :
  ∫ (x : E), |inner ℝ v x| ∂ProbabilityTheory.stdGaussian E ≤ ‖v‖
    theorem ProbabilityTheory.integral_abs_inner_stdGaussian_le_norm.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (v : E) :
  ∫ (x : E),
      |inner ℝ v
          x| ∂ProbabilityTheory.stdGaussian
        E ≤
    ‖v‖
    The first absolute moment of a standard-Gaussian linear functional is at most its norm.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityDerivatives.lean
    complete
    theorem ProbabilityTheory.integral_abs_gaussianThirdHermiteContraction_le.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (w g : E) :
  ∫ (x : E),
      |ProbabilityTheory.gaussianThirdHermiteContraction x w
          g| ∂ProbabilityTheory.stdGaussian E ≤
    (3 + √ProbabilityTheory.standardGaussianFourthMoment) * ‖w‖ ^ 2 *
      ‖g‖
    theorem ProbabilityTheory.integral_abs_gaussianThirdHermiteContraction_le.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (w g : E) :
  ∫ (x : E),
      |ProbabilityTheory.gaussianThirdHermiteContraction
          x w
          g| ∂ProbabilityTheory.stdGaussian
        E ≤
    (3 +
          √ProbabilityTheory.standardGaussianFourthMoment) *
        ‖w‖ ^ 2 *
      ‖g‖
    Dimension-free integral bound for Bentkus's third-derivative contraction.

The coefficient is an absolute constant: it depends only on the fourth moment of a one-dimensional
standard Gaussian.  This is the precise formal counterpart of the estimate following equations
(3.21)--(3.23) on original pages 405--406 of Bentkus (2004).

This supplies the exact Gaussian analytic input to the integration-by-parts estimate in Bentkus (2004), Lemma 2.3, equations (2.3)--(2.4), printed pp. 402--403. The twice-equal third derivative is equation (3.21), printed p. 405, and the absolute Gaussian integral estimate is the dimension-free content used in (3.22)--(3.23), printed pp. 405--406. The general Lipschitz integration-by-parts lemma itself remains the separate node immediately above.

Theorem2.7.3
Statement uses 2
Statement dependency previews
Preview
Lemma 2.7.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 2.7.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbentkusgaussian-analysisintegration-by-partssource-bentkus-2004fidelity-exact-gaussian-specialization

Gaussian integration by parts localized to the support of a Lipschitz factor. Put \rho(y)=(2\pi)^{-d/2}e^{-\|y\|^2/2}. The directional derivative D\rho(\cdot)[w] is Lebesgue integrable. If f:\mathbb R^d\to\mathbb R is globally Lipschitz and differentiable, then \int_{\mathbb R^d}Df(y)[h]\rho(y)\,dy =-\int_{\mathbb R^d}f(y)D\rho(y)[h]\,dy. Moreover, if f is L-Lipschitz, then, for all w,h\in\mathbb R^d, \left|\int_{\mathbb R^d}f(y)D^2\rho(y)[w,h],dy\right| \le L\|h\| \int_{\operatorname{tsupp}f}|D\rho(y)[w]|\,dy.

Lean code for Theorem2.7.3●3 theorems
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityIntegrationByParts.lean
    complete
    theorem ProbabilityTheory.integrable_standardGaussianDensityD1_volume {d : ℕ}
  (w : EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.Integrable
    (fun x => ProbabilityTheory.standardGaussianDensityD1 x w)
    MeasureTheory.volume
    theorem ProbabilityTheory.integrable_standardGaussianDensityD1_volume
  {d : ℕ} (w : EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.Integrable
    (fun x =>
      ProbabilityTheory.standardGaussianDensityD1
        x w)
    MeasureTheory.volume
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityIntegrationByParts.lean
    complete
    theorem ProbabilityTheory.integral_fderiv_mul_standardGaussianDensity_eq_neg
  {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} {C : NNReal}
  (hf : LipschitzWith C f) (hfdiff : Differentiable ℝ f)
  (h : EuclideanSpace ℝ (Fin d)) :
  ∫ (x : EuclideanSpace ℝ (Fin d)),
      (fderiv ℝ f x) h *
        ProbabilityTheory.standardGaussianDensity
          (EuclideanSpace ℝ (Fin d)) x =
    -∫ (x : EuclideanSpace ℝ (Fin d)),
        f x * ProbabilityTheory.standardGaussianDensityD1 x h
    theorem ProbabilityTheory.integral_fderiv_mul_standardGaussianDensity_eq_neg
  {d : ℕ}
  {f : EuclideanSpace ℝ (Fin d) → ℝ}
  {C : NNReal} (hf : LipschitzWith C f)
  (hfdiff : Differentiable ℝ f)
  (h : EuclideanSpace ℝ (Fin d)) :
  ∫ (x : EuclideanSpace ℝ (Fin d)),
      (fderiv ℝ f x) h *
        ProbabilityTheory.standardGaussianDensity
          (EuclideanSpace ℝ (Fin d)) x =
    -∫ (x : EuclideanSpace ℝ (Fin d)),
        f x *
          ProbabilityTheory.standardGaussianDensityD1
            x h
    First-order integration by parts for standard Gaussian density against a globally Lipschitz
`C¹` function.  This is the density identity used before the Taylor expansion in Bentkus (2004),
equation (3.32), p. 407.
  • theoremdefined in ProbabilityApproximation/Bentkus/GaussianDensityIntegrationByParts.lean
    complete
    theorem ProbabilityTheory.bentkus_lipschitz_standardGaussianDensityD1_integral_D2_bound
  {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} {C : NNReal}
  (hf : LipschitzWith C f) (w h : EuclideanSpace ℝ (Fin d)) :
  |∫ (x : EuclideanSpace ℝ (Fin d)),
        f x * ProbabilityTheory.standardGaussianDensityD2 x w h| ≤
    ↑C * ‖h‖ *
      ∫ (x : EuclideanSpace ℝ (Fin d)) in tsupport f,
        |ProbabilityTheory.standardGaussianDensityD1 x w|
    theorem ProbabilityTheory.bentkus_lipschitz_standardGaussianDensityD1_integral_D2_bound
  {d : ℕ}
  {f : EuclideanSpace ℝ (Fin d) → ℝ}
  {C : NNReal} (hf : LipschitzWith C f)
  (w h : EuclideanSpace ℝ (Fin d)) :
  |∫ (x : EuclideanSpace ℝ (Fin d)),
        f x *
          ProbabilityTheory.standardGaussianDensityD2
            x w h| ≤
    ↑C * ‖h‖ *
      ∫ (x : EuclideanSpace ℝ (Fin d)) in
        tsupport f,
        |ProbabilityTheory.standardGaussianDensityD1
            x w|
    Bentkus (2004), Lemma 2.3, specialized to the first derivative of the standard Gaussian
density.  This is the exact rapid-decay integration-by-parts estimate used in equation (3.32).

This is Bentkus (2004), Lemma 2.3, equations (2.3)--(2.4), printed pp. 402--403. The first identity is the Gaussian-density integration-by-parts step used in equation (3.32), printed p. 407; the final estimate specializes Lemma 2.3 to p=D\rho(\cdot)[w].

Theorem2.7.4
Statement uses 2
Statement dependency previews
Preview
Lemma 2.6.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsbentkusgaussian-replacementcutoffintegration-by-partssource-bentkus-2004fidelity-exact-closed-shell-support

Pulled-back cutoff derivative and its shell-localized bound. Let A be closed and convex, \varepsilon>0, and let \varphi_A be the Bentkus cutoff. For a,x\in\mathbb R^d and a linear map L, set q(u)=D\varphi_A(a+Lu)[x]. Then q is 8\|L\|\|x\|/\varepsilon^2-Lipschitz and \operatorname{tsupp}q\subseteq \{u:a+Lu\in A^+_\varepsilon\setminus\operatorname{int}A\}. Consequently, for all w,h\in\mathbb R^d, \begin{aligned} \left|\int q(u)D^2\rho(u)[w,h],du\right| \le{}&\frac{8\|L\|\|x\|\|h\|}{\varepsilon^2}\\ &\cdot\int_{\{u:a+Lu\in A^+_\varepsilon\setminus\operatorname{int}A\}} |D\rho(u)[w]|\,du. \end{aligned}

Lean code for Theorem2.7.4●5 declarations
  • defdefined in ProbabilityApproximation/Bentkus/CutoffDerivativeGaussianIBP.lean
    complete
    def ProbabilityTheory.convexSetCutoffDirectionalPullback {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (ε : ℝ)
  (a x : EuclideanSpace ℝ (Fin d))
  (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)) :
  EuclideanSpace ℝ (Fin d) → ℝ
    def ProbabilityTheory.convexSetCutoffDirectionalPullback
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (ε : ℝ) (a x : EuclideanSpace ℝ (Fin d))
  (L :
    EuclideanSpace ℝ (Fin d) →L[ℝ]
      EuclideanSpace ℝ (Fin d)) :
  EuclideanSpace ℝ (Fin d) → ℝ
    The directional derivative of the Bentkus cutoff after an affine linear pullback.
  • theoremdefined in ProbabilityApproximation/Bentkus/CutoffDerivativeGaussianIBP.lean
    complete
    theorem ProbabilityTheory.lipschitzWith_convexSetCutoffDirectionalPullback
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ} (hε : 0 < ε)
  (a x : EuclideanSpace ℝ (Fin d))
  (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)) :
  LipschitzWith ⟨8 / ε ^ 2 * ‖L‖ * ‖x‖, ⋯⟩
    (ProbabilityTheory.convexSetCutoffDirectionalPullback s ε a x L)
    theorem ProbabilityTheory.lipschitzWith_convexSetCutoffDirectionalPullback
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε)
  (a x : EuclideanSpace ℝ (Fin d))
  (L :
    EuclideanSpace ℝ (Fin d) →L[ℝ]
      EuclideanSpace ℝ (Fin d)) :
  LipschitzWith ⟨8 / ε ^ 2 * ‖L‖ * ‖x‖, ⋯⟩
    (ProbabilityTheory.convexSetCutoffDirectionalPullback
      s ε a x L)
    Pulling a cutoff derivative back by `u ↦ a + L u` multiplies its Lipschitz constant by
`‖L‖`; evaluation in direction `x` contributes `‖x‖`.
  • theoremdefined in ProbabilityApproximation/Bentkus/CutoffDerivativeGaussianIBP.lean
    complete
    theorem ProbabilityTheory.tsupport_convexSetCutoffDirectionalPullback_subset
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} (hsclosed : IsClosed s)
  (_hs : Convexity.IsConvexSet ℝ s) {ε : ℝ} (hε : 0 < ε)
  (a x : EuclideanSpace ℝ (Fin d))
  (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)) :
  tsupport
      (ProbabilityTheory.convexSetCutoffDirectionalPullback s ε a x L) ⊆
    (fun u => a + L u) ⁻¹' (Metric.cthickening ε s \ interior s)
    theorem ProbabilityTheory.tsupport_convexSetCutoffDirectionalPullback_subset
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hsclosed : IsClosed s)
  (_hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε)
  (a x : EuclideanSpace ℝ (Fin d))
  (L :
    EuclideanSpace ℝ (Fin d) →L[ℝ]
      EuclideanSpace ℝ (Fin d)) :
  tsupport
      (ProbabilityTheory.convexSetCutoffDirectionalPullback
        s ε a x L) ⊆
    (fun u => a + L u) ⁻¹'
      (Metric.cthickening ε s \
        interior s)
    The pulled-back cutoff derivative is supported on the closed outer shell.  The inner set is
removed only through its interior: boundary points can belong to the topological support even
though the derivative itself vanishes there.  This is the support convention needed in Bentkus
(2004), equation (3.32), p. 407.
  • theoremdefined in ProbabilityApproximation/Bentkus/CutoffDerivativeGaussianIBP.lean
    complete
    theorem ProbabilityTheory.convexSetCutoffDirectionalPullback_D2_bound {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) (a x : EuclideanSpace ℝ (Fin d))
  (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d))
  (w h : EuclideanSpace ℝ (Fin d)) :
  |∫ (u : EuclideanSpace ℝ (Fin d)),
        ProbabilityTheory.convexSetCutoffDirectionalPullback s ε a x L
            u *
          ProbabilityTheory.standardGaussianDensityD2 u w h| ≤
    8 / ε ^ 2 * ‖L‖ * ‖x‖ * ‖h‖ *
      ∫ (u : EuclideanSpace ℝ (Fin d)) in
        tsupport
          (ProbabilityTheory.convexSetCutoffDirectionalPullback s ε a x
            L),
        |ProbabilityTheory.standardGaussianDensityD1 u w|
    theorem ProbabilityTheory.convexSetCutoffDirectionalPullback_D2_bound
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε)
  (a x : EuclideanSpace ℝ (Fin d))
  (L :
    EuclideanSpace ℝ (Fin d) →L[ℝ]
      EuclideanSpace ℝ (Fin d))
  (w h : EuclideanSpace ℝ (Fin d)) :
  |∫ (u : EuclideanSpace ℝ (Fin d)),
        ProbabilityTheory.convexSetCutoffDirectionalPullback
            s ε a x L u *
          ProbabilityTheory.standardGaussianDensityD2
            u w h| ≤
    8 / ε ^ 2 * ‖L‖ * ‖x‖ * ‖h‖ *
      ∫ (u : EuclideanSpace ℝ (Fin d)) in
        tsupport
          (ProbabilityTheory.convexSetCutoffDirectionalPullback
            s ε a x L),
        |ProbabilityTheory.standardGaussianDensityD1
            u w|
    Bentkus's Gaussian density integration-by-parts bound for the affine pullback of a cutoff
directional derivative.  This is the deterministic core of equation (3.32), p. 407.
  • theoremdefined in ProbabilityApproximation/Bentkus/CutoffDerivativeGaussianIBP.lean
    complete
    theorem ProbabilityTheory.convexSetCutoffDirectionalPullback_D2_shell_bound
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} (hsclosed : IsClosed s)
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ} (hε : 0 < ε)
  (a x : EuclideanSpace ℝ (Fin d))
  (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d))
  (w h : EuclideanSpace ℝ (Fin d)) :
  |∫ (u : EuclideanSpace ℝ (Fin d)),
        ProbabilityTheory.convexSetCutoffDirectionalPullback s ε a x L
            u *
          ProbabilityTheory.standardGaussianDensityD2 u w h| ≤
    8 / ε ^ 2 * ‖L‖ * ‖x‖ * ‖h‖ *
      ∫ (u : EuclideanSpace ℝ (Fin d)) in
        (fun u => a + L u) ⁻¹' (Metric.cthickening ε s \ interior s),
        |ProbabilityTheory.standardGaussianDensityD1 u w|
    theorem ProbabilityTheory.convexSetCutoffDirectionalPullback_D2_shell_bound
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hsclosed : IsClosed s)
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε)
  (a x : EuclideanSpace ℝ (Fin d))
  (L :
    EuclideanSpace ℝ (Fin d) →L[ℝ]
      EuclideanSpace ℝ (Fin d))
  (w h : EuclideanSpace ℝ (Fin d)) :
  |∫ (u : EuclideanSpace ℝ (Fin d)),
        ProbabilityTheory.convexSetCutoffDirectionalPullback
            s ε a x L u *
          ProbabilityTheory.standardGaussianDensityD2
            u w h| ≤
    8 / ε ^ 2 * ‖L‖ * ‖x‖ * ‖h‖ *
      ∫ (u : EuclideanSpace ℝ (Fin d)) in
        (fun u => a + L u) ⁻¹'
          (Metric.cthickening ε s \
            interior s),
        |ProbabilityTheory.standardGaussianDensityD1
            u w|
    The integration-by-parts estimate with the topological support replaced by the explicit
closed shell.  This is the form inserted into the leave-one-out shell probabilities in Bentkus
(2004), equations (3.30)--(3.34), pp. 407--408.

This is the deterministic integration-by-parts step in Bentkus (2004), equation (3.32), printed p. 407, with the shell placement used in equations (3.30)--(3.34), printed pp. 407--408. The topological support retains the boundary of A, hence the exact shell removes only \operatorname{int}A.