Suspension Joint Law As A Tilted Lebesgue Measure

This formalizes the density identity (109) in the proof of Proposition 7.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 28.

Let $V,f:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}n)\to\mathbb R$ be measurable, let $\beta>0$, and assume $e^{-V}$ is integrable with respect to Lebesgue measure. Let $\mu$ be the probability measure obtained by tilting Lebesgue measure by $-V$. For every $N\in\mathbb N$, the joint law formed from $N$ independent copies with law $\mu$ and an independent Laplace variable of parameter $\beta$ equals the tilted Lebesgue measure on the joint space with potential

where $s=p(\operatorname{none})$, $x_i$ is the coordinate indexed by some (i,j), and $\sigma_\beta=\sqrt{1+2/\beta^2}$.

In Lean notation, the conclusion is the equality between jointLaw and Measure.tilted by the negative of potential. This identifies the suspension distribution with a normalized tilted Lebesgue law and is used in subsequent log-concavity arguments.

Original Lean declaration header

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

theorem jointLaw_eq_tilted {n N : ℕ} (V f : EuclideanSpace ℝ (Fin n) → ℝ) {β : ℝ} (hβ : 0 < β)
    (hV : Measurable V) (hf : Measurable f) (hint : Integrable (fun x => Real.exp (-V x))) :
    jointLaw (volume.tilted fun x => -V x) f β (sigma β) N =
      (volume : Measure (JointSpace N n)).tilted fun p =>
        -potential V f β (sigma β) N (p none, fun i => WithLp.toLp 2 fun j => p (some (i, j)))

Module navigation

Module: KLS/BKL/Suspension/Density.

Definition modules: KLS/BKL/Suspension/Law, KLS/BKL/Suspension/Basic.

Supporting theorems: lintegral_pi_prod_fin, map_density_shift_scale.

Previous: map_density_shift_scale.

Source excerpt, lines 278–282 · Frozen source 408915f.