ASTIS mathematical exposition

Weighted squared-gradient energy at a point

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

Statement

For finite-dimensional real Euclidean space E, arbitrary functions q,r:E→ℝ, and x∈E, define densityEnergy(q,r,x) to be q(x) times the squared norm of the totalized classical gradient of r at x. The formal inputs need not be a density and a log-ratio despite their suggestive names.

\[e_{q,r}(x):=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, 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.
x is any point of E; no nonnegativity, normalization, measure, or integrability premise.

Construction and meaning

1. Measure the gradient's squared length

The globally defined gradient expression supplies a vector, and its squared norm supplies a nonnegative real factor.

\[v(x):=\nabla r(x),\qquad\|v(x)\|^2\ge0.\]

Corresponding Lean step

gradient

2. Multiply by the supplied weight

Use q(x) exactly as provided. The resulting energy need not be nonnegative if q(x) is negative.

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

Corresponding Lean step

RelativeFisher.densityEnergy

Lean statement · densityEnergy

The construction returns one real value from two functions and one point. It contains no assertion that q is an RN density or that r is differentiable.

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 densityEnergy
    (q logRatio : State (ι := ι) → ℝ) (x : State (ι := ι)) : ℝ

Exact module and namespace context

Lean construction · densityEnergy

This definition multiplies the supplied weight by a squared gradient norm. Analytic regularity and density interpretation must be justified by a later interface.

noncomputable def densityEnergy
    (q logRatio : State (ι := ι) → ℝ) (x : State (ι := ι)) : ℝ :=
  q x * ‖gradient logRatio x‖ ^ 2

/-- Relative Fisher information with respect to an explicit base measure.

For the usual Euclidean density representation the base measure will be
Lebesgue measure and `q` will be the density of `mu`; equivalently the integral
is `integral ||grad log(d mu / d pi)||^2 d mu` after the Radon--Nikodym bridge is
proved. -/

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.
No RN/log-ratio relation, positive density, source Fisher normalization, or square-root-energy identity is supplied.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

gradient

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Totalized classical gradient — gradient is defined via the Fréchet derivative; its zero default at nondifferentiable points is recorded at line118.
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.