Conditional Versus Unconditional Laplace Derivative Bound

Proved

FunctionalInequalities.Analysis.BakryEmery.norm_iteratedFDeriv_laplace_cond_sub_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an operator-norm estimate for moment tensors of a conditional measure.

Let $\nu$ be a probability measure on a finite-dimensional real inner-product space $E$ , let $r>0$ , and assume $e^{r\|x\|}$ is integrable with respect to $\nu$ . Let $s\subseteq E$ be measurable with $\nu(s)\ne0$ . For every $d\in\mathbb N$ ,

\left\|D^d\!\left(z\mapsto\int e^{\langle z,x\rangle}\,d\nu[\mid s](x)\right)(0) -D^d\!\left(z\mapsto\int e^{\langle z,x\rangle}\,d\nu(x)\right)(0)\right\|

\le \left|\bigl(\nu(s)^{-1}\bigr).\operatorname{toReal}-1\right|\int\|x\|^d\,d\nu(x)+\int_{s^c}\|x\|^d\,d\nu(x).

Here $\nu[\mid s]$ is the conditional probability measure on $s$ . The estimate quantifies the change in Laplace derivative tensors under conditioning.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.

theorem norm_iteratedFDeriv_laplace_cond_sub_le (ν : Measure E) [IsProbabilityMeasure ν]
    {r : ℝ} (hr : 0 < r) (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) ν) (d : ℕ)
    {s : Set E} (hs : MeasurableSet s) (hs0 : ν s ≠ 0) :
    ‖iteratedFDeriv ℝ d (fun z => ∫ x, Real.exp ⟪z, x⟫ ∂(ν[|s])) 0 -
        iteratedFDeriv ℝ d (fun z => ∫ x, Real.exp ⟪z, x⟫ ∂ν) 0‖ ≤
      |((ν s)⁻¹).toReal - 1| * ∫ x, ‖x‖ ^ d ∂ν + ∫ x in sᶜ, ‖x‖ ^ d ∂ν

Module navigation

Module: Analysis/BakryEmery/Cumulant/Truncation.

Next: tendsto_iteratedFDeriv_laplace_cond_closedBall.

Source excerpt, lines 59–64 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Truncation

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

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.norm_iteratedFDeriv_laplace_cond_sub_le_readable (ν : Measure E) [IsProbabilityMeasure ν]
    {r : ℝ} (hr : 0 < r) (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) ν) (d : ℕ)
    {s : Set E} (hs : MeasurableSet s) (hs0 : ν s ≠ 0) :
    ‖iteratedFDeriv ℝ d (fun z => ∫ x, Real.exp ⟪z, x⟫ ∂(ν[|s])) 0 -
        iteratedFDeriv ℝ d (fun z => ∫ x, Real.exp ⟪z, x⟫ ∂ν) 0‖ ≤
      |((ν s)⁻¹).toReal - 1| * ∫ x, ‖x‖ ^ d ∂ν + ∫ x in sᶜ, ‖x‖ ^ d ∂ν := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Cumulant/Truncation.lean#L58-L104 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Cumulant.Truncation`, declaration `FunctionalInequalities.Analysis.BakryEmery.norm_iteratedFDeriv_laplace_cond_sub_le`; the repository is private at upload time).

View graph