Samplinglib mathematical lesson

The selected real RN density

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

Read this first

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

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.

Download module (.lean)

noncomputable def density (mu pi : Measure α) (x : α) : ℝ

Exact module and namespace context

Proof roadmap

1Select 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.
2Convert 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.

Full assumptions and notation

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 verification

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

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.

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

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

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