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.