Tilted Haar Laws Have Full Support

Proved

FunctionalInequalities.KLS.LogConcave.interior_support_nonempty_of_eq_tilted_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem states that a probability law obtained by tilting Haar measure has nonempty support interior.

Let $V$ be a measurable normed space, let $m$ be an additive Haar measure, let $\nu$ be a probability measure, and let $W:V\to\mathbb R$ satisfy

\nu=m.\operatorname{tilted}(-W).

Then

\operatorname{interior}(\operatorname{supp}\nu)\ne\varnothing.

In fact, the support is all of $V$ under the hypotheses in the type. This auxiliary fact is used to supply the nonempty-interior-support assumption required by the closed weighted-gradient constructions.

Original Lean declaration header

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

theorem interior_support_nonempty_of_eq_tilted (m : Measure V) [m.IsAddHaarMeasure] {W : V → ℝ}
    (hνW : (ν : Measure V) = m.tilted (-W)) :
    (interior (ν : Measure V).support).Nonempty

Module navigation

Module: KLS/LogConcave/Density/Tilted.

Supporting theorems: integrable_exp_neg_of_eq_tilted.

Previous: isBorellDensity_of_eq_tilted · Next: convexOn_of_eq_tilted.

Source excerpt, lines 152–154 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_Tilted

open MeasureTheory Set
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {ν : MeasureTheory.ProbabilityMeasure V}
omit [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [BorelSpace V]

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.interior_support_nonempty_of_eq_tilted_readable (m : Measure V) [m.IsAddHaarMeasure] {W : V → ℝ}
    (hνW : (ν : Measure V) = m.tilted (-W)) :
    (interior (ν : Measure V).support).Nonempty := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Density/Tilted.lean#L150-L169 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Density.Tilted`, declaration `FunctionalInequalities.KLS.LogConcave.interior_support_nonempty_of_eq_tilted`; the repository is private at upload time).

View graph