Joint Smoothness of the Posterior Mean

Proved

FunctionalInequalities.Probability.Posterior.contDiff_posteriorMean_joint_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement proves joint smoothness of the posterior mean in the compact-prior setting.

Let $E$ be a finite-dimensional real inner-product space and let $\mu$ be a probability measure with compact support. For each $(c,Q)\in E\times(E\to_L E)$ , let posteriorMean μ c Q denote the mean of the corresponding posterior.

The vector-valued map

(c,Q)\longmapsto \operatorname{posteriorMean}(\mu,c,Q)

is infinitely continuously differentiable:

\operatorname{ContDiff}_{\mathbb R}^{\infty} \left((c,Q)\mapsto\operatorname{posteriorMean}(\mu,c,Q)\right).

This result applies to every finite operator parameter, including nonsymmetric $Q$ and $Q=0$ , without an isotropy assumption.

Original Lean declaration header

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

theorem contDiff_posteriorMean_joint (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) :
    ContDiff ℝ ∞ (fun p : E × (E →L[ℝ] E) => posteriorMean μ p.1 p.2)

Module navigation

Module: Probability/Posterior/JointRegularity.

Definition modules: Probability/Posterior/Generator.

Supporting theorems: contDiff_posteriorExpectation_joint, exists_uniform_norm_moments_tilted_quadraticExponent_of_compact.

Previous: contDiff_posteriorExpectation_joint · Next: contDiff_covariance_pair_joint.

Source excerpt, lines 225–227 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_JointRegularity

open MeasureTheory ProbabilityTheory FunctionalInequalities
open scoped RealInnerProductSpace ContDiff
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.Probability.Posterior.contDiff_posteriorMean_joint_readable (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) :
    ContDiff ℝ ∞ (fun p : E × (E →L[ℝ] E) => posteriorMean μ p.1 p.2) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/JointRegularity.lean#L223-L245 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.JointRegularity`, declaration `FunctionalInequalities.Probability.Posterior.contDiff_posteriorMean_joint`; the repository is private at upload time).

View graph