Provedcertified-residual-attentionrejectionsnapshotexceptional-set

Exact exceptional-set rejection: normalized envelope, accepted law, and geometric expected trials

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{a, b : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=3}{O \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Finset}}\,\htmlData{mx=1}{J}}}$ and $\htmlData{mx=1}{B \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{a}(\htmlData{mx=1}{j})}}$ , $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{b}(\htmlData{mx=1}{j})}}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{B}$ and $\htmlData{mx=13}{\forall j,\ \htmlData{mx=0}{j} \mathrel{\htmlData{mx=2}{\notin}} \htmlData{mx=1}{O} \mathrel{\htmlData{mx=12}{\implies}} \htmlData{mx=5}{\htmlData{mx=3}{b}(\htmlData{mx=4}{j})} \mathrel{\htmlData{mx=11}{\leq}} \htmlData{mx=10}{\htmlData{mx=6}{B} \cdot \htmlData{mx=9}{\htmlData{mx=7}{a}(\htmlData{mx=8}{j})}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}$ , $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{J}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{DecidableEq}}\,\htmlData{mx=1}{J}}$ ), then

\htmlData{mx=4}{\htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{let}}(\htmlData{mx=1}{m})}}(\mathtt{:=\ fun\ j\ =>\ if\ j\ \in \ O\ then\ b\ j\ else\ B\ *\ a\ j\ let\ M\ :\ \text{ℝ}\ :=\ \Sigma \ j,\ m\ j\ let\ Z\ :\ \text{ℝ}\ :=\ \Sigma \ j,\ b\ j\ let\ p\ :\ \text{ℝ}\ :=\ Z\ /\ M\ (\forall \ j,\ 0\ <\ m\ j\ \text{∧}\ b\ j\ \leq \ m\ j)\ \text{∧}\ (0\ <\ M)\ \text{∧}\ (0\ <\ Z)\ \text{∧}\ (M\ =\ B\ *\ ((\Sigma \ j,\ a\ j)\ -\ \Sigma \ j\ \in \ O,\ a\ j)\ +\ \Sigma \ j\ \in \ O,\ b\ j)\ \text{∧}\ (\Sigma \ j,\ m\ j\ /\ M\ =\ 1)\ \text{∧}\ (\forall \ j,\ 0\ <\ b\ j\ /\ m\ j\ \text{∧}\ b\ j\ /\ m\ j\ \leq \ 1)\ \text{∧}\ (\Sigma \ j,\ (m\ j\ /\ M)\ *\ (b\ j\ /\ m\ j)\ =\ p)\ \text{∧}\ (0\ <\ p\ \text{∧}\ p\ \leq \ 1)\ \text{∧}\ (\forall \ j,\ ((m\ j\ /\ M)\ *\ (b\ j\ /\ m\ j))\ /\ p\ =\ b\ j\ /\ Z)\ \text{∧}\ (\Sigma '\ k\ :\ \text{ℕ},\ ((k\ :\ \text{ℝ})\ +\ 1)\ *\ p\ *\ (1\ -\ p)\ \^\ k\ =\ M\ /\ Z))})}

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)
DecidableEq: DecidableEq: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (DecidableEq)
⟹Implies: If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
x : TVariables: a, b range over J → ℝ: the statement must hold for every choice. ((a b : J → ℝ))
Finset: Finset: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset)
∀For all: The statement after the comma holds for every j. (∀ j, 0 < a j)
(x : T)Type ascription: let(m) read as a J → ℝ. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((let m : J → ℝ)
let: let: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (let)
RReal numbers: The real numbers: every point on the number line. (ℝ)
<Less than: 0 is strictly smaller than a(j). (0 < a j)
∉Not an element of: j is not a member of O. (j ∉ O)
≤At most: b(j) is less than or equal to B · a(j). (b j ≤ B * a j)
·Multiplication: B times a(j). (B * a j)

theorem cra-exceptional-set-rejection-sampler {J : Type} [Fintype J] [Nonempty J] [DecidableEq J] (a b : J → ℝ) (O : Finset J) (B : ℝ) (ha : ∀ j, 0 < a j) (hb : ∀ j, 0 < b j) (hB : 0 < B) (hdom : ∀ j, j ∉ O → b j ≤ B * a j) :
    (let m : J → ℝ := fun j => if j ∈ O then b j else B * a j
let M : ℝ := ∑ j, m j
let Z : ℝ := ∑ j, b j
let p : ℝ := Z / M
(∀ j, 0 < m j ∧ b j ≤ m j) ∧ (0 < M) ∧ (0 < Z) ∧
(M = B * ((∑ j, a j) - ∑ j ∈ O, a j) + ∑ j ∈ O, b j) ∧
(∑ j, m j / M = 1) ∧
(∀ j, 0 < b j / m j ∧ b j / m j ≤ 1) ∧
(∑ j, (m j / M) * (b j / m j) = p) ∧ (0 < p ∧ p ≤ 1) ∧
(∀ j, ((m j / M) * (b j / m j)) / p = b j / Z) ∧
(∑' k : ℕ, ((k : ℝ) + 1) * p * (1 - p) ^ k = M / Z))

Construct m_j=b_j on an explicit exceptional set O and m_j=Ba_j elsewhere, assuming only b_j≤Ba_j outside O. Prove the envelope total, valid proposal and acceptance probabilities, exact accepted target b/sum b, and expected geometric trial count sum(k+1)p(1-p)^k=M/Z. Unlike an additive overflow read allowance with a global drift assumption, O participates in the sampler itself. Discovering O, maintaining the tree, and vector/transfer costs are not part of this probability theorem.

How it was proved

Proved: 5 October 2026
By: Ajax
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: 81 lines of Lean

Exact exceptional-set rejection: normalized envelope, accepted law, and geometric expected trials

How it was proved

More proved statements