Existence of a Graph-Law Exponential Norm Moment

This lemma states existence of an exponential norm moment for the graph law from two separate exponential-moment assumptions.

Let $n\in\mathbb N$, $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)), $\mu$ a probability measure on $E$, and $f:E\to\mathbb R$ measurable. Let $a,s>0$ and assume

1. $x\mapsto e^{a|f(x)|}\in L^1(\mu)$.
2. $x\mapsto e^{s\|x\|}\in L^1(\mu)$.

Let $G:E\to\mathbb R^{\operatorname{Option}(\operatorname{Fin}n)}$ be the Euclidean graph map with $G(x)_{\mathrm{none}}=f(x)$ and $G(x)_{\mathrm{some}(j)}=x_j$, and let $\Gamma=G_*\mu$ (Measure.map). Then

This provides a local norm-moment condition on the joint vector $(f(x),x)$ for subsequent transform calculations. Only existence of a positive rate is asserted.

Original Lean declaration header

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

theorem exists_graph_norm_moment_of_local_moments {n : ℕ}
    (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsProbabilityMeasure μ]
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : Measurable f)
    {a s : ℝ} (ha : 0 < a) (hs : 0 < s)
    (hfa : Integrable (fun x => Real.exp (a * |f x|)) μ)
    (hxs : Integrable (fun x => Real.exp (s * ‖x‖)) μ) :
    ∃ t : ℝ, 0 < t ∧
      Integrable (fun y : EuclideanSpace ℝ (Option (Fin n)) => Real.exp (t * ‖y‖))
        (μ.map (fun x : EuclideanSpace ℝ (Fin n) =>
          (WithLp.toLp 2 fun o => Option.elim o (f x) fun j => x j :
            EuclideanSpace ℝ (Option (Fin n)))))

Module navigation

Module: KLS/BKL/Suspension/Cumulant.

Previous: exists_f_abs_exponential_moment.

Source excerpt, lines 362–372 · Frozen source 408915f.