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

Exponentiating the log-ratio recovers density μ-almost everywhere

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

Statement

Let μ and π be measures on a measurable space α, with μ σ-finite, a Lebesgue decomposition of μ relative to π, and μ≪π. Exponentiating the selected real log-ratio gives the selected real density μ-almost everywhere.

\[\exp(r(x))=\rho(x)\quad\text{for }\mu\text{-a.e. }x.\]

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 (μ,π).
  • μ is σ-finite; HaveLebesgueDecomposition μ π is supplied; and hμΠ proves μ≪π. No σ-finiteness of π or probability normalization is required.

Mathematical proof

1. Use the established a.e. likelihood identity

Mathlib's exp_llr_of_ac already handles the positivity/finiteness and change-of-a.e.-measure issues under these precise premises.

\[\exp(\operatorname{llr}(\mu,\pi)(x))=(\mu.\mathrm{rnDeriv}\,\pi\,x).\mathrm{toReal}\quad\mu\text{-a.e.}.\]
Corresponding Lean step

MeasureTheory.exp_llr_of_ac

2. Translate the two selected-function names

On the imported full-μ-measure set, unfold logRatio and density to identify the two sides with the target functions.

\[\exp r=\rho\quad\mu\text{-a.e.}.\]
Corresponding Lean step

filter_upwards; simp [RNLogRatio.logRatio, RNLogRatio.density]

Lean statement · exp_logRatio_ae_eq_density_of_absolutelyContinuous

This compares two functions modulo μ-null sets. It does not identify their values at every point or under the stronger π-a.e. filter.

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 exp_logRatio_ae_eq_density_of_absolutelyContinuous
    (mu pi : Measure α) [SigmaFinite mu]
    [Measure.HaveLebesgueDecomposition mu pi]
    (hmuPi : mu ≪ pi) :
    (fun x => Real.exp (logRatio mu pi x)) =ᵐ[mu] density mu pi

Exact module and namespace context

Lean proof · exp_logRatio_ae_eq_density_of_absolutelyContinuous

The proof directly reuses Mathlib's exponential-likelihood theorem and changes only notation. It does not derive a chain rule by differentiating this a.e. equality.

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 exp_logRatio_ae_eq_density_of_absolutelyContinuous
    (mu pi : Measure α) [SigmaFinite mu]
    [Measure.HaveLebesgueDecomposition mu pi]
    (hmuPi : mu ≪ pi) :
    (fun x => Real.exp (logRatio mu pi x)) =ᵐ[mu] density mu pi := by
  filter_upwards [MeasureTheory.exp_llr_of_ac mu pi hmuPi] with x hx
  simpa [logRatio, density] using hx

/-- The canonical density of a measure relative to itself is one a.e. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • At ρ=0, exp(Real.log ρ)=1, so replacing the a.e. statement by an everywhere identity is unjustified.
  • 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 density-gradient identity or differentiation of a.e.-equal functions is established.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • MeasureTheory.exp_llr_of_ac

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.