SNIS dominates rejection for snapshot reuse: cost factor 1+χ²(π_t‖π_s) = Z_s Z_{2t−s}/Z_t² ≤ 1/p_acc = e^η Z_s/Z_t ≤ e^{2η} under tilt ≤ η
For all , and , if (given and ), then
What the notation means · or point at any symbol
- Type
- Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Type) - Fintype
- Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fintype) - f(x)Function application
- Fintype applied to J. Lean writes f x; papers write f(x). (
Fintype J) - Nonempty
- Nonempty: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Nonempty) - ⟹Implies
- If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (
J → ℝ) - x : TVariables
- s, t range over J → ℝ: the statement must hold for every choice. (
(s t : J → ℝ)) - ∀For all
- The statement after the comma holds for every j. (
∀ j, |t j - s j| ≤ η) - a/bDivision
- (∑ k, exp(s(k))) · (∑ k, exp(2 · t(k) − s(k))) divided by (∑ k, exp(t(k)))^2. In Lean, dividing by 0 gives 0. (
(∑ k, Real.exp (s k)) * (∑ k, Real.exp …) - ∧And
- Both hold: (∑ k, exp(s(k))) · (∑ k, exp(2 · t(k) − s(k)))/(∑ k, exp(t…, and 1/(exp(−η) · (∑ k, exp(t(k)))/(∑ k, exp(s(k)))) ≤ exp(2 · η). (
(∑ k, Real.exp (s k)) * (∑ k, Real.exp …) - ∑Summation
- Add up exp(s(k)) for every k. (
∑ k, Real.exp (s k)) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - |x|Absolute value
- The size of t(j) − s(j) without its sign. (
|t j - s j|) - ≤At most
- |t(j) − s(j)| is less than or equal to η. (
|t j - s j| ≤ η) - -Subtraction
- t(j) minus s(j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
t j - s j) - eˣExponential function
- e raised to the power s(k), where e ≈ 2.718. (
Real.exp (s k)) - ·Multiplication
- 2 times t(k). (
2 * t k) - aᵇPower
- ∑ k, exp(t(k)) raised to the power 2. (
(∑ k, Real.exp (t k)) ^ 2) - −xNegation
- The negative of η. (
-η)
theorem drift-snis-dominates-rejection {J : Type} [Fintype J] [Nonempty J] (s t : J → ℝ) (η : ℝ) (hη : ∀ j, |t j - s j| ≤ η) :
(∑ k, Real.exp (s k)) * (∑ k, Real.exp (2 * t k - s k)) / (∑ k, Real.exp (t k)) ^ 2 ≤ 1 / (Real.exp (-η) * (∑ k, Real.exp (t k)) / ∑ k, Real.exp (s k)) ∧ 1 / (Real.exp (-η) * (∑ k, Real.exp (t k)) / ∑ k, Real.exp (s k)) ≤ Real.exp (2 * η)For decode reuse from a stale snapshot with tilt |t − s| ≤ η, self-normalised importance sampling (made unbiased by MLMC, cost self-certified) uses every draw, at cost factor 1+χ² = Z_s Z_{2t−s}/Z_t², while rejection keeps only accepted draws and needs 1/p_acc = e^η Z_s/Z_t draws per exact sample. Since Z_{2t−s} = Σ_j e^{t_j}e^{t_j−s_j} ≤ e^η Z_t, we get 1+χ² ≤ 1/p_acc ≤ e^{2η}: at equal variance the SNIS variant reads no more keys than rejection, and the gap can be large when the drift is concentrated on low-mass keys. The general comparison of importance sampling with rejection sampling is classical (Liu, Statistics and Computing 1996, credited); this is its specialisation to snapshot reuse in the Drift Law. Trade-off: rejection gives exact samples (one-pass gradient), SNIS needs the MLMC correction and the three-call gradient.
How it was proved
- Proved
- 5 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 41 lines of Lean