Derivative of a Tilted Covariance

This is the compact-support derivative formula for a tilted covariance.

Let $\mu$ be a compactly supported probability measure on a topological, measurable, second-countable Borel space. Let $\phi,g,k$ be continuous and let $f$ be measurable and bounded on $\operatorname{supp}\mu$ by some $C\ge0$. Then

where $\nu=\mu.\operatorname{tilted}(\phi)$. This provides the covariance derivative needed for second-order posterior calculations.

Original Lean declaration header

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

theorem covariance_hasDerivAt_of_compact (μ : ProbabilityMeasure Ω)
    (hc : IsCompact (μ : Measure Ω).support) {φ g k f : Ω → ℝ}
    (hφ : Continuous φ) (hg : Continuous g) (hk : Continuous k) (hf : Measurable f)
    {C : ℝ} (hC : 0 ≤ C) (hfb : ∀ x ∈ (μ : Measure Ω).support, ‖f x‖ ≤ C) :
    HasDerivAt (fun t : ℝ => covariance f k
      ((μ : Measure Ω).tilted (fun x => φ x + t * g x)))
      (covariance f (fun x => g x * k x) ((μ : Measure Ω).tilted φ) -
        (∫ x, g x ∂((μ : Measure Ω).tilted φ)) * covariance f k ((μ : Measure Ω).tilted φ) -
        (∫ x, k x ∂((μ : Measure Ω).tilted φ)) * covariance f g ((μ : Measure Ω).tilted φ)) 0

Module navigation

Module: Probability/Posterior/CompactPrior.

Supporting theorems: expectation_hasDerivAt_of_compact.

Previous: norm_integral_tilted_le_of_compact.

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