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

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

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

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

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

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

Exact module and namespace context

Lean proof · logRatio_apply

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

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

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • MeasureTheory.llr

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.