ASTIS mathematical exposition

Integrate the supplied weighted score energy

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

Statement

On finite-dimensional real Euclidean space E, let β be any measure and q,r:E→ℝ arbitrary functions. Define the shared RelativeFisher information to be the real Bochner integral of q‖∇r‖² under β. This layer has no domain guard, so existence of the real-valued expression does not imply genuine finite Fisher energy.

\[\mathcal I_\beta(q,r):=\int_E e_{q,r}(x)\,d\beta(x)=\int_Eq(x)\|\nabla r(x)\|^2\,d\beta(x).\]

All objects and hypotheses

ι is a finite index type (Fintype ι), and E=EuclideanSpace ℝ ι has its standard real inner product, topology and Borel measurable structure. Empty ι is allowed.
q and r are arbitrary functions E→ℝ. Their argument names do not assert that q is a density or r is a log-density; neither measurability nor differentiability is assumed.
β is any measure on E; it need not be probability, finite, σ-finite, or Lebesgue measure.
No Integrable e β, nonnegative q, normalized q, or differentiability premise.

Construction and meaning

1. Form the supplied energy integrand

Use the existing densityEnergy expression without changing the supplied q or r.

\[e_{q,r}(x)=q(x)\|\nabla r(x)\|^2.\]

Corresponding Lean step

RelativeFisher.densityEnergy

2. Take its totalized real integral

Integrate against the explicit base β. The integrable case has the usual finite integral; if integrability fails, Mathlib assigns zero.

\[\mathcal I_\beta(q,r)=\int_E e_{q,r}\,d\beta,\qquad e_{q,r}\notin L^1(\beta)\Longrightarrow\mathcal I_\beta(q,r)=0.\]

Corresponding Lean step

MeasureTheory.integral; integral_undef

Lean statement · information

The base measure is an explicit parameter, not fixed to Lebesgue measure or to a probability law. Unlike CanonicalRelativeFisher.information, this definition takes no admissibility certificate.

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 information
    (base : Measure (State (ι := ι)))
    (q logRatio : State (ι := ι) → ℝ) : ℝ

Exact module and namespace context

Lean construction · information

The body simply integrates the already-defined pointwise energy. It does not prove integrability, density reconstruction, or any equality with a measure-level Fisher quantity.

noncomputable def information
    (base : Measure (State (ι := ι)))
    (q logRatio : State (ι := ι) → ℝ) : ℝ :=
  ∫ x, densityEnergy q logRatio x ∂base

/-- Fisher energy density is nonnegative wherever the supplied density is
nonnegative. -/

Exact module and namespace context

Scope and omitted-condition boundaries

gradient is the totalized classical gradient, equal to zero at nondifferentiable points. No classical differentiability, weak derivative, Sobolev domain, or selected-representative/score equivalence follows merely from writing it.
The real Bochner integral is totalized: a nonintegrable integrand has integral 0. No finite-energy or extended-valued Fisher interpretation is supplied unless the relevant analytic domain is established separately.
No general nonnegativity is claimed for arbitrary signed q. No normalization, KL relation, RN measure-change identity, or Sobolev/square-root Fisher equivalence is built into this definition.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RelativeFisher.densityEnergy

Mathlib API called (external library)

MeasureTheory.integral

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Nonintegrable Bochner-integral convention — integral_undef explains the totalization; it is not an explicit call in this definition.
Later guarded specialization, not a dependency here — The later module supplies a smooth finite score-domain witness and selects base μ, unit weight and the canonical log-ratio.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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