Derivative of a Weighted Tilted Integral

Proved

FunctionalInequalities.Probability.Posterior.hasDerivAt_weighted_integral_of_compact_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the compact-support differentiation lemma preceding the posterior expectation formula.

Let $\mu$ be a probability measure on a topological, measurable, second-countable Borel space $\Omega$ , and assume its support is compact. Let $\phi,g:\Omega\to\mathbb R$ be continuous and let $f:\Omega\to\mathbb R$ be measurable. Assume that for some $C\ge0$ ,

\lVert f(x)\rVert\le C\quad\text{for every }x\in\operatorname{supp}\mu.

Then the map

t\longmapsto\int_\Omega e^{\phi(x)+t g(x)}f(x)\,d\mu(x)

has derivative at $t=0$ equal to

\int_\Omega e^{\phi(x)}g(x)f(x)\,d\mu(x).

This result supplies differentiation under the integral sign for unnormalized compactly supported tilts.

Original Lean declaration header

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

theorem hasDerivAt_weighted_integral_of_compact (μ : ProbabilityMeasure Ω)
    (hc : IsCompact (μ : Measure Ω).support) {φ g f : Ω → ℝ}
    (hφ : Continuous φ) (hg : Continuous g) (hf : Measurable f) {C : ℝ} (hC : 0 ≤ C)
    (hfb : ∀ x ∈ (μ : Measure Ω).support, ‖f x‖ ≤ C) :
    HasDerivAt (fun t : ℝ => ∫ x, Real.exp (φ x + t * g x) * f x ∂(μ : Measure Ω))
      (∫ x, Real.exp (φ x) * g x * f x ∂(μ : Measure Ω)) 0

Module navigation

Module: Probability/Posterior/CompactPrior.

Next: expectation_hasDerivAt_of_compact.

Source excerpt, lines 86–91 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_CompactPrior

open MeasureTheory Filter Topology ProbabilityTheory
variable {Ω : Type*} [TopologicalSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω]
  [SecondCountableTopology Ω]

Formal statement


theorem FunctionalInequalities.Probability.Posterior.hasDerivAt_weighted_integral_of_compact_readable (μ : ProbabilityMeasure Ω)
    (hc : IsCompact (μ : Measure Ω).support) {φ g f : Ω → ℝ}
    (hφ : Continuous φ) (hg : Continuous g) (hf : Measurable f) {C : ℝ} (hC : 0 ≤ C)
    (hfb : ∀ x ∈ (μ : Measure Ω).support, ‖f x‖ ≤ C) :
    HasDerivAt (fun t : ℝ => ∫ x, Real.exp (φ x + t * g x) * f x ∂(μ : Measure Ω))
      (∫ x, Real.exp (φ x) * g x * f x ∂(μ : Measure Ω)) 0 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/CompactPrior.lean#L85-L129 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.CompactPrior`, declaration `FunctionalInequalities.Probability.Posterior.hasDerivAt_weighted_integral_of_compact`; the repository is private at upload time).

View graph