Posterior Log-Laplace Generator Identity

This formalizes the generator form of BKL (71), cited as Lemma 4.3, p. 20, of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $n\in\mathbb N$, let $\mu$ be a probability measure on $\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$, and assume: (1) the support of $\mu$ is compact; (2) $\mu$ is isotropic in the sense of KLS.Isotropic. Let $z\in\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$ and let $p=(c,Q)$ be a localization parameter in Param n.

Define $\Lambda_p(z)=\log Z_\mu(c+z,Q)-\log Z_\mu(c,Q)$, where logPartition is $\log Z_\mu$, and define $v=a_\mu(c+z,Q)-a_\mu(c,Q)$ using posteriorMean. Then

The inverse is the Ring.inverse of the covariance operator at $p$; no invertibility conclusion is asserted separately because isotropy and compactness are hypotheses of the identity. This is a pointwise generator formula for later localization calculations.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem generator_logLaplace_posterior (hiso : KLS.Isotropic μ) (z : EuclideanSpace ℝ (Fin n))
    (p : Param n) :
    generator μ hc (fun q : Param n => logPartition μ (q.1 + z) q.2 - logPartition μ q.1 q.2) p =
      -(1 / 2 : ℝ) * ⟪posteriorMean μ (p.1 + z) p.2 - posteriorMean μ p.1 p.2,
        Ring.inverse (cov μ hc p) (posteriorMean μ (p.1 + z) p.2 - posteriorMean μ p.1 p.2)⟫

Module navigation

Module: KLS/BKL/Localization/LogLaplaceGenerator.

Definition modules: Probability/Posterior/Generator, KLS/BKL/Localization/Coefficients, Probability/Posterior/LogPartition, KLS/Isotropic.

Selected supporting theorems: inner_self_pos_of_isPositive_of_isUnit, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, fderiv_logLaplace_fst_dir, generator_posteriorExpectation_exp_inner, posteriorExpectation_exp_inner_eq_exp.

Previous: fderiv_logLaplace_fst_dir.

Source excerpt, lines 303–307 · Frozen source 408915f.