ASTIS mathematical exposition

The explicit smooth finite score domain

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.SmoothFiniteScoreDomain · structure · Teaching coverage

Statement

For arbitrary measures μ and π on finite-dimensional Euclidean space, SmoothFiniteScoreDomain μ π is the conjunction of three actual mathematical requirements: μ is absolutely continuous with respect to π; the selected RN log-ratio r is classically differentiable at μ-almost every point; and its squared totalized gradient q is integrable with respect to μ. A witness must prove all three. This declaration does not prove that any given pair belongs to the domain.

\[\mathcal D(\mu,\pi)\;:\Longleftrightarrow\;\mu\ll\pi\ \land\ [r\text{ is Fréchet differentiable at }x\text{ for }\mu\text{-a.e. }x]\ \land\ q\in L^1(\mu),\qquad q=\|\nabla r\|^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.
The structure itself takes only μ and π; its three fields are obligations to prove, not assumptions automatically generated by declaring the structure.
No σ-finiteness or HaveLebesgueDecomposition instance is part of this domain. No probability normalization, strict positivity everywhere, or global smoothness is asserted.

Construction and meaning

1. Supply absolute continuity

Prove that every π-null measurable set is μ-null. This is the first field of a domain witness; it is independent of the later differentiability requirement.

\[\mu\ll\pi.\]

Corresponding Lean step

SmoothFiniteScoreDomain.absolutelyContinuous

2. Supply classical differentiability at almost every μ-point

Prove differentiability of the exact function r on the ambient Euclidean space at all points outside a μ-null exceptional set. The filter is μ, not π or Lebesgue measure.

\[\mu\text{-a.e. }x:\quad r\text{ is differentiable at }x.\]

Corresponding Lean step

SmoothFiniteScoreDomain.differentiable_ae

3. Supply finite score integrability

Prove that q is a.e. strongly measurable and that the integral of its norm is finite. This prevents a real Bochner integral from merely returning its default value for a nonintegrable expression.

\[q\in L^1(\mu),\qquad \int |q|\,d\mu<\infty.\]

Corresponding Lean step

SmoothFiniteScoreDomain.scoreSq_integrable

4. Package the three proofs

Only after all three proofs have been obtained may they be collected into one witness of the proposition. The structure records these facts without deriving one from another.

\[(h_{\mathrm{ac}},h_{\mathrm{diff}},h_{L^1})\;:\;\mathcal D(\mu,\pi).\]

Corresponding Lean step

SmoothFiniteScoreDomain.mk

Lean statement · SmoothFiniteScoreDomain

The result is a proposition with three named proof fields, not descriptive metadata or a string-valued contract. The phrase almost everywhere in the differentiability field refers specifically to μ. Integrable includes both the relevant measurability and finite-norm-integral requirement.

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.

structure SmoothFiniteScoreDomain
    (mu pi : Measure (State (ι := ι))) : Prop where
  absolutelyContinuous : mu ≪ pi
  differentiable_ae :
    ∀ᵐ x ∂mu, DifferentiableAt ℝ (RNLogRatio.logRatio mu pi) x
  scoreSq_integrable : Integrable (scoreSq mu pi) mu

/-- Canonical relative Fisher information on the explicit smooth finite score
domain.

It is exactly the existing `RelativeFisher.information` with base measure `mu`
and density `1`, so no second Fisher hierarchy is introduced. -/

Exact module and namespace context

Lean construction · SmoothFiniteScoreDomain

A structure declaration defines what a certificate must contain; it does not itself construct a certificate. A user must independently prove absolute continuity, differentiability of this selected representative, and squared-score integrability before using the guarded Fisher value.

structure SmoothFiniteScoreDomain
    (mu pi : Measure (State (ι := ι))) : Prop where
  absolutelyContinuous : mu ≪ pi
  differentiable_ae :
    ∀ᵐ x ∂mu, DifferentiableAt ℝ (RNLogRatio.logRatio mu pi) x
  scoreSq_integrable : Integrable (scoreSq mu pi) mu

/-- Canonical relative Fisher information on the explicit smooth finite score
domain.

It is exactly the existing `RelativeFisher.information` with base measure `mu`
and density `1`, so no second Fisher hierarchy is introduced. -/

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.
Differentiable μ-a.e. is not C¹ smoothness, smoothness on the support, differentiability π-a.e., or a weak-derivative assertion.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.Measure.AbsolutelyContinuous
DifferentiableAt
MeasureTheory.Integrable
Filter.Eventually

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Selected log-ratio definition — Identifies the exact function appearing in the differentiability field.
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.