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

The totalized density-entropy integral

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.densityEntropy · def · Teaching coverage

Read this first

Mathematical statement

For any measure μ on a measurable space E and any real-valued function ρ, define densityEntropy μ ρ=∫ρ logρ dμ using Mathlib's totalized real logarithm. No nonnegative-density, normalization, probability, or integrability condition is included in this definition.

\[H_\mu(\rho):=\int_E\rho(x)\operatorname{Real.log}(\rho(x))\,d\mu(x),\qquad0\cdot\operatorname{Real.log}(0)=0.\]
Lean statement · densityEntropy

The name suggests a density interpretation, but the signature accepts arbitrary real functions and arbitrary measures. The later admissibility predicate supplies the conditions needed for that interpretation.

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)
noncomputable def densityEntropy (mu : Measure E) (rho : E → ℝ) : ℝ

Exact module and namespace context

Proof roadmap

  1. 1Form the entropy integrand

    Multiply each value of ρ by its totalized real logarithm. At zero the product is zero. Values of ρ are not restricted by this definition.

  2. 2Integrate against the explicit base

    Take the real Bochner integral of u, with its standard totalization outside the integrable domain.

Full assumptions and notation

All objects and hypotheses

  • E is any measurable space and μ is any measure on E, unless probability normalization is explicitly included below. No topology, norm, finite dimension, σ-finiteness, or nonempty-space premise is imposed.
  • ρ:E→ℝ is arbitrary; it is not supplied as a selected RN representative, nor assumed nonnegative or normalized.
  • No operator is an input and no integrability hypothesis is required to form the expression.

Construction and meaning

1. Form the entropy integrand

Multiply each value of ρ by its totalized real logarithm. At zero the product is zero. Values of ρ are not restricted by this definition.

\[u(x):=\rho(x)\operatorname{Real.log}(\rho(x)).\]
Corresponding Lean step

Real.log

2. Integrate against the explicit base

Take the real Bochner integral of u, with its standard totalization outside the integrable domain.

\[H_\mu(\rho)=\int_Eu\,d\mu.\]
Corresponding Lean step

MeasureTheory.integral; Generator.densityEntropy

Lean verification

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

Lean construction · densityEntropy

This is a construction, not a KL theorem. It forms the product with the real logarithm and integrates it; it neither constructs a density measure nor identifies this expression with canonical KL.

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)
noncomputable def densityEntropy (mu : Measure E) (rho : E → ℝ) : ℝ :=
  ∫ x, rho x * Real.log (rho x) ∂mu

Exact module and namespace context

Scope and omitted-condition boundaries
  • All integrals are real Bochner integrals. An integral is totalized to zero when its integrand is not integrable; writing the integral does not prove a genuine finite expectation or energy.
  • No equality with InformationTheory.klDiv, no nonnegativity, and no genuine relative-entropy interpretation is established for arbitrary signed or unnormalized ρ.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • Real.log
    • MeasureTheory.integral

    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.