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

The real conversion of KL equals the totalized log-ratio integral

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.toReal_klDiv_eq_integral_logRatio_of_probability · theorem · Teaching coverage

Statement

Let μ and π be probability measures on a measurable space α, and suppose μ≪π. Then the real conversion of Mathlib's extended-valued KL divergence equals the real Bochner integral of the selected log-ratio under μ. No log-ratio integrability or finite-KL assumption is present; the equality is also valid in the nonintegrable case, when both displayed real quantities are zero by totalization.

\[\operatorname{toReal}\!\left(\mathrm{KL}(\mu\Vert\pi)\right)=\int_\alpha r_{\mu,\pi}(x)\,d\mu(x).\]

All objects and hypotheses

  • α is any measurable space; no topology, standard-Borel, countability, or nonempty-space hypothesis is imposed.
  • μ and π are probability measures: μ(α)=π(α)=1. Their finiteness instances are automatic.
  • hμΠ proves μ≪π. No separate SigmaFinite, decomposition, finite-KL or Integrable r μ premise appears.
  • Write a(x)=μ.rnDeriv π x∈[0,∞], ρ(x)=a(x).toReal, and r=RNLogRatio.logRatio μ π=MeasureTheory.llr μ π=Real.log ρ. All names refer to the same selected functions for the original pair (μ,π).

Mathematical proof

1. Verify equal finite masses

Probability normalization supplies the equal-mass hypothesis of the imported finite-measure theorem.

\[\mu(\alpha)=1=\pi(\alpha).\]
Corresponding Lean step

IsProbabilityMeasure instances; by simp

2. Apply the equal-mass KL formula

Mathlib's theorem gives exactly this toReal equality without an integrability premise. Its proof separates the integrable and nonintegrable cases.

\[\operatorname{toReal}(\mathrm{KL}(\mu\Vert\pi))=\int\operatorname{llr}(\mu,\pi)\,d\mu.\]
Corresponding Lean step

InformationTheory.toReal_klDiv_of_measure_eq

3. Understand the nonintegrable branch and rename the function

In the integrable branch the mass correction cancels. Otherwise KL is infinity, its real conversion is zero, and the nonintegrable Bochner integral is zero. Finally llr is the ASTIS logRatio.

\[r\notin L^1(\mu)\Longrightarrow\mathrm{KL}=\infty,\quad\operatorname{toReal}(\infty)=0=\int r\,d\mu.\]
Corresponding Lean step

Imported helper: klDiv_of_not_integrable; integral_undef; ENNReal.toReal_top. ASTIS: simp [RNLogRatio.logRatio]

Lean statement · toReal_klDiv_eq_integral_logRatio_of_probability

The left side explicitly converts an extended nonnegative KL value to a real number. This conversion loses the distinction between infinity and zero, so the conclusion is not a proof that KL is finite.

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.

theorem toReal_klDiv_eq_integral_logRatio_of_probability
    (mu pi : Measure α) [IsProbabilityMeasure mu] [IsProbabilityMeasure pi]
    (hmuPi : mu ≪ pi) :
    (_root_.InformationTheory.klDiv mu pi).toReal =
      ∫ x, logRatio mu pi x ∂mu

Exact module and namespace context

Lean proof · toReal_klDiv_eq_integral_logRatio_of_probability

The proof establishes equal total masses from normalization, invokes the existing equal-mass KL theorem, and unfolds the selected log-ratio name. The imported theorem's nonintegrable branch explains why no finite-entropy hypothesis was needed.

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.

theorem toReal_klDiv_eq_integral_logRatio_of_probability
    (mu pi : Measure α) [IsProbabilityMeasure mu] [IsProbabilityMeasure pi]
    (hmuPi : mu ≪ pi) :
    (_root_.InformationTheory.klDiv mu pi).toReal =
      ∫ x, logRatio mu pi x ∂mu := by
  simpa [logRatio] using
    (_root_.InformationTheory.toReal_klDiv_of_measure_eq
      (μ := mu) (ν := pi) hmuPi (by simp))

end

end RNLogRatio
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

  • The ASTIS comment's phrase 'finite KL' is interpretive motivation, not an extra premise in the actual declaration. The formula must retain toReal.
  • The real Bochner integral is totalized: a nonintegrable integrand has integral 0. No finite-energy or extended-valued Fisher interpretation is supplied unless the relevant analytic domain is established separately.
  • No finiteness, differentiability of KL along a path, or entropy-dissipation identity is produced.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • InformationTheory.toReal_klDiv_of_measure_eq

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.