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

The guarded Fisher value is nonnegative

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_nonneg · theorem · Teaching coverage

Statement

For arbitrary μ and π on finite-dimensional Euclidean space and a supplied smooth finite score-domain witness h, the canonical Fisher value is nonnegative. It is the integral of a pointwise squared Euclidean norm, and therefore cannot be negative.

\[0\le I_h(\mu\Vert\pi)=\int_E\|\nabla r(x)\|^2\,d\mu(x).\]

All objects and hypotheses

  • ι is a finite index type (Fintype ι), and E = EuclideanSpace ℝ ι has its standard real inner product, norm, topology and Borel measurable structure. Empty ι is allowed; no Nonempty ι assumption is made.
  • μ and π are arbitrary measures on E. No probability, finite-total-mass, or normalization hypothesis is present.
  • Use the exact selected functions ρ(x) = (μ.rnDeriv π x).toReal and r(x) = RNLogRatio.logRatio μ π x = MeasureTheory.llr μ π x = Real.log(ρ(x)); put q(x) = ‖gradient r x‖². These are fixed by the original ordered pair (μ,π), not arbitrary versions.
  • The supplied witness h (or hscore) proves all three conditions: μ ≪ π; r is classically Fréchet differentiable over ℝ at μ-almost every x; and q is μ-integrable (including its a.e. strong measurability and finite integral of its norm).

Mathematical proof

1. Use the squared-score representation

Replace the named guarded quantity with the μ-integral of q.

\[I_h(\mu\Vert\pi)=\int_Eq\,d\mu.\]
Corresponding Lean step

information_eq_integral_scoreSq mu pi h

2. Establish pointwise nonnegativity

Every real square is nonnegative, including the square of the gradient's norm at each point. This does not require differentiability at that point because the gradient expression is totalized.

\[\forall x\in E,\quad 0\le\|\nabla r(x)\|^2=q(x).\]
Corresponding Lean step

sq_nonneg ‖gradient (RNLogRatio.logRatio mu pi) x‖

3. Integrate the nonnegative function

The Bochner integral of a pointwise nonnegative real function is nonnegative; in this guarded use q is additionally integrable by hypothesis.

\[0\le\int_Eq\,d\mu=I_h(\mu\Vert\pi).\]
Corresponding Lean step

MeasureTheory.integral_nonneg

Lean statement · information_nonneg

The theorem concludes only a lower bound of zero for the same guarded real-valued Fisher quantity. It has no probability-law assumption and does not state when equality is possible.

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_nonneg
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    0 ≤ information mu pi h

Exact module and namespace context

Lean proof · information_nonneg

The proof rewrites the Fisher value as the score integral, observes that every squared norm is nonnegative, and applies the integral-positivity theorem. It does not need to reprove integrability, since the certificate already supplies it.

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_nonneg
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    0 ≤ information mu pi h := by
  rw [information_eq_integral_scoreSq mu pi h]
  exact integral_nonneg (fun x => sq_nonneg ‖gradient (RNLogRatio.logRatio mu pi) x‖)

/-- The guarded value does not depend on the proof witness used to establish the
same smooth finite score domain. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • This is the selected RN/log-ratio and its totalized classical gradient, not a representative-free Sobolev score. Equality of log-ratios merely a.e. does not by itself identify their gradients. Mathlib sets gradient to zero at nondifferentiable points; the score-domain witness excludes those points only μ-a.e.
  • No existence of the smooth score domain is proved. No weak derivative, Sobolev-domain membership, lower-semicontinuous or extended-valued Fisher extension, or square-root-density identity 4∫‖∇√ρ‖² dπ is established.
  • Nonnegativity does not show that zero Fisher implies μ=π, establish strict positivity, or identify the value with a source Sobolev energy.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • MeasureTheory.integral_nonneg
  • sq_nonneg
  • gradient

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.