Posterior Expectation Derivative in the Linear Parameter

This is the $c$-direction derivative formula for a compact posterior expectation.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure. Let $\mu$ be a probability measure with compact support, let $f:E\to\mathbb R$ be measurable, and assume that for some $C\ge0$, $\lVert f(x)\rVert\le C$ on $\operatorname{supp}\mu$. For $c,h\in E$ and a continuous linear map $Q:E\to E$, the Fréchet derivative of

at $c$, applied to $h$, is

where $\mu_{c,Q}$ is the measure μ.tilted (quadraticExponent c Q). This is the gradient component of the deterministic posterior generator formalization.

Original Lean declaration header

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

theorem fderiv_posteriorExpectation_c_apply (μ : 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 : E →L[ℝ] E) (h : E) :
    fderiv ℝ (fun y => posteriorExpectation μ y Q f) c h =
      covariance f (fun x => ⟪h, x⟫) ((μ : Measure E).tilted (quadraticExponent c Q))

Module navigation

Module: Probability/Posterior/Generator.

Definition modules: Probability/Posterior/Exponent.

Supporting theorems: contDiff_posteriorExpectation_c, expectation_hasDerivAt_of_compact.

Previous: contDiff_posteriorExpectation_c · Next: bilinearIteratedFDerivTwo_posteriorExpectation_c.

Source excerpt, lines 118–123 · Frozen source 408915f.