Measurability of the selected real density
AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.measurable_density · theorem · Teaching coverage
Mathematical statement
For arbitrary measures μ and π on any measurable space α, the selected real RN function ρ is measurable as a map to ℝ with its Borel measurable structure.
Lean statement · measurable_density
The conclusion is ordinary measurability of the exact selected function, not an a.e.-measurability claim or a statement about every representative.
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_density (mu pi : Measure α) :
Measurable (density mu pi)Proof roadmap
- 1Use measurability of the selected RN function
Mathlib guarantees measurability even in the fallback case, where the selected function is zero.
- 2Compose with real conversion
The measurable real conversion of an extended-nonnegative measurable function remains measurable.
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 (μ,π).
- No absolute-continuity or σ-finiteness assumption is required.
Mathematical proof
1. Use measurability of the selected RN function
Mathlib guarantees measurability even in the fallback case, where the selected function is zero.
Corresponding Lean step
MeasureTheory.Measure.measurable_rnDeriv
2. Compose with real conversion
The measurable real conversion of an extended-nonnegative measurable function remains measurable.
Corresponding Lean step
Measurable.ennreal_toReal
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · measurable_density
The proof starts with Mathlib's RN measurability theorem and applies the rule preserving measurability under real conversion.
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_density (mu pi : Measure α) :
Measurable (density mu pi) := by
exact (Measure.measurable_rnDeriv mu pi).ennreal_toReal
@[fun_prop]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.
- Measurability does not imply integrability, finite entropy, positivity or differentiability.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- MeasureTheory.Measure.measurable_rnDeriv
- Measurable.ennreal_toReal
Mathematical sources
- Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
- RN measurability with and without decomposition — Actual theorem handles both the selected-decomposition and zero-fallback cases.
- 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.