2.6. Smoothing convex indicators🔗

Lemma2.6.1

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 2.2.7

Loading preview

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

✓L∃∀N

Tagsbentkussmoothingsource-bentkus-2004fidelity-explicit-boundary-convention

Setwise Bentkus smoothing inequality. Let \mu,\nu be probability measures on \mathbb R^d, let A be measurable and convex, and let \varepsilon>0. Define the closed outer parallel set and the inner core by A^+_\varepsilon=\{x:d(x,\overline A)\le\varepsilon\},\qquad A^-_\varepsilon=\{x:B(x,\varepsilon)\subseteq A\}, where B(x,\varepsilon) is the open ball. The inner core is closed, convex, and contained in A. There are total cutoffs \varphi_A and \varphi_{A^-_\varepsilon} with values in [0,1], equal to 1 on their indexing set and equal to 0 respectively off A^+_\varepsilon and off A. They are continuously differentiable and obey \|D\varphi(x)\|\le\frac2\varepsilon,\qquad \|D\varphi(x)-D\varphi(y)\| \le\frac8{\varepsilon^2}\|x-y\|. Moreover, \begin{aligned} |\mu(A)-\nu(A)|\le{}& \max\!\left\{ \left|\int\varphi_A\,d\mu-\int\varphi_A\,d\nu\right|, \left|\int\varphi_{A^-_\varepsilon}\,d\mu- \int\varphi_{A^-_\varepsilon}\,d\nu\right| \right\}\\ &+\max\!\left\{ \nu(A^+_\varepsilon\setminus A), \nu(A\setminus A^-_\varepsilon) \right\}. \end{aligned}

Lean code for Lemma2.6.1●15 declarations

defdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

def ProbabilityTheory.convexInnerParallel {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (ε : ℝ) :
  Set (EuclideanSpace ℝ (Fin d))

def ProbabilityTheory.convexInnerParallel
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (ε : ℝ) : Set (EuclideanSpace ℝ (Fin d))

The inner parallel set at radius `ε`, with the boundary convention obtained by taking the
complement of the *open* `ε`-thickening of the complement.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.mem_convexInnerParallel_iff_ball_subset {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} {ε : ℝ}
  {x : EuclideanSpace ℝ (Fin d)} :
  x ∈ ProbabilityTheory.convexInnerParallel s ε ↔ Metric.ball x ε ⊆ s

theorem ProbabilityTheory.mem_convexInnerParallel_iff_ball_subset
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {ε : ℝ} {x : EuclideanSpace ℝ (Fin d)} :
  x ∈
      ProbabilityTheory.convexInnerParallel
        s ε ↔
    Metric.ball x ε ⊆ s

Membership in the inner parallel set means that the *open* `ε`-ball is contained in the
original set.  This lemma records the boundary convention used by the smoothing inequality.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.convexInnerParallel_subset {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) {ε : ℝ} (hε : 0 < ε) :
  ProbabilityTheory.convexInnerParallel s ε ⊆ s

theorem ProbabilityTheory.convexInnerParallel_subset
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  {ε : ℝ} (hε : 0 < ε) :
  ProbabilityTheory.convexInnerParallel s
      ε ⊆
    s

At positive radius the inner parallel set is contained in the original set.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.convexInnerParallel_isConvexSet {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  (ε : ℝ) :
  Convexity.IsConvexSet ℝ (ProbabilityTheory.convexInnerParallel s ε)

theorem ProbabilityTheory.convexInnerParallel_isConvexSet
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s)
  (ε : ℝ) :
  Convexity.IsConvexSet ℝ
    (ProbabilityTheory.convexInnerParallel
      s ε)

The inner parallel set of a convex set is convex.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.closure_isConvexSet {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) : Convexity.IsConvexSet ℝ (closure s)

theorem ProbabilityTheory.closure_isConvexSet
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) :
  Convexity.IsConvexSet ℝ (closure s)

Closure preserves convexity in finite-dimensional Euclidean space, stated directly in the
new `Convexity.IsConvexSet` API.

defdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

def ProbabilityTheory.convexSetCutoff {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (ε : ℝ) :
  EuclideanSpace ℝ (Fin d) → ℝ

def ProbabilityTheory.convexSetCutoff {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (ε : ℝ) : EuclideanSpace ℝ (Fin d) → ℝ

A total version of the Bentkus cutoff.  For a nonempty set it is the exact distance cutoff of
its closure; for the empty set it is the constant-zero smooth function.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.convexSetCutoff_nonneg {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (ε : ℝ)
  (x : EuclideanSpace ℝ (Fin d)) :
  0 ≤ ProbabilityTheory.convexSetCutoff s ε x

theorem ProbabilityTheory.convexSetCutoff_nonneg
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (ε : ℝ) (x : EuclideanSpace ℝ (Fin d)) :
  0 ≤
    ProbabilityTheory.convexSetCutoff s ε
      x

The total convex-set cutoff is nonnegative.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.convexSetCutoff_le_one {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (ε : ℝ)
  (x : EuclideanSpace ℝ (Fin d)) :
  ProbabilityTheory.convexSetCutoff s ε x ≤ 1

theorem ProbabilityTheory.convexSetCutoff_le_one
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (ε : ℝ) (x : EuclideanSpace ℝ (Fin d)) :
  ProbabilityTheory.convexSetCutoff s ε
      x ≤
    1

The total convex-set cutoff is at most one.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.convexSetCutoff_eq_one_of_mem {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} {ε : ℝ}
  {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ s) :
  ProbabilityTheory.convexSetCutoff s ε x = 1

theorem ProbabilityTheory.convexSetCutoff_eq_one_of_mem
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {ε : ℝ} {x : EuclideanSpace ℝ (Fin d)}
  (hx : x ∈ s) :
  ProbabilityTheory.convexSetCutoff s ε
      x =
    1

The total cutoff equals one on the original set.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.convexSetCutoff_eq_zero_of_notMem_cthickening {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} {ε : ℝ} (hε : 0 < ε)
  {x : EuclideanSpace ℝ (Fin d)}
  (hx : x ∉ Metric.cthickening ε (closure s)) :
  ProbabilityTheory.convexSetCutoff s ε x = 0

theorem ProbabilityTheory.convexSetCutoff_eq_zero_of_notMem_cthickening
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {ε : ℝ} (hε : 0 < ε)
  {x : EuclideanSpace ℝ (Fin d)}
  (hx :
    x ∉
      Metric.cthickening ε (closure s)) :
  ProbabilityTheory.convexSetCutoff s ε
      x =
    0

The total cutoff vanishes outside the closed outer parallel set.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.convexSetCutoff_inner_eq_zero_of_notMem {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} {ε : ℝ} (hε : 0 < ε)
  {x : EuclideanSpace ℝ (Fin d)} (hx : x ∉ s) :
  ProbabilityTheory.convexSetCutoff
      (ProbabilityTheory.convexInnerParallel s ε) ε x =
    0

theorem ProbabilityTheory.convexSetCutoff_inner_eq_zero_of_notMem
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {ε : ℝ} (hε : 0 < ε)
  {x : EuclideanSpace ℝ (Fin d)}
  (hx : x ∉ s) :
  ProbabilityTheory.convexSetCutoff
      (ProbabilityTheory.convexInnerParallel
        s ε)
      ε x =
    0

The cutoff of the inner parallel set vanishes off the original set.  This is where the open
thickening in the definition of `convexInnerParallel` fixes the boundary convention.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.contDiff_convexSetCutoff {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) :
  ContDiff ℝ 1 (ProbabilityTheory.convexSetCutoff s ε)

theorem ProbabilityTheory.contDiff_convexSetCutoff
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε) :
  ContDiff ℝ 1
    (ProbabilityTheory.convexSetCutoff s
      ε)

For convex `s`, the total cutoff is continuously differentiable, including the empty and
whole-space edge cases.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.norm_fderiv_convexSetCutoff_le {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) (x : EuclideanSpace ℝ (Fin d)) :
  ‖fderiv ℝ (ProbabilityTheory.convexSetCutoff s ε) x‖ ≤ 2 / ε

theorem ProbabilityTheory.norm_fderiv_convexSetCutoff_le
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε)
  (x : EuclideanSpace ℝ (Fin d)) :
  ‖fderiv ℝ
        (ProbabilityTheory.convexSetCutoff
          s ε)
        x‖ ≤
    2 / ε

The total convex-set cutoff retains the exact `2 / ε` first-derivative bound.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.norm_fderiv_convexSetCutoff_sub_le {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) (x y : EuclideanSpace ℝ (Fin d)) :
  ‖fderiv ℝ (ProbabilityTheory.convexSetCutoff s ε) x -
        fderiv ℝ (ProbabilityTheory.convexSetCutoff s ε) y‖ ≤
    8 * ‖x - y‖ / ε ^ 2

theorem ProbabilityTheory.norm_fderiv_convexSetCutoff_sub_le
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ‖fderiv ℝ
          (ProbabilityTheory.convexSetCutoff
            s ε)
          x -
        fderiv ℝ
          (ProbabilityTheory.convexSetCutoff
            s ε)
          y‖ ≤
    8 * ‖x - y‖ / ε ^ 2

The total convex-set cutoff retains the exact `8 / ε²` Lipschitz bound on its derivative.

theoremdefined in ProbabilityApproximation/Bentkus/SmoothingInequality.lean

complete

theorem ProbabilityTheory.bentkus_convexSet_smoothingInequality {d : ℕ}
  (mu nu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d)))
  [MeasureTheory.IsProbabilityMeasure mu]
  [MeasureTheory.IsProbabilityMeasure nu]
  {s : Set (EuclideanSpace ℝ (Fin d))} (hsmeas : MeasurableSet s)
  (_hsconv : Convexity.IsConvexSet ℝ s) {ε : ℝ} (hε : 0 < ε) :
  |mu.real s - nu.real s| ≤
    max
        |∫ (x : EuclideanSpace ℝ (Fin d)),
              ProbabilityTheory.convexSetCutoff s ε x ∂mu -
            ∫ (x : EuclideanSpace ℝ (Fin d)),
              ProbabilityTheory.convexSetCutoff s ε x ∂nu|
        |∫ (x : EuclideanSpace ℝ (Fin d)),
              ProbabilityTheory.convexSetCutoff
                (ProbabilityTheory.convexInnerParallel s ε) ε x ∂mu -
            ∫ (x : EuclideanSpace ℝ (Fin d)),
              ProbabilityTheory.convexSetCutoff
                (ProbabilityTheory.convexInnerParallel s ε) ε x ∂nu| +
      max (nu.real (Metric.cthickening ε (closure s) \ s))
        (nu.real (s \ ProbabilityTheory.convexInnerParallel s ε))

theorem ProbabilityTheory.bentkus_convexSet_smoothingInequality
  {d : ℕ}
  (mu nu :
    MeasureTheory.Measure
      (EuclideanSpace ℝ (Fin d)))
  [MeasureTheory.IsProbabilityMeasure mu]
  [MeasureTheory.IsProbabilityMeasure nu]
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hsmeas : MeasurableSet s)
  (_hsconv : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) :
  |mu.real s - nu.real s| ≤
    max
        |∫ (x : EuclideanSpace ℝ (Fin d)),
              ProbabilityTheory.convexSetCutoff
                s ε x ∂mu -
            ∫ (x :
              EuclideanSpace ℝ (Fin d)),
              ProbabilityTheory.convexSetCutoff
                s ε x ∂nu|
        |∫ (x : EuclideanSpace ℝ (Fin d)),
              ProbabilityTheory.convexSetCutoff
                (ProbabilityTheory.convexInnerParallel
                  s ε)
                ε x ∂mu -
            ∫ (x :
              EuclideanSpace ℝ (Fin d)),
              ProbabilityTheory.convexSetCutoff
                (ProbabilityTheory.convexInnerParallel
                  s ε)
                ε x ∂nu| +
      max
        (nu.real
          (Metric.cthickening ε
              (closure s) \
            s))
        (nu.real
          (s \
            ProbabilityTheory.convexInnerParallel
              s ε))

**Bentkus smoothing inequality, setwise form.**

For two probability measures `mu` and `nu`, the convex-set probability error is bounded by the
larger of the two smooth cutoff expectation errors, plus the larger of the outer and inner shell
probabilities under the reference measure `nu`.  This is the exact form that will consume the
Gaussian shell theorem: no shell estimate is assumed here.

The two cutoffs are `C¹` and satisfy the exact derivative bounds `2 / ε` and `8 / ε²` by
`contDiff_convexSetCutoff`, `norm_fderiv_convexSetCutoff_le`, and
`norm_fderiv_convexSetCutoff_sub_le`.

This is the setwise form of Lemma 2.1 in Bentkus (2004), combined with the cutoff of Lemma 2.2, equation (2.2), printed p. 402. The paper takes the outer neighborhood \{d_A\le\varepsilon\} and defines its inner neighborhood using a closed ball. The formal inner core instead uses an open ball, equivalently the complement of the open \varepsilon-thickening of A^c; this keeps the equality boundary in the displayed inner shell. Empty and nonclosed convex sets are handled by the total cutoff and \overline A explicitly.