Samplinglib mathematical lesson

A measure's selected self-density is one almost everywhere

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

Read this first

Mathematical statement

For a σ-finite measure μ on any measurable space α, its selected real RN density relative to itself equals the constant one μ-almost everywhere.

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

Lean statement · density_self_ae

The same σ-finite measure appears twice, and equality is only a.e. under that measure. No representative values on null points are fixed.

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 density_self_ae (mu : Measure α) [SigmaFinite mu] :
    density mu mu =ᵐ[mu] fun _ => 1

Exact module and namespace context

Proof roadmap

1Use the self RN identity
The selected extended RN derivative is one outside a μ-null set.
2Convert the finite unit value
Real conversion sends one to one, yielding the stated real-density identity on the same a.e. 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 a σ-finite measure; no finite-total-mass or probability requirement.
Both measure arguments are the same μ.

Mathematical proof

1. Use the self RN identity

The selected extended RN derivative is one outside a μ-null set.

\[\mu.\mathrm{rnDeriv}\,\mu\,x=1\quad\mu\text{-a.e.}.\]

Corresponding Lean step

MeasureTheory.Measure.rnDeriv_self

2. Convert the finite unit value

Real conversion sends one to one, yielding the stated real-density identity on the same a.e. set.

\[\rho_{\mu,\mu}(x)=\operatorname{toReal}(1)=1.\]

Corresponding Lean step

filter_upwards; simp [RNLogRatio.density]

Lean verification

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

Lean proof · density_self_ae

The proof takes the library self-RN identity and converts its value one into a real one.

Download module (.lean)

theorem density_self_ae (mu : Measure α) [SigmaFinite mu] :
    density mu mu =ᵐ[mu] fun _ => 1 := by
  filter_upwards [mu.rnDeriv_self] with x hx
  simp [density, 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.
No pointwise self-density formula, classical gradient identity, or Fisher-zero theorem is proved here.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density

Mathlib API called (external library)

MeasureTheory.Measure.rnDeriv_self
ENNReal.toReal_one

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Mathlib self RN identity — SigmaFinite μ and μ-a.e. equality.
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.