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

The actual implemented two-layer Picard phase kernel

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. Samplinglib supplies the explicit measurable kernel construction; deterministic quadrature data remain a separate adapter.

arXiv:2609.06906v1 · Algorithm 3.1 steps 1–4, HTML lines 282–306; Appendix D.1 (D.1), Algorithm D.2 and Lemma D.3, lines 2138–2164 · faithful paraphrase

Complete source statement (Samplinglib restatement)

Attributed implementation component of Algorithm 3.1 with Appendix D.1/D.2 approximate proximal queries, not a convergence theorem. Under the normalized C2 Hessian bounds and 0<eta<=c<1, eps>0, construct one measurable stopped proximal map q, its exact proximal comparison p, and its successful gradient-test count N+1. For h>=0 and supplied finite deterministic node and quadrature arrays, draw independent zeta0,zeta1,G0,G1 from the product of two standard Gaussian laws and two finite products of standard Gaussian laws. Set a=exp(-h/2), sigma=sqrt(1-exp(-h)), P0=a P+sigma zeta0, Y0_i=X+t_i P0, Z0_j=grad V(q(Y0_j)+sqrt(eta)G0_j), Y1_i=Y0_i-sum_j omega_ij Z0_j, Z1_j=grad V(q(Y1_j)+sqrt(eta)G1_j), Xnext=X+h P0-sum_j positionWeight_j Z1_j and Pnext=a(P0-sum_j momentumWeight_j Z1_j)+sigma zeta1. The joint update Phi is measurable and defines a Markov kernel K(s,.)=map(Phi(s,.),gamma); at every queried y the actual finite interpreter with fuel N(y)+1 returns (q(y),N(y)+1) and ||q(y)-p(y)||<=eps. Source node/weight construction and the repeated-run accuracy/cost theorems remain separate.

  • E is a complete finite-dimensional real inner-product space with its Borel sigma-algebra; the index type is finite.
  • V is C2, kappa >= 1 and kappa^(-1)||v||^2 <= D2V(x)[v,v] <= ||v||^2 for every x,v.
  • 0 < eta <= c < 1, eps > 0 and h >= 0.
  • t, omega, positionWeight and momentumWeight are supplied finite real arrays. Their source quadrature definitions and bounds are not conclusions of this interface.

Independent driving law

\[\gamma=(\gamma_E\otimes\gamma_E)\otimes(\gamma_E^{\otimes\iota}\otimes\gamma_E^{\otimes\iota}).\]

First refresh and layer

\[P_0=aP+\sigma\zeta_0,\quad Y_i^0=X+t_iP_0,\quad Z_j^0=\nabla V(q(Y_j^0)+\sqrt\eta G_j^0),\quad Y_i^1=Y_i^0-\sum_j\omega_{ij}Z_j^0.\]

Second layer and refresh

\[Z_j^1=\nabla V(q(Y_j^1)+\sqrt\eta G_j^1),\quad X^+=X+hP_0-\sum_j b_jZ_j^1,\quad P^+=a(P_0-\sum_j m_jZ_j^1)+\sigma\zeta_1.\]

Transition law

\[K(s,\cdot)=\Phi(s,\cdot)_\#\gamma,\qquad a=e^{-h/2},\quad\sigma=\sqrt{1-e^{-h}}.\]

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

The actual implemented two-layer Picard phase kernel

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseKernel.implemented_phase_kernel · theorem · Teaching coverage

Read this first

Mathematical statement

Attributed implementation component of Algorithm 3.1 with Appendix D.1/D.2 approximate proximal queries, not a convergence theorem. Under the normalized C2 Hessian bounds and 0<eta≤c<1, eps>0, construct one measurable stopped proximal map q, its exact proximal comparison p, and its successful gradient-test count N+1. For h≥0 and supplied finite deterministic node and quadrature arrays, draw independent zeta0,zeta1,G0,G1 from the product of two standard Gaussian laws and two finite products of standard Gaussian laws. Set a=exp(-h/2), sigma=sqrt(1-exp(-h)), P0=a P+sigma zeta0, Y0_i=X+t_i P0, Z0_j=grad V(q(Y0_j)+sqrt(eta)G0_j), Y1_i=Y0_i-sum_j omega_ij Z0_j, Z1_j=grad V(q(Y1_j)+sqrt(eta)G1_j), Xnext=X+h P0-sum_j positionWeight_j Z1_j and Pnext=a(P0-sum_j momentumWeight_j Z1_j)+sigma zeta1. The joint update Phi is measurable and defines a Markov kernel K(s,.)=map(Phi(s,.),gamma); at every queried y the actual finite interpreter with fuel N(y)+1 returns (q(y),N(y)+1) and ||q(y)-p(y)||≤eps. Source node/weight construction and the repeated-run accuracy/cost theorems remain separate.

\[K(s,\cdot)=\Phi(s,\cdot)_\#\gamma,\qquad a=e^{-h/2},\quad\sigma=\sqrt{1-e^{-h}}.\]
Lean statement · implemented_phase_kernel

The exact statement displays the independent Gaussian law and complete update map under lets; every proximal call shares the actual certified stopped map.

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 implemented_phase_kernel {V : E → ℝ} {κ : ℝ≥0}
    (hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E, (κ : ℝ)⁻¹ * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ ‖v‖ ^ 2)
    {eta c eps : ℝ} (heta : 0 < eta) (hec : eta ≤ c) (hc : c < 1) (heps : 0 < eps)
    (h : ℝ) (hh : 0 ≤ h) (t : ι → ℝ) (omega : ι → ι → ℝ)
    (positionWeight momentumWeight : ι → ℝ) :
    ∃ p q : E → E, ∃ N : E → ℕ,
      Measurable p ∧ Measurable q ∧ Measurable N ∧
      (∀ y, p y + eta • gradient V (p y) = y ∧ ‖q y - p y‖ ≤ eps ∧
        ApproximateProximalExecution.proximalQuery (gradient V) eta eps y (N y + 1) y =
          some (q y, N y + 1)) ∧
      let a := Real.exp (-h / 2)
      let sigma := Real.sqrt (1 - Real.exp (-h))
      let γ := ((stdGaussian E).prod (stdGaussian E)).prod
        ((Measure.pi (fun _ : ι => stdGaussian E)).prod
          (Measure.pi (fun _ : ι => stdGaussian E)))
      let Φ := fun w : (E × E) × ((E × E) × ((ι → E) × (ι → E))) =>
        let P0 := a • w.1.2 + sigma • w.2.1.1
        let Y0 := fun i => w.1.1 + t i • P0
        let Z0 := fun j => gradient V (q (Y0 j) + Real.sqrt eta • w.2.2.1 j)
        let Y1 := fun i => Y0 i - ∑ j, omega i j • Z0 j
        let Z1 := fun j => gradient V (q (Y1 j) + Real.sqrt eta • w.2.2.2 j)
        (w.1.1 + h • P0 - ∑ j, positionWeight j • Z1 j,
          a • (P0 - ∑ j, momentumWeight j • Z1 j) + sigma • w.2.1.2)
      0 ≤ 1 - Real.exp (-h) ∧
      Measurable Φ ∧ ∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
        ∀ s, K s = γ.map (fun z => Φ (s, z))

Exact module and namespace context

Proof roadmap

  1. 1Obtain one actual stopped proximal program

    The existing execution theorem constructs measurable p,N,q for the fixed potential and tolerance. It proves the optimality equation, eps accuracy, and the successful finite interpreter equation at every input. Both layers use this same q; no ideal or assumed oracle replaces it.

  2. 2Keep all Gaussian draws independent

    The two refresh coordinates have independent standard Gaussian laws. Two additional finite product factors supply independently fresh arrays G0 and G1, independent also of the incoming state in the kernel product. Product mass one follows from Mathlib probability instances.

  3. 3Construct the first refreshed trajectory and layer

    h≥0 makes the refresh variance nonnegative. Coordinate projections, finite sums, scalar multiplication and addition are measurable. C2 regularity makes grad V continuous, so the stopped q and each stochastic-gradient evaluation preserve measurability.

  4. 4Use the second fresh array and complete the phase

    The second gradient array evaluates q at the first updated centers, using G1 rather than reusing G0. Separate terminal position and momentum weights produce the second Picard outputs. The final refresh uses zeta1. No node or weight error estimate is assumed in this construction.

  5. 5Construct the canonical Markov kernel

    Combine the identity kernel at the incoming state with the constant probability kernel gamma, and map it by the jointly measurable Phi. At s this product is delta_s tensor gamma. The Dirac-product and composition-of-map identities give the stated pushforward exactly.

Full assumptions and notation

All objects and hypotheses

  • E is a complete finite-dimensional real inner-product space with its Borel sigma-algebra; the index type is finite.
  • V is C2, kappa ≥ 1 and kappa^(-1)||v||^2 ≤ D2V(x)[v,v] ≤ ||v||^2 for every x,v.
  • 0 < eta ≤ c < 1, eps > 0 and h ≥ 0.
  • t, omega, positionWeight and momentumWeight are supplied finite real arrays. Their source quadrature definitions and bounds are not conclusions of this interface.

Mathematical proof

1. Obtain one actual stopped proximal program

The existing execution theorem constructs measurable p,N,q for the fixed potential and tolerance. It proves the optimality equation, eps accuracy, and the successful finite interpreter equation at every input. Both layers use this same q; no ideal or assumed oracle replaces it.

\[p(y)+\eta\nabla V(p(y))=y,\quad\|q(y)-p(y)\|\le\varepsilon_{\rm prox},\quad\operatorname{run}(y,N(y)+1)=(q(y),N(y)+1).\]
Corresponding Lean step

approximate_proximal_execution supplies p,N and the measurable stopped iterate; hall supplies its certificate.

2. Keep all Gaussian draws independent

The two refresh coordinates have independent standard Gaussian laws. Two additional finite product factors supply independently fresh arrays G0 and G1, independent also of the incoming state in the kernel product. Product mass one follows from Mathlib probability instances.

\[\gamma=(\gamma_E\otimes\gamma_E)\otimes(\gamma_E^{\otimes\iota}\otimes\gamma_E^{\otimes\iota}).\]
Corresponding Lean step

stdGaussian, Measure.prod and Measure.pi construct the explicit law gamma.

3. Construct the first refreshed trajectory and layer

h≥0 makes the refresh variance nonnegative. Coordinate projections, finite sums, scalar multiplication and addition are measurable. C2 regularity makes grad V continuous, so the stopped q and each stochastic-gradient evaluation preserve measurability.

\[P_0=aP+\sigma\zeta_0,\quad Y_i^0=X+t_iP_0,\quad Z_j^0=\nabla V(q(Y_j^0)+\sqrt\eta G_j^0),\quad Y_i^1=Y_i^0-\sum_j\omega_{ij}Z_j^0.\]
Corresponding Lean step

The gradient is the continuous dual isometry applied to fderiv; hqm, hg and fun_prop certify the entire joint update.

4. Use the second fresh array and complete the phase

The second gradient array evaluates q at the first updated centers, using G1 rather than reusing G0. Separate terminal position and momentum weights produce the second Picard outputs. The final refresh uses zeta1. No node or weight error estimate is assumed in this construction.

\[Z_j^1=\nabla V(q(Y_j^1)+\sqrt\eta G_j^1),\quad X^+=X+hP_0-\sum_j b_jZ_j^1,\quad P^+=a(P_0-\sum_j m_jZ_j^1)+\sigma\zeta_1.\]
Corresponding Lean step

The explicit lets Z1 and the output pair retain both final sums and the second refresh in Phi.

5. Construct the canonical Markov kernel

Combine the identity kernel at the incoming state with the constant probability kernel gamma, and map it by the jointly measurable Phi. At s this product is delta_s tensor gamma. The Dirac-product and composition-of-map identities give the stated pushforward exactly.

\[K(s,\cdot)=\Phi(s,\cdot)_\#\gamma,\qquad a=e^{-h/2},\quad\sigma=\sqrt{1-e^{-h}}.\]
Corresponding Lean step

Kernel.IsMarkovKernel.map proves mass one; Kernel.map_apply, Kernel.prod_apply, Measure.dirac_prod and Measure.map_map prove the exact output law.

Lean verification

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

Lean proof · implemented_phase_kernel

Construct the stopped map once, prove the explicit update jointly measurable, and map the canonical product Markov kernel.

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 implemented_phase_kernel {V : E → ℝ} {κ : ℝ≥0}
    (hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E, (κ : ℝ)⁻¹ * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ ‖v‖ ^ 2)
    {eta c eps : ℝ} (heta : 0 < eta) (hec : eta ≤ c) (hc : c < 1) (heps : 0 < eps)
    (h : ℝ) (hh : 0 ≤ h) (t : ι → ℝ) (omega : ι → ι → ℝ)
    (positionWeight momentumWeight : ι → ℝ) :
    ∃ p q : E → E, ∃ N : E → ℕ,
      Measurable p ∧ Measurable q ∧ Measurable N ∧
      (∀ y, p y + eta • gradient V (p y) = y ∧ ‖q y - p y‖ ≤ eps ∧
        ApproximateProximalExecution.proximalQuery (gradient V) eta eps y (N y + 1) y =
          some (q y, N y + 1)) ∧
      let a := Real.exp (-h / 2)
      let sigma := Real.sqrt (1 - Real.exp (-h))
      let γ := ((stdGaussian E).prod (stdGaussian E)).prod
        ((Measure.pi (fun _ : ι => stdGaussian E)).prod
          (Measure.pi (fun _ : ι => stdGaussian E)))
      let Φ := fun w : (E × E) × ((E × E) × ((ι → E) × (ι → E))) =>
        let P0 := a • w.1.2 + sigma • w.2.1.1
        let Y0 := fun i => w.1.1 + t i • P0
        let Z0 := fun j => gradient V (q (Y0 j) + Real.sqrt eta • w.2.2.1 j)
        let Y1 := fun i => Y0 i - ∑ j, omega i j • Z0 j
        let Z1 := fun j => gradient V (q (Y1 j) + Real.sqrt eta • w.2.2.2 j)
        (w.1.1 + h • P0 - ∑ j, positionWeight j • Z1 j,
          a • (P0 - ∑ j, momentumWeight j • Z1 j) + sigma • w.2.1.2)
      0 ≤ 1 - Real.exp (-h) ∧
      Measurable Φ ∧ ∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
        ∀ s, K s = γ.map (fun z => Φ (s, z)) := by
  classical
  obtain ⟨p, N, hp, hN, hq, hall⟩ :=
    ApproximateProximalExecution.approximate_proximal_execution
      hκ hV hH heta hec hc heps
  let q := fun y => (fun x : E => y - eta • gradient V x)^[N y] y
  have hqm : Measurable q := hq
  refine ⟨p, q, N, hp, hqm, hN, fun y =>
    ⟨(hall y).1, (hall y).2.2.2.2.1, (hall y).2.2.2.2.2.2⟩, ?_⟩
  dsimp only
  have hg : Measurable (gradient V) := by
    unfold gradient
    exact ((InnerProductSpace.toDual ℝ E).symm.continuous.comp
      (hV.continuous_fderiv (by norm_num))).measurable
  let γ := ((stdGaussian E).prod (stdGaussian E)).prod
    ((Measure.pi (fun _ : ι => stdGaussian E)).prod
      (Measure.pi (fun _ : ι => stdGaussian E)))
  let Φ := fun w : (E × E) × ((E × E) × ((ι → E) × (ι → E))) =>
    let P0 := Real.exp (-h / 2) • w.1.2 + Real.sqrt (1 - Real.exp (-h)) • w.2.1.1
    let Y0 := fun i => w.1.1 + t i • P0
    let Z0 := fun j => gradient V (q (Y0 j) + Real.sqrt eta • w.2.2.1 j)
    let Y1 := fun i => Y0 i - ∑ j, omega i j • Z0 j
    let Z1 := fun j => gradient V (q (Y1 j) + Real.sqrt eta • w.2.2.2 j)
    (w.1.1 + h • P0 - ∑ j, positionWeight j • Z1 j,
      Real.exp (-h / 2) • (P0 - ∑ j, momentumWeight j • Z1 j) +
        Real.sqrt (1 - Real.exp (-h)) • w.2.1.2)
  have hΦ : Measurable Φ := by
    dsimp only [Φ]
    fun_prop
  let K := (Kernel.id ×ₖ Kernel.const (E × E) γ).map Φ
  have hK : IsMarkovKernel K := Kernel.IsMarkovKernel.map _ hΦ
  refine ⟨sub_nonneg.mpr (Real.exp_le_one_iff.mpr (by linarith)),
    hΦ, K, hK, fun s => ?_⟩
  dsimp only [K]
  rw [Kernel.map_apply _ hΦ, Kernel.prod_apply, Kernel.id_apply, Kernel.const_apply,
    Measure.dirac_prod, Measure.map_map hΦ (by fun_prop)]
  rfl

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseKernel

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
The normalized C2 Hessian bounds and Algorithm D.2 parameter range.V is C2, kappa >= 1 and kappa^(-1)||v||^2 <= D2V(x)[v,v] <= ||v||^2 for every x,v. 0 < eta <= c < 1, eps > 0 and h >= 0.sameThe parent supplies the actual finite stopping certificate. h=0 includes a degenerate limiting phase without enlarging the sampling schedule.
Algorithm 3.1 uses source Chebyshev–Lobatto nodes and integral weights.t, omega, positionWeight and momentumWeight are supplied finite real arrays. Their source quadrature definitions and bounds are not conclusions of this interface.generalizationThis constructs the finite coefficient-parametric implementation interface. Identifying these arrays with the source definitions is explicitly unproved; no source convergence credit follows.
Independent standard Gaussian variables in Algorithm 3.1.Two standard Gaussian factors and two finite independent Gaussian-array factors, followed by an explicit joint measurable update.source-implicitCanonical product probability laws and Borel measurability supply omitted stochastic semantics; no moment or integrability premise is needed just to define a Markov kernel.
A Euclidean state space with J>=2 nodes and positive phase length.An arbitrary complete finite-dimensional real inner-product Borel space, finite index type and nonnegative h.generalizationThe purely measurable phase construction also includes degenerate dimensions, empty arrays and h=0. Source schedules remain obligations of consumers.

One actual gradient-only two-layer phase with supplied finite deterministic coefficients. The Chebyshev-Lobatto coefficient construction and instantiation, repeated phase law, state/moment bounds, local and accumulated error, expected work, terminal FORS, proxy warmness and both main theorems remain separate.

Encoder–denoiser: source-reviewed · equivalent-after-elaboration

Detected semantic differences

  • domains: The attributed component generalizes the source Euclidean domain to finite-dimensional real inner-product Borel spaces and allows arbitrary finite index types and h=0. These are disclosed scope extensions of kernel existence, not claims that every input realizes the source numerical scheme. — Independent reviewer classification explicit-elaboration in packet-bound phase.review-result.json; accepted with no blocker.
  • scopes: The deterministic coefficient adapter remains unproved here. The source instantiation requires t_j and weights from (3.6), with positionWeight_j=omega_{J,j} and momentumWeight_j=omega_j. The publication explicitly retains this obligation. — Independent reviewer classification explicit-elaboration in packet-bound phase.review-result.json; accepted with no blocker.
  • conclusion: Joint measurability and the explicit probability-kernel construction are Samplinglib additions to the implementation component. They preserve the source update formulas without promoting the source convergence or complexity results. — Independent reviewer classification explicit-elaboration in packet-bound phase.review-result.json; accepted with no blocker.

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
  • One actual gradient-only two-layer phase with supplied finite deterministic coefficients. The Chebyshev-Lobatto coefficient construction and instantiation, repeated phase law, state/moment bounds, local and accumulated error, expected work, terminal FORS, proxy warmness and both main theorems remain separate.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • ProbabilityTheory.stdGaussian
  • MeasureTheory.Measure.pi
  • ProbabilityTheory.Kernel.IsMarkovKernel.map
  • ProbabilityTheory.Kernel.prod_apply
  • MeasureTheory.Measure.dirac_prod
  • MeasureTheory.Measure.map_map

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.

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual jointly measurable two-layer implemented phase and exact probability law
  • TODO — not closed by these contributions Source Chebyshev–Lobatto coefficient construction and instantiation (remaining)
  • TODO — not closed by these contributions Repeated-run error, moment and actual-input work estimates (remaining)