Samplinglib mathematical lesson

Evaluate the log-ratio as the logarithm of the selected density

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

Read this first

Mathematical statement

For arbitrary measures μ and π on a measurable space α, and every x∈α, the selected log-ratio equals Real.log of the selected real density at x. The equality holds everywhere in the library's totalized conventions.

\[\forall x\in\alpha,\qquad r(x)=\operatorname{Real.log}(\rho(x)).\]

Lean statement · logRatio_apply

This is pointwise equality for an arbitrary input, not just a.e. equality. Its validity at zeros comes from the definition of the totalized logarithm.

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)

theorem logRatio_apply (mu pi : Measure α) (x : α) :
    logRatio mu pi x = Real.log (density mu pi x)

Exact module and namespace context

Proof roadmap

1Unfold both names
Both sides expand to the same logarithm of the same converted RN value, so reflexivity proves equality.

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.
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 (μ,π).
x is arbitrary; no positivity premise is present.

Mathematical proof

1. Unfold both names

Both sides expand to the same logarithm of the same converted RN value, so reflexivity proves equality.

\[r(x)\equiv\log\big(a(x).\mathrm{toReal}\big)\equiv\log\rho(x).\]

Corresponding Lean step

RNLogRatio.logRatio; RNLogRatio.density; rfl

Lean verification

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

Lean proof · logRatio_apply

Unfolding the two selected-function names leaves identical expressions. The proof does not use or establish positivity.

Download module (.lean)

theorem logRatio_apply (mu pi : Measure α) (x : α) :
    logRatio mu pi x = Real.log (density mu pi x) := by
  rfl

@[fun_prop]

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.
This equality alone cannot be exponentiated to recover ρ everywhere: exp(log 0)=1, not 0.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.llr

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Underlying llr definition — Explains why the equality is definitional.
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.