Samplinglib mathematical lesson

A nonnegative weight gives nonnegative pointwise energy

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RelativeFisher.densityEnergy_nonneg · theorem · Teaching coverage

Read this first

Mathematical statement

For arbitrary functions q,r:E→ℝ on finite-dimensional Euclidean space and a point x, if q(x)≥0 then the pointwise densityEnergy(q,r,x) is nonnegative.

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

Lean statement · densityEnergy_nonneg

The sole mathematical premise is a sign condition at this point. The conclusion is a pointwise real inequality, not an integral bound.

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)

theorem densityEnergy_nonneg
    {q logRatio : State (ι := ι) → ℝ} {x : State (ι := ι)}
    (hq : 0 ≤ q x) :
    0 ≤ densityEnergy q logRatio x

Exact module and namespace context

Proof roadmap

1Use the squared-norm sign
The squared norm is a real square and is always nonnegative, including when the gradient is its default zero.
2Multiply nonnegative factors
Combine the supplied weight inequality with the squared-norm inequality.

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∈E and hq proves only the pointwise inequality q(x)≥0. No global nonnegativity or measure hypothesis.

Mathematical proof

1. Use the squared-norm sign

The squared norm is a real square and is always nonnegative, including when the gradient is its default zero.

\[0\le\|\nabla r(x)\|^2.\]

Corresponding Lean step

sq_nonneg

2. Multiply nonnegative factors

Combine the supplied weight inequality with the squared-norm inequality.

\[0\le q(x),\quad0\le\|\nabla r(x)\|^2\Longrightarrow0\le e_{q,r}(x).\]

Corresponding Lean step

mul_nonneg hq

Lean verification

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

Lean proof · densityEnergy_nonneg

The proof applies the nonnegative-product rule to the supplied weight and a nonnegative square. No differentiability calculation is involved.

Download module (.lean)

theorem densityEnergy_nonneg
    {q logRatio : State (ι := ι) → ℝ} {x : State (ι := ι)}
    (hq : 0 ≤ q x) :
    0 ≤ densityEnergy q logRatio x := by
  exact mul_nonneg hq (sq_nonneg _)

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 global sign condition on q, density normalization, or integrated Fisher inequality is proved here.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RelativeFisher.densityEnergy

Mathlib API called (external library)

mul_nonneg
sq_nonneg

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
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.