The guarded value is exactly the shared RelativeFisher energy

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

Statement

For arbitrary μ and π on finite-dimensional Euclidean space, and any witness h that μ≪π, the selected log-ratio r is differentiable μ-a.e., and its squared gradient is μ-integrable, the canonical guarded Fisher value is exactly RelativeFisher.information with base μ, unit weight, and log-ratio r. This equality is built into the 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_relativeFisher
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h =
      RelativeFisher.information mu (fun _ => 1) (RNLogRatio.logRatio mu pi)

theorem information_eq_relativeFisher
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h =
      RelativeFisher.information mu (fun _ => 1) (RNLogRatio.logRatio mu pi) := by
  rfl

/-- On the guarded smooth finite domain, the canonical Fisher information has
the expected measure-level formula

`FI(mu || pi) = integral ||grad log(d mu / d pi)||^2 dmu`. -/

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 wrapper is not an independent analytic identification with a Sobolev, Dirichlet, or source-defined Fisher quantity.