Samplinglib mathematical lesson

The restricted-Gaussian relative score is constant

AutoSamplingTheory.TechnicalLemmas.InformationTheory.TiltedLogRatio.gradient_quadratic_representative · theorem · Teaching coverage

Read this first

Mathematical statement

For η≠0, the explicit normalized log-ratio representative of the quadratic fiber centered at y against the one centered at y′ has the constant gradient η⁻¹(y−y′). The paper consumer specializes to η>0.

\[\nabla_x\!\left[-\frac{\|x-y\|^2}{2\eta}-\log Z_y+\frac{\|x-y'\|^2}{2\eta}+\log Z_{y'}\right]=\eta^{-1}(y-y').\]

Lean statement · gradient_quadratic_representative

The base measure is arbitrary because only the x-independence of its two normalizers is used. No normalization or integrability premise is smuggled into this calculus 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 gradient_quadratic_representative
    (mu : Measure E) {eta : ℝ} (heta : eta ≠ 0) (y y' x : E) :
    gradient
        (fun t =>
          -(‖t - y‖ ^ 2 / (2 * eta)) -
            Real.log (∫ z, Real.exp (-(‖z - y‖ ^ 2 / (2 * eta))) ∂mu) -
          (-(‖t - y'‖ ^ 2 / (2 * eta))) +
            Real.log (∫ z, Real.exp (-(‖z - y'‖ ^ 2 / (2 * eta))) ∂mu)) x =
      eta⁻¹ • (y - y')

Exact module and namespace context

Proof roadmap

1Differentiate the two quadratics
The genuine Fréchet gradients are −η⁻¹(x−y) and −η⁻¹(x−y′).
2Discard only spatial constants
The two log normalizers may depend on μ, η and the centers, but not on x, so their derivatives vanish.
3Cancel x
Subtracting the two quadratic scores cancels x and leaves the center displacement with the source sign.

Full assumptions and notation

All objects and hypotheses

E is a complete real inner-product space.
η is nonzero; SPHMC and the cited restricted-Gaussian theorem use η>0.
The differentiated function is displayed explicitly and is not Mathlib's arbitrary canonical measurable llr representative.

Mathematical proof

1. Differentiate the two quadratics

The genuine Fréchet gradients are −η⁻¹(x−y) and −η⁻¹(x−y′).

\[\nabla q_{\eta,y}(x)=-\eta^{-1}(x-y).\]

Corresponding Lean step

HasFDerivAt.norm_sq; InnerProductSpace.toDual

2. Discard only spatial constants

The two log normalizers may depend on μ, η and the centers, but not on x, so their derivatives vanish.

\[\nabla_x\log Z_y=\nabla_x\log Z_{y'}=0.\]

Corresponding Lean step

HasFDerivAt.sub_const; HasFDerivAt.add_const

3. Cancel x

Subtracting the two quadratic scores cancels x and leaves the center displacement with the source sign.

\[-\eta^{-1}(x-y)+\eta^{-1}(x-y')=\eta^{-1}(y-y').\]

Corresponding Lean step

module; map_sub

Lean verification

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

Lean proof · gradient_quadratic_representative

A private helper derives the genuine gradient of each quadratic from the norm-square derivative and the Hilbert duality map. The public proof removes constant normalizers and performs the linear cancellation.

Download module (.lean)

theorem gradient_quadratic_representative
    (mu : Measure E) {eta : ℝ} (heta : eta ≠ 0) (y y' x : E) :
    gradient
        (fun t =>
          -(‖t - y‖ ^ 2 / (2 * eta)) -
            Real.log (∫ z, Real.exp (-(‖z - y‖ ^ 2 / (2 * eta))) ∂mu) -
          (-(‖t - y'‖ ^ 2 / (2 * eta))) +
            Real.log (∫ z, Real.exp (-(‖z - y'‖ ^ 2 / (2 * eta))) ∂mu)) x =
      eta⁻¹ • (y - y') := by
  have hy := hasGradientAt_quadraticExponent heta y x
  have hy' := hasGradientAt_quadraticExponent heta y' x
  apply HasGradientAt.gradient
  rw [hasGradientAt_iff_hasFDerivAt]
  change HasFDerivAt
    (fun t => quadraticExponent eta y t -
      Real.log (∫ z, Real.exp (quadraticExponent eta y z) ∂mu) -
      quadraticExponent eta y' t +
      Real.log (∫ z, Real.exp (quadraticExponent eta y' z) ∂mu))
    (InnerProductSpace.toDual ℝ E (eta⁻¹ • (y - y'))) x
  let c := Real.log (∫ z, Real.exp (quadraticExponent eta y z) ∂mu)
  let c' := Real.log (∫ z, Real.exp (quadraticExponent eta y' z) ∂mu)
  have hderiv : HasFDerivAt
      (fun t => quadraticExponent eta y t - c - quadraticExponent eta y' t + c')
      ((InnerProductSpace.toDual ℝ E (-eta⁻¹ • (x - y))) -
        InnerProductSpace.toDual ℝ E (-eta⁻¹ • (x - y'))) x :=
    ((hy.hasFDerivAt.sub_const c).sub hy'.hasFDerivAt).add_const c'
  have hvec :
      (-eta⁻¹ • (x - y)) - (-eta⁻¹ • (x - y')) =
        eta⁻¹ • (y - y') := by
    module
  rw [← hvec, map_sub]
  simpa only [c, c'] using hderiv

end Quadratic

end

end TiltedLogRatio
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

The theorem does not differentiate the canonical measurable llr.
A representative-to-canonical-Fisher adapter, the strong-convex Gibbs LSI/T₂ backend and the W₂ contraction all remain separate red nodes.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

HasFDerivAt.norm_sq
InnerProductSpace.toDual
HasGradientAt.gradient

Mathematical sources

Lee–Shen–Tian equation (11) — Exact sign and η⁻¹ coefficient; this equation is cited in the route used by SPHMC Lemma 4.17.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.