Density Transformation Under A Fibrewise Shear

This technical lemma gives the density transformation for a fibrewise affine change of variables.

Let $A$ be a measurable space, let $\mu$ be an s-finite measure on $A$, let $F:A\to\mathbb R$ be measurable, let $\sigma\ne0$, and let $w:A\times\mathbb R\to[0,\infty]$ be measurable. Under the map

the pushforward of the measure with density $w$ relative to $\mu\otimes ds$ is the measure with density

Equivalently,

The lemma records the Jacobian factor for the shear and rescaling used in the suspension density calculation.

Original Lean declaration header

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

private theorem map_density_shift_scale {A : Type*} [MeasurableSpace A] (μ : Measure A)
    [SFinite μ] (F : A → ℝ) (hF : Measurable F) (σ : ℝ) (hσ : σ ≠ 0)
    (w : A × ℝ → ENNReal) (hw : Measurable w) :
    ((μ.prod volume).withDensity w).map (fun p => (p.1, (F p.1 + p.2) / σ)) =
      (μ.prod volume).withDensity
        (fun p => ENNReal.ofReal |σ| * w (p.1, σ * p.2 - F p.1))

Module navigation

Module: KLS/BKL/Suspension/Density.

Next: jointLaw_eq_tilted.

Source excerpt, lines 29–34 · Frozen source 408915f.