Provedunbiased-attentionrandomized-algorithmssoftmaxeasy-side

i.i.d. sums on a finite product space: E[(Σᵢ Xᵢ)²] = N·E[X²] when E[X] = 0

For all $\htmlData{mx=1}{\Omega \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=1}{N \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=3}{w, X : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , if $\htmlData{mx=3}{\sum_{\omega} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}} \mathrel{\htmlData{mx=4}{=}} 1$ and $\htmlData{mx=7}{\sum_{\omega} \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{X}(\htmlData{mx=4}{\omega})}}} \mathrel{\htmlData{mx=8}{=}} 0$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega}}$ ), then

\begin{aligned} & \htmlData{mx=20}{\sum_{f : \htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{N}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\Omega}} \htmlData{mx=19}{\left(\htmlData{mx=11}{\prod_{k} \htmlData{mx=10}{\htmlData{mx=6}{w}(\htmlData{mx=9}{\htmlData{mx=7}{f}(\htmlData{mx=8}{k})})}}\right) \cdot \htmlData{mx=18}{\left(\htmlData{mx=17}{\sum_{i} \htmlData{mx=16}{\htmlData{mx=12}{X}(\htmlData{mx=15}{\htmlData{mx=13}{f}(\htmlData{mx=14}{i})})}}\right)^{2}}}} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=31}{\htmlData{mx=21}{N} \cdot \htmlData{mx=30}{\sum_{\omega} \htmlData{mx=29}{\htmlData{mx=24}{\htmlData{mx=22}{w}(\htmlData{mx=23}{\omega})} \cdot \htmlData{mx=28}{\htmlData{mx=27}{\htmlData{mx=25}{X}(\htmlData{mx=26}{\omega})}^{2}}}}} \end{aligned}

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 Ω)
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.) (Ω → ℝ)
x : TVariables: w, X range over Ω → ℝ: the statement must hold for every choice. ((w X : Ω → ℝ))
∑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. (ℝ)
·Multiplication: w(ω) times X(ω). (w ω * X ω)
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)
∏Product: Multiply together w(f(k)) for every k. (∏ k, w (f k))
aᵇPower: ∑ i, X(f(i)) raised to the power 2. ((∑ i, X (f i)) ^ 2)

theorem ua-iid-sum-second-moment {Ω : Type} [Fintype Ω] {N : ℕ} (w X : Ω → ℝ) (hsum : ∑ ω, w ω = 1) (hmean : ∑ ω, w ω * X ω = 0) :
    ∑ f : Fin N → Ω, (∏ k, w (f k)) * (∑ i, X (f i)) ^ 2 = N * ∑ ω, w ω * X ω ^ 2

Fully formal over Ω^N with product weights ∏ w(f k): cross terms factor and vanish, diagonal terms give N·E X². The probabilistic core of every variance bound here. Part of 'Unbiased randomized attention: cost x variance thresholds' (open theory problem), round 2.

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

i.i.d. sums on a finite product space: E[(Σᵢ Xᵢ)²] = N·E[X²] when E[X] = 0

How it was proved

More proved statements