Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

A nonnegative weight gives nonnegative pointwise energy

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

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

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

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

Exact module and namespace context

Lean proof · densityEnergy_nonneg

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

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.

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

/-- A vanishing relative score gives zero pointwise Fisher energy. -/

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • mul_nonneg
  • sq_nonneg

Mathematical sources

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