Samplinglib mathematical lesson

Canonical llr equals the explicit normalized tilt ratio a.e.

AutoSamplingTheory.TechnicalLemmas.InformationTheory.TiltedLogRatio.llr_tilted_tilted_ae · theorem · Teaching coverage

Read this first

Mathematical statement

For a σ-finite base μ and two integrable exponential tilts, Mathlib's canonical log-likelihood ratio of the f-tilt against the g-tilt agrees almost everywhere under the left tilted law with f−log Z_f−g+log Z_g.

\[\operatorname{llr}(\mu_f,\mu_g)(x)=f(x)-\log Z_f-g(x)+\log Z_g\quad\mu_f\text{-a.e.}\]

Lean statement · llr_tilted_tilted_ae

The right-hand side is written explicitly in the public theorem, so no hidden selected representative occurs in its interface.

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 llr_tilted_tilted_ae
    (mu : Measure X) [SigmaFinite mu] (f g : X → ℝ)
    (hf : Measurable f)
    (hfi : Integrable (fun x => Real.exp (f x)) mu)
    (hgi : Integrable (fun x => Real.exp (g x)) mu) :
    MeasureTheory.llr (mu.tilted f) (mu.tilted g) =ᵐ[mu.tilted f]
      fun x => f x - Real.log (∫ z, Real.exp (f z) ∂mu) - g x +
        Real.log (∫ z, Real.exp (g z) ∂mu)

Exact module and namespace context

Proof roadmap

1Expand the left tilt
Mathlib's left-tilt identity contributes f−log Z_f and leaves a base-to-right-tilt llr.
2Expand the right tilt
The right-tilt identity contributes −g+log Z_g, while the self log ratio is zero.
3Transfer the null set
The equality is first assembled μ-a.e. and then transported to μ_f because every tilted measure is absolutely continuous with respect to its base.

Full assumptions and notation

All objects and hypotheses

The common base μ is σ-finite.
f is measurable and both exp f and exp g are μ-integrable.
The equality is under the left tilt μ_f, which is the law used by relative Fisher information.

Mathematical proof

1. Expand the left tilt

Mathlib's left-tilt identity contributes f−log Z_f and leaves a base-to-right-tilt llr.

\[\operatorname{llr}(\mu_f,\mu_g)=f-\log Z_f+\operatorname{llr}(\mu,\mu_g).\]

Corresponding Lean step

MeasureTheory.llr_tilted_left

2. Expand the right tilt

The right-tilt identity contributes −g+log Z_g, while the self log ratio is zero.

\[\operatorname{llr}(\mu,\mu_g)=-g+\log Z_g.\]

Corresponding Lean step

MeasureTheory.llr_tilted_right; MeasureTheory.llr_self

3. Transfer the null set

The equality is first assembled μ-a.e. and then transported to μ_f because every tilted measure is absolutely continuous with respect to its base.

\[\mu_f\ll\mu.\]

Corresponding Lean step

MeasureTheory.tilted_absolutelyContinuous

Lean verification

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

Lean proof · llr_tilted_tilted_ae

The proof combines the three canonical Mathlib llr identities pointwise on a full-measure set and uses absolute continuity to change the a.e. measure.

Download module (.lean)

theorem llr_tilted_tilted_ae
    (mu : Measure X) [SigmaFinite mu] (f g : X → ℝ)
    (hf : Measurable f)
    (hfi : Integrable (fun x => Real.exp (f x)) mu)
    (hgi : Integrable (fun x => Real.exp (g x)) mu) :
    MeasureTheory.llr (mu.tilted f) (mu.tilted g) =ᵐ[mu.tilted f]
      fun x => f x - Real.log (∫ z, Real.exp (f z) ∂mu) - g x +
        Real.log (∫ z, Real.exp (g z) ∂mu) := by
  have hbase :
      MeasureTheory.llr (mu.tilted f) (mu.tilted g) =ᵐ[mu]
        representative mu f g := by
    filter_upwards [
      MeasureTheory.llr_tilted_left
        (μ := mu) (ν := mu.tilted g) (f := f)
        (absolutelyContinuous_tilted hgi) hfi hf.aemeasurable,
      MeasureTheory.llr_tilted_right
        (μ := mu) (ν := mu) (f := g)
        Measure.AbsolutelyContinuous.rfl hgi,
      MeasureTheory.llr_self mu] with x hleft hright hself
    rw [hleft, hright, hself]
    simp [representative]
    ring
  exact (tilted_absolutelyContinuous mu f).ae_eq hbase

section Quadratic

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [CompleteSpace E]
  [MeasurableSpace E] [BorelSpace E]

Exact module and namespace context

Scope and omitted-condition boundaries

Almost-everywhere equality of values does not identify classical gradients of arbitrary representatives.
No Fisher-information, log-Sobolev, Talagrand or Wasserstein conclusion is included.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.llr_tilted_left
MeasureTheory.llr_tilted_right
MeasureTheory.llr_self
MeasureTheory.tilted_absolutelyContinuous

Mathematical sources

Lee–Shen–Tian, Lemma 2 proof, equation (11) — ASTIS exposes the normalized-density representative and its canonical RN relation, implicit in the paper calculation.

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