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

Measurability of the selected log-ratio

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

Statement

For arbitrary measures μ and π on a measurable space α, the selected real log-ratio r is measurable. No positivity or entropy-integrability assumption is needed.

\[r=\operatorname{llr}(\mu,\pi):\alpha\to\mathbb R\quad\text{is measurable}.\]

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 (μ,π).

Mathematical proof

1. Reuse the library's log-ratio measurability

Mathlib composes measurable RN selection, measurable real conversion, and the measurable totalized real logarithm.

\[a\text{ measurable}\Longrightarrow\log(a.\mathrm{toReal})\text{ measurable}.\]
Corresponding Lean step

MeasureTheory.measurable_llr

2. Replace the alias

The ASTIS name denotes exactly that same function, so the imported assertion is the target.

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

simp [RNLogRatio.logRatio]

Lean statement · measurable_logRatio

The measurable object is a real function despite the totalized zero-density convention. No regularity of its derivative is included.

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

Exact module and namespace context

Lean proof · measurable_logRatio

The proof applies the existing likelihood-ratio measurability theorem and unfolds only the ASTIS alias.

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 measurable_logRatio (mu pi : Measure α) :
    Measurable (logRatio mu pi) := by
  simpa [logRatio] using MeasureTheory.measurable_llr mu pi

/-- The real RN density is pointwise nonnegative. -/

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.
  • No continuity, differentiability, gradient measurability or integrability is deduced.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • MeasureTheory.measurable_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.