Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

A zero supplied gradient gives zero pointwise energy

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

Read this first

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

Download module (.lean)
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

Proof roadmap

  1. 1Substitute the zero gradient

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

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

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

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.

Download module (.lean)
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]

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.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • norm_zero
  • zero_pow
  • mul_zero

Mathematical sources

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