Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

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

  1. Numerical initialization cost for the actual smoothed Gibbs phase law
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

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

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

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

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

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 : ℝ)) := 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

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

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