Provedunbiased-attentionrandomized-algorithmssoftmaxlower-bound

Hitting bound: s i.i.d. draws from w hit a set S with probability ≤ s·w(S)

For all $\htmlData{mx=1}{\Omega \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=1}{s \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=3}{w : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=3}{S \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Finset}}\,\htmlData{mx=1}{\Omega}}}$ , if $\htmlData{mx=4}{\forall \omega,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}}$ and $\htmlData{mx=3}{\sum_{\omega} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}} \mathrel{\htmlData{mx=4}{=}} 1$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{DecidableEq}}\,\htmlData{mx=1}{\Omega}}$ ), then

\htmlData{mx=20}{\sum_{f \in \htmlData{mx=13}{\htmlData{mx=0}{\operatorname{filter}}(\htmlData{mx=12}{f \mapsto \htmlData{mx=6}{\exists i,\ \htmlData{mx=3}{\htmlData{mx=1}{f}(\htmlData{mx=2}{i})} \mathrel{\htmlData{mx=5}{\in}} \htmlData{mx=4}{S}}})}} \htmlData{mx=19}{\prod_{k} \htmlData{mx=18}{\htmlData{mx=14}{w}(\htmlData{mx=17}{\htmlData{mx=15}{f}(\htmlData{mx=16}{k})})}}} \mathrel{\htmlData{mx=28}{\leq}} \htmlData{mx=27}{\htmlData{mx=21}{s} \cdot \htmlData{mx=26}{\sum_{\omega \in \htmlData{mx=22}{S}} \htmlData{mx=25}{\htmlData{mx=23}{w}(\htmlData{mx=24}{\omega})}}}

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 Ω. Lean writes f x; papers write f(x). (Fintype Ω)
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)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
⟹Implies: If Ω, then ℝ. (Between types, A → B is the type of functions from A to B.) (Ω → ℝ)
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 ω. (∀ ω, 0 ≤ w ω)
∑Summation: Add up w(ω) for every ω. (∑ ω, w ω)
=Equality: ∑ ω, w(ω) and 1 are the same. (∑ ω, w ω = 1)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to w(ω). (0 ≤ w ω)
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 ↦ f(x)Function (λ-abstraction): The function sending f to ∃ i, f(i) ∈ S. Lean writes fun x => …; papers write x ↦ …. (fun f : Fin s → Ω => ∃ i, f i ∈ S)
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)
∃There exists: At least one i makes the statement after the comma true. (∃ i, f i ∈ S)
∈Element of: f(i) is a member of S. (f i ∈ S)
∏Product: Multiply together w(f(k)) for every k. (∏ k, w (f k))
·Multiplication: s times ∑ ω, w(ω). (s * ∑ ω ∈ S, w ω)

theorem ua-iid-hitting-bound {Ω : Type} [Fintype Ω] [DecidableEq Ω] {s : ℕ} (w : Ω → ℝ) (S : Finset Ω) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) :
    ∑ f ∈ Finset.univ.filter (fun f : Fin s → Ω => ∃ i, f i ∈ S), ∏ k, w (f k) ≤ s * ∑ ω ∈ S, w ω

Union bound proven exactly on the product space Ω^s. With a planted set of n^{1−α} keys at score α ln n (output ≈ 1/2 versus 0 without it), s uniform draws see the plant with probability ≤ s·n^{−α}; with the two-point bound, any sampling estimator needs Ω(e^R) draws per row for constant MSE: the uniform sampler's e^R is tight for sampling-based estimators. Part of 'Unbiased randomized attention: cost x variance thresholds', round 5 (approximate-score proposals and the sampling lower bound).

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: 45 lines of Lean

Hitting bound: s i.i.d. draws from w hit a set S with probability ≤ s·w(S)

How it was proved

More proved statements