Provedunbiased-attentionrandomized-algorithmssoftmaxdebiasing

Matched geometric rates (c_l V_l = A) give optimal cost × variance = L²·A

For all $\htmlData{mx=1}{L \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{c, V : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{L}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ and $\htmlData{mx=1}{A \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{A}$ and $\htmlData{mx=9}{\forall l,\ \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{c}(\htmlData{mx=1}{l})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{V}(\htmlData{mx=4}{l})}} \mathrel{\htmlData{mx=8}{=}} \htmlData{mx=7}{A}}$ , then

\htmlData{mx=9}{\left(\htmlData{mx=8}{\sum_{l} \htmlData{mx=7}{\sqrt{\htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{c}(\htmlData{mx=1}{l})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{V}(\htmlData{mx=4}{l})}}}}}\right)^{2}} \mathrel{\htmlData{mx=15}{=}} \htmlData{mx=14}{\htmlData{mx=12}{\htmlData{mx=11}{\htmlData{mx=10}{L}}^{2}} \cdot \htmlData{mx=13}{A}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
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)
f(x)Function application: Fin applied to L. Lean writes f x; papers write f(x). (Fin L)
⟹Implies: If Fin(L), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin L → ℝ)
x : TVariables: c, V range over Fin L → ℝ: the statement must hold for every choice. ((c V : Fin L → ℝ))
≤At most: 0 is less than or equal to A. (0 ≤ A)
∀For all: The statement after the comma holds for every l. (∀ l, c l * V l = A)
aᵇPower: ∑ l, √(c(l) · V(l)) raised to the power 2. ((∑ l, Real.sqrt (c l * V l)) ^ 2)
∑Summation: Add up √(c(l) · V(l)) for every l. (∑ l, Real.sqrt (c l * V l))
·Multiplication: c(l) times V(l). (c l * V l)
=Equality: c(l) · V(l) and A are the same. (c l * V l = A)
√Square root: The non-negative number whose square is c(l) · V(l). (Real.sqrt (c l * V l))
RReal numbers: The real numbers: every point on the number line. (ℝ)
(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 ua-geometric-levels-cost-variance {L : ℕ} (c V : Fin L → ℝ) (A : ℝ) (hA : 0 ≤ A) (hcv : ∀ l, c l * V l = A) :
    (∑ l, Real.sqrt (c l * V l)) ^ 2 = (L : ℝ) ^ 2 * A

With level cost 2^l and level variance A·2^{-l} (β = γ = 1) every term is √A, so the optimum is L²A = O(A log² n) for L = log₂ n levels. With antithetic coupling (β = 2 > γ = 1, Blanchet–Glynn) the sum converges instead. Part of 'Unbiased randomized attention: cost x variance thresholds' (open theory problem).

How it was proved

Proved: 4 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: 12 lines of Lean

Matched geometric rates (c_l V_l = A) give optimal cost × variance = L²·A

How it was proved

More proved statements