Prove2Me

Posterior Expectation Hessian in the Linear Parameter

Proved
FunctionalInequalities.Probability.Posterior.bilinearIteratedFDerivTwo_posteriorExpectation_c_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the cc-Hessian formula for a compact posterior expectation.

Let EE be a finite-dimensional real inner-product space, let μ\mu be a compactly supported probability measure, and let f:E→Rf:E\to\mathbb R be measurable and bounded on the support by C≥0C\ge0. For c,h,k∈Ec,h,k\in E and a continuous linear map QQ, let ν=μ.tilted⁡(quadraticExponent⁡(c,Q))\nu=\mu.\operatorname{tilted}(\operatorname{quadraticExponent}(c,Q)). Then

Dc2Eν[f](h,k)=Cov⁡ν(f,x↦⟨h,x⟩⟨k,x⟩)−(∫⟨h,x⟩ dν)Cov⁡ν(f,⟨k,x⟩)−(∫⟨k,x⟩ dν)Cov⁡ν(f,⟨h,x⟩).D_c^2\mathbb E_{\nu}[f](h,k) =\operatorname{Cov}_{\nu}\bigl(f,x\mapsto\langle h,x\rangle\langle k,x\rangle\bigr) -\left(\int\langle h,x\rangle\,d\nu\right)\operatorname{Cov}_{\nu}\bigl(f,\langle k,x\rangle\bigr) -\left(\int\langle k,x\rangle\,d\nu\right)\operatorname{Cov}_{\nu}\bigl(f,\langle h,x\rangle\bigr).

Here bilinearIteratedFDerivTwo is the bilinear second derivative. The identity is the second-order deterministic ingredient for the posterior generator.

Original Lean declaration header

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

theorem bilinearIteratedFDerivTwo_posteriorExpectation_c (μ : 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 k : E) :
    bilinearIteratedFDerivTwo ℝ (fun y => posteriorExpectation μ y Q f) c h k =
      covariance f (fun x => ⟪h, x⟫ * ⟪k, x⟫) ((μ : Measure E).tilted (quadraticExponent c Q)) -
        (∫ x, ⟪h, x⟫ ∂((μ : Measure E).tilted (quadraticExponent c Q))) *
          covariance f (fun x => ⟪k, x⟫) ((μ : Measure E).tilted (quadraticExponent c Q)) -
        (∫ x, ⟪k, x⟫ ∂((μ : Measure E).tilted (quadraticExponent c Q))) *
          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, covariance_hasDerivAt_of_compact, fderiv_posteriorExpectation_c_apply.

Previous: fderiv_posteriorExpectation_c_apply · Next: sum_bilinearIteratedFDerivTwo_posteriorExpectation_c.

Source excerpt, lines 139–148 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_Generator

open MeasureTheory Filter Topology ProbabilityTheory
open scoped RealInnerProductSpace ContDiff
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
Formal statement

theorem FunctionalInequalities.Probability.Posterior.bilinearIteratedFDerivTwo_posteriorExpectation_c_readable (μ : 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 k : E) :
    bilinearIteratedFDerivTwo ℝ (fun y => posteriorExpectation μ y Q f) c h k =
      covariance f (fun x => ⟪h, x⟫ * ⟪k, x⟫) ((μ : Measure E).tilted (quadraticExponent c Q)) -
        (∫ x, ⟪h, x⟫ ∂((μ : Measure E).tilted (quadraticExponent c Q))) *
          covariance f (fun x => ⟪k, x⟫) ((μ : Measure E).tilted (quadraticExponent c Q)) -
        (∫ x, ⟪k, x⟫ ∂((μ : Measure E).tilted (quadraticExponent c Q))) *
          covariance f (fun x => ⟪h, x⟫) ((μ : Measure E).tilted (quadraticExponent c Q)) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/Generator.lean#L138-L169 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.Generator`, declaration `FunctionalInequalities.Probability.Posterior.bilinearIteratedFDerivTwo_posteriorExpectation_c`; the repository is private at upload time).

View graph