Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

BoundedDensityPerturbation: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. The actual second-order entropy integral for bounded perturbations
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

  1. 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.

  2. 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.

  3. 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.

  4. 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.

  5. 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.

  6. 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.

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)) := 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

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