SPHMC stationary phase-reference moments

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. ASTIS supplies the omitted independent-Gaussian and product-integral details.

arXiv:2609.06906v1 · Section 3.1 definition of pi_eta and Pi_eta; Lemma D.4 proof after equation (D.3) · faithful paraphrase

Complete source statement (Samplinglib restatement)

For pi_eta=pi*N(0,eta I) and Pi_eta=pi_eta tensor N(0,I), the stationary reference law has explicit finite position and momentum second moments; ASTIS proves the generic standard-deviation-scale identity used by this specialization.

Finite-dimensional real inner-product Borel space.
A probability base law with an integrable, bounded position second moment.
Use sigma=sqrt eta to recover the paper's variance parameter eta.

Smoothed position

\[\mathbb E\|X+\sigma Z-x_\star\|^2=\mathbb E\|X-x_\star\|^2+\sigma^2d.\]

Phase reference

\[\Pi_\sigma=(\mu*\mathsf N(0,\sigma^2I))\otimes\mathsf N(0,I).\]

Combined phase moment

\[\mathbb E_{\Pi_\sigma}[\|X-x_\star\|^2+\|P\|^2]\le M+(\sigma^2+1)d.\]

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

Gaussian smoothing adds exactly one noise second moment

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseReferenceMoment.gaussianSmoothing_position_second_moment · theorem · Teaching coverage

Read this first

Mathematical statement

Convolving a probability law with an independent centered isotropic Gaussian of scale sigma increases its second moment about xstar by exactly sigma squared times the dimension.

\[\int\|y-x_\star\|^2\,d(\mu*\mathsf N(0,\sigma^2I))(y)=\int\|x-x_\star\|^2\,d\mu(x)+\sigma^2d.\]

Lean statement · gaussianSmoothing_position_second_moment

The theorem is generic in mu and permits every real sigma; covariance depends on sigma squared.

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 gaussianSmoothing_position_second_moment
    (mu : Measure E) [IsProbabilityMeasure mu] (xstar : E) (sigma : ℝ)
    (hpos : Integrable (fun x : E => ‖x - xstar‖ ^ 2) mu) :
    let piSigma := gaussianSmoothing mu sigma
    Integrable (fun y : E => ‖y - xstar‖ ^ 2) piSigma ∧
      (∫ y : E, ‖y - xstar‖ ^ 2 ∂piSigma) =
        (∫ x : E, ‖x - xstar‖ ^ 2 ∂mu) +
          sigma ^ 2 * (Module.finrank ℝ E : ℝ)

Exact module and namespace context

Proof roadmap

1Expose the independent product
Gaussian smoothing is the pushforward of an independent pair (X,Z) under X+sigma Z.
2Expand the square
Separate the old position energy, the centered cross term, and the Gaussian energy.
3Justify and cancel the cross term
The two L2 assumptions imply integrability of the product inner product; independence and E Z=0 then make its integral zero.
4Insert the Gaussian trace
The coordinate-free standard-Gaussian second moment is the real dimension.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional complete real inner-product Borel space.
mu is a probability measure.
The squared distance to xstar is mu-integrable.
sigma is the Gaussian standard-deviation scale; the paper later uses sigma=sqrt(eta).

Mathematical proof

1. Expose the independent product

Gaussian smoothing is the pushforward of an independent pair (X,Z) under X+sigma Z.

\[\mu*\mathsf N(0,\sigma^2I)=(\mu\otimes\gamma)_\#[(x,z)\mapsto x+\sigma z].\]

Corresponding Lean step

gaussianSmoothing, scaledStdGaussian, Measure.map_prod_map and Measure.map_map.

2. Expand the square

Separate the old position energy, the centered cross term, and the Gaussian energy.

\[\|X+\sigma Z-x_\star\|^2=\|X-x_\star\|^2+2\sigma\langle X-x_\star,Z\rangle+\sigma^2\|Z\|^2.\]

Corresponding Lean step

norm_add_sq_real after an explicit subtraction identity.

3. Justify and cancel the cross term

The two L2 assumptions imply integrability of the product inner product; independence and E Z=0 then make its integral zero.

\[\mathbb E\langle X-x_\star,Z\rangle=\mathbb E\langle X-x_\star,\mathbb EZ\rangle=0.\]

Corresponding Lean step

MemLp.integrable, Integrable.op_fst_snd, integral_prod and integral_strongDual_stdGaussian.

4. Insert the Gaussian trace

The coordinate-free standard-Gaussian second moment is the real dimension.

\[\mathbb E\|Z\|^2=d.\]

Corresponding Lean step

StdGaussianMoment.integrable_norm_sq_and_integral_stdGaussian.

Lean verification

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

Lean proof · gaussianSmoothing_position_second_moment

Pushforward integration, an integrable square expansion, Gaussian centering, and the standard-Gaussian trace identity.

Download module (.lean)

theorem gaussianSmoothing_position_second_moment
    (mu : Measure E) [IsProbabilityMeasure mu] (xstar : E) (sigma : ℝ)
    (hpos : Integrable (fun x : E => ‖x - xstar‖ ^ 2) mu) :
    let piSigma := gaussianSmoothing mu sigma
    Integrable (fun y : E => ‖y - xstar‖ ^ 2) piSigma ∧
      (∫ y : E, ‖y - xstar‖ ^ 2 ∂piSigma) =
        (∫ x : E, ‖x - xstar‖ ^ 2 ∂mu) +
          sigma ^ 2 * (Module.finrank ℝ E : ℝ) := by
  classical
  let A : E × E → E := fun w => w.1 + sigma • w.2
  let piSigma := gaussianSmoothing mu sigma
  have hA : Measurable A := by fun_prop
  have hprod :
      mu.prod (scaledStdGaussian (E := E) sigma) =
        (mu.prod (stdGaussian E)).map (Prod.map id (fun z : E => sigma • z)) := by
    simpa only [Measure.map_id, scaledStdGaussian] using
      Measure.map_prod_map mu (stdGaussian E) measurable_id
        (by fun_prop : Measurable (fun z : E => sigma • z))
  have hpiSigma : piSigma = (mu.prod (stdGaussian E)).map A := by
    dsimp [piSigma, gaussianSmoothing,
      AutoSamplingTheory.TechnicalLemmas.Measure.CommonNoiseContraction.addNoise]
    rw [hprod, Measure.map_map (by fun_prop) (by fun_prop)]
    rfl
  have hx1 : Integrable (fun x : E => x - xstar) mu :=
    MemLp.integrable (by norm_num : 1 ≤ (2 : ℝ≥0∞))
      ((memLp_two_iff_integrable_sq_norm (by fun_prop)).2 hpos)
  obtain ⟨hgauss, hgaussIntegral⟩ :=
    integrable_norm_sq_and_integral_stdGaussian (E := E)
  have hz1 : Integrable (fun z : E => z) (stdGaussian E) :=
    IsGaussian.integrable_id
  have hcross : Integrable
      (fun w : E × E => inner ℝ (w.1 - xstar) w.2)
      (mu.prod (stdGaussian E)) :=
    hx1.op_fst_snd (by fun_prop)
      ⟨1, by intro x y; simpa using norm_inner_le_norm (𝕜 := ℝ) x y⟩ hz1
  have hcross0 :
      (∫ w : E × E, inner ℝ (w.1 - xstar) w.2
          ∂mu.prod (stdGaussian E)) = 0 := by
    rw [integral_prod _ hcross]
    have hz (x : E) :
        (∫ z : E, inner ℝ (x - xstar) z ∂stdGaussian E) = 0 :=
      integral_strongDual_stdGaussian (innerSL ℝ (x - xstar))
    simp only [hz, integral_zero]
  have hposP := hpos.comp_fst (stdGaussian E)
  have hgaussP := hgauss.comp_snd mu
  have hcrossC : Integrable (fun w : E × E =>
      (2 * sigma) * inner ℝ (w.1 - xstar) w.2)
      (mu.prod (stdGaussian E)) := hcross.const_mul _
  have hbase : Integrable (fun w : E × E =>
      ‖w.1 - xstar‖ ^ 2 + (2 * sigma) * inner ℝ (w.1 - xstar) w.2)
      (mu.prod (stdGaussian E)) := hposP.add hcrossC
  have hnoise : Integrable (fun w : E × E => sigma ^ 2 * ‖w.2‖ ^ 2)
      (mu.prod (stdGaussian E)) := hgaussP.const_mul _
  have hpieces := hbase.add hnoise
  have hexpand (w : E × E) :
      ‖A w - xstar‖ ^ 2 =
        ‖w.1 - xstar‖ ^ 2 +
          (2 * sigma) * inner ℝ (w.1 - xstar) w.2 +
          sigma ^ 2 * ‖w.2‖ ^ 2 := by
    have hsub : A w - xstar = (w.1 - xstar) + sigma • w.2 := by
      dsimp [A]
      abel
    rw [hsub, norm_add_sq_real, norm_smul, real_inner_smul_right]
    rw [Real.norm_eq_abs]
    simp only [mul_pow, sq_abs]
    ring
  have hmapI : Integrable (fun w : E × E => ‖A w - xstar‖ ^ 2)
      (mu.prod (stdGaussian E)) := by
    apply hpieces.congr
    filter_upwards with w
    simpa only [Pi.add_apply] using (hexpand w).symm
  have houtI : Integrable (fun y : E => ‖y - xstar‖ ^ 2) piSigma := by
    rw [hpiSigma]
    exact (integrable_map_measure (by fun_prop) hA.aemeasurable).2 hmapI
  refine ⟨houtI, ?_⟩
  change (∫ y : E, ‖y - xstar‖ ^ 2 ∂piSigma) = _
  rw [hpiSigma, integral_map hA.aemeasurable (by fun_prop)]
  simp_rw [hexpand]
  rw [integral_add hbase hnoise, integral_add hposP hcrossC,
    integral_const_mul, hcross0, mul_zero, add_zero, integral_const_mul,
    integral_prod _ hposP, integral_prod _ hgaussP]
  simp only [integral_const, hgaussIntegral, probReal_univ]
  ring

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The paper defines pi_eta using covariance eta I.	The theorem accepts every real standard-deviation scale sigma and produces covariance sigma^2 I.	generalization	The source is recovered by sigma=sqrt eta under eta>=0; sign is immaterial because the second moment depends on sigma squared.
The paper works with its strongly log-concave Gibbs target.	The identity holds for any probability law with the displayed finite position second moment.	generalization	No Gibbs structure is used in the independent-noise calculation.

Generic smoothing identity only; no phase dynamics.

Encoder–denoiser: source-reviewed · equivalent-after-elaboration

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

Exact position-moment identity only; no stationarity, Hamiltonian invariance, contraction or phase-history estimate.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Measure.map_prod_map
integral_prod
integral_strongDual_stdGaussian
memLp_two_iff_integrable_sq_norm

Mathematical sources

SPHMC Section 3.1 definition of pi_eta — ASTIS expands the independent-noise second-moment calculation suppressed by the paper.

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

Samplinglib mathematical lesson

The actual SPHMC product reference has controlled phase energy

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseReferenceMoment.phaseReference_second_moment · theorem · Teaching coverage

Read this first

Mathematical statement

The product of the smoothed position law and independent standard-Gaussian momentum is a probability law with exact coordinate moments and an explicit combined phase-energy bound.

\[\mathbb E_{\Pi_\sigma}[\|X-x_\star\|^2+\|P\|^2]\le M+(\sigma^2+1)d.\]

Lean statement · phaseReference_second_moment

The paper convention is obtained with sigma=sqrt eta and eta nonnegative; the theorem itself records the more general scale-squared identity.

Download module (.lean)

theorem phaseReference_second_moment
    (mu : Measure E) [IsProbabilityMeasure mu] (xstar : E) (sigma M : ℝ)
    (hpos : Integrable (fun x : E => ‖x - xstar‖ ^ 2) mu)
    (hposBound : (∫ x : E, ‖x - xstar‖ ^ 2 ∂mu) ≤ M) :
    let piSigma := gaussianSmoothing mu sigma
    let PiSigma := piSigma.prod (stdGaussian E)
    IsProbabilityMeasure PiSigma ∧
      Integrable (fun z : E × E => ‖z.1 - xstar‖ ^ 2) PiSigma ∧
      Integrable (fun z : E × E => ‖z.2‖ ^ 2) PiSigma ∧
      (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 ∂PiSigma) =
        (∫ x : E, ‖x - xstar‖ ^ 2 ∂mu) +
          sigma ^ 2 * (Module.finrank ℝ E : ℝ) ∧
      (∫ z : E × E, ‖z.2‖ ^ 2 ∂PiSigma) = Module.finrank ℝ E ∧
      Integrable
        (fun z : E × E => ‖z.1 - xstar‖ ^ 2 + ‖z.2‖ ^ 2) PiSigma ∧
      (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 + ‖z.2‖ ^ 2 ∂PiSigma) ≤
        M + (sigma ^ 2 + 1) * (Module.finrank ℝ E : ℝ)

Exact module and namespace context

Proof roadmap

1Construct the phase law
Use the actual product measure, not two unrelated marginal assumptions.
2Integrate the position coordinate
The second coordinate has total mass one, so the product integral is the smoothing identity.
3Integrate the momentum coordinate
The first marginal has total mass one and the momentum is standard Gaussian.
4Add the two energies
Product integrability legitimizes splitting the integral before applying the supplied base bound.

Full assumptions and notation

All objects and hypotheses

The hypotheses of the smoothing theorem.
The original position moment is bounded above by M.

Mathematical proof

1. Construct the phase law

Use the actual product measure, not two unrelated marginal assumptions.

\[\Pi_\sigma=(\mu*\mathsf N(0,\sigma^2I))\otimes\mathsf N(0,I).\]

Corresponding Lean step

piSigma.prod (stdGaussian E), with an explicit probability instance for the smoothing pushforward.

2. Integrate the position coordinate

The second coordinate has total mass one, so the product integral is the smoothing identity.

\[\mathbb E_{\Pi_\sigma}\|X-x_\star\|^2=\mathbb E_\mu\|X-x_\star\|^2+\sigma^2d.\]

Corresponding Lean step

Integrable.comp_fst, integral_prod and probReal_univ.

3. Integrate the momentum coordinate

The first marginal has total mass one and the momentum is standard Gaussian.

\[\mathbb E_{\Pi_\sigma}\|P\|^2=d.\]

Corresponding Lean step

Integrable.comp_snd and the standard-Gaussian moment theorem.

4. Add the two energies

Product integrability legitimizes splitting the integral before applying the supplied base bound.

\[(M+\sigma^2d)+d=M+(\sigma^2+1)d.\]

Corresponding Lean step

integral_add followed by linarith.

Lean verification

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

Lean proof · phaseReference_second_moment

Product probability, coordinate integrability, exact Fubini identities, then addition of the supplied base moment bound.

Download module (.lean)

theorem phaseReference_second_moment
    (mu : Measure E) [IsProbabilityMeasure mu] (xstar : E) (sigma M : ℝ)
    (hpos : Integrable (fun x : E => ‖x - xstar‖ ^ 2) mu)
    (hposBound : (∫ x : E, ‖x - xstar‖ ^ 2 ∂mu) ≤ M) :
    let piSigma := gaussianSmoothing mu sigma
    let PiSigma := piSigma.prod (stdGaussian E)
    IsProbabilityMeasure PiSigma ∧
      Integrable (fun z : E × E => ‖z.1 - xstar‖ ^ 2) PiSigma ∧
      Integrable (fun z : E × E => ‖z.2‖ ^ 2) PiSigma ∧
      (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 ∂PiSigma) =
        (∫ x : E, ‖x - xstar‖ ^ 2 ∂mu) +
          sigma ^ 2 * (Module.finrank ℝ E : ℝ) ∧
      (∫ z : E × E, ‖z.2‖ ^ 2 ∂PiSigma) = Module.finrank ℝ E ∧
      Integrable
        (fun z : E × E => ‖z.1 - xstar‖ ^ 2 + ‖z.2‖ ^ 2) PiSigma ∧
      (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 + ‖z.2‖ ^ 2 ∂PiSigma) ≤
        M + (sigma ^ 2 + 1) * (Module.finrank ℝ E : ℝ) := by
  classical
  dsimp only
  let piSigma := gaussianSmoothing mu sigma
  have hposition :
      Integrable (fun y : E => ‖y - xstar‖ ^ 2) piSigma ∧
        (∫ y : E, ‖y - xstar‖ ^ 2 ∂piSigma) =
          (∫ x : E, ‖x - xstar‖ ^ 2 ∂mu) +
            sigma ^ 2 * (Module.finrank ℝ E : ℝ) := by
    simpa only [piSigma] using
      gaussianSmoothing_position_second_moment mu xstar sigma hpos
  obtain ⟨hgauss, hgaussIntegral⟩ :=
    integrable_norm_sq_and_integral_stdGaussian (E := E)
  letI : IsProbabilityMeasure piSigma := by
    dsimp [piSigma, gaussianSmoothing,
      AutoSamplingTheory.TechnicalLemmas.Measure.CommonNoiseContraction.addNoise]
    exact Measure.isProbabilityMeasure_map
      (by fun_prop : AEMeasurable (fun p : E × E => p.1 + p.2)
        (mu.prod (scaledStdGaussian (E := E) sigma)))
  have hX := hposition.1.comp_fst (stdGaussian E)
  have hP := hgauss.comp_snd piSigma
  have hXI :
      (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 ∂piSigma.prod (stdGaussian E)) =
        (∫ x : E, ‖x - xstar‖ ^ 2 ∂mu) +
          sigma ^ 2 * (Module.finrank ℝ E : ℝ) := by
    rw [integral_prod _ hX]
    simp only [integral_const, probReal_univ, one_smul, hposition.2]
  have hPI :
      (∫ z : E × E, ‖z.2‖ ^ 2 ∂piSigma.prod (stdGaussian E)) =
        Module.finrank ℝ E := by
    rw [integral_prod _ hP]
    simp only [hgaussIntegral, integral_const, probReal_univ, one_smul]
  refine ⟨inferInstance, hX, hP, hXI, hPI, hX.add hP, ?_⟩
  rw [integral_add hX hP, hXI, hPI]
  linarith

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseReferenceMoment

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The paper writes Pi_eta=pi_eta tensor N(0,I) and later uses its moments inside universal constants.	ASTIS constructs the actual product measure and states probability, coordinate integrability, exact coordinate integrals and the explicit combined bound.	source-implicit	These facts are required before the later transport-to-moment and Fubini steps are valid.
Strong convexity supplies the base Gibbs position moment.	This bounded packet takes the base moment M as an explicit premise.	source-implicit	The already compiled Gibbs moment is kept as a separate parent; its final specialization remains a visible integration edge.

Reference moments only; D.3, history, D.7 and D.8 remain open.

Encoder–denoiser: source-reviewed · equivalent-after-elaboration

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

Reference-law probability and second moments only; no numerical-kernel invariance, D.3, history supremum, D.7 or D.8.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Measure.prod
integral_prod
probReal_univ

Mathematical sources

SPHMC Pi_eta definition and Lemma D.4 use — Faithful prerequisite exposing the omitted product-law and integrability details.

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?

Independently verified prerequisite Exact independent-noise position moment
Formalized proof edge; source adapter/review separate Actual product phase-reference moments
TODO — not closed by these contributions Insert the compiled Gibbs moment and sigma=sqrt eta (remaining integration)
TODO — not closed by these contributions Equation (D.3) phase-history bound (remaining)
TODO — not closed by these contributions Actual query-center moments (remaining)
TODO — not closed by these contributions Total expected gradient work (remaining)