ASTIS mathematical exposition

The selected real RN density

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density · def · Teaching coverage

Statement

For any measures μ and π on a measurable space α and any x∈α, define the selected real density ρ(x) by converting Mathlib's extended-nonnegative RN derivative to ℝ. This is a globally defined representative-valued expression, not an unconditional assertion that μ has a classical density relative to π.

\[a(x):=\mu.\mathrm{rnDeriv}\,\pi\,x,\qquad\rho(x):=a(x).\mathrm{toReal}.\]

All objects and hypotheses

α is any measurable space; no topology, standard-Borel, countability, or nonempty-space hypothesis is imposed.
μ and π are arbitrary measures on α unless further conditions are stated; no probability or finite-mass assumption is implicit.
x is any point of α; no absolute-continuity, decomposition or σ-finiteness premise.

Construction and meaning

1. Select the existing extended-valued function

Use Mathlib's chosen measurable RN derivative. When a Lebesgue decomposition does not exist, this library function is defined to be zero.

\[a:=\mu.\mathrm{rnDeriv}\,\pi:\alpha\to[0,\infty].\]

Corresponding Lean step

MeasureTheory.Measure.rnDeriv

2. Convert each value to a real number

Finite nonnegative values retain their real value; the extended value infinity is sent to zero. The result is the real function needed by later calculus expressions.

\[\rho(x)=\operatorname{toReal}(a(x)),\qquad\operatorname{toReal}(\infty)=0.\]

Corresponding Lean step

ENNReal.toReal

Lean statement · density

The inputs are two measures and a point, and the output is a real number. No hypothesis certifies a density reconstruction at this stage.

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 density (mu pi : Measure α) (x : α) : ℝ

Exact module and namespace context

Lean construction · density

This is a construction: take the existing RN derivative value and apply its real conversion. No existence, normalization, or finiteness theorem is proved.

noncomputable def density (mu pi : Measure α) (x : α) : ℝ :=
  (mu.rnDeriv pi x).toReal

/-- The canonical log-density ratio.  This is definitionally Mathlib's
log-likelihood ratio, so KL and Fisher layers share one representative. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Mathlib's RN derivative is a selected measurable extended-nonnegative function, and defaults to zero if no Lebesgue decomposition exists. ENNReal.toReal sends ∞ to 0; Real.log 0=0. Unconditional naming or measurability is not a reconstruction or positivity theorem.
No differentiability, strict positivity, normalization, or integral reconstruction is supplied.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.Measure.rnDeriv
ENNReal.toReal

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Mathlib RN selection and fallback — Definition rnDeriv selects from HaveLebesgueDecomposition when available and otherwise is zero.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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