Smoothness of the Unnormalized Quadratic-Exponential Integral

This statement formalizes the smoothness of the unnormalized posterior integral; it is part of the compact-prior stage preceding Equation (67) 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. Let $f:E\to\mathbb R$ be measurable. Let $C\in\mathbb R$ satisfy $0\leq C$, and assume $\|f(x)\|\leq C$ on the support of $\mu$. Fix a continuous linear map $Q:E\to E$.

The map of the linear parameter $c\in E$ defined by

is $C^\infty$, where $E_{c,Q}(x)$ is quadraticExponent c Q x:

This is an unnormalized-integral regularity result and does not assert regularity in $Q$.

Original Lean declaration header

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

theorem contDiff_weighted_integral_quadraticExponent_of_compact (μ : ProbabilityMeasure E) (hc : IsCompact (μ : Measure E).support)
    {f : E → ℝ} (hf : Measurable f) {C : ℝ} (hC : 0 ≤ C)
    (hfb : ∀ x ∈ (μ : Measure E).support, ‖f x‖ ≤ C) (Q : E →L[ℝ] E) :
    ContDiff ℝ ∞ (fun c : E => ∫ x, Real.exp (quadraticExponent c Q x) * f x ∂(μ : Measure E))

Module navigation

Module: Probability/Posterior/Generator.

Definition modules: Probability/Posterior/Exponent.

Supporting theorems: integrable_exp_norm_mul_of_compact.

Previous: integrable_exp_norm_mul_of_compact · Next: contDiff_posteriorExpectation_c.

Source excerpt, lines 62–65 · Frozen source 408915f.