Joint Smoothness of Compact Posterior Expectations

This statement formalizes the joint smoothness assertion 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. Let $f:E\to\mathbb R$ be measurable, and suppose there is $C\in\mathbb R$ such that

for every $x$ in the support of $\mu$. No nonnegativity assumption on $C$ appears in the type.

Then the map on the product of the linear parameter and operator parameter is infinitely continuously differentiable:

for $(c,Q)\in E\times(E\to_L E)$. The result includes arbitrary finite $Q$, including $Q=0$ and nonsymmetric operators, and does not impose isotropy on $\mu$.

Original Lean declaration header

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

theorem contDiff_posteriorExpectation_joint (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) {f : E → ℝ} (hf : Measurable f)
    {C : ℝ} (hb : ∀ x ∈ (μ : Measure E).support, ‖f x‖ ≤ C) :
    ContDiff ℝ ∞ (fun p : E × (E →L[ℝ] E) => posteriorExpectation μ p.1 p.2 f)

Module navigation

Module: Probability/Posterior/JointRegularity.

Definition modules: Probability/Posterior/Generator.

Supporting theorems: contDiff_posteriorExpectation_c.

Next: contDiff_posteriorMean_joint.

Source excerpt, lines 188–191 · Frozen source 408915f.