Logarithmic Laplace Factorization at Integrable Joint Parameters

This lemma states the logarithmic Laplace factorization at a parameter with integrable joint exponential.

Let $n,N\in\mathbb N$ with $N>0$, $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)), $\mu$ a probability measure on $E$, and $f:E\to\mathbb R$ measurable. Let $\beta>0$, $\eta_\beta=$ laplaceMeasure $\beta$, $\sigma_\beta=\sqrt{1+2/\beta^2}$ (sigma), and $\lambda=$ jointLaw $\mu\ f\ \beta\ \sigma_\beta\ N$. The target $H=$ JointSpace $N\ n$ has a scalar coordinate and $N$ copy blocks. For $z\in H$, denote these by $z_0$ and $z_i\in E$.

Assume $e^{\langle z,\cdot\rangle}\in L^1(\lambda)$. With $\Lambda_\lambda(z)=\log\int e^{\langle z,p\rangle}\,d\lambda(p)$ (logLaplace),

This gives the real logarithmic identity used in local derivative calculations, with joint integrability explicitly required.

Original Lean declaration header

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

theorem logLaplace_jointLaw_factorization {n N : ℕ} (μ : Measure (EuclideanSpace ℝ (Fin n)))
    [IsProbabilityMeasure μ] {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : Measurable f)
    {β : ℝ} (hβ : 0 < β) (hN : 0 < N) (z : JointSpace N n)
    (hInt : Integrable (fun p => Real.exp ⟪z, p⟫) (jointLaw μ f β (sigma β) N)) :
    FunctionalInequalities.Analysis.BakryEmery.logLaplace (jointLaw μ f β (sigma β) N) z =
      Real.log (∫ s : ℝ, Real.exp (z none / sigma β * s) ∂laplaceMeasure β) +
        ∑ i : Fin N, Real.log (∫ x, Real.exp
          (z none / (sigma β * Real.sqrt N) * f x +
            ⟪(WithLp.toLp 2 fun j => z (some (i, j)) : EuclideanSpace ℝ (Fin n)), x⟫) ∂μ)

Module navigation

Module: KLS/BKL/Suspension/Cumulant.

Definition modules: Analysis/BakryEmery/Cumulant/Basic, KLS/BKL/Suspension/Law, Probability/Line/Laplace.

Supporting theorems: joint_integrability_factorization.

Previous: joint_integrability_factorization · Next: exists_f_abs_exponential_moment.

Source excerpt, lines 272–280 · Frozen source 408915f.