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

Canonical llr equals the explicit normalized tilt ratio a.e.
The restricted-Gaussian relative score is constant

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.

Samplinglib mathematical lesson

The restricted-Gaussian relative score is constant

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

Read this first

Mathematical statement

For η≠0, the explicit normalized log-ratio representative of the quadratic fiber centered at y against the one centered at y′ has the constant gradient η⁻¹(y−y′). The paper consumer specializes to η>0.

\[\nabla_x\!\left[-\frac{\|x-y\|^2}{2\eta}-\log Z_y+\frac{\|x-y'\|^2}{2\eta}+\log Z_{y'}\right]=\eta^{-1}(y-y').\]

Lean statement · gradient_quadratic_representative

The base measure is arbitrary because only the x-independence of its two normalizers is used. No normalization or integrability premise is smuggled into this calculus theorem.

Download module (.lean)

theorem gradient_quadratic_representative
    (mu : Measure E) {eta : ℝ} (heta : eta ≠ 0) (y y' x : E) :
    gradient
        (fun t =>
          -(‖t - y‖ ^ 2 / (2 * eta)) -
            Real.log (∫ z, Real.exp (-(‖z - y‖ ^ 2 / (2 * eta))) ∂mu) -
          (-(‖t - y'‖ ^ 2 / (2 * eta))) +
            Real.log (∫ z, Real.exp (-(‖z - y'‖ ^ 2 / (2 * eta))) ∂mu)) x =
      eta⁻¹ • (y - y')

Exact module and namespace context

Proof roadmap

1Differentiate the two quadratics
The genuine Fréchet gradients are −η⁻¹(x−y) and −η⁻¹(x−y′).
2Discard only spatial constants
The two log normalizers may depend on μ, η and the centers, but not on x, so their derivatives vanish.
3Cancel x
Subtracting the two quadratic scores cancels x and leaves the center displacement with the source sign.

Full assumptions and notation

All objects and hypotheses

E is a complete real inner-product space.
η is nonzero; SPHMC and the cited restricted-Gaussian theorem use η>0.
The differentiated function is displayed explicitly and is not Mathlib's arbitrary canonical measurable llr representative.

Mathematical proof

1. Differentiate the two quadratics

The genuine Fréchet gradients are −η⁻¹(x−y) and −η⁻¹(x−y′).

\[\nabla q_{\eta,y}(x)=-\eta^{-1}(x-y).\]

Corresponding Lean step

HasFDerivAt.norm_sq; InnerProductSpace.toDual

2. Discard only spatial constants

The two log normalizers may depend on μ, η and the centers, but not on x, so their derivatives vanish.

\[\nabla_x\log Z_y=\nabla_x\log Z_{y'}=0.\]

Corresponding Lean step

HasFDerivAt.sub_const; HasFDerivAt.add_const

3. Cancel x

Subtracting the two quadratic scores cancels x and leaves the center displacement with the source sign.

\[-\eta^{-1}(x-y)+\eta^{-1}(x-y')=\eta^{-1}(y-y').\]

Corresponding Lean step

module; map_sub

Lean verification

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

Lean proof · gradient_quadratic_representative

A private helper derives the genuine gradient of each quadratic from the norm-square derivative and the Hilbert duality map. The public proof removes constant normalizers and performs the linear cancellation.

Download module (.lean)

theorem gradient_quadratic_representative
    (mu : Measure E) {eta : ℝ} (heta : eta ≠ 0) (y y' x : E) :
    gradient
        (fun t =>
          -(‖t - y‖ ^ 2 / (2 * eta)) -
            Real.log (∫ z, Real.exp (-(‖z - y‖ ^ 2 / (2 * eta))) ∂mu) -
          (-(‖t - y'‖ ^ 2 / (2 * eta))) +
            Real.log (∫ z, Real.exp (-(‖z - y'‖ ^ 2 / (2 * eta))) ∂mu)) x =
      eta⁻¹ • (y - y') := by
  have hy := hasGradientAt_quadraticExponent heta y x
  have hy' := hasGradientAt_quadraticExponent heta y' x
  apply HasGradientAt.gradient
  rw [hasGradientAt_iff_hasFDerivAt]
  change HasFDerivAt
    (fun t => quadraticExponent eta y t -
      Real.log (∫ z, Real.exp (quadraticExponent eta y z) ∂mu) -
      quadraticExponent eta y' t +
      Real.log (∫ z, Real.exp (quadraticExponent eta y' z) ∂mu))
    (InnerProductSpace.toDual ℝ E (eta⁻¹ • (y - y'))) x
  let c := Real.log (∫ z, Real.exp (quadraticExponent eta y z) ∂mu)
  let c' := Real.log (∫ z, Real.exp (quadraticExponent eta y' z) ∂mu)
  have hderiv : HasFDerivAt
      (fun t => quadraticExponent eta y t - c - quadraticExponent eta y' t + c')
      ((InnerProductSpace.toDual ℝ E (-eta⁻¹ • (x - y))) -
        InnerProductSpace.toDual ℝ E (-eta⁻¹ • (x - y'))) x :=
    ((hy.hasFDerivAt.sub_const c).sub hy'.hasFDerivAt).add_const c'
  have hvec :
      (-eta⁻¹ • (x - y)) - (-eta⁻¹ • (x - y')) =
        eta⁻¹ • (y - y') := by
    module
  rw [← hvec, map_sub]
  simpa only [c, c'] using hderiv

end Quadratic

end

end TiltedLogRatio
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

The theorem does not differentiate the canonical measurable llr.
A representative-to-canonical-Fisher adapter, the strong-convex Gibbs LSI/T₂ backend and the W₂ contraction all remain separate red nodes.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

HasFDerivAt.norm_sq
InnerProductSpace.toDual
HasGradientAt.gradient

Mathematical sources

Lee–Shen–Tian equation (11) — Exact sign and η⁻¹ coefficient; this equation is cited in the route used by SPHMC Lemma 4.17.

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