StrongConvexGibbsIntegrability: mathematical reading route

Normalize a strongly convex Gibbs target without assuming its minimizer

AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn · theorem · Teaching coverage

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.

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

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)

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.StrongConvexGibbsIntegrability

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.