Log-Laplace Formula for Compact Posteriors

This statement gives the log-Laplace identity for a compactly supported linear–quadratic posterior.

Let $E$ be a complete finite-dimensional real inner-product space, let $\mu$ be a probability law with compact support, let $c,z\in E$, and let $Q:E\to E$ be continuous linear. For the compact posterior $\mu_{c,Q}$ and the log-partition function $\psi=\texttt{logPartition}\,\mu$, one has

where $\Lambda$ is Analysis.BakryEmery.logLaplace. The identity is a direct formula for the posterior log-Laplace transform and is reusable in derivative and cumulant calculations.

Original Lean declaration header

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

omit [CompleteSpace E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] in
theorem logLaplace_compactPosterior
    [CompleteSpace E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E]
    (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (c : E) (Q : E →L[ℝ] E) (z : E) :
    Analysis.BakryEmery.logLaplace (compactPosterior μ hc c Q : Measure E) z =
      logPartition μ (c + z) Q - logPartition μ c Q

Module navigation

Module: Probability/Posterior/LogPartition.

Definition modules: Analysis/BakryEmery/Cumulant/Basic, Probability/Posterior/CompactDomain.

Previous: contDiff_logPartition_joint · Next: cumulant_compactPosterior.

Source excerpt, lines 204–212 · Frozen source 408915f.