PhaseReferenceMoment: 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.

Gaussian smoothing adds exactly one noise second moment
The actual SPHMC product reference has controlled phase energy

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

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

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.