The selected real density is nonnegative everywhere
AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density_nonneg · theorem · Teaching coverage
Statement
For arbitrary measures μ and π on a measurable space α and every x∈α, the real conversion ρ(x) of the selected RN derivative is nonnegative.
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 absolute-continuity or finiteness premise.
Mathematical proof
1. Use the nonnegativity of real conversion
Every extended-nonnegative value has nonnegative toReal, including infinity whose conversion is zero.
Corresponding Lean step
ENNReal.toReal_nonneg
Lean statement · density_nonneg
The conclusion is a non-strict pointwise bound. It does not rule out zero values or distinguish a zero RN value from an infinite one after 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 density_nonneg (mu pi : Measure α) (x : α) :
0 ≤ density mu pi xLean proof · density_nonneg
The density definition is a toReal expression, so the general nonnegativity theorem applies directly.
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 density_nonneg (mu pi : Measure α) (x : α) :
0 ≤ density mu pi x := by
exact ENNReal.toReal_nonneg
/-- Absolute continuity makes the canonical real RN density positive `mu`-a.e.
The `rnDeriv < ∞` obligation is explicit because `toReal ∞ = 0`. -/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.
- No strict positivity, normalization, or reconstruction follows from this bound.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- ENNReal.toReal_nonneg
Mathematical sources
- Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
- Existing declaration-visibility check — Read-only #check evidence; no build/test run.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.