Normalize a strongly convex Gibbs target without assuming its minimizer
AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn · theorem · Teaching coverage
Mathematical statement
Let E be a finite-dimensional real inner-product space equipped with its Borel sigma-algebra and canonical volume. Let V:E→R be differentiable and m-strongly convex on the whole space, where m>0. Then exp(−V) is integrable with respect to volume. A minimizer, a gradient witness, a tail bound and a normalizing constant are not additional inputs.
Lean statement · integrable_exp_neg_of_strongConvexOn
The three explicit hypotheses are positive real modulus, everywhere differentiability, and Mathlib StrongConvexOn univ m V. Finite-dimensional Borel inner-product structure appears as typeclasses. Finite dimension supplies completeness used by the actual-gradient API. The conclusion is Bochner Integrable for a nonnegative real function, which includes measurable and finite-integral content.
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_exp_neg_of_strongConvexOn {V : E → ℝ} {m : ℝ}
(hm : 0 < m) (hV : Differentiable ℝ V)
(hsc : StrongConvexOn Set.univ m V) :
Integrable (fun x => Real.exp (-V x)) (volume : Measure E)Proof roadmap
- 1Use a fixed point rather than assume a minimizer
Set g=∇V(0). Since V is differentiable, this is its actual gradient. The compiled first-order strong-convexity inequality applied at zero controls V everywhere, regardless of whether zero is a critical point or an admissible algorithmic reference point.
- 2Absorb the linear term into the quadratic growth
Cauchy–Schwarz controls the potentially negative inner product. Young's inequality with parameter m/2 then spends half of the quadratic growth to absorb the linear term. The remaining coefficient m/4 is strictly positive.
- 3Dominate the Gibbs weight by the compiled Gaussian envelope
Negation reverses the lower potential bound and the exponential is increasing. The resulting Gaussian envelope is already known to be volume-integrable in finite dimension. Continuity of V makes exp(−V) strongly measurable, so pointwise domination proves integrability.
Full assumptions and notation
All objects and hypotheses
- Strong convexity uses the chord convention V((1−t)x+ty)≤(1−t)V(x)+tV(y)−m t(1−t)‖x−y‖²/2 for every x,y and t∈[0,1].
- Differentiability is genuine everywhere differentiability, not a formula using a possibly totalized gradient alone. It supplies both continuity and the actual gradient at zero.
- The space has finite real dimension. Canonical volume is the Lebesgue normalization attached to the inner product, not an arbitrary measure or infinite-dimensional formal volume.
- Strict positivity of m gives a decaying Gaussian envelope. Convexity with m=0 does not suffice: the constant potential on the real line has infinite normalizer.
- The two papers state Hessian lower bounds for C² potentials. Their conversion to this StrongConvexOn hypothesis remains an explicit separate adapter; this supporting theorem does not silently replace those source assumptions.
Mathematical proof
1. Use a fixed point rather than assume a minimizer
Set g=∇V(0). Since V is differentiable, this is its actual gradient. The compiled first-order strong-convexity inequality applied at zero controls V everywhere, regardless of whether zero is a critical point or an admissible algorithmic reference point.
Corresponding Lean step
Each (hV z).hasGradientAt supplies the genuine gradient required by StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn. The proof specializes its x input to zero and y input to the point being bounded. No global gradient field is assumed.
2. Absorb the linear term into the quadratic growth
Cauchy–Schwarz controls the potentially negative inner product. Young's inequality with parameter m/2 then spends half of the quadratic growth to absorb the linear term. The remaining coefficient m/4 is strictly positive.
Corresponding Lean step
abs_real_inner_le_norm supplies the lower inner-product bound; two_mul_le_add_mul_sq with ε=m/2 supplies Young's inequality. nlinarith combines these with hfirst. The code writes b as V 0−(m/2)⁻¹/2*‖g‖², equal to the displayed value because m>0.
3. Dominate the Gibbs weight by the compiled Gaussian envelope
Negation reverses the lower potential bound and the exponential is increasing. The resulting Gaussian envelope is already known to be volume-integrable in finite dimension. Continuity of V makes exp(−V) strongly measurable, so pointwise domination proves integrability.
Corresponding Lean step
Integrability.integrable_exp_neg_add_mul_norm_sq supplies integrability of the envelope; its exact integral is explanatory and is not reproved here. The explicit composition Real.continuous_exp.comp hV.continuous.neg supplies measurability. Integrable.mono' and Real.exp_le_exp conclude the proof.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · integrable_exp_neg_of_strongConvexOn
This is a new join of two existing ASTIS mathematical parents, not a restatement of an assumed normalizer. The first-order bound and Gaussian tail theorem are owned compiled ASTIS results; Mathlib supplies the gradient bridge, Cauchy–Schwarz, Young's inequality and integral domination. Tests then use Mathlib integral_exp_pos and isProbabilityMeasure_tilted to obtain a positive normalizer and a probability measure, and feed that actual Gibbs probability into the previously compiled RGO closure.
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_exp_neg_of_strongConvexOn {V : E → ℝ} {m : ℝ}
(hm : 0 < m) (hV : Differentiable ℝ V)
(hsc : StrongConvexOn Set.univ m V) :
Integrable (fun x => Real.exp (-V x)) (volume : Measure E) := by
let g : E := gradient V 0
let b : ℝ := V 0 - (m / 2)⁻¹ / 2 * ‖g‖ ^ 2
have hquad : ∀ x : E, m / 4 * ‖x‖ ^ 2 + b ≤ V x := by
intro x
have hfirst : V 0 + inner ℝ g x + m / 2 * ‖x‖ ^ 2 ≤ V x := by
simpa only [g, sub_zero] using
StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn hsc
(fun z _ => (hV z).hasGradientAt) (x := 0) (y := x)
(Set.mem_univ _) (Set.mem_univ _)
have hinner := (abs_le.mp (abs_real_inner_le_norm g x)).1
have hyoung := two_mul_le_add_mul_sq (a := ‖x‖) (b := ‖g‖)
(show 0 < m / 2 by positivity)
dsimp only [b]
nlinarith
have hbound := Integrability.integrable_exp_neg_add_mul_norm_sq
(E := E) (a := m / 4) (b := b) (by positivity)
refine hbound.mono' ((Real.continuous_exp.comp hV.continuous.neg).aestronglyMeasurable) ?_
filter_upwards with x
rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
exact Real.exp_le_exp.mpr (neg_le_neg (hquad x))
end AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrabilitySource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The displayed supporting lemma uses differentiability and positive m-strong convexity | Differentiable ℝ V and StrongConvexOn Set.univ m V, with 0<m | same | Mathlib's chord inequality uses exactly the m/2 normalization displayed in the supporting statement. |
| Euclidean finite-dimensional state and Lebesgue normalization | Any finite-dimensional real inner-product Borel space with canonical volume | generalization | The coordinate-free version retains the same finite-dimensional Gaussian envelope and canonical volume. It does not propose an infinite-dimensional sampling extension. |
| Gibbs normalizability is implicit in proportional-density notation | Integrability is proved from first-order growth and an existing Gaussian envelope; the actual gradient comes from differentiability | source-implicit | Neither minimizer existence nor finite normalizer is added as a premise. Strictly positive mass and the probability law then follow from existing Mathlib APIs, exercised in the focused test. |
| The paper imposes C² Hessian lower bounds on U and adds the quadratic RGO potential | The supporting lemma takes StrongConvexOn for V rather than a Hessian field | unresolved | A source application still must prove the Hessian-to-StrongConvexOn and particular-potential adapters. This binding is a prerequisite and cannot count as closure of those source obligations. |
A genuine normalization prerequisite, not full source Gibbs initialization, Hessian/curvature equivalence, complete Lemma 6.4 or sampling formalization.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- assumptions: The formal prerequisite takes differentiability and StrongConvexOn, while the papers give C² potentials with Hessian lower bounds. — The selected supporting theorem states its own chord hypothesis explicitly. The separate source-hessian-adapter obligation must still derive it for the source potential; this prerequisite does not silently prove or replace that adapter.
- domains: The supporting theorem is stated on arbitrary finite-dimensional real inner-product Borel spaces, including the degenerate zero-dimensional space. — This is an explicit coordinate-free generalization of the source's Euclidean setting, with the same canonical volume normalization. The one-point case is valid, and no infinite-dimensional volume is being assumed.
- conclusion: The production result establishes integrability; positive normalization and construction of an abstract Gibbs probability are exercised as consumers rather than packaged as additional production conclusions. — The focused tests use integral_exp_pos and isProbabilityMeasure_tilted on the new integrability theorem, then invoke normalized quadratic RGO closure. All these tests independently compile without a supplied minimizer or integral bound.
- scopes: This is an explicitly attributed supporting mathematical expansion, not a verbatim theorem from either paper or complete Gibbs/RGO/source-sampler assimilation. — The pinned publication binding is role prerequisite and supports only gibbs-weight-integrability. Particular-source potential and density identification remain source-gibbs-identification; no sampling or process completion is inferred.
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
- The m/4 coefficient is only an integrability envelope. It neither weakens the original strong-convexity claim nor substitutes for the source's curvature or complexity constants.
- The finite offset b depends on V(0), ∇V(0) and m. This is an existence-of-finite-mass argument, not a uniform normalization or sampling-cost bound.
- Hessian lower bound → StrongConvexOn is still open in the current paper route. No global minimizer is assumed or constructed, and no algorithmic reference point is certified.
- The statement supports Gibbs initialization for both companion papers but does not itself prove either source's initialization theorem, RGO implementation, invariant law, mixing rate, output error or expected query cost.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOnAutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.integrable_exp_neg_add_mul_norm_sq
Mathlib API called (external library)
- DifferentiableAt.hasGradientAt
- abs_real_inner_le_norm
- two_mul_le_add_mul_sq
- MeasureTheory.Integrable.mono'
- Real.continuous_exp
- Real.exp_le_exp
Mathematical sources
- Chen, Chewi, Lu and Zhang, Smoothed Picard Hamiltonian Monte Carlo v1 — Normalization prerequisite for the Gibbs and RGO densities defined before Lemma 6.4. ASTIS expanded first-order/Young/Gaussian-envelope proof, not copied prose or the whole lemma.
- Chen, Chewi, Lu and Zhang, Proximal Bouncy Particle Sampler v1 — The strongly convex Gibbs target also requires this finite-normalizer input. Its Hessian and probability-density adapter remain separately explicit.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.