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

QuadraticTiltFisher: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. The quadratic fiber score has exact relative Fisher energy
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

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.