Berry–Esseen Bounds for Independent Sums

2.1. Convex distance and smooth cutoffs🔗

Lemma2.1.1
uses 0
Used by 2
Reverse dependency previews
Preview
Lemma 2.4.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbentkusconvex-geometryparallel-setssource-bentkus-2004fidelity-generalized-radii

Convex parallel sets. If A\subseteq\mathbb R^d is convex, then its open parallel set A^\varepsilon is convex for every \varepsilon\in\mathbb R; its closed parallel set \{x:d_A(x)\le\varepsilon\} is convex whenever \varepsilon\ge0. Both parallel sets are measurable, and for every v\in\mathbb R^d, (v+A)^\varepsilon=v+A^\varepsilon with the analogous identity for closed parallel sets.

Lean code for Lemma2.1.1●6 theorems
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/ParallelSets.lean
    complete
    theorem ProbabilityTheory.thickening_isConvexSet {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  (r : ℝ) : Convexity.IsConvexSet ℝ (Metric.thickening r s)
    theorem ProbabilityTheory.thickening_isConvexSet
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s)
  (r : ℝ) :
  Convexity.IsConvexSet ℝ
    (Metric.thickening r s)
    The open metric thickening of a convex Euclidean set is convex.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/ParallelSets.lean
    complete
    theorem ProbabilityTheory.cthickening_isConvexSet {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {r : ℝ} (hr : 0 ≤ r) :
  Convexity.IsConvexSet ℝ (Metric.cthickening r s)
    theorem ProbabilityTheory.cthickening_isConvexSet
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {r : ℝ}
  (hr : 0 ≤ r) :
  Convexity.IsConvexSet ℝ
    (Metric.cthickening r s)
    A nonnegative-radius closed metric thickening of a convex Euclidean set is convex.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/ParallelSets.lean
    complete
    theorem ProbabilityTheory.measurableSet_thickening {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (r : ℝ) :
  MeasurableSet (Metric.thickening r s)
    theorem ProbabilityTheory.measurableSet_thickening
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (r : ℝ) :
  MeasurableSet (Metric.thickening r s)
    Open Euclidean thickenings are measurable.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/ParallelSets.lean
    complete
    theorem ProbabilityTheory.measurableSet_cthickening {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (r : ℝ) :
  MeasurableSet (Metric.cthickening r s)
    theorem ProbabilityTheory.measurableSet_cthickening
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (r : ℝ) :
  MeasurableSet (Metric.cthickening r s)
    Closed Euclidean thickenings are measurable.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/ParallelSets.lean
    complete
    theorem ProbabilityTheory.thickening_vadd {d : ℕ} (a : EuclideanSpace ℝ (Fin d))
  (r : ℝ) (s : Set (EuclideanSpace ℝ (Fin d))) :
  Metric.thickening r (a +ᵥ s) = a +ᵥ Metric.thickening r s
    theorem ProbabilityTheory.thickening_vadd {d : ℕ}
  (a : EuclideanSpace ℝ (Fin d)) (r : ℝ)
  (s : Set (EuclideanSpace ℝ (Fin d))) :
  Metric.thickening r (a +ᵥ s) =
    a +ᵥ Metric.thickening r s
    Open thickening commutes with Euclidean translation.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/ParallelSets.lean
    complete
    theorem ProbabilityTheory.cthickening_vadd {d : ℕ}
  (a : EuclideanSpace ℝ (Fin d)) (r : ℝ)
  (s : Set (EuclideanSpace ℝ (Fin d))) :
  Metric.cthickening r (a +ᵥ s) = a +ᵥ Metric.cthickening r s
    theorem ProbabilityTheory.cthickening_vadd {d : ℕ}
  (a : EuclideanSpace ℝ (Fin d)) (r : ℝ)
  (s : Set (EuclideanSpace ℝ (Fin d))) :
  Metric.cthickening r (a +ᵥ s) =
    a +ᵥ Metric.cthickening r s
    Closed thickening commutes with Euclidean translation.

These are the set-theoretic facts used in Bentkus (2004), condition (ii) and the neighborhood notation preceding Theorem 1.2, printed pp. 401--402. The formal open-thickening theorem is harmlessly generalized to all real radii.

Theorem2.1.2
uses 0used by 1✓L∃∀N
Tagsbentkusconvex-geometryprojectionsource-bentkus-2003fidelity-exact

Metric projection onto a closed convex set. Let A\subseteq\mathbb R^d be nonempty, closed, and convex. For every x there is a unique point p_A(x)\in A such that \|x-p_A(x)\|=d_A(x). It satisfies \langle x-p_A(x),a-p_A(x)\rangle\le0\quad(a\in A) and, for all x,y, \|p_A(x)-p_A(y)\|^2 \le\langle x-y,p_A(x)-p_A(y)\rangle. Consequently both p_A and the residual map x\mapsto x-p_A(x) are 1-Lipschitz.

Lean code for Theorem2.1.2●6 declarations
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/MetricProjection.lean
    complete
    theorem ProbabilityTheory.existsUnique_isNearestPoint {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s)
  (x : EuclideanSpace ℝ (Fin d)) :
  ∃! p, ProbabilityTheory.IsNearestPoint s x p
    theorem ProbabilityTheory.existsUnique_isNearestPoint
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  (x : EuclideanSpace ℝ (Fin d)) :
  ∃! p,
    ProbabilityTheory.IsNearestPoint s x p
    A nonempty closed convex Euclidean set has a unique nearest point to every point.
  • defdefined in ProbabilityApproximation/ConvexGeometry/MetricProjection.lean
    complete
    def ProbabilityTheory.metricProjection {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (hclosed : IsClosed s)
  (hne : s.Nonempty) (x : EuclideanSpace ℝ (Fin d)) :
  EuclideanSpace ℝ (Fin d)
    def ProbabilityTheory.metricProjection {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (x : EuclideanSpace ℝ (Fin d)) :
  EuclideanSpace ℝ (Fin d)
    The selected nearest point in a nonempty closed Euclidean set.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/MetricProjection.lean
    complete
    theorem ProbabilityTheory.metricProjection_variational {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s)
  (x : EuclideanSpace ℝ (Fin d)) {z : EuclideanSpace ℝ (Fin d)}
  (hz : z ∈ s) :
  inner ℝ (x - ProbabilityTheory.metricProjection s hclosed hne x)
      (z - ProbabilityTheory.metricProjection s hclosed hne x) ≤
    0
    theorem ProbabilityTheory.metricProjection_variational
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  (x : EuclideanSpace ℝ (Fin d))
  {z : EuclideanSpace ℝ (Fin d)}
  (hz : z ∈ s) :
  inner ℝ
      (x -
        ProbabilityTheory.metricProjection
          s hclosed hne x)
      (z -
        ProbabilityTheory.metricProjection
          s hclosed hne x) ≤
    0
    The selected projection onto a closed convex set satisfies the variational inequality.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/MetricProjection.lean
    complete
    theorem ProbabilityTheory.metricProjection_firmlyNonexpansive {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ‖ProbabilityTheory.metricProjection s hclosed hne x -
          ProbabilityTheory.metricProjection s hclosed hne y‖ ^
      2 ≤
    inner ℝ (x - y)
      (ProbabilityTheory.metricProjection s hclosed hne x -
        ProbabilityTheory.metricProjection s hclosed hne y)
    theorem ProbabilityTheory.metricProjection_firmlyNonexpansive
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ‖ProbabilityTheory.metricProjection s
            hclosed hne x -
          ProbabilityTheory.metricProjection
            s hclosed hne y‖ ^
      2 ≤
    inner ℝ (x - y)
      (ProbabilityTheory.metricProjection
          s hclosed hne x -
        ProbabilityTheory.metricProjection
          s hclosed hne y)
    Metric projection satisfies the firm nonexpansiveness inequality.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/MetricProjection.lean
    complete
    theorem ProbabilityTheory.metricProjection_lipschitzWith {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s) :
  LipschitzWith 1 (ProbabilityTheory.metricProjection s hclosed hne)
    theorem ProbabilityTheory.metricProjection_lipschitzWith
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s) :
  LipschitzWith 1
    (ProbabilityTheory.metricProjection s
      hclosed hne)
    Metric projection onto a closed convex Euclidean set is `1`-Lipschitz.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/MetricProjection.lean
    complete
    theorem ProbabilityTheory.metricProjection_residual_lipschitzWith {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s) :
  LipschitzWith 1 fun x =>
    x - ProbabilityTheory.metricProjection s hclosed hne x
    theorem ProbabilityTheory.metricProjection_residual_lipschitzWith
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s) :
  LipschitzWith 1 fun x =>
    x -
      ProbabilityTheory.metricProjection s
        hclosed hne x
    The residual from a point to its metric projection is also `1`-Lipschitz.

This packages the Euclidean projection geometry used in Bentkus (2003), Lemma 2.2, printed pp. 389--390. The paper states the resulting distance-gradient inequalities; the projection formulation records the complete geometric mechanism used by the formal proof.

Theorem2.1.3
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 2.1.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbentkusconvex-geometrydistancesource-bentkus-2003fidelity-explicit-frechet-form

Differentiability of distance to a convex set. Under the hypotheses of the preceding node, for every x,h\in\mathbb R^d, \left|d_A(x+h)^2-d_A(x)^2 -2\langle x-p_A(x),h\rangle\right|\le3\|h\|^2. Thus d_A^2 is Fréchet differentiable everywhere with D(d_A^2)(x)[h]=2\langle x-p_A(x),h\rangle. If x\notin A, then d_A is Fréchet differentiable at x, Dd_A(x)[h] =\left\langle\frac{x-p_A(x)}{d_A(x)},h\right\rangle, \qquad \|Dd_A(x)\|=1.

Lean code for Theorem2.1.3●4 theorems
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/SquaredDistance.lean
    complete
    theorem ProbabilityTheory.squaredInfDist_remainder_bound {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s)
  (x h : EuclideanSpace ℝ (Fin d)) :
  |Metric.infDist (x + h) s ^ 2 - Metric.infDist x s ^ 2 -
        2 *
          inner ℝ
            (x - ProbabilityTheory.metricProjection s hclosed hne x)
            h| ≤
    3 * ‖h‖ ^ 2
    theorem ProbabilityTheory.squaredInfDist_remainder_bound
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  (x h : EuclideanSpace ℝ (Fin d)) :
  |Metric.infDist (x + h) s ^ 2 -
          Metric.infDist x s ^ 2 -
        2 *
          inner ℝ
            (x -
              ProbabilityTheory.metricProjection
                s hclosed hne x)
            h| ≤
    3 * ‖h‖ ^ 2
    Squared distance differs from its first-order projection expansion by a quadratic remainder.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/SquaredDistance.lean
    complete
    theorem ProbabilityTheory.hasFDerivAt_squaredInfDist {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s)
  (x : EuclideanSpace ℝ (Fin d)) :
  HasFDerivAt (fun y => Metric.infDist y s ^ 2)
    (2 •
      (innerSL ℝ)
        (x - ProbabilityTheory.metricProjection s hclosed hne x))
    x
    theorem ProbabilityTheory.hasFDerivAt_squaredInfDist
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  (x : EuclideanSpace ℝ (Fin d)) :
  HasFDerivAt
    (fun y => Metric.infDist y s ^ 2)
    (2 •
      (innerSL ℝ)
        (x -
          ProbabilityTheory.metricProjection
            s hclosed hne x))
    x
    The squared distance to a nonempty closed convex Euclidean set is Fréchet differentiable,
with gradient twice the residual from the metric projection.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/SquaredDistance.lean
    complete
    theorem ProbabilityTheory.hasFDerivAt_infDist_of_notMem {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s)
  {x : EuclideanSpace ℝ (Fin d)} (hx : x ∉ s) :
  HasFDerivAt (fun y => Metric.infDist y s)
    ((Metric.infDist x s)⁻¹ •
      (innerSL ℝ)
        (x - ProbabilityTheory.metricProjection s hclosed hne x))
    x
    theorem ProbabilityTheory.hasFDerivAt_infDist_of_notMem
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  {x : EuclideanSpace ℝ (Fin d)}
  (hx : x ∉ s) :
  HasFDerivAt
    (fun y => Metric.infDist y s)
    ((Metric.infDist x s)⁻¹ •
      (innerSL ℝ)
        (x -
          ProbabilityTheory.metricProjection
            s hclosed hne x))
    x
    Away from a nonempty closed convex set, distance is Fréchet differentiable in the normalized
metric-projection residual direction.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/SquaredDistance.lean
    complete
    theorem ProbabilityTheory.norm_fderiv_infDist_of_notMem {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s)
  {x : EuclideanSpace ℝ (Fin d)} (hx : x ∉ s) :
  ‖fderiv ℝ (fun y => Metric.infDist y s) x‖ = 1
    theorem ProbabilityTheory.norm_fderiv_infDist_of_notMem
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  {x : EuclideanSpace ℝ (Fin d)}
  (hx : x ∉ s) :
  ‖fderiv ℝ (fun y => Metric.infDist y s)
        x‖ =
    1
    Outside the set, the Fréchet derivative of distance has operator norm one.

This is the distance calculus behind Lemma 2.2, equations (2.5)--(2.9), of Bentkus (2003), printed pp. 389--390. The formal statement makes the derivative a bounded linear functional and supplies an explicit quadratic remainder.

Theorem2.1.4
uses 1used by 1✓L∃∀N
Tagsbentkusconvex-geometrysmoothingsource-bentkus-2003source-bentkus-2004fidelity-exact-constants

Bentkus's continuously differentiable distance cutoff. Let A\subseteq\mathbb R^d be nonempty, closed, and convex, and let \varepsilon>0. There is a continuously differentiable function \varphi_{\varepsilon,A}:\mathbb R^d\to[0,1] of the form \varphi_{\varepsilon,A}(x)=\psi(d_A(x)/\varepsilon) such that \varphi_{\varepsilon,A}=1\ \hbox{on }A,\qquad \varphi_{\varepsilon,A}=0\ \hbox{when }d_A(x)\ge\varepsilon, and, for every x,y\in\mathbb R^d, \|D\varphi_{\varepsilon,A}(x)\|\le\frac2\varepsilon, \qquad \|D\varphi_{\varepsilon,A}(x)-D\varphi_{\varepsilon,A}(y)\| \le\frac{8}{\varepsilon^2}\|x-y\|.

Lean code for Theorem2.1.4●8 declarations
  • defdefined in ProbabilityApproximation/ConvexGeometry/SmoothCutoff.lean
    complete
    def ProbabilityTheory.bentkusProfile (t : ℝ) : ℝ
    def ProbabilityTheory.bentkusProfile (t : ℝ) :
  ℝ
    Bentkus's continuously differentiable scalar cutoff profile.
  • defdefined in ProbabilityApproximation/ConvexGeometry/SmoothCutoff.lean
    complete
    def ProbabilityTheory.bentkusCutoff {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (ε : ℝ)
  (x : EuclideanSpace ℝ (Fin d)) : ℝ
    def ProbabilityTheory.bentkusCutoff {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (ε : ℝ) (x : EuclideanSpace ℝ (Fin d)) :
  ℝ
    Bentkus's distance cutoff for a set at smoothing radius `ε`.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/SmoothCutoff.lean
    complete
    theorem ProbabilityTheory.hasFDerivAt_bentkusCutoff {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} {ε : ℝ} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s) (hε : 0 < ε)
  (x : EuclideanSpace ℝ (Fin d)) :
  HasFDerivAt (ProbabilityTheory.bentkusCutoff s ε)
    (ProbabilityTheory.bentkusCutoffFDeriv s ε hclosed hne x) x
    theorem ProbabilityTheory.hasFDerivAt_bentkusCutoff
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {ε : ℝ} (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  (hε : 0 < ε)
  (x : EuclideanSpace ℝ (Fin d)) :
  HasFDerivAt
    (ProbabilityTheory.bentkusCutoff s ε)
    (ProbabilityTheory.bentkusCutoffFDeriv
      s ε hclosed hne x)
    x
    The Bentkus cutoff is Fréchet differentiable everywhere.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/SmoothCutoff.lean
    complete
    theorem ProbabilityTheory.bentkusCutoff_eq_one_of_mem {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} {ε : ℝ}
  {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ s) :
  ProbabilityTheory.bentkusCutoff s ε x = 1
    theorem ProbabilityTheory.bentkusCutoff_eq_one_of_mem
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {ε : ℝ} {x : EuclideanSpace ℝ (Fin d)}
  (hx : x ∈ s) :
  ProbabilityTheory.bentkusCutoff s ε x =
    1
    The Bentkus cutoff equals one on the set.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/SmoothCutoff.lean
    complete
    theorem ProbabilityTheory.bentkusCutoff_eq_zero_of_le_infDist {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} {ε : ℝ} (hε : 0 < ε)
  {x : EuclideanSpace ℝ (Fin d)} (hx : ε ≤ Metric.infDist x s) :
  ProbabilityTheory.bentkusCutoff s ε x = 0
    theorem ProbabilityTheory.bentkusCutoff_eq_zero_of_le_infDist
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {ε : ℝ} (hε : 0 < ε)
  {x : EuclideanSpace ℝ (Fin d)}
  (hx : ε ≤ Metric.infDist x s) :
  ProbabilityTheory.bentkusCutoff s ε x =
    0
    The Bentkus cutoff vanishes when distance is at least `ε`; equality at the boundary is
included.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/SmoothCutoff.lean
    complete
    theorem ProbabilityTheory.norm_fderiv_bentkusCutoff_le {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} {ε : ℝ} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s) (hε : 0 < ε)
  (x : EuclideanSpace ℝ (Fin d)) :
  ‖fderiv ℝ (ProbabilityTheory.bentkusCutoff s ε) x‖ ≤ 2 / ε
    theorem ProbabilityTheory.norm_fderiv_bentkusCutoff_le
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {ε : ℝ} (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  (hε : 0 < ε)
  (x : EuclideanSpace ℝ (Fin d)) :
  ‖fderiv ℝ
        (ProbabilityTheory.bentkusCutoff s
          ε)
        x‖ ≤
    2 / ε
    The Fréchet derivative of the Bentkus cutoff has norm at most `2 / ε`.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/SmoothCutoff.lean
    complete
    theorem ProbabilityTheory.norm_fderiv_bentkusCutoff_sub_le {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} {ε : ℝ} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s) (hε : 0 < ε)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ‖fderiv ℝ (ProbabilityTheory.bentkusCutoff s ε) x -
        fderiv ℝ (ProbabilityTheory.bentkusCutoff s ε) y‖ ≤
    8 * ‖x - y‖ / ε ^ 2
    theorem ProbabilityTheory.norm_fderiv_bentkusCutoff_sub_le
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {ε : ℝ} (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  (hε : 0 < ε)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ‖fderiv ℝ
          (ProbabilityTheory.bentkusCutoff
            s ε)
          x -
        fderiv ℝ
          (ProbabilityTheory.bentkusCutoff
            s ε)
          y‖ ≤
    8 * ‖x - y‖ / ε ^ 2
    The derivative field of the Bentkus cutoff is `8 / ε²`-Lipschitz.
  • theoremdefined in ProbabilityApproximation/ConvexGeometry/SmoothCutoff.lean
    complete
    theorem ProbabilityTheory.contDiff_bentkusCutoff {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} {ε : ℝ} (hclosed : IsClosed s)
  (hne : s.Nonempty) (hconv : Convexity.IsConvexSet ℝ s) (hε : 0 < ε) :
  ContDiff ℝ 1 (ProbabilityTheory.bentkusCutoff s ε)
    theorem ProbabilityTheory.contDiff_bentkusCutoff
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {ε : ℝ} (hclosed : IsClosed s)
  (hne : s.Nonempty)
  (hconv : Convexity.IsConvexSet ℝ s)
  (hε : 0 < ε) :
  ContDiff ℝ 1
    (ProbabilityTheory.bentkusCutoff s ε)
    The Bentkus distance cutoff is continuously differentiable.

This is Lemma 2.3, equations (2.10)--(2.12), of Bentkus (2003), printed pp. 390--391, and the same cutoff imported in Bentkus (2004), Lemma 2.2, equation (2.2), printed p. 402. The formal profile is the paper's piecewise quadratic \psi; endpoint values are included explicitly.