ASTIS mathematical exposition

Squared score of the selected RN log-ratio

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.scoreSq · def · Teaching coverage

Statement

Let μ and π be arbitrary measures on a finite-dimensional real Euclidean space E and let x∈E. Form the specific Mathlib RN log-ratio r(x)=log((dμ/dπ)selected(x).toReal). The canonical squared score at x is the squared Euclidean norm of the totalized classical gradient of this very function r.

\[\rho(x):=(\mu.\mathrm{rnDeriv}\,\pi\,x).\mathrm{toReal},\qquad r(x):=\log\rho(x),\qquad q(x):=\|\nabla r(x)\|^2.\]

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.
x is any point of E. This definition has no absolute-continuity, differentiability, integrability, σ-finiteness, or Lebesgue-decomposition premise.

Construction and meaning

1. Fix the log-ratio function

Use the canonical RNLogRatio.logRatio attached to the original measures. This is Mathlib's selected log-likelihood ratio; it is not a user-selected smooth density representative.

\[r=\mathrm{llr}(\mu,\pi)=\log\big((\mu.\mathrm{rnDeriv}\,\pi).\mathrm{toReal}\big).\]

Corresponding Lean step

RNLogRatio.logRatio mu pi

2. Take the totalized Euclidean gradient

Mathlib represents a derivative by its Riesz-dual vector when the classical derivative exists, and uses zero when it does not. Thus this operation is globally defined before a regularity domain has been supplied.

\[\nabla r(x)=(\mathrm{toDual}_{\mathbb R,E})^{-1}(\mathrm{fderiv}_{\mathbb R}r(x)).\]

Corresponding Lean step

gradient (RNLogRatio.logRatio mu pi) x

3. Measure its squared length

Take the norm of the gradient vector and square it. This completes a construction, not a proof of differentiability or integrability.

\[q(x)=\|\nabla r(x)\|^2.\]

Corresponding Lean step

‖gradient (RNLogRatio.logRatio mu pi) x‖ ^ 2

Lean statement · scoreSq

The definition takes two measures and one state and returns a real number. No hypothesis accompanies it, so its availability does not certify that the chosen log-ratio is differentiable at that state.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

noncomputable def scoreSq
    (mu pi : Measure (State (ι := ι)))
    (x : State (ι := ι)) : ℝ

Exact module and namespace context

Lean construction · scoreSq

The body first obtains the fixed log-ratio function, then its Mathlib gradient at the input point, and finally a squared norm. These are existing operations; the later domain structure is what justifies interpreting the result as a classical finite score energy.

noncomputable def scoreSq
    (mu pi : Measure (State (ι := ι)))
    (x : State (ι := ι)) : ℝ :=
  ‖gradient (RNLogRatio.logRatio mu pi) x‖ ^ 2

/-- Explicit regularity contract for the smooth finite branch of relative
Fisher information.

The future Sobolev/Dirichlet-energy extension should map into this contract on
its smooth finite subdomain; it should not weaken or erase these obligations. -/

Exact module and namespace context

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.
Real.log and ENNReal.toReal are totalized (log 0 = 0 and ∞.toReal = 0). Without the separately stated decomposition/σ-finiteness/absolute-continuity assumptions, this notation alone is not a theorem that ρ represents dμ/dπ with a finite positive value.
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.
No identification with ∇log of an arbitrary smooth version of a density is supplied.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.logRatio

Mathlib API called (external library)

gradient

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
ASTIS selected RN density and log-ratio — Definitions density and logRatio plus pointwise logRatio_apply at line45; representative conventions only.
Mathlib gradient and its nondifferentiable default — Definition gradient; gradient_eq_zero_of_not_differentiableAt is at line118.
Existing selected-score representative boundary in the downstream module card — Context only, not a dependency of either current module. The card explicitly preserves selected-RN versus Sobolev-score limits and records independent source certification withheld for that downstream transport packet. No status is changed here.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.