Move the score integral from μ to the reference measure

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_eq_integral_density_mul_scoreSq · theorem · Teaching coverage

Statement

Let μ and π be measures on finite-dimensional Euclidean space. Assume μ is σ-finite, a Lebesgue decomposition of μ with respect to π is available, and h proves μ≪π, differentiability of the selected log-ratio r μ-a.e., and integrability of q=‖∇r‖² under μ. Then the same canonical Fisher value equals the π-integral of the selected real RN density times the same squared score. Only the integration measure changes; both ρ and q retain the original pair (μ,π).

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

Mathematical proof

theorem information_eq_integral_density_mul_scoreSq
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h =
      ∫ x, RNLogRatio.density mu pi x * scoreSq mu pi x ∂pi

theorem information_eq_integral_density_mul_scoreSq
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h =
      ∫ x, RNLogRatio.density mu pi x * scoreSq mu pi x ∂pi := by
  rw [information_eq_integral_scoreSq mu pi h]
  simpa [RNLogRatio.density] using
    (MeasureTheory.integral_toReal_rnDeriv_mul
      (f := scoreSq mu pi) h.absolutelyContinuous).symm

/-- The squared score is integrable by the domain contract, rather than by an
implicit convention of the total integral. -/

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.
• 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.
• The RN formula is a reused totalized-integral identity; genuine finite-energy interpretation here is supported by h.scoreSq_integrable. Its companion integrability theorem is contextual, not a direct dependency of the displayed proof.
• No σ-finiteness of π, probability normalization, pointwise positivity of ρ, or smooth density version is inferred.
• Changing only the integration measure does not justify changing either measure argument inside RNLogRatio or scoreSq.