Samplinglib mathematical lesson

Identify the density–log-density Dirichlet pairing with guarded Fisher

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisher.dirichletForm_density_logRatio_eq_information · theorem · Teaching coverage

Read this first

Mathematical statement

Let μ and π be measures on finite-dimensional Euclidean space, with μ σ-finite and a Lebesgue decomposition of μ relative to π. Let L be a real-linear operator on real-valued functions. Suppose the selected RN log-ratio has a smooth finite score-domain witness hscore; the three terms L(ρr), ρLr, rLρ are π-integrable; the integral of L(ρr) is zero; the two cross integrals are equal; and Γ_L(ρ,r)=ρ‖∇r‖² π-a.e. Then the generator Dirichlet pairing of the selected density and log-ratio equals their guarded canonical Fisher value.

\[\mathcal E_\pi^L(\rho,r):=-\int_E\rho\,Lr\,d\pi\ =\ \int_E\Gamma_L(\rho,r)\,d\pi\ =\ \int_E\rho\,\|\nabla r\|^2\,d\pi\ =\ I_{h_{\mathrm{score}}}(\mu\Vert\pi).\]

Lean statement · dirichletForm_density_logRatio_eq_information

The three named witnesses carry different obligations: the score witness controls μ-a.e. classical differentiability and μ-integrability, the pair witness supplies five π-integral conditions, and the Γ witness supplies a π-a.e. equality. The bracketed RN assumptions are additional. None of these witnesses is constructed by this theorem.

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 dirichletForm_density_logRatio_eq_information
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ))
    (hscore : CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hpair : DirichletPairDomain mu pi generator)
    (hgamma : HasCanonicalFisherGamma mu pi generator) :
    FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) =
      CanonicalRelativeFisher.information mu pi hscore

Exact module and namespace context

Proof roadmap

1Apply the existing integration-by-parts theorem to the selected pair
Pass all five fields of hpair to the existing helper with base measure π, f=ρ, and g=r. The relevant second conclusion identifies the Dirichlet pairing with the integrated Γ.
2Understand why that reused identity is valid
Inside the helper, the three integrability assumptions permit subtracting integrals term by term in the Γ definition. This is explanatory expansion of the reused proof, not a newly proved helper.
3Use only the supplied local stationarity and symmetry
The first integral is zero and the two cross integrals coincide, so the half-sum is exactly minus either cross integral, with the same sign as the Dirichlet-form definition.
4Put the Fisher value over the same measure
Use the already-established RN change-of-measure formula for the fixed original score, under μ's σ-finiteness, the decomposition instance, and the absolute continuity in hscore.
5Compare the integrands almost everywhere
Now both sides are π-integrals. Apply integral congruence to hgamma; its exceptional π-null set is harmless and no pointwise-everywhere identity is needed.

Full assumptions and notation

All objects and hypotheses

ι is a finite index type (Fintype ι), and E = EuclideanSpace ℝ ι has its standard real inner product, norm, topology and Borel measurable structure. Empty ι is allowed; no Nonempty ι assumption is made.
μ and π are arbitrary measures on E. No probability, finite-total-mass, or normalization hypothesis is present.
Use the exact selected functions ρ(x) = (μ.rnDeriv π x).toReal and r(x) = RNLogRatio.logRatio μ π x = MeasureTheory.llr μ π x = Real.log(ρ(x)); put q(x) = ‖gradient r x‖². These are fixed by the original ordered pair (μ,π), not arbitrary versions.
μ is σ-finite, and the typeclass HaveLebesgueDecomposition μ π is supplied. π need not be assumed σ-finite. These are in addition to μ ≪ π in the score-domain witness.
L is a real-linear map from all functions E → ℝ to all functions E → ℝ. Its linearity alone does not say that it generates a Markov semigroup, preserves a measure, or is a diffusion.
The supplied witness h (or hscore) proves all three conditions: μ ≪ π; r is classically Fréchet differentiable over ℝ at μ-almost every x; and q is μ-integrable (including its a.e. strong measurability and finite integral of its norm).
The supplied witness hpair proves, for the fixed functions ρ and r, that L(ρr), x ↦ ρ(x)Lr(x), and x ↦ r(x)Lρ(x) are π-integrable, that ∫ L(ρr) dπ = 0, and that ∫ ρ Lr dπ = ∫ r Lρ dπ.
The supplied hgamma asserts Γ_L(ρ,r)(x) = ρ(x)q(x) for π-almost every x, where Γ_L(f,g) = ½[L(fg) − f Lg − g Lf]. It is not required pointwise everywhere.

Mathematical proof

1. Apply the existing integration-by-parts theorem to the selected pair

Pass all five fields of hpair to the existing helper with base measure π, f=ρ, and g=r. The relevant second conclusion identifies the Dirichlet pairing with the integrated Γ.

\[\mathcal E_\pi^L(\rho,r)=\int_E\Gamma_L(\rho,r)\,d\pi.\]

Corresponding Lean step

StochasticProcesses.CarreDuChamp.fundamental_integration_by_parts ...; hibp.2

2. Understand why that reused identity is valid

Inside the helper, the three integrability assumptions permit subtracting integrals term by term in the Γ definition. This is explanatory expansion of the reused proof, not a newly proved helper.

\[\int_E\Gamma_L(\rho,r)\,d\pi=\tfrac12\left[\int_EL(\rho r)\,d\pi-\int_E\rho Lr\,d\pi-\int_ErL\rho\,d\pi\right].\]

Corresponding Lean step

fundamental_integration_by_parts: hLfg.sub hfLg; integral_const_mul; integral_sub

3. Use only the supplied local stationarity and symmetry

The first integral is zero and the two cross integrals coincide, so the half-sum is exactly minus either cross integral, with the same sign as the Dirichlet-form definition.

\[\tfrac12(0-A-A)=-A=\mathcal E_\pi^L(\rho,r),\qquad A:=\int_E\rho Lr\,d\pi.\]

Corresponding Lean step

fundamental_integration_by_parts: hstationary; hsymmetric; Generator.dirichletForm

4. Put the Fisher value over the same measure

Use the already-established RN change-of-measure formula for the fixed original score, under μ's σ-finiteness, the decomposition instance, and the absolute continuity in hscore.

\[I_{h_{\mathrm{score}}}(\mu\Vert\pi)=\int_E\rho(x)q(x)\,d\pi(x).\]

Corresponding Lean step

CanonicalRelativeFisher.information_eq_integral_density_mul_scoreSq mu pi hscore

5. Compare the integrands almost everywhere

Now both sides are π-integrals. Apply integral congruence to hgamma; its exceptional π-null set is harmless and no pointwise-everywhere identity is needed.

\[\Gamma_L(\rho,r)=\rho q\quad\pi\text{-a.e.}\quad\Longrightarrow\quad\int_E\Gamma_L(\rho,r)\,d\pi=\int_E\rho q\,d\pi.\]

Corresponding Lean step

MeasureTheory.integral_congr_ae hgamma

Lean verification

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

Lean proof · dirichletForm_density_logRatio_eq_information

Lean first obtains the two-part integration-by-parts result and uses its second component. It next rewrites the Fisher side as a weighted π-integral. The remaining goal is equality of two π-integrals, which follows directly from the supplied a.e. Γ identity. The integral algebra behind the imported helper explains the factor one-half and the negative-generator sign.

Download module (.lean)

theorem dirichletForm_density_logRatio_eq_information
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ))
    (hscore : CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hpair : DirichletPairDomain mu pi generator)
    (hgamma : HasCanonicalFisherGamma mu pi generator) :
    FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) =
      CanonicalRelativeFisher.information mu pi hscore := by
  have hibp :=
    StochasticProcesses.CarreDuChamp.fundamental_integration_by_parts
      pi generator (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi)
      hpair.generator_product_integrable
      hpair.density_mul_generator_logRatio_integrable
      hpair.logRatio_mul_generator_density_integrable
      hpair.stationary_product hpair.symmetric_pair
  rw [hibp.2]
  rw [CanonicalRelativeFisher.information_eq_integral_density_mul_scoreSq
    mu pi hscore]
  exact integral_congr_ae hgamma

Exact module and namespace context

Scope and omitted-condition boundaries

This is the selected RN/log-ratio and its totalized classical gradient, not a representative-free Sobolev score. Equality of log-ratios merely a.e. does not by itself identify their gradients. Mathlib sets gradient to zero at nondifferentiable points; the score-domain witness excludes those points only μ-a.e.
These are only local pair conditions. No global stationarity, reversibility, generator-domain closure, concrete Langevin generator, or diffusion chain rule is derived.
No existence of the smooth score domain is proved. No weak derivative, Sobolev-domain membership, lower-semicontinuous or extended-valued Fisher extension, or square-root-density identity 4∫‖∇√ρ‖² dπ is established.
This bridge preserves the selected representative, generator normalization, and all three witnesses. It does not produce a concrete Γ formula or show that any diffusion satisfies the hypotheses.
The source card belongs to the reused integration-by-parts helper. This combined canonical Fisher edge is not assigned a new numbered source theorem or a source-equivalence certification.
No probability normalization, entropy identity, or law-evolution statement is required or concluded.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.integral_congr_ae

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Reused fundamental integration-by-parts proof — Direct helper; its integral expansion is explained in steps2–3, not reimplemented.
Dirichlet-form sign convention — Eπ(f,g)=−∫f Lg dπ.
Existing canonical RN transport identity — Direct adapter carrying μ σ-finiteness, the decomposition instance, and the exact score representative.
Mathlib a.e. integral congruence — Direct final equality of π-integrals.
Existing source-correspondence card: chewi-1-2-theorem-1-2-14 — Existing local source-correspondence entry for the reused fundamental_integration_by_parts theorem. It records Chewi Theorem 1.2.14, edition 2026-08-09, printed p.14/PDF p.26, status compiled, with three integrability inputs, stationarity and symmetry. This exposition does not independently re-audit that source or promote the canonical Fisher bridge to a numbered source theorem.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

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