Joint Smoothness of Posterior Covariances

This theorem states the joint $C^\infty$ regularity of posterior covariances of two linear statistics.

Let $E$ be a finite-dimensional real inner-product space equipped with a measurable structure and its Borel structure. Let $\mu$ be a probability measure on $E$ such that its measure-theoretic support is compact. For arbitrary vectors $u,v\in E$, let $p=(c,Q)$ range over $E\times(E\to_L[\mathbb R]E)$, where $c\in E$ and $Q$ is a continuous linear operator from $E$ to $E$. The posterior measure at $p$ is the tilted measure (μ : Measure E).tilted (quadraticExponent c Q).

The covariance of the linear statistics $x\mapsto\langle u,x\rangle$ and $x\mapsto\langle v,x\rangle$ under this tilted measure is infinitely continuously differentiable jointly in $(c,Q)$:

This is a technical regularity result that can be reused when differentiating posterior covariance expressions with respect to both the linear parameter and the quadratic operator parameter. It applies to arbitrary $u$ and $v$, including when $Q=0$, and does not require isotropy of the prior.

Formalization Note The conclusion is the Lean predicate ContDiff ℝ ∞ on the product space $E\times(E\to_L[\mathbb R]E)$, with the operator space carrying its usual operator-norm structure. The covariance is formed with respect to the tilted measure and the statement does not assert any covariance identity beyond its joint smoothness.

Original Lean declaration header

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

theorem contDiff_covariance_pair_joint (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (u v : E) :
    ContDiff ℝ ∞ (fun p : E × (E →L[ℝ] E) =>
      covariance (fun x => ⟪u, x⟫) (fun x => ⟪v, x⟫)
        ((μ : Measure E).tilted (quadraticExponent p.1 p.2)))

Module navigation

Module: Probability/Posterior/JointRegularity.

Definition modules: Probability/Posterior/Exponent.

Supporting theorems: contDiff_posteriorExpectation_joint.

Previous: contDiff_posteriorMean_joint · Next: contDiff_posteriorCovariance_joint.

Source excerpt, lines 249–253 · Frozen source 408915f.