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

Absolute continuity gives a positive real density μ-almost everywhere

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

Statement

Let μ and π be measures on a measurable space α. Assume μ is σ-finite, a Lebesgue decomposition of μ relative to π exists, and μ≪π. Then the selected real density ρ is strictly positive at μ-almost every point. The assertion is neither everywhere nor necessarily π-almost everywhere.

\[\mu\ll\pi,\quad\mu\ \sigma\text{-finite},\quad\operatorname{HaveLebesgueDecomposition}(\mu,\pi)\quad\Longrightarrow\quad0<\rho(x)\ \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. Obtain positive extended RN values under μ

The decomposition and absolute continuity imply that a is positive outside a μ-null set.

\[0<a(x)\quad\mu\text{-a.e.}.\]
Corresponding Lean step

MeasureTheory.Measure.rnDeriv_pos hmuPi

2. Transport a.e. finiteness from π to μ

σ-finiteness of μ gives a<∞ π-a.e. Absolute continuity transfers that assertion to μ-a.e.; it is not necessary to assume π σ-finite.

\[a(x)<\infty\quad\pi\text{-a.e.}\Longrightarrow a(x)<\infty\quad\mu\text{-a.e.}.\]
Corresponding Lean step

MeasureTheory.Measure.rnDeriv_lt_top; MeasureTheory.Measure.AbsolutelyContinuous.ae_le

3. Convert positive finite values

Intersect the two μ-a.e. sets. A nonzero extended value distinct from infinity has strictly positive real conversion.

\[0<a(x)<\infty\Longrightarrow0<a(x).\mathrm{toReal}=\rho(x).\]
Corresponding Lean step

filter_upwards; ENNReal.toReal_pos

Lean statement · density_ae_pos_of_absolutelyContinuous

The a.e. filter is μ. The decomposition instance and μ's σ-finiteness have separate roles: RN positivity and exclusion of infinity before real conversion.

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_ae_pos_of_absolutelyContinuous
    (mu pi : Measure α) [SigmaFinite mu]
    [Measure.HaveLebesgueDecomposition mu pi]
    (hmuPi : mu ≪ pi) :
    ∀ᵐ x ∂mu, 0 < density mu pi x

Exact module and namespace context

Lean proof · density_ae_pos_of_absolutelyContinuous

The proof combines μ-a.e. positivity with π-a.e. finiteness transported through absolute continuity. The final conversion theorem needs both nonzero and non-infinite RN values.

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_ae_pos_of_absolutelyContinuous
    (mu pi : Measure α) [SigmaFinite mu]
    [Measure.HaveLebesgueDecomposition mu pi]
    (hmuPi : mu ≪ pi) :
    ∀ᵐ x ∂mu, 0 < density mu pi x := by
  filter_upwards [Measure.rnDeriv_pos hmuPi,
    hmuPi.ae_le (Measure.rnDeriv_lt_top mu pi)] with x hxPos hxTop
  exact ENNReal.toReal_pos hxPos.ne' hxTop.ne

/-- Exponentiating the canonical log-density ratio recovers the canonical RN
density `mu`-a.e. under absolute continuity. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • Neither pointwise positivity nor π-a.e. positivity is asserted. In particular π may assign positive mass to a region where μ has zero density.
  • 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.
  • Positivity μ-a.e. does not provide differentiability, finite entropy, or a score domain.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • MeasureTheory.Measure.rnDeriv_pos
  • MeasureTheory.Measure.rnDeriv_lt_top
  • MeasureTheory.Measure.AbsolutelyContinuous.ae_le
  • ENNReal.toReal_pos

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.