Existence of an Absolute Exponential Moment From the Joint Law

This lemma transfers existence of an exponential norm moment of the suspension joint law to an absolute exponential moment of the observable.

Let $n,N\in\mathbb N$ with $N>0$, let $\mu$ be a probability measure on $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)), and let $f:E\to\mathbb R$ be measurable. Let $\beta,r>0$, $\sigma_\beta=\sqrt{1+2/\beta^2}$ (sigma), and $\lambda=$ jointLaw $\mu\ f\ \beta\ \sigma_\beta\ N$. This is the law on JointSpace $N\ n$ of the scalar $(N^{-1/2}\sum_i f(X_i)+\eta)/\sigma_\beta$ and the copies, with independent Laplace noise $\eta$ of rate $\beta$.

Assume $p\mapsto e^{r\|p\|}$ is integrable under $\lambda$. Then

This is an existence result for a positive rate, useful for local transform regularity. Its conclusion does not prescribe a particular value of $t$.

Original Lean declaration header

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

theorem exists_f_abs_exponential_moment {n N : ℕ} (μ : Measure (EuclideanSpace ℝ (Fin n)))
    [IsProbabilityMeasure μ] {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : Measurable f)
    {β r : ℝ} (hβ : 0 < β) (hN : 0 < N) (hr : 0 < r)
    (hexp : Integrable (fun p : JointSpace N n => Real.exp (r * ‖p‖))
      (jointLaw μ f β (sigma β) N)) :
    ∃ t : ℝ, 0 < t ∧ Integrable (fun x => Real.exp (t * |f x|)) μ

Module navigation

Module: KLS/BKL/Suspension/Cumulant.

Definition modules: KLS/BKL/Suspension/Law.

Supporting theorems: joint_integrability_factorization.

Previous: logLaplace_jointLaw_factorization · Next: exists_graph_norm_moment_of_local_moments.

Source excerpt, lines 303–308 · Frozen source 408915f.