Samplinglib mathematical lesson

Almost-everywhere zero gradient gives zero shared information

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

Read this first

Mathematical statement

Let β be any measure on finite-dimensional Euclidean space E and q,r:E→ℝ arbitrary functions. If the totalized gradient of r is zero β-almost everywhere, then the shared information integral is zero. No positivity, normalization, or independent integrability premise is needed.

\[\nabla r=0\quad\beta\text{-a.e.}\quad\Longrightarrow\quad\mathcal I_\beta(q,r)=\int_Eq\|\nabla r\|^2\,d\beta=0.\]

Lean statement · information_eq_zero_of_gradient_ae_eq_zero

The a.e. premise refers to gradients themselves under the explicit base measure. It is not merely an assertion that r equals a constant a.e.

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 information_eq_zero_of_gradient_ae_eq_zero
    (base : Measure (State (ι := ι)))
    (q logRatio : State (ι := ι) → ℝ)
    (hgrad : ∀ᵐ x ∂base, gradient logRatio x = 0) :
    information base q logRatio = 0

Exact module and namespace context

Proof roadmap

1Expose the defining integral
Unfold the shared information functional; the integrand remains the same weighted score energy.
2Obtain a zero integrand on the supplied full-measure set
At every point where the supplied gradient vanishes, the preceding pointwise theorem gives zero energy regardless of the weight.
3Integrate the a.e. zero function
The Bochner integral of a function equal to zero a.e. is zero; no separate integrability hypothesis is needed for this theorem.

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.
β is an arbitrary measure on E, without probability or finiteness assumptions.
hgrad is the β-a.e. equality gradient r x=0. No differentiability or integrability condition on q or r is present.

Mathematical proof

1. Expose the defining integral

Unfold the shared information functional; the integrand remains the same weighted score energy.

\[\mathcal I_\beta(q,r)=\int_Ee_{q,r}\,d\beta.\]

Corresponding Lean step

RelativeFisher.information

2. Obtain a zero integrand on the supplied full-measure set

At every point where the supplied gradient vanishes, the preceding pointwise theorem gives zero energy regardless of the weight.

\[\nabla r(x)=0\Longrightarrow e_{q,r}(x)=0,\qquad e_{q,r}=0\quad\beta\text{-a.e.}.\]

Corresponding Lean step

filter_upwards; RelativeFisher.densityEnergy_eq_zero_of_gradient_eq_zero

3. Integrate the a.e. zero function

The Bochner integral of a function equal to zero a.e. is zero; no separate integrability hypothesis is needed for this theorem.

\[e_{q,r}=0\quad\beta\text{-a.e.}\Longrightarrow\int_E e_{q,r}\,d\beta=0.\]

Corresponding Lean step

MeasureTheory.integral_eq_zero_of_ae

Lean verification

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

Lean proof · information_eq_zero_of_gradient_ae_eq_zero

The proof first unfolds information, then transfers the supplied zero-gradient equality to a zero-energy equality a.e., and finally uses the zero-integral rule.

Download module (.lean)

theorem information_eq_zero_of_gradient_ae_eq_zero
    (base : Measure (State (ι := ι)))
    (q logRatio : State (ι := ι) → ℝ)
    (hgrad : ∀ᵐ x ∂base, gradient logRatio x = 0) :
    information base q logRatio = 0 := by
  rw [information]
  apply integral_eq_zero_of_ae
  filter_upwards [hgrad] with x hx
  exact densityEnergy_eq_zero_of_gradient_eq_zero hx

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.
An equality a.e. of function values does not by itself identify classical gradients. No pointwise choice on exceptional null sets or independence under arbitrary null-set changes is proved.
This is a sufficient condition, not a converse: zero totalized information does not in general imply a zero genuine score or equality of measures.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.integral_eq_zero_of_ae

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Bochner integral of an a.e. zero function — The exact final theorem has no separate integrability premise.
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.