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