ASTIS mathematical exposition

A measure's selected self-log-ratio is zero almost everywhere

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

Statement

For every σ-finite measure μ on a measurable space α, the selected log-ratio of μ relative to itself equals the constant zero μ-almost everywhere.

\[r_{\mu,\mu}(x)=0\quad\mu\text{-a.e.}.\]

All objects and hypotheses

α is any measurable space; no topology, standard-Borel, countability, or nonempty-space hypothesis is imposed.
μ is σ-finite; no probability, nonzero-mass or finite-entropy premise.
Both arguments of logRatio are μ.

Mathematical proof

1. Reuse the self likelihood identity

Mathlib obtains this from the self RN derivative being one a.e. and log 1=0.

\[\operatorname{llr}(\mu,\mu)=0\quad\mu\text{-a.e.}.\]

Corresponding Lean step

MeasureTheory.llr_self

2. Unfold the ASTIS alias

The selected ASTIS log-ratio is exactly this likelihood ratio, with the same exceptional set.

\[r_{\mu,\mu}=0\quad\mu\text{-a.e.}.\]

Corresponding Lean step

filter_upwards; simp [RNLogRatio.logRatio]

Lean statement · logRatio_self_ae

The assertion concerns values of a selected function a.e. It does not say the function is everywhere constant or differentiable.

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 logRatio_self_ae (mu : Measure α) [SigmaFinite mu] :
    logRatio mu mu =ᵐ[mu] fun _ => 0

Exact module and namespace context

Lean proof · logRatio_self_ae

The proof uses the existing self-likelihood theorem and unfolds the alias. There is no argument about gradients.

theorem logRatio_self_ae (mu : Measure α) [SigmaFinite mu] :
    logRatio mu mu =ᵐ[mu] fun _ => 0 := by
  filter_upwards [MeasureTheory.llr_self mu] with x hx
  simpa [logRatio] using hx

/-- For probability measures, finite KL has the source-facing integral form

`KL(mu || pi) = integral log(d mu / d pi) dmu`

at the real-valued level.  Mathlib's `klDiv` remains the canonical ENNReal
measure divergence; this theorem is the bridge used by calculus arguments. -/

Exact module and namespace context

Scope and omitted-condition boundaries

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.
In particular, do not infer that the selected log-ratio's totalized classical gradient vanishes μ-a.e. from this function-value identity alone.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.logRatio

Mathlib API called (external library)

MeasureTheory.llr_self

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Mathlib self log-likelihood theorem — A.e. consequence of self RN identity; exact reused API.
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.