Samplinglib mathematical lesson

The actual second-order entropy integral for bounded perturbations

AutoSamplingTheory.TechnicalLemmas.InformationTheory.BoundedDensityPerturbation.tendsto_integral_klFun_one_add_mul_div_sq · theorem · Teaching coverage

Read this first

Mathematical statement

Let mu be a finite measure on any measurable space, and let f be real-valued, a.e. strongly measurable and uniformly a.e. bounded by some finite real M. The compensated entropy integral of 1+epsilon*f, divided by epsilon squared, tends as nonzero real epsilon tends to zero to one half of the integral of f squared. No centering, probability normalization, differentiability of f or supplied convergence certificate is needed for this compensated statement.

\[q(u)=u\log u-u+1,\qquad\lim_{\varepsilon\to0,\,\varepsilon\ne0}\frac{\int q(1+\varepsilon f)\,d\mu}{\varepsilon^2}=\frac12\int f^2\,d\mu.\]

Lean statement · tendsto_integral_klFun_one_add_mul_div_sq

The exact statement quantifies over any measurable carrier and finite measure, with one a.e. bound. It concerns the compensated klFun integral, not canonical klDiv of probability laws.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem tendsto_integral_klFun_one_add_mul_div_sq
    {X : Type*} [MeasurableSpace X] (mu : Measure X) [IsFiniteMeasure mu]
    (f : X → ℝ) (hf : AEStronglyMeasurable f mu) {M : ℝ}
    (hbound : ∀ᵐ x ∂mu, |f x| ≤ M) :
    Tendsto (fun e : ℝ => (∫ x, _root_.InformationTheory.klFun (1 + e * f x) ∂mu) / e ^ 2)
      (𝓝[≠] (0 : ℝ)) (𝓝 ((∫ x, f x ^ 2 ∂mu) / 2))

Exact module and namespace context

Proof roadmap

1Compensate the first-order term
Use Mathlib's existing klFun rather than defining another entropy. Substitution cancels the constant term. Centering is unnecessary at this stage: subtracting epsilon*f is part of the integrand, not a theorem hypothesis.
2Prove the scalar coefficient using genuine derivatives
For a fixed real a, the logarithm is genuinely differentiable near epsilon=0 because its argument is near 1, not 0. Its slope quotient tends to a. Differentiate the compensated numerator and epsilon squared, then apply punctured two-sided L'Hopital. This includes a=0 without dividing by a.
3Construct the quadratic envelope
For u≥0, convexity gives q(u)≥0. The elementary log inequality log(u)≤u-1 gives q(u)≤(u-1)^2 for u>0; handle u=0 separately. Boundedness makes |epsilon|*|M|<1 eventually and hence 1+epsilon*f>0 almost everywhere. Divide the envelope by epsilon squared only for nonzero epsilon.
4Discharge measurability and integrability
Finite measure and the essential bound imply that f squared is integrable. Continuity of klFun and the measurable arithmetic operations make every parameter integrand a.e. strongly measurable. These are produced inside the proof rather than assumed as certificates.
5Pass the actual limit through the integral
Apply filter dominated convergence with the single integrable dominator f squared. The pointwise limit is the scalar result, and the bounds hold eventually almost everywhere. Pull the parameter-dependent scalar outside each Bochner integral to obtain exactly the displayed quotient limit.
6Keep the source consumers separate
For a probability law and centered f, the later adapter must prove that the actual positive density has mass one, identify its Radon-Nikodym derivative and finite canonical KL, and remove the compensated linear term. The LSI application, Fisher limit and exact PI test domain require their own proofs. Centering a compact function generally leaves the function noncompact, although its gradient remains compactly supported.

Full assumptions and notation

All objects and hypotheses

The measure mu is finite. It need not be a probability law, nonzero, sigma-finite by a separate premise, or defined by a smooth Gibbs density.
The real function f is a.e. strongly measurable and |f| ≤ M almost everywhere for one finite real M. No pointwise representative, smoothness or compact support is required. The proof uses |M|, so no extra M≥0 premise or division by M is introduced.
The parameter limit is the two-sided punctured real neighborhood of zero. The totalized quotient value at epsilon=0 is irrelevant. The logarithm arguments are proved positive eventually almost everywhere.

Mathematical proof

1. Compensate the first-order term

Use Mathlib's existing klFun rather than defining another entropy. Substitution cancels the constant term. Centering is unnecessary at this stage: subtracting epsilon*f is part of the integrand, not a theorem hypothesis.

\[q(1+\varepsilon f)=(1+\varepsilon f)\log(1+\varepsilon f)-\varepsilon f.\]

Corresponding Lean step

The statement uses InformationTheory.klFun. Its literal definition is x*log(x)+1-x.

2. Prove the scalar coefficient using genuine derivatives

For a fixed real a, the logarithm is genuinely differentiable near epsilon=0 because its argument is near 1, not 0. Its slope quotient tends to a. Differentiate the compensated numerator and epsilon squared, then apply punctured two-sided L'Hopital. This includes a=0 without dividing by a.

\[\frac{\log(1+\varepsilon a)}{\varepsilon}\longrightarrow a,\qquad\frac{q(1+\varepsilon a)}{\varepsilon^2}\longrightarrow\frac{a^2}{2}.\]

Corresponding Lean step

The private scalar_limit uses hasDerivAt_klFun, Real.hasDerivAt_log, HasDerivAt.tendsto_slope_zero and HasDerivAt.lhopital_zero_nhdsNE. No conclusion is read from a totalized derivative at zero.

3. Construct the quadratic envelope

For u≥0, convexity gives q(u)≥0. The elementary log inequality log(u)≤u-1 gives q(u)≤(u-1)^2 for u>0; handle u=0 separately. Boundedness makes |epsilon|*|M|<1 eventually and hence 1+epsilon*f>0 almost everywhere. Divide the envelope by epsilon squared only for nonzero epsilon.

\[0\le q(u)\le(u-1)^2,\qquad0\le\frac{q(1+\varepsilon f)}{\varepsilon^2}\le f^2.\]

Corresponding Lean step

klFun_nonneg and the private klFun_upper produce the bounds. The eventually-small parameter and the a.e. bound are combined explicitly; mul_div_cancel_left0 cancels the nonzero square.

4. Discharge measurability and integrability

Finite measure and the essential bound imply that f squared is integrable. Continuity of klFun and the measurable arithmetic operations make every parameter integrand a.e. strongly measurable. These are produced inside the proof rather than assumed as certificates.

\[f^2\le |M|^2\quad\mu\text{-a.e.},\qquad\int |M|^2\,d\mu<\infty.\]

Corresponding Lean step

Integrable.mono' starts from integrable_const. continuous_klFun.comp_aestronglyMeasurable constructs the parameter integrands.

5. Pass the actual limit through the integral

Apply filter dominated convergence with the single integrable dominator f squared. The pointwise limit is the scalar result, and the bounds hold eventually almost everywhere. Pull the parameter-dependent scalar outside each Bochner integral to obtain exactly the displayed quotient limit.

\[\int\frac{q(1+\varepsilon f)}{\varepsilon^2}\,d\mu\longrightarrow\int\frac{f^2}{2}\,d\mu=\frac12\int f^2\,d\mu.\]

Corresponding Lean step

Use tendsto_integral_filter_of_dominated_convergence followed by integral_div.

6. Keep the source consumers separate

For a probability law and centered f, the later adapter must prove that the actual positive density has mass one, identify its Radon-Nikodym derivative and finite canonical KL, and remove the compensated linear term. The LSI application, Fisher limit and exact PI test domain require their own proofs. Centering a compact function generally leaves the function noncompact, although its gradient remains compactly supported.

\[\int f\,d\pi=0\quad\Longrightarrow\quad\int(1+\varepsilon f)\,d\pi=1.\]

Corresponding Lean step

These are downstream obligations, not conclusions of this declaration or new public assumptions on a complete Exercise 1.7 theorem.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · tendsto_integral_klFun_one_add_mul_div_sq

A scalar genuine-derivative limit plus a uniform quadratic envelope feed a fully discharged filter dominated-convergence argument. Private helpers share the public result's whole-module review and earn no separate leaf credit.

Download module (.lean)

theorem tendsto_integral_klFun_one_add_mul_div_sq
    {X : Type*} [MeasurableSpace X] (mu : Measure X) [IsFiniteMeasure mu]
    (f : X → ℝ) (hf : AEStronglyMeasurable f mu) {M : ℝ}
    (hbound : ∀ᵐ x ∂mu, |f x| ≤ M) :
    Tendsto (fun e : ℝ => (∫ x, _root_.InformationTheory.klFun (1 + e * f x) ∂mu) / e ^ 2)
      (𝓝[≠] (0 : ℝ)) (𝓝 ((∫ x, f x ^ 2 ∂mu) / 2)) := by
  have hsq : Integrable (fun x => f x ^ 2) mu := by
    refine (integrable_const (|M| ^ 2)).mono' (hf.pow 2) ?_
    filter_upwards [hbound] with x hx
    simpa only [Real.norm_eq_abs, abs_pow] using
      pow_le_pow_left₀ (abs_nonneg (f x)) (hx.trans (le_abs_self M)) 2
  have hsmall : ∀ᶠ e : ℝ in 𝓝 (0 : ℝ), |e| * |M| < 1 :=
    (isOpen_lt (continuous_abs.mul continuous_const) continuous_const).mem_nhds (by simp)
  have hlimit := tendsto_integral_filter_of_dominated_convergence (μ := mu)
    (F := fun e : ℝ => fun x => _root_.InformationTheory.klFun (1 + e * f x) / e ^ 2)
    (f := fun x => f x ^ 2 / 2) (l := 𝓝[≠] (0 : ℝ)) (fun x => f x ^ 2)
    (Filter.Eventually.of_forall fun e =>
      (by simpa only [div_eq_mul_inv, Pi.add_apply] using
        (_root_.InformationTheory.continuous_klFun.comp_aestronglyMeasurable
          (aestronglyMeasurable_const.add (hf.const_mul e))).mul_const ((e ^ 2)⁻¹)))
    ?_ hsq (ae_of_all mu fun x => scalar_limit (f x))
  · simpa only [integral_div] using hlimit
  · filter_upwards [hsmall.filter_mono nhdsWithin_le_nhds, self_mem_nhdsWithin] with e he he0
    have hne : e ≠ 0 := by simpa using he0
    filter_upwards [hbound] with x hx
    have habs : |e * f x| < 1 := by
      rw [abs_mul]
      exact (mul_le_mul_of_nonneg_left (hx.trans (le_abs_self M)) (abs_nonneg e)).trans_lt he
    have hpos : 0 < 1 + e * f x := by linarith [neg_abs_le (e * f x)]
    have hn := _root_.InformationTheory.klFun_nonneg (le_of_lt hpos)
    have hu : _root_.InformationTheory.klFun (1 + e * f x) ≤ (e * f x) ^ 2 := by
      simpa using klFun_upper (le_of_lt hpos)
    rw [Real.norm_eq_abs, abs_of_nonneg (div_nonneg hn (sq_nonneg e))]
    calc
      _ ≤ (e * f x) ^ 2 / e ^ 2 := div_le_div_of_nonneg_right hu (sq_nonneg e)
      _ = f x ^ 2 := by rw [mul_pow, mul_div_cancel_left₀ _ (pow_ne_zero 2 hne)]

end AutoSamplingTheory.TechnicalLemmas.InformationTheory.BoundedDensityPerturbation

Exact module and namespace context

Scope and omitted-condition boundaries

No probability-law construction, canonical KL identity/finiteness, Fisher limit, LSI-domain extension, PI, T2 or complete exercise is proved.
The generic finite-measure and bounded-measurable domain is a disclosed prerequisite generalization, not a weakened claim that the full textbook theorem is finished.
Source-only exercise topology review is not a Lean equivalence audit. Semantic reconstruction, independent verification, integration and reader purification require their own canonical evidence; compilation alone certifies none of them.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

InformationTheory.klFun
InformationTheory.hasDerivAt_klFun
InformationTheory.klFun_nonneg
Real.log_le_sub_one_of_pos
HasDerivAt.tendsto_slope_zero
HasDerivAt.lhopital_zero_nhdsNE
MeasureTheory.tendsto_integral_filter_of_dominated_convergence
MeasureTheory.integral_div

Mathematical sources

Chewi, Log-Concave Sampling, August 20 2026, Exercise 1.7 / (1.E.1) — ASTIS-authored analytic expansion of the omitted compensated-integral prerequisite; full KL/LSI/PI remain separate.
Chewi, Corollary 2.1.2 — The proof explicitly reuses (1.E.1) for bounded centered smooth functions with compactly supported gradient, not necessarily compactly supported functions.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.