2.8. Taylor remainders and angle splitting🔗

Lemma2.8.1

uses 0used by 1✓L∃∀N

Tagsbentkusgaussian-replacementtaylorsource-bentkus-2004fidelity-sharp-quadratic-remainder

First-order and two-shift Taylor remainders. Let E be a real normed vector space, let f:E\to\mathbb R be continuously differentiable, and suppose that Df is L-Lipschitz. Then |f(x+h)-f(x)-Df(x)[h]|\le\frac L2\|h\|^2. For two shifts v,w\in E, freezing the derivative at x gives \left|(f(x+v+w)-f(x+v))-Df(x)[w]\right| \le L\|w\|\left(\|v\|+\frac{\|w\|}{2}\right).

Lean code for Lemma2.8.1●2 theorems

theoremdefined in ProbabilityApproximation/Bentkus/TaylorRemainder.lean

complete

theorem ProbabilityTheory.abs_firstOrderTaylorRemainder_le.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ)
  (hf : ContDiff ℝ 1 f) {L : NNReal}
  (hLip : LipschitzWith L (fderiv ℝ f)) (x h : E) :
  |f (x + h) - f x - (fderiv ℝ f x) h| ≤ ↑L / 2 * ‖h‖ ^ 2

theorem ProbabilityTheory.abs_firstOrderTaylorRemainder_le.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] (f : E → ℝ)
  (hf : ContDiff ℝ 1 f) {L : NNReal}
  (hLip : LipschitzWith L (fderiv ℝ f))
  (x h : E) :
  |f (x + h) - f x - (fderiv ℝ f x) h| ≤
    ↑L / 2 * ‖h‖ ^ 2

First-order Taylor's theorem with the `L / 2` quadratic remainder for a scalar function with
globally Lipschitz Fréchet derivative.

theoremdefined in ProbabilityApproximation/Bentkus/TaylorRemainder.lean

complete

theorem ProbabilityTheory.norm_twoShiftTaylorRemainder_le.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ)
  (hf : ContDiff ℝ 1 f) {L : NNReal}
  (hLip : LipschitzWith L (fderiv ℝ f)) (x v w : E) :
  ‖f (x + v + w) - f (x + v) - (fderiv ℝ f x) w‖ ≤
    ↑L * ‖w‖ * (‖v‖ + ‖w‖ / 2)

theorem ProbabilityTheory.norm_twoShiftTaylorRemainder_le.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] (f : E → ℝ)
  (hf : ContDiff ℝ 1 f) {L : NNReal}
  (hLip : LipschitzWith L (fderiv ℝ f))
  (x v w : E) :
  ‖f (x + v + w) - f (x + v) -
        (fderiv ℝ f x) w‖ ≤
    ↑L * ‖w‖ * (‖v‖ + ‖w‖ / 2)

Two-shift Taylor remainder with the derivative frozen at the original base point.  This is
the cancellation-friendly form of Bentkus's expansion (3.28).

This is the integral Taylor estimate used in Bentkus (2004), equation (3.28), printed p. 407, before the centering and covariance cancellations are applied. The first inequality keeps the exact 1/2 obtained by integrating the linear derivative increment.

Theorem2.8.2

uses 1used by 1✓L∃∀N

Tagsbentkusgaussian-analysisgaussian-replacementtaylorsource-bentkus-2004fidelity-explicit-dimension-free-remainder

Integrated second-order remainder for the first Gaussian-density derivative. Let \rho be the standard Gaussian density on \mathbb R^d, and let \varphi:\mathbb R^d\to\mathbb R be measurable with |\varphi|\le1. For all a,w,g\in\mathbb R^d, \left|\int\varphi(x)D^3\rho(x-a)[w,w,g],dx\right| \le(3+\sqrt{m_4})\|w\|^2\|g\|, where m_4=\int t^4\,dN(0,1)(t). Consequently, for every h,g\in\mathbb R^d, \begin{aligned} \bigg|\int\varphi(x)\big(&D\rho(x-h)[g]-D\rho(x)[g]\\ &+D^2\rho(x)[h,g]\big)\,dx\bigg| \le\frac{3+\sqrt{m_4}}2\|h\|^2\|g\|. \end{aligned}

Lean code for Theorem2.8.2●4 theorems

theoremdefined in ProbabilityApproximation/Bentkus/Induction/GaussianDensityComparison.lean

complete

theorem ProbabilityTheory.integral_abs_standardGaussianDensityD3_volume_le
  {d : ℕ} (w g : EuclideanSpace ℝ (Fin d)) :
  ∫ (x : EuclideanSpace ℝ (Fin d)),
      |ProbabilityTheory.standardGaussianDensityD3 x w w g| ≤
    (3 + √ProbabilityTheory.standardGaussianFourthMoment) * ‖w‖ ^ 2 *
      ‖g‖

theorem ProbabilityTheory.integral_abs_standardGaussianDensityD3_volume_le
  {d : ℕ}
  (w g : EuclideanSpace ℝ (Fin d)) :
  ∫ (x : EuclideanSpace ℝ (Fin d)),
      |ProbabilityTheory.standardGaussianDensityD3
          x w w g| ≤
    (3 +
          √ProbabilityTheory.standardGaussianFourthMoment) *
        ‖w‖ ^ 2 *
      ‖g‖

The absolute third directional derivative of the standard Gaussian density has the same
dimension-free integral bound as its cubic Hermite contraction.

theoremdefined in ProbabilityApproximation/Bentkus/Induction/GaussianDensityComparison.lean

complete

theorem ProbabilityTheory.integrable_standardGaussianDensityD3_volume {d : ℕ}
  (w g : EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.Integrable
    (fun x => ProbabilityTheory.standardGaussianDensityD3 x w w g)
    MeasureTheory.volume

theorem ProbabilityTheory.integrable_standardGaussianDensityD3_volume
  {d : ℕ}
  (w g : EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.Integrable
    (fun x =>
      ProbabilityTheory.standardGaussianDensityD3
        x w w g)
    MeasureTheory.volume

theoremdefined in ProbabilityApproximation/Bentkus/Induction/GaussianDensityComparison.lean

complete

theorem ProbabilityTheory.bentkus_abs_integral_bounded_mul_standardGaussianDensityD3_sub_le
  {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ}
  (hφm : MeasureTheory.AEStronglyMeasurable φ MeasureTheory.volume)
  (hφ : ∀ (x : EuclideanSpace ℝ (Fin d)), |φ x| ≤ 1)
  (a w g : EuclideanSpace ℝ (Fin d)) :
  |∫ (x : EuclideanSpace ℝ (Fin d)),
        φ x *
          ProbabilityTheory.standardGaussianDensityD3 (x - a) w w g| ≤
    (3 + √ProbabilityTheory.standardGaussianFourthMoment) * ‖w‖ ^ 2 *
      ‖g‖

theorem ProbabilityTheory.bentkus_abs_integral_bounded_mul_standardGaussianDensityD3_sub_le
  {d : ℕ}
  {φ : EuclideanSpace ℝ (Fin d) → ℝ}
  (hφm :
    MeasureTheory.AEStronglyMeasurable φ
      MeasureTheory.volume)
  (hφ :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      |φ x| ≤ 1)
  (a w g : EuclideanSpace ℝ (Fin d)) :
  |∫ (x : EuclideanSpace ℝ (Fin d)),
        φ x *
          ProbabilityTheory.standardGaussianDensityD3
            (x - a) w w g| ≤
    (3 +
          √ProbabilityTheory.standardGaussianFourthMoment) *
        ‖w‖ ^ 2 *
      ‖g‖

Bentkus (3.20)--(3.22): multiplying a translated third Gaussian-density contraction by an
arbitrary measurable factor of absolute value at most one costs no more than the universal cubic
Hermite-contraction constant.

theoremdefined in ProbabilityApproximation/Bentkus/Induction/GaussianDensityComparison.lean

complete

theorem ProbabilityTheory.bentkus_standardGaussianDensityD1_secondOrderRemainder_integral_bound
  {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφm : Measurable φ)
  (hφ : ∀ (x : EuclideanSpace ℝ (Fin d)), |φ x| ≤ 1)
  (h g : EuclideanSpace ℝ (Fin d)) :
  |∫ (x : EuclideanSpace ℝ (Fin d)),
        φ x *
          (ProbabilityTheory.standardGaussianDensityD1 (x - h) g -
              ProbabilityTheory.standardGaussianDensityD1 x g +
            ProbabilityTheory.standardGaussianDensityD2 x h g)| ≤
    (3 + √ProbabilityTheory.standardGaussianFourthMoment) / 2 *
        ‖h‖ ^ 2 *
      ‖g‖

theorem ProbabilityTheory.bentkus_standardGaussianDensityD1_secondOrderRemainder_integral_bound
  {d : ℕ}
  {φ : EuclideanSpace ℝ (Fin d) → ℝ}
  (hφm : Measurable φ)
  (hφ :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      |φ x| ≤ 1)
  (h g : EuclideanSpace ℝ (Fin d)) :
  |∫ (x : EuclideanSpace ℝ (Fin d)),
        φ x *
          (ProbabilityTheory.standardGaussianDensityD1
                (x - h) g -
              ProbabilityTheory.standardGaussianDensityD1
                x g +
            ProbabilityTheory.standardGaussianDensityD2
              x h g)| ≤
    (3 +
            √ProbabilityTheory.standardGaussianFourthMoment) /
          2 *
        ‖h‖ ^ 2 *
      ‖g‖

Bentkus (3.19)--(3.23): after the constant, linear, and quadratic terms cancel, the translated
first Gaussian-density contraction has an integrated second-order remainder bounded by one half
of the universal cubic Hermite-contraction constant.

This is the cancellation-ready Taylor estimate in Bentkus (2004), equations (3.19)--(3.23), printed pp. 405--406. The factor 1/2 is the integral of the second-order Taylor kernel, while the dimension-free constant is the absolute cubic Hermite contraction.

Lemma2.8.3

uses 0

Used by 2

Reverse dependency previews

Preview

Lemma 2.8.4

Loading preview

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

✓L∃∀N

Tagsbentkusgaussian-replacementinductionangle-splittingsource-bentkus-2004fidelity-exact-antiderivatives-and-arcsine-substitution

Exact trigonometric integrals for Bentkus's angle split. If 0<\gamma\le\pi/2, then \int_\gamma^{\pi/2}\frac{\cos\alpha}{\sin^2\alpha}\,d\alpha =\frac1{\sin\gamma}-1 \le\frac1{\sin\gamma}. Consequently, if 0<\varepsilon\le1 and \gamma=\arcsin\varepsilon, then \int_{\arcsin\varepsilon}^{\pi/2} \frac{\cos\alpha}{\sin^2\alpha}\,d\alpha =\varepsilon^{-1}-1. For 0\le\varepsilon\le1, the complementary small-angle mass is exactly \int_0^{\arcsin\varepsilon}\cos\alpha\,d\alpha=\varepsilon.

Lean code for Lemma2.8.3●4 theorems

theoremdefined in ProbabilityApproximation/Bentkus/AngleCalculus.lean

complete

theorem ProbabilityTheory.intervalIntegral_cos_div_sin_sq {γ : ℝ} (hγ : 0 < γ)
  (hγpi : γ ≤ Real.pi / 2) :
  ∫ (α : ℝ) in γ..Real.pi / 2, Real.cos α / Real.sin α ^ 2 =
    (Real.sin γ)⁻¹ - 1

theorem ProbabilityTheory.intervalIntegral_cos_div_sin_sq
  {γ : ℝ} (hγ : 0 < γ)
  (hγpi : γ ≤ Real.pi / 2) :
  ∫ (α : ℝ) in γ..Real.pi / 2,
      Real.cos α / Real.sin α ^ 2 =
    (Real.sin γ)⁻¹ - 1

The exact large-angle integral in Bentkus (2004), equations (3.13)--(3.14).

theoremdefined in ProbabilityApproximation/Bentkus/AngleCalculus.lean

complete

theorem ProbabilityTheory.intervalIntegral_cos_div_sin_sq_le_inv {γ : ℝ}
  (hγ : 0 < γ) (hγpi : γ ≤ Real.pi / 2) :
  ∫ (α : ℝ) in γ..Real.pi / 2, Real.cos α / Real.sin α ^ 2 ≤
    (Real.sin γ)⁻¹

theorem ProbabilityTheory.intervalIntegral_cos_div_sin_sq_le_inv
  {γ : ℝ} (hγ : 0 < γ)
  (hγpi : γ ≤ Real.pi / 2) :
  ∫ (α : ℝ) in γ..Real.pi / 2,
      Real.cos α / Real.sin α ^ 2 ≤
    (Real.sin γ)⁻¹

The large-angle integral is at most the reciprocal of its lower-end sine.

theoremdefined in ProbabilityApproximation/Bentkus/AngleCalculus.lean

complete

theorem ProbabilityTheory.intervalIntegral_cos_div_sin_sq_arcsin {ε : ℝ}
  (hε : 0 < ε) (hε1 : ε ≤ 1) :
  ∫ (α : ℝ) in Real.arcsin ε..Real.pi / 2, Real.cos α / Real.sin α ^ 2 =
    ε⁻¹ - 1

theorem ProbabilityTheory.intervalIntegral_cos_div_sin_sq_arcsin
  {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) :
  ∫ (α : ℝ) in Real.arcsin ε..Real.pi / 2,
      Real.cos α / Real.sin α ^ 2 =
    ε⁻¹ - 1

With Bentkus's choice `γ = arcsin ε`, the exact large-angle integral is `ε⁻¹ - 1`.

theoremdefined in ProbabilityApproximation/Bentkus/AngleCalculus.lean

complete

theorem ProbabilityTheory.intervalIntegral_cos_zero_arcsin {ε : ℝ} (hε : 0 ≤ ε)
  (hε1 : ε ≤ 1) : ∫ (α : ℝ) in 0..Real.arcsin ε, Real.cos α = ε

theorem ProbabilityTheory.intervalIntegral_cos_zero_arcsin
  {ε : ℝ} (hε : 0 ≤ ε) (hε1 : ε ≤ 1) :
  ∫ (α : ℝ) in 0..Real.arcsin ε,
      Real.cos α =
    ε

The small-angle cosine mass becomes exactly `ε` at `γ = arcsin ε`.

Bentkus (2004), splits the rotation at \gamma in equations (3.11)--(3.15), printed pp. 404--405. In the proof of (3.13), the integral \int_0^\gamma\cos\alpha\,d\alpha occurs immediately after equation (3.33), printed p. 407. In the proof of (3.14), equations (3.39)--(3.40) are followed by the bound on \int_\gamma^{\pi/2}\cos\alpha/\sin^2\alpha\,d\alpha, printed p. 409. Bentkus chooses \sin\gamma=\varepsilon after equation (3.8), printed p. 404; the node retains the exact antiderivatives before taking the inequalities used in the paper.

Lemma2.8.4

uses 1used by 1✓L∃∀N

Tagsbentkusgaussian-replacementinductionangle-splittingscalar-assemblysource-bentkus-2004fidelity-explicit-constant-bookkeeping

Three-piece angle decomposition and coordinate summation. If F is interval-integrable on [0,\gamma] and [\gamma,b], and R is interval-integrable on [\gamma,b], then \int_0^bF =\int_0^\gamma F+ \int_\gamma^b(F-R)+ \int_\gamma^bR. For 0<\varepsilon\le1, if K\ge0 and |F(\alpha)|\le K\frac{\cos\alpha}{\sin^2\alpha} \quad\text{for }\alpha\in(\arcsin\varepsilon,\pi/2], then \left|\int_{\arcsin\varepsilon}^{\pi/2}F(\alpha)\,d\alpha\right| \le\frac K\varepsilon, \qquad \frac\pi2-\arcsin\varepsilon\le2. Suppose a coordinate contribution satisfies T=S+L+R and, for nonnegative d_{1/4},q,\beta_k,K_L,K_R, |S|\le K_Sd_{1/4}(1+q)\beta_k,\quad |L|\le K_Ld_{1/4}q\beta_k,\quad |R|\le K_Rd_{1/4}\beta_k. Then |T|\le(K_S+K_L+K_R)d_{1/4}(1+q)\beta_k. Moreover, if \beta=\sum_k\beta_k, \varepsilon>0, and |T_k|\le Kd_{1/4} \left(1+\frac{C\beta}{\varepsilon}\right)\beta_k, then \left|\sum_kT_k\right| \le Kd_{1/4}\left(\beta+\frac{C\beta^2}{\varepsilon}\right). Deleting one nonnegative coordinate cannot increase the corresponding finite sum: \sum_{i\ne k}\beta_i\le\sum_i\beta_i.

Lean code for Lemma2.8.4●6 theorems

theoremdefined in ProbabilityApproximation/Bentkus/AngleCalculus.lean

complete

theorem ProbabilityTheory.pi_div_two_sub_arcsin_le_two {ε : ℝ} (hε : 0 ≤ ε) :
  Real.pi / 2 - Real.arcsin ε ≤ 2

theorem ProbabilityTheory.pi_div_two_sub_arcsin_le_two
  {ε : ℝ} (hε : 0 ≤ ε) :
  Real.pi / 2 - Real.arcsin ε ≤ 2

The Gaussian-reference part of Bentkus's angle split has length at most two.

theoremdefined in ProbabilityApproximation/Bentkus/AngleCalculus.lean

complete

theorem ProbabilityTheory.intervalIntegral_eq_small_add_difference_add_reference
  {F R : ℝ → ℝ} {γ b : ℝ}
  (hF0γ : IntervalIntegrable F MeasureTheory.volume 0 γ)
  (hFγb : IntervalIntegrable F MeasureTheory.volume γ b)
  (hRγb : IntervalIntegrable R MeasureTheory.volume γ b) :
  ∫ (α : ℝ) in 0..b, F α =
    ((∫ (α : ℝ) in 0..γ, F α) + ∫ (α : ℝ) in γ..b, F α - R α) +
      ∫ (α : ℝ) in γ..b, R α

theorem ProbabilityTheory.intervalIntegral_eq_small_add_difference_add_reference
  {F R : ℝ → ℝ} {γ b : ℝ}
  (hF0γ :
    IntervalIntegrable F
      MeasureTheory.volume 0 γ)
  (hFγb :
    IntervalIntegrable F
      MeasureTheory.volume γ b)
  (hRγb :
    IntervalIntegrable R
      MeasureTheory.volume γ b) :
  ∫ (α : ℝ) in 0..b, F α =
    ((∫ (α : ℝ) in 0..γ, F α) +
        ∫ (α : ℝ) in γ..b, F α - R α) +
      ∫ (α : ℝ) in γ..b, R α

Exact three-piece decomposition at an intermediate angle: the initial actual contribution,
the later actual-minus-reference contribution, and the later reference contribution.

theoremdefined in ProbabilityApproximation/Bentkus/AngleCalculus.lean

complete

theorem ProbabilityTheory.bentkus_largeAngle_integral_le_of_cos_div_sin_sq_envelope
  {ε K : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hK : 0 ≤ K) {F : ℝ → ℝ}
  (hF :
    ∀ α ∈ Set.Ioc (Real.arcsin ε) (Real.pi / 2),
      |F α| ≤ K * (Real.cos α / Real.sin α ^ 2)) :
  |∫ (α : ℝ) in Real.arcsin ε..Real.pi / 2, F α| ≤ K / ε

theorem ProbabilityTheory.bentkus_largeAngle_integral_le_of_cos_div_sin_sq_envelope
  {ε K : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1)
  (hK : 0 ≤ K) {F : ℝ → ℝ}
  (hF :
    ∀
      α ∈
        Set.Ioc (Real.arcsin ε)
          (Real.pi / 2),
      |F α| ≤
        K *
          (Real.cos α / Real.sin α ^ 2)) :
  |∫ (α : ℝ) in
        Real.arcsin ε..Real.pi / 2, F α| ≤
    K / ε

Integrating a Bentkus large-angle envelope from `arcsin ε` costs at most one factor
of `ε⁻¹`.

theoremdefined in ProbabilityApproximation/Bentkus/ParameterClosure.lean

complete

theorem ProbabilityTheory.bentkus_coordinate_bounds_sum {n : ℕ}
  {T βk : Fin n → ℝ} {K d14 C β ε : ℝ} (hβ : β = ∑ k, βk k) (hε : 0 < ε)
  (hcoord : ∀ (k : Fin n), |T k| ≤ K * d14 * (1 + C * β / ε) * βk k) :
  |∑ k, T k| ≤ K * d14 * (β + C * β ^ 2 / ε)

theorem ProbabilityTheory.bentkus_coordinate_bounds_sum
  {n : ℕ} {T βk : Fin n → ℝ}
  {K d14 C β ε : ℝ} (hβ : β = ∑ k, βk k)
  (hε : 0 < ε)
  (hcoord :
    ∀ (k : Fin n),
      |T k| ≤
        K * d14 * (1 + C * β / ε) *
          βk k) :
  |∑ k, T k| ≤
    K * d14 * (β + C * β ^ 2 / ε)

Summing the coordinatewise replacement estimates converts the factor
`1 + C * β / ε` into Bentkus's smooth-error expression
`β + C * β² / ε`.

theoremdefined in ProbabilityApproximation/Bentkus/ParameterClosure.lean

complete

theorem ProbabilityTheory.fin_sum_succAbove_le_sum_univ {n : ℕ}
  (k : Fin (n + 1)) (f : Fin (n + 1) → ℝ)
  (hf : ∀ (i : Fin (n + 1)), 0 ≤ f i) :
  ∑ i, f (k.succAbove i) ≤ ∑ i, f i

theorem ProbabilityTheory.fin_sum_succAbove_le_sum_univ
  {n : ℕ} (k : Fin (n + 1))
  (f : Fin (n + 1) → ℝ)
  (hf : ∀ (i : Fin (n + 1)), 0 ≤ f i) :
  ∑ i, f (k.succAbove i) ≤ ∑ i, f i

Removing one nonnegative coordinate from a finite sum can only decrease the sum.

theoremdefined in ProbabilityApproximation/Bentkus/ParameterClosure.lean

complete

theorem ProbabilityTheory.bentkus_three_coordinate_pieces
  {S L R T Ks Kl Kr d14 q βk : ℝ} (hKl : 0 ≤ Kl) (hKr : 0 ≤ Kr)
  (hd : 0 ≤ d14) (hq : 0 ≤ q) (hβk : 0 ≤ βk) (hT : T = S + L + R)
  (hS : |S| ≤ Ks * d14 * (1 + q) * βk) (hL : |L| ≤ Kl * d14 * q * βk)
  (hR : |R| ≤ Kr * d14 * βk) : |T| ≤ (Ks + Kl + Kr) * d14 * (1 + q) * βk

theorem ProbabilityTheory.bentkus_three_coordinate_pieces
  {S L R T Ks Kl Kr d14 q βk : ℝ}
  (hKl : 0 ≤ Kl) (hKr : 0 ≤ Kr)
  (hd : 0 ≤ d14) (hq : 0 ≤ q)
  (hβk : 0 ≤ βk) (hT : T = S + L + R)
  (hS : |S| ≤ Ks * d14 * (1 + q) * βk)
  (hL : |L| ≤ Kl * d14 * q * βk)
  (hR : |R| ≤ Kr * d14 * βk) :
  |T| ≤
    (Ks + Kl + Kr) * d14 * (1 + q) * βk

The small-angle term, the large-angle comparison, and the Gaussian reference term share one
coordinate envelope after enlarging each nonnegative coefficient by `1 + q`.

This is the scalar assembly behind Bentkus (2004), Section 3, printed p. 404. The small-angle, large-angle difference, and Gaussian-reference estimates are equations (3.13)--(3.15); they combine to equation (3.6), summation over coordinates gives equation (3.7), and insertion into the smoothing inequality gives equations (3.8)--(3.9). The displayed decomposition and omitted-coordinate inequality make explicit the bookkeeping compressed in the paper.

Lemma2.8.5

uses 0used by 1✓L∃∀N

Tagsbentkusgaussian-replacementinductionscalar-closuresource-bentkus-2004fidelity-exact-smoothing-scale

Closure of the smoothing parameter. Let C\ge1, d\ge1, \beta>0, and \Delta\le1. Suppose K(2\sqrt C+1)\le C and, whenever \beta\sqrt C<1, \Delta\le Kd^{1/4} \left(\beta\sqrt C+\beta+ \frac{C\beta^2}{\beta\sqrt C}\right). Then \Delta\le Cd^{1/4}\beta.

Lean code for Lemma2.8.5●1 theorem

theoremdefined in ProbabilityApproximation/Bentkus/ParameterClosure.lean

complete

theorem ProbabilityTheory.bentkus_parameter_closure {K C d β Δ : ℝ} (hC : 1 ≤ C)
  (hKC : K * (2 * √C + 1) ≤ C) (hd : 1 ≤ d) (hβ : 0 < β) (hΔ1 : Δ ≤ 1)
  (hmain :
    β * √C < 1 →
      Δ ≤ K * d ^ (1 / 4) * (β * √C + β + C * β ^ 2 / (β * √C))) :
  Δ ≤ C * d ^ (1 / 4) * β

theorem ProbabilityTheory.bentkus_parameter_closure
  {K C d β Δ : ℝ} (hC : 1 ≤ C)
  (hKC : K * (2 * √C + 1) ≤ C)
  (hd : 1 ≤ d) (hβ : 0 < β) (hΔ1 : Δ ≤ 1)
  (hmain :
    β * √C < 1 →
      Δ ≤
        K * d ^ (1 / 4) *
          (β * √C + β +
            C * β ^ 2 / (β * √C))) :
  Δ ≤ C * d ^ (1 / 4) * β

The parameter choice `ε = β * sqrt C` closes Bentkus's induction once the absolute constant
dominates the coefficient in the Taylor estimate.

This is the scalar calculation in Bentkus (2004), equations (3.9)--(3.10), printed p. 404. It chooses \varepsilon=\beta\sqrt C; the complementary branch \varepsilon\ge1 closes directly from \Delta\le1.