Samplinglib mathematical lesson
Equal gradients almost everywhere give equal weighted information
AutoSamplingTheory.TechnicalLemmas.InformationTheory.RelativeFisher.information_congr_gradient_ae · theorem · Teaching coverage
Read this first
Mathematical 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).\]
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
Proof roadmap
- 1Open both energy integrals
Use the same base measure and weight, leaving only the squared-gradient factor to compare.
- 2Transfer 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.
- 3Use a.e. integral congruence
The two integrands are equal a.e., so their totalized Bochner integrals agree without needing separate integrability proofs.
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.
- β 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 verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
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.
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 := 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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- MeasureTheory.integral_congr_ae
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.