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.

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