Samplinglib mathematical lesson

Counted phase program

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgram.phaseQuery · def · Teaching coverage

Read this first

Mathematical statement

For arbitrary real normed E, gradient oracle g, eta,eps,h, Fin m nodes and weights, input w and fuel:E→Nat, phaseQuery returns Option((E*E)*Nat). It first refreshes P0 and builds Y0. It sequentially executes every proximalQuery at Y0_i from Y0_i using fuel(Y0_i), and if successful evaluates g at returned point plus sqrt(eta)G0_i and adds one query to that returned count. It builds Y1 from these actual returned gradients, sequentially executes every second proximal/noisy-gradient call similarly using G1, then returns the complete phase output and the sum of both arrays actual counts. Any failed call returns none, with no successful cost certificate.

\[T=2m+\sum_{i=0}^{m-1}\bigl[N(Y_i^0)+1+N(Y_i^1)+1\bigr],\quad \mathbb E_\mu T\le m(2+L_0+L_1).\]

Lean statement · phaseQuery

Exact finite arrays, full input/return types, parameters and counting boundary are retained in Lean.

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)

def phaseQuery {m : ℕ} (g : E → E) (eta eps h : ℝ)
    (t : Fin m → ℝ) (omega : Fin m → Fin m → ℝ)
    (positionWeight momentumWeight : Fin m → ℝ) (fuel : E → ℕ)
    (w : (E × E) × ((E × E) × ((Fin m → E) × (Fin m → E)))) :
    Option ((E × E) × ℕ)

Exact module and namespace context

Proof roadmap

1Execute a finite successful query array
Induct on the finite array size. The empty array returns count zero. For a nonempty array, execute index zero, then the tail, returning the actual vector of outputs and the sum of their returned counts. Fin.cons reconstruction and Fin.sum_univ_succ identify the complete returned vector and count. This helper has no probabilistic or termination premise beyond the individual successful calls.
2Run the actual two-layer program
For each first center, run the residual-stopped proximal interpreter and evaluate the Gaussian-shifted gradient of its returned point, adding one direct query. Construct the second centers using these actual first returned gradients; run the second array in the same manner. Form the full updated state including both half-refreshes from the second returned gradients. In both layers each proximal count N(Y)+1 already includes its terminal successful residual test. Thus the returned count is the sum of both arrays plus exactly 2*m direct gradient evaluations. Failed insufficient-fuel calls return none.

Full assumptions and notation

All objects and hypotheses

E is an arbitrary real normed vector space; g, parameters, supplied finite nodes/weights and fuel are arbitrary. The input contains one state pair, two refresh noises and two Fin-m noise arrays; no probability or success assumption.

Construction and meaning

1. Execute a finite successful query array

Induct on the finite array size. The empty array returns count zero. For a nonempty array, execute index zero, then the tail, returning the actual vector of outputs and the sum of their returned counts. Fin.cons reconstruction and Fin.sum_univ_succ identify the complete returned vector and count. This helper has no probabilistic or termination premise beyond the individual successful calls.

\[\operatorname{collect}(r_i)=(x_i,\sum_i c_i)\quad\text{if }r_i=\operatorname{some}(x_i,c_i).\]

Corresponding Lean step

collectQueries; collectQueries_some

2. Run the actual two-layer program

For each first center, run the residual-stopped proximal interpreter and evaluate the Gaussian-shifted gradient of its returned point, adding one direct query. Construct the second centers using these actual first returned gradients; run the second array in the same manner. Form the full updated state including both half-refreshes from the second returned gradients. In both layers each proximal count N(Y)+1 already includes its terminal successful residual test. Thus the returned count is the sum of both arrays plus exactly 2*m direct gradient evaluations. Failed insufficient-fuel calls return none.

\[T=2m+\sum_{i=0}^{m-1}\bigl[N(Y_i^0)+1+N(Y_i^1)+1\bigr],\quad \mathbb E_\mu T\le m(2+L_0+L_1).\]

Corresponding Lean step

phaseQuery; phaseQuery_success; Finset.sum_add_distrib

Lean verification

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

Lean construction · phaseQuery

The proof steps cover both private execution helpers and the public actual-law total-cost theorem. The definition itself is an execution prerequisite, not a proof edge.

Download module (.lean)

def phaseQuery {m : ℕ} (g : E → E) (eta eps h : ℝ)
    (t : Fin m → ℝ) (omega : Fin m → Fin m → ℝ)
    (positionWeight momentumWeight : Fin m → ℝ) (fuel : E → ℕ)
    (w : (E × E) × ((E × E) × ((Fin m → E) × (Fin m → E)))) :
    Option ((E × E) × ℕ) := do
  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 r0 ← collectQueries m (fun i =>
    (ApproximateProximalExecution.proximalQuery g eta eps (Y0 i) (fuel (Y0 i)) (Y0 i)).map
      (fun r => (g (r.1+Real.sqrt eta • w.2.2.1 i),r.2+1)))
  let Y1 := fun i => Y0 i - ∑ j, omega i j • r0.1 j
  let r1 ← collectQueries m (fun i =>
    (ApproximateProximalExecution.proximalQuery g eta eps (Y1 i) (fuel (Y1 i)) (Y1 i)).map
      (fun r => (g (r.1+Real.sqrt eta • w.2.2.2 i),r.2+1)))
  pure ((w.1.1+h • P0-∑ j, positionWeight j • r1.1 j,
    Real.exp (-h/2) • (P0-∑ j, momentumWeight j • r1.1 j) +
      Real.sqrt (1-Real.exp (-h)) • w.2.1.2),r0.2+r1.2)

Exact module and namespace context

Scope and omitted-condition boundaries

Actual interpreter definition only. Single full Gaussian phase with supplied incoming integrable state L2 budget, finite bounded nodes and row l1 bounds; actual successful exact-real interpreter output and total gradient count. Sufficient finite fuel certifies execution and is not a runtime precomputation or a count/cost hypothesis. No cost claim for failed insufficient-fuel executions. Gaussian sampling and arithmetic are not gradient queries. Source quadrature/J adapter, run-wide D7 induction, D8 parameter/iteration substitution, Wp, proxy-warmness, initialization, PBPS and composition/main results remain open. No TV-to-unbounded-cost transfer.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution.proximalQuery

Mathlib API called (external library)

Fin.sum_univ_succ
MeasureTheory.integrable_finsetSum
MeasureTheory.integral_finsetSum
MeasureTheory.probReal_univ

Mathematical sources

SPHMC actual two-layer phase queries — Actual interpreter definition only. Single full Gaussian phase with supplied incoming integrable state L2 budget, finite bounded nodes and row l1 bounds; actual successful exact-real interpreter output and total gradient count. Sufficient finite fuel certifies execution and is not a runtime precomputation or a count/cost hypothesis. No cost claim for failed insufficient-fuel executions. Gaussian sampling and arithmetic are not gradient queries. Source quadrature/J adapter, run-wide D7 induction, D8 parameter/iteration substitution, Wp, proxy-warmness, initialization, PBPS and composition/main results remain open. No TV-to-unbounded-cost transfer.

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