Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

The totalized density-entropy integral

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

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.\]

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

noncomputable def densityEntropy (mu : Measure E) (rho : E → ℝ) : ℝ

Exact module and namespace context

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.

noncomputable def densityEntropy (mu : Measure E) (rho : E → ℝ) : ℝ :=
  ∫ x, rho x * Real.log (rho x) ∂mu

/-- Domain conditions for the density formulation of log-Sobolev. -/

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

Source and reuse

ASTIS parents called

    Mathlib API called (external library)

    • Real.log
    • MeasureTheory.integral

    Mathematical sources

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