Measurability of the selected log-ratio
AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.measurable_logRatio · theorem · Teaching coverage
Mathematical 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.
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)Proof roadmap
- 1Reuse the library's log-ratio measurability
Mathlib composes measurable RN selection, measurable real conversion, and the measurable totalized real logarithm.
- 2Replace the alias
The ASTIS name denotes exactly that same function, so the imported assertion is the target.
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 (μ,π).
Mathematical proof
1. Reuse the library's log-ratio measurability
Mathlib composes measurable RN selection, measurable real conversion, and the measurable totalized real logarithm.
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.
Corresponding Lean step
simp [RNLogRatio.logRatio]
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
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 piScope 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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- MeasureTheory.measurable_llr
Mathematical sources
- Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
- Mathlib likelihood-ratio measurability — Proof composes measurable RN, toReal, and Real.log; direct reused API.
- 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.