Provedunbiased-attentionend-to-endsoftmaxlower-bound

Counting: the (k+1)-subsets of Fin n containing a fixed point number choose (n−1) k

For all $\htmlData{mx=1}{n, k \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=3}{p \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}}}$ :

\begin{aligned} & \htmlData{mx=37}{\lvert \htmlData{mx=36}{\htmlData{mx=31}{\operatorname{filter}\left(\htmlData{mx=30}{\htmlData{mx=25}{\operatorname{powersetCard}}(\htmlData{mx=27}{\htmlData{mx=26}{k} + 1}, \htmlData{mx=29}{\htmlData{mx=28}{\operatorname{univ}}})}\right)}(\htmlData{mx=35}{S \mapsto \htmlData{mx=32}{p} \mathrel{\htmlData{mx=34}{\in}} \htmlData{mx=33}{S}})} \rvert} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=41}{\binom{\htmlData{mx=39}{\htmlData{mx=38}{n} - 1}}{\htmlData{mx=40}{k}}} \end{aligned}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables: n, k range over natural numbers: the statement must hold for every choice. ((n k : ℕ))
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 n. Lean writes f x; papers write f(x). (Fin n)
|s|Cardinality: The number of elements of filter(powersetCard(k + 1, univ))(S ↦ p ∈ S). (((Finset.powersetCard (k + 1) (Finset.u…)
=Equality: card(filter(powersetCard(k + 1, univ))(S ↦ p ∈ S)) and choose(n − 1, k) are the same. (((Finset.powersetCard (k + 1) (Finset.u…)
e.ffilter: filter of powersetCard(k + 1, univ): Lean's dot notation e.filter means filter applied to e. ((Finset.powersetCard (k + 1) (Finset.un…)
powersetCard: Finset.powersetCard: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.powersetCard)
+Addition: k plus 1. (k + 1)
(x : T)Type ascription: univ read as a Finset(Fin(n)). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((Finset.univ : Finset (Fin n)))
univ: Finset.univ: 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)
x ↦ f(x)Function (λ-abstraction): The function sending S to p ∈ S. Lean writes fun x => …; papers write x ↦ …. (fun S => p ∈ S)
∈Element of: p is a member of S. (p ∈ S)
(n k)Binomial coefficient: “n − 1 choose k”: the number of ways to pick k things from n − 1. (Nat.choose (n - 1) k)
-Subtraction: n minus 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (n - 1)

theorem ua-subsets-containing-point {n k : ℕ} (p : Fin n) :
    ((Finset.powersetCard (k + 1) (Finset.univ : Finset (Fin n))).filter (fun S => p ∈ S)).card = Nat.choose (n - 1) k

Via powersetCard_succ_insert on univ = insert p (univ.erase p): subsets of the erased set never contain p, and the image part under insert p is injective on them. Part of 'Unbiased randomized attention: cost x variance thresholds' (end-to-end composition round).

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

Counting: the (k+1)-subsets of Fin n containing a fixed point number choose (n−1) k

How it was proved

More proved statements