Prove2Me

Interior Support Convex Hull from Centering and Nondegeneracy

Proved
FunctionalInequalities.Probability.zero_mem_interior_convexHull_support_of_integral_eq_zero_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

corderoklartag2015functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves that the origin is an interior support point under centering and full-dimensionality assumptions.

Let μ\mu be a nonzero finite Borel measure on a finite-dimensional real inner-product space. Assume:

  1. no proper linear subspace carries all of μ\mu;
  2. the identity map is integrable;
  3. the barycenter is zero:
∫x dμ(x)=0.\int x\,d\mu(x)=0.

Then

0∈int⁡(conv⁡(supp⁡μ)).0\in\operatorname{int}\bigl(\operatorname{conv}(\operatorname{supp}\mu)\bigr).

This geometric statement supplies the origin-interior hypothesis used in normalization and convex-support arguments.

Original Lean declaration header

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

theorem zero_mem_interior_convexHull_support_of_integral_eq_zero {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hint : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    (0 : E) ∈ interior (convexHull ℝ μ.support)

Module navigation

Module: Probability/ConvexSupport.

Previous: exists_pos_le_mul_lintegral_toReal_of_convex_epigraph.

Source excerpt, lines 709–714 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_ConvexSupport

open MeasureTheory
Formal statement

theorem FunctionalInequalities.Probability.zero_mem_interior_convexHull_support_of_integral_eq_zero_readable {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hint : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    (0 : E) ∈ interior (convexHull ℝ μ.support) := by sorry
Source
Source: Cordero-Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), Lemma 17. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/ConvexSupport.lean#L707-L774 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.ConvexSupport`, declaration `FunctionalInequalities.Probability.zero_mem_interior_convexHull_support_of_integral_eq_zero`; the repository is private at upload time).

View graph