Compact Sublevels From Exponential Integrability

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure, let $m$ be an additive Haar measure on $E$, and let $\varphi:E\to\mathbb R$ be convex. Assume

Then $\varphi$ has a global minimizer and every real sublevel set is compact:

and

This gives the compactness and attainment properties required for finite-dimensional convex potentials with integrable exponential weight.

Formalization Note No normalization of the integral is assumed; only Integrable is required. Dimension zero is included.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem exists_forall_le_and_isCompact_sublevel_of_convexOn_integrable_exp_neg
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] (m : Measure E) [m.IsAddHaarMeasure] {φ : E → ℝ}
    (hconv : ConvexOn ℝ Set.univ φ) (hint : Integrable (fun x => Real.exp (-φ x)) m) :
    (∃ y₀ : E, ∀ y, φ y₀ ≤ φ y) ∧ ∀ c : ℝ, IsCompact {y | φ y ≤ c}

Module navigation

Module: Analysis/Convex/Coercivity.

Source excerpt, lines 25–29 · Frozen source 408915f.

Literature

This formalizes Lemma A.4 of Letwin (arXiv:2607.24164v1), p. 17, in its coercivity form.