Samplinglib mathematical lesson

Weighted squared-gradient energy at a point

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

Read this first

Mathematical 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.\]

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.

Download module (.lean)

noncomputable def densityEnergy
    (q logRatio : State (ι := ι) → ℝ) (x : State (ι := ι)) : ℝ

Exact module and namespace context

Proof roadmap

1Measure the gradient's squared length
The globally defined gradient expression supplies a vector, and its squared norm supplies a nonnegative real factor.
2Multiply by the supplied weight
Use q(x) exactly as provided. The resulting energy need not be nonnegative if q(x) is negative.

Full assumptions and notation

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 verification

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

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.

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

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

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