GaussianLipschitzExponential: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Gaussian Lipschitz first moment and signed exponential domain
Sharp standard Gaussian concentration for every Lipschitz observable

Samplinglib mathematical lesson

Gaussian Lipschitz first moment and signed exponential domain

AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential.integrable_and_integrable_exp_centered_of_lipschitz · theorem · Teaching coverage

Read this first

Mathematical statement

For every actual Gaussian mu and globally L-Lipschitz scalar f on the stated Banach/Borel space, f is Bochner integrable and exp(t*(f-int f dmu)) is integrable for every real t. This is a Gaussian-domain background theorem, not the sharp concentration bound.

\[f\in L^1(\mu),\qquad e^{t(f-\int f\,d\mu)}\in L^1(\mu)\quad(t\in\mathbb R).\]

Lean statement · integrable_and_integrable_exp_centered_of_lipschitz

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem integrable_and_integrable_exp_centered_of_lipschitz
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E]
    {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ]
    {L : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith L f) :
    MeasureTheory.Integrable f μ ∧ ∀ t : ℝ,
      MeasureTheory.Integrable
        (fun x => Real.exp (t * (f x - ∫ z, f z ∂μ))) μ

Exact module and namespace context

Proof roadmap

1Produce the genuine first moment
Lipschitz growth bounds the actual scalar observable by L times the norm plus its value at zero. Gaussian first Bochner integrability from pinned Mathlib yields norm L1. Continuity gives measurability, so domination yields scalar L1 and a genuine finite mean.
2Use actual Fernique integrability
Pinned Gaussian Fernique gives one actual C>0 with exp(C norm(x)^2) integrable. The space is a complete second-countable real Banach Borel space. The Gaussian need not be centered or nondegenerate; zero dimensions and zero Lipschitz constant require no extra branch or premise.
3Dominate every signed centered exponential
For each real t set b=abs(t)L and D=abs(t)(abs(f(0))+abs(m)). Young inequality gives b norm(x)≤C norm(x)^2+C^-1 b^2. Thus the centered exponential is dominated by a finite scalar times the genuine Fernique integrand. This proves the domain only; its constant depends on C and f(0), and supplies no sharp concentration coefficient.

Full assumptions and notation

All objects and hypotheses

Real complete second-countable normed vector space E with Borel measurable structure, Gaussian probability measure mu (possibly noncentered/degenerate).
Actual globally Lipschitz scalar function f:E→R with NNReal constant L, including L=0. No differentiability, boundedness, positive dimension, given mean, Laplace certificate or sharp coefficient premise.

Mathematical proof

1. Produce the genuine first moment

Lipschitz growth bounds the actual scalar observable by L times the norm plus its value at zero. Gaussian first Bochner integrability from pinned Mathlib yields norm L1. Continuity gives measurability, so domination yields scalar L1 and a genuine finite mean.

\[|f(x)|\le L\|x\|+|f(0)|,\quad f\in L^1(\mu),\quad m=\int f\,d\mu.\]

Corresponding Lean step

IsGaussian.integrable_id; LipschitzWith.dist_le_mul; Integrable.mono'

2. Use actual Fernique integrability

Pinned Gaussian Fernique gives one actual C>0 with exp(C norm(x)^2) integrable. The space is a complete second-countable real Banach Borel space. The Gaussian need not be centered or nondegenerate; zero dimensions and zero Lipschitz constant require no extra branch or premise.

\[\exists C>0:\quad\int e^{C\|x\|^2}\,d\mu(x)<\infty.\]

Corresponding Lean step

ProbabilityTheory.IsGaussian.exists_integrable_exp_sq

3. Dominate every signed centered exponential

For each real t set b=abs(t)L and D=abs(t)(abs(f(0))+abs(m)). Young inequality gives b norm(x)≤C norm(x)^2+C^-1 b^2. Thus the centered exponential is dominated by a finite scalar times the genuine Fernique integrand. This proves the domain only; its constant depends on C and f(0), and supplies no sharp concentration coefficient.

\[b=|t|L,\ D=|t|(|f(0)|+|m|),\quad e^{t(f(x)-m)}\le e^{D+C^{-1}b^2}e^{C\|x\|^2}.\]

Corresponding Lean step

two_mul_le_add_mul_sq; Real.exp_le_exp; Integrable.const_mul; Integrable.mono'

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · integrable_and_integrable_exp_centered_of_lipschitz

Produce the genuine first moment; Use actual Fernique integrability; Dominate every signed centered exponential

Download module (.lean)

theorem integrable_and_integrable_exp_centered_of_lipschitz
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E]
    {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ]
    {L : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith L f) :
    MeasureTheory.Integrable f μ ∧ ∀ t : ℝ,
      MeasureTheory.Integrable
        (fun x => Real.exp (t * (f x - ∫ z, f z ∂μ))) μ := by
  have hbound (x : E) : |f x| ≤ (L : ℝ)*‖x‖+|f 0| := by
    have hd := hf.dist_le_mul x 0
    simp only [dist_eq_norm, sub_zero, Real.norm_eq_abs] at hd
    calc
      |f x| = |(f x-f 0)+f 0| := by congr 1; ring
      _ ≤ |f x-f 0|+|f 0| := abs_add_le _ _
      _ ≤ (L : ℝ)*‖x‖+|f 0| := add_le_add hd le_rfl
  have hi : Integrable f μ :=
    (((IsGaussian.integrable_id (μ := μ)).norm.const_mul (L : ℝ)).add
      (integrable_const |f 0|)).mono' hf.continuous.aestronglyMeasurable
        (ae_of_all _ fun x => by simpa only [Real.norm_eq_abs, Pi.add_apply, id_eq] using hbound x)
  refine ⟨hi,fun t => ?_⟩
  obtain ⟨C,hC,hint⟩ := IsGaussian.exists_integrable_exp_sq μ
  let b : ℝ := |t| *(L : ℝ)
  let D : ℝ := |t| *(|f 0|+|∫ z, f z ∂μ|)
  have hb : 0 ≤ b := mul_nonneg (abs_nonneg _) L.coe_nonneg
  have hdom (x : E) : t*(f x-∫ z, f z ∂μ) ≤
      D+C⁻¹*b^2+C*‖x‖^2 := by
    have hlin : t*(f x-∫ z, f z ∂μ) ≤ b*‖x‖+D := by
      calc
        _ ≤ |t*(f x-∫ z, f z ∂μ)| := le_abs_self _
        _ = |t| *|f x-∫ z, f z ∂μ| := abs_mul _ _
        _ ≤ |t| *(|f x|+|∫ z, f z ∂μ|) :=
          mul_le_mul_of_nonneg_left (by simpa only [sub_zero, zero_sub, abs_neg] using
            (abs_sub_le (f x) 0 (∫ z, f z ∂μ))) (abs_nonneg _)
        _ ≤ |t| *((L : ℝ)*‖x‖+|f 0|+|∫ z, f z ∂μ|) :=
          mul_le_mul_of_nonneg_left (add_le_add (hbound x) le_rfl) (abs_nonneg _)
        _ = b*‖x‖+D := by dsimp [b,D]; ring
    have hy : 2*‖x‖*b ≤ C*‖x‖^2+C⁻¹*b^2 := two_mul_le_add_mul_sq hC
    have hnon : 0 ≤ b*‖x‖ := mul_nonneg hb (norm_nonneg _)
    nlinarith
  apply (hint.const_mul (Real.exp (D+C⁻¹*b^2))).mono'
    (by fun_prop)
  filter_upwards with x
  rw [Real.norm_eq_abs,abs_of_pos (Real.exp_pos _),← Real.exp_add]
  exact Real.exp_le_exp.mpr (hdom x)

/- The zero-Lipschitz branch of the sealed sharp target is internal; this is
not an assertion of the remaining positive-dimensional concentration bound. -/

Exact module and namespace context

Scope and omitted-condition boundaries

This unchanged general Gaussian domain leaf produces the actual first moment and every signed centered exponential L1; it does not itself supply a sharp concentration coefficient. The separate current finite-Hilbert standard-Gaussian theorem integral_exp_centered_le_stdGaussian_of_lipschitz and actual proximal oracle prove the scoped sharp (4.3) bound locally, with independent admission stages recorded separately. Bias (4.2), first W2/LSI/T2 bound (4.6), full Lemma4.2, higher smoothing/Picard/Wp/proxy-warmness/initialization, PBPS implementation/work, both main results and actual-input expected-query-cost composition remain open. TV proximity does not transfer unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.IsGaussian.integrable_id
ProbabilityTheory.IsGaussian.exists_integrable_exp_sq
LipschitzWith.dist_le_mul
Integrable.mono'
two_mul_le_add_mul_sq

Mathematical sources

Pinned Gaussian domain background; sharp coefficient supplied by separate declaration — This unchanged general Gaussian domain leaf produces the actual first moment and every signed centered exponential L1; it does not itself supply a sharp concentration coefficient. The separate current finite-Hilbert standard-Gaussian theorem integral_exp_centered_le_stdGaussian_of_lipschitz and actual proximal oracle prove the scoped sharp (4.3) bound locally, with independent admission stages recorded separately. Bias (4.2), first W2/LSI/T2 bound (4.6), full Lemma4.2, higher smoothing/Picard/Wp/proxy-warmness/initialization, PBPS implementation/work, both main results and actual-input expected-query-cost composition remain open. TV proximity does not transfer unbounded expected cost.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Samplinglib mathematical lesson

Sharp standard Gaussian concentration for every Lipschitz observable

AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential.integral_exp_centered_le_stdGaussian_of_lipschitz · theorem · Teaching coverage

Read this first

Mathematical statement

For every globally L-Lipschitz scalar observable on the stated finite real Hilbert/Borel space, its actual standard Gaussian centered exponential integral is at most exp(L^2*t^2/2) for every signed real t. Actual first moments and all exponential domains are produced by the existing shared domain theorem; the C1 restriction used inside the proof is removed internally.

\[\gamma=\operatorname{stdGaussian}(E),\quad m=\int f\,d\gamma,\quad\int e^{t(f-m)}\,d\gamma\le e^{L^2t^2/2}\quad(t\in\mathbb R).\]

Lean statement · integral_exp_centered_le_stdGaussian_of_lipschitz

Download module (.lean)

theorem integral_exp_centered_le_stdGaussian_of_lipschitz
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {L : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith L f) (t : ℝ) :
    (∫ x, Real.exp (t * (f x - ∫ z, f z ∂ProbabilityTheory.stdGaussian E))
      ∂ProbabilityTheory.stdGaussian E) ≤ Real.exp ((L : ℝ)^2 * t^2 / 2)

Exact module and namespace context

Proof roadmap

1Establish the actual Gaussian domains
The existing Fernique-domain declaration proves first Bochner integrability and every signed centered exponential L1 from global Lipschitz growth. Shifting the center gives radial exponential domains. Polynomial factors are dominated by a larger radial exponential, also on the actual product Gaussian equipped with its Banach max norm.
2Derive Gaussian Stein integration by parts
For the temporary C1 case, the canonical ASTIS Gaussian density with respect to the given Hilbert volume has derivative -w(x) inner(x,-). Growth, the genuine Gaussian second moment and the derivative bound by L prove every Haar integration-by-parts integrability input. The resulting Stein equality has no supplied domain certificate.
3Rotate two independent standard Gaussians
For X,Y independently distributed as gamma, U=cos(theta)X+sin(theta)Y and W=-sin(theta)X+cos(theta)Y have the same product law. Differentiate F(theta)=E[f(X) exp(t(f(U)-m))] using an explicit polynomial times radial-exponential domination valid for every theta. The inverse relation X=cos(theta)U-sin(theta)W is exact.
4Apply Stein only to the affine Lipschitz factor
After rotation, fix U=u and let a(u) be the Riesz representative of Df(u). Apply Stein in W to the C1 Lipschitz function W→f(cu-sW). Its derivative is -s Df(cu-sW). The exponential is constant in this conditional variable; it is never asserted globally Lipschitz. Actual product L1 and Fubini justify the conditional calculation.
5Recover the covariance bound with correct sign
The inner integral has absolute value at most L squared. On theta in [0,pi/2] and t≥0 the factor -sin(theta)t is nonpositive, so the upper bound on the inner integral gives a lower bound on F prime. For C=t L squared M, H=F-cos(theta)C is nondecreasing by the mean-value theorem. Actual derivative existence gives endpoint continuity. Endpoint independence yields the covariance inequality.
6Prove the sharp Herbst estimate and both signs
All signed exponential domains give integrableExpSet=the full real line. Pinned Mathlib MGF differentiation gives the actual M prime. The covariance estimate implies M prime≤t L squared M on t≥0. The integrating factor exp(-L squared t squared/2)M is nonincreasing and equals one at zero. Apply the result to -f and -t for negative parameters.
7Smooth internally without changing the constant
Use the actual nonnegative normalized compactly supported smooth bump against canonical Hilbert volume. Its outer radius is epsilon_n=2^-n and its mass is one. The convolution f_n is C1 and remains globally L Lipschitz. The uniform error is at most L epsilon_n. This introduces no differentiability assumption on the public observable.
8Pass the actual center and exponential integral to the limit
First-moment integrability and the uniform approximation give |m_n-m|≤L epsilon_n. The centered exponents converge pointwise, and every n is dominated by exp(2|t|L) exp(t(f-m)), whose L1 was proved before the sharp estimate. Dominated convergence passes the same sharp bound to f. Zero L and the zero-dimensional carrier are discharged directly as constant observables.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional complete real Hilbert space E with its actual inner product and Borel measurable structure, including dimension zero; gamma is the canonical covariance-identity standard Gaussian.
Actual globally L-Lipschitz f:E→R with NNReal L≥0 including zero; every signed t in R. No differentiability, boundedness, given mean, positive dimension or concentration/LSI/domain certificate.

Mathematical proof

1. Establish the actual Gaussian domains

The existing Fernique-domain declaration proves first Bochner integrability and every signed centered exponential L1 from global Lipschitz growth. Shifting the center gives radial exponential domains. Polynomial factors are dominated by a larger radial exponential, also on the actual product Gaussian equipped with its Banach max norm.

\[m=\int f\,d\gamma,\quad e^{t(f-m)}\in L^1(\gamma),\quad (1+\|x\|)^2e^{a\|x\|}\in L^1(\gamma).\]

Corresponding Lean step

integrable_and_integrable_exp_centered_of_lipschitz; gaussian_radial_exponential_integrable; gaussian_polynomial_radial_integrable

2. Derive Gaussian Stein integration by parts

For the temporary C1 case, the canonical ASTIS Gaussian density with respect to the given Hilbert volume has derivative -w(x) inner(x,-). Growth, the genuine Gaussian second moment and the derivative bound by L prove every Haar integration-by-parts integrability input. The resulting Stein equality has no supplied domain certificate.

\[w(x)=(\sqrt{2\pi})^{-d}e^{-\|x\|^2/2},\quad Dw(x)[v]=-w(x)\langle x,v\rangle,\quad\int\langle x,v\rangle f(x)\,d\gamma=\int Df(x)[v]\,d\gamma.\]

Corresponding Lean step

standardGaussian_density; standardWeight_hasFDerivAt; standardGaussian_stein_lipschitz_c1; integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable

3. Rotate two independent standard Gaussians

For X,Y independently distributed as gamma, U=cos(theta)X+sin(theta)Y and W=-sin(theta)X+cos(theta)Y have the same product law. Differentiate F(theta)=E[f(X) exp(t(f(U)-m))] using an explicit polynomial times radial-exponential domination valid for every theta. The inverse relation X=cos(theta)U-sin(theta)W is exact.

\[U_\theta=cX+sY,\ W_\theta=-sX+cY,\quad F^{\prime}(\theta)=t\,\mathbb E[f(X)e^{t(f(U_\theta)-m)}Df(U_\theta)[W_\theta]].\]

Corresponding Lean step

standardGaussian_rotation_integral; rotX_hasDerivAt; rotated_laplace_integral_hasDerivAt; rotation_inverse_first

4. Apply Stein only to the affine Lipschitz factor

After rotation, fix U=u and let a(u) be the Riesz representative of Df(u). Apply Stein in W to the C1 Lipschitz function W→f(cu-sW). Its derivative is -s Df(cu-sW). The exponential is constant in this conditional variable; it is never asserted globally Lipschitz. Actual product L1 and Fubini justify the conditional calculation.

\[F^{\prime}(\theta)=-s t\int e^{t(f(u)-m)}\!\left[\int Df(cu-sv)[a(u)]\,d\gamma(v)\right]d\gamma(u),\quad\|a(u)\|\le L.\]

Corresponding Lean step

standardGaussian_stein_affine; affine_stein_laplace_slice; rotated_laplace_derivative_integral_identity

5. Recover the covariance bound with correct sign

The inner integral has absolute value at most L squared. On theta in [0,pi/2] and t≥0 the factor -sin(theta)t is nonpositive, so the upper bound on the inner integral gives a lower bound on F prime. For C=t L squared M, H=F-cos(theta)C is nondecreasing by the mean-value theorem. Actual derivative existence gives endpoint continuity. Endpoint independence yields the covariance inequality.

\[M=\int e^{t(f-m)}d\gamma,\quad F^{\prime}\ge-\sin\theta\,tL^2M,\quad H^{\prime}\ge0,\quad\operatorname{Cov}_\gamma(f,e^{t(f-m)})\le tL^2M.\]

Corresponding Lean step

affine_directional_derivative_integral_norm_le; rotated_laplace_derivative_integral_lower_bound; gaussian_laplace_covariance_bound; monotoneOn_of_hasDerivWithinAt_nonneg

6. Prove the sharp Herbst estimate and both signs

All signed exponential domains give integrableExpSet=the full real line. Pinned Mathlib MGF differentiation gives the actual M prime. The covariance estimate implies M prime≤t L squared M on t≥0. The integrating factor exp(-L squared t squared/2)M is nonincreasing and equals one at zero. Apply the result to -f and -t for negative parameters.

\[M^{\prime}(t)\le tL^2M(t),\quad\left(e^{-L^2t^2/2}M(t)\right)^{\prime}\le0,\quad M(t)\le e^{L^2t^2/2}\quad(t\in\mathbb R).\]

Corresponding Lean step

gaussian_centered_integrableExpSet; gaussian_centered_laplace_hasDerivAt; gaussian_centered_laplace_bound_c1; hasDerivAt_mgf; antitoneOn_of_hasDerivWithinAt_nonpos

7. Smooth internally without changing the constant

Use the actual nonnegative normalized compactly supported smooth bump against canonical Hilbert volume. Its outer radius is epsilon_n=2^-n and its mass is one. The convolution f_n is C1 and remains globally L Lipschitz. The uniform error is at most L epsilon_n. This introduces no differentiability assumption on the public observable.

\[f_n=\phi_n*f,\quad\phi_n\ge0,\quad\int\phi_n\,dx=1,\quad\operatorname{Lip}(f_n)\le L,\quad\|f_n-f\|_\infty\le L2^{-n}.\]

Corresponding Lean step

normed_bump_convolution_lipschitz; normed_bump_convolution_error; smoothApprox_contDiff; smoothApprox_lipschitz

8. Pass the actual center and exponential integral to the limit

First-moment integrability and the uniform approximation give |m_n-m|≤L epsilon_n. The centered exponents converge pointwise, and every n is dominated by exp(2|t|L) exp(t(f-m)), whose L1 was proved before the sharp estimate. Dominated convergence passes the same sharp bound to f. Zero L and the zero-dimensional carrier are discharged directly as constant observables.

\[|m_n-m|\le L2^{-n},\quad e^{t(f_n-m_n)}\le e^{2|t|L}e^{t(f-m)},\quad\int e^{t(f-m)}d\gamma\le e^{L^2t^2/2}.\]

Corresponding Lean step

smoothApprox_mean_error; smoothApprox_centered_exp_integral_tendsto; centered_exp_integral_of_lipschitz_zero; centered_exp_integral_of_subsingleton; integral_exp_centered_le_stdGaussian_of_lipschitz

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · integral_exp_centered_le_stdGaussian_of_lipschitz

Establish the actual Gaussian domains; Derive Gaussian Stein integration by parts; Rotate two independent standard Gaussians; Apply Stein only to the affine Lipschitz factor; Recover the covariance bound with correct sign; Prove the sharp Herbst estimate and both signs; Smooth internally without changing the constant; Pass the actual center and exponential integral to the limit

Download module (.lean)

theorem integral_exp_centered_le_stdGaussian_of_lipschitz
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {L : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith L f) (t : ℝ) :
    (∫ x, Real.exp (t * (f x - ∫ z, f z ∂ProbabilityTheory.stdGaussian E))
      ∂ProbabilityTheory.stdGaussian E) ≤ Real.exp ((L : ℝ)^2 * t^2 / 2) := by
  by_cases hL : L = 0
  · subst L
    rw [centered_exp_integral_of_lipschitz_zero hf t]
    norm_num
  · rcases subsingleton_or_nontrivial E with hE | hE
    · letI : Subsingleton E := hE
      rw [centered_exp_integral_of_subsingleton f t]
      exact Real.one_le_exp_iff.mpr (by positivity)
    · exact le_of_tendsto' (smoothApprox_centered_exp_integral_tendsto hf t)
        (fun n => gaussian_centered_laplace_bound_c1
          (smoothApprox_contDiff hf n) (smoothApprox_lipschitz hf n) t)

end AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential
end

Exact module and namespace context

Scope and omitted-condition boundaries

Locally compiled sharp centered Gaussian-output estimate (4.3), retained exact positive-step proximal/evaluator and (4.4)-(4.5), genuine first Bochner moments and all signed exponential domains. Independent mathematics/blind/source/publication/exact-commit/integration admission pending. Bias (4.2), first W2 inequality in (4.6), LSI/T2 adapter, full Lemma4.2, higher smoothing/Picard/Wp/proxy-warmness/initialization, PBPS invariance/nonexplosion/hypocoercivity/implementation/work, both main results and actual-input precision/expected-query-cost composition remain open. Centers are actual Gaussian output means. TV proximity does not transfer unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.IsGaussian.map_rotation_eq_self
integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable
hasDerivAt_integral_of_dominated_loc_of_deriv_le
MeasureTheory.integral_prod
ProbabilityTheory.hasDerivAt_mgf
ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet
monotoneOn_of_hasDerivWithinAt_nonneg
antitoneOn_of_hasDerivWithinAt_nonpos
ContDiffBump.hasCompactSupport_normed
ContDiffBump.contDiff_normed
MeasureTheory.tendsto_integral_of_dominated_convergence

Mathematical sources

Exact Gaussian background for sharp (4.3) — Locally compiled sharp centered Gaussian-output estimate (4.3), retained exact positive-step proximal/evaluator and (4.4)-(4.5), genuine first Bochner moments and all signed exponential domains. Independent mathematics/blind/source/publication/exact-commit/integration admission pending. Bias (4.2), first W2 inequality in (4.6), LSI/T2 adapter, full Lemma4.2, higher smoothing/Picard/Wp/proxy-warmness/initialization, PBPS invariance/nonexplosion/hypocoercivity/implementation/work, both main results and actual-input precision/expected-query-cost composition remain open. Centers are actual Gaussian output means. TV proximity does not transfer unbounded expected cost.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.