Factor Integrability and Real Laplace Transform Factorization

This lemma states that joint exponential integrability yields integrability of each factor and a real-valued product formula.

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$, and $\sigma_\beta=\sqrt{1+2/\beta^2}$ (sigma). Put $\lambda=$ jointLaw $\mu\ f\ \beta\ \sigma_\beta\ N$, the law of the normalized suspension scalar and the $N$ copies, on $H=$ JointSpace $N\ n$. For $z\in H$, write $z_0$ for its scalar coordinate and $z_i\in E$ for its $i$th copy block.

Assume $p\mapsto e^{\langle z,p\rangle}$ is integrable under $\lambda$. Set $A(s)=e^{(z_0/\sigma_\beta)s}$ and $B_i(x)=e^{\frac{z_0}{\sigma_\beta\sqrt N}f(x)+\langle z_i,x\rangle}$. Then

This supplies the individual integrability conditions together with the real transform identity. The statement is an implication from joint integrability, not an equivalence.

Original Lean declaration header

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

theorem joint_integrability_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)) :
    Integrable (fun s : ℝ => Real.exp (z none / sigma β * s)) (laplaceMeasure β) ∧
      (∀ i : Fin N, Integrable (fun x => Real.exp
        (z none / (sigma β * Real.sqrt N) * f x +
          ⟪(WithLp.toLp 2 fun j => z (some (i, j)) : EuclideanSpace ℝ (Fin n)), x⟫)) μ) ∧
      (∫ p, Real.exp ⟪z, p⟫ ∂jointLaw μ f β (sigma β) N) =
        (∫ s : ℝ, Real.exp (z none / sigma β * s) ∂laplaceMeasure β) *
          ∏ i : Fin N, ∫ 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: KLS/BKL/Suspension/Law, Probability/Line/Laplace.

Supporting theorems: lintegral_exp_inner_jointLaw.

Previous: lintegral_exp_inner_jointLaw · Next: logLaplace_jointLaw_factorization.

Source excerpt, lines 212–224 · Frozen source 408915f.