Weak Moment Map for a Bounded Isotropic Law

This is the auxiliary form of the weak moment-map existence statement.

Let $E$ be finite-dimensional with Borel structure, let $\mu$ be an isotropic probability measure, and let $L\in[0,\infty)$. Assume $\|y\|\le L$ for $\mu$-almost every $y$. Then there exists $\psi:E\to\mathbb{R}$ such that $\psi$ is convex, $L$-Lipschitz, and normalized by

Furthermore, the tilted Lebesgue measure pushes forward under the gradient to $\mu$:

Equivalently, ((volume : Measure E).tilted (-ψ)).map (gradient ψ) = μ. The statement claims no additional regularity of $\psi$.

Original Lean declaration header

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

private theorem exists_momentMap_aux (μ : ProbabilityMeasure E)
    (hμ : KLS.Isotropic μ) (L : NNReal) (hL : ∀ᵐ y ∂(μ : Measure E), ‖y‖ ≤ (L : ℝ)) :
    ∃ ψ : E → ℝ, ConvexOn ℝ (univ : Set E) ψ ∧ LipschitzWith L ψ ∧
      (∫ x, Real.exp (-ψ x) ∂(volume : Measure E)) = 1 ∧
      ((volume : Measure E).tilted (fun x => -ψ x)).map (gradient ψ) = (μ : Measure E)

Module navigation

Module: KLS/CEK/MomentMap.

Definition modules: KLS/Isotropic.

Supporting theorems: legendre_bounded_perturbation_finite_curve, bounded_source_lipschitz_primal, hasDerivAt_integral_exp_neg_legendre_add_smul.

Source excerpt, lines 32–36 · Frozen source 408915f.