The guarded value is the squared-score integral under μ

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

Statement

For measures μ and π on finite-dimensional Euclidean space and an explicit smooth finite score-domain witness h, the canonical Fisher value equals the μ-integral of the squared gradient of the selected RN log-ratio. The domain witness makes the integrand genuinely integrable; the equality itself follows by removing the unit weight in the reused definition.

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.
• 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_scoreSq
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h = ∫ x, scoreSq mu pi x ∂mu

theorem information_eq_integral_scoreSq
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h = ∫ x, scoreSq mu pi x ∂mu := by
  simp [information, RelativeFisher.information, RelativeFisher.densityEnergy, scoreSq]

/-- The same canonical Fisher information rewritten against the reference
measure using Mathlib's Radon--Nikodym integral formula:

`FI(mu || pi) = integral density(mu|pi) * scoreSq(mu|pi) dpi`.

Crucially, this changes only the integration measure.  The integrand keeps the
original `mu` parameter; rewriting `mu` itself as a `withDensity` measure would
incorrectly rewrite the score object as well. -/

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.
• This theorem does not require σ-finiteness or a Lebesgue-decomposition instance because it only unfolds the μ-based definition.
• No finiteness of KL divergence or entropy is asserted.