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

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

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.

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

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

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

/-- Equivalent source-facing integral form of the same bridge. -/

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.