Samplinglib mathematical lesson

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

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

Read this first

Mathematical 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.}.\]

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.

Download module (.lean)

theorem logRatio_self_ae (mu : Measure α) [SigmaFinite mu] :
    logRatio mu mu =ᵐ[mu] fun _ => 0

Exact module and namespace context

Proof roadmap

1Reuse the self likelihood identity
Mathlib obtains this from the self RN derivative being one a.e. and log 1=0.
2Unfold the ASTIS alias
The selected ASTIS log-ratio is exactly this likelihood ratio, with the same exceptional set.

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · logRatio_self_ae

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

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib 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.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.