Samplinglib mathematical lesson

A guarded finite Fisher value using the shared energy

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

Read this first

Mathematical statement

Given arbitrary measures μ and π on finite-dimensional Euclidean space and a proof h of the smooth finite score domain, define their canonical relative Fisher value by evaluating the existing RelativeFisher energy with base measure μ, constant weight one, and the selected log-ratio r. Thus the guarded value is the finite integral of the squared classical score of that representative.

\[I_h(\mu\Vert\pi):=\operatorname{RelativeFisher}(\mu,1,r)=\int_E 1\cdot\|\nabla r(x)\|^2\,d\mu(x),\qquad h:\mathcal D(\mu,\pi).\]

Lean statement · information

The last input is a proof that the pair lies in the stated domain. Although this proof is not used to compute the real-valued expression, requiring it at the interface prevents callers from presenting an unqualified totalized integral as the guarded Fisher value.

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.

Download module (.lean)

noncomputable def information
    (mu pi : Measure (State (ι := ι)))
    (_h : SmoothFiniteScoreDomain mu pi) : ℝ

Exact module and namespace context

Proof roadmap

1Use the explicit domain certificate
The input certificate guarantees a classical score μ-a.e. and integrability of its squared norm. No certificate is inferred from the measures alone.
2Choose the shared energy's three inputs
Set its base measure to μ, its multiplier to the constant function one, and its log-ratio argument to the selected r. Since μ itself is the integration measure, no additional density factor is needed here.
3Read the constructed value
The shared energy integrates its pointwise weight times squared gradient. The domain's integrability field makes this a genuine finite real integral, not an infinite-energy extension.

Full assumptions and notation

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

Construction and meaning

1. Use the explicit domain certificate

The input certificate guarantees a classical score μ-a.e. and integrability of its squared norm. No certificate is inferred from the measures alone.

\[h:\mathcal D(\mu,\pi)\ \Longrightarrow\ q\in L^1(\mu).\]

Corresponding Lean step

_h : SmoothFiniteScoreDomain mu pi

2. Choose the shared energy's three inputs

Set its base measure to μ, its multiplier to the constant function one, and its log-ratio argument to the selected r. Since μ itself is the integration measure, no additional density factor is needed here.

\[(\mathrm{base},\mathrm{weight},\mathrm{logRatio})=(\mu,1,r).\]

Corresponding Lean step

RelativeFisher.information mu (fun _ => 1) (RNLogRatio.logRatio mu pi)

3. Read the constructed value

The shared energy integrates its pointwise weight times squared gradient. The domain's integrability field makes this a genuine finite real integral, not an infinite-energy extension.

\[I_h(\mu\Vert\pi)=\int 1\cdot q\,d\mu=\int q\,d\mu.\]

Corresponding Lean step

RelativeFisher.information; RelativeFisher.densityEnergy

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean construction · information

This is a definition, not a new integral theorem. It calls the already-existing RelativeFisher functional with μ as the base measure and unit weight. The proof certificate controls admissibility; the numerical expression does not depend on how that certificate was established.

Download module (.lean)

noncomputable def information
    (mu pi : Measure (State (ι := ι)))
    (_h : SmoothFiniteScoreDomain mu pi) : ℝ :=
  RelativeFisher.information mu (fun _ => 1) (RNLogRatio.logRatio mu pi)

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.
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 second independent Fisher hierarchy is constructed. The codomain is ℝ, and inputs outside the explicit domain have no value through this guarded interface.
The domain certificate contains no probability assumption and no finite-entropy assumption; this definition alone gives neither.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Shared density-energy functional reused by definition — densityEnergy at42 and information at52 define the existing weighted Bochner integral.
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.

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