Samplinglib mathematical lesson

A gradient-query interpreter that counts the successful test

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution.proximalQuery · def · Teaching coverage

Read this first

Mathematical statement

With no fuel return none. Otherwise evaluate g at x, form z=y−eta g(x), and test the residual. Success returns the current x and count one. Failure recurses at z with one less fuel and adds one to a successful returned count; unsuccessful recursion returns none.

\[Q_0(x)=\mathrm{none},\qquad Q_{m+1}(x)=\begin{cases}\mathrm{some}(x,1),&\|y-\eta g(x)-x\|\le(1-\eta)\varepsilon,\\\mathrm{map}((u,k)\mapsto(u,k+1),Q_m(y-\eta g(x))),&\text{otherwise}.\end{cases}\]

Lean statement · proximalQuery

The adjacent disclosure extracts the exact oracle, real parameters, natural fuel, and Option-valued return type from 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)

noncomputable def proximalQuery (g : E → E) (eta eps : ℝ) (y : E) :
    ℕ → E → Option (E × ℕ)
  | 0, _ => none
  | n+1, x => by
    classical
    let z := y-eta • g x
    exact if ‖z-x‖ ≤ (1-eta)*eps then some (x,1)
      else (proximalQuery g eta eps y n z).map (fun r => (r.1,r.2+1))

Exact module and namespace context

Proof roadmap

1Spend one query before testing
Even an immediately successful residual test needs the gradient at the current point. The let-bound z represents that single oracle evaluation. Mathematical arithmetic and comparison are exact; this is not a numerical-roundoff model.
2Return the tested point, not the next point
The certificate in the companion theorem controls the error at x through the residual between x and z. Therefore the successful branch returns x. Each unsuccessful level contributes exactly one additional query to the recursively returned count.

Full assumptions and notation

All objects and hypotheses

E is a real normed vector space. g:E→E is an arbitrary oracle, eta and eps are real parameters, y is the fixed center, x is the current point, and fuel is a natural number. No regularity or positivity is required just to define the interpreter.

Construction and meaning

1. Spend one query before testing

Even an immediately successful residual test needs the gradient at the current point. The let-bound z represents that single oracle evaluation. Mathematical arithmetic and comparison are exact; this is not a numerical-roundoff model.

\[z=y-\eta g(x),\qquad r=\|z-x\|.\]

Corresponding Lean step

The positive-fuel branch binds z before the if; success is some (x,1).

2. Return the tested point, not the next point

The certificate in the companion theorem controls the error at x through the residual between x and z. Therefore the successful branch returns x. Each unsuccessful level contributes exactly one additional query to the recursively returned count.

\[\mathrm{returned\ point}=x,\qquad\mathrm{count}=1+\mathrm{recursive\ count}.\]

Corresponding Lean step

Option.map preserves failure and increments only the count in a successful pair; run_first_stop proves the recurrence's execution equation.

Lean verification

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

Lean construction · proximalQuery

This is a recursive definition, not an independently proved accuracy theorem. Its execution is certified by approximate_proximal_execution.

Download module (.lean)

noncomputable def proximalQuery (g : E → E) (eta eps : ℝ) (y : E) :
    ℕ → E → Option (E × ℕ)
  | 0, _ => none
  | n+1, x => by
    classical
    let z := y-eta • g x
    exact if ‖z-x‖ ≤ (1-eta)*eps then some (x,1)
      else (proximalQuery g eta eps y n z).map (fun r => (r.1,r.2+1))

Exact module and namespace context

Scope and omitted-condition boundaries

Exact-real noncomputable finite-fuel semantics, not floating-point software. This definition alone proves neither termination nor accuracy. It records output and count, not a query-list trace.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Option.map

Mathematical sources

Chen–Chewi–Lu–Zhang, SPHMC Algorithm D.2 — Attributed paraphrase; Samplinglib's finite-fuel representation is explicit implementation structure.

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