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

A zero supplied gradient gives zero pointwise energy

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

Statement

For arbitrary functions q,r:E→ℝ on finite-dimensional Euclidean space, if the totalized gradient of r at x is zero, then densityEnergy(q,r,x)=0. No restriction on the sign or magnitude of q(x) is needed.

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

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 hgrad asserts gradient r x=0 as an equality of vectors. No differentiability premise is included.

Mathematical proof

1. Substitute the zero gradient

Its norm and squared norm are zero, so multiplication by any real q(x) leaves zero.

\[e_{q,r}(x)=q(x)\|0\|^2=q(x)\cdot0=0.\]
Corresponding Lean step

simp [RelativeFisher.densityEnergy, hgrad]

Lean statement · densityEnergy_eq_zero_of_gradient_eq_zero

The gradient equality is supplied, not inferred from equality or constancy of function values at a point. The weight is arbitrary.

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_eq_zero_of_gradient_eq_zero
    {q logRatio : State (ι := ι) → ℝ} {x : State (ι := ι)}
    (hgrad : gradient logRatio x = 0) :
    densityEnergy q logRatio x = 0

Exact module and namespace context

Lean proof · densityEnergy_eq_zero_of_gradient_eq_zero

Unfold the energy, replace the gradient by zero, and simplify the norm, square and product.

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_eq_zero_of_gradient_eq_zero
    {q logRatio : State (ι := ι) → ℝ} {x : State (ι := ι)}
    (hgrad : gradient logRatio x = 0) :
    densityEnergy q logRatio x = 0 := by
  simp [densityEnergy, hgrad]

/-- If the relative score vanishes almost everywhere, then the relative Fisher
information vanishes.  This statement needs no positivity or normalization
assumption on `q`; those belong to the source-facing density bridge. -/

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.
  • A zero totalized gradient may reflect nondifferentiability; this implication does not establish genuine differentiability or characterize when the energy vanishes.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • norm_zero
  • zero_pow
  • mul_zero

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.