First-Coordinate Derivative of the Posterior Log-Laplace Transform

Proved

FunctionalInequalities.KLS.BKL.Localization.fderiv_logLaplace_fst_dir_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This gives the first-coordinate derivative of the posterior log-Laplace transform.

Let $\mu$ be a compactly supported probability measure on $\mathbb{R}^n$ , let $z,u\in\mathbb{R}^n$ , and let $p=(c,Q)$ be a localization parameter. Define

\Lambda_p(z)=\psi(c+z,Q)-\psi(c,Q).

Then

D_c\Lambda_p(z)[u] =\left\langle u,\operatorname{posteriorMean}(\mu,c+z,Q) -\operatorname{posteriorMean}(\mu,c,Q)\right\rangle.

This is a partial-derivative helper for the generator calculation of the posterior log-Laplace transform.

Original Lean declaration header

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

theorem fderiv_logLaplace_fst_dir (z : EuclideanSpace ℝ (Fin n)) (p : Param n)
    (u : EuclideanSpace ℝ (Fin n)) :
    fderiv ℝ (fun q : Param n => logPartition μ (q.1 + z) q.2 - logPartition μ q.1 q.2) p (u, 0) =
      ⟪u, 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.

Supporting theorems: contDiff_logPartition_joint, fderiv_logPartition_c_apply.

Previous: posteriorExpectation_exp_inner_eq_exp · Next: generator_logLaplace_posterior.

Source excerpt, lines 274–277 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_LogLaplaceGenerator

open scoped RealInnerProductSpace
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Probability.Diffusion
variable {n : ℕ} (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)
include hc

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.fderiv_logLaplace_fst_dir_readable (z : EuclideanSpace ℝ (Fin n)) (p : Param n)
    (u : EuclideanSpace ℝ (Fin n)) :
    fderiv ℝ (fun q : Param n => logPartition μ (q.1 + z) q.2 - logPartition μ q.1 q.2) p (u, 0) =
      ⟪u, posteriorMean μ (p.1 + z) p.2 - posteriorMean μ p.1 p.2⟫ := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/LogLaplaceGenerator.lean#L272-L298 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.LogLaplaceGenerator`, declaration `FunctionalInequalities.KLS.BKL.Localization.fderiv_logLaplace_fst_dir`; the repository is private at upload time).

View graph