Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

The selected log-density ratio

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

Read this first

Mathematical statement

For arbitrary measures μ and π on a measurable space α, define r to be Mathlib's selected log-likelihood ratio. At a point x, it is the totalized real logarithm of the selected real RN function ρ(x).

\[r:=\operatorname{llr}(\mu,\pi),\qquad r(x)=\operatorname{Real.log}\big((\mu.\mathrm{rnDeriv}\,\pi\,x).\mathrm{toReal}\big).\]
Lean statement · logRatio

The output is a real-valued function on α. Its name does not assert regularity or finiteness of relative entropy.

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

Exact module and namespace context

Proof roadmap

  1. 1Reuse the likelihood-ratio object

    Choose the existing llr function unchanged so the later measure and calculus layers share the same selected representative.

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.
  • No absolute-continuity, σ-finiteness, differentiability or integrability premise.

Construction and meaning

1. Reuse the likelihood-ratio object

Choose the existing llr function unchanged so the later measure and calculus layers share the same selected representative.

\[r=\operatorname{llr}(\mu,\pi).\]
Corresponding Lean step

MeasureTheory.llr

Lean verification

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

Lean construction · logRatio

This is an alias-style construction, not a new logarithm theorem. The body reuses Mathlib's entire selected log-likelihood-ratio function.

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 logRatio (mu pi : Measure α) : α → ℝ :=
  MeasureTheory.llr mu pi

@[simp]

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.
  • An equality a.e. of function values does not by itself identify classical gradients. No pointwise choice on exceptional null sets or independence under arbitrary null-set changes is proved.
  • The function is real-valued even when the mathematical extended logarithm would be −∞ at a zero density. No Sobolev or classical score is constructed.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • MeasureTheory.llr

    Mathematical sources

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