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

Exact Fisher energy of the restricted-Gaussian fiber score

Yin Tat Lee, Ruoqi Shen and Kevin Tian; used by Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. ASTIS isolates the explicit-representative integration step; no author endorsement implied.

arXiv:2010.03106v4 · Lemma 2 proof, the Fisher-information display immediately before equation (11); used by SPHMC arXiv:2609.06906v1 Lemma 4.17 · faithful paraphrase

Complete source statement (Samplinglib restatement)

Under the left restricted-Gaussian probability fiber, the explicit normalized quadratic log-ratio representative has constant score eta^{-1}(y-y'), so its relative Fisher energy is exactly eta^{-2} times the squared center displacement. This is one input to the cited LSI/Talagrand route, not the resulting Wasserstein contraction.

  • The common normalization base and the probability law used for the expectation are separate measures; the source expectation law is the left tilt of the common base.
  • The paper has eta>0; the algebraic integration theorem needs only eta nonzero.
  • The smooth displayed representative is used. Almost-everywhere agreement with a canonical llr does not transfer classical differentiability.

exact score energy

\[\mathcal I_{R_{\eta,y}}(r_{y,y'})=\int\|\nabla r_{y,y'}(x)\|^2\,dR_{\eta,y}(x)=\eta^{-2}\|y-y'\|^2\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

The quadratic fiber score has exact relative Fisher energy

AutoSamplingTheory.TechnicalLemmas.InformationTheory.QuadraticTiltFisher.information_quadratic_representative · theorem · Teaching coverage

Read this first

Mathematical statement

Let ν be the common measure used in the two quadratic normalizers and let μ be any probability law on a finite-dimensional Euclidean space. For η≠0 and centers y,y′, the μ-relative Fisher energy of this explicit normalized quadratic log-ratio representative is exactly η⁻²‖y−y′‖². In the source specialization, ν is the common Gibbs base and μ is its left restricted-Gaussian fiber.

\[\mathcal I_{\mu}(r_{y,y'})=\int\!\|\nabla r_{y,y'}(x)\|^2\,d\mu(x)=\eta^{-2}\|y-y'\|^2.\]
Lean statement · information_quadratic_representative

The function supplied to RelativeFisher.information contains both ν-normalizers explicitly, while the Fisher integral is taken under the separate probability law μ. The normalizers disappear only through the previously proved genuine gradient theorem.

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_quadratic_representative
    (nu mu : Measure (State (ι := ι))) [IsProbabilityMeasure mu]
    {eta : ℝ} (heta : eta ≠ 0) (y y' : State (ι := ι)) :
    RelativeFisher.information mu (fun _ => 1)
        (fun t =>
          -(‖t - y‖ ^ 2 / (2 * eta)) -
            Real.log (∫ z, Real.exp (-(‖z - y‖ ^ 2 / (2 * eta))) ∂nu) -
          (-(‖t - y'‖ ^ 2 / (2 * eta))) +
            Real.log (∫ z, Real.exp (-(‖z - y'‖ ^ 2 / (2 * eta))) ∂nu)) =
      eta⁻¹ ^ 2 * ‖y - y'‖ ^ 2

Exact module and namespace context

Proof roadmap

  1. 1Insert the exact score

    The preceding ASTIS theorem differentiates the displayed quadratic representative genuinely and gives a vector independent of x.

  2. 2Expose the constant integrand

    Substituting the score in the definition of relative Fisher information leaves a spatially constant squared norm.

  3. 3Use probability mass one

    Because μ has total mass one, integrating this nonnegative constant does not introduce a mass factor.

  4. 4Pull the scalar out of the norm

    The norm of a real scalar multiple is its absolute value times the norm. Squaring removes the sign and gives the exact η⁻² coefficient.

Full assumptions and notation

All objects and hypotheses

  • The common normalization measure ν and the probability integration law μ are separate parameters. In the source, μ is the left tilt of ν.
  • The integration law μ is a probability measure; this is what turns the integral of a constant into the same constant.
  • The state space is a finite-dimensional Euclidean space and η is nonzero. The paper's fiber variance satisfies η>0.
  • The argument evaluates the displayed smooth log-ratio representative. It does not differentiate Mathlib's canonical measurable llr representative.

Mathematical proof

1. Insert the exact score

The preceding ASTIS theorem differentiates the displayed quadratic representative genuinely and gives a vector independent of x.

\[\nabla r_{y,y'}(x)=\eta^{-1}(y-y').\]
Corresponding Lean step

TiltedLogRatio.gradient_quadratic_representative

2. Expose the constant integrand

Substituting the score in the definition of relative Fisher information leaves a spatially constant squared norm.

\[\mathcal I_{\mu}(r_{y,y'})=\int\!\|\eta^{-1}(y-y')\|^2\,d\mu(x).\]
Corresponding Lean step

RelativeFisher.information; RelativeFisher.densityEnergy

3. Use probability mass one

Because μ has total mass one, integrating this nonnegative constant does not introduce a mass factor.

\[\int c\,d\mu=c\,\mu(\mathbb R^d)=c.\]
Corresponding Lean step

IsProbabilityMeasure μ; MeasureTheory.integral_const

4. Pull the scalar out of the norm

The norm of a real scalar multiple is its absolute value times the norm. Squaring removes the sign and gives the exact η⁻² coefficient.

\[\|\eta^{-1}(y-y')\|^2=|\eta^{-1}|^2\|y-y'\|^2=\eta^{-2}\|y-y'\|^2.\]
Corresponding Lean step

norm_smul; Real.norm_eq_abs; mul_pow

Lean verification

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

Lean proof · information_quadratic_representative

The proof unfolds the ASTIS relative-Fisher definitions, rewrites every pointwise gradient with the compiled quadratic-score theorem, and lets Mathlib evaluate the constant integral under the probability instance and normalize the scalar norm square.

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_quadratic_representative
    (nu mu : Measure (State (ι := ι))) [IsProbabilityMeasure mu]
    {eta : ℝ} (heta : eta ≠ 0) (y y' : State (ι := ι)) :
    RelativeFisher.information mu (fun _ => 1)
        (fun t =>
          -(‖t - y‖ ^ 2 / (2 * eta)) -
            Real.log (∫ z, Real.exp (-(‖z - y‖ ^ 2 / (2 * eta))) ∂nu) -
          (-(‖t - y'‖ ^ 2 / (2 * eta))) +
            Real.log (∫ z, Real.exp (-(‖z - y'‖ ^ 2 / (2 * eta))) ∂nu)) =
      eta⁻¹ ^ 2 * ‖y - y'‖ ^ 2 := by
  rw [RelativeFisher.information]
  simp_rw [RelativeFisher.densityEnergy, one_mul,
    TiltedLogRatio.gradient_quadratic_representative nu heta y y']
  simp [norm_smul, Real.norm_eq_abs, mul_pow]

end

end QuadraticTiltFisher
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
The expectation is under the normalized left restricted-Gaussian fiber with eta>0.Any common normalization measure nu, any separate probability integration law mu on finite-dimensional Euclidean space, and eta!=0.generalizationAfter the exact score has been proved, only probability mass one and nonzero eta enter the integration step. Separating nu from mu permits the actual source specialization; constructing mu as the normalized left fiber remains a separate adapter.
The paper writes Fisher information of the displayed density ratio.RelativeFisher.information is evaluated on that explicit smooth representative, not on an arbitrary canonical measurable llr.mathematically-necessaryAlmost-everywhere equality of function values does not determine a classical gradient after null-set changes.
The Fisher value is inserted into LSI and Talagrand inequalities to obtain a W2 estimate.Only the exact Fisher value is concluded.unresolvedThe strong-convex Gibbs LSI/T2 backend and its actual fiber specialization are independent red obligations.

Exact probability integral of the explicit constant score only. Canonical-score domains, LSI, T2, W2 and kernel contraction remain open.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • quantifiers: Lean quantifies over any probability integration law mu independent of the common normalizer base nu. The cited left-fiber case is a direct specialization, and the proof genuinely needs only total mass one after the constant-score rewrite. — Independent source review classification: faithful-generalization; nonblocking.
  • assumptions: Lean weakens the paper assumption eta > 0 to eta != 0. The gradient and squared-energy identity are algebraically valid on this larger domain, while the source specialization remains available. — Independent source review classification: faithful-generalization; nonblocking.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries
  • This theorem does not identify the Fisher information of an arbitrary canonical llr representative.
  • It does not prove a log-Sobolev inequality, Talagrand inequality, Wasserstein contraction, Markov-kernel contraction, or any SPHMC main theorem.
  • The left law is assumed to be a probability measure and is kept distinct from the common normalization base. Construction and normalization of the actual restricted-Gaussian fiber remain separate adapters.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • MeasureTheory.IsProbabilityMeasure
  • MeasureTheory.integral_const
  • norm_smul
  • Real.norm_eq_abs

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.

Which proof obligations and prerequisites are covered?

  • TODO — not closed by these contributions Evaluate the relative Fisher functional of the explicit quadratic log-ratio representative