Trace of the Posterior Expectation Hessian

This is the trace formula for the posterior expectation Hessian against a symmetric operator.

Let $E$ be a finite-dimensional complete real inner-product space, let $\mu$ be compactly supported, and let $f$ be measurable and bounded on the support by $C\ge0$. Let $Q,M:E\to E$ be continuous linear maps, let $(b_i)$ be an orthonormal basis indexed by a finite type $\iota$, and assume $M$ is self-adjoint:

For $\nu=\mu.\operatorname{tilted}(\operatorname{quadraticExponent}(c,Q))$ and $a=\operatorname{posteriorMean}(\mu,c,Q)$,

This converts the Hessian contribution into the covariance expression used in the generator calculation.

Original Lean declaration header

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

theorem sum_bilinearIteratedFDerivTwo_posteriorExpectation_c (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) {f : E → ℝ} (hf : Measurable f)
    {C : ℝ} (hC : 0 ≤ C) (hfb : ∀ x ∈ (μ : Measure E).support, ‖f x‖ ≤ C)
    (c : E) (Q M : E →L[ℝ] E) (b : OrthonormalBasis ι ℝ E)
    (hM : ∀ u v : E, ⟪M u, v⟫ = ⟪u, M v⟫) :
    (∑ i, bilinearIteratedFDerivTwo ℝ (fun y => posteriorExpectation μ y Q f) c (M (b i)) (b i)) =
      covariance f (fun x => ⟪M x, x⟫) ((μ : Measure E).tilted (quadraticExponent c Q)) -
        2 * covariance f (fun x => ⟪M (posteriorMean μ c Q), x⟫)
          ((μ : Measure E).tilted (quadraticExponent c Q))

Module navigation

Module: Probability/Posterior/Generator.

Definition modules: Probability/Posterior/Exponent.

Supporting theorems: bilinearIteratedFDerivTwo_posteriorExpectation_c, exists_uniform_norm_moments_tilted_quadraticExponent_of_compact.

Previous: bilinearIteratedFDerivTwo_posteriorExpectation_c.

Source excerpt, lines 213–221 · Frozen source 408915f.