RNLogRatio: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

The selected real RN density
The selected log-density ratio
Evaluate the log-ratio as the logarithm of the selected density
Measurability of the selected real density
Measurability of the selected log-ratio
The selected real density is nonnegative everywhere
Absolute continuity gives a positive real density μ-almost everywhere
Exponentiating the log-ratio recovers density μ-almost everywhere
A measure's selected self-density is one almost everywhere
A measure's selected self-log-ratio is zero almost everywhere
The real conversion of KL equals the totalized log-ratio integral

ASTIS mathematical exposition

The selected real RN density

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density · def · Teaching coverage

Statement

For any measures μ and π on a measurable space α and any x∈α, define the selected real density ρ(x) by converting Mathlib's extended-nonnegative RN derivative to ℝ. This is a globally defined representative-valued expression, not an unconditional assertion that μ has a classical density relative to π.

\[a(x):=\mu.\mathrm{rnDeriv}\,\pi\,x,\qquad\rho(x):=a(x).\mathrm{toReal}.\]

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.
x is any point of α; no absolute-continuity, decomposition or σ-finiteness premise.

Construction and meaning

1. Select the existing extended-valued function

Use Mathlib's chosen measurable RN derivative. When a Lebesgue decomposition does not exist, this library function is defined to be zero.

\[a:=\mu.\mathrm{rnDeriv}\,\pi:\alpha\to[0,\infty].\]

Corresponding Lean step

MeasureTheory.Measure.rnDeriv

2. Convert each value to a real number

Finite nonnegative values retain their real value; the extended value infinity is sent to zero. The result is the real function needed by later calculus expressions.

\[\rho(x)=\operatorname{toReal}(a(x)),\qquad\operatorname{toReal}(\infty)=0.\]

Corresponding Lean step

ENNReal.toReal

Lean statement · density

The inputs are two measures and a point, and the output is a real number. No hypothesis certifies a density reconstruction at this stage.

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.

noncomputable def density (mu pi : Measure α) (x : α) : ℝ

Exact module and namespace context

Lean construction · density

This is a construction: take the existing RN derivative value and apply its real conversion. No existence, normalization, or finiteness theorem is proved.

noncomputable def density (mu pi : Measure α) (x : α) : ℝ :=
  (mu.rnDeriv pi x).toReal

/-- The canonical log-density ratio.  This is definitionally Mathlib's
log-likelihood ratio, so KL and Fisher layers share one representative. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Mathlib's RN derivative is a selected measurable extended-nonnegative function, and defaults to zero if no Lebesgue decomposition exists. ENNReal.toReal sends ∞ to 0; Real.log 0=0. Unconditional naming or measurability is not a reconstruction or positivity theorem.
No differentiability, strict positivity, normalization, or integral reconstruction is supplied.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.Measure.rnDeriv
ENNReal.toReal

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Mathlib RN selection and fallback — Definition rnDeriv selects from HaveLebesgueDecomposition when available and otherwise is zero.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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

ASTIS mathematical exposition

The selected log-density ratio

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.logRatio · def · Teaching coverage

Statement

For arbitrary measures μ and π on a measurable space α, define r to be Mathlib's selected log-likelihood ratio. At a point x, it is the totalized real logarithm of the selected real RN function ρ(x).

\[r:=\operatorname{llr}(\mu,\pi),\qquad r(x)=\operatorname{Real.log}\big((\mu.\mathrm{rnDeriv}\,\pi\,x).\mathrm{toReal}\big).\]

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.
No absolute-continuity, σ-finiteness, differentiability or integrability premise.

Construction and meaning

1. Reuse the likelihood-ratio object

Choose the existing llr function unchanged so the later measure and calculus layers share the same selected representative.

\[r=\operatorname{llr}(\mu,\pi).\]

Corresponding Lean step

MeasureTheory.llr

Lean statement · logRatio

The output is a real-valued function on α. Its name does not assert regularity or finiteness of relative entropy.

noncomputable def logRatio (mu pi : Measure α) : α → ℝ

Exact module and namespace context

Lean construction · logRatio

This is an alias-style construction, not a new logarithm theorem. The body reuses Mathlib's entire selected log-likelihood-ratio function.

noncomputable def logRatio (mu pi : Measure α) : α → ℝ :=
  MeasureTheory.llr mu pi

@[simp]

Exact module and namespace context

Scope and omitted-condition boundaries

Mathlib's RN derivative is a selected measurable extended-nonnegative function, and defaults to zero if no Lebesgue decomposition exists. ENNReal.toReal sends ∞ to 0; Real.log 0=0. Unconditional naming or measurability is not a reconstruction or positivity theorem.
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.
The function is real-valued even when the mathematical extended logarithm would be −∞ at a zero density. No Sobolev or classical score is constructed.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.llr

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Mathlib log-likelihood ratio definition — Exact pointwise definition via Real.log and rnDeriv.toReal.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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

ASTIS mathematical exposition

Evaluate the log-ratio as the logarithm of the selected density

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

Statement

For arbitrary measures μ and π on a measurable space α, and every x∈α, the selected log-ratio equals Real.log of the selected real density at x. The equality holds everywhere in the library's totalized conventions.

\[\forall x\in\alpha,\qquad r(x)=\operatorname{Real.log}(\rho(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 (μ,π).
x is arbitrary; no positivity premise is present.

Mathematical proof

1. Unfold both names

Both sides expand to the same logarithm of the same converted RN value, so reflexivity proves equality.

\[r(x)\equiv\log\big(a(x).\mathrm{toReal}\big)\equiv\log\rho(x).\]

Corresponding Lean step

RNLogRatio.logRatio; RNLogRatio.density; rfl

Lean statement · logRatio_apply

This is pointwise equality for an arbitrary input, not just a.e. equality. Its validity at zeros comes from the definition of the totalized logarithm.

theorem logRatio_apply (mu pi : Measure α) (x : α) :
    logRatio mu pi x = Real.log (density mu pi x)

Exact module and namespace context

Lean proof · logRatio_apply

Unfolding the two selected-function names leaves identical expressions. The proof does not use or establish positivity.

theorem logRatio_apply (mu pi : Measure α) (x : α) :
    logRatio mu pi x = Real.log (density mu pi x) := by
  rfl

@[fun_prop]

Exact module and namespace context

Scope and omitted-condition boundaries

Mathlib's RN derivative is a selected measurable extended-nonnegative function, and defaults to zero if no Lebesgue decomposition exists. ENNReal.toReal sends ∞ to 0; Real.log 0=0. Unconditional naming or measurability is not a reconstruction or positivity theorem.
This equality alone cannot be exponentiated to recover ρ everywhere: exp(log 0)=1, not 0.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.llr

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Underlying llr definition — Explains why the equality is definitional.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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

ASTIS mathematical exposition

Measurability of the selected real density

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

Statement

For arbitrary measures μ and π on any measurable space α, the selected real RN function ρ is measurable as a map to ℝ with its Borel measurable structure.

\[\rho:\alpha\to\mathbb R\quad\text{is measurable}.\]

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 (μ,π).
No absolute-continuity or σ-finiteness assumption is required.

Mathematical proof

1. Use measurability of the selected RN function

Mathlib guarantees measurability even in the fallback case, where the selected function is zero.

\[a:\alpha\to[0,\infty]\quad\text{is measurable}.\]

Corresponding Lean step

MeasureTheory.Measure.measurable_rnDeriv

2. Compose with real conversion

The measurable real conversion of an extended-nonnegative measurable function remains measurable.

\[\rho=\operatorname{toReal}\circ a\quad\text{is measurable}.\]

Corresponding Lean step

Measurable.ennreal_toReal

Lean statement · measurable_density

The conclusion is ordinary measurability of the exact selected function, not an a.e.-measurability claim or a statement about every representative.

theorem measurable_density (mu pi : Measure α) :
    Measurable (density mu pi)

Exact module and namespace context

Lean proof · measurable_density

The proof starts with Mathlib's RN measurability theorem and applies the rule preserving measurability under real conversion.

theorem measurable_density (mu pi : Measure α) :
    Measurable (density mu pi) := by
  exact (Measure.measurable_rnDeriv mu pi).ennreal_toReal

@[fun_prop]

Exact module and namespace context

Scope and omitted-condition boundaries

Mathlib's RN derivative is a selected measurable extended-nonnegative function, and defaults to zero if no Lebesgue decomposition exists. ENNReal.toReal sends ∞ to 0; Real.log 0=0. Unconditional naming or measurability is not a reconstruction or positivity theorem.
Measurability does not imply integrability, finite entropy, positivity or differentiability.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density

Mathlib API called (external library)

MeasureTheory.Measure.measurable_rnDeriv
Measurable.ennreal_toReal

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
RN measurability with and without decomposition — Actual theorem handles both the selected-decomposition and zero-fallback cases.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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

ASTIS mathematical exposition

Measurability of the selected log-ratio

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

Statement

For arbitrary measures μ and π on a measurable space α, the selected real log-ratio r is measurable. No positivity or entropy-integrability assumption is needed.

\[r=\operatorname{llr}(\mu,\pi):\alpha\to\mathbb R\quad\text{is measurable}.\]

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 (μ,π).

Mathematical proof

1. Reuse the library's log-ratio measurability

Mathlib composes measurable RN selection, measurable real conversion, and the measurable totalized real logarithm.

\[a\text{ measurable}\Longrightarrow\log(a.\mathrm{toReal})\text{ measurable}.\]

Corresponding Lean step

MeasureTheory.measurable_llr

2. Replace the alias

The ASTIS name denotes exactly that same function, so the imported assertion is the target.

\[r=\operatorname{llr}(\mu,\pi).\]

Corresponding Lean step

simp [RNLogRatio.logRatio]

Lean statement · measurable_logRatio

The measurable object is a real function despite the totalized zero-density convention. No regularity of its derivative is included.

theorem measurable_logRatio (mu pi : Measure α) :
    Measurable (logRatio mu pi)

Exact module and namespace context

Lean proof · measurable_logRatio

The proof applies the existing likelihood-ratio measurability theorem and unfolds only the ASTIS alias.

theorem measurable_logRatio (mu pi : Measure α) :
    Measurable (logRatio mu pi) := by
  simpa [logRatio] using MeasureTheory.measurable_llr mu pi

/-- The real RN density is pointwise nonnegative. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Mathlib's RN derivative is a selected measurable extended-nonnegative function, and defaults to zero if no Lebesgue decomposition exists. ENNReal.toReal sends ∞ to 0; Real.log 0=0. Unconditional naming or measurability is not a reconstruction or positivity theorem.
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 continuity, differentiability, gradient measurability or integrability is deduced.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.logRatio

Mathlib API called (external library)

MeasureTheory.measurable_llr

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Mathlib likelihood-ratio measurability — Proof composes measurable RN, toReal, and Real.log; direct reused API.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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

ASTIS mathematical exposition

The selected real density is nonnegative everywhere

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

Statement

For arbitrary measures μ and π on a measurable space α and every x∈α, the real conversion ρ(x) of the selected RN derivative is nonnegative.

\[\forall x\in\alpha,\qquad0\le\rho(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 (μ,π).
x is arbitrary; no absolute-continuity or finiteness premise.

Mathematical proof

1. Use the nonnegativity of real conversion

Every extended-nonnegative value has nonnegative toReal, including infinity whose conversion is zero.

\[a(x)\in[0,\infty]\Longrightarrow0\le a(x).\mathrm{toReal}=\rho(x).\]

Corresponding Lean step

ENNReal.toReal_nonneg

Lean statement · density_nonneg

The conclusion is a non-strict pointwise bound. It does not rule out zero values or distinguish a zero RN value from an infinite one after conversion.

theorem density_nonneg (mu pi : Measure α) (x : α) :
    0 ≤ density mu pi x

Exact module and namespace context

Lean proof · density_nonneg

The density definition is a toReal expression, so the general nonnegativity theorem applies directly.

theorem density_nonneg (mu pi : Measure α) (x : α) :
    0 ≤ density mu pi x := by
  exact ENNReal.toReal_nonneg

/-- Absolute continuity makes the canonical real RN density positive `mu`-a.e.
The `rnDeriv < ∞` obligation is explicit because `toReal ∞ = 0`. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Mathlib's RN derivative is a selected measurable extended-nonnegative function, and defaults to zero if no Lebesgue decomposition exists. ENNReal.toReal sends ∞ to 0; Real.log 0=0. Unconditional naming or measurability is not a reconstruction or positivity theorem.
No strict positivity, normalization, or reconstruction follows from this bound.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density

Mathlib API called (external library)

ENNReal.toReal_nonneg

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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

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.

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.

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

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density

Mathlib API called (external library)

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

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Extended RN positivity — Requires HaveLebesgueDecomposition and absolute continuity; conclusion is μ-a.e.
RN finiteness — Requires SigmaFinite μ; initial conclusion is π-a.e.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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

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.

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.

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

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Exact imported exponential-likelihood identity — Includes SigmaFinite μ, HaveLebesgueDecomposition μ π, μ≪π, and a μ-a.e. conclusion.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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

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.

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.

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

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.

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

ASTIS mathematical exposition

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

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

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

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

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

Exact module and namespace context

Lean proof · logRatio_self_ae

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

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

/-- For probability measures, finite KL has the source-facing integral form

`KL(mu || pi) = integral log(d mu / d pi) dmu`

at the real-valued level.  Mathlib's `klDiv` remains the canonical ENNReal
measure divergence; this theorem is the bridge used by calculus arguments. -/

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.

Source and reuse

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

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

ASTIS mathematical exposition

The real conversion of KL equals the totalized log-ratio integral

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

Statement

Let μ and π be probability measures on a measurable space α, and suppose μ≪π. Then the real conversion of Mathlib's extended-valued KL divergence equals the real Bochner integral of the selected log-ratio under μ. No log-ratio integrability or finite-KL assumption is present; the equality is also valid in the nonintegrable case, when both displayed real quantities are zero by totalization.

\[\operatorname{toReal}\!\left(\mathrm{KL}(\mu\Vert\pi)\right)=\int_\alpha r_{\mu,\pi}(x)\,d\mu(x).\]

All objects and hypotheses

α is any measurable space; no topology, standard-Borel, countability, or nonempty-space hypothesis is imposed.
μ and π are probability measures: μ(α)=π(α)=1. Their finiteness instances are automatic.
hμΠ proves μ≪π. No separate SigmaFinite, decomposition, finite-KL or Integrable r μ premise appears.
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 (μ,π).

Mathematical proof

1. Verify equal finite masses

Probability normalization supplies the equal-mass hypothesis of the imported finite-measure theorem.

\[\mu(\alpha)=1=\pi(\alpha).\]

Corresponding Lean step

IsProbabilityMeasure instances; by simp

2. Apply the equal-mass KL formula

Mathlib's theorem gives exactly this toReal equality without an integrability premise. Its proof separates the integrable and nonintegrable cases.

\[\operatorname{toReal}(\mathrm{KL}(\mu\Vert\pi))=\int\operatorname{llr}(\mu,\pi)\,d\mu.\]

Corresponding Lean step

InformationTheory.toReal_klDiv_of_measure_eq

3. Understand the nonintegrable branch and rename the function

In the integrable branch the mass correction cancels. Otherwise KL is infinity, its real conversion is zero, and the nonintegrable Bochner integral is zero. Finally llr is the ASTIS logRatio.

\[r\notin L^1(\mu)\Longrightarrow\mathrm{KL}=\infty,\quad\operatorname{toReal}(\infty)=0=\int r\,d\mu.\]

Corresponding Lean step

Imported helper: klDiv_of_not_integrable; integral_undef; ENNReal.toReal_top. ASTIS: simp [RNLogRatio.logRatio]

Lean statement · toReal_klDiv_eq_integral_logRatio_of_probability

The left side explicitly converts an extended nonnegative KL value to a real number. This conversion loses the distinction between infinity and zero, so the conclusion is not a proof that KL is finite.

theorem toReal_klDiv_eq_integral_logRatio_of_probability
    (mu pi : Measure α) [IsProbabilityMeasure mu] [IsProbabilityMeasure pi]
    (hmuPi : mu ≪ pi) :
    (_root_.InformationTheory.klDiv mu pi).toReal =
      ∫ x, logRatio mu pi x ∂mu

Exact module and namespace context

Lean proof · toReal_klDiv_eq_integral_logRatio_of_probability

The proof establishes equal total masses from normalization, invokes the existing equal-mass KL theorem, and unfolds the selected log-ratio name. The imported theorem's nonintegrable branch explains why no finite-entropy hypothesis was needed.

theorem toReal_klDiv_eq_integral_logRatio_of_probability
    (mu pi : Measure α) [IsProbabilityMeasure mu] [IsProbabilityMeasure pi]
    (hmuPi : mu ≪ pi) :
    (_root_.InformationTheory.klDiv mu pi).toReal =
      ∫ x, logRatio mu pi x ∂mu := by
  simpa [logRatio] using
    (_root_.InformationTheory.toReal_klDiv_of_measure_eq
      (μ := mu) (ν := pi) hmuPi (by simp))

end

end RNLogRatio
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

The ASTIS comment's phrase 'finite KL' is interpretive motivation, not an extra premise in the actual declaration. The formula must retain toReal.
The real Bochner integral is totalized: a nonintegrable integrand has integral 0. No finite-energy or extended-valued Fisher interpretation is supplied unless the relevant analytic domain is established separately.
No finiteness, differentiability of KL along a path, or entropy-dissipation identity is produced.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.logRatio

Mathlib API called (external library)

InformationTheory.toReal_klDiv_of_measure_eq

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Equal-mass real KL identity and its two branches — Finite measures, absolute continuity and equal mass; no Integrable premise. Nonintegrable branch explicitly uses integral_undef and toReal_top.
KL definition — KL is infinity when the log-ratio is not integrable or absolute continuity fails.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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