The same Dirichlet bridge written as an integral under μ

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

Statement

Under exactly the same hypotheses as the Dirichlet–Fisher bridge—μ σ-finite, a Lebesgue decomposition relative to π, a real-linear L, the smooth finite selected-score domain, the five local π-pair conditions, and Γ_L(ρ,r)=ρ‖∇r‖² π-a.e.—the Dirichlet pairing equals the μ-integral of the squared selected score. This is a reformulation of the preceding bridge using the integral definition of guarded Fisher information.

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_integral_scoreSq
    (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) =
      ∫ x, CanonicalRelativeFisher.scoreSq mu pi x ∂mu

theorem dirichletForm_density_logRatio_eq_integral_scoreSq
    (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) =
      ∫ x, CanonicalRelativeFisher.scoreSq mu pi x ∂mu := by
  rw [dirichletForm_density_logRatio_eq_information
    mu pi generator hscore hpair hgamma]
  exact CanonicalRelativeFisher.information_eq_integral_scoreSq mu pi hscore

/-- A supplied KL derivative written as minus the canonical density/log-ratio
Dirichlet form immediately becomes the standard dissipation rate `-FI`.

This theorem intentionally starts *after* the analytic law-evolution /
differentiation-under-the-integral step.  The next topology node must prove that
step for the Langevin measure flow rather than hiding it inside this algebraic
handoff. -/

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 source-facing notation does not make the selected score automatically equal to a source's Sobolev or square-root-density Fisher functional.
• No new diffusion-domain existence, integrability producer, source theorem, or entropy dissipation result.