ASTIS mathematical exposition

Equal gradients almost everywhere give equal weighted information

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

Statement

Let β be any measure on finite-dimensional Euclidean space and let q,r,s:E→ℝ be arbitrary functions. If the totalized gradients of r and s agree β-almost everywhere, their shared weighted information values with the same weight q and base β are equal. No equality of r and s themselves is required.

\[\nabla r=\nabla s\quad\beta\text{-a.e.}\quad\Longrightarrow\quad\mathcal I_\beta(q,r)=\mathcal I_\beta(q,s).\]

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.
β is any measure on E, and q,r,s are arbitrary real-valued functions on E.
hgrad supplies gradient r x=gradient s x for β-almost every x; no function-value equality, differentiability, nonnegativity or integrability premise is included.
The base β and the weight q are identical on both sides.

Mathematical proof

1. Open both energy integrals

Use the same base measure and weight, leaving only the squared-gradient factor to compare.

\[\mathcal I_\beta(q,r)=\int_Eq\|\nabla r\|^2\,d\beta,\qquad\mathcal I_\beta(q,s)=\int_Eq\|\nabla s\|^2\,d\beta.\]

Corresponding Lean step

RelativeFisher.information; RelativeFisher.densityEnergy

2. Transfer gradient equality to energy equality

At points in the supplied full-β-measure set, equal vectors have equal squared norms, and multiplication by the same q preserves equality.

\[\nabla r(x)=\nabla s(x)\Longrightarrow q(x)\|\nabla r(x)\|^2=q(x)\|\nabla s(x)\|^2.\]

Corresponding Lean step

filter_upwards; simp [RelativeFisher.densityEnergy, hx]

3. Use a.e. integral congruence

The two integrands are equal a.e., so their totalized Bochner integrals agree without needing separate integrability proofs.

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

Corresponding Lean step

MeasureTheory.integral_congr_ae

Lean statement · information_congr_gradient_ae

The hypothesis compares gradients, not log-ratio values. No equality of function values is required. Conversely, an a.e. function-value identity alone is not the premise here: the gradient equality must be supplied separately.

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

Exact module and namespace context

Lean proof · information_congr_gradient_ae

The proof rewrites both functional names as integrals, uses the gradient hypothesis to make their integrands equal a.e., and applies integral congruence. It does not prove the gradient equality.

theorem information_congr_gradient_ae
    (base : Measure (State (ι := ι)))
    (q r s : State (ι := ι) → ℝ)
    (hgrad : ∀ᵐ x ∂base, gradient r x = gradient s x) :
    information base q r = information base q s := by
  rw [information, information]
  apply integral_congr_ae
  filter_upwards [hgrad] with x hx
  simp [densityEnergy, hx]

end

end RelativeFisher
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

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.
The real Bochner integral is totalized: a nonintegrable integrand has integral 0. No finite-energy or extended-valued Fisher interpretation is supplied unless the relevant analytic domain is established separately.
This is not automatic independence of Fisher information under arbitrary a.e. changes to an RN/log-ratio representative. Actual a.e. gradient equality is the required adapter.
No change of base measure, weight, weak/classical derivative domain or source Fisher definition is covered.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.integral_congr_ae

Mathematical sources

Exact existing ASTIS declaration and body — Local source authority; renderer extracts the exact code.
Bochner a.e. integral congruence — Direct comparison theorem; valid for totalized integrals with no independent integrability assumptions.
Existing declaration-visibility check — Read-only #check evidence; no build/test run.

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