SPHMC actual smoothed-Gibbs q=2 initialization component

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. ASTIS expands the conditional q=2 moment and transport calculation.

Complete source statement (Samplinglib restatement)

Lemma 4.16 gives an all-q initialization bound for the actual smoothed Gibbs phase law. Its proof selects a minimizer, bounds its distance from the admissible reference point, applies Gibbs concentration and Gaussian smoothing, and couples the momenta identically. This ASTIS component proves the numerical q=2 squared-cost bound conditional on a supplied critical point; existence and all-q concentration remain open.

Gibbs and smoothing

Numerical q=2 bound

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

Numerical initialization cost for the actual smoothed Gibbs phase law

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialGibbsPhaseTransport.initial_gibbs_phase_transport_q2 · theorem · Teaching coverage

Read this first

Mathematical statement

For the normalized Gibbs law of U, smooth the position by an independent Gaussian of variance eta and adjoin independent standard-Gaussian momentum. The squared transport cost from the initial Dirac-position/Gaussian-momentum law to this actual phase reference is at most five times kappa times dimension.

\[W_{2,M_\kappa}^{2}(\delta_{x_{\rm ref}}\otimes\gamma,(\pi*\mathsf N(0,\eta I))\otimes\gamma)\le 5\kappa d,\qquad\kappa=1/\alpha.\]

Lean statement · initial_gibbs_phase_transport_q2

The Lean conclusion is a squared extended-nonnegative Kantorovich value, not yet a full q>=2 Wasserstein bound. A supplied critical point is a proof-interface assumption that still needs an existence theorem for source-level closure.

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 initial_gibbs_phase_transport_q2
    {U : E → ℝ} {α η : ℝ≥0} (hα : 0 < α) (hαone : α ≤ 1)
    (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
        fderiv ℝ (fderiv ℝ U) x v v ≤ ‖v‖ ^ 2)
    (p xref : E) (hp : gradient U p = 0)
    (href : ‖gradient U xref‖ ^ 2 ≤
      (α : ℝ) * (Module.finrank ℝ E : ℝ)) (hη : η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -U x)
    let πη := gaussianSmoothing μ (Real.sqrt η)
    PhaseMetric.phaseWassersteinSq (1 / (α : ℝ))
      ((Measure.dirac xref).prod (stdGaussian E))
      (πη.prod (stdGaussian E)) ≤
        ENNReal.ofReal (5 * (1 / (α : ℝ)) * (Module.finrank ℝ E : ℝ))

Exact module and namespace context

Proof roadmap

1Control the reference-point displacement
Strong convexity compares the gradient at xref with its zero value at p. Cauchy-Schwarz and the source's small-gradient condition then bound the distance to p.
2Integrate the Gibbs position moment
The already proved normalized Gibbs moment about p is finite and at most d/alpha. The squared triangle inequality makes the moment about xref integrable and bounds it by 4d/alpha.
3Add Gaussian smoothing
Independent centered Gaussian noise contributes exactly eta times dimension to the position second moment. This is an identity, not an unverified limit exchange.
4Couple the momenta identically
The initial and reference phase laws share standard-Gaussian momentum. The compiled coupling estimate bounds their squared M-kappa cost by the smoothed position moment; eta ≤ 1 ≤ kappa yields 5 kappa d.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional complete real inner-product Borel space.
The genuine C2 Hessian of U lies between alpha I and I, with 0 < alpha ≤ 1 and kappa = 1/alpha.
A point p satisfies gradient U(p) = 0; xref satisfies squared gradient norm at most alpha times dimension.
The Gaussian smoothing variance eta lies in [0,1].

Mathematical proof

1. Control the reference-point displacement

Strong convexity compares the gradient at xref with its zero value at p. Cauchy-Schwarz and the source's small-gradient condition then bound the distance to p.

\[\alpha\|x_{\rm ref}-p\|^2\le\langle\nabla U(x_{\rm ref}),x_{\rm ref}-p\rangle\le\|\nabla U(x_{\rm ref})\|\,\|x_{\rm ref}-p\|,\quad\|x_{\rm ref}-p\|^2\le d/\alpha.\]

Corresponding Lean step

HessianStrongConvexity and StrongConvexFirstOrder supply genuine strong monotonicity; positivity permits cancellation.

2. Integrate the Gibbs position moment

The already proved normalized Gibbs moment about p is finite and at most d/alpha. The squared triangle inequality makes the moment about xref integrable and bounds it by 4d/alpha.

\[\mathbb E_\pi\|X-x_{\rm ref}\|^2\le 2\mathbb E_\pi\|X-p\|^2+2\|x_{\rm ref}-p\|^2\le4d/\alpha.\]

Corresponding Lean step

GibbsPositionMoment.gibbs_position_moment provides the probability law, integrability and sharp center moment; integral_mono applies only after the shifted moment is shown integrable.

3. Add Gaussian smoothing

Independent centered Gaussian noise contributes exactly eta times dimension to the position second moment. This is an identity, not an unverified limit exchange.

\[\mathbb E\|X+\sqrt\eta G-x_{\rm ref}\|^2=\mathbb E\|X-x_{\rm ref}\|^2+\eta d\le(4\kappa+\eta)d.\]

Corresponding Lean step

PhaseReferenceMoment.gaussianSmoothing_position_second_moment proves product measurability, cross-term cancellation and integrability.

4. Couple the momenta identically

The initial and reference phase laws share standard-Gaussian momentum. The compiled coupling estimate bounds their squared M-kappa cost by the smoothed position moment; eta ≤ 1 ≤ kappa yields 5 kappa d.

\[W_{2,M_\kappa}^{2}(\mu_0,\Pi_\eta)\le(4\kappa+\eta)d\le5\kappa d.\]

Corresponding Lean step

InitialPhaseTransport.phaseWassersteinSq_initial_le_position_moment supplies the actual coupling and its cost.

Lean verification

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

Lean proof · initial_gibbs_phase_transport_q2

The proof reuses three compiled mathematical parents, derives the reference distance from the genuine Hessian bound, proves shifted-square integrability before monotone integration, and specializes the smoothing scale to sqrt eta.

Download module (.lean)

theorem initial_gibbs_phase_transport_q2
    {U : E → ℝ} {α η : ℝ≥0} (hα : 0 < α) (hαone : α ≤ 1)
    (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
        fderiv ℝ (fderiv ℝ U) x v v ≤ ‖v‖ ^ 2)
    (p xref : E) (hp : gradient U p = 0)
    (href : ‖gradient U xref‖ ^ 2 ≤
      (α : ℝ) * (Module.finrank ℝ E : ℝ)) (hη : η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -U x)
    let πη := gaussianSmoothing μ (Real.sqrt η)
    PhaseMetric.phaseWassersteinSq (1 / (α : ℝ))
      ((Measure.dirac xref).prod (stdGaussian E))
      (πη.prod (stdGaussian E)) ≤
        ENNReal.ofReal (5 * (1 / (α : ℝ)) * (Module.finrank ℝ E : ℝ)) := by
  classical
  let μ := (volume : Measure E).tilted (fun x => -U x)
  let πη := gaussianSmoothing μ (Real.sqrt η)
  have ha : (0 : ℝ) < α := hα
  have haone : (α : ℝ) ≤ 1 := hαone
  have hκ : (1 : ℝ) ≤ 1 / (α : ℝ) := (one_le_div ha).2 haone
  have hdim : (0 : ℝ) ≤ Module.finrank ℝ E := by exact_mod_cast Nat.zero_le _
  have hdata := GibbsPositionMoment.gibbs_position_moment
    (β := 1) hα hαone hU
      (fun x v => ⟨(hH x v).1, by simpa using (hH x v).2⟩) p hp
  obtain ⟨hprob, _, _, hpos, _, _, hposBound⟩ := hdata
  change Integrable (fun x : E => ‖x - p‖ ^ 2) μ at hpos
  change (∫ x : E, ‖x - p‖ ^ 2 ∂μ) ≤
    (Module.finrank ℝ E : ℝ) / (α : ℝ) at hposBound
  letI : IsProbabilityMeasure μ := hprob
  have hsc : StrongConvexOn (Set.univ : Set E) (α : ℝ) U :=
    HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower hU
      (fun x v => (hH x v).1)
  have hd : Differentiable ℝ U := hU.differentiable (by norm_num)
  have hmono : (α : ℝ) * ‖xref - p‖ ^ 2 ≤
      inner ℝ (gradient U xref) (xref - p) := by
    simpa only [hp, sub_zero] using
      (StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn
        hsc (fun z _ => (hd z).hasGradientAt)
        (x := p) (y := xref) (Set.mem_univ _) (Set.mem_univ _))
  have hr : (α : ℝ) * ‖xref - p‖ ≤ ‖gradient U xref‖ := by
    by_cases hz : ‖xref - p‖ = 0
    · simp [hz]
    · have hposr : 0 < ‖xref - p‖ :=
        lt_of_le_of_ne (norm_nonneg _) (Ne.symm hz)
      have hi := (hmono.trans (real_inner_le_norm (gradient U xref) (xref - p)))
      have hm : ((α : ℝ) * ‖xref - p‖) * ‖xref - p‖ ≤
          ‖gradient U xref‖ * ‖xref - p‖ := by nlinarith [hi]
      exact le_of_mul_le_mul_right hm hposr
  have hsq : ((α : ℝ) * ‖xref - p‖) ^ 2 ≤
      ‖gradient U xref‖ ^ 2 :=
    (sq_le_sq₀ (by positivity) (norm_nonneg _)).2 hr
  have hrefDist : ‖xref - p‖ ^ 2 ≤
      (Module.finrank ℝ E : ℝ) / (α : ℝ) := by
    apply (le_div_iff₀ ha).2
    have hm : (α : ℝ) * ((α : ℝ) * ‖xref - p‖ ^ 2) ≤
        (α : ℝ) * (Module.finrank ℝ E : ℝ) := by nlinarith [hsq, href]
    exact le_of_mul_le_mul_left (by nlinarith [hm]) ha
  have hpoint (x : E) : ‖xref - x‖ ^ 2 ≤
      2 * ‖x - p‖ ^ 2 + 2 * ‖xref - p‖ ^ 2 := by
    have ht : ‖xref - x‖ ≤ ‖xref - p‖ + ‖x - p‖ := by
      calc
        ‖xref - x‖ = ‖(xref - p) + (p - x)‖ := by congr 1; abel
        _ ≤ ‖xref - p‖ + ‖p - x‖ := norm_add_le _ _
        _ = _ := by rw [norm_sub_rev p x]
    have htsq : ‖xref - x‖ ^ 2 ≤ (‖xref - p‖ + ‖x - p‖) ^ 2 :=
      (sq_le_sq₀ (norm_nonneg _) (by positivity)).2 ht
    nlinarith [sq_nonneg (‖xref - p‖ - ‖x - p‖)]
  have hsum : Integrable
      (fun x : E => 2 * ‖x - p‖ ^ 2 + 2 * ‖xref - p‖ ^ 2) μ :=
    (hpos.const_mul 2).add (integrable_const _)
  have hrefI : Integrable (fun x : E => ‖xref - x‖ ^ 2) μ := by
    apply hsum.mono' (by fun_prop)
    filter_upwards with x
    simpa only [Real.norm_eq_abs,
      abs_of_nonneg (sq_nonneg (‖xref - x‖))] using hpoint x
  have hbase : (∫ x : E, ‖xref - x‖ ^ 2 ∂μ) ≤
      4 * ((Module.finrank ℝ E : ℝ) / (α : ℝ)) := by
    have hi := integral_mono hrefI hsum hpoint
    have hs : (∫ x : E,
        2 * ‖x - p‖ ^ 2 + 2 * ‖xref - p‖ ^ 2 ∂μ) =
        2 * (∫ x : E, ‖x - p‖ ^ 2 ∂μ) + 2 * ‖xref - p‖ ^ 2 := by
      rw [integral_add (hpos.const_mul _) (integrable_const _),
        integral_const_mul, integral_const]
      simp
    rw [hs] at hi
    linarith
  have hbaseI : Integrable (fun x : E => ‖x - xref‖ ^ 2) μ := by
    simpa only [norm_sub_rev] using hrefI
  have hsm := PhaseReferenceMoment.gaussianSmoothing_position_second_moment
    μ xref (Real.sqrt η) hbaseI
  change Integrable (fun y : E => ‖y - xref‖ ^ 2) πη ∧
    (∫ y : E, ‖y - xref‖ ^ 2 ∂πη) =
      (∫ x : E, ‖x - xref‖ ^ 2 ∂μ) +
        (Real.sqrt η) ^ 2 * (Module.finrank ℝ E : ℝ) at hsm
  letI : IsProbabilityMeasure πη := by
    dsimp [πη, gaussianSmoothing,
      AutoSamplingTheory.TechnicalLemmas.Measure.CommonNoiseContraction.addNoise]
    exact Measure.isProbabilityMeasure_map
      (by fun_prop : AEMeasurable (fun z : E × E => z.1 + z.2)
        (μ.prod (scaledStdGaussian (E := E) (Real.sqrt η))))
  have hcost := InitialPhaseTransport.phaseWassersteinSq_initial_le_position_moment
    πη xref hκ (by simpa only [norm_sub_rev] using hsm.1)
  have hnum : (∫ y : E, ‖xref - y‖ ^ 2 ∂πη) ≤
      5 * (1 / (α : ℝ)) * (Module.finrank ℝ E : ℝ) := by
    have hb : (∫ x : E, ‖x - xref‖ ^ 2 ∂μ) ≤
        4 * ((Module.finrank ℝ E : ℝ) / (α : ℝ)) := by
      simpa only [norm_sub_rev] using hbase
    have hetaκ : (η : ℝ) ≤ 1 / (α : ℝ) := le_trans hη hκ
    have hh := mul_nonneg (sub_nonneg.mpr hetaκ) hdim
    rw [show (∫ y : E, ‖xref - y‖ ^ 2 ∂πη) =
      (∫ y : E, ‖y - xref‖ ^ 2 ∂πη) by simp only [norm_sub_rev], hsm.2,
      Real.sq_sqrt (show (0 : ℝ) ≤ η by exact_mod_cast η.property)]
    rw [div_eq_mul_one_div] at hb
    nlinarith [hb, hh]
  exact hcost.trans (ENNReal.ofReal_le_ofReal hnum)

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialGibbsPhaseTransport

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The proof of Lemma 4.16 selects a minimizer of U without adding it to the theorem hypotheses.	A point p with gradient U p = 0 is supplied explicitly.	API-limitation	The Gibbs moment parent requires a stationary-point witness. Existence under the source assumptions must be formalized separately; this declaration is not source-equivalent to the unconditional lemma.
The source concludes for every q>=2.	Only a squared M_kappa Kantorovich bound at q=2 is proved.	source-implicit	This is a scoped proof component, not the full source conclusion.
The source works in R^d and positive smoothing variance.	Any finite-dimensional real inner-product Borel space and eta>=0 are allowed.	generalization	The identities and the zero-noise case remain valid without changing the source constant.

Only the conditional numerical q=2 initialization component; no critical-point existence, all-q source lemma, history, output accuracy or query cost.

Encoder–denoiser: source-reviewed · lean-strengthened-assumptions

Detected semantic differences

assumptions: Lean supplies a critical point p; the source lemma selects a minimizer internally. — Independent source reviewer confirmed this is a stronger proof-interface premise, retained visibly until an existence theorem is formalized.
quantifiers: Lean proves only the q=2 component, not all q>=2. — The source reviewer compared the actual paper Lemma 4.16 and accepted this declaration only as a scoped proof-edge.
constant_dependencies: The factor 5 is an ASTIS-derived explicit q=2 constant, not printed in the paper. — The reviewed moment chain gives 4 kappa d + eta d <= 5 kappa d.

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 is a conditional q=2 component of SPHMC Lemma 4.16. The critical point p used in the source proof is supplied; its existence, all-q concentration, Picard dynamics and the main algorithmic result are not proved here.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Measure.isProbabilityMeasure_map
Integrable.mono'
integral_mono
ENNReal.ofReal_le_ofReal
Real.sq_sqrt

Mathematical sources

Smoothed Picard Hamiltonian Monte Carlo, Lemma 4.16, PDF p.22 — ASTIS expands the numerical second-moment calculation and keeps the critical-point witness explicit.

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

SPHMC actual smoothed-Gibbs q=2 initialization component

Complete source statement (Samplinglib restatement)

Gibbs and smoothing

Numerical q=2 bound

Read the formalized proofs

Numerical initialization cost for the actual smoothed Gibbs phase law

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Control the reference-point displacement

2. Integrate the Gibbs position moment

3. Add Gaussian smoothing

4. Couple the momenta identically

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?