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.