Regular-Class Representation After Ball Conditioning and Affine Transport

This statement formalizes Letwin's Lemma A.1 regular-class construction.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure. Let $V:E\to\mathbb R$ satisfy RegularPotential V a b, let $R>0$, let $L:E\simeq_L E$ be a continuous linear equivalence, and let $c\in E$. Then there exist a set $K\subseteq E$, a function $W:E\to\mathbb R$, and a constant $κ\in\mathbb R$ such that:

1. $κ>0$, $K$ is compact and convex, and $\operatorname{int}K$ is nonempty;
2. $W$ is $C^\infty$ and $y\mapsto W(y)-(κ/2)\|y\|^2$ is convex on all of $E$;
3. the affine image of the conditional law of hV.law on the closed ball $\overline B(0,R)$ has density

This is an existence result for compact, smooth, uniformly convex regular approximants.

Original Lean declaration header

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

theorem exists_regularClass_of_cond_closedBall_map [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {a b : ℝ} (hV : RegularPotential V a b) {R : ℝ} (hR : 0 < R) (L : E ≃L[ℝ] E)
    (c : E) :
    ∃ (K : Set E) (W : E → ℝ) (κ : ℝ), 0 < κ ∧ IsCompact K ∧ Convex ℝ K ∧ (interior K).Nonempty ∧
      ContDiff ℝ ∞ W ∧ ConvexOn ℝ univ (fun y => W y - (κ / 2) * ‖y‖ ^ 2) ∧
      (ProbabilityTheory.cond (hV.law : Measure E) (closedBall (0 : E) R)).map (fun x => L (x - c)) =
        (volume : Measure E).withDensity (K.indicator fun p => ENNReal.ofReal (Real.exp (-W p)))

Module navigation

Module: KLS/LogConcave/BallConditioning.

Definition modules: KLS/LogConcave/Regular/Basic.

Supporting theorems: convexOn_of_hessian_ge, RegularPotential.law_comp_affine.

Next: covariance_tendsto_one.

Source excerpt, lines 99–105 · Frozen source 408915f.