Samplinglib mathematical lesson

Compare entropy under a bounded change of probability law

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BoundedPerturbation.entropy_le_mul_of_measure_le · theorem · Teaching coverage

Read this first

Mathematical statement

Let μ and ν be probability measures on the same measurable space. If b ≥ 0, ν ≤ b μ, and g is nonnegative μ-almost everywhere with g and g log g μ-integrable, then Ent_ν(g) ≤ b Ent_μ(g). Integrability under ν is derived, including the zero-mean case.

\[\nu\le b\mu\quad\Longrightarrow\quad\operatorname{Ent}_\nu(g)\le b\operatorname{Ent}_\mu(g).\]

Lean statement · entropy_le_mul_of_measure_le

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 entropy_le_mul_of_measure_le {μ ν : Measure X}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {g : X → ℝ} {b : ℝ}
    (hb : 0 ≤ b) (hν : ν ≤ ENNReal.ofReal b • μ)
    (hg0 : 0 ≤ᵐ[μ] g) (hg : Integrable g μ)
    (hlog : Integrable (fun x => g x * Real.log (g x)) μ) :
    entropy ν g ≤ b * entropy μ g

Exact module and namespace context

Proof roadmap

1Use a nonnegative scalar cost
For s ≥ 0 and t > 0, the logarithm inequality gives Φ_t(s) = s log(s/t)-s+t ≥ 0. The case s=0 is handled separately, so no strict positivity of the test is assumed.
2Separate entropy from the cost at the mean
Linearity of the integrable terms and probability mass one give an exact identity. The cost at the target mean is nonnegative, hence every positive t is an upper bound on entropy.
3Compare the nonnegative costs under the two laws
Measure domination transports integrability and compares the integral of the nonnegative cost. Choose t equal to the positive reference mean; its reference cost at the mean vanishes.
4Discharge zero mean
A nonnegative integrable function with zero integral vanishes almost everywhere. Absolute continuity transfers this to the target law, so both displayed real entropies equal zero.

Full assumptions and notation

All objects and hypotheses

Objects, quantifiers, constants and all finite-integral restrictions are stated in the adjacent statement and exact Lean.
The test predicate and energy density are fixed before changing the measure; no differential operator is transported.

Mathematical proof

1. Use a nonnegative scalar cost

For s ≥ 0 and t > 0, the logarithm inequality gives Φ_t(s) = s log(s/t)-s+t ≥ 0. The case s=0 is handled separately, so no strict positivity of the test is assumed.

\[\Phi_t(s)=s\log(s/t)-s+t\ge0.\]

Corresponding Lean step

cost_nonneg uses Real.log_le_sub_one_of_pos and a zero split.

2. Separate entropy from the cost at the mean

Linearity of the integrable terms and probability mass one give an exact identity. The cost at the target mean is nonnegative, hence every positive t is an upper bound on entropy.

\[\int\Phi_t(g)\,d\mu=\operatorname{Ent}_\mu(g)+\Phi_t\!\left(\int g\,d\mu\right).\]

Corresponding Lean step

integrable_cost, integral_cost and entropy_le_integral_cost are private providers.

3. Compare the nonnegative costs under the two laws

Measure domination transports integrability and compares the integral of the nonnegative cost. Choose t equal to the positive reference mean; its reference cost at the mean vanishes.

\[\operatorname{Ent}_\nu(g)\le\int\Phi_m(g)\,d\nu\le b\int\Phi_m(g)\,d\mu=b\operatorname{Ent}_\mu(g).\]

Corresponding Lean step

Use integral_mono_measure after Integrable.smul_measure and mono_measure.

4. Discharge zero mean

A nonnegative integrable function with zero integral vanishes almost everywhere. Absolute continuity transfers this to the target law, so both displayed real entropies equal zero.

\[\int g\,d\mu=0\quad\Longrightarrow\quad g=0\quad\mu\text{-a.e. and }\nu\text{-a.e.}\]

Corresponding Lean step

Use integral_eq_zero_iff_of_nonneg_ae and absolutelyContinuous_of_le_smul.

Lean verification

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

Lean proof · entropy_le_mul_of_measure_le

See the adjacent exact source and the stepwise mathematical proof.

Download module (.lean)

theorem entropy_le_mul_of_measure_le {μ ν : Measure X}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {g : X → ℝ} {b : ℝ}
    (hb : 0 ≤ b) (hν : ν ≤ ENNReal.ofReal b • μ)
    (hg0 : 0 ≤ᵐ[μ] g) (hg : Integrable g μ)
    (hlog : Integrable (fun x => g x * Real.log (g x)) μ) :
    entropy ν g ≤ b * entropy μ g := by
  have hνμ : ν ≪ μ := Measure.absolutelyContinuous_of_le_smul hν
  have hgn : Integrable g ν := (hg.smul_measure ENNReal.ofReal_ne_top).mono_measure hν
  have hln : Integrable (fun x => g x * Real.log (g x)) ν :=
    (hlog.smul_measure ENNReal.ofReal_ne_top).mono_measure hν
  have hgn0 : 0 ≤ᵐ[ν] g := hνμ.ae_le hg0
  have hm0 : 0 ≤ ∫ x, g x ∂μ := integral_nonneg_of_ae hg0
  rcases hm0.eq_or_lt with hm | hm
  · have hgzero : g =ᵐ[μ] 0 := (integral_eq_zero_iff_of_nonneg_ae hg0 hg).1 hm.symm
    have hgnzero : g =ᵐ[ν] 0 := hνμ.ae_le hgzero
    have hlogzero : (fun x => g x * Real.log (g x)) =ᵐ[μ] 0 :=
      hgzero.mono fun x hx => by simp [hx]
    have hlognzero : (fun x => g x * Real.log (g x)) =ᵐ[ν] 0 :=
      hgnzero.mono fun x hx => by simp [hx]
    simp [entropy, integral_congr_ae hgzero, integral_congr_ae hgnzero,
      integral_congr_ae hlogzero, integral_congr_ae hlognzero]
  · calc
      entropy ν g ≤ ∫ x, cost (g x) (∫ y, g y ∂μ) ∂ν :=
        entropy_le_integral_cost hgn0 hgn hln hm
      _ ≤ ∫ x, cost (g x) (∫ y, g y ∂μ) ∂(ENNReal.ofReal b • μ) :=
        integral_mono_measure hν
          (by filter_upwards [Measure.ae_smul_measure hg0 (ENNReal.ofReal b)] with x hx
              exact cost_nonneg hx hm)
          ((integrable_cost hg hlog hm).smul_measure ENNReal.ofReal_ne_top)
      _ = b * entropy μ g := by
        rw [integral_smul_measure, ENNReal.toReal_ofReal hb, smul_eq_mul,
          integral_cost hg hlog hm]
        simp [cost]

/- The energy functional is held fixed while the probability law changes.
   For the usual gradient form choose Γ f = ‖∇f‖². -/

Exact module and namespace context

Scope and omitted-condition boundaries

Real-integral domain only; the extended-real entropy and arbitrary Sobolev closure are not supplied.
No geometric base LSI, gradient identification, PI, T2, diffusion, or model theorem is supplied.
No public manuscript identity or private application data is part of this contribution.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Real.log_le_sub_one_of_pos
MeasureTheory.integral_mono_measure
MeasureTheory.integral_eq_zero_iff_of_nonneg_ae
MeasureTheory.Measure.absolutelyContinuous_of_le_smul
MeasureTheory.Integrable.smul_measure
MeasureTheory.Integrable.mono_measure

Mathematical sources

Chewi, Log-Concave Sampling, August20 2026, §2.3.1 — Classical variational-cost and bounded-perturbation proof background; only the displayed canonical finite-integral core is asserted.

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