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

Read squared-score integrability from its certificate

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

Read this first

Mathematical statement

If h is a smooth finite score-domain witness for μ and π on finite-dimensional Euclidean space, then the squared gradient q of their selected log-ratio is integrable with respect to μ. This is exactly the integrability field already contained in h, not a consequence newly derived from absolute continuity or differentiability.

\[h:\mathcal D(\mu,\pi)\quad\Longrightarrow\quad q_{\mu,\pi}\in L^1(\mu).\]
Lean statement · scoreSq_integrable

The conclusion repeats one field of the domain certificate. Integrable means a.e. strong measurability together with a finite integral of the norm, not merely that a total real integral expression can be written.

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 scoreSq_integrable
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    Integrable (scoreSq mu pi) mu

Exact module and namespace context

Proof roadmap

  1. 1Extract the requested field

    The domain witness contains three proofs. Return its third proof, whose assertion is precisely the target integrability statement.

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. Extract the requested field

The domain witness contains three proofs. Return its third proof, whose assertion is precisely the target integrability statement.

\[h=(h_{\mathrm{ac}},h_{\mathrm{diff}},h_{L^1})\quad\Longrightarrow\quad h_{L^1}:q\in L^1(\mu).\]
Corresponding Lean step

h.scoreSq_integrable

Lean verification

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

Lean proof · scoreSq_integrable

The proof retrieves the certificate's stored integrability proof by its field name. No calculation or estimate is performed, and the other two fields do not by themselves imply this one.

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 scoreSq_integrable
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    Integrable (scoreSq mu pi) mu :=
  h.scoreSq_integrable

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 is a convenience wrapper for reusing an assumption. It must not be presented as a theorem producing a finite score domain from absolute continuity or differentiability.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Domain assumptions accessed

These are fields of the linked structure, not additional independently authored theorem leaves.

Mathlib API called (external library)

  • MeasureTheory.Integrable

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.