Uniform Posterior Bounds for All Norm Moments

This statement formalizes a uniform moment bound in the compact-prior stage associated with Equation (67), p. 19, of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $E$ be a finite-dimensional real inner-product space and let $\mu$ be a probability measure with compact support. Then there exists a radius $R\in\mathbb R$ such that $0\leq R$ and, for every $c\in E$, every continuous linear map $Q:E\to E$, and every $p\in\mathbb N$, the posterior associated with quadraticExponent c Q satisfies

1. $x\mapsto\|x\|^p$ is integrable under the tilted measure;
2. its moment is bounded by $R^p$:

The same support radius works uniformly for all finite parameters $(c,Q)$ and all natural exponents $p$. The conclusion is an existence statement for $R$, not a claim that a particular displayed radius is chosen.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.Posterior. Shown in its original module context. Proof omitted.

theorem exists_uniform_norm_moments_tilted_quadraticExponent_of_compact (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) :
    ∃ R : ℝ, 0 ≤ R ∧ ∀ (c : E) (Q : E →L[ℝ] E) (p : ℕ),
      Integrable (fun x => ‖x‖ ^ p) ((μ : Measure E).tilted (quadraticExponent c Q)) ∧
      (∫ x, ‖x‖ ^ p ∂((μ : Measure E).tilted (quadraticExponent c Q))) ≤ R ^ p

Module navigation

Module: Probability/Posterior/CompactQuadratic.

Definition modules: Probability/Posterior/Exponent.

Supporting theorems: norm_integral_tilted_le_of_compact.

Source excerpt, lines 60–64 · Frozen source 408915f.