Gaussian Lipschitz first moment and signed exponential domain
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential.integrable_and_integrable_exp_centered_of_lipschitz · theorem · Teaching coverage
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.
Lean statement · integrable_and_integrable_exp_centered_of_lipschitz
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.
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.
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 ∂μ))) μ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.
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.
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.
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
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.
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. -/Source assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Authored Gaussian-domain background implication from pinned Mathlib Fernique; this is not the printed sharp concentration estimate. | 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. 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. | same | Canonical global Lipschitz mathematical input and Gaussian Banach/Borel contracts exactly stated. Actual source consumer produces its direction Lipschitz bound internally; no new source premise. |
| SPHMC4.3 sharp centered concentration coefficient eta*normu^2/2. | 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. | unresolved | Fernique supplies domain only; this mapping claims no sharp estimate from the domain leaf. The separate current sharp declaration addresses the scoped coefficient, with full-paper obligations unchanged. |
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.
Encoder–denoiser: accepted · equivalent-after-elaboration
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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.