Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

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

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

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

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

theorem density_self_ae (mu : Measure α) [SigmaFinite mu] :
    density mu mu =ᵐ[mu] fun _ => 1

Exact module and namespace context

Lean proof · density_self_ae

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

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_self_ae (mu : Measure α) [SigmaFinite mu] :
    density mu mu =ᵐ[mu] fun _ => 1 := by
  filter_upwards [mu.rnDeriv_self] with x hx
  simp [density, hx]

/-- The canonical log-density ratio of a measure relative to itself is zero
a.e. -/

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • MeasureTheory.Measure.rnDeriv_self
  • ENNReal.toReal_one

Mathematical sources

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