Provedattention-compute-lawheadline-theoremconversion-theoremimportance-sampling
Attention Compute Law, conversion form (one statement): a coin-dependent ε-oracle yields an exactly unbiased importance sampler with expected cost ≤ Z²F²[(1+2ε)^L + L2^Lq((1+2ε)/ε)^L]
For all , , , , , , , , , and , if , , , , , , , , , , and (given ), then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - 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 Ω. Lean writes f x; papers write f(x). (
Fintype Ω) - ⟹Implies
- If Ω, then ℝ. (Between types, A → B is the type of functions from A to B.) (
Ω → ℝ) - ∀For all
- The statement after the comma holds for every ω. (
∀ ω, 0 ≤ w ω) - ∑Summation
- Add up w(ω) for every ω. (
∑ ω, w ω) - =Equality
- ∑ ω, w(ω) and 1 are the same. (
∑ ω, w ω = 1) - x ∈ TVariables
- ε, q range over real numbers: the statement must hold for every choice. (
(ε q : ℝ)) - <Less than
- 0 is strictly smaller than ε. (
0 < ε) - x : TVariables
- pt, Q range over Ω → ℕ → (Fin L → Bool) → ℝ: the statement must hold for every choice. (
(pt Q : Ω → ℕ → (Fin L → Bool) → ℝ)) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ≤At most
- 0 is less than or equal to w(ω). (
0 ≤ w ω) - Bool
- Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Bool) - πPi
- The ratio of a circle's circumference to its diameter, ≈ 3.14159. (
π) - eˣExponential function
- e raised to the power s(b), where e ≈ 2.718. (
Real.exp (s b)) - maxMaximum
- The larger of 0 and min(1, phat(ω, ℓ, b)). (
max 0 (min 1 (phat ω ℓ b))) - ∏Product
- Multiply together Q(ω, ℓ, b) for ℓ = 0, 1, …, L − 1. (
∏ ℓ ∈ Finset.range L, Q ω ℓ b) - minMinimum
- The smaller of 1 and phat(ω, ℓ, b). (
min 1 (phat ω ℓ b)) - then
- then: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
then) - { a if c; b otherwiseCases (if … then … else)
- π(b') when ∀ i, i < ℓ → b'(i) = b(i), and 0 otherwise. (
if (∀ i : Fin L, (i : ℕ) < ℓ → b' i = b…) - filter
- Finset.univ.filter: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Finset.univ.filter) - (x : T)As natural numbers
- i read as an element of natural numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(i : ℕ)) - ·Multiplication
- 2 times ε. (
2 * ε) - x ↦ f(x)Function (λ-abstraction)
- The function sending ω to 0 < m(ℓ, b) ∧ ε < |phat(ω, ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, …. Lean writes fun x => …; papers write x ↦ …. (
fun ω => 0 < m ℓ b ∧ ε < |phat ω ℓ b - …) - ∧And
- Both hold: 0 < m(ℓ, b), and ε < |phat(ω, ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ…. (
0 < m ℓ b ∧ ε < |phat ω ℓ b - m (ℓ + 1)…) - |x|Absolute value
- The size of phat(ω, ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b) without its sign. (
|phat ω ℓ b - m (ℓ + 1) (Function.updat…) - -Subtraction
- phat(ω, ℓ, b) minus m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
phat ω ℓ b - m (ℓ + 1) (Function.update…) - a/bDivision
- m(ℓ + 1, update(b, ⟨ℓ, h⟩, true)) divided by m(ℓ, b). In Lean, dividing by 0 gives 0. (
m (ℓ + 1) (Function.update b ⟨ℓ, h⟩ tru…) - +Addition
- ℓ plus 1. (
ℓ + 1) - update
- Function.update: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Function.update) - ⟨a, b⟩Anonymous constructor
- Builds a structure (a pair, a subtype element, …) from ℓ, h. (
⟨ℓ, h⟩) - true
- true: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
true) - aᵇPower
- exp(s(b)) · v(b)/(∏ ℓ, Q(ω, ℓ, b)) raised to the power 2. (
(Real.exp (s b) * v b / ∏ ℓ ∈ Finset.ra…) - (x : T)As real numbers
- L read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(L : ℝ))
theorem attention-compute-law-conversion-form {L : ℕ} {Ω : Type} [Fintype Ω] (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (π : (Fin L → Bool) → ℝ) (hπ : ∀ b, 0 ≤ π b) (hπs : ∑ b, π b = 1) (ε q : ℝ) (hε : 0 < ε) (m : ℕ → (Fin L → Bool) → ℝ) (hm : ∀ ℓ b, m ℓ b = ∑ b' : Fin L → Bool, (if (∀ i : Fin L, (i : ℕ) < ℓ → b' i = b i) then π b' else 0)) (phat : Ω → ℕ → (Fin L → Bool) → ℝ) (hpre : ∀ ω ℓ (b b' : Fin L → Bool), (∀ i : Fin L, (i : ℕ) < ℓ → b i = b' i) → phat ω ℓ b = phat ω ℓ b') (hfail : ∀ ℓ (h : ℓ < L) (b : Fin L → Bool), ∑ ω ∈ Finset.univ.filter (fun ω => 0 < m ℓ b ∧ ε < |phat ω ℓ b - m (ℓ + 1) (Function.update b ⟨ℓ, h⟩ true) / m ℓ b|), w ω ≤ q) (pt Q : Ω → ℕ → (Fin L → Bool) → ℝ) (hpt : ∀ ω ℓ b, pt ω ℓ b = (max 0 (min 1 (phat ω ℓ b)) + ε) / (1 + 2 * ε)) (hQ : ∀ ω ℓ b, Q ω ℓ b = if h : ℓ < L then (if b ⟨ℓ, h⟩ then pt ω ℓ b else 1 - pt ω ℓ b) else 1) (s v : (Fin L → Bool) → ℝ) (Z F : ℝ) (hZ : Z = ∑ b, Real.exp (s b)) (hπdef : ∀ b, π b = Real.exp (s b) / Z) (hv : ∀ b, |v b| ≤ F) :
(∀ ω, ∑ b : Fin L → Bool, (∏ ℓ ∈ Finset.range L, Q ω ℓ b) * (Real.exp (s b) * v b / ∏ ℓ ∈ Finset.range L, Q ω ℓ b) = ∑ b, Real.exp (s b) * v b) ∧ (∀ ω, ∑ b : Fin L → Bool, (∏ ℓ ∈ Finset.range L, Q ω ℓ b) * (Real.exp (s b) / ∏ ℓ ∈ Finset.range L, Q ω ℓ b) = Z) ∧ (∀ ω, ∑ b : Fin L → Bool, (∏ ℓ ∈ Finset.range L, Q ω ℓ b) * (Real.exp (s b) * v b / ∏ ℓ ∈ Finset.range L, Q ω ℓ b) ^ 2 ≤ Z ^ 2 * F ^ 2 * ∑ b : Fin L → Bool, π b ^ 2 / ∏ ℓ ∈ Finset.range L, Q ω ℓ b) ∧ ∑ ω, w ω * ∑ b : Fin L → Bool, (∏ ℓ ∈ Finset.range L, Q ω ℓ b) * (Real.exp (s b) * v b / ∏ ℓ ∈ Finset.range L, Q ω ℓ b) ^ 2 ≤ Z ^ 2 * F ^ 2 * ((1 + 2 * ε) ^ L + ((L : ℝ) * 2 ^ L * q) * ((1 + 2 * ε) / ε) ^ L)The capstone's upper side, end-to-end in one statement: algorithm → proposal → exactly unbiased estimator with a quantified cost. For attention scores s (Z = Σe^s, π = e^s/Z) and values |v| ≤ F over 2^L keys, any coin-dependent node oracle that is ε-accurate except with probability q per node induces the smoothed descent proposal r_ω; then for every coin outcome (1) importance sampling from r_ω is exactly unbiased for the numerator Σ e^{s}v and (2) for the normaliser Z, (3) its second moment is at most Z²F²·Σπ²/r_ω, and (4) averaged over the coins the second moment is at most Z²F²·[(1+2ε)^L + L·2^L·q·((1+2ε)/ε)^L]. The end-to-end Randomized Conversion Theorem (rc-randomized-conversion-end-to-end, itself embedding the deterministic Conversion Theorem) is embedded. The ratio numerator/Z is debiased by randomised MLMC (ua-end-to-end-mlmc), not re-proved here.
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
- 397 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.