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

The guarded value is the squared-score integral under μ

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

Read this first

Mathematical statement

For measures μ and π on finite-dimensional Euclidean space and an explicit smooth finite score-domain witness h, the canonical Fisher value equals the μ-integral of the squared gradient of the selected RN log-ratio. The domain witness makes the integrand genuinely integrable; the equality itself follows by removing the unit weight in the reused definition.

\[I_h(\mu\Vert\pi)=\int_E q(x)\,d\mu(x)=\int_E\|\nabla r(x)\|^2\,d\mu(x),\qquad q\in L^1(\mu).\]
Lean statement · information_eq_integral_scoreSq

The conclusion is an equality of real numbers. The same selected score appears in the named functional and in the integral, and the domain assumption includes the integrability needed to read that integral as a finite energy.

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_integral_scoreSq
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h = ∫ x, scoreSq mu pi x ∂mu

Exact module and namespace context

Proof roadmap

  1. 1Open the shared-energy definition

    The guarded value uses μ as the base measure and the constant multiplier one.

  2. 2Expand the pointwise energy

    The density-energy definition is weight times squared gradient norm.

  3. 3Remove the unit multiplier

    Multiplication by one leaves the squared score unchanged, so both integral expressions coincide.

Full assumptions and notation

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. Open the shared-energy definition

The guarded value uses μ as the base measure and the constant multiplier one.

\[I_h(\mu\Vert\pi)=\int_E\operatorname{densityEnergy}(\mathbf 1,r)(x)\,d\mu(x).\]
Corresponding Lean step

information; RelativeFisher.information

2. Expand the pointwise energy

The density-energy definition is weight times squared gradient norm.

\[\operatorname{densityEnergy}(\mathbf 1,r)(x)=1\cdot\|\nabla r(x)\|^2.\]
Corresponding Lean step

RelativeFisher.densityEnergy

3. Remove the unit multiplier

Multiplication by one leaves the squared score unchanged, so both integral expressions coincide.

\[1\cdot\|\nabla r(x)\|^2=q(x),\qquad I_h(\mu\Vert\pi)=\int_Eq\,d\mu.\]
Corresponding Lean step

simp [information, RelativeFisher.information, RelativeFisher.densityEnergy, scoreSq]

Lean verification

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

Lean proof · information_eq_integral_scoreSq

Lean expands the two energy definitions and the squared-score name, then simplifies multiplication by one. It does not establish integrability during this proof: that fact was required in the supplied domain certificate.

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_integral_scoreSq
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h = ∫ x, scoreSq mu pi x ∂mu := by
  simp [information, RelativeFisher.information, RelativeFisher.densityEnergy, scoreSq]

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.
  • This theorem does not require σ-finiteness or a Lebesgue-decomposition instance because it only unfolds the μ-based definition.
  • No finiteness of KL divergence or entropy is asserted.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • one_mul

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.